Library Coq.Numbers.NatInt.NZGcd
Greatest Common Divisor
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.
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
Results concerning divisibility
Instance divide_wd : Proper (eq==>eq==>iff) divide.
Lemma divide_1_l : forall n, (1 | n).
Lemma divide_0_r : forall n, (n | 0).
Lemma divide_0_l : forall n, (0 | n) -> n==0.
Lemma eq_mul_1_nonneg : forall n m,
0<=n -> n*m == 1 -> n==1 /\ m==1.
Lemma eq_mul_1_nonneg' : forall n m,
0<=m -> n*m == 1 -> n==1 /\ m==1.
Lemma divide_1_r_nonneg : forall n, 0<=n -> (n | 1) -> n==1.
Lemma divide_refl : forall n, (n | n).
Lemma divide_trans : forall n m p, (n | m) -> (m | p) -> (n | p).
Instance divide_reflexive : Reflexive divide | 5 := divide_refl.
Instance divide_transitive : Transitive divide | 5 := 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.
Lemma mul_divide_mono_l : forall n m p, (n | m) -> (p * n | p * m).
Lemma mul_divide_mono_r : forall n m p, (n | m) -> (n * p | m * p).
Lemma mul_divide_cancel_l : forall n m p, p ~= 0 ->
((p * n | p * m) <-> (n | m)).
Lemma mul_divide_cancel_r : forall n m p, p ~= 0 ->
((n * p | m * p) <-> (n | m)).
Lemma divide_add_r : forall n m p, (n | m) -> (n | p) -> (n | m + p).
Lemma divide_mul_l : forall n m p, (n | m) -> (n | m * p).
Lemma divide_mul_r : forall n m p, (n | p) -> (n | m * p).
Lemma divide_factor_l : forall n m, (n | n * m).
Lemma divide_factor_r : forall n m, (n | m * n).
Lemma divide_pos_le : forall n m, 0 < m -> (n | m) -> n <= m.
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.
Instance gcd_wd : Proper (eq==>eq==>eq) gcd.
Lemma gcd_divide_iff : forall n m p,
(p | gcd n m) <-> (p | n) /\ (p | m).
Lemma gcd_unique_alt : forall n m p, 0<=p ->
(forall q, (q|p) <-> (q|n) /\ (q|m)) ->
gcd n m == p.
Lemma gcd_comm : forall n m, gcd n m == gcd m n.
Lemma gcd_assoc : forall n m p, gcd n (gcd m p) == gcd (gcd n m) p.
Lemma gcd_0_l_nonneg : forall n, 0<=n -> gcd 0 n == n.
Lemma gcd_0_r_nonneg : forall n, 0<=n -> gcd n 0 == n.
Lemma gcd_1_l : forall n, gcd 1 n == 1.
Lemma gcd_1_r : forall n, gcd n 1 == 1.
Lemma gcd_diag_nonneg : forall n, 0<=n -> gcd n n == n.
Lemma gcd_eq_0_l : forall n m, gcd n m == 0 -> n == 0.
Lemma gcd_eq_0_r : forall n m, gcd n m == 0 -> m == 0.
Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0.
Lemma gcd_mul_diag_l : forall n m, 0<=n -> gcd n (n*m) == n.
Lemma divide_gcd_iff : forall n m, 0<=n -> ((n|m) <-> gcd n m == n).
End NZGcdProp.