Numbers: axiomatization, properties and implementations of gcd

 - For nat, we create a brand-new gcd function, structural in
   the sense of Coq, even if it's Euclid algorithm. Cool...
 - We re-organize the Zgcd that was in Znumtheory, create out of it
   files Pgcd, Ngcd_def, Zgcd_def. Proofs of correctness are revised
   in order to be much simpler (no omega, no advanced lemmas of
   Znumtheory, etc).
 - Abstract Properties NZGcd / ZGcd / NGcd could still be completed,
   for the moment they contain up to Gauss thm. We could add stuff
   about (relative) primality, relationship between gcd and div,mod,
   or stuff about parity, etc etc.
 - Znumtheory remains as it was, apart for Zgcd and correctness proofs
   gone elsewhere. We could later take advantage of ZGcd in it.
   Someday, we'll have to switch from the current Zdivide inductive,
   to Zdivide' via exists. To be continued...

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

1 files changed, 14 insertions, 22 deletions

diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index ad16f8a25..4888ce4b1 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -9,7 +9,7 @@
 (** Normalisation functions for rational numbers. *)
 
 Require Export QArith_base.
-Require Import Znumtheory.
+Require Import Zgcd_def Znumtheory.
 
 (** First, a function that (tries to) build a positive back from a Z. *)
 
@@ -41,23 +41,16 @@ Definition Qred (q:Q) :=
 Lemma Qred_correct : forall q, (Qred q) == q.
 Proof.
   unfold Qred, Qeq; intros (n,d); simpl.
-  generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d))
-    (Zgcd_is_gcd n ('d)) (Zggcd_correct_divisors n ('d)).
+  generalize (Zggcd_gcd n ('d)) (Zgcd_nonneg n ('d))
+    (Zggcd_correct_divisors n ('d)).
   destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl.
   Open Scope Z_scope.
-  intuition.
-  rewrite <- H in H0,H1; clear H.
-  rewrite H3; rewrite H4.
-  assert (0 <> g).
-  intro; subst g; discriminate.
-
-  assert (0 < dd).
-  apply Zmult_gt_0_lt_0_reg_r with g.
-  omega.
-  rewrite Zmult_comm.
-  rewrite <- H4; compute; auto.
-  rewrite Z2P_correct; auto.
-  ring.
+  intros Hg LE (Hn,Hd). rewrite Hd, Hn.
+  rewrite <- Hg in LE; clear Hg.
+  assert (0 <> g) by (intro; subst; discriminate).
+  rewrite Z2P_correct. ring.
+  apply Zmult_gt_0_lt_0_reg_r with g; auto with zarith.
+  now rewrite Zmult_comm, <- Hd.
   Close Scope Z_scope.
 Qed.
 
@@ -67,10 +60,10 @@ Proof.
   unfold Qred, Qeq in *; simpl in *.
   Open Scope Z_scope.
   generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b))
-    (Zgcd_is_pos a ('b)) (Zggcd_correct_divisors a ('b)).
+    (Zgcd_nonneg a ('b)) (Zggcd_correct_divisors a ('b)).
   destruct (Zggcd a (Zpos b)) as (g,(aa,bb)).
   generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d))
-    (Zgcd_is_pos c ('d)) (Zggcd_correct_divisors c ('d)).
+    (Zgcd_nonneg c ('d)) (Zggcd_correct_divisors c ('d)).
   destruct (Zggcd c (Zpos d)) as (g',(cc,dd)).
   simpl.
   intro H; rewrite <- H; clear H.
@@ -78,10 +71,9 @@ Proof.
   intro H; rewrite <- H; clear H.
   intros Hg1 Hg2 (Hg3,Hg4).
   intros.
-  assert (g <> 0).
-  intro; subst g; discriminate.
-  assert (g' <> 0).
-  intro; subst g'; discriminate.
+  assert (g <> 0) by (intro; subst g; discriminate).
+  assert (g' <> 0) by (intro; subst g'; discriminate).
+
   elim (rel_prime_cross_prod aa bb cc dd).
   congruence.
   unfold rel_prime in |- *.