Port the docs to Coq 8.20 (#77)

* update Tuto Equations Basics

* update Tuto Equations Obligations

* port Tuto Equations wf

* port Tutorial search

* Use 8.20 for the CI

* Use 8.20.1 fr the CI

* Use 8.20.1 fr the CI

* update index

.github/workflows/docker-action.yml

@@ -17,7 +17,7 @@ jobs:
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-platform-docs.opam'
-          coq_version: '8.19'
+          coq_version: '8.20.1'
           before_script: |
             startGroup "Workaround permission issue"
               sudo chown -R coq:coq .  # <--

meta.yml

@@ -19,4 +19,4 @@ dependencies:
     name: coq-equations
 opam-file-maintainer: "Théo Zimmermann <[email protected]>"
 tested_coq_opam_versions:
-- version: "8.19"
+- version: "8.20.1"

src/SearchTutorial.v

@@ -1,11 +1,11 @@
 (** * Search tutorial for Coq
-    
+
     *** Summary
 
 	This tutorial is about the powerful [Search] vernacular command in Coq.
 	The [Search] command prints names and types of constants in the local or
 	global context satisfying a number of criteria.
-    
+
     *** Table of content
 
     - 1. Searching for lemmas
@@ -153,8 +153,8 @@ Locate "_ + _".
 
     As a side note, the ["+"] operator between types is the disjoint union. It's
     fine if you don't know what this means, our only concern here is that it
-    exists. 
-    
+    exists.
+
     Now, how does Coq choose between them? What is the current interpretation
     of ["+"]?. *)
 
@@ -183,12 +183,12 @@ Print Visibility.
 
 (** Here, the last scope is [nat_scope], we see all the notations associated
     to it: order relations ([<=], [<], ...) and operations ([+], [*], ...).
-  
+
     If we want to use [+] with its interpretation in [type_scope], without
     changing the opened scope order, we can do so with a scope delimiting key:
 *)
 Check (nat + bool)%type.
-About "_ + _"%type.
+About "_ + _".
 
 (** Scope delimiting keys are abbreviations of scope names, usually obtained by
     removing the [_scope] suffix.
@@ -439,7 +439,8 @@ Search _ in Init.Nat.
 
 (** We can even shadow [PeanoNat.Nat] module in this file: *)
 Module Nat.
-  Lemma foo : 21 + 21 = 42. Proof. reflexivity. Qed.
+  Lemma foo : 21 + 21 = 42.
+  Proof. reflexivity. Qed.
 End Nat.
 
 Search _ in Nat.

src/Tutorial_Equations_Obligations.v

@@ -69,13 +69,13 @@ Definition vec A n := { l : list A | length l = n }.
     [vapp : vec A n -> vec A m -> vec A (n + m)], as done below, one has to:
     - specify that the concatenation of [l] and [l'] is [app l l'] and,
     - provide a proof term that [length (ln ++ lm) = n + m], which is done
-      below by the term [eq_trans (app_length ln lm) (f_equal2 Nat.add Hn Hm)].
+      below by the term [eq_trans (length_app ln lm) (f_equal2 Nat.add Hn Hm)].
 *)
 
 Equations vapp {A n m} (v1 : vec A n) (v2 : vec A m) : vec A (n + m) :=
 vapp (exist _ ln Hn) (exist _ lm Hm) :=
       (exist _ (app ln lm)
-               (eq_trans (app_length ln lm) (f_equal2 Nat.add Hn Hm))).
+               (eq_trans (length_app ln lm) (f_equal2 Nat.add Hn Hm))).
 
 (** Yet, in most cases, when defining a function, we do not want to write down
     the proofs directly as terms, as we did above.
@@ -108,7 +108,7 @@ vapp (exist _ ln Hn) (exist _ lm Hm) :=
 Equations vapp' {A n m} (v1 : vec A n) (v2 : vec A m) : vec A (n + m) :=
 vapp' (exist _ ln Hn) (exist _ lm Hm) := exist _ (app ln lm) _.
 Next Obligation.
-  apply app_length.
+  apply length_app.
 Qed.
 
 (** As you can see, this is very practical, however, you should be aware of
@@ -154,7 +154,7 @@ Obligations of vmap_obligations.
 *)
 
 Next Obligation.
-  apply map_length.
+  apply length_map.
 Qed.
 
 (** Using [Next Obligation] has the advantage that once an obligation has been
@@ -177,7 +177,7 @@ Qed.
 Equations? vmap' {A B n} (f : A -> B) (v : vec A n) : vec B n :=
 vmap' f (exist _ ln Hn) := exist _ (map f ln) _ .
 Proof.
-  apply map_length.
+  apply length_map.
 Defined.
 
 (** Though, note that [Equations?] triggers a warning when used on a definition

src/Tutorial_Equations_basics.v

@@ -49,7 +49,6 @@
   Let us start by importing the package:
 *)
 
-From Coq Require Import Arith.
 From Equations Require Import Equations.
 
 Axiom to_fill : forall A, A.
@@ -403,7 +402,7 @@ Abort.
 Check half_elim.
 
 (** Moreover, [Equations] comes with a powerful tactic [funelim] that
-    applies the induction principle while doing different simplifications.
+    applies the functional induction principle and simplifies the associated definition.
     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.
 
@@ -415,7 +414,7 @@ Check half_elim.
 Lemma nth_eq {A} (l : list A) (n : nat) : nth_option n l = nth_option' l n.
 Proof.
   funelim (nth_option n l).
-  all: autorewrite with nth_option nth_option'.
+  all: autorewrite with nth_option'.
   - reflexivity.
   - reflexivity.
   - reflexivity.
@@ -425,8 +424,8 @@ 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.
-  induction n; try reflexivity.
+  induction n. 1: reflexivity.
+  induction n. 1: reflexivity.
   (* We simplify the goal *)
   autorewrite with half mod2.
   rewrite PeanoNat.Nat.add_succ_r. cbn.
@@ -437,7 +436,7 @@ 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.
+  funelim (half n). 1-2: reflexivity.
   autorewrite with half mod2.
   rewrite PeanoNat.Nat.add_succ_r. cbn.
   f_equal. f_equal.
@@ -472,14 +471,12 @@ 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 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].
+    you need to add it as a hint to one of the hint databse [simp] used by [simp].
     In particular, you can extend [simp] to to prove definitional equality using
     the following command.
 *)
 
-#[local] Hint Resolve eq_refl : Below.
+#[local] Hint Resolve eq_refl : simp.
 
 Definition nth_eq {A} (l : list A) (n : nat) : nth_option n l = nth_option' l n.
 Proof.
@@ -595,8 +592,9 @@ Admitted.
 
 (** ** 2. With clauses
 
-    The structure of real programs is generally richer than a simple case tree on the
-    original arguments.
+    The structure of real programs is generally richer than a simple case tree
+    on the original arguments.
+
     In the course of a computation, we might want to compute or scrutinize
     intermediate results (e.g. coming from function calls) to produce an answer.
     In terms of dependent pattern matching, this literally means adding a new
@@ -641,7 +639,8 @@ Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
 filter' [] p => [];
 filter' (a :: l) p with p a => {
   | true  => a :: filter' l p
-  | false => filter' l p }.
+  | false => filter' l p
+  }.
 
 (** To show that [filter] is well-behaved, we can define a predicate [In] and
     check that if an element is in the list and verifies the predicate,
@@ -658,23 +657,33 @@ In x (a::l) => (x = a) \/ In x l.
     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], 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.
+    For regular patterns, simplifying [filter] behaves as usual when using [funelim]:
 *)
 
 Lemma filter_In {A} (x : A) (l : list A) (p : A -> bool)
       : In x (filter l p) <-> In x l /\ p x = true.
 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.
