Merge pull request #104 from rocq-community/warn-cleaner

Handle some deprecation warnings

Author: proux01

BigNumPrelude.v

@@ -315,8 +315,7 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
   Z.gcd a b = 0.
  Proof.
  intros.
- generalize (Zgcd_is_gcd a b); destruct 1.
- destruct H2 as (k,Hk).
+ pose proof (Z.gcd_divide_r a b) as (k, Hk).
  generalize H; rewrite Hk at 1.
  destruct (Z.eq_dec (Z.gcd a b) 0) as [H'|H']; auto.
  rewrite Z_div_mult_full; auto.
@@ -326,9 +325,7 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
  Lemma Zgcd_mult_rel_prime : forall a b c,
   Z.gcd a c = 1 -> Z.gcd b c = 1 -> Z.gcd (a*b) c = 1.
  Proof.
- intros.
- rewrite Zgcd_1_rel_prime in *.
- apply rel_prime_sym; apply rel_prime_mult; apply rel_prime_sym; auto.
+   exact Z.coprime_mul_l.
  Qed.
 
  Lemma Zcompare_gt : forall (A:Type)(a a':A)(p q:Z),

BigQ/QMake.v

@@ -230,7 +230,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  generalize (Zgcd_div_pos (ZZ.to_Z p) (NN.to_Z q)). lia.
  replace (NN.to_Z q) with 0%Z in * by (symmetry; assumption).
  rewrite Zdiv_0_l in *; auto with zarith.
- apply Zgcd_div_swap0; lia.
+ apply Z.gcd_div_swap; lia.
  (* Gt *)
  qsimpl.
  assert (H' : Z.gcd (ZZ.to_Z p) (NN.to_Z q) = 0%Z).
@@ -253,10 +253,8 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  qsimpl.
  (* Lt *)
  qsimpl.
- rewrite Zgcd_1_rel_prime.
  destruct (Z_lt_le_dec 0 (NN.to_Z q)).
- apply Zis_gcd_rel_prime; auto with zarith.
- apply Zgcd_is_gcd.
+ apply Z.gcd_div_gcd; auto with zarith.
  replace (NN.to_Z q) with 0%Z in * by lia.
  rewrite Zdiv_0_l in *; lia.
  (* Gt *)
@@ -476,11 +474,9 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  simpl.
  split.
  nzsimpl.
- destruct (Zgcd_is_gcd (ZZ.to_Z n) (NN.to_Z d)).
- rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith.
+ rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto using Z.gcd_divide_l with zarith.
  nzsimpl.
- destruct (Zgcd_is_gcd (ZZ.to_Z n) (NN.to_Z d)).
- rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith.
+ rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto using Z.gcd_divide_r with zarith.
  Qed.
 
  Lemma spec_irred_zero : forall n d,
@@ -519,11 +515,9 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); lia.
 
  nzsimpl.
- rewrite Zgcd_1_rel_prime.
- apply Zis_gcd_rel_prime.
+ apply Z.gcd_div_gcd.
  generalize (NN.spec_pos d); lia.
  generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); lia.
- apply Zgcd_is_gcd; auto.
  Qed.
 
  Definition mul_norm_Qz_Qq z n d :=
@@ -562,7 +556,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  rewrite Zdiv_gcd_zero in GT; auto with zarith.
  nsubst. rewrite Zdiv_0_l in *; discriminate.
  rewrite <- Z.mul_assoc, (Z.mul_comm (ZZ.to_Z n)), Z.mul_assoc.
- rewrite Zgcd_div_swap0; lia.
+ rewrite Z.gcd_div_swap; lia.
  Qed.
 
 #[global]
@@ -602,17 +596,16 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  intros; nzsimpl.
  rewrite Z2Pos.id; auto.
  apply Zgcd_mult_rel_prime.
- rewrite Zgcd_1_rel_prime.
- apply Zis_gcd_rel_prime.
+ apply Z.gcd_div_gcd.
  generalize (NN.spec_pos d); lia.
  generalize (Z.gcd_nonneg (ZZ.to_Z z) (NN.to_Z d)); lia.
- apply Zgcd_is_gcd.
- destruct (Zgcd_is_gcd (ZZ.to_Z z) (NN.to_Z d)) as [ (z0,Hz0) (d0,Hd0) Hzd].
+ destruct (Z.gcd_divide_l (ZZ.to_Z z) (NN.to_Z d)) as [ z0 Hz0 ].
+ destruct (Z.gcd_divide_r (ZZ.to_Z z) (NN.to_Z d)) as [ d0 Hd0 ].
+ pose proof (Z.gcd_greatest (ZZ.to_Z z) (NN.to_Z d)) as Hzd.
  replace (NN.to_Z d / Z.gcd (ZZ.to_Z z) (NN.to_Z d))%Z with d0.
- rewrite Zgcd_1_rel_prime in *.
- apply bezout_rel_prime.
- destruct (rel_prime_bezout _ _ H) as [u v Huv].
- apply Bezout_intro with u (v*(Z.gcd (ZZ.to_Z z) (NN.to_Z d)))%Z.
+ apply Z.coprime_Bezout.
+ destruct (Z.Bezout_coprime _ _ H) as [u [v Huv]].
+ exists u, (v*(Z.gcd (ZZ.to_Z z) (NN.to_Z d)))%Z.
  rewrite <- Huv; rewrite Hd0 at 2; ring.
  rewrite Hd0 at 1.
  symmetry; apply Z_div_mult_full; auto with zarith.
