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

diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v
new file mode 100644
index 000000000..9c022646b
--- /dev/null
+++ b/theories/Numbers/NatInt/NZGcd.v
@@ -0,0 +1,299 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Greatest Common Divisor *)
+
+Require Import NZAxioms NZMulOrder.
+
+(** Interface of a gcd function, then its specification on naturals *)
+
+Module Type Gcd (Import A : Typ).
+ Parameters Inline gcd : t -> t -> t.
+End Gcd.
+
+Module Type NZGcdSpec (A : NZOrdAxiomsSig')(B : Gcd A).
+ Import A B.
+ Definition divide n m := exists p, n*p == m.
+ Local Notation "( n | m )" := (divide n m) (at level 0).
+ Axiom gcd_divide_l : forall n m, (gcd n m | n).
+ Axiom gcd_divide_r : forall n m, (gcd n m | m).
+ Axiom gcd_greatest : forall n m p, (p | n) -> (p | m) -> (p | gcd n m).
+ Axiom gcd_nonneg : forall n m, 0 <= gcd n m.
+End NZGcdSpec.
+
+Module Type DivideNotation (A:NZOrdAxiomsSig')(B:Gcd A)(C:NZGcdSpec A B).
+ Import A B C.
+ Notation "( n | m )" := (divide n m) (at level 0).
+End DivideNotation.
+
+Module Type NZGcd (A : NZOrdAxiomsSig) := Gcd A <+ NZGcdSpec A.
+Module Type NZGcd' (A : NZOrdAxiomsSig) :=
+ Gcd A <+ NZGcdSpec A <+ DivideNotation A.
+
+(** Derived properties of gcd *)
+
+Module NZGcdProp
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZGcd' A)
+ (Import C : NZMulOrderProp A).
+
+(** Results concerning divisibility*)
+
+Instance divide_wd : Proper (eq==>eq==>iff) divide.
+Proof.
+ unfold divide. intros x x' Hx y y' Hy.
+ setoid_rewrite Hx. setoid_rewrite Hy. easy.
+Qed.
+
+Lemma divide_1_l : forall n, (1 | n).
+Proof.
+ intros n. exists n. now nzsimpl.
+Qed.
+
+Lemma divide_0_r : forall n, (n | 0).
+Proof.
+ intros n. exists 0. now nzsimpl.
+Qed.
+
+Hint Rewrite divide_1_l divide_0_r : nz.
+
+Lemma divide_0_l : forall n, (0 | n) -> n==0.
+Proof.
+ intros n (m,Hm). revert Hm. now nzsimpl.
+Qed.
+
+Lemma eq_mul_1_nonneg : forall n m,
+ 0<=n -> n*m == 1 -> n==1 /\ m==1.
+Proof.
+ intros n m Hn H.
+ apply le_lteq in Hn. destruct Hn as [Hn|Hn].
+ destruct (lt_ge_cases m 0) as [Hm|Hm].
+ generalize (mul_pos_neg n m Hn Hm). order'.
+ apply le_lteq in Hm. destruct Hm as [Hm|Hm].
+ apply le_succ_l in Hn. rewrite <- one_succ in Hn.
+ apply le_lteq in Hn. destruct Hn as [Hn|Hn].
+ generalize (lt_1_mul_pos n m Hn Hm). order.
+ rewrite <- Hn, mul_1_l in H. now split.
+ rewrite <- Hm, mul_0_r in H. order'.
+ rewrite <- Hn, mul_0_l in H. order'.
+Qed.
+
+Lemma divide_1_r_nonneg : forall n, 0<=n -> (n | 1) -> n==1.
+Proof.
+ intros n Hn (m,Hm). now apply (eq_mul_1_nonneg n m).
+Qed.
+
+Lemma divide_refl : forall n, (n | n).
+Proof.
+ intros n. exists 1. now nzsimpl.
+Qed.
+
+Lemma divide_trans : forall n m p, (n | m) -> (m | p) -> (n | p).
+Proof.
+ intros n m p (q,Hq) (r,Hr). exists (q*r).
+ now rewrite mul_assoc, Hq.
+Qed.
+
+Instance divide_reflexive : Reflexive divide := divide_refl.
+Instance divide_transitive : Transitive divide := divide_trans.
+
+(** Due to sign, no general antisymmetry result *)
+
+Lemma divide_antisym_nonneg : forall n m,
+ 0<=n -> 0<=m -> (n | m) -> (m | n) -> n == m.
+Proof.
+ intros n m Hn Hm (q,Hq) (r,Hr).
+ apply le_lteq in Hn. destruct Hn as [Hn|Hn].
+ destruct (lt_ge_cases q 0) as [Hq'|Hq'].
+ generalize (mul_pos_neg n q Hn Hq'). order.
+ rewrite <- Hq, <- mul_assoc in Hr.
+ apply mul_id_r in Hr; [|order].
+ destruct (eq_mul_1_nonneg q r) as [H _]; trivial.
+ now rewrite H, mul_1_r in Hq.
+ rewrite <- Hn, mul_0_l in Hq. now rewrite <- Hn.
+Qed.
+
+Lemma mul_divide_mono_l : forall n m p, (n | m) -> (p * n | p * m).
+Proof.
+ intros n m p (q,Hq). exists q. now rewrite <- mul_assoc, Hq.
+Qed.
+
+Lemma mul_divide_mono_r : forall n m p, (n | m) -> (n * p | m * p).
+Proof.
+ intros n m p (q,Hq). exists q. now rewrite mul_shuffle0, Hq.
+Qed.
+
+Lemma mul_divide_cancel_l : forall n m p, p ~= 0 ->
+ ((p * n | p * m) <-> (n | m)).
+Proof.
+ intros n m p Hp. split.
+ intros (q,Hq). exists q. now rewrite <- mul_assoc, mul_cancel_l in Hq.
+ apply mul_divide_mono_l.
+Qed.
+
+Lemma mul_divide_cancel_r : forall n m p, p ~= 0 ->
+ ((n * p | m * p) <-> (n | m)).
+Proof.
+ intros. rewrite 2 (mul_comm _ p). now apply mul_divide_cancel_l.
+Qed.
+
+Lemma divide_add_r : forall n m p, (n | m) -> (n | p) -> (n | m + p).
+Proof.
+ intros n m p (q,Hq) (r,Hr). exists (q+r).
+ now rewrite mul_add_distr_l, Hq, Hr.
+Qed.
+
+Lemma divide_mul_l : forall n m p, (n | m) -> (n | m * p).
+Proof.
+ intros n m p (q,Hq). exists (q*p). now rewrite mul_assoc, Hq.
+Qed.
+
+Lemma divide_mul_r : forall n m p, (n | p) -> (n | m * p).
+Proof.
+ intros n m p. rewrite mul_comm. apply divide_mul_l.
+Qed.
+
+Lemma divide_factor_l : forall n m, (n | n * m).
+Proof.
+ intros. apply divide_mul_l, divide_refl.
+Qed.
+
+Lemma divide_factor_r : forall n m, (n | m * n).
+Proof.
+ intros. apply divide_mul_r, divide_refl.
+Qed.
+
+Lemma divide_pos_le : forall n m, 0 < m -> (n | m) -> n <= m.
+Proof.
+ intros n m Hm (q,Hq).
+ destruct (le_gt_cases n 0) as [Hn|Hn]. order.
+ rewrite <- Hq.
+ destruct (lt_ge_cases q 0) as [Hq'|Hq'].
+ generalize (mul_pos_neg n q Hn Hq'). order.
+ apply le_lteq in Hq'. destruct Hq' as [Hq'|Hq'].
+ rewrite <- (mul_1_r n) at 1. apply mul_le_mono_pos_l; trivial.
+ now rewrite one_succ, le_succ_l.
+ rewrite <- Hq', mul_0_r in Hq. order.
+Qed.
+
+(** Basic properties of gcd *)
+
+Lemma gcd_unique : forall n m p,
+ 0<=p -> (p|n) -> (p|m) ->
+ (forall q, (q|n) -> (q|m) -> (q|p)) ->
+ gcd n m == p.
+Proof.
+ intros n m p Hp Hn Hm H.
+ apply divide_antisym_nonneg; trivial. apply gcd_nonneg.
+ apply H. apply gcd_divide_l. apply gcd_divide_r.
+ now apply gcd_greatest.
+Qed.
+
+Instance gcd_wd : Proper (eq==>eq==>eq) gcd.
+Proof.
+ intros x x' Hx y y' Hy.
+ apply gcd_unique.
+ apply gcd_nonneg.
+ rewrite Hx. apply gcd_divide_l.
+ rewrite Hy. apply gcd_divide_r.
+ intro. rewrite Hx, Hy. apply gcd_greatest.
+Qed.
+
+Lemma gcd_divide_iff : forall n m p,
+  (p | gcd n m) <-> (p | n) /\ (p | m).
+Proof.
+ intros. split. split.
+ transitivity (gcd n m); trivial using gcd_divide_l.
+ transitivity (gcd n m); trivial using gcd_divide_r.
+ intros (H,H'). now apply gcd_greatest.
+Qed.
+
+Lemma gcd_unique_alt : forall n m p, 0<=p ->
+ (forall q, (q|p) <-> (q|n) /\ (q|m)) ->
+ gcd n m == p.
+Proof.
+ intros n m p Hp H.
+ apply gcd_unique; trivial.
+ apply -> H. apply divide_refl.
+ apply -> H. apply divide_refl.
+ intros. apply H. now split.
+Qed.
+
+Lemma gcd_comm : forall n m, gcd n m == gcd m n.
+Proof.
+ intros. apply gcd_unique_alt; try apply gcd_nonneg.
+ intros. rewrite and_comm. apply gcd_divide_iff.
+Qed.
+
+Lemma gcd_assoc : forall n m p, gcd n (gcd m p) == gcd (gcd n m) p.
+Proof.
+ intros. apply gcd_unique_alt; try apply gcd_nonneg.
+ intros. now rewrite !gcd_divide_iff, and_assoc.
+Qed.
+
+Lemma gcd_0_l_nonneg : forall n, 0<=n -> gcd 0 n == n.
+Proof.
+ intros. apply gcd_unique; trivial.
+ apply divide_0_r.
+ apply divide_refl.
+Qed.
+
+Lemma gcd_0_r_nonneg : forall n, 0<=n -> gcd n 0 == n.
+Proof.
+ intros. now rewrite gcd_comm, gcd_0_l_nonneg.
+Qed.
+
+Lemma gcd_1_l : forall n, gcd 1 n == 1.
+Proof.
+ intros. apply gcd_unique; trivial using divide_1_l, le_0_1.
+Qed.
+
+Lemma gcd_1_r : forall n, gcd n 1 == 1.
+Proof.
+ intros. now rewrite gcd_comm, gcd_1_l.
+Qed.
+
+Lemma gcd_diag_nonneg : forall n, 0<=n -> gcd n n == n.
+Proof.
+ intros. apply gcd_unique; trivial using divide_refl.
+Qed.
+
+Lemma gcd_eq_0_l : forall n m, gcd n m == 0 -> n == 0.
+Proof.
+ intros.
+ generalize (gcd_divide_l n m). rewrite H. apply divide_0_l.
+Qed.
+
+Lemma gcd_eq_0_r : forall n m, gcd n m == 0 -> m == 0.
+Proof.
+ intros. apply gcd_eq_0_l with n. now rewrite gcd_comm.
+Qed.
+
+Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0.
+Proof.
+ intros. split. split.
+ now apply gcd_eq_0_l with m.
+ now apply gcd_eq_0_r with n.
+ intros (EQ,EQ'). rewrite EQ, EQ'. now apply gcd_0_r_nonneg.
+Qed.
+
+Lemma gcd_mul_diag_l : forall n m, 0<=n -> gcd n (n*m) == n.
+Proof.
+ intros n m Hn. apply gcd_unique_alt; trivial.
+ intros q. split. split; trivial. now apply divide_mul_l.
+ now destruct 1.
+Qed.
+
+Lemma divide_gcd_iff : forall n m, 0<=n -> ((n|m) <-> gcd n m == n).
+Proof.
+ intros n m Hn. split. intros (q,Hq). rewrite <- Hq.
+ now apply gcd_mul_diag_l.
+ intros EQ. rewrite <- EQ. apply gcd_divide_r.
+Qed.
+
+End NZGcdProp.