diff options
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 1066 |
1 files changed, 534 insertions, 532 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index e722b679..d89ec052 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Znumtheory.v 8990 2006-06-26 13:57:44Z notin $ i*) +(*i $Id: Znumtheory.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import ZArith_base. Require Import ZArithRing. @@ -38,91 +38,91 @@ Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope. Lemma Zdivide_refl : forall a:Z, (a | a). Proof. -intros; apply Zdivide_intro with 1; ring. + intros; apply Zdivide_intro with 1; ring. Qed. Lemma Zone_divide : forall a:Z, (1 | a). Proof. -intros; apply Zdivide_intro with a; ring. + intros; apply Zdivide_intro with a; ring. Qed. Lemma Zdivide_0 : forall a:Z, (a | 0). Proof. -intros; apply Zdivide_intro with 0; ring. + intros; apply Zdivide_intro with 0; ring. Qed. Hint Resolve Zdivide_refl Zone_divide Zdivide_0: zarith. Lemma Zmult_divide_compat_l : forall a b c:Z, (a | b) -> (c * a | c * b). Proof. -simple induction 1; intros; apply Zdivide_intro with q. -rewrite H0; ring. + simple induction 1; intros; apply Zdivide_intro with q. + rewrite H0; ring. Qed. Lemma Zmult_divide_compat_r : forall a b c:Z, (a | b) -> (a * c | b * c). Proof. -intros a b c; rewrite (Zmult_comm a c); rewrite (Zmult_comm b c). -apply Zmult_divide_compat_l; trivial. + intros a b c; rewrite (Zmult_comm a c); rewrite (Zmult_comm b c). + apply Zmult_divide_compat_l; trivial. Qed. Hint Resolve Zmult_divide_compat_l Zmult_divide_compat_r: zarith. Lemma Zdivide_plus_r : forall a b c:Z, (a | b) -> (a | c) -> (a | b + c). Proof. -simple induction 1; intros q Hq; simple induction 1; intros q' Hq'. -apply Zdivide_intro with (q + q'). -rewrite Hq; rewrite Hq'; ring. + simple induction 1; intros q Hq; simple induction 1; intros q' Hq'. + apply Zdivide_intro with (q + q'). + rewrite Hq; rewrite Hq'; ring. Qed. Lemma Zdivide_opp_r : forall a b:Z, (a | b) -> (a | - b). Proof. -simple induction 1; intros; apply Zdivide_intro with (- q). -rewrite H0; ring. + simple induction 1; intros; apply Zdivide_intro with (- q). + rewrite H0; ring. Qed. Lemma Zdivide_opp_r_rev : forall a b:Z, (a | - b) -> (a | b). Proof. -intros; replace b with (- - b). apply Zdivide_opp_r; trivial. ring. + intros; replace b with (- - b). apply Zdivide_opp_r; trivial. ring. Qed. Lemma Zdivide_opp_l : forall a b:Z, (a | b) -> (- a | b). Proof. -simple induction 1; intros; apply Zdivide_intro with (- q). -rewrite H0; ring. + simple induction 1; intros; apply Zdivide_intro with (- q). + rewrite H0; ring. Qed. Lemma Zdivide_opp_l_rev : forall a b:Z, (- a | b) -> (a | b). Proof. -intros; replace a with (- - a). apply Zdivide_opp_l; trivial. ring. + intros; replace a with (- - a). apply Zdivide_opp_l; trivial. ring. Qed. Lemma Zdivide_minus_l : forall a b c:Z, (a | b) -> (a | c) -> (a | b - c). Proof. -simple induction 1; intros q Hq; simple induction 1; intros q' Hq'. -apply Zdivide_intro with (q - q'). -rewrite Hq; rewrite Hq'; ring. + simple induction 1; intros q Hq; simple induction 1; intros q' Hq'. + apply Zdivide_intro with (q - q'). + rewrite Hq; rewrite Hq'; ring. Qed. Lemma Zdivide_mult_l : forall a b c:Z, (a | b) -> (a | b * c). Proof. -simple induction 1; intros q Hq; apply Zdivide_intro with (q * c). -rewrite Hq; ring. + simple induction 1; intros q Hq; apply Zdivide_intro with (q * c). + rewrite Hq; ring. Qed. Lemma Zdivide_mult_r : forall a b c:Z, (a | c) -> (a | b * c). Proof. -simple induction 1; intros q Hq; apply Zdivide_intro with (q * b). -rewrite Hq; ring. + simple induction 1; intros q Hq; apply Zdivide_intro with (q * b). + rewrite Hq; ring. Qed. Lemma Zdivide_factor_r : forall a b:Z, (a | a * b). Proof. -intros; apply Zdivide_intro with b; ring. + intros; apply Zdivide_intro with b; ring. Qed. Lemma Zdivide_factor_l : forall a b:Z, (a | b * a). Proof. -intros; apply Zdivide_intro with b; ring. + intros; apply Zdivide_intro with b; ring. Qed. Hint Resolve Zdivide_plus_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l @@ -133,7 +133,7 @@ Hint Resolve Zdivide_plus_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l Lemma Zmult_one : forall x y:Z, x >= 0 -> x * y = 1 -> x = 1. Proof. -intros x y H H0; destruct (Zmult_1_inversion_l _ _ H0) as [Hpos| Hneg]. + intros x y H H0; destruct (Zmult_1_inversion_l _ _ H0) as [Hpos| Hneg]. assumption. rewrite Hneg in H; simpl in H. contradiction (Zle_not_lt 0 (-1)). @@ -145,11 +145,11 @@ Qed. Lemma Zdivide_1 : forall x:Z, (x | 1) -> x = 1 \/ x = -1. Proof. -simple induction 1; intros. -elim (Z_lt_ge_dec 0 x); [ left | right ]. -apply Zmult_one with q; auto with zarith; rewrite H0; ring. -assert (- x = 1); auto with zarith. -apply Zmult_one with (- q); auto with zarith; rewrite H0; ring. + simple induction 1; intros. + elim (Z_lt_ge_dec 0 x); [ left | right ]. + apply Zmult_one with q; auto with zarith; rewrite H0; ring. + assert (- x = 1); auto with zarith. + apply Zmult_one with (- q); auto with zarith; rewrite H0; ring. Qed. (** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *) @@ -164,7 +164,7 @@ left; rewrite H0; rewrite e; ring. assert (Hqq0 : q0 * q = 1). apply Zmult_reg_l with a. assumption. -ring. +ring_simplify. pattern a at 2 in |- *; rewrite H2; ring. assert (q | 1). rewrite <- Hqq0; auto with zarith. @@ -177,21 +177,21 @@ Qed. Lemma Zdivide_bounds : forall a b:Z, (a | b) -> b <> 0 -> Zabs a <= Zabs b. Proof. -simple induction 1; intros. -assert (Zabs b = Zabs q * Zabs a). - subst; apply Zabs_Zmult. -rewrite H2. -assert (H3 := Zabs_pos q). -assert (H4 := Zabs_pos a). -assert (Zabs q * Zabs a >= 1 * Zabs a); auto with zarith. -apply Zmult_ge_compat; auto with zarith. -elim (Z_lt_ge_dec (Zabs q) 1); [ intros | auto with zarith ]. -assert (Zabs q = 0). - omega. -assert (q = 0). - rewrite <- (Zabs_Zsgn q). -rewrite H5; auto with zarith. -subst q; omega. + simple induction 1; intros. + assert (Zabs b = Zabs q * Zabs a). + subst; apply Zabs_Zmult. + rewrite H2. + assert (H3 := Zabs_pos q). + assert (H4 := Zabs_pos a). + assert (Zabs q * Zabs a >= 1 * Zabs a); auto with zarith. + apply Zmult_ge_compat; auto with zarith. + elim (Z_lt_ge_dec (Zabs q) 1); [ intros | auto with zarith ]. + assert (Zabs q = 0). + omega. + assert (q = 0). + rewrite <- (Zabs_Zsgn q). + rewrite H5; auto with zarith. + subst q; omega. Qed. (** * Greatest common divisor (gcd). *) @@ -201,48 +201,48 @@ Qed. (We show later that the [gcd] is actually unique if we discard its sign.) *) Inductive Zis_gcd (a b d:Z) : Prop := - Zis_gcd_intro : - (d | a) -> - (d | b) -> (forall x:Z, (x | a) -> (x | b) -> (x | d)) -> Zis_gcd a b d. + Zis_gcd_intro : + (d | a) -> + (d | b) -> (forall x:Z, (x | a) -> (x | b) -> (x | d)) -> Zis_gcd a b d. (** Trivial properties of [gcd] *) Lemma Zis_gcd_sym : forall a b d:Z, Zis_gcd a b d -> Zis_gcd b a d. Proof. -simple induction 1; constructor; intuition. + simple induction 1; constructor; intuition. Qed. Lemma Zis_gcd_0 : forall a:Z, Zis_gcd a 0 a. Proof. -constructor; auto with zarith. + constructor; auto with zarith. Qed. Lemma Zis_gcd_1 : forall a, Zis_gcd a 1 1. Proof. -constructor; auto with zarith. + constructor; auto with zarith. Qed. Lemma Zis_gcd_refl : forall a, Zis_gcd a a a. Proof. -constructor; auto with zarith. + constructor; auto with zarith. Qed. Lemma Zis_gcd_minus : forall a b d:Z, Zis_gcd a (- b) d -> Zis_gcd b a d. Proof. -simple induction 1; constructor; intuition. + simple induction 1; constructor; intuition. Qed. Lemma Zis_gcd_opp : forall a b d:Z, Zis_gcd a b d -> Zis_gcd b a (- d). Proof. -simple induction 1; constructor; intuition. + simple induction 1; constructor; intuition. Qed. Lemma Zis_gcd_0_abs : forall a:Z, Zis_gcd 0 a (Zabs a). Proof. -intros a. -apply Zabs_ind. -intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. -intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. + intros a. + apply Zabs_ind. + intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. + intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. Qed. Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith. @@ -253,18 +253,18 @@ Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith. the following property. *) Lemma Zis_gcd_for_euclid : - forall a b d q:Z, Zis_gcd b (a - q * b) d -> Zis_gcd a b d. + forall a b d q:Z, Zis_gcd b (a - q * b) d -> Zis_gcd a b d. Proof. -simple induction 1; constructor; intuition. -replace a with (a - q * b + q * b). auto with zarith. ring. + simple induction 1; constructor; intuition. + replace a with (a - q * b + q * b). auto with zarith. ring. Qed. Lemma Zis_gcd_for_euclid2 : - forall b d q r:Z, Zis_gcd r b d -> Zis_gcd b (b * q + r) d. + forall b d q r:Z, Zis_gcd r b d -> Zis_gcd b (b * q + r) d. Proof. -simple induction 1; constructor; intuition. -apply H2; auto. -replace r with (b * q + r - b * q). auto with zarith. ring. + simple induction 1; constructor; intuition. + apply H2; auto. + replace r with (b * q + r - b * q). auto with zarith. ring. Qed. (** We implement the extended version of Euclid's algorithm, @@ -274,117 +274,117 @@ Qed. Section extended_euclid_algorithm. -Variables a b : Z. + Variables a b : Z. -(** The specification of Euclid's algorithm is the existence of - [u], [v] and [d] such that [ua+vb=d] and [(gcd a b d)]. *) + (** The specification of Euclid's algorithm is the existence of + [u], [v] and [d] such that [ua+vb=d] and [(gcd a b d)]. *) -Inductive Euclid : Set := + Inductive Euclid : Set := Euclid_intro : - forall u v d:Z, u * a + v * b = d -> Zis_gcd a b d -> Euclid. - -(** The recursive part of Euclid's algorithm uses well-founded - recursion of non-negative integers. It maintains 6 integers - [u1,u2,u3,v1,v2,v3] such that the following invariant holds: - [u1*a+u2*b=u3] and [v1*a+v2*b=v3] and [gcd(u2,v3)=gcd(a,b)]. - *) - -Lemma euclid_rec : - forall v3:Z, - 0 <= v3 -> - forall u1 u2 u3 v1 v2:Z, - u1 * a + u2 * b = u3 -> - v1 * a + v2 * b = v3 -> - (forall d:Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) -> Euclid. -Proof. -intros v3 Hv3; generalize Hv3; pattern v3 in |- *. -apply Zlt_0_rec. -clear v3 Hv3; intros. -elim (Z_zerop x); intro. -apply Euclid_intro with (u := u1) (v := u2) (d := u3). -assumption. -apply H3. -rewrite a0; auto with zarith. -set (q := u3 / x) in *. -assert (Hq : 0 <= u3 - q * x < x). -replace (u3 - q * x) with (u3 mod x). -apply Z_mod_lt; omega. -assert (xpos : x > 0). omega. -generalize (Z_div_mod_eq u3 x xpos). -unfold q in |- *. -intro eq; pattern u3 at 2 in |- *; rewrite eq; ring. -apply (H (u3 - q * x) Hq (proj1 Hq) v1 v2 x (u1 - q * v1) (u2 - q * v2)). -tauto. -replace ((u1 - q * v1) * a + (u2 - q * v2) * b) with - (u1 * a + u2 * b - q * (v1 * a + v2 * b)). -rewrite H1; rewrite H2; trivial. -ring. -intros; apply H3. -apply Zis_gcd_for_euclid with q; assumption. -assumption. -Qed. - -(** We get Euclid's algorithm by applying [euclid_rec] on - [1,0,a,0,1,b] when [b>=0] and [1,0,a,0,-1,-b] when [b<0]. *) - -Lemma euclid : Euclid. -Proof. -case (Z_le_gt_dec 0 b); intro. -intros; - apply euclid_rec with - (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := 1) (v3 := b); - auto with zarith; ring. -intros; - apply euclid_rec with - (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := -1) (v3 := - b); - auto with zarith; try ring. -Qed. + forall u v d:Z, u * a + v * b = d -> Zis_gcd a b d -> Euclid. + + (** The recursive part of Euclid's algorithm uses well-founded + recursion of non-negative integers. It maintains 6 integers + [u1,u2,u3,v1,v2,v3] such that the following invariant holds: + [u1*a+u2*b=u3] and [v1*a+v2*b=v3] and [gcd(u2,v3)=gcd(a,b)]. + *) + + Lemma euclid_rec : + forall v3:Z, + 0 <= v3 -> + forall u1 u2 u3 v1 v2:Z, + u1 * a + u2 * b = u3 -> + v1 * a + v2 * b = v3 -> + (forall d:Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) -> Euclid. + Proof. + intros v3 Hv3; generalize Hv3; pattern v3 in |- *. + apply Zlt_0_rec. + clear v3 Hv3; intros. + elim (Z_zerop x); intro. + apply Euclid_intro with (u := u1) (v := u2) (d := u3). + assumption. + apply H3. + rewrite a0; auto with zarith. + set (q := u3 / x) in *. + assert (Hq : 0 <= u3 - q * x < x). + replace (u3 - q * x) with (u3 mod x). + apply Z_mod_lt; omega. + assert (xpos : x > 0). omega. + generalize (Z_div_mod_eq u3 x xpos). + unfold q in |- *. + intro eq; pattern u3 at 2 in |- *; rewrite eq; ring. + apply (H (u3 - q * x) Hq (proj1 Hq) v1 v2 x (u1 - q * v1) (u2 - q * v2)). + tauto. + replace ((u1 - q * v1) * a + (u2 - q * v2) * b) with + (u1 * a + u2 * b - q * (v1 * a + v2 * b)). + rewrite H1; rewrite H2; trivial. + ring. + intros; apply H3. + apply Zis_gcd_for_euclid with q; assumption. + assumption. + Qed. + + (** We get Euclid's algorithm by applying [euclid_rec] on + [1,0,a,0,1,b] when [b>=0] and [1,0,a,0,-1,-b] when [b<0]. *) + + Lemma euclid : Euclid. + Proof. + case (Z_le_gt_dec 0 b); intro. + intros; + apply euclid_rec with + (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := 1) (v3 := b); + auto with zarith; ring. + intros; + apply euclid_rec with + (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := -1) (v3 := - b); + auto with zarith; try ring. + Qed. End extended_euclid_algorithm. Theorem Zis_gcd_uniqueness_apart_sign : - forall a b d d':Z, Zis_gcd a b d -> Zis_gcd a b d' -> d = d' \/ d = - d'. + forall a b d d':Z, Zis_gcd a b d -> Zis_gcd a b d' -> d = d' \/ d = - d'. Proof. -simple induction 1. -intros H1 H2 H3; simple induction 1; intros. -generalize (H3 d' H4 H5); intro Hd'd. -generalize (H6 d H1 H2); intro Hdd'. -exact (Zdivide_antisym d d' Hdd' Hd'd). + simple induction 1. + intros H1 H2 H3; simple induction 1; intros. + generalize (H3 d' H4 H5); intro Hd'd. + generalize (H6 d H1 H2); intro Hdd'. + exact (Zdivide_antisym d d' Hdd' Hd'd). Qed. (** * Bezout's coefficients *) Inductive Bezout (a b d:Z) : Prop := - Bezout_intro : forall u v:Z, u * a + v * b = d -> Bezout a b d. + Bezout_intro : forall u v:Z, u * a + v * b = d -> Bezout a b d. (** Existence of Bezout's coefficients for the [gcd] of [a] and [b] *) Lemma Zis_gcd_bezout : forall a b d:Z, Zis_gcd a b d -> Bezout a b d. Proof. -intros a b d Hgcd. -elim (euclid a b); intros u v d0 e g. -generalize (Zis_gcd_uniqueness_apart_sign a b d d0 Hgcd g). -intro H; elim H; clear H; intros. -apply Bezout_intro with u v. -rewrite H; assumption. -apply Bezout_intro with (- u) (- v). -rewrite H; rewrite <- e; ring. + intros a b d Hgcd. + elim (euclid a b); intros u v d0 e g. + generalize (Zis_gcd_uniqueness_apart_sign a b d d0 Hgcd g). + intro H; elim H; clear H; intros. + apply Bezout_intro with u v. + rewrite H; assumption. + apply Bezout_intro with (- u) (- v). + rewrite H; rewrite <- e; ring. Qed. (** gcd of [ca] and [cb] is [c gcd(a,b)]. *) Lemma Zis_gcd_mult : - forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d). -Proof. -intros a b c d; simple induction 1; constructor; intuition. -elim (Zis_gcd_bezout a b d H); intros. -elim H3; intros. -elim H4; intros. -apply Zdivide_intro with (u * q + v * q0). -rewrite <- H5. -replace (c * (u * a + v * b)) with (u * (c * a) + v * (c * b)). -rewrite H6; rewrite H7; ring. -ring. + forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d). +Proof. + intros a b c d; simple induction 1; constructor; intuition. + elim (Zis_gcd_bezout a b d H); intros. + elim H3; intros. + elim H4; intros. + apply Zdivide_intro with (u * q + v * q0). + rewrite <- H5. + replace (c * (u * a + v * b)) with (u * (c * a) + v * (c * b)). + rewrite H6; rewrite H7; ring. + ring. Qed. @@ -397,13 +397,13 @@ Definition rel_prime (a b:Z) : Prop := Zis_gcd a b 1. Lemma rel_prime_bezout : forall a b:Z, rel_prime a b -> Bezout a b 1. Proof. -intros a b; exact (Zis_gcd_bezout a b 1). + intros a b; exact (Zis_gcd_bezout a b 1). Qed. Lemma bezout_rel_prime : forall a b:Z, Bezout a b 1 -> rel_prime a b. Proof. -simple induction 1; constructor; auto with zarith. -intros. rewrite <- H0; auto with zarith. + simple induction 1; constructor; auto with zarith. + intros. rewrite <- H0; auto with zarith. Qed. (** Gauss's theorem: if [a] divides [bc] and if [a] and [b] are @@ -411,134 +411,134 @@ Qed. Theorem Gauss : forall a b c:Z, (a | b * c) -> rel_prime a b -> (a | c). Proof. -intros. elim (rel_prime_bezout a b H0); intros. -replace c with (c * 1); [ idtac | ring ]. -rewrite <- H1. -replace (c * (u * a + v * b)) with (c * u * a + v * (b * c)); - [ eauto with zarith | ring ]. + intros. elim (rel_prime_bezout a b H0); intros. + replace c with (c * 1); [ idtac | ring ]. + rewrite <- H1. + replace (c * (u * a + v * b)) with (c * u * a + v * (b * c)); + [ eauto with zarith | ring ]. Qed. (** If [a] is relatively prime to [b] and [c], then it is to [bc] *) Lemma rel_prime_mult : - forall a b c:Z, rel_prime a b -> rel_prime a c -> rel_prime a (b * c). + forall a b c:Z, rel_prime a b -> rel_prime a c -> rel_prime a (b * c). Proof. -intros a b c Hb Hc. -elim (rel_prime_bezout a b Hb); intros. -elim (rel_prime_bezout a c Hc); intros. -apply bezout_rel_prime. -apply Bezout_intro with - (u := u * u0 * a + v0 * c * u + u0 * v * b) (v := v * v0). -rewrite <- H. -replace (u * a + v * b) with ((u * a + v * b) * 1); [ idtac | ring ]. -rewrite <- H0. -ring. + intros a b c Hb Hc. + elim (rel_prime_bezout a b Hb); intros. + elim (rel_prime_bezout a c Hc); intros. + apply bezout_rel_prime. + apply Bezout_intro with + (u := u * u0 * a + v0 * c * u + u0 * v * b) (v := v * v0). + rewrite <- H. + replace (u * a + v * b) with ((u * a + v * b) * 1); [ idtac | ring ]. + rewrite <- H0. + ring. Qed. Lemma rel_prime_cross_prod : - forall a b c d:Z, - rel_prime a b -> - rel_prime c d -> b > 0 -> d > 0 -> a * d = b * c -> a = c /\ b = d. -Proof. -intros a b c d; intros. -elim (Zdivide_antisym b d). -split; auto with zarith. -rewrite H4 in H3. -rewrite Zmult_comm in H3. -apply Zmult_reg_l with d; auto with zarith. -intros; omega. -apply Gauss with a. -rewrite H3. -auto with zarith. -red in |- *; auto with zarith. -apply Gauss with c. -rewrite Zmult_comm. -rewrite <- H3. -auto with zarith. -red in |- *; auto with zarith. + forall a b c d:Z, + rel_prime a b -> + rel_prime c d -> b > 0 -> d > 0 -> a * d = b * c -> a = c /\ b = d. +Proof. + intros a b c d; intros. + elim (Zdivide_antisym b d). + split; auto with zarith. + rewrite H4 in H3. + rewrite Zmult_comm in H3. + apply Zmult_reg_l with d; auto with zarith. + intros; omega. + apply Gauss with a. + rewrite H3. + auto with zarith. + red in |- *; auto with zarith. + apply Gauss with c. + rewrite Zmult_comm. + rewrite <- H3. + auto with zarith. + red in |- *; auto with zarith. Qed. (** After factorization by a gcd, the original numbers are relatively prime. *) Lemma Zis_gcd_rel_prime : - forall a b g:Z, - b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g). -intros a b g; intros. -assert (g <> 0). - intro. - elim H1; intros. - elim H4; intros. - rewrite H2 in H6; subst b; omega. -unfold rel_prime in |- *. -destruct H1. -destruct H1 as (a',H1). -destruct H3 as (b',H3). -replace (a/g) with a'; - [|rewrite H1; rewrite Z_div_mult; auto with zarith]. -replace (b/g) with b'; - [|rewrite H3; rewrite Z_div_mult; auto with zarith]. -constructor. -exists a'; auto with zarith. -exists b'; auto with zarith. -intros x (xa,H5) (xb,H6). -destruct (H4 (x*g)). -exists xa; rewrite Zmult_assoc; rewrite <- H5; auto. -exists xb; rewrite Zmult_assoc; rewrite <- H6; auto. -replace g with (1*g) in H7; auto with zarith. -do 2 rewrite Zmult_assoc in H7. -generalize (Zmult_reg_r _ _ _ H2 H7); clear H7; intros. -rewrite Zmult_1_r in H7. -exists q; auto with zarith. + forall a b g:Z, + b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g). + intros a b g; intros. + assert (g <> 0). + intro. + elim H1; intros. + elim H4; intros. + rewrite H2 in H6; subst b; omega. + unfold rel_prime in |- *. + destruct H1. + destruct H1 as (a',H1). + destruct H3 as (b',H3). + replace (a/g) with a'; + [|rewrite H1; rewrite Z_div_mult; auto with zarith]. + replace (b/g) with b'; + [|rewrite H3; rewrite Z_div_mult; auto with zarith]. + constructor. + exists a'; auto with zarith. + exists b'; auto with zarith. + intros x (xa,H5) (xb,H6). + destruct (H4 (x*g)). + exists xa; rewrite Zmult_assoc; rewrite <- H5; auto. + exists xb; rewrite Zmult_assoc; rewrite <- H6; auto. + replace g with (1*g) in H7; auto with zarith. + do 2 rewrite Zmult_assoc in H7. + generalize (Zmult_reg_r _ _ _ H2 H7); clear H7; intros. + rewrite Zmult_1_r in H7. + exists q; auto with zarith. Qed. (** * Primality *) Inductive prime (p:Z) : Prop := - prime_intro : - 1 < p -> (forall n:Z, 1 <= n < p -> rel_prime n p) -> prime p. + prime_intro : + 1 < p -> (forall n:Z, 1 <= n < p -> rel_prime n p) -> prime p. (** The sole divisors of a prime number [p] are [-1], [1], [p] and [-p]. *) Lemma prime_divisors : - forall p:Z, - prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p. -Proof. -simple induction 1; intros. -assert - (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p). -assert (Zabs a <= Zabs p). apply Zdivide_bounds; [ assumption | omega ]. -generalize H3. -pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs p) in |- *; - apply Zabs_ind; intros; omega. -intuition idtac. -(* -p < a < -1 *) -absurd (rel_prime (- a) p); intuition. -inversion H3. -assert (- a | - a); auto with zarith. -assert (- a | p); auto with zarith. -generalize (H8 (- a) H9 H10); intuition idtac. -generalize (Zdivide_1 (- a) H11); intuition. -(* a = 0 *) -inversion H2. subst a; omega. -(* 1 < a < p *) -absurd (rel_prime a p); intuition. -inversion H3. -assert (a | a); auto with zarith. -assert (a | p); auto with zarith. -generalize (H8 a H9 H10); intuition idtac. -generalize (Zdivide_1 a H11); intuition. + forall p:Z, + prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p. +Proof. + simple induction 1; intros. + assert + (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p). + assert (Zabs a <= Zabs p). apply Zdivide_bounds; [ assumption | omega ]. + generalize H3. + pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs p) in |- *; + apply Zabs_ind; intros; omega. + intuition idtac. + (* -p < a < -1 *) + absurd (rel_prime (- a) p); intuition. + inversion H3. + assert (- a | - a); auto with zarith. + assert (- a | p); auto with zarith. + generalize (H8 (- a) H9 H10); intuition idtac. + generalize (Zdivide_1 (- a) H11); intuition. + (* a = 0 *) + inversion H2. subst a; omega. + (* 1 < a < p *) + absurd (rel_prime a p); intuition. + inversion H3. + assert (a | a); auto with zarith. + assert (a | p); auto with zarith. + generalize (H8 a H9 H10); intuition idtac. + generalize (Zdivide_1 a H11); intuition. Qed. (** A prime number is relatively prime with any number it does not divide *) Lemma prime_rel_prime : - forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a. + forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a. Proof. -simple induction 1; intros. -constructor; intuition. -elim (prime_divisors p H x H3); intuition; subst; auto with zarith. -absurd (p | a); auto with zarith. -absurd (p | a); intuition. + simple induction 1; intros. + constructor; intuition. + elim (prime_divisors p H x H3); intuition; subst; auto with zarith. + absurd (p | a); auto with zarith. + absurd (p | a); intuition. Qed. Hint Resolve prime_rel_prime: zarith. @@ -546,46 +546,48 @@ Hint Resolve prime_rel_prime: zarith. (** [Zdivide] can be expressed using [Zmod]. *) Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a). -intros a b H H0. -apply Zdivide_intro with (a / b). -pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H). -rewrite H0; ring. +Proof. + intros a b H H0. + apply Zdivide_intro with (a / b). + pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H). + rewrite H0; ring. Qed. Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0. -intros a b; simple destruct 2; intros; subst. -change (q * b) with (0 + q * b) in |- *. -rewrite Z_mod_plus; auto. +Proof. + intros a b; simple destruct 2; intros; subst. + change (q * b) with (0 + q * b) in |- *. + rewrite Z_mod_plus; auto. Qed. (** [Zdivide] is hence decidable *) Lemma Zdivide_dec : forall a b:Z, {(a | b)} + {~ (a | b)}. Proof. -intros a b; elim (Ztrichotomy_inf a 0). -(* a<0 *) -intros H; elim H; intros. -case (Z_eq_dec (b mod - a) 0). -left; apply Zdivide_opp_l_rev; apply Zmod_divide; auto with zarith. -intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith. -(* a=0 *) -case (Z_eq_dec b 0); intro. -left; subst; auto with zarith. -right; subst; intro H0; inversion H0; omega. -(* a>0 *) -intro H; case (Z_eq_dec (b mod a) 0). -left; apply Zmod_divide; auto with zarith. -intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith. + intros a b; elim (Ztrichotomy_inf a 0). + (* a<0 *) + intros H; elim H; intros. + case (Z_eq_dec (b mod - a) 0). + left; apply Zdivide_opp_l_rev; apply Zmod_divide; auto with zarith. + intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith. + (* a=0 *) + case (Z_eq_dec b 0); intro. + left; subst; auto with zarith. + right; subst; intro H0; inversion H0; omega. + (* a>0 *) + intro H; case (Z_eq_dec (b mod a) 0). + left; apply Zmod_divide; auto with zarith. + intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith. Qed. (** If a prime [p] divides [ab] then it divides either [a] or [b] *) Lemma prime_mult : - forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b). + forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b). Proof. -intro p; simple induction 1; intros. -case (Zdivide_dec p a); intuition. -right; apply Gauss with a; auto with zarith. + intro p; simple induction 1; intros. + case (Zdivide_dec p a); intuition. + right; apply Gauss with a; auto with zarith. Qed. @@ -606,53 +608,53 @@ Qed. Open Scope positive_scope. Fixpoint Pgcdn (n: nat) (a b : positive) { struct n } : positive := - match n with - | O => 1 - | S n => - match a,b with - | xH, _ => 1 - | _, xH => 1 - | xO a, xO b => xO (Pgcdn n a b) - | a, xO b => Pgcdn n a b - | xO a, b => Pgcdn n a b - | xI a', xI b' => match Pcompare a' b' Eq with - | Eq => a - | Lt => Pgcdn n (b'-a') a - | Gt => Pgcdn n (a'-b') b - end - end + match n with + | O => 1 + | S n => + match a,b with + | xH, _ => 1 + | _, xH => 1 + | xO a, xO b => xO (Pgcdn n a b) + | a, xO b => Pgcdn n a b + | xO a, b => Pgcdn n a b + | xI a', xI b' => match Pcompare a' b' Eq with + | Eq => a + | Lt => Pgcdn n (b'-a') a + | Gt => Pgcdn n (a'-b') b + end + end end. Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := - match n with - | O => (1,(a,b)) - | S n => - match a,b with - | xH, b => (1,(1,b)) - | a, xH => (1,(a,1)) - | xO a, xO b => - let (g,p) := Pggcdn n a b in - (xO g,p) - | a, xO b => - let (g,p) := Pggcdn n a b in - let (aa,bb) := p in - (g,(aa, xO bb)) - | xO a, b => - let (g,p) := Pggcdn n a b in - let (aa,bb) := p in - (g,(xO aa, bb)) - | xI a', xI b' => match Pcompare a' b' Eq with - | Eq => (a,(1,1)) - | Lt => - let (g,p) := Pggcdn n (b'-a') a in - let (ba,aa) := p in - (g,(aa, aa + xO ba)) - | Gt => - let (g,p) := Pggcdn n (a'-b') b in - let (ab,bb) := p in - (g,(bb+xO ab, bb)) - end - end + match n with + | O => (1,(a,b)) + | S n => + match a,b with + | xH, b => (1,(1,b)) + | a, xH => (1,(a,1)) + | xO a, xO b => + let (g,p) := Pggcdn n a b in + (xO g,p) + | a, xO b => + let (g,p) := Pggcdn n a b in + let (aa,bb) := p in + (g,(aa, xO bb)) + | xO a, b => + let (g,p) := Pggcdn n a b in + let (aa,bb) := p in + (g,(xO aa, bb)) + | xI a', xI b' => match Pcompare a' b' Eq with + | Eq => (a,(1,1)) + | Lt => + let (g,p) := Pggcdn n (b'-a') a in + let (ba,aa) := p in + (g,(aa, aa + xO ba)) + | Gt => + let (g,p) := Pggcdn n (a'-b') b in + let (ab,bb) := p in + (g,(bb+xO ab, bb)) + end + end end. Definition Pgcd (a b: positive) := Pgcdn (Psize a + Psize b)%nat a b. @@ -661,269 +663,269 @@ Definition Pggcd (a b: positive) := Pggcdn (Psize a + Psize b)%nat a b. Open Scope Z_scope. Definition Zgcd (a b : Z) : Z := match a,b with - | Z0, _ => Zabs b - | _, Z0 => Zabs a - | Zpos a, Zpos b => Zpos (Pgcd a b) - | Zpos a, Zneg b => Zpos (Pgcd a b) - | Zneg a, Zpos b => Zpos (Pgcd a b) - | Zneg a, Zneg b => Zpos (Pgcd a b) -end. + | Z0, _ => Zabs b + | _, Z0 => Zabs a + | Zpos a, Zpos b => Zpos (Pgcd a b) + | Zpos a, Zneg b => Zpos (Pgcd a b) + | Zneg a, Zpos b => Zpos (Pgcd a b) + | Zneg a, Zneg b => Zpos (Pgcd a b) + end. Definition Zggcd (a b : Z) : Z*(Z*Z) := match a,b with - | Z0, _ => (Zabs b,(0, Zsgn b)) - | _, Z0 => (Zabs a,(Zsgn a, 0)) - | Zpos a, Zpos b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in - (Zpos g, (Zpos aa, Zpos bb)) - | Zpos a, Zneg b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in - (Zpos g, (Zpos aa, Zneg bb)) - | Zneg a, Zpos b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in - (Zpos g, (Zneg aa, Zpos bb)) - | Zneg a, Zneg b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in - (Zpos g, (Zneg aa, Zneg bb)) -end. + | Z0, _ => (Zabs b,(0, Zsgn b)) + | _, Z0 => (Zabs a,(Zsgn a, 0)) + | Zpos a, Zpos b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zpos aa, Zpos bb)) + | Zpos a, Zneg b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zpos aa, Zneg bb)) + | Zneg a, Zpos b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zneg aa, Zpos bb)) + | Zneg a, Zneg b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zneg aa, Zneg bb)) + end. Lemma Zgcd_is_pos : forall a b, 0 <= Zgcd a b. Proof. -unfold Zgcd; destruct a; destruct b; auto with zarith. + unfold Zgcd; destruct a; destruct b; auto with zarith. Qed. Lemma Psize_monotone : forall p q, Pcompare p q Eq = Lt -> (Psize p <= Psize q)%nat. Proof. -induction p; destruct q; simpl; auto with arith; intros; try discriminate. -intros; generalize (Pcompare_Gt_Lt _ _ H); auto with arith. -intros; destruct (Pcompare_Lt_Lt _ _ H); auto with arith; subst; auto. + induction p; destruct q; simpl; auto with arith; intros; try discriminate. + intros; generalize (Pcompare_Gt_Lt _ _ H); auto with arith. + intros; destruct (Pcompare_Lt_Lt _ _ H); auto with arith; subst; auto. Qed. Lemma Pminus_Zminus : forall a b, Pcompare a b Eq = Lt -> - Zpos (b-a) = Zpos b - Zpos a. + Zpos (b-a) = Zpos b - Zpos a. Proof. -intros. -repeat rewrite Zpos_eq_Z_of_nat_o_nat_of_P. -rewrite nat_of_P_minus_morphism. -apply inj_minus1. -apply lt_le_weak. -apply nat_of_P_lt_Lt_compare_morphism; auto. -rewrite ZC4; rewrite H; auto. + intros. + repeat rewrite Zpos_eq_Z_of_nat_o_nat_of_P. + rewrite nat_of_P_minus_morphism. + apply inj_minus1. + apply lt_le_weak. + apply nat_of_P_lt_Lt_compare_morphism; auto. + rewrite ZC4; rewrite H; auto. Qed. Lemma Zis_gcd_even_odd : forall a b g, Zis_gcd (Zpos a) (Zpos (xI b)) g -> - Zis_gcd (Zpos (xO a)) (Zpos (xI b)) g. -Proof. -intros. -destruct H. -constructor; auto. -destruct H as (e,H2); exists (2*e); auto with zarith. -rewrite Zpos_xO; rewrite H2; ring. -intros. -apply H1; auto. -rewrite Zpos_xO in H2. -rewrite Zpos_xI in H3. -apply Gauss with 2; auto. -apply bezout_rel_prime. -destruct H3 as (bb, H3). -apply Bezout_intro with bb (-Zpos b). -omega. + Zis_gcd (Zpos (xO a)) (Zpos (xI b)) g. +Proof. + intros. + destruct H. + constructor; auto. + destruct H as (e,H2); exists (2*e); auto with zarith. + rewrite Zpos_xO; rewrite H2; ring. + intros. + apply H1; auto. + rewrite Zpos_xO in H2. + rewrite Zpos_xI in H3. + apply Gauss with 2; auto. + apply bezout_rel_prime. + destruct H3 as (bb, H3). + apply Bezout_intro with bb (-Zpos b). + omega. Qed. Lemma Pgcdn_correct : forall n a b, (Psize a + Psize b<=n)%nat -> - Zis_gcd (Zpos a) (Zpos b) (Zpos (Pgcdn n a b)). -Proof. -intro n; pattern n; apply lt_wf_ind; clear n; intros. -destruct n. -simpl. -destruct a; simpl in *; try inversion H0. -destruct a. -destruct b; simpl. -case_eq (Pcompare a b Eq); intros. -(* a = xI, b = xI, compare = Eq *) -rewrite (Pcompare_Eq_eq _ _ H1); apply Zis_gcd_refl. -(* a = xI, b = xI, compare = Lt *) -apply Zis_gcd_sym. -apply Zis_gcd_for_euclid with 1. -apply Zis_gcd_sym. -replace (Zpos (xI b) - 1 * Zpos (xI a)) with (Zpos(xO (b - a))). -apply Zis_gcd_even_odd. -apply H; auto. -simpl in *. -assert (Psize (b-a) <= Psize b)%nat. - apply Psize_monotone. - change (Zpos (b-a) < Zpos b). - rewrite (Pminus_Zminus _ _ H1). - assert (0 < Zpos a) by (compute; auto). - omega. -omega. -rewrite Zpos_xO; do 2 rewrite Zpos_xI. -rewrite Pminus_Zminus; auto. -omega. -(* a = xI, b = xI, compare = Gt *) -apply Zis_gcd_for_euclid with 1. -replace (Zpos (xI a) - 1 * Zpos (xI b)) with (Zpos(xO (a - b))). -apply Zis_gcd_sym. -apply Zis_gcd_even_odd. -apply H; auto. -simpl in *. -assert (Psize (a-b) <= Psize a)%nat. - apply Psize_monotone. - change (Zpos (a-b) < Zpos a). - rewrite (Pminus_Zminus b a). - assert (0 < Zpos b) by (compute; auto). - omega. - rewrite ZC4; rewrite H1; auto. -omega. -rewrite Zpos_xO; do 2 rewrite Zpos_xI. -rewrite Pminus_Zminus; auto. -omega. -rewrite ZC4; rewrite H1; auto. -(* a = xI, b = xO *) -apply Zis_gcd_sym. -apply Zis_gcd_even_odd. -apply Zis_gcd_sym. -apply H; auto. -simpl in *; omega. -(* a = xI, b = xH *) -apply Zis_gcd_1. -destruct b; simpl. -(* a = xO, b = xI *) -apply Zis_gcd_even_odd. -apply H; auto. -simpl in *; omega. -(* a = xO, b = xO *) -rewrite (Zpos_xO a); rewrite (Zpos_xO b); rewrite (Zpos_xO (Pgcdn n a b)). -apply Zis_gcd_mult. -apply H; auto. -simpl in *; omega. -(* a = xO, b = xH *) -apply Zis_gcd_1. -(* a = xH *) -simpl; apply Zis_gcd_sym; apply Zis_gcd_1. + Zis_gcd (Zpos a) (Zpos b) (Zpos (Pgcdn n a b)). +Proof. + intro n; pattern n; apply lt_wf_ind; clear n; intros. + destruct n. + simpl. + destruct a; simpl in *; try inversion H0. + destruct a. + destruct b; simpl. + case_eq (Pcompare a b Eq); intros. + (* a = xI, b = xI, compare = Eq *) + rewrite (Pcompare_Eq_eq _ _ H1); apply Zis_gcd_refl. + (* a = xI, b = xI, compare = Lt *) + apply Zis_gcd_sym. + apply Zis_gcd_for_euclid with 1. + apply Zis_gcd_sym. + replace (Zpos (xI b) - 1 * Zpos (xI a)) with (Zpos(xO (b - a))). + apply Zis_gcd_even_odd. + apply H; auto. + simpl in *. + assert (Psize (b-a) <= Psize b)%nat. + apply Psize_monotone. + change (Zpos (b-a) < Zpos b). + rewrite (Pminus_Zminus _ _ H1). + assert (0 < Zpos a) by (compute; auto). + omega. + omega. + rewrite Zpos_xO; do 2 rewrite Zpos_xI. + rewrite Pminus_Zminus; auto. + omega. + (* a = xI, b = xI, compare = Gt *) + apply Zis_gcd_for_euclid with 1. + replace (Zpos (xI a) - 1 * Zpos (xI b)) with (Zpos(xO (a - b))). + apply Zis_gcd_sym. + apply Zis_gcd_even_odd. + apply H; auto. + simpl in *. + assert (Psize (a-b) <= Psize a)%nat. + apply Psize_monotone. + change (Zpos (a-b) < Zpos a). + rewrite (Pminus_Zminus b a). + assert (0 < Zpos b) by (compute; auto). + omega. + rewrite ZC4; rewrite H1; auto. + omega. + rewrite Zpos_xO; do 2 rewrite Zpos_xI. + rewrite Pminus_Zminus; auto. + omega. + rewrite ZC4; rewrite H1; auto. + (* a = xI, b = xO *) + apply Zis_gcd_sym. + apply Zis_gcd_even_odd. + apply Zis_gcd_sym. + apply H; auto. + simpl in *; omega. + (* a = xI, b = xH *) + apply Zis_gcd_1. + destruct b; simpl. + (* a = xO, b = xI *) + apply Zis_gcd_even_odd. + apply H; auto. + simpl in *; omega. + (* a = xO, b = xO *) + rewrite (Zpos_xO a); rewrite (Zpos_xO b); rewrite (Zpos_xO (Pgcdn n a b)). + apply Zis_gcd_mult. + apply H; auto. + simpl in *; omega. + (* a = xO, b = xH *) + apply Zis_gcd_1. + (* a = xH *) + simpl; apply Zis_gcd_sym; apply Zis_gcd_1. Qed. Lemma Pgcd_correct : forall a b, Zis_gcd (Zpos a) (Zpos b) (Zpos (Pgcd a b)). Proof. -unfold Pgcd; intros. -apply Pgcdn_correct; auto. + unfold Pgcd; intros. + apply Pgcdn_correct; auto. Qed. Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Zgcd a b). Proof. -destruct a. -intros. -simpl. -apply Zis_gcd_0_abs. -destruct b; simpl. -apply Zis_gcd_0. -apply Pgcd_correct. -apply Zis_gcd_sym. -apply Zis_gcd_minus; simpl. -apply Pgcd_correct. -destruct b; simpl. -apply Zis_gcd_minus; simpl. -apply Zis_gcd_sym. -apply Zis_gcd_0. -apply Zis_gcd_minus; simpl. -apply Zis_gcd_sym. -apply Pgcd_correct. -apply Zis_gcd_sym. -apply Zis_gcd_minus; simpl. -apply Zis_gcd_minus; simpl. -apply Zis_gcd_sym. -apply Pgcd_correct. + destruct a. + intros. + simpl. + apply Zis_gcd_0_abs. + destruct b; simpl. + apply Zis_gcd_0. + apply Pgcd_correct. + apply Zis_gcd_sym. + apply Zis_gcd_minus; simpl. + apply Pgcd_correct. + destruct b; simpl. + apply Zis_gcd_minus; simpl. + apply Zis_gcd_sym. + apply Zis_gcd_0. + apply Zis_gcd_minus; simpl. + apply Zis_gcd_sym. + apply Pgcd_correct. + apply Zis_gcd_sym. + apply Zis_gcd_minus; simpl. + apply Zis_gcd_minus; simpl. + apply Zis_gcd_sym. + apply Pgcd_correct. Qed. Lemma Pggcdn_gcdn : forall n a b, - fst (Pggcdn n a b) = Pgcdn n a b. + fst (Pggcdn n a b) = Pgcdn n a b. Proof. -induction n. -simpl; auto. -destruct a; destruct b; simpl; auto. -destruct (Pcompare a b Eq); simpl; auto. -rewrite <- IHn; destruct (Pggcdn n (b-a) (xI a)) as (g,(aa,bb)); simpl; auto. -rewrite <- IHn; destruct (Pggcdn n (a-b) (xI b)) as (g,(aa,bb)); simpl; auto. -rewrite <- IHn; destruct (Pggcdn n (xI a) b) as (g,(aa,bb)); simpl; auto. -rewrite <- IHn; destruct (Pggcdn n a (xI b)) as (g,(aa,bb)); simpl; auto. -rewrite <- IHn; destruct (Pggcdn n a b) as (g,(aa,bb)); simpl; auto. + induction n. + simpl; auto. + destruct a; destruct b; simpl; auto. + destruct (Pcompare a b Eq); simpl; auto. + rewrite <- IHn; destruct (Pggcdn n (b-a) (xI a)) as (g,(aa,bb)); simpl; auto. + rewrite <- IHn; destruct (Pggcdn n (a-b) (xI b)) as (g,(aa,bb)); simpl; auto. + rewrite <- IHn; destruct (Pggcdn n (xI a) b) as (g,(aa,bb)); simpl; auto. + rewrite <- IHn; destruct (Pggcdn n a (xI b)) as (g,(aa,bb)); simpl; auto. + rewrite <- IHn; destruct (Pggcdn n a b) as (g,(aa,bb)); simpl; auto. Qed. Lemma Pggcd_gcd : forall a b, fst (Pggcd a b) = Pgcd a b. Proof. -intros; exact (Pggcdn_gcdn (Psize a+Psize b)%nat a b). + intros; exact (Pggcdn_gcdn (Psize a+Psize b)%nat a b). Qed. Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b. Proof. -destruct a; destruct b; simpl; auto; rewrite <- Pggcd_gcd; -destruct (Pggcd p p0) as (g,(aa,bb)); simpl; auto. + destruct a; destruct b; simpl; auto; rewrite <- Pggcd_gcd; + destruct (Pggcd p p0) as (g,(aa,bb)); simpl; auto. Qed. Open Scope positive_scope. Lemma Pggcdn_correct_divisors : forall n a b, let (g,p) := Pggcdn n a b in - let (aa,bb):=p in - (a=g*aa) /\ (b=g*bb). -Proof. -induction n. -simpl; auto. -destruct a; destruct b; simpl; auto. -case_eq (Pcompare a b Eq); intros. -(* Eq *) -rewrite Pmult_comm; simpl; auto. -rewrite (Pcompare_Eq_eq _ _ H); auto. -(* Lt *) -generalize (IHn (b-a) (xI a)); destruct (Pggcdn n (b-a) (xI a)) as (g,(ba,aa)); simpl. -intros (H0,H1); split; auto. -rewrite Pmult_plus_distr_l. -rewrite Pmult_xO_permute_r. -rewrite <- H1; rewrite <- H0. -simpl; f_equal; symmetry. -apply Pplus_minus; auto. -rewrite ZC4; rewrite H; auto. -(* Gt *) -generalize (IHn (a-b) (xI b)); destruct (Pggcdn n (a-b) (xI b)) as (g,(ab,bb)); simpl. -intros (H0,H1); split; auto. -rewrite Pmult_plus_distr_l. -rewrite Pmult_xO_permute_r. -rewrite <- H1; rewrite <- H0. -simpl; f_equal; symmetry. -apply Pplus_minus; auto. -(* Then... *) -generalize (IHn (xI a) b); destruct (Pggcdn n (xI a) b) as (g,(ab,bb)); simpl. -intros (H0,H1); split; auto. -rewrite Pmult_xO_permute_r; rewrite H1; auto. -generalize (IHn a (xI b)); destruct (Pggcdn n a (xI b)) as (g,(ab,bb)); simpl. -intros (H0,H1); split; auto. -rewrite Pmult_xO_permute_r; rewrite H0; auto. -generalize (IHn a b); destruct (Pggcdn n a b) as (g,(ab,bb)); simpl. -intros (H0,H1); split; subst; auto. + let (aa,bb):=p in + (a=g*aa) /\ (b=g*bb). +Proof. + induction n. + simpl; auto. + destruct a; destruct b; simpl; auto. + case_eq (Pcompare a b Eq); intros. + (* Eq *) + rewrite Pmult_comm; simpl; auto. + rewrite (Pcompare_Eq_eq _ _ H); auto. + (* Lt *) + generalize (IHn (b-a) (xI a)); destruct (Pggcdn n (b-a) (xI a)) as (g,(ba,aa)); simpl. + intros (H0,H1); split; auto. + rewrite Pmult_plus_distr_l. + rewrite Pmult_xO_permute_r. + rewrite <- H1; rewrite <- H0. + simpl; f_equal; symmetry. + apply Pplus_minus; auto. + rewrite ZC4; rewrite H; auto. + (* Gt *) + generalize (IHn (a-b) (xI b)); destruct (Pggcdn n (a-b) (xI b)) as (g,(ab,bb)); simpl. + intros (H0,H1); split; auto. + rewrite Pmult_plus_distr_l. + rewrite Pmult_xO_permute_r. + rewrite <- H1; rewrite <- H0. + simpl; f_equal; symmetry. + apply Pplus_minus; auto. + (* Then... *) + generalize (IHn (xI a) b); destruct (Pggcdn n (xI a) b) as (g,(ab,bb)); simpl. + intros (H0,H1); split; auto. + rewrite Pmult_xO_permute_r; rewrite H1; auto. + generalize (IHn a (xI b)); destruct (Pggcdn n a (xI b)) as (g,(ab,bb)); simpl. + intros (H0,H1); split; auto. + rewrite Pmult_xO_permute_r; rewrite H0; auto. + generalize (IHn a b); destruct (Pggcdn n a b) as (g,(ab,bb)); simpl. + intros (H0,H1); split; subst; auto. Qed. Lemma Pggcd_correct_divisors : forall a b, let (g,p) := Pggcd a b in - let (aa,bb):=p in - (a=g*aa) /\ (b=g*bb). + let (aa,bb):=p in + (a=g*aa) /\ (b=g*bb). Proof. -intros a b; exact (Pggcdn_correct_divisors (Psize a + Psize b)%nat a b). + intros a b; exact (Pggcdn_correct_divisors (Psize a + Psize b)%nat a b). Qed. Open Scope Z_scope. Lemma Zggcd_correct_divisors : forall a b, let (g,p) := Zggcd a b in - let (aa,bb):=p in - (a=g*aa) /\ (b=g*bb). + let (aa,bb):=p in + (a=g*aa) /\ (b=g*bb). Proof. -destruct a; destruct b; simpl; auto; try solve [rewrite Pmult_comm; simpl; auto]; -generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb)); -destruct 1; subst; auto. + destruct a; destruct b; simpl; auto; try solve [rewrite Pmult_comm; simpl; auto]; + generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb)); + destruct 1; subst; auto. Qed. Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}. |