Merge pull request #170 from coq-community/Fix818Warnings

remove a bunch of deprecate warnings
coq-community · Jan 7, 2024 · c27a80b · c27a80b
2 parents 45e65f5 + e8b4ad8
commit c27a80b
Show file tree

Hide file tree

Showing 23 changed files with 117 additions and 114 deletions.
diff --git a/.github/workflows/docker-action.yml b/.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'

diff --git a/coq-addition-chains.opam b/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"
 ]
 

diff --git a/coq-gaia-hydras.opam b/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: [

diff --git a/coq-goedel.opam b/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: [

diff --git a/coq-hydra-battles.opam b/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"
 ]

diff --git a/meta.yml b/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:

diff --git a/theories/additions/AM.v b/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.
 
+
diff --git a/theories/additions/Demo_power.v b/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 *)
 

diff --git a/theories/additions/Dichotomy.v b/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.

diff --git a/theories/additions/Euclidean_Chains.v b/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).