Remove Restart and ltac:(...)

src/Tutorial_Equations_basics.v

@@ -270,7 +270,11 @@ Global Transparent f4.
 Goal f4 3 = 4.
 Proof.
   (* [f4] can now be unfolded *)
-  unfold f4. Restart.
+  unfold f4.
+Abort.
+
+Goal f4 3 = 4.
+Proof.
   (* Yet, it still cannot be simplify by [cbn] *)
   Fail progress cbn.
   (* [Arguments] enables to recover simplification *)
@@ -418,6 +422,7 @@ Proof.
   - apply H.
 Abort.
 
+(* Doing induction naively to reproduce a pattern can get you stuck *)
 Definition half_mod2 (n : nat) : n = half n + half n + mod2 n.
 Proof.
   induction n; try reflexivity.
@@ -427,7 +432,11 @@ Proof.
   rewrite PeanoNat.Nat.add_succ_r. cbn.
   f_equal. f_equal.
   (* We then get stuck as we have the wrong hypotheses *)
-  Restart.
+Abort.
+
+(* Wheras funelim does it automatically for you *)
+Definition half_mod2 (n : nat) : n = half n + half n + mod2 n.
+Proof.
   funelim (half n); try reflexivity.
   autorewrite with half mod2.
   rewrite PeanoNat.Nat.add_succ_r. cbn.

src/Tutorial_Equations_wf.v

@@ -451,8 +451,10 @@ Definition ack1 {n} : ack 1 n = 2 + n.
 Proof.
   (* If we apply [ack_elim], we get unwarranted cases *)
   apply ack_elim; intros.
-  Restart.
-  (* So we reproduce the pattern with induction *)
+Abort.
+
+(* So we reproduce the pattern with induction *)
+Definition ack1 {n} : ack 1 n = 2 + n.
   induction n; simp ack.
   - reflexivity.
   - rewrite IHn. reflexivity.
@@ -496,23 +498,29 @@ Context (h : exists m : nat, f m = true).
       Consequently, to prove [Acc n] when [n < m], we want to reason by induction
       on [k := m - n]. To do so, we add [n = S m] to the relation.
 
-    This gives us the following relation and proof of our intuition:
+    This gives us the following relation and proof of our intuition.
+    Note that understanding the proofs doe not matter for this tutorial.
 *)
 
 Definition R n m := (forall k, k <= m -> f k = false) /\ n = S m.
 
 Lemma wf_R_m_le m (h : f m = true) : forall n, m <= n -> Acc R n.
 Proof.
   intros n H. constructor. intros ? [h' ?].
-  specialize (h' m ltac:(auto)).
+  specialize (h' m H).
   congruence.
 Qed.
 
+
 Lemma wf_R_lt_m m (h : f m = true) : forall n, n < m -> Acc R n.
 Proof.
-  intros n H. assert (Acc R m) by (eapply wf_R_m_le; eauto).
-  rewrite <- (Nat.sub_add n m ltac:(lia)) in *.
+  intros n H.
+  (* Prove Acc m *)
+  assert (Acc R m) as Hm_acc by (eapply wf_R_m_le; eauto).
+  (* Set up induction on k := m - n *)
+  rewrite <- (Nat.sub_add n m) in * by lia.
   set (k := m - n) in *; clearbody k. clear h H.
+  (* Proof *)
   induction k.
   - easy.
   - apply IHk. constructor. intros ? [? ->]. assumption.