remove a bunch of deprecate warnings

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.Div0.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. 
 
 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).

theories/additions/Monoid_instances.v

@@ -10,7 +10,7 @@ Require Import RelationClasses Morphisms.
 Require Import ZArith PArith.
 Require Import Arith.
 Require Import NArith.
-Require Import Ring31.
+Require Import Ring63.
 
 Open Scope Z_scope.
 
@@ -100,52 +100,52 @@ Proof.
 Qed.
 
 
-Import Int31.
-Open Scope int31_scope.
+Import Uint63.
+Open Scope int63_scope.
 
-(** ***  Multiplicative monoid on 31-bits integers 
+(** ***  Multiplicative monoid on 63-bits integers 
 
 Cyclic numeric types are  good candidates for testing exponentiations
 with big exponents, since the size of data is bounded.
 
 
-The type [int31] is defined in Standard Library in Module
-[Coq.Numbers.Cyclic.Int31.Int31].
+The type [int63] is defined in Standard Library in Module
+[Coq.Numbers.Cyclic.Int63.Uint63].
 *)
 
 (* begin snippet int31:: no-out *)
-#[ global ] Instance int31_mult_op : Mult_op int31 := mul31.
+#[ global ] Instance int63_mult_op : Mult_op int := mul.
 
-#[ global ] Instance  Int31mult : Monoid int31_mult_op  1.
+#[ global ] Instance  Int63mult : Monoid int63_mult_op  1.
 Proof.
-   split;unfold int31_mult_op, mult_op; intros; ring.
+   split;unfold int63_mult_op, mult_op; intros; ring.
 Qed.
-(* end snippet int31 *)
+(* end snippet int63 *)
 
 
 
   (* begin snippet BadFact *)
 Module Bad.
 
-  Fixpoint int31_from_nat (n:nat) :=
+  Fixpoint int63_from_nat (n:nat) :int :=
     match n with
     | O => 1
-    | S p => 1 + int31_from_nat p
+    | S p => 1 + int63_from_nat p
     end.
 
-  Coercion int31_from_nat : nat >-> int31.
+  Coercion int63_from_nat : nat >-> int.
 
-  Fixpoint fact (n:nat) := match n with
+  Fixpoint fact (n:nat) : int := match n with
                              O => 1
                            | S p => n * fact p
                            end.
-  Compute fact 40. 
+  Compute fact 160. 
 
 End Bad. 
 (* end snippet BadFact *)
 
 
-Close Scope int31_scope.
+Close Scope int63_scope.
 
 
 (** *** Monoid of 2x2 matrices 
@@ -262,9 +262,9 @@ Section Nmodulo.
   Proof.
     unfold mod_equiv, mod_op, mult_mod, mod_eq.
     intros x y Hxy z t Hzt.
-    repeat rewrite N.mod_mod; auto with chains.
-    rewrite (N.mul_mod x z);auto with chains.
-    rewrite (N.mul_mod y t);auto with chains.
+    repeat rewrite N.Div0.mod_mod; auto with chains.
+    rewrite (N.Div0.mul_mod x z);auto with chains.
+    rewrite (N.Div0.mul_mod y t);auto with chains.
     rewrite Hxy, Hzt; reflexivity.
   Qed.
 
@@ -277,8 +277,8 @@ Section Nmodulo.
   Proof.
     intros  x y z.
     unfold mod_op, mult_op, mult_mod.
-    rewrite N.mul_mod_idemp_r;auto with chains.
-    rewrite N.mul_mod_idemp_l;auto with chains.
+    rewrite N.Div0.mul_mod_idemp_r;auto with chains.
+    rewrite N.Div0.mul_mod_idemp_l;auto with chains.
     now rewrite  N.mul_assoc.
   Qed.
 
@@ -287,14 +287,14 @@ Section Nmodulo.
   (* end snippet Nmoduloe *)
   Proof.
     unfold equiv, mod_equiv, mod_eq, mult_op, mod_op, mult_mod.
-    intro x; rewrite N.mul_1_l, N.mod_mod; auto with chains.
+    intro x; rewrite N.mul_1_l, N.Div0.mod_mod; auto with chains.
   Qed.
   (* begin snippet Nmodulof:: no-out *)
   Lemma one_mod_neutral_r  : forall x, x * 1 == x.
   (* end snippet Nmodulof *)
   Proof.
     unfold equiv, mod_equiv, mod_eq, mult_op, mod_op, mult_mod.
-    intro x; rewrite N.mul_1_r, N.mod_mod; auto with chains.
+    intro x; rewrite N.mul_1_r, N.Div0.mod_mod; auto with chains.
   Qed.
 
 

theories/goedel/PRrepresentable.v

@@ -1545,7 +1545,7 @@ Proof.
               ** elim closedNN with v. exists x0; auto.
               ** destruct H6. destruct H5 as [H5 | H5]; try congruence.
                  fold (freeVarT (n2t a)) in H5. simpl in H5.
-                 rewrite <- app_nil_end in H5. elim (closedNatToTerm _ _ H5).
+                 rewrite  app_nil_r in H5. elim (closedNatToTerm _ _ H5).
               ** apply impE with (LT (var x) (n2t a)).
                  --- apply sysWeaken. apply boundedLT. intros n H5.
                      rewrite (subFormulaNot LNN).

theories/goedel/rosserPA.v

@@ -425,7 +425,7 @@ Proof.
         exists x0; intros g H1; apply extendsPA.
         fold mem; auto.
       + exists (LNN2LNT_formula x :: nil); split.
-        * simpl; repeat rewrite <- app_nil_end.
+        * simpl; repeat rewrite app_nil_r.
           apply (LNN2LNT_freeVarF1 x).
         * exists (AXM _ (LNN2LNT_formula x)).
           intros g H1; induction H1 as [H1| H1].