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

5 files changed, 325 insertions, 8 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 47286c729..754c0b3d1 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Export NZAxioms.
-Require Import NZPow NZSqrt NZLog.
+Require Import NZPow NZSqrt NZLog NZGcd.
 
 (** We obtain integers by postulating that successor of predecessor
     is identity. *)
@@ -70,16 +70,16 @@ Module Type Parity (Import Z : ZAxiomsMiniSig').
  Axiom odd_spec : forall n, odd n = true <-> Odd n.
 End Parity.
 
-(** For pow sqrt log2, the NZ axiomatizations are enough. *)
+(** For pow sqrt log2 gcd, the NZ axiomatizations are enough. *)
 
 (** Let's group everything *)
 
 Module Type ZAxiomsSig :=
   ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2.
+   <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd.
 Module Type ZAxiomsSig' :=
   ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2.
+   <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'.
 
 
 (** Division is left apart, since many different flavours are available *)
diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v
new file mode 100644
index 000000000..d58d1f1e2
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZGcd.v
@@ -0,0 +1,276 @@
+(************************************************************************)
+(*  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 ZAxioms ZMulOrder ZSgnAbs NZGcd.
+
+Module ZGcdProp
+ (Import A : ZAxiomsSig')
+ (Import B : ZMulOrderProp A)
+ (Import D : ZSgnAbsProp A B).
+
+ Include NZGcdProp A A B.
+
+(** Results concerning divisibility*)
+
+Lemma divide_opp_l : forall n m, (-n | m) <-> (n | m).
+Proof.
+ intros n m. split; intros (p,Hp); exists (-p); rewrite <- Hp.
+  now rewrite mul_opp_l, mul_opp_r.
+  now rewrite mul_opp_opp.
+Qed.
+
+Lemma divide_opp_r : forall n m, (n | -m) <-> (n | m).
+Proof.
+ intros n m. split; intros (p,Hp); exists (-p).
+  now rewrite mul_opp_r, Hp, opp_involutive.
+  now rewrite <- Hp, mul_opp_r.
+Qed.
+
+Lemma divide_abs_l : forall n m, (abs n | m) <-> (n | m).
+Proof.
+ intros n m. destruct (abs_eq_or_opp n) as [H|H]; rewrite H.
+ easy. apply divide_opp_l.
+Qed.
+
+Lemma divide_abs_r : forall n m, (n | abs m) <-> (n | m).
+Proof.
+ intros n m. destruct (abs_eq_or_opp m) as [H|H]; rewrite H.
+ easy. apply divide_opp_r.
+Qed.
+
+Lemma divide_1_r_abs : forall n, (n | 1) -> abs n == 1.
+Proof.
+ intros n Hn. apply divide_1_r_nonneg. apply abs_nonneg.
+ now apply divide_abs_l.
+Qed.
+
+Lemma divide_1_r : forall n, (n | 1) -> n==1 \/ n==-(1).
+Proof.
+ intros n (m,Hm). now apply eq_mul_1 with m.
+Qed.
+
+Lemma divide_antisym_abs : forall n m,
+ (n | m) -> (m | n) -> abs n == abs m.
+Proof.
+ intros. apply divide_antisym_nonneg; try apply abs_nonneg.
+ now apply divide_abs_l, divide_abs_r.
+ now apply divide_abs_l, divide_abs_r.
+Qed.
+
+Lemma divide_antisym : forall n m,
+ (n | m) -> (m | n) -> n == m \/ n == -m.
+Proof.
+ intros. now apply abs_eq_cases, divide_antisym_abs.
+Qed.
+
+Lemma divide_sub_r : forall n m p, (n | m) -> (n | p) -> (n | m - p).
+Proof.
+ intros n m p H H'. rewrite <- add_opp_r.
+ apply divide_add_r; trivial. now apply divide_opp_r.
+Qed.
+
+Lemma divide_add_cancel_r : forall n m p, (n | m) -> (n | m + p) -> (n | p).
+Proof.
+ intros n m p H H'. rewrite <- (add_simpl_l m p). now apply divide_sub_r.
+Qed.
+
+(** Properties of gcd *)
+
+Lemma gcd_opp_l : forall n m, gcd (-n) m == gcd n m.
+Proof.
+ intros. apply gcd_unique_alt; try apply gcd_nonneg.
+ intros. rewrite divide_opp_r. apply gcd_divide_iff.
+Qed.
+
+Lemma gcd_opp_r : forall n m, gcd n (-m) == gcd n m.
+Proof.
+ intros. now rewrite gcd_comm, gcd_opp_l, gcd_comm.
+Qed.
+
+Lemma gcd_abs_l : forall n m, gcd (abs n) m == gcd n m.
+Proof.
+ intros. destruct (abs_eq_or_opp n) as [H|H]; rewrite H.
+ easy. apply gcd_opp_l.
+Qed.
+
+Lemma gcd_abs_r : forall n m, gcd n (abs m) == gcd n m.
+Proof.
+ intros. now rewrite gcd_comm, gcd_abs_l, gcd_comm.
+Qed.
+
+Lemma gcd_0_l : forall n, gcd 0 n == abs n.
+Proof.
+ intros. rewrite <- gcd_abs_r. apply gcd_0_l_nonneg, abs_nonneg.
+Qed.
+
+Lemma gcd_0_r : forall n, gcd n 0 == abs n.
+Proof.
+ intros. now rewrite gcd_comm, gcd_0_l.
+Qed.
+
+Lemma gcd_diag : forall n, gcd n n == abs n.
+Proof.
+ intros. rewrite <- gcd_abs_l, <- gcd_abs_r.
+ apply gcd_diag_nonneg, abs_nonneg.
+Qed.
+
+Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m.
+Proof.
+ intros. apply gcd_unique_alt; try apply gcd_nonneg.
+ 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, gcd n (m-n) == gcd n m.
+Proof.
+ intros n m. rewrite <- (mul_1_l n) at 2.
+ rewrite <- add_opp_r, <- mul_opp_l. apply gcd_add_mult_diag_r.
+Qed.
+
+Definition Bezout n m p := exists a, exists b, a*n + b*m == p.
+
+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.
+ rewrite <- H. apply divide_add_r; now apply divide_mul_r.
+Qed.
+
+Lemma gcd_bezout : forall n m p, gcd n m == p -> Bezout n m p.
+Proof.
+ (* First, a version restricted to natural numbers *)
+ assert (aux : forall n, 0<=n -> forall m, 0<=m -> Bezout n m (gcd n m)).
+  intros n Hn; pattern n.
+  apply strong_right_induction with (z:=0); trivial.
+  unfold Bezout. solve_predicate_wd.
+  clear n Hn. intros n Hn IHn.
+  apply le_lteq in Hn; destruct Hn as [Hn|Hn].
+  intros m Hm; pattern m.
+  apply strong_right_induction with (z:=0); 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).
+  apply sub_nonneg; order.
+  now apply lt_sub_pos.
+  exists (a-b). exists b.
+  rewrite gcd_sub_diag_r in EQ. rewrite <- EQ.
+  rewrite mul_sub_distr_r, mul_sub_distr_l.
+  now rewrite add_sub_assoc, add_sub_swap.
+  (* n = m *)
+  rewrite EQ. rewrite gcd_diag_nonneg; trivial.
+  exists 1. exists 0. now nzsimpl.
+  (* m < n *)
+  destruct (IHn m Hm LT n) as (a & b & EQ). order.
+  exists b. exists a. now rewrite gcd_comm, <- EQ, add_comm.
+  (* n = 0 *)
+  intros m Hm. rewrite <- Hn, gcd_0_l_nonneg; trivial.
+  exists 0. exists 1. now nzsimpl.
+ (* Then we relax the positivity condition on n *)
+ assert (aux' : forall n m, 0<=m -> Bezout n m (gcd n m)).
+  intros n m Hm.
+  destruct (le_ge_cases 0 n). now apply aux.
+  assert (Hn' : 0 <= -n) by now apply opp_nonneg_nonpos.
+  destruct (aux (-n) Hn' m Hm) as (a & b & EQ).
+  exists (-a). exists b. now rewrite <- gcd_opp_l, <- EQ, mul_opp_r, mul_opp_l.
+ (* And finally we do the same for m *)
+ intros n m p Hp. rewrite <- Hp; clear Hp.
+ destruct (le_ge_cases 0 m). now apply aux'.
+ assert (Hm' : 0 <= -m) by now apply opp_nonneg_nonpos.
+ destruct (aux' n (-m) Hm') as (a & b & EQ).
+ exists a. exists (-b). now rewrite <- gcd_opp_r, <- EQ, mul_opp_r, mul_opp_l.
+Qed.
+
+Lemma gcd_mul_mono_l :
+  forall n m p, gcd (p * n) (p * m) == abs p * gcd n m.
+Proof.
+ intros n m p.
+ apply gcd_unique.
+ apply mul_nonneg_nonneg; trivial using gcd_nonneg, abs_nonneg.
+ destruct (gcd_divide_l n m) as (q,Hq).
+ rewrite <- Hq at 2. rewrite <- (abs_sgn p) at 2.
+ rewrite mul_shuffle1. apply divide_factor_l.
+ destruct (gcd_divide_r n m) as (q,Hq).
+ rewrite <- Hq at 2. rewrite <- (abs_sgn p) at 2.
+ rewrite mul_shuffle1. apply divide_factor_l.
+ intros q H H'.
+ destruct (gcd_bezout n m (gcd n m) (eq_refl _)) as (a & b & EQ).
+ rewrite <- EQ, <- sgn_abs, mul_add_distr_l. apply divide_add_r.
+ rewrite mul_shuffle2. now apply divide_mul_l.
+ rewrite mul_shuffle2. now apply divide_mul_l.
+Qed.
+
+Lemma gcd_mul_mono_l_nonneg :
+ forall n m p, 0<=p -> gcd (p*n) (p*m) == p * gcd n m.
+Proof.
+ intros. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_l.
+Qed.
+
+Lemma gcd_mul_mono_r :
+ forall n m p, gcd (n * p) (m * p) == gcd n m * abs p.
+Proof.
+ intros n m p. now rewrite !(mul_comm _ p), gcd_mul_mono_l, mul_comm.
+Qed.
+
+Lemma gcd_mul_mono_r_nonneg :
+ forall n m p, 0<=p -> gcd (n*p) (m*p) == gcd n m * p.
+Proof.
+ intros. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_r.
+Qed.
+
+Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p).
+Proof.
+ intros n m p H G.
+ destruct (gcd_bezout n m 1 G) as (a & b & EQ).
+ rewrite <- (mul_1_l p), <- EQ, mul_add_distr_r.
+ apply divide_add_r. rewrite mul_shuffle0. apply divide_factor_r.
+ rewrite <- mul_assoc. now apply divide_mul_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_nonneg, 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 ZGcdProp.
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index d2e962673..6fbf0f23d 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -6,10 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow.
+Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZGcd.
 
 (** This functor summarizes all known facts about Z. *)
 
 Module Type ZProp (Z:ZAxiomsSig) :=
  ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z
- <+ NZSqrt.NZSqrtProp Z Z <+ NZLog.NZLog2Prop Z Z Z.
+ <+ NZSqrt.NZSqrtProp Z Z <+ NZLog.NZLog2Prop Z Z Z <+ ZGcdProp Z.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index b92b303f0..01d36854b 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -10,7 +10,7 @@
 
 
 Require Import ZAxioms ZProperties BinInt Zcompare Zorder ZArith_dec
- Zbool Zeven Zsqrt_def Zpow_def Zlog_def.
+ Zbool Zeven Zsqrt_def Zpow_def Zlog_def Zgcd_def.
 
 Local Open Scope Z_scope.
 
@@ -161,6 +161,15 @@ Definition log2_spec := Zlog2_spec.
 Definition log2_nonpos := Zlog2_nonpos.
 Definition log2 := Zlog2.
 
+(** Gcd *)
+
+Definition gcd_divide_l := Zgcd_divide_l.
+Definition gcd_divide_r := Zgcd_divide_r.
+Definition gcd_greatest := Zgcd_greatest.
+Definition gcd_nonneg := Zgcd_nonneg.
+Definition divide := Zdivide'.
+Definition gcd := Zgcd.
+
 (** We define [eq] only here to avoid refering to this [eq] above. *)
 
 Definition eq := (@eq Z).
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 6689875cb..999e7cd03 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -20,7 +20,7 @@ Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
  spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
- spec_pow spec_log2 spec_even spec_odd
+ spec_pow spec_log2 spec_even spec_odd spec_gcd
  : zsimpl.
 
 Ltac zsimpl := autorewrite with zsimpl.
@@ -349,6 +349,38 @@ Proof.
 intros a b. zify. intros. apply Z_mod_neg; 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_Z z). now zify.
+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.
+
 End ZTypeIsZAxioms.
 
 Module ZType_ZAxioms (Z : ZType)