diff options
Diffstat (limited to 'coqprime/Coqprime/Pmod.v')
| -rw-r--r-- | coqprime/Coqprime/Pmod.v | 617 |
1 files changed, 0 insertions, 617 deletions
diff --git a/coqprime/Coqprime/Pmod.v b/coqprime/Coqprime/Pmod.v deleted file mode 100644 index fdaf321a2..000000000 --- a/coqprime/Coqprime/Pmod.v +++ /dev/null @@ -1,617 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -Require Export ZArith. -Require Export ZCmisc. - -Local Open Scope positive_scope. - -Local Open Scope P_scope. - -(* [div_eucl a b] return [(q,r)] such that a = q*b + r *) -Fixpoint div_eucl (a b : positive) {struct a} : N * N := - match a with - | xH => if 1 ?< b then (0%N, 1%N) else (1%N, 0%N) - | xO a' => - let (q, r) := div_eucl a' b in - match q, r with - | N0, N0 => (0%N, 0%N) (* n'arrive jamais *) - | N0, Npos r => - if (xO r) ?< b then (0%N, Npos (xO r)) - else (1%N,PminusN (xO r) b) - | Npos q, N0 => (Npos (xO q), 0%N) - | Npos q, Npos r => - if (xO r) ?< b then (Npos (xO q), Npos (xO r)) - else (Npos (xI q),PminusN (xO r) b) - end - | xI a' => - let (q, r) := div_eucl a' b in - match q, r with - | N0, N0 => (0%N, 0%N) (* Impossible *) - | N0, Npos r => - if (xI r) ?< b then (0%N, Npos (xI r)) - else (1%N,PminusN (xI r) b) - | Npos q, N0 => if 1 ?< b then (Npos (xO q), 1%N) else (Npos (xI q), 0%N) - | Npos q, Npos r => - if (xI r) ?< b then (Npos (xO q), Npos (xI r)) - else (Npos (xI q),PminusN (xI r) b) - end - end. -Infix "/" := div_eucl : P_scope. - -Open Scope Z_scope. -Opaque Zmult. -Lemma div_eucl_spec : forall a b, - Zpos a = fst (a/b)%P * b + snd (a/b)%P - /\ snd (a/b)%P < b. -Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega). - intros a b;generalize a;clear a;induction a;simpl;zsimpl. - case IHa; destruct (a/b)%P as [q r]. - case q; case r; simpl fst; simpl snd. - rewrite Zmult_0_l; rewrite Zplus_0_r; intros HH; discriminate HH. - intros p H; rewrite H; - match goal with - | [|- context [ ?xx ?< b ]] => - generalize (is_lt_spec xx b);destruct (xx ?< b) - | _ => idtac - end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto. - rewrite PminusN_le... - generalize H1; zsimpl; auto. - rewrite PminusN_le... - generalize H1; zsimpl; auto. - intros p H; rewrite H; - match goal with - | [|- context [ ?xx ?< b ]] => - generalize (is_lt_spec xx b);destruct (xx ?< b) - | _ => idtac - end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring. - ring_simplify. - case (Zle_lt_or_eq _ _ H1); auto with zarith. - intros p p1 H; rewrite H. - match goal with - | [|- context [ ?xx ?< b ]] => - generalize (is_lt_spec xx b);destruct (xx ?< b) - | _ => idtac - end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring. - rewrite PminusN_le... - generalize H1; zsimpl; auto. - rewrite PminusN_le... - generalize H1; zsimpl; auto. - case IHa; destruct (a/b)%P as [q r]. - case q; case r; simpl fst; simpl snd. - rewrite Zmult_0_l; rewrite Zplus_0_r; intros HH; discriminate HH. - intros p H; rewrite H; - match goal with - | [|- context [ ?xx ?< b ]] => - generalize (is_lt_spec xx b);destruct (xx ?< b) - | _ => idtac - end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto. - rewrite PminusN_le... - generalize H1; zsimpl; auto. - rewrite PminusN_le... - generalize H1; zsimpl; auto. - intros p H; rewrite H; simpl; intros H1; split; auto. - zsimpl; ring. - intros p p1 H; rewrite H. - match goal with - | [|- context [ ?xx ?< b ]] => - generalize (is_lt_spec xx b);destruct (xx ?< b) - | _ => idtac - end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring. - rewrite PminusN_le... - generalize H1; zsimpl; auto. - rewrite PminusN_le... - generalize H1; zsimpl; auto. - match goal with - | [|- context [ ?xx ?< b ]] => - generalize (is_lt_spec xx b);destruct (xx ?< b) - | _ => idtac - end; zsimpl; simpl. - split; auto. - case (Zle_lt_or_eq 1 b); auto with zarith. - generalize (Zlt_0_pos b); auto with zarith. -Qed. -Transparent Zmult. - -(******** Definition du modulo ************) - -(* [mod a b] return [a] modulo [b] *) -Fixpoint Pmod (a b : positive) {struct a} : N := - match a with - | xH => if 1 ?< b then 1%N else 0%N - | xO a' => - let r := Pmod a' b in - match r with - | N0 => 0%N - | Npos r' => - if (xO r') ?< b then Npos (xO r') - else PminusN (xO r') b - end - | xI a' => - let r := Pmod a' b in - match r with - | N0 => if 1 ?< b then 1%N else 0%N - | Npos r' => - if (xI r') ?< b then Npos (xI r') - else PminusN (xI r') b - end - end. - -Infix "mod" := Pmod (at level 40, no associativity) : P_scope. -Local Open Scope P_scope. - -Lemma Pmod_div_eucl : forall a b, a mod b = snd (a/b). -Proof with auto. - intros a b;generalize a;clear a;induction a;simpl; - try (rewrite IHa; - assert (H1 := div_eucl_spec a b); destruct (a/b) as [q r]; - destruct q as [|q];destruct r as [|r];simpl in *; - match goal with - | [|- context [ ?xx ?< b ]] => - assert (H2 := is_lt_spec xx b);destruct (xx ?< b) - | _ => idtac - end;simpl) ... - destruct H1 as [H3 H4];discriminate H3. - destruct (1 ?< b);simpl ... -Qed. - -Lemma mod1: forall a, a mod 1 = 0%N. -Proof. induction a;simpl;try rewrite IHa;trivial. Qed. - -Lemma mod_a_a_0 : forall a, a mod a = N0. -Proof. - intros a;generalize (div_eucl_spec a a);rewrite <- Pmod_div_eucl. - destruct (fst (a / a));unfold Z_of_N at 1. - rewrite Zmult_0_l;intros (H1,H2);elimtype False;omega. - assert (a<=p*a). - pattern (Zpos a) at 1;rewrite <- (Zmult_1_l a). - assert (H1:= Zlt_0_pos p);assert (H2:= Zle_0_pos a); - apply Zmult_le_compat;trivial;try omega. - destruct (a mod a)%P;auto with zarith. - unfold Z_of_N;assert (H1:= Zlt_0_pos p0);intros (H2,H3);elimtype False;omega. -Qed. - -Lemma mod_le_2r : forall (a b r: positive) (q:N), - Zpos a = b*q + r -> b <= a -> r < b -> 2*r <= a. -Proof. - intros a b r q H0 H1 H2. - assert (H3:=Zlt_0_pos a). assert (H4:=Zlt_0_pos b). assert (H5:=Zlt_0_pos r). - destruct q as [|q]. rewrite Zmult_0_r in H0. elimtype False;omega. - assert (H6:=Zlt_0_pos q). unfold Z_of_N in H0. - assert (Zpos r = a - b*q). omega. - simpl;zsimpl. pattern r at 2;rewrite H. - assert (b <= b * q). - pattern (Zpos b) at 1;rewrite <- (Zmult_1_r b). - apply Zmult_le_compat;try omega. - apply Zle_trans with (a - b * q + b). omega. - apply Zle_trans with (a - b + b);omega. -Qed. - -Lemma mod_lt : forall a b r, a mod b = Npos r -> r < b. -Proof. - intros a b r H;generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl; - rewrite H;simpl;intros (H1,H2);omega. -Qed. - -Lemma mod_le : forall a b r, a mod b = Npos r -> r <= b. -Proof. intros a b r H;assert (H1:= mod_lt _ _ _ H);omega. Qed. - -Lemma mod_le_a : forall a b r, a mod b = r -> r <= a. -Proof. - intros a b r H;generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl; - rewrite H;simpl;intros (H1,H2). - assert (0 <= fst (a / b) * b). - destruct (fst (a / b));simpl;auto with zarith. - auto with zarith. -Qed. - -Lemma lt_mod : forall a b, Zpos a < Zpos b -> (a mod b)%P = Npos a. -Proof. - intros a b H; rewrite Pmod_div_eucl. case (div_eucl_spec a b). - assert (0 <= snd(a/b)). destruct (snd(a/b));simpl;auto with zarith. - destruct (fst (a/b)). - unfold Z_of_N at 1;rewrite Zmult_0_l;rewrite Zplus_0_l. - destruct (snd (a/b));simpl; intros H1 H2;inversion H1;trivial. - unfold Z_of_N at 1;assert (b <= p*b). - pattern (Zpos b) at 1; rewrite <- (Zmult_1_l (Zpos b)). - assert (H1 := Zlt_0_pos p);apply Zmult_le_compat;try omega. - apply Zle_0_pos. - intros;elimtype False;omega. -Qed. - -Fixpoint gcd_log2 (a b c:positive) {struct c}: option positive := - match a mod b with - | N0 => Some b - | Npos r => - match b mod r, c with - | N0, _ => Some r - | Npos r', xH => None - | Npos r', xO c' => gcd_log2 r r' c' - | Npos r', xI c' => gcd_log2 r r' c' - end - end. - -Fixpoint egcd_log2 (a b c:positive) {struct c}: - option (Z * Z * positive) := - match a/b with - | (_, N0) => Some (0, 1, b) - | (q, Npos r) => - match b/r, c with - | (_, N0), _ => Some (1, -q, r) - | (q', Npos r'), xH => None - | (q', Npos r'), xO c' => - match egcd_log2 r r' c' with - None => None - | Some (u', v', w') => - let u := u' - v' * q' in - Some (u, v' - q * u, w') - end - | (q', Npos r'), xI c' => - match egcd_log2 r r' c' with - None => None - | Some (u', v', w') => - let u := u' - v' * q' in - Some (u, v' - q * u, w') - end - end - end. - -Lemma egcd_gcd_log2: forall c a b, - match egcd_log2 a b c, gcd_log2 a b c with - None, None => True - | Some (u,v,r), Some r' => r = r' - | _, _ => False - end. -induction c; simpl; auto; try - (intros a b; generalize (Pmod_div_eucl a b); case (a/b); simpl; - intros q r1 H; subst; case (a mod b); auto; - intros r; generalize (Pmod_div_eucl b r); case (b/r); simpl; - intros q' r1 H; subst; case (b mod r); auto; - intros r'; generalize (IHc r r'); case egcd_log2; auto; - intros ((p1,p2),p3); case gcd_log2; auto). -Qed. - -Ltac rw l := - match l with - | (?r, ?r1) => - match type of r with - True => rewrite <- r1 - | _ => rw r; rw r1 - end - | ?r => rewrite r - end. - -Lemma egcd_log2_ok: forall c a b, - match egcd_log2 a b c with - None => True - | Some (u,v,r) => u * a + v * b = r - end. -induction c; simpl; auto; - intros a b; generalize (div_eucl_spec a b); case (a/b); - simpl fst; simpl snd; intros q r1; case r1; try (intros; ring); - simpl; intros r (Hr1, Hr2); clear r1; - generalize (div_eucl_spec b r); case (b/r); - simpl fst; simpl snd; intros q' r1; case r1; - try (intros; rewrite Hr1; ring); - simpl; intros r' (Hr'1, Hr'2); clear r1; auto; - generalize (IHc r r'); case egcd_log2; auto; - intros ((u',v'),w'); case gcd_log2; auto; intros; - rw ((I, H), Hr1, Hr'1); ring. -Qed. - - -Fixpoint log2 (a:positive) : positive := - match a with - | xH => xH - | xO a => Psucc (log2 a) - | xI a => Psucc (log2 a) - end. - -Lemma gcd_log2_1: forall a c, gcd_log2 a xH c = Some xH. -Proof. destruct c;simpl;try rewrite mod1;trivial. Qed. - -Lemma log2_Zle :forall a b, Zpos a <= Zpos b -> log2 a <= log2 b. -Proof with zsimpl;try omega. - induction a;destruct b;zsimpl;intros;simpl ... - assert (log2 a <= log2 b) ... apply IHa ... - assert (log2 a <= log2 b) ... apply IHa ... - assert (H1 := Zlt_0_pos a);elimtype False;omega. - assert (log2 a <= log2 b) ... apply IHa ... - assert (log2 a <= log2 b) ... apply IHa ... - assert (H1 := Zlt_0_pos a);elimtype False;omega. - assert (H1 := Zlt_0_pos (log2 b)) ... - assert (H1 := Zlt_0_pos (log2 b)) ... -Qed. - -Lemma log2_1_inv : forall a, Zpos (log2 a) = 1 -> a = xH. -Proof. - destruct a;simpl;zsimpl;intros;trivial. - assert (H1:= Zlt_0_pos (log2 a));elimtype False;omega. - assert (H1:= Zlt_0_pos (log2 a));elimtype False;omega. -Qed. - -Lemma mod_log2 : - forall a b r:positive, a mod b = Npos r -> b <= a -> log2 r + 1 <= log2 a. -Proof. - intros; cut (log2 (xO r) <= log2 a). simpl;zsimpl;trivial. - apply log2_Zle. - replace (Zpos (xO r)) with (2 * r)%Z;trivial. - generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl;rewrite H. - rewrite Zmult_comm;intros [H1 H2];apply mod_le_2r with b (fst (a/b));trivial. -Qed. - -Lemma gcd_log2_None_aux : - forall c a b, Zpos b <= Zpos a -> log2 b <= log2 c -> - gcd_log2 a b c <> None. -Proof. - induction c;simpl;intros; - (CaseEq (a mod b);[intros Heq|intros r Heq];try (intro;discriminate)); - (CaseEq (b mod r);[intros Heq'|intros r' Heq'];try (intro;discriminate)). - apply IHc. apply mod_le with b;trivial. - generalize H0 (mod_log2 _ _ _ Heq' (mod_le _ _ _ Heq));zsimpl;intros;omega. - apply IHc. apply mod_le with b;trivial. - generalize H0 (mod_log2 _ _ _ Heq' (mod_le _ _ _ Heq));zsimpl;intros;omega. - assert (Zpos (log2 b) = 1). - assert (H1 := Zlt_0_pos (log2 b));omega. - rewrite (log2_1_inv _ H1) in Heq;rewrite mod1 in Heq;discriminate Heq. -Qed. - -Lemma gcd_log2_None : forall a b, Zpos b <= Zpos a -> gcd_log2 a b b <> None. -Proof. intros;apply gcd_log2_None_aux;auto with zarith. Qed. - -Lemma gcd_log2_Zle : - forall c1 c2 a b, log2 c1 <= log2 c2 -> - gcd_log2 a b c1 <> None -> gcd_log2 a b c2 = gcd_log2 a b c1. -Proof with zsimpl;trivial;try omega. - induction c1;destruct c2;simpl;intros; - (destruct (a mod b) as [|r];[idtac | destruct (b mod r)]) ... - apply IHc1;trivial. generalize H;zsimpl;intros;omega. - apply IHc1;trivial. generalize H;zsimpl;intros;omega. - elim H;destruct (log2 c1);trivial. - apply IHc1;trivial. generalize H;zsimpl;intros;omega. - apply IHc1;trivial. generalize H;zsimpl;intros;omega. - elim H;destruct (log2 c1);trivial. - elim H0;trivial. elim H0;trivial. -Qed. - -Lemma gcd_log2_Zle_log : - forall a b c, log2 b <= log2 c -> Zpos b <= Zpos a -> - gcd_log2 a b c = gcd_log2 a b b. -Proof. - intros a b c H1 H2; apply gcd_log2_Zle; trivial. - apply gcd_log2_None; trivial. -Qed. - -Lemma gcd_log2_mod0 : - forall a b c, a mod b = N0 -> gcd_log2 a b c = Some b. -Proof. intros a b c H;destruct c;simpl;rewrite H;trivial. Qed. - - -Require Import Zwf. - -Lemma Zwf_pos : well_founded (fun x y => Zpos x < Zpos y). -Proof. - unfold well_founded. - assert (forall x a ,x = Zpos a -> Acc (fun x y : positive => x < y) a). - intros x;assert (Hacc := Zwf_well_founded 0 x);induction Hacc;intros;subst x. - constructor;intros. apply H0 with (Zpos y);trivial. - split;auto with zarith. - intros a;apply H with (Zpos a);trivial. -Qed. - -Opaque Pmod. -Lemma gcd_log2_mod : forall a b, Zpos b <= Zpos a -> - forall r, a mod b = Npos r -> gcd_log2 a b b = gcd_log2 b r r. -Proof. - intros a b;generalize a;clear a; assert (Hacc := Zwf_pos b). - induction Hacc; intros a Hle r Hmod. - rename x into b. destruct b;simpl;rewrite Hmod. - CaseEq (xI b mod r)%P;intros. rewrite gcd_log2_mod0;trivial. - assert (H2 := mod_le _ _ _ H1);assert (H3 := mod_lt _ _ _ Hmod); - assert (H4 := mod_le _ _ _ Hmod). - rewrite (gcd_log2_Zle_log r p b);trivial. - symmetry;apply H0;trivial. - generalize (mod_log2 _ _ _ H1 H4);simpl;zsimpl;intros;omega. - CaseEq (xO b mod r)%P;intros. rewrite gcd_log2_mod0;trivial. - assert (H2 := mod_le _ _ _ H1);assert (H3 := mod_lt _ _ _ Hmod); - assert (H4 := mod_le _ _ _ Hmod). - rewrite (gcd_log2_Zle_log r p b);trivial. - symmetry;apply H0;trivial. - generalize (mod_log2 _ _ _ H1 H4);simpl;zsimpl;intros;omega. - rewrite mod1 in Hmod;discriminate Hmod. -Qed. - -Lemma gcd_log2_xO_Zle : - forall a b, Zpos b <= Zpos a -> gcd_log2 a b (xO b) = gcd_log2 a b b. -Proof. - intros a b Hle;apply gcd_log2_Zle. - simpl;zsimpl;auto with zarith. - apply gcd_log2_None_aux;auto with zarith. -Qed. - -Lemma gcd_log2_xO_Zlt : - forall a b, Zpos a < Zpos b -> gcd_log2 a b (xO b) = gcd_log2 b a a. -Proof. - intros a b H;simpl. assert (Hlt := Zlt_0_pos a). - assert (H0 := lt_mod _ _ H). - rewrite H0;simpl. - CaseEq (b mod a)%P;intros;simpl. - symmetry;apply gcd_log2_mod0;trivial. - assert (H2 := mod_lt _ _ _ H1). - rewrite (gcd_log2_Zle_log a p b);auto with zarith. - symmetry;apply gcd_log2_mod;auto with zarith. - apply log2_Zle. - replace (Zpos p) with (Z_of_N (Npos p));trivial. - apply mod_le_a with a;trivial. -Qed. - -Lemma gcd_log2_x0 : forall a b, gcd_log2 a b (xO b) <> None. -Proof. - intros;simpl;CaseEq (a mod b)%P;intros. intro;discriminate. - CaseEq (b mod p)%P;intros. intro;discriminate. - assert (H1 := mod_le_a _ _ _ H0). unfold Z_of_N in H1. - assert (H2 := mod_le _ _ _ H0). - apply gcd_log2_None_aux. trivial. - apply log2_Zle. trivial. -Qed. - -Lemma egcd_log2_x0 : forall a b, egcd_log2 a b (xO b) <> None. -Proof. -intros a b H; generalize (egcd_gcd_log2 (xO b) a b) (gcd_log2_x0 a b); - rw H; case gcd_log2; auto. -Qed. - -Definition gcd a b := - match gcd_log2 a b (xO b) with - | Some p => p - | None => (* can not appear *) 1%positive - end. - -Definition egcd a b := - match egcd_log2 a b (xO b) with - | Some p => p - | None => (* can not appear *) (1,1,1%positive) - end. - - -Lemma gcd_mod0 : forall a b, (a mod b)%P = N0 -> gcd a b = b. -Proof. - intros a b H;unfold gcd. - pattern (gcd_log2 a b (xO b)) at 1; - rewrite (gcd_log2_mod0 _ _ (xO b) H);trivial. -Qed. - -Lemma gcd1 : forall a, gcd a xH = xH. -Proof. intros a;rewrite gcd_mod0;[trivial|apply mod1]. Qed. - -Lemma gcd_mod : forall a b r, (a mod b)%P = Npos r -> - gcd a b = gcd b r. -Proof. - intros a b r H;unfold gcd. - assert (log2 r <= log2 (xO r)). simpl;zsimpl;omega. - assert (H1 := mod_lt _ _ _ H). - pattern (gcd_log2 b r (xO r)) at 1; rewrite gcd_log2_Zle_log;auto with zarith. - destruct (Z_lt_le_dec a b) as [z|z]. - pattern (gcd_log2 a b (xO b)) at 1; rewrite gcd_log2_xO_Zlt;trivial. - rewrite (lt_mod _ _ z) in H;inversion H. - assert (r <= b). omega. - generalize (gcd_log2_None _ _ H2). - destruct (gcd_log2 b r r);intros;trivial. - assert (log2 b <= log2 (xO b)). simpl;zsimpl;omega. - pattern (gcd_log2 a b (xO b)) at 1; rewrite gcd_log2_Zle_log;auto with zarith. - pattern (gcd_log2 a b b) at 1;rewrite (gcd_log2_mod _ _ z _ H). - assert (r <= b). omega. - generalize (gcd_log2_None _ _ H3). - destruct (gcd_log2 b r r);intros;trivial. -Qed. - -Require Import ZArith. -Require Import Znumtheory. - -Hint Rewrite Zpos_mult times_Zmult square_Zmult Psucc_Zplus: zmisc. - -Ltac mauto := - trivial;autorewrite with zmisc;trivial;auto with zarith. - -Lemma gcd_Zis_gcd : forall a b:positive, (Zis_gcd b a (gcd b a)%P). -Proof with mauto. - intros a;assert (Hacc := Zwf_pos a);induction Hacc;rename x into a;intros. - generalize (div_eucl_spec b a)... - rewrite <- (Pmod_div_eucl b a). - CaseEq (b mod a)%P;[intros Heq|intros r Heq]; intros (H1,H2). - simpl in H1;rewrite Zplus_0_r in H1. - rewrite (gcd_mod0 _ _ Heq). - constructor;mauto. - apply Zdivide_intro with (fst (b/a)%P);trivial. - rewrite (gcd_mod _ _ _ Heq). - rewrite H1;apply Zis_gcd_sym. - rewrite Zmult_comm;apply Zis_gcd_for_euclid2;simpl in *. - apply Zis_gcd_sym;auto. -Qed. - -Lemma egcd_Zis_gcd : forall a b:positive, - let (uv,w) := egcd a b in - let (u,v) := uv in - u * a + v * b = w /\ (Zis_gcd b a w). -Proof with mauto. - intros a b; unfold egcd. - generalize (egcd_log2_ok (xO b) a b) (egcd_gcd_log2 (xO b) a b) - (egcd_log2_x0 a b) (gcd_Zis_gcd b a); unfold egcd, gcd. - case egcd_log2; try (intros ((u,v),w)); case gcd_log2; - try (intros; match goal with H: False |- _ => case H end); - try (intros _ _ H1; case H1; auto; fail). - intros; subst; split; try apply Zis_gcd_sym; auto. -Qed. - -Definition Zgcd a b := - match a, b with - | Z0, _ => b - | _, Z0 => a - | Zpos a, Zneg b => Zpos (gcd a b) - | Zneg a, Zpos b => Zpos (gcd a b) - | Zpos a, Zpos b => Zpos (gcd a b) - | Zneg a, Zneg b => Zpos (gcd a b) - end. - - -Lemma Zgcd_is_gcd : forall x y, Zis_gcd x y (Zgcd x y). -Proof. - destruct x;destruct y;simpl. - apply Zis_gcd_0. - apply Zis_gcd_sym;apply Zis_gcd_0. - apply Zis_gcd_sym;apply Zis_gcd_0. - apply Zis_gcd_0. - apply gcd_Zis_gcd. - apply Zis_gcd_sym;apply Zis_gcd_minus;simpl;apply gcd_Zis_gcd. - apply Zis_gcd_0. - apply Zis_gcd_minus;simpl;apply Zis_gcd_sym;apply gcd_Zis_gcd. - apply Zis_gcd_minus;apply Zis_gcd_minus;simpl;apply gcd_Zis_gcd. -Qed. - -Definition Zegcd a b := - match a, b with - | Z0, Z0 => (0,0,0) - | Zpos _, Z0 => (1,0,a) - | Zneg _, Z0 => (-1,0,-a) - | Z0, Zpos _ => (0,1,b) - | Z0, Zneg _ => (0,-1,-b) - | Zpos a, Zneg b => - match egcd a b with (u,v,w) => (u,-v, Zpos w) end - | Zneg a, Zpos b => - match egcd a b with (u,v,w) => (-u,v, Zpos w) end - | Zpos a, Zpos b => - match egcd a b with (u,v,w) => (u,v, Zpos w) end - | Zneg a, Zneg b => - match egcd a b with (u,v,w) => (-u,-v, Zpos w) end - end. - -Lemma Zegcd_is_egcd : forall x y, - match Zegcd x y with - (u,v,w) => u * x + v * y = w /\ Zis_gcd x y w /\ 0 <= w - end. -Proof. - assert (zx0: forall x, Zneg x = -x). - simpl; auto. - assert (zx1: forall x, -(-x) = x). - intro x; case x; simpl; auto. - destruct x;destruct y;simpl; try (split; [idtac|split]); - auto; try (red; simpl; intros; discriminate); - try (rewrite zx0; apply Zis_gcd_minus; try rewrite zx1; auto; - apply Zis_gcd_minus; try rewrite zx1; simpl; auto); - try apply Zis_gcd_0; try (apply Zis_gcd_sym;apply Zis_gcd_0); - generalize (egcd_Zis_gcd p p0); case egcd; intros (u,v) w (H1, H2); - split; repeat rewrite zx0; try (rewrite <- H1; ring); auto; - (split; [idtac | red; intros; discriminate]). - apply Zis_gcd_sym; auto. - apply Zis_gcd_sym; apply Zis_gcd_minus; rw zx1; - apply Zis_gcd_sym; auto. - apply Zis_gcd_minus; rw zx1; auto. - apply Zis_gcd_minus; rw zx1; auto. - apply Zis_gcd_minus; rw zx1; auto. - apply Zis_gcd_sym; auto. -Qed. |