Library Coq.Numbers.Natural.Abstract.NLcm


Require Import NAxioms NSub NDiv NGcd.

Least Common Multiple

Unlike other functions around, we will define lcm below instead of axiomatizing it. Indeed, there is no "prior art" about lcm in the standard library to be compliant with, and the generic definition of lcm via gcd is quite reasonable.
By the way, we also state here some combined properties of div/mod and gcd.

Module Type NLcmProp
 (Import A : NAxiomsSig')
 (Import B : NSubProp A)
 (Import C : NDivProp A B)
 (Import D : NGcdProp A B).

Divibility and modulo

Lemma mod_divide : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)).

Lemma divide_div_mul_exact : forall a b c, b~=0 -> (b|a) ->
 (c*a)/b == c*(a/b).

Gcd of divided elements, for exact divisions

Lemma gcd_div_factor : forall a b c, c~=0 -> (c|a) -> (c|b) ->
 gcd (a/c) (b/c) == (gcd a b)/c.

Lemma gcd_div_gcd : forall a b g, g~=0 -> g == gcd a b ->
 gcd (a/g) (b/g) == 1.

The following equality is crucial for Euclid algorithm

Lemma gcd_mod : forall a b, b~=0 -> gcd (a mod b) b == gcd b a.

We now define lcm thanks to gcd:
lcm a b = a * (b / gcd a b) = (a / gcd a b) * b = (a*b) / gcd a b
Nota: lcm 0 0 should be 0, which isn't guarantee with the third equation above.

Definition lcm a b := a*(b/gcd a b).

#[global]
Instance lcm_wd : Proper (eq==>eq==>eq) lcm.

Lemma lcm_equiv1 : forall a b, gcd a b ~= 0 ->
  a * (b / gcd a b) == (a*b)/gcd a b.

Lemma lcm_equiv2 : forall a b, gcd a b ~= 0 ->
  (a / gcd a b) * b == (a*b)/gcd a b.

Lemma gcd_div_swap : forall a b,
 (a / gcd a b) * b == a * (b / gcd a b).

Lemma divide_lcm_l : forall a b, (a | lcm a b).

Lemma divide_lcm_r : forall a b, (b | lcm a b).

Lemma divide_div : forall a b c, a~=0 -> (a|b) -> (b|c) -> (b/a|c/a).

Lemma lcm_least : forall a b c,
 (a | c) -> (b | c) -> (lcm a b | c).

Lemma lcm_comm : forall a b, lcm a b == lcm b a.

Lemma lcm_divide_iff : forall n m p,
  (lcm n m | p) <-> (n | p) /\ (m | p).

Lemma lcm_unique : forall n m p,
 0<=p -> (n|p) -> (m|p) ->
 (forall q, (n|q) -> (m|q) -> (p|q)) ->
 lcm n m == p.

Lemma lcm_unique_alt : forall n m p, 0<=p ->
 (forall q, (p|q) <-> (n|q) /\ (m|q)) ->
 lcm n m == p.

Lemma lcm_assoc : forall n m p, lcm n (lcm m p) == lcm (lcm n m) p.

Lemma lcm_0_l : forall n, lcm 0 n == 0.

Lemma lcm_0_r : forall n, lcm n 0 == 0.

Lemma lcm_1_l : forall n, lcm 1 n == n.

Lemma lcm_1_r : forall n, lcm n 1 == n.

Lemma lcm_diag : forall n, lcm n n == n.

Lemma lcm_eq_0 : forall n m, lcm n m == 0 <-> n == 0 \/ m == 0.

Lemma divide_lcm_eq_r : forall n m, (n|m) -> lcm n m == m.

Lemma divide_lcm_iff : forall n m, (n|m) <-> lcm n m == m.

Lemma lcm_mul_mono_l :
  forall n m p, lcm (p * n) (p * m) == p * lcm n m.

Lemma lcm_mul_mono_r :
 forall n m p, lcm (n * p) (m * p) == lcm n m * p.

Lemma gcd_1_lcm_mul : forall n m, n~=0 -> m~=0 ->
 (gcd n m == 1 <-> lcm n m == n*m).

End NLcmProp.