From ef92beece3147f8af0764521e22cb7fc9a3f32a3 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Sat, 24 Feb 2018 10:17:35 -0500
Subject: coqprime in COQPATH (closes #269)

---
 coqprime/Coqprime/Pmod.v | 617 -----------------------------------------------
 1 file changed, 617 deletions(-)
 delete mode 100644 coqprime/Coqprime/Pmod.v

(limited to 'coqprime/Coqprime/Pmod.v')

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.
-- 
cgit v1.2.3