Typos and Capitalization

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.

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

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]

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,