change boilerplate for 8.19 and beyond

.github/workflows/docker-action.yml

@@ -18,16 +18,19 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.19'
+          - 'coqorg/coq:8.18'
+          - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.16'
-          - 'coqorg/coq:8.15'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-coq-art.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -10,8 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Zulip][zulip-shield]][zulip-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/coq-art/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/coq-art/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/coq-art/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/coq-art/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -40,7 +40,7 @@ out of over 200 exercises from the book.
   - Yves Bertot ([**@ybertot**](https://github.com/ybertot))
   - Pierre Castéran ([**@Casteran**](https://github.com/Casteran))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.15 or later (use the corresponding release for other Coq versions)
+- Compatible Coq versions: 8.16 or later (use the corresponding release for other Coq versions)
 - Additional dependencies: none
 - Coq namespace: `coqart`
 - Related publication(s):

ch12_modules/SRC/chap12.v

@@ -452,16 +452,16 @@ Module Nat_Order : DEC_ORDER with Definition A := nat with Definition
 
 
   Theorem lt_le_weak : forall a b:A, lt a b -> le a b.
-  Proof lt_le_weak. 
+  Proof Nat.lt_le_incl.
 
   Theorem lt_diff : forall a b:A, lt a b -> a <> b.
   Proof.
     unfold  lt, le in |- *; intros a b H e;
-      rewrite e in H;  case (lt_irrefl b H).
+      rewrite e in H;  case (Nat.lt_irrefl b H).
   Qed.
 
   Theorem le_lt_or_eq : forall a b:A, le a b -> lt a b \/ a = b.
-  Proof le_lt_or_eq. 
+  Proof (fun a b Hle => proj1 (Nat.lt_eq_cases _ _) Hle).
 
 
   Definition lt_eq_lt_dec : forall a b:A, {lt a b} + {a = b} + {lt b a} :=

ch15_general_recursion/SRC/bdivspec.v

@@ -1,6 +1,13 @@
 Require Export Arith.
 Require Export Lia.
 Require Export ArithRing.
+
+Lemma le_plus_minus_r : forall n m : nat, n <= m -> n + (m - n) = m.
+Proof.
+intros n m Hle.
+rewrite (Nat.add_comm n (m - n)), (Nat.sub_add n m Hle).
+reflexivity.
+Qed.
 
 Lemma sub_decrease : forall b n m:nat, n <= S b -> 0 < m -> n - m <= b.
 Proof. intros; lia. Qed.
@@ -10,11 +17,11 @@ Ltac remove_minus :=
   |  |- context [(?X1 - ?X2 + ?X3)] =>
       rewrite <- (Nat.add_comm X3); remove_minus
   |  |- context [(?X1 + (?X2 - ?X3) + ?X4)] =>
-      rewrite (plus_assoc_reverse X1 (X2 - X3)); remove_minus
+      rewrite <- (Nat.add_assoc X1 (X2 - X3)); remove_minus
   |  |- context [(?X1 + (?X2 + (?X3 - ?X4)))] =>
-      rewrite (plus_assoc X1 X2 (X3 - X4))
+      rewrite (Nat.add_assoc X1 X2 (X3 - X4))
   |  |- (_ = ?X1 + (?X2 - ?X3)) =>
-      apply (fun n m p:nat => plus_reg_l m p n) with X3;
+      apply (fun n m p:nat => proj1 (Nat.add_cancel_l m p n)) with X3;
        try rewrite (Nat.add_shuffle3 X3 X1 (X2 - X3)); 
        rewrite le_plus_minus_r
   end.
@@ -24,7 +31,7 @@ Definition bdivspec :
     n <= b -> 0 < m -> {q : nat &  {r : nat | n = m * q + r /\ r < m}}.
  fix bdivspec 1.
  {  intros b; case b.
-    -  intros n m Hle Hlt; rewrite <- (le_n_O_eq _ Hle);
+    -  intros n m Hle Hlt; rewrite (proj1 (Nat.le_0_r _) Hle);
        exists 0; exists 0; split;
        auto with arith.
        ring.

ch15_general_recursion/SRC/chap15.v

@@ -33,7 +33,7 @@ Proof.
  -  intros b' Hrec m n Hleb Hlt; case (le_gt_dec n m); simpl; auto.
     intros Hle; generalize (Hrec (m-n) n);
     case (bdiv_aux b' (m-n) n); simpl; intros q r Hrec'.
-    rewrite <- plus_assoc; rewrite <- Hrec'; auto with arith.
+    rewrite <- Nat.add_assoc; rewrite <- Hrec'; auto with arith.
     lia. 
 Qed.
 
@@ -72,8 +72,6 @@ Time Eval lazy beta delta iota zeta in
 
 *)
 
-Require Import Lt.
-
 (** Also proven in Coq.Arith.Wf_nat *)
 
 Theorem lt_Acc : forall n:nat, Acc lt n.
@@ -143,7 +141,7 @@ Proof.
             (exist (div_type'' m n 0) m _)
      end); unfold div_type''; auto with arith.
   elim H_spec; intros H1 H2; split; auto.
-  rewrite (le_plus_minus n m H_n_le_m); rewrite H1; ring.
+  rewrite <- (Nat.sub_add n m H_n_le_m), H1; ring.
 Qed.
 
 Definition div :
@@ -214,7 +212,7 @@ Proof.
         rewrite Heq; auto with arith.
         rewrite Heq_test; auto.
   -  exists (0, n'); exists 0; intros k; case k.
-     + intros; elim (lt_irrefl 0); auto.
+     + intros; elim (Nat.lt_irrefl 0); auto.
      +  intros k' Hltp g; simpl; unfold div_it_F at 1.
         rewrite Heq_test; auto.
 Defined.
@@ -262,7 +260,7 @@ Proof.
  intros m; elim m using (well_founded_ind lt_wf).
  intros m' Hrec n h; rewrite div_it_fix_eqn.
  case (le_gt_dec n m'); intros H; trivial.
- pattern m' at 1; rewrite (le_plus_minus n m'); auto.
+ pattern m' at 1; rewrite <- (Nat.sub_add n m'), Nat.add_comm; auto.
  pattern (m'-n) at 1.
  rewrite Hrec with (m'-n) n h; auto with arith.
  case (div_it (m'-n) n h); simpl; auto with arith.
@@ -351,7 +349,7 @@ Proof.
  intros p l Hle.
  lazy beta iota zeta delta [two_power log_domain_inv log];
   fold log two_power.
- apply le_trans with (2 * S (div2 p)); auto with arith.
+ apply Nat.le_trans with (2 * S (div2 p)); auto with arith.
  generalize (double_div2_le (S (S p))); simpl;intro;lia.
 Qed.
 

ch15_general_recursion/SRC/cubic.v

@@ -2,7 +2,14 @@ Require Export Arith.
 Require Export ArithRing.
 Require Export Lia.
 Require Export Wf_nat.
-
+
+Lemma le_plus_minus_r : forall n m : nat, n <= m -> n + (m - n) = m.
+Proof.
+intros n m Hle.
+rewrite (Nat.add_comm n (m - n)), (Nat.sub_add n m Hle).
+reflexivity.
+Qed.
+
 Definition div8_spec:
  forall n,  ({q : nat & {r : nat | n = 8 * q + r /\ r < 8}}).
 Proof.

ch15_general_recursion/SRC/div_it_companion2.v

@@ -21,7 +21,7 @@ Proof.
 intros m; induction m  as [m' Hrec]  using (well_founded_ind lt_wf).
 intros  n h; rewrite div_it_fix_eqn.
 case (le_gt_dec n m'); intros H; trivial.
-pattern m' at 1; rewrite (le_plus_minus n m'); auto.
+pattern m' at 1; rewrite <- (Nat.sub_add n m' H), Nat.add_comm; auto.
 pattern (m' - n) at 1; rewrite Hrec with (m' - n) n h; auto with arith.
 case (div_it (m' - n) n h); simpl; auto with arith.
 Qed.

ch15_general_recursion/SRC/log2_function.v

@@ -83,7 +83,7 @@ Proof.
       intro H.
       case_eq (exp2 p).
       * intro H0; destruct (exp2_positive p);auto.
-      * intros n H0;  rewrite H0 in H.  elimtype False; lia.   
+      * intros n H0;  rewrite H0 in H.  exfalso; lia.   
  - intros p H;  destruct p. 
    +  simpl in H;  subst n; contradiction. 
    +  simpl in H; rewrite (IHn0 p); auto. 

ch15_general_recursion/SRC/log2_it.v

@@ -102,7 +102,7 @@ intros x; case x.
       elim (div2_eq (S (S p))).
       lia.
       lia.
-      apply le_lt_trans with (2 * div2 (S (S p)) + 1).
+      apply Nat.le_lt_trans with (2 * div2 (S (S p)) + 1).
       elim (div2_eq (S (S p))).
       lia.
       lia.

ch15_general_recursion/SRC/sqrt.v

@@ -1,6 +1,13 @@
 Require Export Arith.
 Require Export ArithRing.
 Require Export Lia.
+
+Lemma le_plus_minus_r : forall n m : nat, n <= m -> n + (m - n) = m.
+Proof.
+intros n m Hle.
+rewrite (Nat.add_comm n (m - n)), (Nat.sub_add n m Hle).
+reflexivity.
+Qed.
 
 Ltac CaseEq f := generalize (refl_equal f); 
     pattern f at -1 in |- *; case f.
@@ -77,9 +84,9 @@ Ltac remove_minus :=
   |  |- context [(?X1 - ?X2 + ?X3)] =>
       rewrite <- (Nat.add_comm X3); remove_minus
   |  |- context [(?X1 + (?X2 - ?X3) + ?X4)] =>
-      rewrite (plus_assoc_reverse X1 (X2 - X3)); remove_minus
+      rewrite <- (Nat.add_assoc X1 (X2 - X3)); remove_minus
   |  |- context [(?X1 + (?X2 + (?X3 - ?X4)))] =>
-      rewrite (plus_assoc X1 X2 (X3 - X4))
+      rewrite (Nat.add_assoc X1 X2 (X3 - X4))
   |  |- (_ = ?X1 + (?X2 - ?X3)) =>
       apply (fun n m p:nat => Nat.add_cancel_l m p n) with X3;
        try rewrite (Nat.add_shuffle3 X3 X1 (X2 - X3)); 
@@ -124,7 +131,7 @@ Proof.
 (* When the bound is zero, if n is lower than the bound, it
   is also 0, it is only a matter of computation to check the
   equality. *)
- intros n Hle; rewrite <- (le_n_O_eq _ Hle); simpl in |- *; auto.
+ intros n Hle; rewrite (proj1 (Nat.le_0_r _) Hle); simpl in |- *; auto.
 
  (*We limit simplification to the bsqrt function. *)
  intros b' Hrec n Hle; cbv beta iota zeta delta [bsqrt] in |- *;
@@ -152,7 +159,7 @@ Theorem bsqrt_rem :
    let (s, r) := bsqrt n b in n < (s + 1) * (s + 1).
 Proof.
  intros b; elim b.
- -  intros n Hle; rewrite <- (le_n_O_eq _ Hle); 
+ -  intros n Hle; rewrite (proj1 (Nat.le_0_r _) Hle); 
   simpl in |- *; auto with arith.
 
  (*We limit simplification to the bsqrt function. *)
@@ -173,7 +180,7 @@ Proof.
    the case analysis on this function call. *)
  case (le_gt_dec (4 * s' + 1) (4 * r' + r)).
  *  intros Hle' Heq'; rewrite Heq.
-    apply lt_le_trans with (4 * S q' + 4).
+    apply Nat.lt_le_trans with (4 * S q' + 4).
     auto with arith.
      replace ((2 * s' + 1 + 1) * (2 * s' + 1 + 1)) with
      (4 * ((s' + 1) * (s' + 1))).

ch15_general_recursion/SRC/sqrt_nat_wf.v

@@ -3,6 +3,13 @@ Require Export ArithRing.
 Require Export Lia.
 Require Export Compare_dec.
 Require Export Wf_nat.
+
+Lemma le_plus_minus_r : forall n m : nat, n <= m -> n + (m - n) = m.
+Proof.
+intros n m Hle.
+rewrite (Nat.add_comm n (m - n)), (Nat.sub_add n m Hle).
+reflexivity.
+Qed.
 
 Definition div4_spec:
  forall (n : nat),  ({q : nat & {r : nat | n = 4 * q + r /\ r < 4}}).
@@ -48,9 +55,9 @@ refine (fun n sqrt_nat =>
     * replace (4 * (s' * s' + r'') + r') with ((4 * s') * s' + (4 * r'' + r')).
       replace (((2 * s' + 1) + 1) * ((2 * s' + 1) + 1))
       with ((4 * s') * s' + (8 * s' + 4)).
-      apply plus_lt_compat_l.
+      apply Nat.add_lt_mono_l.
       assert (H: r'' < 2 * s' + 1).
-      { apply plus_lt_reg_l with (s' * s').
+      { apply Nat.add_lt_mono_l with (s' * s').
         rewrite <- Heq'.
         replace (s' * s' + (2 * s' + 1)) with ((s' + 1) * (s' + 1)).
         assumption.

ch16_proof_by_reflection/SRC/chap16.v

@@ -27,10 +27,10 @@ Theorem divisor_smaller :
 Proof.
  intros m p Hlt; case p.
  -  intros q Heq; rewrite Heq in Hlt; rewrite Nat.mul_comm in Hlt.
-    elim (lt_irrefl 0);exact Hlt.
+    elim (Nat.lt_irrefl 0);exact Hlt.
  -  intros p' q; case q.
     +  intros Heq; rewrite Heq in Hlt.
-       elim (lt_irrefl 0);exact Hlt.
+       elim (Nat.lt_irrefl 0);exact Hlt.
     +  intros q' Heq; rewrite Heq.
        rewrite Nat.mul_comm; simpl; auto with arith.
 Qed.
@@ -73,10 +73,10 @@ Theorem Zabs_nat_0 : forall x:Z, Z.abs_nat x = 0 -> (x = 0)%Z.
 Proof.
  intros x; case x.
  -  simpl; auto.
- -  intros p Heq; elim (lt_irrefl 0).
+ -  intros p Heq; elim (Nat.lt_irrefl 0).
     pattern 0 at 2; rewrite <- Heq.
     simpl; apply lt_O_nat_of_P.
- -  intros p Heq; elim (lt_irrefl 0).
+ -  intros p Heq; elim (Nat.lt_irrefl 0).
     pattern 0 at 2; rewrite <- Heq.
     simpl; apply lt_O_nat_of_P.
 Qed.
@@ -207,7 +207,7 @@ Proof.
  -  intros Hcp (k, (Hne1, (Hne1bis, (q, Heq))));
    rewrite Nat.mul_comm in Heq.
     assert (Hle' : k < 1).
-   +  elim (le_lt_or_eq k 1); try(intuition; fail).
+   +  elim (proj1 (Nat.lt_eq_cases k 1)); try(intuition; fail).
       apply divisor_smaller with (2:= Heq); auto.
    + case_eq k.
      intros Heq'; rewrite Heq' in Heq; simpl in Heq; discriminate Heq.
@@ -249,7 +249,7 @@ Time Qed.
 Theorem reflection_test :
  forall x y z t u:nat, x+(y+z+(t+u)) = x+y+(z+(t+u)).
 Proof.
- intros; repeat rewrite plus_assoc; auto.
+ intros; repeat rewrite Nat.add_assoc; auto.
 Qed.
 
 Inductive bin : Set := node : bin->bin->bin | leaf : nat->bin.
@@ -285,7 +285,7 @@ Theorem flatten_aux_valid :
 Proof.
  intros t; elim t; simpl; auto.
  intros t1 IHt1 t2 IHt2 t'; rewrite <- IHt1; rewrite <- IHt2.
- rewrite plus_assoc; trivial.
+ rewrite Nat.add_assoc; trivial.
 Qed.
 
 Theorem flatten_valid : forall t:bin, bin_nat t = bin_nat (flatten t).

ch16_proof_by_reflection/SRC/prime_sqrt.v

@@ -122,17 +122,17 @@ Theorem test_odds_correct :
 Proof.
  induction n.
  -  intros x p Hp1 H1ltx Hn q Hint.
-    elimtype False;  lia.
+    exfalso;  lia.
   - intros x p Hp H1ltx; simpl (test_odds (S n) p (Z_of_nat x));
     intros Htest q (H1ltq, Hqle).
     case_eq (test_odds n (p -2) (Z_of_nat x)).
     + intros Htest'true.
       rewrite Htest'true in Htest.
       unfold divides_bool in Htest.
-      elim (le_lt_or_eq q (2*S n + 1)%nat Hqle).
+      elim (proj1 (Nat.lt_eq_cases q (2*S n + 1)%nat) Hqle).
       *  intros Hqlt.
          assert (Hqle': (q <= (2* S n))%nat) by  lia.
-         elim (le_lt_or_eq q (2 * S n)%nat Hqle').
+         elim (proj1 (Nat.lt_eq_cases q (2 * S n)%nat) Hqle').
          replace (2*S n)%nat with (2*n +2)%nat.
          intros Hqlt'.
          assert (Hqle'' : (q <= 2*n +1)%nat) by lia.
@@ -218,7 +218,7 @@ Proof.
        split.
        case_eq k.
        intros Hk0; rewrite Hk0 in Heq; rewrite Heq in H1ltn;
-       rewrite mult_0_r in H1ltn; lia.
+       rewrite Nat.mul_0_r in H1ltn; lia.
        intros; unfold Z.lt; simpl; auto.
        lia.
        rewrite Zmult_comm; rewrite <- inj_mult; rewrite Heq;auto.

ch16_proof_by_reflection/SRC/verif_divide.v

@@ -32,10 +32,10 @@ Theorem divisor_smaller :
 Proof.
  intros m p Hlt; case p.
  -  intros q Heq; rewrite Heq in Hlt; rewrite Nat.mul_comm in Hlt.
-     elim (lt_irrefl 0);exact Hlt.
+     elim (Nat.lt_irrefl 0);exact Hlt.
  -  intros p' q; case q.
     +  intros Heq; rewrite Heq in Hlt.
-       elim (lt_irrefl _ Hlt).
+       elim (Nat.lt_irrefl _ Hlt).
     + intros q' Heq; rewrite Heq.
       rewrite Nat.mul_comm; simpl; auto with arith.
 Qed.
@@ -44,10 +44,10 @@ Theorem Zabs_nat_0 : forall x:Z, Z.abs_nat x = 0 -> (x = 0)%Z.
 Proof.
  intros x; case x.
  -  simpl; auto.
- -  intros p Heq; elim (lt_irrefl 0).
+ -  intros p Heq; elim (Nat.lt_irrefl 0).
     pattern 0 at 2; rewrite <- Heq.
     simpl; apply lt_O_nat_of_P.
- -  intros p Heq; elim (lt_irrefl 0).
+ -  intros p Heq; elim (Nat.lt_irrefl 0).
     pattern 0 at 2; rewrite <- Heq.
     simpl; apply lt_O_nat_of_P.
 Qed.
@@ -157,7 +157,7 @@ Proof.
  unfold lt; intros p Hle; elim Hle.
  -  intros Hcp (k, (Hne1, (Hne1bis, (q, Heq)))); rewrite Nat.mul_comm in Heq.
     assert (Hle' : k < 1).
-    +  elim (le_lt_or_eq k 1); try(intuition; fail).
+    +  elim (proj1 (Nat.lt_eq_cases k 1)); try(intuition; fail).
        apply divisor_smaller with (2:= Heq); auto.
     +  case_eq k.
        *  intros Heq'; rewrite Heq' in Heq; simpl in Heq; discriminate Heq.