diff --git a/src/equations/tutorial_basics.v b/src/equations/tutorial_basics.v index 28c8dbd..56ef311 100644 --- a/src/equations/tutorial_basics.v +++ b/src/equations/tutorial_basics.v @@ -21,15 +21,15 @@ *** Table of content - - 1. Basic definitions and reasoning - - 1.1 Defining functions by dependent pattern matching + - 1. Basic Definitions and Reasoning + - 1.1 Defining Functions by Dependent Pattern Matching - 1.2 Reasoning with [Equations] - - 1.2.1 Simplifying goals with [autorewrite] - - 1.2.2 Proving properties by functional elimination with [funelim] - - 1.2.3 Discharging trivial goals with [simp] + - 1.2.1 Simplifying Goals with [autorewrite] + - 1.2.2 Proving Properties by Functional Elimination with [funelim] + - 1.2.3 Discharging Trivial Goals with [simp] - 1.2.4 Extending [autorewrite] and [simp] - - 2. With clauses - - 3. Where clauses + - 2. With Clauses + - 3. Where Clauses *** Prerequisites @@ -44,7 +44,7 @@ -(** ** 1. Basic definitions and reasoning +(** ** 1. Basic Definitions and Reasoning Let us start by importing the package: *) @@ -54,7 +54,7 @@ From Equations Require Import Equations. Axiom to_fill : forall A, A. Arguments to_fill {_}. -(** *** 1.1 Defining functions by dependent pattern matching +(** *** 1.1 Defining Functions by Dependent Pattern Matching In its simplest form, [Equations] provides a practical interface to define functions on inductive types by pattern matching and recursion @@ -69,13 +69,13 @@ Inductive list A : Type := Arguments nil {_}. Arguments cons {_} _ _. -(** To write a function [f : list A -> B] on lists or another a basic +(** To write a function [f : list A -> B] on lists or another basic inductive type, it suffices to: - Begin your definition with "[Equations]" rather than "[Fixpoint]". - Specify how the function, [f], computes on each constructor, [cst x1 ... xn], by writing [f (cst x1 ... xn) := t] where [t] may contain [f] recursively. - Separate the different cases by semi-colon "[;]" - - As usual finish you definition by a dot "[.]" + - As usual finish your definition by a dot "[.]" For instance, we can define the functions [tail], [length] and [app] by: *) @@ -131,7 +131,7 @@ app' [] l' := l'; app' (a::l) l' := a :: (app' l l'). (** For the users that would prefer it, there is also an alternative syntax - closer to the the one provided by the [Fixpoint] command and Rocq's native pattern-matching. + closer to the one provided by the [Fixpoint] command and Rocq's native pattern-matching. With this syntax, we have to start each clause with "[|]" and separate the different patterns in a clause by "[,]", but we no longer have to repeat the name of the function nor to put parenthesis or finish a line by "[;]". @@ -226,7 +226,7 @@ Succeed Example testing : fold_right Nat.mul 1 (1::2::3::4::nil) = 24 := eq_refl (** Now that we have seen how to define basic functions, we need to understand how to reason about them. - *** 1.2.1 Simplifying goals + *** 1.2.1 Simplifying Goals with [autorewrite] By default, functions defined using [Equations] are opaque and cannot be unfolded with [unfold] nor simplified with [simpl] or [cbn] as one @@ -320,10 +320,10 @@ Qed. rewrite directly by a specific equation. In particular, compared to [cbn] it will never unfold unwanted terms, like proof terms that would be part of the definition, for instance, when defining - proof carrying functions or defining functions by well-fouded recursion. + proof carrying functions or defining functions by well-founded recursion. *) -(** *** 1.2.2 Proving properties by functional elimination +(** *** 1.2.2 Proving Properties by Functional Elimination with [funelim] In the examples above, [app_nil] and [app_assoc], we mimicked the pattern used in the definition of [app] by [induction l]. @@ -434,7 +434,7 @@ Proof. (* We then get stuck as we have the wrong hypotheses *) Abort. -(* Wheras funelim does it automatically for you *) +(* Whereas funelim does it automatically for you *) Definition half_mod2 (n : nat) : n = half n + half n + mod2 n. Proof. funelim (half n). 1-2: reflexivity. @@ -445,7 +445,7 @@ Proof. assumption. Qed. -(** *** 1.2.3 Discharging trivial goals with [simp] +(** *** 1.2.3 Discharging Trivial Goals with [simp] In practice, it often happens in proofs by functional induction that after simplification we get a lot of uninteresting cases that we would like to @@ -591,7 +591,7 @@ Admitted. -(** ** 2. With clauses +(** ** 2. With Clauses The structure of real programs is generally richer than a simple case tree on the original arguments. diff --git a/src/equations/tutorial_indexed.v b/src/equations/tutorial_indexed.v index 5adbd5d..a7f24f0 100644 --- a/src/equations/tutorial_indexed.v +++ b/src/equations/tutorial_indexed.v @@ -24,13 +24,13 @@ - 2. Advanced Dependent Pattern Matching - 2.1 Discarding Automatically Impossible Cases - 2.2 The No-Confusion Properties - - 2.3 The Tactic Depelim + - 2.3 No-confusion and Dependent Elimination Tactics - 3. Unifying Indices and Inaccessible Patterns *** Prerequisites: Needed: - - We assume basic knowledge of Rocq, of and defining functions by recursion + - We assume basic knowledge of Rocq, and of defining functions by recursion - We assume basic knowledge of the plugin Equations, e.g, as presented in the tutorial Equations : Basics @@ -48,7 +48,7 @@ From Equations Require Import Equations. (** ** 1. Basic Reasoning on Indexed Inductive Types - Indexed inductive types are particular kind of inductive definitions + Indexed inductive types are a particular kind of inductive definitions Given a fixed parameter [A : Type], vectors define a family of linked inductive types. One of the most well-known examples of indexed inductive types are vectors. @@ -71,7 +71,7 @@ Arguments vnil {_}. Arguments vcons {_} _ _ _. (** The difference between a parameter and an index is that a parameter is - constant accross all the return types of the constructors, whereas an index + constant across all the return types of the constructors, whereas an index changes in at least one of the return types. For instance, in the definition of vectors the type [A] is a parameter as it is constant across all the return types: [vec A 0] and [vec A (S n)]. @@ -517,7 +517,7 @@ vmap'' f (S n) (vcons a v) := vcons (f a) (vmap'' f n v). Extraction vmap. Extraction vmap''. -(** Using inaccessible patterns hence allows to separate explicitely the subjects of +(** Using inaccessible patterns hence allows to separate explicitly the subjects of pattern-matchings and the inferred indices in definitions. The following alternative definition of the square matrix diagonal pattern-matches only on the [vec] argument, but uses well-founded recursion on the index [n] to justify termination, as diff --git a/src/equations/tutorial_obligations.v b/src/equations/tutorial_obligations.v index 8321853..c6e43e1 100644 --- a/src/equations/tutorial_obligations.v +++ b/src/equations/tutorial_obligations.v @@ -4,7 +4,7 @@ [Equations] is a plugin for Rocq that offers a powerful support for writing functions by dependent pattern matching. - In this tutorial, we discuss how it interface with [Program] to help write + In this tutorial, we discuss how it interfaces with [Program] to help write programs using obligations. In section 1, we recall the concept of obligation and how they interface with [Equations]. @@ -15,10 +15,10 @@ - 1. Equations and Obligations - 1.1 Obligations - - 1.2 Solving obligations - - 2. Equations' solving tactic - - 2.1 Personalizing the tactic proving obligations - - 2.2 What to do if goals are oversimplified + - 1.2 Solving Obligations + - 2. Equations' Solving Tactic + - 2.1 Personalizing the Tactic Proving Obligations + - 2.2 What to Do If Goals Are Oversimplified *** Prerequisites @@ -52,7 +52,7 @@ Arguments to_fill {_}. In some cases, to define functions we may have to prove properties. There can be many reasons for that. Among others, the data structure under - consideration may can include invariants that we must prove to be preserved + consideration may include invariants that we must prove to be preserved when defining functions. For instance, vectors of size [n] can be defined as lists of length [n], @@ -88,7 +88,7 @@ vapp (exist _ ln Hn) (exist _ lm Hm) := to adapt Therefore, we would much rather like to build our terms using the proof mode. - This is exactly what [Program] and obligations enables us to do. + This is exactly what [Program] and obligations enable us to do. At every point in a definition, it allows us to write down a wildcard [_] instead of a term, it will then: - 1. create an obligation, intuitively a goal left to solve @@ -127,8 +127,8 @@ Qed. 3. Be aware that a definition is not defined until all its associated obligations have been solved. Trying to refer to it before that, we - consequently trigger the error that the defintion was not found. - For instance, consider the unfinished definition of [vmap] with a wildcar [_] + consequently trigger the error that the definition was not found. + For instance, consider the unfinished definition of [vmap] with a wildcard [_] *) Equations vmap {A B n} (f : A -> B) (v : vec A n) : vec B n := @@ -144,7 +144,7 @@ Fail Definition vmap_comp {A B C n} (g : B -> C) (f : A -> B) (v : vec A n) Obligations of vmap_obligations. -(** *** 1.2 Solving obligations +(** *** 1.2 Solving Obligations There are two different methods to solve the remaining obligations. @@ -194,7 +194,7 @@ vnil := exist _ nil eq_refl. Defined. -(** ** 2. Equations' solving tactic +(** ** 2. Equations' Solving Tactic As mentioned, [Equations] automatically tries to solve obligations. It does so using a custom strategy basically simplifying the goals and @@ -204,7 +204,7 @@ Defined. Show Obligation Tactic. -(** 2.1 Personalizing the tactic proving obligations +(** *** 2.1 Personalizing the Tactic Proving Obligations When working, it is common to be dealing with a particular class of functions that shares a common theory, e.g, they involve basic arithmetic. @@ -260,10 +260,10 @@ gcd x y with gt_eq_gt_dec x y := { | inright _ := gcd (x - y) y }. -(** 2.2 What to do if goals are oversimplified +(** *** 2.2 What to Do If Goals Are Oversimplified - In some cases, it can happen that [Equations]' solving tactic is too abrut - and oversimplies goals, or mis-specialised and ends up getting us stuck. + In some cases, it can happen that [Equations]' solving tactic is too abrupt + and oversimplifies goals, or mis-specialised and ends up getting us stuck. The automation can also become slow, and one might want to diagnose this. In any of these cases, it can be useful to set the solving tactic locally to the identity. That way, the obligations one gets is the raw ones generated by [Equations] diff --git a/src/equations/tutorial_wf_recursion.v b/src/equations/tutorial_wf_recursion.v index 59a1202..b928107 100644 --- a/src/equations/tutorial_wf_recursion.v +++ b/src/equations/tutorial_wf_recursion.v @@ -12,20 +12,20 @@ them using well-founded recursion and [Equations]. In some cases, applying well-founded recursion can fail because information relevant to termination get lost during recursion. - In section 3, we discuss two such cases a how to go around them. + In section 3, we discuss two such cases and how to go around them. *** Table of content - - 1. Introduction to well-founded recursion - - 1.1 The syntactic guard condition is limited - - 1.2 Well-founded recursion - 2. Well-founded recursion and Equations - - 2.1 Using a measure - - 2.2 Using a lexicographic order - - 2.3 Using a custom well-founded relation - - 3. Different tricks to work with well-founded recursion - - 3.1 The inspect method - - 3.2 Improving recursion hypotheses + - 1. Introduction to Well-Founded Recursion + - 1.1 The Syntactic Guard Condition Is Limited + - 1.2 Well-Founded Recursion + - 2. Well-Founded Recursion and Equations + - 2.1 Using a Measure + - 2.2 Using a Lexicographic Order + - 2.3 Using a Custom Well-Founded Relation + - 3. Different Methods to Work with Well-Founded Recursion + - 3.1 The Inspect Method + - 3.2 Improving Recursion Hypotheses *** Prerequisites @@ -51,7 +51,7 @@ From Stdlib Require Import List Arith Nat Lia. Import ListNotations. -(** ** 1. Introduction to well-founded recursion +(** ** 1. Introduction to Well-Founded Recursion For Rocq to be consistent, all functions must be terminating. To ensure they are, Rocq checks that they satisfy a syntactic @@ -64,7 +64,7 @@ Import ListNotations. to see them as such. - *** 1.1 The syntactic guard condition is limited + *** 1.1 The Syntactic Guard Condition Is Limited A common pitfall is when a recursive call is obfuscated, that is when it is not performed directly on a subterm [x], but on a subterm to which a @@ -105,7 +105,7 @@ gcd x y with eq_dec y 0 => { | right _ => gcd y (x mod y) }. -(** *** 1.2 Well-founded recursion +(** *** 1.2 Well-Founded Recursion **** Informally @@ -209,7 +209,7 @@ Definition gcd_Fix (x y : nat) : nat := *) -(** ** 2. Well-founded recursion and Equations +(** ** 2. Well-Founded Recursion and Equations To define a function by well-founded recursion with Equations, one must add after the type of the function [by wf x R], where [x] is the decreasing @@ -242,7 +242,7 @@ Definition gcd_Fix (x y : nat) : nat := In the following, we assume basic knowledge of obligations and [Equations] works together as discussed in the (short) tutorial Equations: Obligations. - ** 2.1 Using a measure + *** 2.1 Using a Measure The most basic (and actually very versatile) method to define a function by well-founded recursion is to define a measure into [nat] to use the well-founded order [<], @@ -372,7 +372,7 @@ Proof. Qed. -(** ** 2.2 Using a lexicographic order +(** *** 2.2 Using a Lexicographic Order Not all definitions can be proven terminating using a measure and the strict order [<] on [nat]. In some cases, it is more practical to use a different well-founded order. @@ -428,7 +428,7 @@ Proof. Qed. -(** ** 2.3 Using a custom well-founded relation +(** *** 2.3 Using a Custom Well-Founded Relation In some cases, there is no basic order that easily lets one define a function by well-founded recursion. @@ -545,16 +545,16 @@ Qed. End LinearSearch. -(** ** 3. Different methods to work with well-founded recursion +(** ** 3. Different Methods to Work with Well-Founded Recursion When defining a function, it can happen that we lose information relevant to termination when matching a value, and that we then get stuck trying to prove termination. - In this section, we discuss two such example an methods to go around the issue. - Note that the inspect method was already used in section 2.4. + In this section, we discuss two such examples and methods to go around the issue. + Note that the inspect method was already used in section 3.1. - *** 3.1 The inspect method + *** 3.1 The Inspect Method Working with a particular well-founded order [lt], it may happen that we have a choice function [f : A -> option A] that for any [(a :A)] @@ -628,7 +628,7 @@ Qed. End Inspect. -(** 3.2 Improving recursion hypotheses +(** *** 3.2 Improving Recursion Hypotheses In some cases, most particularly when using a size or measure, it can happen that when defining a function by well-founded recursion, diff --git a/src/features/tutorial_require_import.v b/src/features/tutorial_require_import.v index bcc6e03..b10e3ba 100644 --- a/src/features/tutorial_require_import.v +++ b/src/features/tutorial_require_import.v @@ -36,16 +36,16 @@ *** Table of content - - 1. Library files, modules and identifiers - - 1.1 The [Require] command and fully qualified names - - 1.2. Basic modules and the [Import] command - - 1.3. Name clashes and disambiguation - - 1.4. Other content types in modules - - 1.5. Guidelines about the order of [Require] and [Import] commands - - 2. Fine control over module features - - 2.1. On the user's side: selective import - - 2.2. On the writer's side: locality attributes in modules - - 3. The [Export] command + - 1. Library Files, Modules and Identifiers + - 1.1 The [Require] Command and Fully Qualified Names + - 1.2. Basic Modules and the [Import] Command + - 1.3. Name Clashes and Disambiguation + - 1.4. Other Content Types in Modules + - 1.5. Guidelines about the Order of [Require] and [Import] Commands + - 2. Fine Control over Module Features + - 2.1. On the User's Side: Selective Import + - 2.2. On the Writer's Side: Locality Attributes in Modules + - 3. The [Export] Command *** Prerequisites @@ -60,9 +60,9 @@ This tutorial should work for Rocq V8.17 or later. *) -(** ** 1. Library files, modules and identifiers *) +(** ** 1. Library Files, Modules and Identifiers *) -(** *** 1.1 The [Require] command and fully qualified names *) +(** *** 1.1 The [Require] Command and Fully Qualified Names *) (** Rocq's basic compilation unit is the _library file_. Each compiled file can be [Require]d in order to make its logical and computational content @@ -188,7 +188,7 @@ About Stdlib.Bool.Bool. This is done, for instance, with the syntax: [From Stdlib Require Import Bool.Bool.] - In passing, there are many more possibilities to [Require] (with or with + In passing, there are many more possibilities to [Require] (with or without [Import]) a library file. The fully qualified name of this file is [Stdlib.Bool.Bool], and one can factor any prefix in the [From] part of the command, so the following @@ -211,7 +211,7 @@ About Stdlib.Bool.Bool. What to choose is then mostly a matter of taste (and clearly depends on the number of files in the library). *) -(** *** 1.2. Basic modules and the [Import] command *) +(** *** 1.2. Basic Modules and the [Import] Command *) (** We will use modules here mostly because they will help us understand how to get what we want from library files (and reject, if possible, what we @@ -232,7 +232,7 @@ End Foo. following way: *) Print Module Foo. -(** Notice that, surprisingly, the too lemmas are printed as [Parameter]s, but +(** Notice that, surprisingly, the two lemmas are printed as [Parameter]s, but they really are actual lemmas. We can access the content of the module with the dot syntax. *) @@ -283,7 +283,7 @@ Check bar. things we will see shortly) - _Library files are modules_. *) -(** *** 1.3. Name clashes and disambiguation *) +(** *** 1.3. Name Clashes and Disambiguation *) (** When we [Import]ed our [Foo] module before, there was no possible name clash since no constant in our context were named [foo], [bar] or [baz]. @@ -464,7 +464,7 @@ Print NestedABC1.ABC.alice. - it is possible to have two constants with the same name as long as they are in different modules (including library files) *) -(** *** 1.4. Other content types in Modules *) +(** *** 1.4. Other Content Types in Modules *) (** So far, our module [Foo] contained only definitions and lemmas. In practice there are many more content types in a module: @@ -543,7 +543,7 @@ Qed. - the same holds for coercions, hints, type class instances and canonical structures (we omit the experiments for brevity). *) -(** *** 1.5 Guidelines about the order of [Require] and [Import] commands *) +(** *** 1.5 Guidelines about the Order of [Require] and [Import] Commands *) (** We have seen that the order of [Require] and [Import] statements is important. Some constants could be shadowed by others, which can break @@ -574,9 +574,9 @@ Qed. - We should try to [Require Import] files in the same order everytime to increase predictability of breakage due to shadowing. *) -(** ** 2. Fine control over module features *) +(** ** 2. Fine Control over Module Features *) -(** *** 2.1. On the user's side: selective import *) +(** *** 2.1. On the User's Side: Selective Import *) (** Now is a good time to present a recent addition: selective import of modules. Recall that importing a module has basically two effects: @@ -729,7 +729,7 @@ Check UnaryZ. Check plus. Check UnaryZ_ind. -(** ** 2.2. On the writer's side: locality attributes in modules *) +(** *** 2.2. On the Writer's Side: Locality Attributes in Modules *) (** Let's now turn to a complementary tool to give control over what should remain local (if not hidden) and what should be exposed in a module (which @@ -874,7 +874,7 @@ Proof. Qed. (** **** Exercise: why could we use the same name in the two previous lemmas? *) -(** ** 3. Exporting a module *) +(** ** 3. The [Export] Command *) (** Contrarily to [Require]d library files, module imports are not transitive. Consider the following nested module: *) diff --git a/src/features/tutorial_search_for_lemma.v b/src/features/tutorial_search_for_lemma.v index 553c0d2..63fe61d 100644 --- a/src/features/tutorial_search_for_lemma.v +++ b/src/features/tutorial_search_for_lemma.v @@ -8,19 +8,19 @@ *** Table of content - - 1. Searching for lemmas - - 1.1 Basic [Search] by name and type - - 1.1.1 Exercise: find parity results on [nat] - - 1.2 Search and notations - - 1.2.1 Exercise: sum and products on [nat] and [Type] - - 1.3 Searching using metavariables - - 1.3.1 Exercise: find lemmas with metavariables - - 1.4 Filtering on hypotheses (parameters) or conclusions (return type) - - 1.4.1 Exercise: finding divisibility results - - 2. Advanced [Search] options - - 2.1 Disambiguating strings in Search queries - - 2.2 Filtering results by logical kind and disjunctions of criteria. - - 2.3 Searching inside or outside a specific module + - 1. Searching for Lemmas + - 1.1 Basic [Search] by Name and Type + - 1.1.1 Exercise: Find Parity Results on [nat] + - 1.2 Search and Notations + - 1.2.1 Exercise: Sum and Products on [nat] and [Type] + - 1.3 Searching Using Metavariables + - 1.3.1 Exercise: Find Lemmas with Metavariables + - 1.4 Filtering on Hypotheses (Parameters) or Conclusions (Return Type) + - 1.4.1 Exercise: Finding Divisibility Results + - 2. Advanced [Search] Options + - 2.1 Disambiguating Strings in Search Queries + - 2.2 Filtering Results by Logical Kind and Disjunctions of Criteria + - 2.3 Searching Inside or Outside a Specific Module *** Prerequisites @@ -49,9 +49,9 @@ From Stdlib Require Import PeanoNat. -(** ** 1. Searching for lemmas *) +(** ** 1. Searching for Lemmas *) -(** *** 1.1 Basic [Search] by name and type *) +(** *** 1.1 Basic [Search] by Name and Type *) (** In its most basic form, one searches for lemmas or definitions containing - a given constant, eg [Nat.add], or [nat] @@ -82,7 +82,7 @@ Search "add" Nat.mul. - has [Nat.odd] in the type *) Search Nat.add "mul" Nat.odd. -(** We can also _filter out_ results satisfying a criterion with by prepending +(** We can also _filter out_ results satisfying a criterion by prepending it with a minus [-] symbol. Say we're looking for a lemma stating that the sum of an even number and an odd number is odd: *) @@ -93,7 +93,7 @@ Search Nat.odd Nat.add. [-"mul"]: *) Search Nat.odd Nat.add -"mul". -(** **** 1.1.1 Exercise: find parity results on [nat] *) +(** **** 1.1.1 Exercise: Find Parity Results on [nat] *) (** We're interested in lemmas about parity in [nat]. There are two complementary definitions of being even and being odd: @@ -124,7 +124,7 @@ Compute Nat.odd 42. (* 5. *) Search orb Nat.even Nat.odd -Nat.add -Nat.mul. (* End of solution *) -(** *** 1.2 Search and notations *) +(** *** 1.2 Search and Notations *) (** Previously, we have been using the names of the operations to [Search] for. It may be confusing that such names do not even appear in the output. *) @@ -231,7 +231,7 @@ Search nat (_ + _) (_ * _). (* still too much *) their names. *) Search (_ + _) (_ * _) "distr". -(** **** 1.2.1 Exercise: sum and products on [nat] and [Type] *) +(** **** 1.2.1 Exercise: Sum and Products on [nat] and [Type] *) (** Write [Search] commands with notations to find out if: 1. there are operations whose return type is a product type containing [nat]; @@ -245,7 +245,7 @@ Search (_ + _) (_ * _) "distr". (* 3. *) Search (_ + _ <= _ * _)%nat. (* End of solution *) -(** *** 1.3 Searching using metavariables *) +(** *** 1.3 Searching Using Metavariables *) (** We have cheated a little bit. It often happens that we have no idea how a lemma is named. However, we know what distributivity (say, on the left) @@ -269,14 +269,14 @@ Search nat (?op ?a ?b = ?op ?b ?a). (** Another possibility is to exclude any results mentioning [bool]: *) Search (?op ?a ?b = ?op ?b ?a) -bool. -(** We can also opt to remove only results with "orb" it its name: *) +(** We can also opt to remove only results with "orb" in its name: *) Search (?op ?a ?b = ?op ?b ?a) -"orb". (** Or results where the (_ || _) operator appears (notice the scope key, since [bool_scope] is not currently opened): *) Search (?op ?a ?b = ?op ?b ?a) -(_ || _)%bool. -(** **** 1.3.1 Exercise: find lemmas with metavariables *) +(** **** 1.3.1 Exercise: Find Lemmas with Metavariables *) (** Write [Search] commands with notations and metavariables to find out: 1. a lemma stating that adding a natural number on the right cannot be @@ -292,7 +292,7 @@ Search (?op ?a ?b = ?op ?b ?a) -(_ || _)%bool. (* 3. *) Search ((Nat.divide ?a ?b) -> ?a <= ?b). (* End of solution *) -(** *** 1.4 Filtering on hypotheses (parameters) or conclusions (return type) *) +(** *** 1.4 Filtering on Hypotheses (Parameters) or Conclusions (Return Type) *) (** It often happens that we [Search] in the middle of a proof for a lemma we suspect will apply to the current goal. In that case, we can use @@ -334,7 +334,7 @@ Search headhyp:"<->". [headhyp]: *) Search head:"<->". -(** **** 1.4.1 Exercise: finding divisibility results *) +(** **** 1.4.1 Exercise: Finding Divisibility Results *) (** Write [Search] commands with filters on hypotheses and/or conclusions in order to: @@ -349,9 +349,9 @@ Search hyp:(Nat.divide _ (_ * _)). Search headconcl:Nat.divide. (* End of solution *) -(** ** 2. Advanced [Search] options *) +(** ** 2. Advanced [Search] Options *) -(** *** 2.1 Disambiguating strings in Search queries *) +(** *** 2.1 Disambiguating Strings in Search Queries *) (** We have seen two different usages of strings in search queries, namely, searching for constants whose name contains the string, such as: *) @@ -386,7 +386,7 @@ Search "mod"%nat. (** Of course, we can still use a pattern instead of a string: *) Search (_ mod _). -(** *** 2.2 Filtering results by logical kind and disjunctions of criteria. *) +(** *** 2.2 Filtering Results by Logical Kind and Disjunctions of Criteria *) (** We can also [Search] for a constant defined with a specific keyword. For instance, the following lists all [Lemma]s whose names contain "add" @@ -408,7 +408,7 @@ Search [Nat.add | Nat.mul] ["comm" | "assoc"] [is:Lemma | is:Theorem]. [the reference manual](https://coq.inria.fr/doc/V8.19.0/refman/proof-engine/vernacular-commands.html?highlight=search#search-by-keyword) for the list of all logical kinds which can appear after [is:]. *) -(** *** 2.3 Searching inside or outside a specific module *) +(** *** 2.3 Searching Inside or Outside a Specific Module *) (** Finally it is possible to further restrict the [Search] results inside or outside a specific [Module]. *) diff --git a/src/hierarchy_builder/tutorial_basics.v b/src/hierarchy_builder/tutorial_basics.v index 769ea8b..1eb146e 100644 --- a/src/hierarchy_builder/tutorial_basics.v +++ b/src/hierarchy_builder/tutorial_basics.v @@ -10,15 +10,15 @@ *** Table of contents - - 1. Mixins and structures: declaring a structure - - 2. Instances: building an instance of a structure - - 3. Factories and builders: alternative representations of structures - - 4. Options, parameters, visibility of instances - - 4.1. Short names + - 1. Mixins and Structures: Declaring a Structure + - 2. Instances: Building an Instance of a Structure + - 3. Factories and Builders: Alternative Representations of Structures + - 4. Options, Parameters, Visibility of Instances + - 4.1. Short Names - 4.2. Parameters - - 4.3. Primitive records - - 4.4. Visibility of instances - - 5. Non-forgetful inheritance + - 4.3. Primitive Records + - 4.4. Visibility of Instances + - 5. Non-Forgetful Inheritance *** Prerequisites @@ -46,7 +46,7 @@ However, describing such hierarchies using Rocq commands takes a lot of effort, is prone to errors and leads to code that is hard to maintain. - Hierarchy Builder prodives commands that declare all the required objects + Hierarchy Builder provides commands that declare all the required objects automatically. It also guarantees a few properties, like the compatibility of coercion paths. If there are several ways to build an instance of a structure, HB ensures that they all yield the same resulting instance. HB also has @@ -69,7 +69,7 @@ From HB Require Import structures. From Stdlib Require Import PeanoNat. -(** ** 1. Mixins and structures: declaring a structure +(** ** 1. Mixins and Structures: Declaring a Structure By structure, we mean an object (which we call structure) equipped with some data (usually operations) and properties. The basic building block of a @@ -163,7 +163,7 @@ HB.about Semigroup. Check fun (T : Semigroup.type) => T : Magma.type. -(** ** 2. Instances : building an instance of a structure +(** ** 2. Instances: Building an Instance of a Structure Let us now build actual magmas. to find an instance for a given type, Rocq only looks at the "head" of the subject, which we call its key. @@ -239,7 +239,7 @@ rewrite (@opA nat). reflexivity. Qed. -(** ** 3. Factories and builders: alternative representations of structures +(** ** 3. Factories and Builders: Alternative Representations of Structures There may be several ways to describe the same structure. For example, when dealing with orders, giving either of the large operator and the strict @@ -317,11 +317,11 @@ HB.structure Definition ComSemigroup := {T of isSemigroup T & isComm T}. structures with the same set of mixins. *) -(** ** 4. Options, scope +(** ** 4. Options, Parameters, Visibility of Instances HB lets us customize a few things. - *** 4.1. Short names + *** 4.1. Short Names First, we can give a short name for a structure with the [short] attribute. @@ -348,7 +348,7 @@ HB.mixin Record isMagmaMorphism (T U : Magma.type) (f : T -> U) := { HB.structure Definition MagmaMorphism (T U : Magma.type) := {f of isMagmaMorphism T U f}. -(** *** 4.3 Primitive records +(** *** 4.3. Primitive Records We can ask for HB to use primitive records with the [primitive] attribute. Primitive records satisfy the eta-contraction rule, stating that for a @@ -377,7 +377,7 @@ Check fun (T : Magma.type) (f : MagmaMorphism'.type T T) => MagmaMorphism'.sort T T f. Unset Printing Coercions. -(** *** 4.4. Visibility of instances +(** *** 4.4. Visibility of Instances Now, let us talk about the visibility of instances. An instance is visible only when it is declared in the current module. @@ -426,7 +426,7 @@ Check idfun' nat : MagmaMorphism.type nat nat. (* The instance has been imported Fail Check hidden. (* [hidden] has not been imported. *) Check B.hidden. -(** 5. Non-forgetful inheritance *) +(** ** 5. Non-Forgetful Inheritance *) (** Non-forgetful inheritance is a common issue we encounter when building hierarchies of structures. This issue arises when there are several @@ -470,7 +470,7 @@ destruct w; reflexivity. Qed. (** In this case, both instances are extensionally the same so we can still - conclude, but the could very well have not been. + conclude, but they could very well have not been. *) (** The standard solution to this is to make one structure depend on the other. diff --git a/src/metaprogramming/ltac2/how_to_contradiction.v b/src/metaprogramming/ltac2/how_to_contradiction.v index 766b602..aeae68b 100644 --- a/src/metaprogramming/ltac2/how_to_contradiction.v +++ b/src/metaprogramming/ltac2/how_to_contradiction.v @@ -15,14 +15,14 @@ *** Table of content - 1. Introduction - - 2. Matching the goal for [P] and [~P] + - 2. Matching the Goal for [P] and [~P] - 2.1 Choosing [lazy_match!], [match!] or [multi_match!] - 2.2 Matching Syntactically or Semantically - - 2.3 Error messages + - 2.3 Error Messages - 3. Using Constr.Unsafe and Ind API to Add Syntactic Checks - 3.1 Checking for Empty and Singleton Types - 3.2 Checking for Empty and Singleton Hypotheses - - 4. Putting it All Together + - 4. Putting It All Together *** Prerequisites @@ -66,7 +66,7 @@ From Ltac2 Require Import Ltac2 Constr Printf. *) -(** ** 2. Matching the goal for [P] and [~P] +(** ** 2. Matching the Goal for [P] and [~P] *** 2.1 Choosing [lazy_match!], [match!] or [multi_match!] @@ -95,7 +95,7 @@ From Ltac2 Require Import Ltac2 Constr Printf. For this scenario, the [contradiction] tactic is meant to solve goals with a simple enough inconsistent context. It is not meant to be linked with other tactics. Consequently, we have no use for [multimatch!] to implement [contradiction]. - Choosing betwen [lazy_match!] and [match!] really depends on whether we need + Choosing between [lazy_match!] and [match!] really depends on whether we need more than a syntactic checkr, as we will see in the rest of this document. *) @@ -642,7 +642,7 @@ Ltac2 match_nP_singleton () := then let np := Control.hyp np in solve [destruct ($np ltac2:(constructor 1))] - else printf "%t is not a singeleton or %t is not False" x y ; fail + else printf "%t is not a singleton or %t is not False" x y ; fail | _ => printf "%t is not product" t2; fail end | [ |- _ ] => Control.zero (Contradiction_Failed (Some (fprintf "No such contradiction"))) @@ -660,14 +660,14 @@ Goal ~(0 = 1) -> False. intros. Fail match_nP_singleton (). Abort. -(** ** 4. Putting it All Together *) +(** ** 4. Putting It All Together *) (** It took a few explanations, but in the end the code of [contradiction_empty] is rather short using Ltac2. To be efficient, we first perform the syntax check as it is very cheap. - We hence first check for an empty hypotheses, then if it is a negation, - in particular of a singletion inductive type. If it is none of these, + We hence first check for an empty hypothesis, then if it is a negation, + in particular of a singleton inductive type. If it is none of these, check for [P] and [~P] which we perform last in order not to check the whole context for nothing. *) diff --git a/src/metaprogramming/ltac2/tutorial_backtracking.v b/src/metaprogramming/ltac2/tutorial_backtracking.v index a0b0463..3c9bcc1 100644 --- a/src/metaprogramming/ltac2/tutorial_backtracking.v +++ b/src/metaprogramming/ltac2/tutorial_backtracking.v @@ -16,13 +16,13 @@ - 1. Introduction to Backtracking - 1.1 The Stream Model - - 1.2 backtracking and Goal Focusing + - 1.2 Backtracking and Goal Focusing - 2. Using [Control.zero] to Raise Exceptions - - 3. Using [Control.Plus] to Stack Possibilities + - 3. Using [Control.plus] to Stack Possibilities - 3.1 Reimplementing [+] - 4. Using [Control.Case] to Inspect Backtracking - 4.1 Reimplementing [||] - - 4.1 Reimplementing [once] + - 4.2 Reimplementing [once] *** Prerequisites @@ -78,7 +78,7 @@ Ltac2 Notation "only" startgoal(tactic) endgoal(opt(seq("-", tactic))) ":" tac(t -(** ** 1. Introducing on Backtracking +(** ** 1. Introduction to Backtracking In Rocq, all tactics are potentially backtracking. @@ -88,7 +88,7 @@ Ltac2 Notation "only" startgoal(tactic) endgoal(opt(seq("-", tactic))) ":" tac(t In this case, if [tac2] fails triggering backtracking, it will backtrack to [tac1], try its next success if there is one, then try [tac2] again. This until either all possibilities have been exhausted or [tac2] succeeds for - one of the success procuded by [tac1]. + one of the success produced by [tac1]. The most well known example is the [constructor] tactic that tries the constructors one by one, until one leads to a success or all constructors have @@ -208,7 +208,7 @@ Qed. Therefore, most basic tactics and tactic cominators like [constructor] or [first] are already wrapped in [Control.enter] for us, so we don't have to think about it. - In the rest of the tutorial, we will recode basic constructor so + In the rest of the tutorial, we will recode basic constructors so we need to think about it. *) @@ -224,7 +224,7 @@ Qed. *) -(** 2. Using [Control.zero] to Raise Exceptions +(** ** 2. Using [Control.zero] to Raise Exceptions Suppose we want to re-implement a tactic like [eassumption] that checks if the goals corresponds to an hypothesis, possibly unifying evariables. @@ -295,7 +295,7 @@ Abort. -(** ** 3. [Control.plus] to Catch Exceptions +(** ** 3. Using [Control.plus] to Stack Possibilities Since [Ltac2] has proper exceptions and backtracking is primitive, it is not only possible to catch exceptions, but also to backtrack upon them. @@ -386,7 +386,7 @@ Abort. if it is empty, and if not return the head with the rest of the stream. - *** 4.1 Reimplement [||] + *** 4.1 Reimplementing [||] As a first example where [Control.case] is needed, consider [++] or section 3. In practice, backtracking on [tac2] in case subsequent failure of the choice of [tac1] @@ -464,7 +464,7 @@ Abort. -(** *** 4.2 Reimplement [once] +(** *** 4.2 Reimplementing [once] Backtracking is allowed by default. To offer better control over it, the standard library of tactics offers the tactic combinator [once tac] that diff --git a/src/metaprogramming/ltac2/tutorial_matching_terms_and_goals.v b/src/metaprogramming/ltac2/tutorial_matching_terms_and_goals.v index 1107a17..442a01b 100644 --- a/src/metaprogramming/ltac2/tutorial_matching_terms_and_goals.v +++ b/src/metaprogramming/ltac2/tutorial_matching_terms_and_goals.v @@ -21,8 +21,8 @@ - 1.3 Matching Bound Variables - 1.4 Using the Unsafe API to Access the Term Structure - 2. Matching Goals - - 1.1 Basics - - 1.2 Non-Linear Matching + - 2.1 Basics + - 2.2 Non-Linear Matching - 3. Backtracking and [lazy_match!], [match!], [multi_match!] - 3.1 [lazy_match!] - 3.2 [match!] @@ -52,7 +52,7 @@ Ltac2 print_goals0 () := Ltac2 Notation print_goals := print_goals0 (). -(** ** 1 Matching terms +(** ** 1. Matching Terms *** 1.1 Basics diff --git a/src/metaprogramming/ltac2/tutorial_quoting.v b/src/metaprogramming/ltac2/tutorial_quoting.v index 0a7c792..d798944 100644 --- a/src/metaprogramming/ltac2/tutorial_quoting.v +++ b/src/metaprogramming/ltac2/tutorial_quoting.v @@ -17,8 +17,8 @@ - 2.1 Quoting Terms - 2.2 Quoting Terms Without Existential Variables - 2.3 Preterms : Internalize without Typechecking - - 3. Ltac2 in terms - - 4. Quotations as Ltac2 notations + - 3. Ltac2 in Terms + - 4. Quotations as Ltac2 Notations - 5. Ltac1 and Ltac2 *** Prerequisites @@ -53,7 +53,7 @@ Goal nat -> bool. Abort. (** Note, up to Rocq 9.2, there is a slight printing inconsistency: the - evaluated identifier is printed ith the [@] syntax, but the non evaluated + evaluated identifier is printed with the [@] syntax, but the non evaluated Ltac2 expression is printed with [ident:(...)]: *) Ltac2 make_x () := @x. Print make_x. @@ -319,7 +319,7 @@ Ltac2 succ_preterm (x:preterm) := preterm:(S $preterm:x). Ltac2 Eval Constr.pretype (succ_preterm (succ_preterm (succ_preterm preterm:(0)))). -(** *** 3. Ltac2 in terms +(** ** 3. Ltac2 in Terms We can write a Ltac2 expression inside a Gallina expression: *) Check ltac2:(exact 0). @@ -386,7 +386,7 @@ Ltac2 Eval let x := '1 in '($x + $x). variable [x]. *) -(** ** 4. Quotations as Ltac2 notations +(** ** 4. Quotations as Ltac2 Notations Most (all?) Ltac2 quotations do not need to be primitive (though they often are) and can be written as Ltac2 notations. diff --git a/src/metaprogramming/ltac2/tutorial_types_and_thunking.v b/src/metaprogramming/ltac2/tutorial_types_and_thunking.v index 89878f0..81a5ba8 100644 --- a/src/metaprogramming/ltac2/tutorial_types_and_thunking.v +++ b/src/metaprogramming/ltac2/tutorial_types_and_thunking.v @@ -29,7 +29,7 @@ From Ltac2 Require Import Ltac2. From Ltac2 Require Import Printf. -(** 1. Types of Tactics in Ltac2, and Thunks +(** ** 1. Types of Tactics in Ltac2, and Thunks Usual tactics like [assumption] or [left] are notations for Ltac2 functions. They modify the proof state through side effects, such as modifying diff --git a/src/rocq_theory/explanation_bidirectionality_hints.v b/src/rocq_theory/explanation_bidirectionality_hints.v index cac0129..a7d536b 100644 --- a/src/rocq_theory/explanation_bidirectionality_hints.v +++ b/src/rocq_theory/explanation_bidirectionality_hints.v @@ -2,7 +2,7 @@ *** Summary - An explanation of bidirectionlity hints. + An explanation of bidirectionality hints. After presenting the requisite background on bidirectional typing and existential variables in Rocq, we will see how bidirectionality hints affect type checking of function applications, and we will illustrate with simple @@ -10,9 +10,9 @@ *** Contents - - 1. Bidirectional typing - - 2. Bidirectional typing and existential variables - - 3. Bidirectionality hints + - 1. Bidirectional Typing + - 2. Bidirectional Typing and Existential Variables + - 3. Bidirectionality Hints - 4. Examples *) @@ -21,7 +21,7 @@ Before we explain what bidirectionality hints are, we must first understand some basics of how type checking works in Rocq. -** 1. Bidirectional typing +** 1. Bidirectional Typing Rocq uses bidirectional typing, an approach to type systems that interleaves type checking with type inference. A bidirectional type system replaces the @@ -81,7 +81,7 @@ To check whether the application [f a] has a given type [T]: - 2. _check_ the argument [a] against its type [A]; - 3. _unify_ the inferred result type [B a] and the checked one [T]. -** 2. Bidirectional typing and existential variables +** 2. Bidirectional Typing and Existential Variables To a first approximation, the unification judgement ([T’ ≡ T]) merely denotes an equivalence relation between types. @@ -110,7 +110,7 @@ Unifying [?u ≡ true] first allows the second unification to succeed since will fail if we haven't instantiated [?u] yet, because [if ?u then 0 else 1] is stuck. -** 3. Bidirectionality hints +** 3. Bidirectionality Hints Bidirectionality hints indicate when unification with the result type should happen during type-checking of a function application. By default, that happens diff --git a/src/rocq_theory/explanation_template_polymorphism.v b/src/rocq_theory/explanation_template_polymorphism.v index 6d60f36..c904f17 100644 --- a/src/rocq_theory/explanation_template_polymorphism.v +++ b/src/rocq_theory/explanation_template_polymorphism.v @@ -30,15 +30,15 @@ *** Contents - - 1. Quick reminder about universes - - 2. Some issues with monomorphic universes - - 3. What template universe polymorphism does and doesn't do + - 1. Quick Reminder about Universes + - 2. Some Issues with Monomorphic Universes + - 3. What Template Universe Polymorphism Does and Doesn't Do - 3.1. Principle - - 3.2. Breaking cycles with template polymorphism - - 3.3. Template polymorphism doesn't go through intermediate definitions - - 4. A taste of “full” universe polymorphism + - 3.2. Breaking Cycles with Template Polymorphism + - 3.3. Template Polymorphism Doesn't Go through Intermediate Definitions + - 4. A Taste of “Full” Universe Polymorphism - 4.1. Principle - - 4.2. Universe polymorphic definitions + - 4.2. Universe Polymorphic Definitions *** Prerequisites @@ -52,10 +52,10 @@ Installation: No plugins or libraries required. *) -(** ** 1. Quick reminder about universes +(** ** 1. Quick Reminder about Universes A basic understanding of universes would be best to read this tutorial, but - just in case here's a quick recap'. + just in case here's a quick recap. The reason for universes is that there is no obvious type that can be assigned to the term [Type]. You can decide not to give it a type (in which @@ -80,7 +80,7 @@ means something closer to [Type@{_}] where Rocq infers a universe level based on context, which can be confusing. This is why any job that involves inspecting universes requires [Set Printing Universes], and why here we'll - will write most universes explicitly. + write most universes explicitly. Beyond checking the types of sorts, universes above 0 appear as a result of quantification. As a naïve intuition, any term that quantifies over types @@ -167,7 +167,7 @@ Check (fun (T: Type@{Set+1}) => mprod T). will only evolve in its relations with other universe variables, i.e. through constraints. *) -(** ** 2. Some issues with monomorphic universes *) +(** ** 2. Some Issues with Monomorphic Universes *) (** The core limitations of template universe polymorphism are related to when it doesn't activate and leaves you with monomorphic universes, so we can @@ -258,9 +258,9 @@ Fail Definition mprod_lazy {A B: Type} (a: A) (b: B): errors appearing or disappearing based on what modules have been imported and in what order, a.k.a., everyone's favorite. *) -(** ** 3. What template universe polymorphism does and doesn't do *) +(** ** 3. What Template Universe Polymorphism Does and Doesn't Do *) -(** *** Principle *) +(** *** 3.1. Principle *) (** Template universe polymorphism is a middle-ground between monomorphic universes and proper polymorphic universes that allows for some degree of @@ -293,7 +293,7 @@ Check (fun (S: Set) => S * S). with the constraint that the input levels must be below [prod.u0] and [prod.u1] respectively. *) -(** *** Breaking cycles with template polymorphism *) +(** *** 3.2. Breaking Cycles with Template Polymorphism *) (** It looks like we've solved our universe problem now because we can have both definitions of [prod] within [lazyT] and [lazyT] within [prod]. *) @@ -318,7 +318,7 @@ Print Universes Subgraph ( (** There are other constraints here but they're unrelated to the inconsistency that we had with the monomorphic version. *) -(** *** Template polymorphism doesn't go through intermediate definitions *) +(** *** 3.3. Template Polymorphism Doesn't Go through Intermediate Definitions *) (** And thus, the problem is solved... but only when the universe at fault comes from an inductive type directly (here, [prod]). Template polymorphic @@ -358,9 +358,9 @@ Fail Definition state_lazy {S T: Type} (t: T): state S (lazyT T) := About sum. About list. -(** ** 4. A taste of “full” universe polymorphism ***) +(** ** 4. A Taste of “Full” Universe Polymorphism *) -(** *** Principle *) +(** *** 4.1. Principle *) (** Template universe polymorphism is limited in that it only applies to inductives and any indirect uses of such a type are just monomorphic. The @@ -385,7 +385,7 @@ Check pprod@{uprod uprod}. (** So far, this is the same as template universe polymorphism. *) -(** *** Universe polymorphic definitions *) +(** *** 4.2. Universe Polymorphic Definitions *) (** The new trick is that definitions derived from [pprod] can retain the polymorphism by having their own universe parameters. *) diff --git a/src/writing_proofs/tutorial_chaining_tactics.v b/src/writing_proofs/tutorial_chaining_tactics.v index 4323ac2..512f2e0 100644 --- a/src/writing_proofs/tutorial_chaining_tactics.v +++ b/src/writing_proofs/tutorial_chaining_tactics.v @@ -13,9 +13,9 @@ - 1. Introduction to Chaining - 2. Chaining Selectively on Subgoals - 2.1 Basics - - 2.2 Ignoring Subgoals when Chaining - - 2.3 Chaining on a Range of Sugoals - - 3. Chaining is actually backtracking + - 2.2 Ignoring Subgoals When Chaining + - 2.3 Chaining on a Range of Subgoals + - 3. Chaining Is Actually Backtracking - 4. Repeating Tactics and Chaining *** Prerequisites @@ -44,7 +44,7 @@ Section Chaining. Set Printing Parentheses. (** In Rocq, we prove theorems interactively, applying at each step a tactic - that transform the goal, and basically corresponds to applying a logical resonning. + that transform the goal, and basically corresponds to applying a logical reasoning. Yet, in practice, it often happens that some of the primitive tactics are too low-level, and that a higher-level resoning step we would like to do gets decomposed into a sequence of tactics, and hence of interactive steps. @@ -170,7 +170,7 @@ Section Chaining. Qed. -(** *** 2.2 Ignoring Subgoals when Chaining +(** *** 2.2 Ignoring Subgoals When Chaining The construction [tac ; [tac1 | ... | tacn] ] requires a tactic per subgoal. Yet, in some cases, before continuing the common proof, an action is needed @@ -261,7 +261,7 @@ Section Chaining. Qed. -(** *** 2.3 Chaining on a Range of Sugoals +(** *** 2.3 Chaining on a Range of Subgoals It often happens that we have several subgoals, for which we want to apply the same tactic, or do nothing. @@ -324,7 +324,7 @@ Section Chaining. End Range. -(** ** 3 Chaining is actually backtracking +(** ** 3. Chaining Is Actually Backtracking A subtility with chaining tactics is that [tac1 ; tac2] does not only chain tactics together, applying [tac2] on the subgoals created by [tac1], diff --git a/src/writing_proofs/tutorial_intro_patterns.v b/src/writing_proofs/tutorial_intro_patterns.v index 7b20d58..f8e0f22 100644 --- a/src/writing_proofs/tutorial_intro_patterns.v +++ b/src/writing_proofs/tutorial_intro_patterns.v @@ -17,7 +17,7 @@ - 3. Rewriting and Injection - 4. Simplifying Equalities - 5. Applying Lemmas - - 6. Intro patterns everywhere + - 6. Intro Patterns Everywhere *** Prerequisites @@ -273,7 +273,7 @@ Proof. exists x, y. apply f. assumption. Qed. -(** ** 3. Rewriting Lemmas *) +(** ** 3. Rewriting and Injection *) (** It is also very common to introduce an equality that we only wish to use once as a rewrite rule on the goal: *) @@ -448,7 +448,7 @@ Proof. - intros [= -> [-> ->]%app_eq_nil]. right. split; reflexivity. Qed. -(** ** 6. Intro patterns everywhere *) +(** ** 6. Intro Patterns Everywhere *) (** We mentioned before the fact that the tactic [destruct ... as ...] expects an intro pattern after [as].