remove a bunch of deprecate warnings

.github/workflows/docker-action.yml

@@ -15,6 +15,7 @@ jobs:
  strategy:
  matrix:
  image:
+ - 'mathcomp/mathcomp:1.18.0-coq-8.18'
  - 'mathcomp/mathcomp:1.17.0-coq-8.17'
  - 'mathcomp/mathcomp:1.15.0-coq-8.16'
  - 'mathcomp/mathcomp:1.14.0-coq-8.15'

coq-addition-chains.opam

@@ -18,8 +18,8 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
  "dune" {>= "2.5"}
  "coq" {>= "8.14"}
- "coq-paramcoq" {(>= "1.1.3" & < "1.2~") | (= "dev")}
- "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.18"}
+ "coq-paramcoq" {>= "1.1.3"}
+ "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.19"}
  "coq-mathcomp-algebra"
 ]
 

coq-gaia-hydras.opam

@@ -18,9 +18,9 @@ depends: [
  "dune" {>= "2.5"}
  "coq" {>= "8.14"}
  "coq-hydra-battles" {= version}
- "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.18"}
+ "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.19"}
  "coq-mathcomp-zify" {< "2"}
- "coq-gaia-schutte" {>= "1.14" & < "1.18~"}
+ "coq-gaia-schutte" {>= "1.14" & < "1.18"}
 ]
 
 tags: [

coq-goedel.opam

@@ -18,7 +18,7 @@ depends: [
  "dune" {>= "2.5"}
  "coq" {>= "8.14"}
  "coq-hydra-battles" {= version}
- "coq-coqprime" {= "dev"}
+ "coq-coqprime" {>= "1.3.0"}
 ]
 
 tags: [

coq-hydra-battles.opam

@@ -19,7 +19,7 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
  "dune" {>= "2.5"}
  "coq" {>= "8.14"}
- "coq-equations" {(>= "1.2" & < "1.4~") | (= "dev")}
+ "coq-equations" {>= "1.2"}
  "coq-zorns-lemma" {>= "10.2.0"}
  "coq-libhyps"
 ]

meta.yml

@@ -120,6 +120,8 @@ supported_coq_versions:
  opam: '{>= "8.14"}'
 
 tested_coq_opam_versions:
+- version: '1.18.0-coq-8.18'
+ repo: 'mathcomp/mathcomp'
 - version: '1.17.0-coq-8.17'
  repo: 'mathcomp/mathcomp'
 - version: '1.15.0-coq-8.16'
@@ -132,28 +134,28 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
  name: coq-equations
- version: '{(>= "1.2" & < "1.4~") | (= "dev")}'
+ version: '{>= "1.2"}'
  description: |-
  [Equations](https://github.com/mattam82/Coq-Equations) 1.2 or later
 - opam:
  name: coq-paramcoq
- version: '{(>= "1.1.3" & < "1.2~") | (= "dev")}'
+ version: '{>= "1.1.3"}'
  description: |-
  [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
 - opam:
  name: coq-mathcomp-ssreflect
- version: '{(>= "1.13.0" & < "1.18~")}'
+ version: '{>= "1.13.0" & < "1.19"}'
  description: |-
- [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.13 or later
+ [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.13 to 1.18
 - opam:
  name: coq-mathcomp-algebra
  description: |-
  [MathComp Algebra](https://github.com/math-comp/math-comp)
 - opam:
  name: coq-gaia-schutte
- version: '{(>= "1.14" & < "1.18~") | (= "dev")}'
+ version: '{>= "1.14" & < "1.18"}'
  description: |-
- [Gaia's Schütte ordinals](https://github.com/coq-community/gaia) 1.14 or later
+ [Gaia's Schütte ordinals](https://github.com/coq-community/gaia) 1.14 to 1.17
 - opam:
  name: coq-mathcomp-zify
  version: '{< "2~"}'
@@ -165,7 +167,7 @@ dependencies:
  [LibHyps](https://github.com/Matafou/LibHyps)
 - opam:
  name: coq-coqprime
- version: '{= "dev"}'
+ version: '{>= "1.3.0"}'
  description: |-
  [CoqPrime](https://github.com/thery/coqprime)
 - opam:

theories/additions/AM.v

@@ -552,9 +552,9 @@ Function chain_gen (s:signature) {measure signature_measure}
  | (q, 0%N) => 
  (chain_gen (gen_F (gamma i))) ++
  (chain_gen (gen_F (N2pos q)))
- | (q,r) => KFF (chain_gen
- (gen_K (N2pos r)
- (gamma i - N2pos r)))
+ | (q,_r) => KFF (chain_gen
+ (gen_K (N2pos _r)
+ (gamma i - N2pos _r)))
  (chain_gen (gen_F (N2pos q)))
 
  end 
@@ -565,8 +565,8 @@ Function chain_gen (s:signature) {measure signature_measure}
  match N.pos_div_eucl (p + d) (Npos p) with
  | (q, 0%N) => FFK (chain_gen (gen_F p))
  (chain_gen (gen_F (N2pos q)))
- | (q,r) => KFK (chain_gen (gen_K (N2pos r)
- (p - N2pos r)))
+ | (q, _r) => KFK (chain_gen (gen_K (N2pos _r)
+ (p - N2pos _r)))
  (chain_gen (gen_F (N2pos q)))
  end
  end.
@@ -601,20 +601,20 @@ Proof.
  + apply IHc.
  + apply IHc0.
  - cbn; pattern i at 1;
- replace i with (gamma i * (N2pos q) + N2pos r).
+ replace i with (gamma i * (N2pos q) + N2pos _r).
  + cbn in *. 
  * apply KFF_correct;auto.
  replace (gamma i) with 
- (N2pos r + (gamma i - N2pos r)) at 1.
+ (N2pos _r + (gamma i - N2pos _r)) at 1.
  -- apply IHc.
  -- rewrite Pplus_minus;auto with chains.
  apply Pos.lt_gt; rewrite N2pos_lt_switch2. 
  generalize 
  (N.pos_div_eucl_remainder i (N.pos (gamma i) )); 
  rewrite e3; simpl;auto with chains.
- destruct r; [ contradiction | auto with chains].
+ destruct _r; [ contradiction | auto with chains].
  + apply N_pos_div_eucl_rest; auto with chains.
- destruct r;try contradiction; auto with chains. 
+ destruct _r;try contradiction; auto with chains. 
  apply (div_gamma_pos _ _ _ e3); auto with chains.
  apply pos_gt_3;auto with chains.
  destruct (exact_log2 i); [contradiction | reflexivity].
@@ -630,15 +630,15 @@ Proof.
  N2pos_destruct q q.
  injection H4;auto with chains.
  rewrite Pos.mul_comm; auto with chains.
- - cbn; red; replace (p+d) with (p * N2pos q + N2pos r).
+ - cbn; red; replace (p+d) with (p * N2pos q + N2pos _r).
  + apply KFK_correct;auto with chains.
- cbn in *; replace (N2pos r + (p - N2pos r))%positive with p in IHc.
+ cbn in *; replace (N2pos _r + (p - N2pos _r))%positive with p in IHc.
  apply IHc. 
  rewrite Pplus_minus; auto.
  generalize (N.pos_div_eucl_remainder (p + d) (N.pos p));
  rewrite e1; cbn; intro H3.
  apply Pos.lt_gt; rewrite N2pos_lt_switch2;auto with chains.
- destruct r; [contradiction | auto with chains].
+ destruct _r; [contradiction | auto with chains].
 
  + generalize (N.pos_div_eucl_spec (p + d) (N.pos p)). 
  rewrite e1; intros H3. 
@@ -647,7 +647,7 @@ Proof.
  destruct 1;auto with chains.
  rewrite pos2N_inj_add; apply N.le_add_r.
  }
- { intros p0 Hp0;subst q; cbn; destruct r; [ contradiction | ].
+ { intros p0 Hp0;subst q; cbn; destruct _r; [ contradiction | ].
  simpl; simpl in H3; injection H3.
  rewrite Pos.mul_comm; auto with chains.
  }
@@ -702,3 +702,4 @@ Time Compute chain_apply F197887 NPlus 1%N.
 
 Time Compute chain_apply F197887 NPlus 1%N.
 
+

theories/additions/Demo_power.v

@@ -4,11 +4,11 @@ Open Scope M_scope.
 
 Compute 22%Z ^ 20.
 
-Import Int31.
+Import Uint63.
+Search (Z -> int).
+Coercion of_Z : Z >-> int.
 
-Coercion phi_inv : Z >-> int31.
-
-Compute 22%int31 ^ 20.
+Compute 22%int63 ^ 50.
 
 (* end snippet DemoPower *)
 

theories/additions/Dichotomy.v

@@ -171,7 +171,7 @@ Proof.
 intros p H; unfold dicho; generalize (dicho_aux_lt p H).
 intro H0; assert (2 <= N.pos p / (N.pos (dicho_aux p)) )%N.
 - replace 2%N with (2%N * Npos (dicho_aux p) / Npos (dicho_aux p))%N.
- + apply (* N.Div0.div_le_mono. *) N.div_le_mono; try discriminate. 
+ + apply N.div_le_mono; try discriminate. 
  * replace 2%N with (Npos 2%positive); cbn;auto.
  + rewrite N.div_mul; [auto | discriminate].
 - case_eq (N.pos p / N.pos (dicho_aux p))%N.

theories/additions/Euclidean_Chains.v

@@ -162,6 +162,7 @@ Compute the_exponent (F2C F9).
 
 
 
+
 (** A first attempt to define Fchain correctness *)
 
 (* begin snippet BadDefa *)
@@ -1369,9 +1370,9 @@ Function chain_gen (s:signature) {measure signature_measure}
  | (q, 0%N) => 
  Fcompose (chain_gen (gen_F (gamma i)))
  (chain_gen (gen_F (N2pos q)))
- | (q,r) => KFF (chain_gen
- (gen_K (N2pos r)
- (gamma i - N2pos r)))
+ | (q,_r) => KFF (chain_gen
+ (gen_K (N2pos _r)
+ (gamma i - N2pos _r)))
  (chain_gen (gen_F (N2pos q)))
  end end
  | gen_K p d =>
@@ -1380,8 +1381,8 @@ Function chain_gen (s:signature) {measure signature_measure}
  match N.pos_div_eucl (p + d) (Npos p) with
  | (q, 0%N) => FFK (chain_gen (gen_F p))
  (chain_gen (gen_F (N2pos q)))
- | (q,r) => KFK (chain_gen (gen_K (N2pos r)
- (p - N2pos r)))
+ | (q, _r) => KFK (chain_gen (gen_K (N2pos _r)
+ (p - N2pos _r)))
  (chain_gen (gen_F (N2pos q)))
  end
  end.
@@ -1426,23 +1427,23 @@ Proof.
 
 
  - pattern i at 1;
- replace i with (gamma i * (N2pos q) + N2pos r).
+ replace i with (gamma i * (N2pos q) + N2pos _r).
  + destruct IHc, IHc0;split.
  * apply KFF_correct;auto.
  simpl; simpl in H.
  replace (gamma i) with 
- (N2pos r + (gamma i - N2pos r)) at 1.
+ (N2pos _r + (gamma i - N2pos _r)) at 1.
  apply H.
  rewrite Pplus_minus;auto with chains.
  apply Pos.lt_gt; rewrite N2pos_lt_switch2. 
  generalize 
  (N.pos_div_eucl_remainder i (N.pos (gamma i) )); 
  rewrite e3; simpl;auto with chains.
- destruct r; [ contradiction | auto with chains].
+ destruct _r; [ contradiction | auto with chains].
  * apply KFF_proper;auto with chains.
 
  + apply N_pos_div_eucl_rest; auto with chains.
- destruct r;try contradiction; auto with chains. 
+ destruct _r;try contradiction; auto with chains. 
  apply (div_gamma_pos _ _ _ e3); auto with chains.
  apply pos_gt_3;auto with chains.
  destruct (exact_log2 i); [contradiction | reflexivity].
@@ -1468,15 +1469,15 @@ Proof.
  + apply FFK_proper;auto with chains.
 
  - destruct IHc, IHc0; split.
- + red; replace (p+d) with (p * N2pos q + N2pos r).
+ + red; replace (p+d) with (p * N2pos q + N2pos _r).
  * apply KFK_correct;auto with chains.
- red in H; replace (N2pos r + (p - N2pos r))%positive with p in H.
+ red in H; replace (N2pos _r + (p - N2pos _r))%positive with p in H.
  apply H. 
  rewrite Pplus_minus; auto.
  generalize (N.pos_div_eucl_remainder (p + d) (N.pos p));
  rewrite e1; cbn; intro H3.
  apply Pos.lt_gt; rewrite N2pos_lt_switch2;auto with chains.
- destruct r; [contradiction | auto with chains].
+ destruct _r; [contradiction | auto with chains].
 
  * generalize (N.pos_div_eucl_spec (p + d) (N.pos p));
  rewrite e1; intros H3; clear H H0 H1 H2.
@@ -1486,7 +1487,7 @@ Proof.
  rewrite pos2N_inj_add; apply N.le_add_r.
  }
  {
- intros p0 Hp0;subst q; cbn; destruct r; [ contradiction | ].
+ intros p0 Hp0;subst q; cbn; destruct _r; [ contradiction | ].
  simpl; simpl in H3; injection H3.
  rewrite Pos.mul_comm; auto with chains.
  }
@@ -1508,23 +1509,26 @@ Arguments make_chain gamma {_} _ _ _ .
 Compute the_exponent (make_chain dicho 87).
 (* end snippet C87Dicho *)
 
-(** cf Coq workshop 2014 by Jason Grosss *)
 
-Module Examples.
+Require Import Int63.Uint63. 
+Require Import Monoid_instances.
 
-Import Int31.
+Check cpower (make_chain dicho) 10.
+Module Examples.
 Compute cpower (make_chain dicho) 10 12.
 Compute cpower (make_chain dicho) 87 12.
+Search (int -> Z).
+Search (positive -> int).
+
 
-Definition fast_int31_power (x :positive)(n:N) : Z :=
- Int31.phi (cpower (make_chain dicho) n (snd (positive_to_int31 x))).
+Definition fast_int63_power (x :positive)(n:N) : Z :=
+ to_Z (cpower (make_chain dicho) n (of_pos x)).
 
 Definition slow_int31_power (x :positive)(n:N) : Z :=
- Int31.phi (power (snd (positive_to_int31 x)) (N.to_nat n) ).
+ to_Z (power (of_pos x) (N.to_nat n) ).
 
 Definition binary_int31_power (x :positive)(n:N) : Z :=
-Int31.phi (N_bpow (snd (positive_to_int31 x)) n ).
-
+ to_Z (N_bpow (of_pos x) n). 
 
 (** long computations ... *)
 
@@ -1537,7 +1541,7 @@ Arguments big_chain _%type_scope.
 Remark RM : (1 < 56789)%N. 
 Proof. reflexivity. Qed.
 
-Definition M := Nmod_Monoid _ RM.
+Definition M := Nmod_Monoid 56789%N RM.
 
 Definition exp56789 x := chain_apply big_chain (M:=M) x.
 
@@ -1550,12 +1554,6 @@ Eval cbv iota match delta [big_chain chain_apply computation_eval ] zeta beta
 Definition C87' := ltac:( compute_chain C87 ).
 
 
-Time Compute Int31.phi
- (chain_apply big_chain (snd (positive_to_int31 67777))) .
-
-
-Compute Int31.phi (chain_apply big_chain (snd (positive_to_int31 67777))) .
-
 Compute chain_length big_chain.
 
 Goal parametric (make_chain dicho 45319).