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, 36 insertions, 0 deletions

diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 547f51b3d5..7b90aa09e0 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -299,6 +299,42 @@ destruct (Z_mod_lt [a] [b]); auto.
 generalize (spec_pos b); auto with zarith.
 Qed.
 
+(** Gcd *)
+
+Definition divide n m := exists p, n*p == m.
+Local Notation "( x | y )" := (divide x y) (at level 0).
+
+Lemma spec_divide : forall n m, (n|m) <-> Zdivide' [n] [m].
+Proof.
+ intros n m. split.
+ intros (p,H). exists [p]. revert H; now zify.
+ intros (z,H). exists (of_N (Zabs_N z)). zify.
+ rewrite spec_of_N, Z_of_N_abs.
+ rewrite <- (Zabs_eq [n]) by apply spec_pos.
+ rewrite <- Zabs_Zmult, H.
+ apply Zabs_eq, spec_pos.
+Qed.
+
+Lemma gcd_divide_l : forall n m, (gcd n m | n).
+Proof.
+ intros n m. apply spec_divide. zify. apply Zgcd_divide_l.
+Qed.
+
+Lemma gcd_divide_r : forall n m, (gcd n m | m).
+Proof.
+ intros n m. apply spec_divide. zify. apply Zgcd_divide_r.
+Qed.
+
+Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m).
+Proof.
+ intros n m p. rewrite !spec_divide. zify. apply Zgcd_greatest.
+Qed.
+
+Lemma gcd_nonneg : forall n m, 0 <= gcd n m.
+Proof.
+ intros. zify. apply Zgcd_nonneg.
+Qed.
+
 (** Recursion *)
 
 Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=