Library Coq.Numbers.NatInt.NZGcd


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.

Lemma divide_1_l : forall n, (1 | n).

Lemma divide_0_r : forall n, (n | 0).

Hint Rewrite divide_1_l divide_0_r : nz.

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 := 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.

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.