diff options
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 846 |
1 files changed, 429 insertions, 417 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index dfe1c31fda..ed6272c445 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -8,11 +8,10 @@ (*i $Id$ i*) -Require ZArith_base. -Require ZArithRing. -Require Zcomplements. -Require Zdiv. -V7only [Import Z_scope.]. +Require Import ZArith_base. +Require Import ZArithRing. +Require Import Zcomplements. +Require Import Zdiv. Open Local Scope Z_scope. (** This file contains some notions of number theory upon Z numbers: @@ -26,176 +25,173 @@ Open Local Scope Z_scope. (** * Divisibility *) -Inductive Zdivide [a,b:Z] : Prop := - Zdivide_intro : (q:Z) `b = q * a` -> (Zdivide a b). +Inductive Zdivide (a b:Z) : Prop := + Zdivide_intro : forall q:Z, b = q * a -> Zdivide a b. (** Syntax for divisibility *) -Notation "( a | b )" := (Zdivide a b) - (at level 0, a,b at level 10) : Z_scope - V8only (at level 0, a,b at level 250). +Notation "( a | b )" := (Zdivide a b) (at level 0, a, b at level 250) : + Z_scope. (** Results concerning divisibility*) -Lemma Zdivide_refl : (a:Z) (a|a). +Lemma Zdivide_refl : forall a:Z, (a | a). Proof. -Intros; Apply Zdivide_intro with `1`; Ring. -Save. +intros; apply Zdivide_intro with 1; ring. +Qed. -Lemma Zone_divide : (a:Z) (1|a). +Lemma Zone_divide : forall a:Z, (1 | a). Proof. -Intros; Apply Zdivide_intro with `a`; Ring. -Save. +intros; apply Zdivide_intro with a; ring. +Qed. -Lemma Zdivide_0 : (a:Z) (a|0). +Lemma Zdivide_0 : forall a:Z, (a | 0). Proof. -Intros; Apply Zdivide_intro with `0`; Ring. -Save. +intros; apply Zdivide_intro with 0; ring. +Qed. -Hints Resolve Zdivide_refl Zone_divide Zdivide_0 : zarith. +Hint Resolve Zdivide_refl Zone_divide Zdivide_0: zarith. -Lemma Zdivide_mult_left : (a,b,c:Z) (a|b) -> (`c*a`|`c*b`). +Lemma Zmult_divide_compat_l : forall a b c:Z, (a | b) -> (c * a | c * b). Proof. -Induction 1; Intros; Apply Zdivide_intro with q. -Rewrite H0; Ring. -Save. +simple induction 1; intros; apply Zdivide_intro with q. +rewrite H0; ring. +Qed. -Lemma Zdivide_mult_right : (a,b,c:Z) (a|b) -> (`a*c`|`b*c`). +Lemma Zmult_divide_compat_r : forall a b c:Z, (a | b) -> (a * c | b * c). Proof. -Intros a b c; Rewrite (Zmult_sym a c); Rewrite (Zmult_sym b c). -Apply Zdivide_mult_left; Trivial. -Save. +intros a b c; rewrite (Zmult_comm a c); rewrite (Zmult_comm b c). +apply Zmult_divide_compat_l; trivial. +Qed. -Hints Resolve Zdivide_mult_left Zdivide_mult_right : zarith. +Hint Resolve Zmult_divide_compat_l Zmult_divide_compat_r: zarith. -Lemma Zdivide_plus : (a,b,c:Z) (a|b) -> (a|c) -> (a|`b+c`). +Lemma Zdivide_plus_r : forall a b c:Z, (a | b) -> (a | c) -> (a | b + c). Proof. -Induction 1; Intros q Hq; Induction 1; Intros q' Hq'. -Apply Zdivide_intro with `q+q'`. -Rewrite Hq; Rewrite Hq'; Ring. -Save. +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 : (a,b:Z) (a|b) -> (a|`-b`). +Lemma Zdivide_opp_r : forall a b:Z, (a | b) -> (a | - b). Proof. -Induction 1; Intros; Apply Zdivide_intro with `-q`. -Rewrite H0; Ring. -Save. +simple induction 1; intros; apply Zdivide_intro with (- q). +rewrite H0; ring. +Qed. -Lemma Zdivide_opp_rev : (a,b:Z) (a|`-b`) -> (a| b). +Lemma Zdivide_opp_r_rev : forall a b:Z, (a | - b) -> (a | b). Proof. -Intros; Replace b with `-(-b)`. Apply Zdivide_opp; Trivial. Ring. -Save. +intros; replace b with (- - b). apply Zdivide_opp_r; trivial. ring. +Qed. -Lemma Zdivide_opp_left : (a,b:Z) (a|b) -> (`-a`|b). +Lemma Zdivide_opp_l : forall a b:Z, (a | b) -> (- a | b). Proof. -Induction 1; Intros; Apply Zdivide_intro with `-q`. -Rewrite H0; Ring. -Save. +simple induction 1; intros; apply Zdivide_intro with (- q). +rewrite H0; ring. +Qed. -Lemma Zdivide_opp_left_rev : (a,b:Z) (`-a`|b) -> (a|b). +Lemma Zdivide_opp_l_rev : forall a b:Z, (- a | b) -> (a | b). Proof. -Intros; Replace a with `-(-a)`. Apply Zdivide_opp_left; Trivial. Ring. -Save. +intros; replace a with (- - a). apply Zdivide_opp_l; trivial. ring. +Qed. -Lemma Zdivide_minus : (a,b,c:Z) (a|b) -> (a|c) -> (a|`b-c`). +Lemma Zdivide_minus_l : forall a b c:Z, (a | b) -> (a | c) -> (a | b - c). Proof. -Induction 1; Intros q Hq; Induction 1; Intros q' Hq'. -Apply Zdivide_intro with `q-q'`. -Rewrite Hq; Rewrite Hq'; Ring. -Save. +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_left : (a,b,c:Z) (a|b) -> (a|`b*c`). +Lemma Zdivide_mult_l : forall a b c:Z, (a | b) -> (a | b * c). Proof. -Induction 1; Intros q Hq; Apply Zdivide_intro with `q*c`. -Rewrite Hq; Ring. -Save. +simple induction 1; intros q Hq; apply Zdivide_intro with (q * c). +rewrite Hq; ring. +Qed. -Lemma Zdivide_right : (a,b,c:Z) (a|c) -> (a|`b*c`). +Lemma Zdivide_mult_r : forall a b c:Z, (a | c) -> (a | b * c). Proof. -Induction 1; Intros q Hq; Apply Zdivide_intro with `q*b`. -Rewrite Hq; Ring. -Save. +simple induction 1; intros q Hq; apply Zdivide_intro with (q * b). +rewrite Hq; ring. +Qed. -Lemma Zdivide_a_ab : (a,b:Z) (a|`a*b`). +Lemma Zdivide_factor_r : forall a b:Z, (a | a * b). Proof. -Intros; Apply Zdivide_intro with b; Ring. -Save. +intros; apply Zdivide_intro with b; ring. +Qed. -Lemma Zdivide_a_ba : (a,b:Z) (a|`b*a`). +Lemma Zdivide_factor_l : forall a b:Z, (a | b * a). Proof. -Intros; Apply Zdivide_intro with b; Ring. -Save. +intros; apply Zdivide_intro with b; ring. +Qed. -Hints Resolve Zdivide_plus Zdivide_opp Zdivide_opp_rev - Zdivide_opp_left Zdivide_opp_left_rev - Zdivide_minus Zdivide_left Zdivide_right - Zdivide_a_ab Zdivide_a_ba : zarith. +Hint Resolve Zdivide_plus_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l + Zdivide_opp_l_rev Zdivide_minus_l Zdivide_mult_l Zdivide_mult_r + Zdivide_factor_r Zdivide_factor_l: zarith. (** Auxiliary result. *) -Lemma Zmult_one : - (x,y:Z) `x>=0` -> `x*y=1` -> `x=1`. +Lemma Zmult_one : forall x y:Z, x >= 0 -> x * y = 1 -> x = 1. Proof. -Intros x y H H0; NewDestruct (Zmult_1_inversion_l ? ? H0) as [Hpos|Hneg]. - Assumption. - Rewrite Hneg in H; Simpl in H. - Contradiction (Zle_not_lt `0` `-1`). - Apply Zge_le; Assumption. - Apply NEG_lt_ZERO. -Save. +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)). + apply Zge_le; assumption. + apply Zorder.Zlt_neg_0. +Qed. (** Only [1] and [-1] divide [1]. *) -Lemma Zdivide_1 : (x:Z) (x|1) -> `x=1` \/ `x=-1`. +Lemma Zdivide_1 : forall x:Z, (x | 1) -> x = 1 \/ x = -1. Proof. -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. -Save. +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]. *) -Lemma Zdivide_antisym : (a,b:Z) (a|b) -> (b|a) -> `a=b` \/ `a=-b`. -Proof. -Induction 1; Intros. -Inversion H1. -Rewrite H0 in H2; Clear H H1. -Case (Z_zerop a); Intro. -Left; Rewrite H0; Rewrite e; Ring. -Assert Hqq0: `q0*q = 1`. -Apply Zmult_reg_left with a. -Assumption. -Ring. -Pattern 2 a; Rewrite H2; Ring. -Assert (q|1). -Rewrite <- Hqq0; Auto with zarith. -Elim (Zdivide_1 q H); Intros. -Rewrite H1 in H0; Left; Omega. -Rewrite H1 in H0; Right; Omega. -Save. +Lemma Zdivide_antisym : forall a b:Z, (a | b) -> (b | a) -> a = b \/ a = - b. +Proof. +simple induction 1; intros. +inversion H1. +rewrite H0 in H2; clear H H1. +case (Z_zerop a); intro. +left; rewrite H0; rewrite e; ring. +assert (Hqq0 : q0 * q = 1). +apply Zmult_reg_l with a. +assumption. +ring. +pattern a at 2 in |- *; rewrite H2; ring. +assert (q | 1). +rewrite <- Hqq0; auto with zarith. +elim (Zdivide_1 q H); intros. +rewrite H1 in H0; left; omega. +rewrite H1 in H0; right; omega. +Qed. (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *) -Lemma Zdivide_bounds : (a,b:Z) (a|b) -> `b<>0` -> `|a| <= |b|`. -Proof. -Induction 1; Intros. -Assert `|b|=|q|*|a|`. - Subst; Apply Zabs_Zmult. -Rewrite H2. -Assert H3 := (Zabs_pos q). -Assert H4 := (Zabs_pos a). -Assert `|q|*|a|>=1*|a|`; Auto with zarith. -Apply Zge_Zmult_pos_compat; Auto with zarith. -Elim (Z_lt_ge_dec `|q|` `1`); [ Intros | Auto with zarith ]. -Assert `|q|=0`. - Omega. -Assert `q=0`. - Rewrite <- (Zabs_Zsgn q). -Rewrite H5; Auto with zarith. -Subst q; Omega. -Save. +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. +Qed. (** * Greatest common divisor (gcd). *) @@ -203,53 +199,54 @@ Save. expressing that [d] is a gcd of [a] and [b]. (We show later that the [gcd] is actually unique if we discard its sign.) *) -Inductive gcd [a,b,d:Z] : Prop := - gcd_intro : - (d|a) -> (d|b) -> ((x:Z) (x|a) -> (x|b) -> (x|d)) -> (gcd a b d). +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. (** Trivial properties of [gcd] *) -Lemma gcd_sym : (a,b,d:Z)(gcd a b d) -> (gcd b a d). +Lemma Zis_gcd_sym : forall a b d:Z, Zis_gcd a b d -> Zis_gcd b a d. Proof. -Induction 1; Constructor; Intuition. -Save. +simple induction 1; constructor; intuition. +Qed. -Lemma gcd_0 : (a:Z)(gcd a `0` a). +Lemma Zis_gcd_0 : forall a:Z, Zis_gcd a 0 a. Proof. -Constructor; Auto with zarith. -Save. +constructor; auto with zarith. +Qed. -Lemma gcd_minus :(a,b,d:Z)(gcd a `-b` d) -> (gcd b a d). +Lemma Zis_gcd_minus : forall a b d:Z, Zis_gcd a (- b) d -> Zis_gcd b a d. Proof. -Induction 1; Constructor; Intuition. -Save. +simple induction 1; constructor; intuition. +Qed. -Lemma gcd_opp :(a,b,d:Z)(gcd a b d) -> (gcd b a `-d`). +Lemma Zis_gcd_opp : forall a b d:Z, Zis_gcd a b d -> Zis_gcd b a (- d). Proof. -Induction 1; Constructor; Intuition. -Save. +simple induction 1; constructor; intuition. +Qed. -Hints Resolve gcd_sym gcd_0 gcd_minus gcd_opp : zarith. +Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith. (** * Extended Euclid algorithm. *) (** Euclid's algorithm to compute the [gcd] mainly relies on the following property. *) -Lemma gcd_for_euclid : - (a,b,d,q:Z) (gcd b `a-q*b` d) -> (gcd a b d). +Lemma Zis_gcd_for_euclid : + forall a b d q:Z, Zis_gcd b (a - q * b) d -> Zis_gcd a b d. Proof. -Induction 1; Constructor; Intuition. -Replace a with `a-q*b+q*b`. Auto with zarith. Ring. -Save. +simple induction 1; constructor; intuition. +replace a with (a - q * b + q * b). auto with zarith. ring. +Qed. -Lemma gcd_for_euclid2 : - (b,d,q,r:Z) (gcd r b d) -> (gcd b `b*q+r` d). +Lemma Zis_gcd_for_euclid2 : + forall b d q r:Z, Zis_gcd r b d -> Zis_gcd b (b * q + r) d. Proof. -Induction 1; Constructor; Intuition. -Apply H2; Auto. -Replace r with `b*q+r-b*q`. Auto with zarith. Ring. -Save. +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, i.e. the one computing Bezout's coefficients as it computes @@ -258,14 +255,14 @@ Save. Section extended_euclid_algorithm. -Variable 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)]. *) Inductive Euclid : Set := - Euclid_intro : - (u,v,d:Z) `u*a+v*b=d` -> (gcd a b d) -> Euclid. + 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 @@ -274,356 +271,371 @@ Inductive Euclid : Set := *) Lemma euclid_rec : - (v3:Z) `0 <= v3` -> (u1,u2,u3,v1,v2:Z) `u1*a+u2*b=u3` -> `v1*a+v2*b=v3` -> - ((d:Z)(gcd u3 v3 d) -> (gcd a b d)) -> Euclid. -Proof. -Intros v3 Hv3; Generalize Hv3; Pattern v3. -Apply Z_lt_rec. -Clear v3 Hv3; Intros. -Elim (Z_zerop x); Intro. -Apply Euclid_intro with u:=u1 v:=u2 d:=u3. -Assumption. -Apply H2. -Rewrite a0; Auto with zarith. -LetTac q := (Zdiv u3 x). -Assert Hq: `0 <= u3-q*x < x`. -Replace `u3-q*x` with `u3%x`. -Apply Z_mod_lt; Omega. -Assert xpos : `x > 0`. Omega. -Generalize (Z_div_mod_eq u3 x xpos). -Unfold q. -Intro eq; Pattern 2 u3; 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 H0; Rewrite H1; Trivial. -Ring. -Intros; Apply H2. -Apply gcd_for_euclid with q; Assumption. -Assumption. -Save. + 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 Z_lt_rec. +clear v3 Hv3; intros. +elim (Z_zerop x); intro. +apply Euclid_intro with (u := u1) (v := u2) (d := u3). +assumption. +apply H2. +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 H0; rewrite H1; trivial. +ring. +intros; apply H2. +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. -Save. +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 gcd_uniqueness_apart_sign : - (a,b,d,d':Z) (gcd a b d) -> (gcd a b d') -> `d = d'` \/ `d = -d'`. +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'. Proof. -Induction 1. -Intros H1 H2 H3; 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). -Save. +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 : (u,v:Z) `u*a + v*b = d` -> (Bezout a b d). +Inductive Bezout (a b d:Z) : Prop := + 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 gcd_bezout : (a,b,d:Z) (gcd a b d) -> (Bezout a b d). +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 (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. -Save. +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 gcd_mult : (a,b,c,d:Z) (gcd a b d) -> (gcd `c*a` `c*b` `c*d`). -Proof. -Intros a b c d; Induction 1; Constructor; Intuition. -Elim (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. -Save. +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. +Qed. (** We could obtain a [Zgcd] function via [euclid]. But we propose here a more direct version of a [Zgcd], with better extraction (no bezout coeffs). *) -Definition Zgcd_pos : (a:Z)`0<=a` -> (b:Z) - { g:Z | `0<=a` -> (gcd a b g) /\ `g>=0` }. -Proof. -Intros a Ha. -Apply (Z_lt_rec [a:Z](b:Z) { g:Z | `0<=a` -> (gcd a b g) /\`g>=0` }); Try Assumption. -Intro x; Case x. -Intros _ b; Exists (Zabs b). - Elim (Z_le_lt_eq_dec ? ? (Zabs_pos b)). - Intros H0; Split. - Apply Zabs_ind. - Intros; Apply gcd_sym; Apply gcd_0; Auto. - Intros; Apply gcd_opp; Apply gcd_0; Auto. - Auto with zarith. +Definition Zgcd_pos : + forall a:Z, + 0 <= a -> forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}. +Proof. +intros a Ha. +apply + (Z_lt_rec + (fun a:Z => forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0})); + try assumption. +intro x; case x. +intros _ b; exists (Zabs b). + elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)). + intros H0; split. + apply Zabs_ind. + intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. + intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. + auto with zarith. - Intros H0; Rewrite <- H0. - Rewrite <- (Zabs_Zsgn b); Rewrite <- H0; Simpl. - Split; [Apply gcd_0|Idtac];Auto with zarith. + intros H0; rewrite <- H0. + rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *. + split; [ apply Zis_gcd_0 | idtac ]; auto with zarith. -Intros p Hrec b. -Generalize (Z_div_mod b (POS p)). -Case (Zdiv_eucl b (POS p)); Intros q r Hqr. -Elim Hqr; Clear Hqr; Intros; Auto with zarith. -Elim (Hrec r H0 (POS p)); Intros g Hgkl. -Inversion_clear H0. -Elim (Hgkl H1); Clear Hgkl; Intros H3 H4. -Exists g; Intros. -Split; Auto. -Rewrite H. -Apply gcd_for_euclid2; Auto. - -Intros p Hrec b. -Exists `0`; Intros. -Elim H; Auto. +intros p Hrec b. +generalize (Z_div_mod b (Zpos p)). +case (Zdiv_eucl b (Zpos p)); intros q r Hqr. +elim Hqr; clear Hqr; intros; auto with zarith. +elim (Hrec r H0 (Zpos p)); intros g Hgkl. +inversion_clear H0. +elim (Hgkl H1); clear Hgkl; intros H3 H4. +exists g; intros. +split; auto. +rewrite H. +apply Zis_gcd_for_euclid2; auto. + +intros p Hrec b. +exists 0; intros. +elim H; auto. Defined. -Definition Zgcd_spec : (a,b:Z){ g : Z | (gcd a b g) /\ `g>=0` }. +Definition Zgcd_spec : forall a b:Z, {g : Z | Zis_gcd a b g /\ g >= 0}. Proof. -Intros a; Case (Z_gt_le_dec `0` a). -Intros; Assert `0 <= -a`. -Omega. -Elim (Zgcd_pos `-a` H b); Intros g Hgkl. -Exists g. -Intuition. -Intros Ha b; Elim (Zgcd_pos a Ha b); Intros g; Exists g; Intuition. +intros a; case (Z_gt_le_dec 0 a). +intros; assert (0 <= - a). +omega. +elim (Zgcd_pos (- a) H b); intros g Hgkl. +exists g. +intuition. +intros Ha b; elim (Zgcd_pos a Ha b); intros g; exists g; intuition. Defined. -Definition Zgcd := [a,b:Z](let (g,_) = (Zgcd_spec a b) in g). +Definition Zgcd (a b:Z) := let (g, _) := Zgcd_spec a b in g. -Lemma Zgcd_is_pos : (a,b:Z)`(Zgcd a b) >=0`. -Intros a b; Unfold Zgcd; Case (Zgcd_spec a b); Tauto. +Lemma Zgcd_is_pos : forall a b:Z, Zgcd a b >= 0. +intros a b; unfold Zgcd in |- *; case (Zgcd_spec a b); tauto. Qed. -Lemma Zgcd_is_gcd : (a,b:Z)(gcd a b (Zgcd a b)). -Intros a b; Unfold Zgcd; Case (Zgcd_spec a b); Tauto. +Lemma Zgcd_is_gcd : forall a b:Z, Zis_gcd a b (Zgcd a b). +intros a b; unfold Zgcd in |- *; case (Zgcd_spec a b); tauto. Qed. (** * Relative primality *) -Definition rel_prime [a,b:Z] : Prop := (gcd a b `1`). +Definition rel_prime (a b:Z) : Prop := Zis_gcd a b 1. (** Bezout's theorem: [a] and [b] are relatively prime if and only if there exist [u] and [v] such that [ua+vb = 1]. *) -Lemma rel_prime_bezout : - (a,b:Z) (rel_prime a b) -> (Bezout a b `1`). +Lemma rel_prime_bezout : forall a b:Z, rel_prime a b -> Bezout a b 1. Proof. -Intros a b; Exact (gcd_bezout a b `1`). -Save. +intros a b; exact (Zis_gcd_bezout a b 1). +Qed. -Lemma bezout_rel_prime : - (a,b:Z) (Bezout a b `1`) -> (rel_prime a b). +Lemma bezout_rel_prime : forall a b:Z, Bezout a b 1 -> rel_prime a b. Proof. -Induction 1; Constructor; Auto with zarith. -Intros. Rewrite <- H0; Auto with zarith. -Save. +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 relatively prime, then [a] divides [c]. *) -Theorem Gauss : (a,b,c:Z) (a |`b*c`) -> (rel_prime a b) -> (a | c). +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 ]. -Save. +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 : - (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. -Save. +Lemma rel_prime_mult : + 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. +Qed. Lemma rel_prime_cross_prod : - (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_sym in H3. -Apply Zmult_reg_left with d; Auto with zarith. -Intros; Omega. -Apply Gauss with a. -Rewrite H3. -Auto with zarith. -Red; Auto with zarith. -Apply Gauss with c. -Rewrite Zmult_sym. -Rewrite <- H3. -Auto with zarith. -Red; Auto with zarith. -Save. + 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 gcd_rel_prime : - (a,b,g:Z)`b>0` -> `g>=0`-> (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. -Elim (Zgcd_spec `a/g` `b/g`); Intros g' (H3,H4). -Assert H5 := (gcd_mult ? ? g ? H3). -Rewrite <- Z_div_exact_2 in H5; Auto with zarith. -Rewrite <- Z_div_exact_2 in H5; Auto with zarith. -Elim (gcd_uniqueness_apart_sign ? ? ? ? H1 H5). -Intros; Rewrite (!Zmult_reg_left `1` g' g); Auto with zarith. -Intros; Rewrite (!Zmult_reg_left `1` `-g'` g); Auto with zarith. -Pattern 1 g; Rewrite H6; Ring. - -Elim H1; Intros. -Elim H7; Intros. -Rewrite H9. -Replace `q*g` with `0+q*g`. -Rewrite Z_mod_plus. -Compute; Auto. -Omega. -Ring. - -Elim H1; Intros. -Elim H6; Intros. -Rewrite H9. -Replace `q*g` with `0+q*g`. -Rewrite Z_mod_plus. -Compute; Auto. -Omega. -Ring. -Save. +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 |- *. +elim (Zgcd_spec (a / g) (b / g)); intros g' [H3 H4]. +assert (H5 := Zis_gcd_mult _ _ g _ H3). +rewrite <- Z_div_exact_2 in H5; auto with zarith. +rewrite <- Z_div_exact_2 in H5; auto with zarith. +elim (Zis_gcd_uniqueness_apart_sign _ _ _ _ H1 H5). +intros; rewrite (Zmult_reg_l 1 g' g); auto with zarith. +intros; rewrite (Zmult_reg_l 1 (- g') g); auto with zarith. +pattern g at 1 in |- *; rewrite H6; ring. + +elim H1; intros. +elim H7; intros. +rewrite H9. +replace (q * g) with (0 + q * g). +rewrite Z_mod_plus. +compute in |- *; auto. +omega. +ring. + +elim H1; intros. +elim H6; intros. +rewrite H9. +replace (q * g) with (0 + q * g). +rewrite Z_mod_plus. +compute in |- *; auto. +omega. +ring. +Qed. (** * Primality *) -Inductive prime [p:Z] : Prop := - prime_intro : - `1 < p` -> ((n:Z) `1 <= n < p` -> (rel_prime n p)) -> (prime p). +Inductive prime (p:Z) : Prop := + 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 : - (p:Z) (prime p) -> - (a:Z) (a|p) -> `a = -1` \/ `a = 1` \/ a = p \/ `a = -p`. -Proof. -Induction 1; Intros. -Assert `a = (-p)`\/`-p<a< -1`\/`a = -1`\/`a=0`\/`a = 1`\/`1<a<p`\/`a = p`. -Assert `|a| <= |p|`. Apply Zdivide_bounds; [ Assumption | Omega ]. -Generalize H3. -Pattern `|a|`; Apply Zabs_ind; Pattern `|p|`; Apply Zabs_ind; Intros; Omega. -Intuition Idtac. +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. +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. +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. -Save. +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 : - (p:Z) (prime p) -> (a:Z) ~ (p|a) -> (rel_prime p a). +Lemma prime_rel_prime : + forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a. Proof. -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. -Save. +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. -Hints Resolve prime_rel_prime : zarith. +Hint Resolve prime_rel_prime: zarith. (** [Zdivide] can be expressed using [Zmod]. *) -Lemma Zmod_Zdivide : (a,b:Z) `b>0` -> `a%b = 0` -> (b|a). -Intros a b H H0. -Apply Zdivide_intro with `(a/b)`. -Pattern 1 a; Rewrite (Z_div_mod_eq a b H). -Rewrite H0; Ring. -Save. +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. +Qed. -Lemma Zdivide_Zmod : (a,b:Z) `b>0` -> (b|a) -> `a%b = 0`. -Intros a b; Destruct 2; Intros; Subst. -Change `q*b` with `0+q*b`. -Rewrite Z_mod_plus; Auto. -Save. +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. +Qed. (** [Zdivide] is hence decidable *) -Lemma Zdivide_dec : (a,b:Z) { (a|b) } + { ~ (a|b) }. +Lemma Zdivide_dec : forall a b:Z, {(a | b)} + {~ (a | b)}. Proof. -Intros a b; Elim (Ztrichotomy_inf a `0`). +intros a b; elim (Ztrichotomy_inf a 0). (* a<0 *) -Intros H; Elim H; Intros. -Case (Z_eq_dec `b%(-a)` `0`). -Left; Apply Zdivide_opp_left_rev; Apply Zmod_Zdivide; Auto with zarith. -Intro H1; Right; Intro; Elim H1; Apply Zdivide_Zmod; Auto with zarith. +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. +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%a` `0`). -Left; Apply Zmod_Zdivide; Auto with zarith. -Intro H1; Right; Intro; Elim H1; Apply Zdivide_Zmod; Auto with zarith. -Save. +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 : - (p:Z) (prime p) -> (a,b:Z) (p | `a*b`) -> (p | a) \/ (p | b). +Lemma prime_mult : + forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b). Proof. -Intro p; Induction 1; Intros. -Case (Zdivide_dec p a); Intuition. -Right; Apply Gauss with a; Auto with zarith. -Save. - +intro p; simple induction 1; intros. +case (Zdivide_dec p a); intuition. +right; apply Gauss with a; auto with zarith. +Qed. |