diff --git a/BigNumPrelude.v b/BigNumPrelude.v index 1708ebd..a81580f 100644 --- a/BigNumPrelude.v +++ b/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), diff --git a/BigQ/QMake.v b/BigQ/QMake.v index d01a936..a6f4787 100644 --- a/BigQ/QMake.v +++ b/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 := diff --git a/CyclicDouble/DoubleDiv.v b/CyclicDouble/DoubleDiv.v index 1c441cd..5fed9dc 100644 --- a/CyclicDouble/DoubleDiv.v +++ b/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. diff --git a/CyclicDouble/DoubleDivn1.v b/CyclicDouble/DoubleDivn1.v index f95a0b2..f2f41a8 100644 --- a/CyclicDouble/DoubleDivn1.v +++ b/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|] -> diff --git a/CyclicDouble/DoubleLift.v b/CyclicDouble/DoubleLift.v index f868c3b..ce85a30 100644 --- a/CyclicDouble/DoubleLift.v +++ b/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. diff --git a/CyclicDouble/DoubleSqrt.v b/CyclicDouble/DoubleSqrt.v index dc26397..1d7724b 100644 --- a/CyclicDouble/DoubleSqrt.v +++ b/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.