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

3 files changed, 87 insertions, 0 deletions

diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index 5cfd0c416..22c9012a7 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.v
@@ -13,6 +13,7 @@ Require Export BinNat.
 Require Export Nnat.
 Require Export Ndiv_def.
 Require Export Nsqrt_def.
+Require Export Ngcd_def.
 Require Export Ndigits.
 Require Export NArithRing.
 Require NBinary.
diff --git a/theories/NArith/Ngcd_def.v b/theories/NArith/Ngcd_def.v
new file mode 100644
index 000000000..fe5185c6b
--- /dev/null
+++ b/theories/NArith/Ngcd_def.v
@@ -0,0 +1,85 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import BinPos BinNat Pgcd.
+
+Local Open Scope N_scope.
+
+(** * Divisibility *)
+
+Definition Ndivide p q := exists r, p*r = q.
+Notation "( p | q )" := (Ndivide p q) (at level 0) : N_scope.
+
+(** * Definition of a Pgcd function for binary natural numbers *)
+
+Definition Ngcd (a b : N) :=
+ match a, b with
+  | 0, _ => b
+  | _, 0 => a
+  | Npos p, Npos q => Npos (Pgcd p q)
+ end.
+
+(** * Generalized Gcd, also computing rests of a and b after
+    division by gcd. *)
+
+Definition Nggcd (a b : N) :=
+ match a, b with
+  | 0, _ => (b,(0,1))
+  | _, 0 => (a,(1,0))
+  | Npos p, Npos q =>
+     let '(g,(aa,bb)) := Pggcd p q in
+     (Npos g, (Npos aa, Npos bb))
+ end.
+
+(** The first component of Nggcd is Ngcd *)
+
+Lemma Nggcd_gcd : forall  a b, fst (Nggcd a b) = Ngcd a b.
+Proof.
+ intros [ |p] [ |q]; simpl; auto.
+ generalize (Pggcd_gcd p q). destruct Pggcd as (g,(aa,bb)); simpl; congruence.
+Qed.
+
+(** The other components of Nggcd are indeed the correct factors. *)
+
+Lemma Nggcd_correct_divisors : forall a b,
+  let '(g,(aa,bb)) := Nggcd a b in
+  a=g*aa /\ b=g*bb.
+Proof.
+ intros [ |p] [ |q]; simpl; auto.
+ now rewrite Pmult_1_r.
+ now rewrite Pmult_1_r.
+ generalize (Pggcd_correct_divisors p q).
+ destruct Pggcd as (g,(aa,bb)); simpl. destruct 1; split; congruence.
+Qed.
+
+(** We can use this fact to prove a part of the gcd correctness *)
+
+Lemma Ngcd_divide_l : forall a b, (Ngcd a b | a).
+Proof.
+ intros a b. rewrite <- Nggcd_gcd. generalize (Nggcd_correct_divisors a b).
+ destruct Nggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto.
+Qed.
+
+Lemma Ngcd_divide_r : forall a b, (Ngcd a b | b).
+Proof.
+ intros a b. rewrite <- Nggcd_gcd. generalize (Nggcd_correct_divisors a b).
+ destruct Nggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto.
+Qed.
+
+(** We now prove directly that gcd is the greatest amongst common divisors *)
+
+Lemma Ngcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|Ngcd a b).
+Proof.
+ intros [ |p] [ |q]; simpl; auto.
+ intros [ |r]. intros (s,H). discriminate.
+ intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *.
+ destruct (Pgcd_greatest p q r) as (u,H).
+ exists s. now inversion Hs.
+ exists t. now inversion Ht.
+ exists (Npos u). simpl; now f_equal.
+Qed.
diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget
index 1797b25e4..3e285772d 100644
--- a/theories/NArith/vo.itarget
+++ b/theories/NArith/vo.itarget
@@ -6,3 +6,4 @@ Ndist.vo
 Nnat.vo
 Ndiv_def.vo
 Nsqrt_def.vo
+Ngcd_def.vo
\ No newline at end of file