From fa907c76d5b92d34a500dd3506d1cfb7238bc173 Mon Sep 17 00:00:00 2001
From: Li-yao Xia <lysxia@gmail.com>
Date: Mon, 28 Oct 2024 23:30:50 +0100
Subject: [PATCH] Update Equations tutorial for coq-equations 1.3.1

---
 src/Tutorial_Equations_basics.v | 10 +++++-----
 src/Tutorial_Equations_wf.v     | 13 ++++++-------
 2 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v
index 2bcdd27..451ad85 100644
--- a/src/Tutorial_Equations_basics.v
+++ b/src/Tutorial_Equations_basics.v
@@ -483,7 +483,7 @@ Abort.
 
 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'.
+  funelim (nth_option n l); simp nth_option nth_option'; reflexivity.
 Qed.
 
 (** *** 1.2.4 Extending [autorewrite] and [simp]
@@ -551,7 +551,7 @@ Abort.
 (** 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.
+  funelim (rev l); simp rev rev_acc app; reflexivity.
 Qed.
 
 (** *** Exercises *)
@@ -673,8 +673,8 @@ Lemma filter_In {A} (x : A) (l : list A) (p : A -> bool)
 Proof.
   funelim (filter l p); simp filter In.
   - intuition congruence.
-  - rewrite Heq; simp filter In. rewrite H. intuition congruence.
-  - rewrite Heq; simp filter In. rewrite H. intuition congruence.
+  - rewrite H. intuition congruence.
+  - rewrite H. intuition congruence.
 Qed.
 
 (** [With] clauses can also be useful to inspect a recursive call.
@@ -802,5 +802,5 @@ Lemma rev_acc_rev {A} (l : list A) : rev_acc' l = rev l.
 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 *.
+  all: cbn; intros; simp rev app in *; reflexivity.
 Qed.
diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v
index cfa58d9..b27410d 100644
--- a/src/Tutorial_Equations_wf.v
+++ b/src/Tutorial_Equations_wf.v
@@ -349,7 +349,7 @@ Defined.
 
 Lemma gcd_same x : gcd x x = x.
 Proof.
-  funelim (gcd x x). all: try lia. reflexivity.
+  funelim (gcd x x). all: lia.
 Qed.
 
 Lemma gcd_spec0 a : gcd a 0 = a.
@@ -367,10 +367,9 @@ Proof.
   - now rewrite Nat.Div0.mod_0_l.
   - reflexivity.
   - now rewrite (Nat.mod_small (S n) (S n0)).
-  - rewrite <- Heqcall.
-    rewrite refl, Nat.Div0.mod_same.
+  - rewrite refl, Nat.Div0.mod_same.
     reflexivity.
-  - rewrite <- Heqcall. rewrite H; auto.
+  - rewrite H; auto.
     rewrite mod_minus; auto.
 Qed.
 
@@ -424,7 +423,7 @@ ack (S m) (S n) := ack m (ack (S m) n).
 
 Definition ack_min {m n} : n < ack m n.
 Proof.
-  Fail timeout 5 (funelim (ack m n)).
+  Timeout 5 (funelim (ack m n)).
 Abort.
 
 (** There are two main solutions to go around similar issues depending on your case.
@@ -479,8 +478,8 @@ Qed.
 
 Module LinearSearch.
 
-Context (f : nat -> bool).
-Context (h : exists m : nat, f m = true).
+Parameter (f : nat -> bool).
+Parameter (h : exists m : nat, f m = true).
 
 (** Knowing there exists an [m : nat] such that [f m = true], we would like to
     actually compute one.