diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZGcd.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZGcd.v | 307 |
1 files changed, 307 insertions, 0 deletions
diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v new file mode 100644 index 00000000..f72023d9 --- /dev/null +++ b/theories/Numbers/NatInt/NZGcd.v @@ -0,0 +1,307 @@ +(************************************************************************) +(* 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). + Parameter Inline gcd : t -> t -> t. +End Gcd. + +Module Type NZGcdSpec (A : NZOrdAxiomsSig')(B : Gcd A). + Import A B. + Definition divide n m := exists p, m == p*n. + 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. + le_elim Hn. + destruct (lt_ge_cases m 0) as [Hm|Hm]. + generalize (mul_pos_neg n m Hn Hm). order'. + le_elim Hm. + apply le_succ_l in Hn. rewrite <- one_succ in Hn. + le_elim 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 eq_mul_1_nonneg' : forall n m, + 0<=m -> n*m == 1 -> n==1 /\ m==1. +Proof. + intros n m Hm H. rewrite mul_comm in H. + now apply and_comm, eq_mul_1_nonneg. +Qed. + +Lemma divide_1_r_nonneg : forall n, 0<=n -> (n | 1) -> n==1. +Proof. + intros n Hn (m,Hm). symmetry in Hm. + now apply (eq_mul_1_nonneg' m n). +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 (r*q). + now rewrite Hr, Hq, mul_assoc. +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). + le_elim Hn. + destruct (lt_ge_cases q 0) as [Hq'|Hq']. + generalize (mul_neg_pos q n Hq' Hn). order. + rewrite Hq, mul_assoc in Hr. symmetry in Hr. + apply mul_id_l in Hr; [|order]. + destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial. + now rewrite H, mul_1_l in Hq. + rewrite <- Hn, mul_0_r 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_shuffle3, 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_assoc, 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_shuffle3, 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_r, 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_shuffle0, 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_neg_pos q n Hq' Hn). order. + le_elim Hq'. + rewrite <- (mul_1_l n) at 1. apply mul_le_mono_pos_r; trivial. + now rewrite one_succ, le_succ_l. + rewrite <- Hq', mul_0_l 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. + rewrite mul_comm. now apply gcd_mul_diag_l. + intros EQ. rewrite <- EQ. apply gcd_divide_r. +Qed. + +End NZGcdProp. |