+
+(** However, simplifying [with] clauses can make subclauses appear corresponding
+    to the different branches of the [with] clause.
+    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.
+*)
+
+Lemma filter_filter' {A} (l : list A) (p : A -> bool)
+      : filter l p = filter' l p.
+Proof.
+  funelim (filter l p); simp filter'.
+  - rewrite Heq. cbn. reflexivity.
+  - rewrite Heq. cbn. reflexivity.
 Qed.
 
 (** [With] clauses can also be useful to inspect a recursive call.

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: try lia.
 Qed.
 
 Lemma gcd_spec0 a : gcd a 0 = a.
@@ -367,11 +367,8 @@ 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.
-    reflexivity.
-  - rewrite <- Heqcall. rewrite H; auto.
-    rewrite mod_minus; auto.
+  - now rewrite refl, Nat.Div0.mod_same.
+  - rewrite H; auto. now rewrite mod_minus.
 Qed.
 
 
@@ -415,49 +412,19 @@ ack (S m) 0     := ack m 1;
 ack (S m) (S n) := ack m (ack (S m) n).
 
 
-(** In principle, we should be able to reason about [ack] as usual using [funelim].
-    Unfortunately, in this particular case, [funelim] runs forever which you can
-    check out below.
-    It is a known issue currently being fixed due to oversimplification being done
-    by [funelim].
+(** Reasoning about [ack] works as usual whether the pattern is general or specialized:
 *)
 
 Definition ack_min {m n} : n < ack m n.
 Proof.
-  Fail timeout 5 (funelim (ack m n)).
-Abort.
-
-(** There are two main solutions to go around similar issues depending on your case.
-
-    If your pattern is fully generic, i.e. of the form [ack m n], you can apply
-    functional elimination directly by [apply ack_elim].
-    Though note, that in this case you may need to generalise the goal by hand,
-    in particular by equalities (e.g. using the remember tactic) if the function
-    call being eliminated is not made of distinct variables.
-*)
-Definition ack_min {m n} : n < ack m n.
-Proof.
-  apply ack_elim; intros; eauto with arith.
+  funelim (ack m n). all: eauto with arith.
 Qed.
 
-(** However, if your pattern is partially specialised like [ack 1 n],
-    it can be better to finish reproducing the pattern using [induction].
-    Indeed, [ack_elim] "reproduces" the full pattern, that is, it generalises [1]
-    to [m] and tries to prove [ack m n = 2 + n] by induction, creating cases like
-    [ack (S m) n] which clearly are not warranted here.
-*)
-
 Definition ack1 {n} : ack 1 n = 2 + n.
 Proof.
-  (* If we apply [ack_elim], we get unwarranted cases *)
-  apply ack_elim; intros.
-Abort.
-
-(* So we reproduce the pattern with induction *)
-Definition ack1 {n} : ack 1 n = 2 + n.
-  induction n; simp ack.
+  funelim (ack 1 n); simp ack.
   - reflexivity.
-  - rewrite IHn. reflexivity.
+  - rewrite H. reflexivity.
 Qed.
 
 
@@ -477,7 +444,7 @@ Qed.
     This is represented by this context:
  *)
 
-Module LinearSearch.
+Section LinearSearch.
 
 Context (f : nat -> bool).
 Context (h : exists m : nat, f m = true).
@@ -504,22 +471,21 @@ Context (h : exists m : nat, f m = true).
 
 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.
+Lemma wf_R_m_le m (p : f m = true) : forall n, m <= n -> Acc R n.
 Proof.
   intros n H. constructor. intros ? [h' ?].
   specialize (h' m H).
   congruence.
 Qed.
 
-
-Lemma wf_R_lt_m m (h : f m = true) : forall n, n < m -> Acc R n.
+Lemma wf_R_lt_m m (p : f m = true) : forall n, n < m -> Acc R n.
 Proof.
   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.
+  set (k := m - n) in *; clearbody k. clear p H.
   (* Proof *)
   induction k.
   - easy.
@@ -529,7 +495,7 @@ Qed.
    (** We can now prove that the relation is well-founded: *)
 Lemma wf_R : (exists n : nat, f n = true) -> well_founded R.
 Proof.
-    intros [m h] n. destruct (le_lt_dec m n).
+    intros [m p] n. destruct (le_lt_dec m n).
     - eapply wf_R_m_le; eassumption.
     - eapply wf_R_lt_m; eassumption.
 Qed.
@@ -631,7 +597,7 @@ Abort.
     elements [(a, eq_refl) : {b : A | a = b}].
 *)
 
-Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl.
+Print inspect.
 
 Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).
 

src/index.html

@@ -90,11 +90,11 @@ <h3>Small Disclamer</h3>
           In the future, the documentation is planned to be indexed on the
           Coq Platform's version, but as of yet, it is only guaranteed to fully work
           with the latest version of the
-          <a href="https://github.com/coq/platform/blob/main/doc/README~8.19~2024.10.md">Coq Platform</a> for Coq 8.19.2.
+          <a href="https://github.com/coq/platform/blob/main/doc/README~8.20~2025.01.md">Coq Platform</a> for Coq 8.19.2.
         </li>
         <li>
           The interactive interface is relying on JsCoq1 that only supports Coq up to 8.17
-          so it may fail on some content requiring Coq 8.19.
+          so it may fail on some content requiring Coq 8.20.1.
           We are working towards switching to JsCoq2.
         </li>
       </ul>