un Zgcd general gardant trace des coefs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8789 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 59 insertions, 0 deletions

diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 452ebd30f..e528dd3db 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -430,6 +430,65 @@ 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.
 
+(** A version of gcd that stores coefficients (used for fraction reduction) *)
+
+Definition Zgcd_gen_pos :
+  forall a:Z,
+    0 <= a -> forall b:Z, {p : Z*(Z*Z) | let (g,p):=p in let (aa,bb):=p in 
+                                       0 <= a -> Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}.
+Proof.
+intros a Ha.
+pattern a; apply Zlt_0_rec; try assumption.
+intro x; case x.
+intros _ _ b; exists (Zabs b,(0,Zsgn 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.
+    repeat split; auto with zarith.
+    symmetry; apply Zabs_Zsgn.
+    
+    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 (Zpos p)).
+case (Zdiv_eucl b (Zpos p)); intros q r Hqr.
+elim Hqr; clear Hqr; intros; auto with zarith.
+destruct (Hrec r H0 (Zpos p)) as ((g,(rr,pp)),Hgkl).
+destruct H0.
+destruct (Hgkl H0) as (H3,(H4,(H5,H6))).
+exists (g,(pp,pp*q+rr)); intros.
+split; auto.
+rewrite H.
+apply Zis_gcd_for_euclid2; auto.
+repeat split; auto.
+rewrite H; rewrite H6; rewrite H5; ring.
+
+intros p _ H b.
+elim H; auto.
+Defined.
+
+Definition Zgcd_gen_spec : 
+ forall a b:Z, {p : Z*(Z*Z) |  let (g,p):=p in let (aa,bb):=p in 
+                                          Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}.
+Proof.
+intros a; case (Z_gt_le_dec 0 a).
+intros; assert (0 <= - a).
+omega.
+destruct (Zgcd_gen_pos (- a) H b) as ((g,(aa,bb)),Hgkl).
+exists (g,(-aa,bb)).
+intuition.
+rewrite <- Zopp_mult_distr_r.
+rewrite <- H2; auto with zarith.
+intros Ha b; elim (Zgcd_gen_pos a Ha b); intros p; exists p.
+ repeat destruct p; intuition.
+Defined.
+
+Definition Zgcd_gen (a b:Z) := let (p, _) := Zgcd_gen_spec a b in p.
+
 (** * Relative primality *)
 
 Definition rel_prime (a b:Z) : Prop := Zis_gcd a b 1.