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, 220 insertions, 6 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 2fbfb04c24..ee2a92e84d 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Export NZAxioms NZPow NZSqrt NZLog NZDiv.
+Require Export NZAxioms NZPow NZSqrt NZLog NZDiv NZGcd.
 
 (** From [NZ], we obtain natural numbers just by stating that [pred 0] == 0 *)
 
@@ -39,16 +39,16 @@ Module Type NDivSpecific (Import N : NAxiomsMiniSig')(Import DM : DivMod' N).
  Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b.
 End NDivSpecific.
 
-(** For pow sqrt log2, the NZ axiomatizations are enough. *)
+(** For gcd pow sqrt log2, the NZ axiomatizations are enough. *)
 
 (** We now group everything together. *)
 
 Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ Parity
-  <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2
+  <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd
   <+ DivMod <+ NZDivCommon <+ NDivSpecific.
 
 Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ Parity
-  <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2
+  <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'
   <+ DivMod' <+ NZDivCommon <+ NDivSpecific.
 
 
diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v
new file mode 100644
index 0000000000..5bf33d4d26
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NGcd.v
@@ -0,0 +1,214 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Properties of the greatest common divisor *)
+
+Require Import NAxioms NSub NZGcd.
+
+Module NGcdProp
+ (Import A : NAxiomsSig')
+ (Import B : NSubProp A).
+
+ Include NZGcdProp A A B.
+
+(** Results concerning divisibility*)
+
+Definition divide_1_r n : (n | 1) -> n == 1
+ := divide_1_r_nonneg n (le_0_l n).
+
+Definition divide_antisym n m : (n | m) -> (m | n) -> n == m
+ := divide_antisym_nonneg n m (le_0_l n) (le_0_l m).
+
+Lemma divide_add_cancel_r : forall n m p, (n | m) -> (n | m + p) -> (n | p).
+Proof.
+ intros n m p (q,Hq) (r,Hr).
+ exists (r-q). rewrite mul_sub_distr_l, Hq, Hr.
+ now rewrite add_comm, add_sub.
+Qed.
+
+Lemma divide_sub_r : forall n m p, (n | m) -> (n | p) -> (n | m - p).
+Proof.
+ intros n m p H H'.
+ destruct (le_ge_cases m p) as [LE|LE].
+ apply sub_0_le in LE. rewrite LE. apply divide_0_r.
+ apply divide_add_cancel_r with p; trivial.
+ now rewrite add_comm, sub_add.
+Qed.
+
+(** Properties of gcd *)
+
+Definition gcd_0_l n : gcd 0 n == n := gcd_0_l_nonneg n (le_0_l n).
+Definition gcd_0_r n : gcd n 0 == n := gcd_0_r_nonneg n (le_0_l n).
+Definition gcd_diag n : gcd n n == n := gcd_diag_nonneg n (le_0_l n).
+Definition gcd_unique' n m p := gcd_unique n m p (le_0_l p).
+Definition gcd_unique_alt' n m p := gcd_unique_alt n m p (le_0_l p).
+Definition divide_gcd_iff' n m := divide_gcd_iff n m (le_0_l n).
+
+Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m.
+Proof.
+ intros. apply gcd_unique_alt'.
+ intros. rewrite gcd_divide_iff. split; intros (U,V); split; trivial.
+ apply divide_add_r; trivial. now apply divide_mul_r.
+ apply divide_add_cancel_r with (p*n); trivial.
+ now apply divide_mul_r. now rewrite add_comm.
+Qed.
+
+Lemma gcd_add_diag_r : forall n m, gcd n (m+n) == gcd n m.
+Proof.
+ intros n m. rewrite <- (mul_1_l n) at 2. apply gcd_add_mult_diag_r.
+Qed.
+
+Lemma gcd_sub_diag_r : forall n m, n<=m -> gcd n (m-n) == gcd n m.
+Proof.
+ intros n m H. symmetry.
+ rewrite <- (sub_add n m H) at 1. apply gcd_add_diag_r.
+Qed.
+
+(** On natural numbers, we should use a particular form
+  for the Bezout identity, since we don't have full subtraction. *)
+
+Definition Bezout n m p := exists a, exists b, a*n == p + b*m.
+
+Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout.
+Proof.
+ unfold Bezout. intros x x' Hx y y' Hy z z' Hz.
+ setoid_rewrite Hx. setoid_rewrite Hy. now setoid_rewrite Hz.
+Qed.
+
+Lemma bezout_1_gcd : forall n m, Bezout n m 1 -> gcd n m == 1.
+Proof.
+ intros n m (q & r & H).
+ apply gcd_unique; trivial using divide_1_l, le_0_1.
+ intros p Hn Hm.
+ apply divide_add_cancel_r with (r*m).
+ now apply divide_mul_r.
+ rewrite add_comm, <- H. now apply divide_mul_r.
+Qed.
+
+(** For strictly positive numbers, we have Bezout in the two directions. *)
+
+Lemma gcd_bezout_pos_pos : forall n, 0<n -> forall m, 0<m ->
+ Bezout n m (gcd n m) /\ Bezout m n (gcd n m).
+Proof.
+ intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn.
+ pattern n. apply strong_right_induction with (z:=1); trivial.
+ unfold Bezout. solve_predicate_wd.
+ clear n Hn. intros n Hn IHn.
+ intros m Hm. rewrite <- le_succ_l, <- one_succ in Hm.
+ pattern m. apply strong_right_induction with (z:=1); trivial.
+ unfold Bezout. solve_predicate_wd.
+ clear m Hm. intros m Hm IHm.
+ destruct (lt_trichotomy n m) as [LT|[EQ|LT]].
+ (* n < m *)
+ destruct (IHm (m-n)) as ((a & b & EQ), (a' & b' & EQ')).
+ rewrite one_succ, le_succ_l.
+ apply lt_add_lt_sub_l; now nzsimpl.
+ apply sub_lt; order'.
+ split.
+ exists (a+b). exists b.
+ rewrite mul_add_distr_r, EQ, mul_sub_distr_l, <- add_assoc.
+ rewrite gcd_sub_diag_r by order.
+ rewrite sub_add. reflexivity. apply mul_le_mono_l; order.
+ exists a'. exists (a'+b').
+ rewrite gcd_sub_diag_r in EQ' by order.
+ rewrite (add_comm a'), mul_add_distr_r, add_assoc, <- EQ'.
+ rewrite mul_sub_distr_l, sub_add. reflexivity. apply mul_le_mono_l; order.
+ (* n = m *)
+ rewrite EQ. rewrite gcd_diag.
+ split.
+ exists 1. exists 0. now nzsimpl.
+ exists 1. exists 0. now nzsimpl.
+ (* m < n *)
+ rewrite gcd_comm, and_comm.
+ apply IHn; trivial.
+ now rewrite <- le_succ_l, <- one_succ.
+Qed.
+
+Lemma gcd_bezout_pos : forall n m, 0<n -> Bezout n m (gcd n m).
+Proof.
+ intros n m Hn.
+ destruct (eq_0_gt_0_cases m) as [EQ|LT].
+ rewrite EQ, gcd_0_r. exists 1. exists 0. now nzsimpl.
+ now apply gcd_bezout_pos_pos.
+Qed.
+
+(** For arbitrary natural numbers, we could only say that at least
+  one of the Bezout identities holds. *)
+
+Lemma gcd_bezout : forall n m,
+ Bezout n m (gcd n m) \/ Bezout m n (gcd n m).
+Proof.
+ intros n m.
+ destruct (eq_0_gt_0_cases n) as [EQ|LT].
+ right. rewrite EQ, gcd_0_l. exists 1. exists 0. now nzsimpl.
+ left. now apply gcd_bezout_pos.
+Qed.
+
+Lemma gcd_mul_mono_l :
+  forall n m p, gcd (p * n) (p * m) == p * gcd n m.
+Proof.
+ intros n m p.
+ apply gcd_unique'.
+ apply mul_divide_mono_l, gcd_divide_l.
+ apply mul_divide_mono_l, gcd_divide_r.
+ intros q H H'.
+ destruct (eq_0_gt_0_cases n) as [EQ|LT].
+ rewrite EQ in *. now rewrite gcd_0_l.
+ destruct (gcd_bezout_pos n m) as (a & b & EQ); trivial.
+ apply divide_add_cancel_r with (p*m*b).
+ now apply divide_mul_l.
+ rewrite <- mul_assoc, <- mul_add_distr_l, add_comm, (mul_comm m), <- EQ.
+ rewrite (mul_comm a), mul_assoc.
+ now apply divide_mul_l.
+Qed.
+
+Lemma gcd_mul_mono_r :
+ forall n m p, gcd (n*p) (m*p) == gcd n m * p.
+Proof.
+ intros. rewrite !(mul_comm _ p). apply gcd_mul_mono_l.
+Qed.
+
+Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p).
+Proof.
+ intros n m p H G.
+ destruct (eq_0_gt_0_cases n) as [EQ|LT].
+ rewrite EQ in *. rewrite gcd_0_l in G. now rewrite <- (mul_1_l p), <- G.
+ destruct (gcd_bezout_pos n m) as (a & b & EQ); trivial.
+ rewrite G in EQ.
+ apply divide_add_cancel_r with (m*p*b).
+ now apply divide_mul_l.
+ rewrite (mul_comm _ b), mul_assoc. rewrite <- (mul_1_l p) at 2.
+ rewrite <- mul_add_distr_r, add_comm, <- EQ.
+ now apply divide_mul_l, divide_factor_r.
+Qed.
+
+Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) ->
+ exists q, exists r, n == q*r /\ (q | m) /\ (r | p).
+Proof.
+ intros n m p Hn H.
+ assert (G := gcd_nonneg n m).
+ apply le_lteq in G; destruct G as [G|G].
+ destruct (gcd_divide_l n m) as (q,Hq).
+ exists (gcd n m). exists q.
+ split. easy.
+ split. apply gcd_divide_r.
+ destruct (gcd_divide_r n m) as (r,Hr).
+ rewrite <- Hr in H. rewrite <- Hq in H at 1.
+ rewrite <- mul_assoc in H. apply mul_divide_cancel_l in H; [|order].
+ apply gauss with r; trivial.
+ apply mul_cancel_l with (gcd n m); [order|].
+ rewrite mul_1_r.
+ rewrite <- gcd_mul_mono_l, Hq, Hr; order.
+ symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order.
+Qed.
+
+(** TODO : relation between gcd and division and modulo *)
+
+(** TODO : more about rel_prime (i.e. gcd == 1), about prime ... *)
+
+End NGcdProp.
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 35b6af8342..3fc44124f3 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -7,10 +7,10 @@
 (************************************************************************)
 
 Require Export NAxioms.
-Require Import NMaxMin NParity NPow NSqrt NLog NDiv.
+Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd.
 
 (** This functor summarizes all known facts about N. *)
 
 Module Type NProp (N:NAxiomsSig) :=
  NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N
-  <+ NLog2Prop N <+ NDivProp N.
+  <+ NLog2Prop N <+ NDivProp N <+ NGcdProp N.