Adapt addition chains to Rocq dev

coq-addition-chains.opam

@@ -19,7 +19,7 @@ depends: [
   "dune" {>= "2.5"}
   "coq" {>= "8.16"}
   "coq-elpi" {>= "1.16.0"}
-  "coq-mathcomp-ssreflect" {>= "1.15.0" & < "1.19"}
+  "coq-mathcomp-ssreflect" {>= "2.0.0"}
   "coq-mathcomp-algebra"
 ]
 

theories/additions/Demo.v

@@ -4,7 +4,7 @@ Module Alt.
 
 End Alt.
 
-From Coq Require Import Arith Lia Even.
+From Coq Require Import Arith Lia.
 
 Lemma alt_double_ok n : Nat.double n = Alt.double n.
 Proof.
@@ -13,4 +13,3 @@ Proof.
 Qed.
 
 
-

theories/additions/Euclidean_Chains.v

@@ -1536,7 +1536,7 @@ Definition big_chain := ltac:(compute_chain  (make_chain dicho 45319)).
 
 Print big_chain.
 
-Arguments big_chain _%type_scope.
+Arguments big_chain _%_type_scope.
 
 Remark RM : (1 < 56789)%N. 
 Proof. reflexivity. Qed.
@@ -1644,4 +1644,3 @@ Extraction "bigmod" Examples.exp56789.
 
 Recursive Extraction cpower.
 Recursive Extraction make_chain.
-

theories/additions/Monoid_def.v

@@ -141,25 +141,25 @@ Class EMonoid (A:Type)(E_op : Mult_op A)(E_one : A)
 
 #[ global ] Instance Equiv_Equiv (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
-   Equivalence E_eq.
+   Equivalence (@equiv A E_eq).
 destruct M;auto.
 Qed.
 
 #[ global ] Instance Equiv_Refl (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
-   Reflexive E_eq.
+   Reflexive (@equiv A E_eq).
 destruct (Equiv_Equiv   M);auto.
 Qed.
 
 #[ global ] Instance Equiv_Sym (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
-   Symmetric E_eq.
+   Symmetric (@equiv A E_eq).
 destruct (Equiv_Equiv   M);auto.
 Qed.
 
 #[ global ] Instance Equiv_Trans (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
-   Transitive E_eq.
+   Transitive (@equiv A E_eq).
 destruct (Equiv_Equiv   M);auto.
 Qed.
 
@@ -215,4 +215,3 @@ Class Abelian_Monoid `(M:Monoid ):= {
 Ltac add_op_proper M H := 
  let h := fresh H in
    generalize (@Eop_proper _ _ _ _ M); intro h.
-

theories/additions/Pow.v

@@ -13,7 +13,7 @@ binary method, that takes less than $2\times \log_2(n)$ multiplications.
 
 Set Implicit Arguments.
 
-Require Export ZArith  Div2.
+Require Export ZArith.
 Require Export Recdef.
 Require Import Relations Morphisms.
 
@@ -66,7 +66,7 @@ Proof. reflexivity. Qed.
 
 Lemma power_eq3  `{M: @EMonoid A  E_op E_one E_eq}(x:A) :
  x ^ 1 == x.
-Proof. cbn;  rewrite Eone_right; reflexivity. Qed.
+Proof. cbn; apply Eone_right. Qed.
 (* end snippet powerEqns *)
 
 (** *** The binary exponentiation function (exponents in  [positive])  *)
@@ -162,8 +162,8 @@ Ltac monoid_simpl := repeat monoid_rw.
 (* end snippet powerProper *)
 Proof.
   intros x y Hxy n p Hnp;  subst p; induction n.
-  - reflexivity.
-  - cbn; now rewrite IHn, Hxy.
+  - exact (@Equiv_Refl A E_op E_one E_eq M E_one).
+  - cbn; apply Eop_proper; assumption.
 Qed.
 
 (* begin snippet powerOfPlus:: no-out *)

theories/additions/Pow_variant.v

@@ -11,7 +11,7 @@ the "axioms" of monoid structure.
 
 Set Implicit Arguments.
 
-Require Export ZArith  Div2.
+Require Export ZArith.
 Require Export Recdef.
 Require Import Relations Morphisms.
 
@@ -61,7 +61,7 @@ Proof. reflexivity. Qed.
 
 Lemma power_eq3 {A:Type} `{M: @EMonoid A  E_op E_one E_eq}(x:A) :
  x ^ 1 == x.
-Proof. cbn;  rewrite Eone_right; reflexivity. Qed.
+Proof. cbn; apply Eone_right. Qed.
 
 
 (** *** The binary exponentiation function (exponents in  [positive])  *)
@@ -146,8 +146,8 @@ Section About_power.
 #[global] Instance power_proper : Proper (equiv ==> eq ==> equiv) power.
 Proof.
   intros x y Hxy n p Hnp;  subst p; induction n.
-  - reflexivity.
-  - cbn; now rewrite IHn, Hxy.
+  - exact (@Equiv_Refl A E_op E_one E_eq M E_one).
+  - cbn; apply Eop_proper; assumption.
 Qed.
 
 Lemma power_of_plus : forall x n p, x ^ (n + p) ==  x ^ n *  x ^ p.

theories/additions/fib.v

@@ -5,6 +5,8 @@ From Coq Require Import Extraction ZArith Lia.
 
 From mathcomp Require Import all_ssreflect all_algebra.
 
+Set SsrOldRewriteGoalsOrder.
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -537,4 +539,3 @@ Definition bigarg := 30000%positive.
 
 Extraction "bigfib" Z.ltb Z.div_eucl Pos.iter Z.log2 fastexp4
   my_pow m4lmul m3lmul m2lmul m4lfib m3lfib m2lfib bigarg.
-