From ff17e1fd6cbdd55a58dc05cded5da8b0de31fe0e Mon Sep 17 00:00:00 2001
From: thomas-lamiaux <thomas.lamiaux@ens-paris-saclay.fr>
Date: Mon, 20 May 2024 20:18:11 +0200
Subject: [PATCH 01/10] integrates first comments

---
 src/Tutorial_Equations_basics.v | 187 ++++++++++++++++++--------------
 1 file changed, 108 insertions(+), 79 deletions(-)

diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v
index af4ae8d7..69b7dc82 100644
--- a/src/Tutorial_Equations_basics.v
+++ b/src/Tutorial_Equations_basics.v
@@ -49,7 +49,7 @@ Arguments to_fill {_}.
 
 (** * 1. Basic definitions and reasoning
 
-  Let's start by importing the package:
+  let us start by importing the package:
 *)
 
 From Equations Require Import Equations.
@@ -59,7 +59,7 @@ From Equations Require Import Equations.
     In its simplest form, [Equations] provides a practical interface to
     define functions on inductive types by pattern matching and recursion
     rather than using Fixpoint and match.
-    As first examples, let's define basic functions on lists.
+    As first examples, let us define basic functions on lists.
 *)
 
 Inductive list A : Type :=
@@ -71,7 +71,7 @@ Arguments cons {_} _ _.
 
 (** To write a function [f : list A -> B] on lists or another a basic
       inductive type, it suffices to write:
-    - Equation at the beginning of you function rather than Fixpoint
+    - function_name at the beginning of you function rather than Fixpoint
     - For each constructor [cst x1 ... xn] like [cons a l], specify how [f]
       computes on it by writing [f (cst x1 ... xn) := t] where [t] may
       contain [f] recursively.
@@ -99,18 +99,18 @@ Infix "++" := app (right associativity, at level 60).
 (** [Equations] is compatible with usual facilities provided by Coq to write
     terms:
     - It is compatible with implicit arguments that as usual do not need to
-      be written provided it can be inferred, for instance, above, we wrote
-      [app nil l'] rather than [app (nil A) l'] as [A] was declared as an
-      implicit argument of [nil].
-    - We can use the underscores "_" for terms that we do not use, terms
+      be written provided it can be inferred.
+      For instance, above, we wrote [app nil l'] rather than [app (nil A) l']
+      as [A] was declared as an implicit argument of [nil].
+    - We can use underscores "_" for terms that we do not use, terms
       that Coq can infer on its own, but also to describe what to do in all
       remaining cases of our pattern matching.
-      As [list] only has two constructors to it is not very useful here,
+      As [list] only has two constructors, it is not very useful here,
       but we can still see it works by defining a constant function:
 *)
 
 Equations cst_b {A B} (b : B) (l : list A) : B :=
-cst_b b (_) := b.
+cst_b b _ := b.
 
 (** - We can use notations both in the pattern matching (on the left-hand
       side of :=) or in the bodies of the function (on the right-hand side
@@ -132,7 +132,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 [Fixpoint] one.
+    closer to the the one provided by the [Fixpoint] command and Coq'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 functions nor to put parenthesis or finish a line by "[;]".
@@ -148,14 +148,14 @@ Equations app'' {A} (l l' : list A) : list A :=
   | []    , l' := l'
   | (a::l), l' := a :: (app'' l l').
 
-(** In this tutorial, we will keep to the first syntax but both are acceptable.
+(** In this tutorial, we will keep to the first syntax but both are can be used interchangeably..
 
     [Equations] enables us to pattern match on several different
     variables at the same time, for instance, to define a function [nth_option]
     getting the nth-element of a list and returning [None] otherwise.
 *)
 
-Equations nth_option {A} (n : nat ) (l : list A) : option A :=
+Equations nth_option {A} (n : nat) (l : list A) : option A :=
 nth_option 0 nil := None ;
 nth_option 0 (a::l) := Some a ;
 nth_option (S n) nil := None ;
@@ -176,7 +176,7 @@ nth_option' (a::l) (S n) := nth_option' l n.
 
 Goal forall {A} (a:A) n, nth_option n (nil (A := A)) = nth_option' (nil (A := A)) n.
 Proof.
-  (* Here [autorewrite with f] is a simplification tactic of Equation (c.f 1.1.2).
+  (* Here [autorewrite with f] is a simplification tactic of [Equations] (c.f 1.1.2).
      As we can see, [nth_option'] reduces on [ [] ] to [None] but not [nth_option]. *)
   intros.
   autorewrite with nth_option.
@@ -184,7 +184,7 @@ Proof.
 Abort.
 
 (** As exercices, you can try to define:
-    - A function [map f l] that applies [f] pointwise, on [ [a, ... ,a] ] it
+    - A function [map f l] that applies [f] pointwise, on [ [a1, ... ,an] ] it
       returns [ [f a1, ... , f an] ]
     - A function [head_option] that returns the head of a list and [None] otherwise
     - A function [fold_right f b l] that on a list [ [a1, ..., an] ]
@@ -192,8 +192,7 @@ Abort.
 *)
 
 Equations map {A B} (f : A -> B) (l : list A) : list B :=
-map f nil := nil ;
-map f (a::l) := (f a)::(map f l).
+map f _ := to_fill.
 
 Equations head_option {A} (l : list A) : option A :=
 head_option _ := to_fill.
@@ -216,7 +215,7 @@ Succeed Example testing : fold_right Nat.mul 1 (1::2::3::4::[]) = 24 := eq_refl.
 (** Now that we have seen how to define basic functions, we need to
     understand how to reason about them.
 
-    By default, the functions defined using [Equations] are opaque and can not
+    By default, functions defined using [Equations] are opaque and cannot
     be unfolded with [unfold] nor simplified with [simpl] or [cbn] as one
     would do with a [Fixpoint] definition.
     This is on purpose to prevent uncontrolled unfolding which can easily
@@ -226,7 +225,7 @@ Succeed Example testing : fold_right Nat.mul 1 (1::2::3::4::[]) = 24 := eq_refl.
     of an equation are definitionally equal.
 
     For instance, consider [nil_app] the usual computation rule for [app].
-    It can not be unfolded, nor simplified by [cbn] but can be proven by
+    It cannot be unfolded, nor simplified by [cbn] but can be proven by
     [reflexivity].
 *)
 
@@ -242,12 +241,14 @@ Qed.
     basis using the option [Global Transparent f] as shown below.
     It is also possible to set this option globally with [Set Equations
     Transparent], but it is not recommended to casual users.
-    To recover simplification by [simpl] and [cbn], one needs to additionally
-    use the command [Arguments name_function /].
+    To recover simplification by [simpl] and [cbn], one can additionally
+    use the command [Arguments function_name !_ /. ].
+    It will simplify the function as soon as it is applied to one argument
+    that is a constructor.
 *)
 
 Equations f4 (n : nat) : nat :=
-f4 (_) := 4.
+f4 _ := 4.
 
 Global Transparent f4.
 
@@ -255,27 +256,32 @@ Goal f4 3 = 4.
 Proof.
   (* [f4] can now be unfolded *)
   unfold f4. Restart.
-  (* Yet, it still can not be simplify by [cbn] *)
+  (* Yet, it still cannot be simplify by [cbn] *)
   Fail progress cbn.
   (* [Arguments] enables to recover simplification *)
-  Arguments f4 /. cbn.
+  Arguments f4 !_ /. cbn.
 Abort.
 
 (** Rather than using [cbn] or [simpl], for each function [f], [Equations]
-    internally declares an equality for each case of the pattern matching
-    defining [f], in a database named [f].
-    For instance, for [app], it declares [app [] l' = l'] and
+    internally proves an equality for each case of the pattern matching
+    defining [f], and declares them in a hint database named [f].
+    For instance, for [app], it proves and declares [app [] l' = l'] and
     [app (a::l) l' = a :: (app l l')].
-    It is then possible to simply simplify by the equations associated
+    The equalities are named "function_name_equation_n", and you can check
+    them out using the command [Print Rewrite HintDb function_name]:
+*)
+
+Print Rewrite HintDb app.
+
+(** It is then possible to simply simplify by the equations associated
     to function [f1 ... fn] using the tactic [autorewrite with f1 ... fn].
-    This provide a better control of unfolding when doing in proofs as
+    This provide a better control of unfolding when in proofs as
     compared to cbn the user can choose which functions [f1 ... fn],
     they wants to simplify.
 
-    As an example, let's prove [app_nil l : l ++ [] = l].
+    As an example, let us prove [app_nil l : l ++ [] = l].
     As [app] is defined by pattern match on [l], we prove the result by
-    induction on [l],  and uses [autorewrite with app] to simplify the goals.
-    We can similarly prove that [app] is associative.
+    induction on [l], and use [autorewrite with app] to simplify the goals.
 *)
 
 Lemma app_nil {A} (l : list A) : l ++ [] = l.
@@ -292,7 +298,7 @@ Abort.
     that both definition of [nth_option] are equal.
     We have to be careful to first revert [n] in order to generalise the
     induction hypothesis and get something strong enough when inducting on [l],
-    and we then need to detruct n.
+    and we then need to destruct n.
 *)
 
 Lemma nth_eq {A} (l : list A) (n : nat) : nth_option n l = nth_option' l n.
@@ -305,19 +311,29 @@ Proof.
   - apply IHl.
 Abort.
 
-(** This process quickly gets tedious and complicated to do by hand on real life examples,
-    especially when using complicated inductive types, or more advanced
-    notions of matching like [with] and [where] clauses (c.f 1.2).
-    Consequently, [Equations] comes with a tactic [funelim] that automatically
-    does an induction following the pattern matching used to define a
-    function, there is no need to do it by hand.
-    Moreover, it does so directly with the right induction hypothesis, there
-    is no need to generalise the induction hypothesis as done by
-    reverting [n] in the proof of [nth_eq] above.
-    To use it, it suffices to write [funelim (name_function a1 ... an)]
+(** This process quickly gets tedious and complicated to do by hand on real life
+    examples, especially when using complicated inductive types, or more advanced
+    notions of matching like [with] and [where] clauses (c.f 2. and 3.).
+    Consequently, for each definition, [Equations] derives a functional induction
+    principle: this is an induction principle that follows the structure of the
+    function, including deep pattern-matching, [with] and [where] clauses,
+    correct induction hypotheses and generalisation as in the above example.
+    This principle is named using the scheme "function_name_elim".
+
+    For instance, to prove a goal [P] depending on [app_elim] [l], [l'], and [l ++ l'],
+    [app_elim] asserts that it suffices to:
+    - prove the base case [P [] l' l']
+    - and that [P l l' (l ++ l')] implies [P (a :: l) l' (a :: l ++ l'))]
+*)
+
+Check app_elim.
+
+(** Moreover, [Equations] comes with a powerful tactic [funelim] that
+    applies the induction principle while doing different simplifications.
+    To use it, it suffices to write [funelim (function_name a1 ... an)]
     where [a1 ... an] are the arguments you want to do your induction on.
 
-    As an example, let's prove [app_nil], [app_assoc], and [nth_eq] for
+    As an example, let us prove [app_nil], [app_assoc], and [nth_eq] for
     which we can already see the advantages over trying to reproduce the
     pattern matching by hand:
 *)
@@ -348,8 +364,8 @@ Abort.
 
 (** By default, the tactic [autorewrite with f] only simplifies a term by the
     equations defining [f], like [[] ++ l = l] for [app].
-    Yet, in practice, it often happens that there are more equations
-    that we have proven that we would like to automatically simplify by
+    In practice, it can happen that there are more equations
+    that we have proven that we would like to use for automatic simplification
     when proving further properties.
     For instance, when reasoning on [app], we may want to further always simplify
     by [app_nil : l + [] = l] or [app_assoc : (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)].
@@ -357,13 +373,13 @@ Abort.
     lemma to the database associated to [f].
     This can be done by the syntax:
 
-      [ #[local] Hint Rewrite @name_lemma : name_function. ]
+      [ #[local] Hint Rewrite @name_lemma : function_name. ]
 
-    This provides us with a very powerful personnalisable rewrite mechanism.
-    However, please note that this mechanism is powerful enough for it
-    to become non terminating if one adds the right lemma.
+    This is a very powerful personnalisable rewrite mechanism.
+    However, note that this mechanism is expressive enough to be
+    non-terminating if the wrong lemmas are added to the database.
 
-    To see how it can be useful, let's define a tail-recursive version of
+    To see how it can be useful, let us define a tail-recursive version of
     list reversal and prove it equal the usual one:
 *)
 
@@ -386,6 +402,9 @@ Abort.
 (* Adding [app_nil] and [app_assoc] the database associated to [app] *)
 #[local] Hint Rewrite @app_nil @app_assoc : app.
 
+(* We can check it has indeed been added *)
+Print Rewrite HintDb app.
+
 (* [autorewrite with app] can now use [app_assoc] *)
 Goal forall {A} (l1 l2 l3 l4 : list A),
      ((l1 ++ l2) ++ l3) ++ l4 = l1 ++ (l2 ++ (l3 ++ l4)).
@@ -397,25 +416,25 @@ Lemma rev_eq {A} (l l' : list A) : rev_acc l l' = rev l ++ l'.
 Proof.
   funelim (rev l). all: autorewrite with rev rev_acc app.
   - reflexivity.
-  (* There is no more need to call it by hand in proofs *)
+  (* There is no more need to call [app_assoc] by hand in proofs *)
   - apply H.
 Abort.
 
-(** In practice, it also often happens that after simplification we get a
-    lot of uninteresting cases when proving properties by induction,
-    properties that we would like to deal with automatically in a controlled way.
+
+(** In practice, it also often happens in such proofs by functional induction that
+    after simplification we get a lot of uninteresting cases, that we would like to
+    deal with in an automatic but controlled way.
     To help us, [Equations] provides us with a tactic [simp f1 ... fn]
     that first simplify the goal by [autorewrite with f1 ... fn] then
     tries to solve the goal by a proof search by a particular instance of
     [try typeclasses eauto].
-    It does so using the equations associated to [f1 ... fn], and a few more
-    lemmas specific to [Equations] meant to ease the proof search.
-    Though, please note that this proof search does not run [reflexivity].
+    It does so using the equations associated to [f1 ... fn], and the database
+    Below and Subterm meant to TO_FILL.
 
     Linking [simpl] with [funelim] like [funelim sth ; simp f1 ... fn] then
     enables us to simplify all the goals and at the same to automatically
     prove uninteresting ones.
-    As examples, let's prove again [nth_eq] and [rev_rev_acc]:
+    For instance:
 *)
 
 Definition nth_eq {A} (l : list A) (n : nat) : nth_option n l = nth_option' l n.
@@ -424,6 +443,12 @@ Proof.
   all : reflexivity.
 Abort.
 
+(** As you can see, it does not run [reflexivity] by default.
+    You can add it to the proof search using the command
+    ISSUE *)
+
+(* #[local] Hint Resolve Euqations.Init.reflexivity : Below. *)
+
 Lemma rev_eq {A} (l l' : list A) : rev_acc l l' = rev l ++ l'.
 Proof.
   funelim (rev l). all: simp rev rev_acc app.
@@ -444,7 +469,7 @@ Proof.
 Admitted.
 
 (* You will need to use the lemma [Arith_prebase.lt_S_n]
-  HINT : [funelim] must be applied to the parameters you are doing the induction on.
+  HINT : [funelim] must be applied to the parameters you want to do the induction on.
          Here, it is [n] and [l], and not [n] and [l++l'].
 *)
 Lemma app_nth1 {A} (n : nat) (l l' : list A) :
@@ -453,7 +478,7 @@ Proof.
 Admitted.
 
 (* You will need the lemma [PeanoNat.Nat.sub_succ] and [le_S_n].
-  HINT : [funelim] must be applied to the parameters you are doing the induction on.
+  HINT : [funelim] must be applied to the parameters you want to do the induction on.
          Here, it is [n] and [l], and not [(n - length l)] and [l']. *)
 Lemma app_nth2 {A} (n : nat) (l l' : list A) :
       length l <= n -> nth_option n (l++l') = nth_option (n-length l) l'.
@@ -476,8 +501,8 @@ Admitted.
     intermediate results (e.g. coming from function calls) to produce an answer.
     In terms of dependent pattern matching, this literally means adding a new
     pattern to the left of our equations made available for further refinement.
-    This concept is know as [with] clauses in the Agda community and was first
-    introduced in the Epigram language.
+    This concept is know as [with] clauses in the dependently-typed programming
+    community and was first introduced in the Epigram language.
 
     [With] clause are available in [Equations] with the following syntax
     where [b] is the term we wish to inspect, and [p1 ... pk] the patterns we
@@ -495,7 +520,7 @@ Admitted.
     predicate [p].
     In the case [cons a l], the [with] clause enables us to compute
     the intermediate value [p a] and to check whether it is [true] or [false],
-    and hence if [a] verify the predicate [p] and should be kept or not:
+    and hence if [a] satisfy the predicate [p] and should be kept or not:
 *)
 
 Equations filter {A} (l : list A) (p : A -> bool) : list A :=
@@ -529,16 +554,16 @@ In x (a::l) => (x = a) \/ In x l.
 
 (** For function defined using [with] clauses, [funelim] does the usual
     disjunction of cases for us, and additionally destructs the pattern
-    associated to the |with] clause and remembers it.
+    associated to the [with] clause and remembers it.
     In the case of [filter], it means additionally destructing [p a] and
     remembering whether [p a = true] or [p a = false].
 
     For regular patterns, simplifying [filter] behaves as usual.
     For the [with] clause, simplifying [filter] makes a subclause
     corresponding to the current case appear.
-    For [filter], it makes appear [filter_clause_1] in the case [p a = true],
-    and [filter_clause_2] in the case [p a = false].
-    This is due to [Equations] internal mechanics.
+    For [filter], in the [p a = true] case, a [filter_clause_1] appears, and
+    similarly in the [false] case.
+    This is due to [Equations]' internal mechanics.
     To simplify the goal further, it suffices to rewrite [p a] by its value
     in the branch, and to simplify [filter] again.
 *)
@@ -563,12 +588,12 @@ unzip ((a,b)::l) with unzip l => {
   | (la,lb) => (a::la, b::lb)
 }.
 
-(** They can also be useful to discard impossible branches.
+(** Finally, [with] clauses can be used to discard impossible branches.
     For instance, rather than returning an option type, we can define a
-    [head] function by requiring for the input to be different than the
+    [head] function by requiring the input to be different than the
     empty list.
     In the [nil] case, we can then destruct [pf eq_refl : False] which
-    as no constructors to define our function.
+    has no constructors to define our function.
 *)
 
 Equations head {A} (l : list A) (pf : l <> nil) : A :=
@@ -601,7 +626,7 @@ find_dictionary eq key _ with to_fill => {
   | _ := to_fill
 }.
 
-(* You can uncomment the following tests to try your function *)
+(* You can uncomment the following tests to try your functions *)
 (* Definition example_dictionnary :=
   (3,true::true::[]) :: (0,[]) :: (2,true::false::[]) :: (1,true::[]) :: [].
 Succeed Example testing :
@@ -623,7 +648,7 @@ Succeed Example testing :
     function defined in the context of the main one.
     To define a function using a [where] clause, it suffices to start
     a new block after the main body starting with [where] and using
-    [Equations] usual syntax.
+    [Equations]' usual syntax.
     Though be careful that as it is defined in the context of the main
     body, it is not possible to reuse the same names.
 
@@ -641,11 +666,14 @@ rev_acc_aux [] acc := acc;
 rev_acc_aux (a::tl) acc := rev_acc_aux tl (a::acc).
 
 (** Reasoning on functions defined using [where] clauses is a bit more tricky as we
-    need a predicate for the first function, and for the auxiliary function.
-    The first one is usually call the wrapper and the other the worker.
+    need a predicate for the first function, and for the auxiliary function. *)
+
+Check rev_acc_elim.
+
+(** The first one is usually call the wrapper and the other the worker.
     While the first one is obvious as it is the property we are trying to prove,
-    Coq can not invent the second one on its own.
-    Consequently, we can not simply apply [funelim]. We need to apply ourself
+    Coq cannot invent the second one on its own.
+    Consequently, we cannot simply apply [funelim]. We need to apply ourself
     the recurrence principle [rev_acc_elim] automatically generated by [Equations]
     for [rev_acc] that is behind [funelim].
 *)
@@ -653,7 +681,8 @@ rev_acc_aux (a::tl) acc := rev_acc_aux tl (a::acc).
 Lemma rev_acc_rev {A} (l : list A) : rev_acc' l = rev l.
 Proof.
   unshelve eapply rev_acc'_elim.
-  exact (fun A _ l acc aux_res => aux_res = rev l ++ acc). all: cbn; intros.
+  1: exact (fun A _ l acc aux_res => aux_res = rev l ++ acc).
+  all: cbn; intros.
   (* Functional elimination provides us with the worker property initialised
     as in the definition of the main function *)
   - rewrite app_nil in H. assumption.
@@ -662,7 +691,7 @@ Proof.
   - simp rev. rewrite H. rewrite app_assoc. reflexivity.
 Abort.
 
-(** This proof can actually be mostly automatised thanks to [Equations].
+(** This proof can actually be mostly automated thanks to [Equations].
     - We can automatically deal with [app_nil] and [app_assoc] by adding
       them to simplification done by [autorewrite] as done in 1.1.2
     - We can combine that with a proof search using [simp]
@@ -672,7 +701,7 @@ Abort.
 Lemma rev_acc_rev {A} (l : list A) : rev_acc' l = rev l.
 Proof.
   unshelve eapply rev_acc'_elim.
-  exact (fun A _ l acc aux_res => aux_res = rev l ++ acc).
+  1: exact (fun A _ l acc aux_res => aux_res = rev l ++ acc).
   all: cbn; intros; simp rev app in *.
   reflexivity.
 Qed.

From ef2bac240a1c341b6ecc83a1bd67eaef0a6b5689 Mon Sep 17 00:00:00 2001
From: thomas-lamiaux <thomas.lamiaux@ens-paris-saclay.fr>
Date: Mon, 20 May 2024 20:34:10 +0200
Subject: [PATCH 02/10] small edits

---
 src/Tutorial_Equations_basics.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v
index 69b7dc82..ab8f648b 100644
--- a/src/Tutorial_Equations_basics.v
+++ b/src/Tutorial_Equations_basics.v
@@ -71,7 +71,7 @@ Arguments cons {_} _ _.
 
 (** To write a function [f : list A -> B] on lists or another a basic
       inductive type, it suffices to write:
-    - function_name at the beginning of you function rather than Fixpoint
+    - Equations at the beginning of you function rather than Fixpoint
     - For each constructor [cst x1 ... xn] like [cons a l], specify how [f]
       computes on it by writing [f (cst x1 ... xn) := t] where [t] may
       contain [f] recursively.
@@ -371,7 +371,7 @@ Abort.
     by [app_nil : l + [] = l] or [app_assoc : (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)].
     It is possible to extend [autorewrite] to make it automatic by adding
     lemma to the database associated to [f].
-    This can be done by the syntax:
+    This can be done with the following syntax:
 
       [ #[local] Hint Rewrite @name_lemma : function_name. ]
 
@@ -424,7 +424,7 @@ Abort.
 (** In practice, it also often happens in such proofs by functional induction that
     after simplification we get a lot of uninteresting cases, that we would like to
     deal with in an automatic but controlled way.
-    To help us, [Equations] provides us with a tactic [simp f1 ... fn]
+    To help us, [Equations] provides a tactic [simp f1 ... fn]
     that first simplify the goal by [autorewrite with f1 ... fn] then
     tries to solve the goal by a proof search by a particular instance of
     [try typeclasses eauto].

From 5a3166f4c18aae90729b6e1adcb6d3fce14b30f8 Mon Sep 17 00:00:00 2001
From: thomas-lamiaux <thomas.lamiaux@ens-paris-saclay.fr>
Date: Tue, 21 May 2024 02:42:40 +0200
Subject: [PATCH 03/10] small edits

---
 src/Tutorial_Equations_basics.v | 25 ++++++++++++++++---------
 1 file changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v
index ab8f648b..52baba54 100644
--- a/src/Tutorial_Equations_basics.v
+++ b/src/Tutorial_Equations_basics.v
@@ -148,7 +148,8 @@ Equations app'' {A} (l l' : list A) : list A :=
   | []    , l' := l'
   | (a::l), l' := a :: (app'' l l').
 
-(** In this tutorial, we will keep to the first syntax but both are can be used interchangeably..
+(** In this tutorial, we will keep to the first syntax but both are can be
+    used interchangeably.
 
     [Equations] enables us to pattern match on several different
     variables at the same time, for instance, to define a function [nth_option]
@@ -156,9 +157,9 @@ Equations app'' {A} (l l' : list A) : list A :=
 *)
 
 Equations nth_option {A} (n : nat) (l : list A) : option A :=
-nth_option 0 nil := None ;
+nth_option 0 []     := None ;
 nth_option 0 (a::l) := Some a ;
-nth_option (S n) nil := None ;
+nth_option (S n) []     := None ;
 nth_option (S n) (a::l) := nth_option n l.
 
 (** However, be careful that as for definitions using [Fixpoint], the order
@@ -267,13 +268,13 @@ Abort.
     defining [f], and declares them in a hint database named [f].
     For instance, for [app], it proves and declares [app [] l' = l'] and
     [app (a::l) l' = a :: (app l l')].
-    The equalities are named "function_name_equation_n", and you can check
-    them out using the command [Print Rewrite HintDb function_name]:
+    The equalities are named using the scheme "function_name_equation_n", and you
+    can check them out using the command [Print Rewrite HintDb function_name]:
 *)
 
 Print Rewrite HintDb app.
 
-(** It is then possible to simply simplify by the equations associated
+(** It is then possible to simplify by the equations associated
     to function [f1 ... fn] using the tactic [autorewrite with f1 ... fn].
     This provide a better control of unfolding when in proofs as
     compared to cbn the user can choose which functions [f1 ... fn],
@@ -311,9 +312,15 @@ Proof.
   - apply IHl.
 Abort.
 
-(** This process quickly gets tedious and complicated to do by hand on real life
-    examples, especially when using complicated inductive types, or more advanced
-    notions of matching like [with] and [where] clauses (c.f 2. and 3.).
+(** On real life examples, reproducing the patterns by hand with the good
+    induction hypotheses can quickly get tedious, if not challenging.
+    Inductive types and patterns can quickly get complicated.
+    Moreover, function may not even be defined following the natural structure
+    of an inductive type.
+    This is particularly the case when defining functions using more advanced
+    notions of matching like [with] and [where] clauses (c.f 2. and 3.)
+    or well-founded recursion.
+
     Consequently, for each definition, [Equations] derives a functional induction
     principle: this is an induction principle that follows the structure of the
     function, including deep pattern-matching, [with] and [where] clauses,

From e6c7a9b7a85bdc27eda7bc76eea9604bceb26124 Mon Sep 17 00:00:00 2001
From: thomas-lamiaux <thomas.lamiaux@ens-paris-saclay.fr>
Date: Tue, 21 May 2024 04:33:26 +0200
Subject: [PATCH 04/10] added half and refactoring

---
 src/Tutorial_Equations_basics.v | 204 +++++++++++++++++++++-----------
 1 file changed, 132 insertions(+), 72 deletions(-)

diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v
index 52baba54..2d22c6fd 100644
--- a/src/Tutorial_Equations_basics.v
+++ b/src/Tutorial_Equations_basics.v
@@ -31,6 +31,10 @@ Arguments to_fill {_}.
   - 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.4 Extending [autorewrite] and [simp]
   - 2. With clauses
   - 3. Where clauses
 
@@ -216,6 +220,8 @@ Succeed Example testing : fold_right Nat.mul 1 (1::2::3::4::[]) = 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
+
     By default, functions defined using [Equations] are opaque and cannot
     be unfolded with [unfold] nor simplified with [simpl] or [cbn] as one
     would do with a [Fixpoint] definition.
@@ -238,7 +244,7 @@ Proof.
   reflexivity.
 Qed.
 
-(** If one wishes to recover unfolding, it is possible on a case by case
+(** If one really wishes to recover unfolding, it is possible though on a case by case
     basis using the option [Global Transparent f] as shown below.
     It is also possible to set this option globally with [Set Equations
     Transparent], but it is not recommended to casual users.
@@ -290,10 +296,19 @@ Proof.
   intros; induction l. all: autorewrite with app.
   - reflexivity.
   - rewrite IHl. reflexivity.
-Abort.
+Qed.
+
+Lemma app_assoc {A} (l1 l2 l3 : list A) : (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
+Proof.
+  induction l1. all: autorewrite with app.
+  - reflexivity.
+  - rewrite IHl1. reflexivity.
+Qed.
+
+(** *** 1.2.2 Proving properties by functional elimination
 
-(** In the example above of [app_nil], we mimicked the pattern used in the
-    definition of [app] by [induction l].
+    In the examples above [app_nil] and [app_assoc], we mimicked the pattern
+    used in the definition of [app] by [induction l].
     While it works on simple examples, it quickly gets more complicated.
     For instance, consider the barely more elaborate example proving
     that both definition of [nth_option] are equal.
@@ -315,50 +330,69 @@ Abort.
 (** On real life examples, reproducing the patterns by hand with the good
     induction hypotheses can quickly get tedious, if not challenging.
     Inductive types and patterns can quickly get complicated.
-    Moreover, function may not even be defined following the natural structure
-    of an inductive type.
-    This is particularly the case when defining functions using more advanced
-    notions of matching like [with] and [where] clauses (c.f 2. and 3.)
-    or well-founded recursion.
-
-    Consequently, for each definition, [Equations] derives a functional induction
-    principle: this is an induction principle that follows the structure of the
+    Moreover, function may actually not even be defined following the natural
+    structure of an inductive type making it hard to reproduce at all.
+
+    For a simple example, consider the function [half] and [mod2] that
+    are defined recursively on [S (S n)] rather than on [S n]:
+*)
+
+Equations half (n : nat) : nat :=
+half 0 := 0 ;
+half 1 := 0 ;
+half (S (S n)) := S (half n).
+
+Equations mod2 (n : nat) : nat :=
+mod2 0 := 0;
+mod2 1 := 1;
+mod2 (S (S n)) := mod2 n.
+
+(** If we try to naively prove a propertiy [P] about [half] or [mod2]
+    by double induction on [n], we actually quickly get stuck.
+    Indeed, as we can see below, in the recursive case we have to prove
+    [P (S (S n))] knowing [P (S n)] and that [P n -> P (S n)].
+    Yet, in general to be able to reason about [half] or [mod2],
+    we actually need to know that [P n] hold to prove [P (S (S n))].
+*)
+
+Goal forall (P : nat -> Prop) (H0 : P 0) (H1 : P 1) (n : nat), P n.
+Proof.
+  induction n. 1: exact H0.
+  induction n. 1: exact H1.
+  (* We are stuck *)
+Abort.
+
+(** This issue arise more generally as soon as we start defining functions using
+    more advanced notions of matching like [with] and [where] clauses (c.f 2. and 3.),
+    or when defining functions using well-founded recursion.
+
+    Consequently, to help us reason about complex functions, for each definition,
+    [Equations] derives a functional induction principle.
+    This is an induction principle that follows the structure of the
     function, including deep pattern-matching, [with] and [where] clauses,
     correct induction hypotheses and generalisation as in the above example.
     This principle is named using the scheme "function_name_elim".
 
-    For instance, to prove a goal [P] depending on [app_elim] [l], [l'], and [l ++ l'],
-    [app_elim] asserts that it suffices to:
-    - prove the base case [P [] l' l']
-    - and that [P l l' (l ++ l')] implies [P (a :: l) l' (a :: l ++ l'))]
+    For instance, to prove a goal [P] depending on [n] and [half n],
+    [half_elim] asserts that it suffices to prove
+    - [P 0 (half 0)]
+    - [P 1 (half 1)]
+    - and that [P n (half n) -> P (S (S n)) (half (S (S n)))]
+    that is, exactly the pattern we wanted.
 *)
 
-Check app_elim.
+Check half_elim.
 
 (** Moreover, [Equations] comes with a powerful tactic [funelim] that
     applies the induction principle while doing different simplifications.
     To use it, it suffices to write [funelim (function_name a1 ... an)]
     where [a1 ... an] are the arguments you want to do your induction on.
 
-    As an example, let us prove [app_nil], [app_assoc], and [nth_eq] for
+    As an example, let us prove [nth_eq] and [half_mod2] for
     which we can already see the advantages over trying to reproduce the
     pattern matching by hand:
 *)
 
-Lemma app_nil {A} (l : list A) : l ++ [] = l.
-Proof.
-  funelim (app l []). all: autorewrite with app.
-  - reflexivity.
-  - rewrite H. reflexivity.
-Qed.
-
-Lemma app_assoc {A} (l1 l2 l3 : list A) : (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
-Proof.
-  funelim (app l1 l2). all : autorewrite with app.
-  - reflexivity.
-  - rewrite H. reflexivity.
-Qed.
-
 Lemma nth_eq {A} (l : list A) (n : nat) : nth_option n l = nth_option' l n.
 Proof.
   funelim (nth_option n l).
@@ -369,18 +403,73 @@ Proof.
   - apply H.
 Abort.
 
-(** By default, the tactic [autorewrite with f] only simplifies a term by the
+Definition half_mod2 (n : nat) : n = half n + half n + mod2 n.
+Proof.
+  induction n; try reflexivity.
+  induction n; try reflexivity.
+  (* We simplify the goal *)
+  autorewrite with half mod2.
+  rewrite PeanoNat.Nat.add_succ_r. cbn.
+  f_equal. f_equal.
+  (* We then get stuck as we have the wrong hypotheses *)
+  Restart.
+  funelim (half n); try reflexivity.
+  autorewrite with half mod2.
+  rewrite PeanoNat.Nat.add_succ_r. cbn.
+  f_equal. f_equal.
+  (* We now have the good recursion hypotheses *)
+  assumption.
+Qed.
+
+(** *** 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
+    deal with in an automatic but controlled way.
+    To help us, [Equations] provides a tactic [simp f1 ... fn]
+    that first simplify the goal by [autorewrite with f1 ... fn] then
+    tries to solve the goal by a proof search by a particular instance of
+    [try typeclasses eauto].
+    It does so using the equations associated to [f1 ... fn], and the database
+    Below and Subterm meant to TO_FILL.
+
+    Linking [simp] with [funelim] like [funelim sth ; simp f1 ... fn] then
+    enables us to simplify all the goals and at the same to automatically
+    prove uninteresting ones.
+    For instance:
+*)
+
+Definition nth_eq {A} (l : list A) (n : nat) : nth_option n l = nth_option' l n.
+Proof.
+  funelim (nth_option n l); simp nth_option nth_option'.
+  all : reflexivity.
+Abort.
+
+(** As you can see, it does not run [reflexivity] by default.
+    You can add it to the proof search using the command
+    ISSUE *)
+
+(* #[local] Hint Resolve Euqations.Init.reflexivity : Below. *)
+
+Definition nth_eq {A} (l : list A) (n : nat) : nth_option n l = nth_option' l n.
+Proof.
+  funelim (nth_option n l); simp nth_option nth_option'.
+  all : reflexivity.
+Qed.
+
+(** *** 1.2.4 Extending [autorewrite] and [simp]
+
+    By default, the tactic [autorewrite with f] only simplifies a term by the
     equations defining [f], like [[] ++ l = l] for [app].
-    In practice, it can happen that there are more equations
-    that we have proven that we would like to use for automatic simplification
-    when proving further properties.
+    In practice, it can happen that there are more equations that we have proven that
+    we would like to use for automatic simplificationwhen proving further properties.
     For instance, when reasoning on [app], we may want to further always simplify
     by [app_nil : l + [] = l] or [app_assoc : (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)].
-    It is possible to extend [autorewrite] to make it automatic by adding
-    lemma to the database associated to [f].
+    It is possible to extend [autorewrite] (and hence [simp]) to make it automatic,
+    by adding lemma to the database associated to [f].
     This can be done with the following syntax:
 
-      [ #[local] Hint Rewrite @name_lemma : function_name. ]
+      [ #[local] Hint Rewrite @lemma_name : function_name. ]
 
     This is a very powerful personnalisable rewrite mechanism.
     However, note that this mechanism is expressive enough to be
@@ -421,49 +510,20 @@ Qed.
 
 Lemma rev_eq {A} (l l' : list A) : rev_acc l l' = rev l ++ l'.
 Proof.
-  funelim (rev l). all: autorewrite with rev rev_acc app.
+  funelim (rev l);  autorewrite with rev rev_acc app.
   - reflexivity.
   (* There is no more need to call [app_assoc] by hand in proofs *)
   - apply H.
 Abort.
 
-
-(** In practice, it also often happens in such proofs by functional induction that
-    after simplification we get a lot of uninteresting cases, that we would like to
-    deal with in an automatic but controlled way.
-    To help us, [Equations] provides a tactic [simp f1 ... fn]
-    that first simplify the goal by [autorewrite with f1 ... fn] then
-    tries to solve the goal by a proof search by a particular instance of
-    [try typeclasses eauto].
-    It does so using the equations associated to [f1 ... fn], and the database
-    Below and Subterm meant to TO_FILL.
-
-    Linking [simpl] with [funelim] like [funelim sth ; simp f1 ... fn] then
-    enables us to simplify all the goals and at the same to automatically
-    prove uninteresting ones.
-    For instance:
-*)
-
-Definition nth_eq {A} (l : list A) (n : nat) : nth_option n l = nth_option' l n.
-Proof.
-  funelim (nth_option n l). all: simp nth_option nth_option'.
-  all : reflexivity.
-Abort.
-
-(** As you can see, it does not run [reflexivity] by default.
-    You can add it to the proof search using the command
-    ISSUE *)
-
-(* #[local] Hint Resolve Euqations.Init.reflexivity : Below. *)
-
+(** It actually enables to greatly automatise proofs using [simp] *)
 Lemma rev_eq {A} (l l' : list A) : rev_acc l l' = rev l ++ l'.
 Proof.
-  funelim (rev l). all: simp rev rev_acc app.
+  funelim (rev l); simp rev rev_acc app.
   reflexivity.
 Qed.
 
-
-
+(** *** Exercices *)
 
 (** As exercices, you can try to prove the following properties  *)
 Lemma app_length {A} (l l' : list A) : length (l ++ l') = length l + length l'.

From d1c6bba8bac0f9243f493db7eefaaa4265242fe1 Mon Sep 17 00:00:00 2001
From: thomas-lamiaux <thomas.lamiaux@ens-paris-saclay.fr>
Date: Tue, 21 May 2024 04:41:28 +0200
Subject: [PATCH 05/10] small edits

---
 src/Tutorial_Equations_basics.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v
index 2d22c6fd..932cd318 100644
--- a/src/Tutorial_Equations_basics.v
+++ b/src/Tutorial_Equations_basics.v
@@ -449,12 +449,11 @@ Abort.
     You can add it to the proof search using the command
     ISSUE *)
 
-(* #[local] Hint Resolve Euqations.Init.reflexivity : Below. *)
+#[local] Hint Resolve eq_refl : Below.
 
 Definition nth_eq {A} (l : list A) (n : nat) : nth_option n l = nth_option' l n.
 Proof.
   funelim (nth_option n l); simp nth_option nth_option'.
-  all : reflexivity.
 Qed.
 
 (** *** 1.2.4 Extending [autorewrite] and [simp]
@@ -520,7 +519,6 @@ Abort.
 Lemma rev_eq {A} (l l' : list A) : rev_acc l l' = rev l ++ l'.
 Proof.
   funelim (rev l); simp rev rev_acc app.
-  reflexivity.
 Qed.
 
 (** *** Exercices *)

From 2ac361b1cc4f84dae6f15eafe7e487af50a5dd03 Mon Sep 17 00:00:00 2001
From: thomas-lamiaux <thomas.lamiaux@ens-paris-saclay.fr>
Date: Tue, 21 May 2024 06:08:05 +0200
Subject: [PATCH 06/10] adding comments loop rewrite

---
 src/Tutorial_Equations_basics.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v
index 932cd318..26f3aca2 100644
--- a/src/Tutorial_Equations_basics.v
+++ b/src/Tutorial_Equations_basics.v
@@ -471,8 +471,11 @@ Qed.
       [ #[local] Hint Rewrite @lemma_name : function_name. ]
 
     This is a very powerful personnalisable rewrite mechanism.
-    However, note that this mechanism is expressive enough to be
-    non-terminating if the wrong lemmas are added to the database.
+    Actually, this mechanism is expressive enough to be non-terminating if the
+    wrong lemmas are added to the database.
+    Indeed, while it is confluent and terminating using only the defining
+    equations, adding lemma like [add_comm : forall a b, a + b = b + a] will
+    surely create a loop.
 
     To see how it can be useful, let us define a tail-recursive version of
     list reversal and prove it equal the usual one:

From 90e2b2e0e6a5e0628718948adbdf6c6e928e4917 Mon Sep 17 00:00:00 2001
From: thomas-lamiaux <thomas.lamiaux@ens-paris-saclay.fr>
Date: Tue, 21 May 2024 06:49:34 +0200
Subject: [PATCH 07/10] typos

---
 src/Tutorial_Equations_basics.v | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v
index 26f3aca2..9bba4613 100644
--- a/src/Tutorial_Equations_basics.v
+++ b/src/Tutorial_Equations_basics.v
@@ -305,6 +305,10 @@ Proof.
   - rewrite IHl1. reflexivity.
 Qed.
 
+(** Note, you can also use [autorewrite] to simplify hypotheses using
+    [autorewrite with f1 ... fn in H]
+*)
+
 (** *** 1.2.2 Proving properties by functional elimination
 
     In the examples above [app_nil] and [app_assoc], we mimicked the pattern
@@ -313,7 +317,7 @@ Qed.
     For instance, consider the barely more elaborate example proving
     that both definition of [nth_option] are equal.
     We have to be careful to first revert [n] in order to generalise the
-    induction hypothesis and get something strong enough when inducting on [l],
+    induction hypotheses and get something strong enough when inducting on [l],
     and we then need to destruct n.
 *)
 
@@ -543,9 +547,11 @@ Admitted.
 Lemma app_nth1 {A} (n : nat) (l l' : list A) :
       n < length l -> nth_option n (l++l') = nth_option n l.
 Proof.
+  (* intro H; funelim (nth_option n l); simp nth_option app.
+  3: { apply H. apply PeanoNat.lt_S_n. } *)
 Admitted.
 
-(* You will need the lemma [PeanoNat.Nat.sub_succ] and [le_S_n].
+(* You will need the lemma [le_S_n].
   HINT : [funelim] must be applied to the parameters you want to do the induction on.
          Here, it is [n] and [l], and not [(n - length l)] and [l']. *)
 Lemma app_nth2 {A} (n : nat) (l l' : list A) :

From 9a81b68016fe7f6d80f9be839a1a174c97a67ac3 Mon Sep 17 00:00:00 2001
From: thomas-lamiaux <thomas.lamiaux@ens-paris-saclay.fr>
Date: Tue, 21 May 2024 07:21:38 +0200
Subject: [PATCH 08/10] edits + typos

---
 src/Tutorial_Equations_basics.v | 27 +++++++++++++++++++--------
 1 file changed, 19 insertions(+), 8 deletions(-)

diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v
index 9bba4613..cd1c0d80 100644
--- a/src/Tutorial_Equations_basics.v
+++ b/src/Tutorial_Equations_basics.v
@@ -167,11 +167,11 @@ nth_option (S n) []     := None ;
 nth_option (S n) (a::l) := nth_option n l.
 
 (** However, be careful that as for definitions using [Fixpoint], the order
-    of matching matters : it produces term that are equal but with
-    different computation rules.
+    of matching matters: it produces terms that are observationally equal but
+    with different computation rules.
     For instance, if we pattern match on [l] first, we get a function
     [nth_option'] that is equal to [nth_option] but computes differently
-    as it can been seen when proving [eq_nth].
+    as it can been seen below:
 *)
 
 Equations nth_option' {A} (l : list A) (n : nat) : option A :=
@@ -186,9 +186,20 @@ Proof.
   intros.
   autorewrite with nth_option.
   autorewrite with nth_option'.
+  (* We need to further destruct n to simplify *)
+  destruct n; reflexivity.
 Abort.
 
-(** As exercices, you can try to define:
+(** [Equations] also supports nested pattern matching.
+    For instance, we can define a function swapping lists of pairs
+    by matching pairs at the same as we match the list.
+*)
+
+Equations swap_list_pair {A B} (l : list (A * B)) : list (B * A) :=
+swap_list_pair [] := [];
+swap_list_pair ((a , b)::l) := (b,a)::(swap_list_pair l).
+
+(** As exercises, you can try to define:
     - A function [map f l] that applies [f] pointwise, on [ [a1, ... ,an] ] it
       returns [ [f a1, ... , f an] ]
     - A function [head_option] that returns the head of a list and [None] otherwise
@@ -351,7 +362,7 @@ mod2 0 := 0;
 mod2 1 := 1;
 mod2 (S (S n)) := mod2 n.
 
-(** If we try to naively prove a propertiy [P] about [half] or [mod2]
+(** If we try to naively prove a property [P] about [half] or [mod2]
     by double induction on [n], we actually quickly get stuck.
     Indeed, as we can see below, in the recursive case we have to prove
     [P (S (S n))] knowing [P (S n)] and that [P n -> P (S n)].
@@ -465,7 +476,7 @@ Qed.
     By default, the tactic [autorewrite with f] only simplifies a term by the
     equations defining [f], like [[] ++ l = l] for [app].
     In practice, it can happen that there are more equations that we have proven that
-    we would like to use for automatic simplificationwhen proving further properties.
+    we would like to use for automatic simplification when proving further properties.
     For instance, when reasoning on [app], we may want to further always simplify
     by [app_nil : l + [] = l] or [app_assoc : (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)].
     It is possible to extend [autorewrite] (and hence [simp]) to make it automatic,
@@ -528,9 +539,9 @@ Proof.
   funelim (rev l); simp rev rev_acc app.
 Qed.
 
-(** *** Exercices *)
+(** *** Exercises *)
 
-(** As exercices, you can try to prove the following properties  *)
+(** As exercises, you can try to prove the following properties  *)
 Lemma app_length {A} (l l' : list A) : length (l ++ l') = length l + length l'.
 Proof.
 Admitted.

From 773d4bb75b48de4db717899d1d60be2f82c837cd Mon Sep 17 00:00:00 2001
From: thomas-lamiaux <thomas.lamiaux@ens-paris-saclay.fr>
Date: Tue, 21 May 2024 15:42:39 +0200
Subject: [PATCH 09/10] final edits

---
 src/Tutorial_Equations_basics.v | 34 +++++++++++++++++++++------------
 1 file changed, 22 insertions(+), 12 deletions(-)

diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v
index cd1c0d80..b890d41b 100644
--- a/src/Tutorial_Equations_basics.v
+++ b/src/Tutorial_Equations_basics.v
@@ -56,6 +56,7 @@ Arguments to_fill {_}.
   let us start by importing the package:
 *)
 
+From Coq Require Import PeanoNat.
 From Equations Require Import Equations.
 
 (** ** 1.1 Defining functions by dependent pattern matching
@@ -292,10 +293,9 @@ Abort.
 Print Rewrite HintDb app.
 
 (** It is then possible to simplify by the equations associated
-    to function [f1 ... fn] using the tactic [autorewrite with f1 ... fn].
-    This provide a better control of unfolding when in proofs as
-    compared to cbn the user can choose which functions [f1 ... fn],
-    they wants to simplify.
+    to functions [f1 ... fn] using the tactic [autorewrite with f1 ... fn].
+    Note, it is also possible to simplify in hypotheses using
+    [autorewrite with f1 ... fn in H].
 
     As an example, let us prove [app_nil l : l ++ [] = l].
     As [app] is defined by pattern match on [l], we prove the result by
@@ -316,8 +316,12 @@ Proof.
   - rewrite IHl1. reflexivity.
 Qed.
 
-(** Note, you can also use [autorewrite] to simplify hypotheses using
-    [autorewrite with f1 ... fn in H]
+(** This provide a fine control of unfolding as it simplifies only by the defining
+    equations, and will not unfold nothing else, while leaving the possibility to
+    rewrite directly by a specific equation.
+    In particular, compared to [cbn] it will never unfold unwanted terms, like
+    proofs terms that would be part of the definition, for instance, when defining
+    proof carrying function or functions by well-fouded recursion.
 *)
 
 (** *** 1.2.2 Proving properties by functional elimination
@@ -445,8 +449,8 @@ Qed.
     that first simplify the goal by [autorewrite with f1 ... fn] then
     tries to solve the goal by a proof search by a particular instance of
     [try typeclasses eauto].
-    It does so using the equations associated to [f1 ... fn], and the database
-    Below and Subterm meant to TO_FILL.
+    It does so using the equations associated to [f1 ... fn], and the databases
+    [Below] and [Subterm].
 
     Linking [simp] with [funelim] like [funelim sth ; simp f1 ... fn] then
     enables us to simplify all the goals and at the same to automatically
@@ -460,9 +464,15 @@ Proof.
   all : reflexivity.
 Abort.
 
-(** As you can see, it does not run [reflexivity] by default.
-    You can add it to the proof search using the command
-    ISSUE *)
+(** As you can see, by default [simp] does not try to prove goals that hold
+    by definition, like [None = None].
+    If you wish for [simp] to do so, or to try any other tactic, you need to add
+    it as a hint to one of the hint databse used by [simp].
+    Currently, there is no dedicated database for that, and it is hence
+    recommanded to add hints to the hint database [Below].
+    In particular, you can extend [simp] to to prove definitional equality using
+    the following command.
+*)
 
 #[local] Hint Resolve eq_refl : Below.
 
@@ -551,7 +561,7 @@ Lemma nth_overflow {A} (n : nat) (l : list A) : length l <= n -> nth_option n l
 Proof.
 Admitted.
 
-(* You will need to use the lemma [Arith_prebase.lt_S_n]
+(* You will need to use the lemma [PeanoNat.lt_S_n]
   HINT : [funelim] must be applied to the parameters you want to do the induction on.
          Here, it is [n] and [l], and not [n] and [l++l'].
 *)

From b9fb0bac05765711bc0b139213e1cf132d7d269f Mon Sep 17 00:00:00 2001
From: thomas-lamiaux <thomas.lamiaux@ens-paris-saclay.fr>
Date: Tue, 21 May 2024 18:21:18 +0200
Subject: [PATCH 10/10] final edits

---
 src/Tutorial_Equations_basics.v | 37 ++++++++++++++++-----------------
 1 file changed, 18 insertions(+), 19 deletions(-)

diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v
index b890d41b..89fdd8b3 100644
--- a/src/Tutorial_Equations_basics.v
+++ b/src/Tutorial_Equations_basics.v
@@ -53,10 +53,10 @@ Arguments to_fill {_}.
 
 (** * 1. Basic definitions and reasoning
 
-  let us start by importing the package:
+  Let us start by importing the package:
 *)
 
-From Coq Require Import PeanoNat.
+From Coq Require Import Arith.
 From Equations Require Import Equations.
 
 (** ** 1.1 Defining functions by dependent pattern matching
@@ -168,8 +168,8 @@ nth_option (S n) []     := None ;
 nth_option (S n) (a::l) := nth_option n l.
 
 (** However, be careful that as for definitions using [Fixpoint], the order
-    of matching matters: it produces terms that are observationally equal but
-    with different computation rules.
+    of matching matters: it produces terms that are pointwise propositionally
+    equal but with different computation rules.
     For instance, if we pattern match on [l] first, we get a function
     [nth_option'] that is equal to [nth_option] but computes differently
     as it can been seen below:
@@ -182,7 +182,7 @@ nth_option' (a::l) (S n) := nth_option' l n.
 
 Goal forall {A} (a:A) n, nth_option n (nil (A := A)) = nth_option' (nil (A := A)) n.
 Proof.
-  (* Here [autorewrite with f] is a simplification tactic of [Equations] (c.f 1.1.2).
+  (* Here [autorewrite with f] is a simplification tactic of [Equations] (c.f. 1.1.2).
      As we can see, [nth_option'] reduces on [ [] ] to [None] but not [nth_option]. *)
   intros.
   autorewrite with nth_option.
@@ -262,8 +262,8 @@ Qed.
     Transparent], but it is not recommended to casual users.
     To recover simplification by [simpl] and [cbn], one can additionally
     use the command [Arguments function_name !_ /. ].
-    It will simplify the function as soon as it is applied to one argument
-    that is a constructor.
+    It will simplify the function as soon as it is applied to at least one
+    argument that is a constructor.
 *)
 
 Equations f4 (n : nat) : nat :=
@@ -283,7 +283,7 @@ Abort.
 
 (** Rather than using [cbn] or [simpl], for each function [f], [Equations]
     internally proves an equality for each case of the pattern matching
-    defining [f], and declares them in a hint database named [f].
+    defining [f], and declares it in a hint database named [f].
     For instance, for [app], it proves and declares [app [] l' = l'] and
     [app (a::l) l' = a :: (app l l')].
     The equalities are named using the scheme "function_name_equation_n", and you
@@ -317,7 +317,7 @@ Proof.
 Qed.
 
 (** This provide a fine control of unfolding as it simplifies only by the defining
-    equations, and will not unfold nothing else, while leaving the possibility to
+    equations, and will not unfold anything else, while leaving the possibility to
     rewrite directly by a specific equation.
     In particular, compared to [cbn] it will never unfold unwanted terms, like
     proofs terms that would be part of the definition, for instance, when defining
@@ -349,7 +349,7 @@ Abort.
 (** On real life examples, reproducing the patterns by hand with the good
     induction hypotheses can quickly get tedious, if not challenging.
     Inductive types and patterns can quickly get complicated.
-    Moreover, function may actually not even be defined following the natural
+    Moreover, functions may actually not even be defined following the
     structure of an inductive type making it hard to reproduce at all.
 
     For a simple example, consider the function [half] and [mod2] that
@@ -367,7 +367,7 @@ mod2 1 := 1;
 mod2 (S (S n)) := mod2 n.
 
 (** If we try to naively prove a property [P] about [half] or [mod2]
-    by double induction on [n], we actually quickly get stuck.
+    by repeated induction on [n], we actually quickly get stuck.
     Indeed, as we can see below, in the recursive case we have to prove
     [P (S (S n))] knowing [P (S n)] and that [P n -> P (S n)].
     Yet, in general to be able to reason about [half] or [mod2],
@@ -381,14 +381,14 @@ Proof.
   (* We are stuck *)
 Abort.
 
-(** This issue arise more generally as soon as we start defining functions using
-    more advanced notions of matching like [with] and [where] clauses (c.f 2. and 3.),
+(** This issue arises more generally as soon as we start defining functions using
+    more advanced notions of matching like [with] and [where] clauses (c.f. 2. and 3.),
     or when defining functions using well-founded recursion.
 
     Consequently, to help us reason about complex functions, for each definition,
     [Equations] derives a functional induction principle.
     This is an induction principle that follows the structure of the
-    function, including deep pattern-matching, [with] and [where] clauses,
+    function, including nested pattern-matching, [with] and [where] clauses,
     correct induction hypotheses and generalisation as in the above example.
     This principle is named using the scheme "function_name_elim".
 
@@ -466,8 +466,8 @@ Abort.
 
 (** As you can see, by default [simp] does not try to prove goals that hold
     by definition, like [None = None].
-    If you wish for [simp] to do so, or to try any other tactic, you need to add
-    it as a hint to one of the hint databse used by [simp].
+    If you wish for [simp] to do so, or for [simp] to try any other tactic,
+    you need to add it as a hint to one of the hint databses used by [simp].
     Currently, there is no dedicated database for that, and it is hence
     recommanded to add hints to the hint database [Below].
     In particular, you can extend [simp] to to prove definitional equality using
@@ -543,7 +543,7 @@ Proof.
   - apply H.
 Abort.
 
-(** It actually enables to greatly automatise proofs using [simp] *)
+(** It actually enables to greatly automate proofs using [simp] *)
 Lemma rev_eq {A} (l l' : list A) : rev_acc l l' = rev l ++ l'.
 Proof.
   funelim (rev l); simp rev rev_acc app.
@@ -615,7 +615,7 @@ Admitted.
     predicate [p].
     In the case [cons a l], the [with] clause enables us to compute
     the intermediate value [p a] and to check whether it is [true] or [false],
-    and hence if [a] satisfy the predicate [p] and should be kept or not:
+    and hence if [a] satisfies the predicate [p] and should be kept or not:
 *)
 
 Equations filter {A} (l : list A) (p : A -> bool) : list A :=
@@ -798,5 +798,4 @@ Proof.
   unshelve eapply rev_acc'_elim.
   1: exact (fun A _ l acc aux_res => aux_res = rev l ++ acc).
   all: cbn; intros; simp rev app in *.
-  reflexivity.
 Qed.