@@ -691,16 +684,14 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  apply Zgcd_mult_rel_prime; rewrite Z.gcd_comm;
   apply Zgcd_mult_rel_prime; rewrite Z.gcd_comm; auto.
 
- rewrite Zgcd_1_rel_prime in *.
- apply bezout_rel_prime.
- destruct (rel_prime_bezout (ZZ.to_Z ny) (NN.to_Z dy)) as [u v Huv]; trivial.
- apply Bezout_intro with (u*g')%Z (v*g)%Z.
+ apply Z.coprime_Bezout.
+ destruct (Z.Bezout_coprime (ZZ.to_Z ny) (NN.to_Z dy)) as [u [v Huv]]; trivial.
+ exists (u*g')%Z, (v*g)%Z.
  rewrite <- Huv, <- Hg1', <- Hg2. ring.
 
- rewrite Zgcd_1_rel_prime in *.
- apply bezout_rel_prime.
- destruct (rel_prime_bezout (ZZ.to_Z nx) (NN.to_Z dx)) as [u v Huv]; trivial.
- apply Bezout_intro with (u*g)%Z (v*g')%Z.
+ apply Z.coprime_Bezout.
+ destruct (Z.Bezout_coprime (ZZ.to_Z nx) (NN.to_Z dx)) as [u [v Huv]]; trivial.
+ exists (u*g)%Z, (v*g')%Z.
  rewrite <- Huv, <- Hg2', <- Hg1. ring.
  Qed.
 
@@ -878,9 +869,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  rewrite Z2Pos.id in *; auto.
  intros.
  rewrite Z.gcd_comm, Z.gcd_abs_l, Z.gcd_comm.
- apply Zis_gcd_gcd; auto with zarith.
- apply Zis_gcd_minus.
- rewrite Z.opp_involutive, <- H1; apply Zgcd_is_gcd.
+ rewrite Z.gcd_opp_l, Z.gcd_comm; assumption.
  rewrite Z.abs_neq; lia.
  Qed.
 
@@ -986,8 +975,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  rewrite Z.pow_0_l' in *; [lia|discriminate].
  rewrite Z2Pos.id in *; auto.
  rewrite NN.spec_pow_pos, ZZ.spec_pow_pos; auto.
- rewrite Zgcd_1_rel_prime in *.
- apply rel_prime_Zpower; auto with zarith.
+ apply Z.coprime_pow_l, Z.coprime_pow_r; auto with zarith.
  Qed.
 
  Definition power (x : t) (z : Z) : t :=

CyclicDouble/DoubleDiv.v

@@ -139,7 +139,7 @@ Section POS_MOD.
     rewrite spec_low.
     rewrite spec_ww_sub.
     rewrite spec_w_0W; rewrite spec_zdigits.
-    rewrite <- Zmod_div_mod. 2-3: zarith.
+    rewrite Z.mod_mod_divide.
     rewrite Zmod_small. zarith.
     split. zarith.
     apply Z.lt_le_trans with (Zpos w_digits). zarith.

CyclicDouble/DoubleDivn1.v

@@ -87,7 +87,9 @@ Section GENDIVN1.
   Lemma spec_split : forall (n : nat) (x : zn2z (word w n)),
        let (h, l) := double_split w_0 n x in
        [!S n | x!] = [!n | h!] * double_wB w_digits n + [!n | l!].
-  Proof (spec_double_split w_0 w_digits w_to_Z spec_0).
+  Proof.
+    exact (spec_double_split w_0 w_digits w_to_Z spec_0).
+  Qed.
 
   Lemma spec_double_divn1_0 : forall n r a,
     [|r|] < [|b2p|] ->

CyclicDouble/DoubleLift.v

@@ -297,7 +297,7 @@ Section DoubleLift.
      rewrite spec_low.
      rewrite spec_ww_sub.
      unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits.
-     rewrite <- Zmod_div_mod; auto with zarith.
+     rewrite Z.mod_mod_divide; auto with zarith.
      rewrite Zmod_small; auto with zarith.
      split; auto with zarith.
      apply Z.le_lt_trans with (Zpos w_digits); auto with zarith.
@@ -392,7 +392,7 @@ Section DoubleLift.
      revert H1.
      rewrite spec_low.
      rewrite spec_ww_sub; w_rewrite; intros H1.
-     rewrite <- Zmod_div_mod; auto with zarith.
+     rewrite Z.mod_mod_divide; auto with zarith.
      rewrite Zmod_small; auto with zarith.
      split; auto with zarith.
      apply Z.le_lt_trans with (Zpos w_digits); auto with zarith.

CyclicDouble/DoubleSqrt.v

@@ -273,7 +273,7 @@ intros x; case x; simpl ww_is_even.
  intros w1 w2; simpl.
  unfold base.
  rewrite Zplus_mod by zarith.
- rewrite (fun x y => (Zdivide_mod (x * y))).
+ rewrite (fun x y => (Z.mod0_divide (x * y))).
  rewrite Z.add_0_l; rewrite Zmod_mod by zarith.
  apply spec_w_is_even; zarith.
  apply Z.divide_mul_r; apply Zpower_divide; zarith.