Skip to content

Handle some deprecation warnings #104

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
proux01 merged 1 commit into from
Jul 18, 2025
Merged

Handle some deprecation warnings #104

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 2 additions & 5 deletions BigNumPrelude.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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),
Expand Down
54 changes: 21 additions & 33 deletions BigQ/QMake.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand All @@ -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 *)
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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 :=
Expand Down Expand Up @@ -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]
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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 :=
Expand Down
2 changes: 1 addition & 1 deletion CyclicDouble/DoubleDiv.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion CyclicDouble/DoubleDivn1.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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|] ->
Expand Down
4 changes: 2 additions & 2 deletions CyclicDouble/DoubleLift.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion CyclicDouble/DoubleSqrt.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down