-- The least common multiple: defined from the greatest common divisor by
-- gcd(a, b) · lcm(a, b) = a · b, characterised as the least common multiple,
-- with its units, commutativity, associativity, and behaviour on coprime
-- numbers
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.NumberTheory.LCM
import GCDMore

predicate IsLCM (a b m : Nat) :=
  a ∣ m ∧ b ∣ m ∧ (∀ c, Nat(c) → a ∣ c → b ∣ c → m ∣ c)

theorem IsLCM.intro (a b m : Nat)
  requires left : a ∣ m
  requires right : b ∣ m
  requires least : ∀ c, Nat(c) → a ∣ c → b ∣ c → m ∣ c
  shows IsLCM(a, b, m)
proof
  exact ⟨left, right, least⟩

theorem IsLCM.divides_left (a b m : Nat)
  requires lcm : IsLCM(a, b, m)
  shows a ∣ m
proof
  exact lcm.left

theorem IsLCM.divides_right (a b m : Nat)
  requires lcm : IsLCM(a, b, m)
  shows b ∣ m
proof
  exact lcm.right.left

theorem IsLCM.least (a b m c : Nat)
  requires lcm : IsLCM(a, b, m)
  requires left : a ∣ c
  requires right : b ∣ c
  shows m ∣ c
proof
  exact lcm.right.right with c, left, right

theorem IsLCM.unique (a b m n : Nat)
  requires first : IsLCM(a, b, m)
  requires second : IsLCM(a, b, n)
  shows m = n
proof
  have forward := IsLCM.least at a, b, m, n
    with first, second.left, second.right.left
  have backward := IsLCM.least at a, b, n, m
    with second, first.left, first.right.left
  exact divides.antisymmetric with forward, backward

theorem IsLCM.symmetric (a b m : Nat)
  requires lcm : IsLCM(a, b, m)
  shows IsLCM(b, a, m)
proof
  rcases lcm with ⟨left, right, least⟩
  refine ⟨right, left, _⟩
  intros c cNat first second
  exact least with c, second, first

def lcm (a b : Nat) : Nat := quotientNat(a * b, gcd(a, b))

theorem lcm.natural (a b : Nat)
  shows Nat(lcm(a, b))
proof
  unfold lcm
  exact quotientNat.natural at gcd(a, b), a * b

theorem lcm.zero_left (b : Nat)
  shows lcm(0, b) = 0
proof
  unfold lcm
  have zero : 0 * b = 0 by ring
  rw zero
  simp [quotientNat]

theorem lcm.zero_right (a : Nat)
  shows lcm(a, 0) = 0
proof
  unfold lcm
  have zero : a * 0 = 0 by ring
  rw zero
  simp [quotientNat]

theorem lcm.commutative (a b : Nat)
  shows lcm(a, b) = lcm(b, a)
proof
  unfold lcm
  have commute := gcd.commutative at a, b
  have product : a * b = b * a by ring
  rw [commute, product]
  rfl

theorem gcd.mul_lcm (a b : Nat)
  shows gcd(a, b) * lcm(a, b) = a * b
proof
  have split : gcd(a, b) = 0 ∨ gcd(a, b) ≠ 0 by tauto
  cases split with zero | nonzero
  . have both := gcd.zero_iff at a, b
    have zeros := both.forward with zero
    rcases zeros with ⟨aZero, bZero⟩
    rw [zero, aZero, bZero]
    ring
  . have multiple := gcd.divides_mul at a, b, b
    have equation := divides.quotient_equation at gcd(a, b), a * b
      with nonzero, multiple
    unfold lcm
    cc

theorem lcm.mul_gcd (a b : Nat)
  shows lcm(a, b) * gcd(a, b) = a * b
proof
  have product := gcd.mul_lcm at a, b
  have commute : lcm(a, b) * gcd(a, b) = gcd(a, b) * lcm(a, b) by ring
  rw commute
  exact product

-- The cofactors of a and b against their greatest common divisor are coprime.
theorem gcd.cofactor_coprime (a b p q : Nat)
  requires nonzero : gcd(a, b) ≠ 0
  requires left : gcd(a, b) * p = a
  requires right : gcd(a, b) * q = b
  shows gcd(p, q) = 1
proof
  have distribute := gcd.mul_left_distribute at p, q, gcd(a, b)
  rw [left, right] at distribute
  have products : gcd(a, b) * gcd(p, q) = gcd(a, b) * 1
    have one : gcd(a, b) * 1 = gcd(a, b) by ring
    rw one
    symm
    exact distribute
  exact mul.left_cancel_positive at gcd(p, q), 1, gcd(a, b)
    with nonzero, products

theorem lcm.cofactor_form (a b p q : Nat)
  requires nonzero : gcd(a, b) ≠ 0
  requires left : gcd(a, b) * p = a
  requires right : gcd(a, b) * q = b
  shows lcm(a, b) = gcd(a, b) * p * q
proof
  have product := gcd.mul_lcm at a, b
  have form : gcd(a, b) * lcm(a, b) = gcd(a, b) * (gcd(a, b) * p * q)
    linear_combination product - a * right - (gcd(a, b) * q) * left
  exact mul.left_cancel_positive at lcm(a, b), gcd(a, b) * p * q, gcd(a, b)
    with nonzero, form

theorem lcm.divides_left (a b : Nat)
  shows a ∣ lcm(a, b)
proof
  have split : gcd(a, b) = 0 ∨ gcd(a, b) ≠ 0 by tauto
  cases split with zero | nonzero
  . have both := gcd.zero_iff at a, b
    have zeros := both.forward with zero
    rcases zeros with ⟨aZero, bZero⟩
    rw [aZero, bZero]
    have value := lcm.zero_left at 0
    rw value
    exact divides.reflexive at 0
  . have product := gcd.mul_lcm at a, b
    obtain ⟨k, kNat, equation⟩ := gcd.divides_right at a, b
    have rearranged : gcd(a, b) * lcm(a, b) = gcd(a, b) * (a * k)
      linear_combination product - a * equation
    have cancelled := mul.left_cancel_positive at lcm(a, b), a * k, gcd(a, b)
      with nonzero, rearranged
    witness k
    symm
    exact cancelled

theorem lcm.divides_right (a b : Nat)
  shows b ∣ lcm(a, b)
proof
  have commute := lcm.commutative at a, b
  rw commute
  exact lcm.divides_left at b, a

theorem lcm.least (a b c : Nat)
  requires left : a ∣ c
  requires right : b ∣ c
  shows lcm(a, b) ∣ c
proof
  have split : gcd(a, b) = 0 ∨ gcd(a, b) ≠ 0 by tauto
  cases split with zero | nonzero
  . have both := gcd.zero_iff at a, b
    have zeros := both.forward with zero
    rcases zeros with ⟨aZero, bZero⟩
    rw aZero at left
    rw [aZero, bZero]
    have value := lcm.zero_left at 0
    rw value
    exact left
  . obtain ⟨p, pNat, pEquation⟩ := gcd.divides_left at a, b
    obtain ⟨q, qNat, qEquation⟩ := gcd.divides_right at a, b
    have cofactor := gcd.cofactor_coprime at a, b, p, q
      with nonzero, pEquation, qEquation
    have form := lcm.cofactor_form at a, b, p, q
      with nonzero, pEquation, qEquation
    obtain ⟨k, kNat, kEquation⟩ := left
    have scaled : gcd(a, b) * q ∣ gcd(a, b) * (p * k)
      rw qEquation
      have shape : gcd(a, b) * (p * k) = c
        linear_combination k * pEquation + kEquation
      rw shape
      exact right
    have cancelled := divides.mul_cancel_left at gcd(a, b), q, p * k
      with nonzero
    have reduced := cancelled.forward with scaled
    have dividesK := coprime.cancel at p, q, k with cofactor, reduced
    obtain ⟨m, mNat, mEquation⟩ := dividesK
    witness m
    rw form
    linear_combination (q * m) * pEquation + a * mEquation + kEquation

theorem lcm.correct (a b : Nat)
  shows IsLCM(a, b, lcm(a, b))
proof
  have left := lcm.divides_left at a, b
  have right := lcm.divides_right at a, b
  refine ⟨left, right, _⟩
  intros c cNat first second
  exact lcm.least at a, b, c with first, second

theorem lcm.unique (a b m : Nat)
  requires certificate : IsLCM(a, b, m)
  shows lcm(a, b) = m
proof
  have correct := lcm.correct at a, b
  exact IsLCM.unique with correct, certificate

theorem lcm.divides_iff (a b c : Nat)
  shows lcm(a, b) ∣ c ↔ a ∣ c ∧ b ∣ c
proof
  constructor
  . intro h
    have left := lcm.divides_left at a, b
    have right := lcm.divides_right at a, b
    constructor
    . exact divides.transitive at a, lcm(a, b), c with left, h
    . exact divides.transitive at b, lcm(a, b), c with right, h
  . intro both
    rcases both with ⟨left, right⟩
    exact lcm.least at a, b, c with left, right

theorem lcm.of_divides (a b : Nat)
  requires hab : a ∣ b
  shows lcm(a, b) = b
proof
  have reflexive := divides.reflexive at b
  have certificate : IsLCM(a, b, b)
    refine ⟨hab, reflexive, _⟩
    intros c cNat first second
    exact second
  exact lcm.unique with certificate

theorem lcm.of_divides_right (a b : Nat)
  requires hba : b ∣ a
  shows lcm(a, b) = a
proof
  have commute := lcm.commutative at a, b
  rw commute
  exact lcm.of_divides at b, a with hba

theorem lcm.one_left (a : Nat)
  shows lcm(1, a) = a
proof
  have one := one.divides at a
  exact lcm.of_divides with one

theorem lcm.one_right (a : Nat)
  shows lcm(a, 1) = a
proof
  have one := one.divides at a
  exact lcm.of_divides_right with one

theorem lcm.self (a : Nat)
  shows lcm(a, a) = a
proof
  have reflexive := divides.reflexive at a
  exact lcm.of_divides with reflexive

theorem lcm.divides_mul (a b : Nat)
  shows lcm(a, b) ∣ a * b
proof
  have left := divides.mul_left_self at a, b
  have right := divides.mul_right_self at b, a
  exact lcm.least at a, b, a * b with left, right

theorem lcm.zero_iff (a b : Nat)
  shows lcm(a, b) = 0 ↔ a = 0 ∨ b = 0
proof
  constructor
  . intro zero
    have product := gcd.mul_lcm at a, b
    rw zero at product
    have vanish : a * b = 0
      rw ← product
      ring
    have split := mul.eq_zero_iff at a, b
    exact split.forward with vanish
  . intro split
    cases split with aZero | bZero
    . rw aZero
      exact lcm.zero_left at b
    . rw bZero
      exact lcm.zero_right at a

theorem lcm.nonzero (a b : Nat)
  requires left : a ≠ 0
  requires right : b ≠ 0
  shows lcm(a, b) ≠ 0
proof
  intro zero
  have split := lcm.zero_iff at a, b
  have alternatives := split.forward with zero
  cases alternatives with aZero | bZero
  . exact left with aZero
  . exact right with bZero

theorem lcm.positive (a b : Nat)
  requires left : a ≠ 0
  requires right : b ≠ 0
  shows 0 < lcm(a, b)
proof
  have distinct := lcm.nonzero with left, right
  exact Less.positive_of_ne_zero with distinct

theorem lcm.ge_left (a b : Nat)
  requires left : a ≠ 0
  requires right : b ≠ 0
  shows a ≤ lcm(a, b)
proof
  have multiple := lcm.divides_left at a, b
  have distinct := lcm.nonzero with left, right
  exact divides.le at a, lcm(a, b) with multiple, distinct

theorem lcm.ge_right (a b : Nat)
  requires left : a ≠ 0
  requires right : b ≠ 0
  shows b ≤ lcm(a, b)
proof
  have multiple := lcm.divides_right at a, b
  have distinct := lcm.nonzero with left, right
  exact divides.le at b, lcm(a, b) with multiple, distinct

theorem lcm.le_mul (a b : Nat)
  requires left : a ≠ 0
  requires right : b ≠ 0
  shows lcm(a, b) ≤ a * b
proof
  have multiple := lcm.divides_mul at a, b
  have distinct := mul.nonzero with left, right
  exact divides.le at lcm(a, b), a * b with multiple, distinct

theorem lcm.coprime (a b : Nat)
  requires coprimeAB : gcd(a, b) = 1
  shows lcm(a, b) = a * b
proof
  have product := gcd.mul_lcm at a, b
  rw coprimeAB at product
  have one : 1 * lcm(a, b) = lcm(a, b) by ring
  rw one at product
  exact product

theorem lcm.eq_mul_iff (a b : Nat)
  requires left : a ≠ 0
  requires right : b ≠ 0
  shows lcm(a, b) = a * b ↔ gcd(a, b) = 1
proof
  constructor
  . intro same
    have product := gcd.mul_lcm at a, b
    rw same at product
    have distinct := mul.nonzero with left, right
    have unit : gcd(a, b) * (a * b) = 1 * (a * b)
      rw product
      ring
    have swapLeft : gcd(a, b) * (a * b) = (a * b) * gcd(a, b) by ring
    have swapRight : 1 * (a * b) = (a * b) * 1 by ring
    rw [swapLeft, swapRight] at unit
    exact mul.left_cancel_positive at gcd(a, b), 1, a * b with distinct, unit
  . intro coprimeAB
    exact lcm.coprime with coprimeAB

theorem gcd.divides_lcm (a b : Nat)
  shows gcd(a, b) ∣ lcm(a, b)
proof
  have left := gcd.divides_left at a, b
  have multiple := lcm.divides_left at a, b
  exact divides.transitive at gcd(a, b), a, lcm(a, b) with left, multiple

theorem lcm.associative (a b c : Nat)
  shows lcm(lcm(a, b), c) = lcm(a, lcm(b, c))
proof
  have innerLeft := lcm.divides_left at a, b
  have innerRight := lcm.divides_right at a, b
  have outerLeft := lcm.divides_left at lcm(a, b), c
  have outerRight := lcm.divides_right at lcm(a, b), c
  have dividesA := divides.transitive at a, lcm(a, b), lcm(lcm(a, b), c)
    with innerLeft, outerLeft
  have dividesB := divides.transitive at b, lcm(a, b), lcm(lcm(a, b), c)
    with innerRight, outerLeft
  have dividesBC := lcm.least at b, c, lcm(lcm(a, b), c)
    with dividesB, outerRight
  have certificate : IsLCM(a, lcm(b, c), lcm(lcm(a, b), c))
    refine ⟨dividesA, dividesBC, _⟩
    intros d dNat dA dBC
    have left := lcm.divides_left at b, c
    have right := lcm.divides_right at b, c
    have dB := divides.transitive at b, lcm(b, c), d with left, dBC
    have dC := divides.transitive at c, lcm(b, c), d with right, dBC
    have dAB := lcm.least at a, b, d with dA, dB
    exact lcm.least at lcm(a, b), c, d with dAB, dC
  symm
  exact lcm.unique with certificate

theorem lcm.mul_right_distribute (a b c : Nat)
  shows lcm(a * c, b * c) = lcm(a, b) * c
proof
  have split : c = 0 ∨ c ≠ 0 by tauto
  cases split with zero | nonzero
  . rw zero
    have left : a * 0 = 0 by ring
    have right : b * 0 = 0 by ring
    rw [left, right]
    have value := lcm.zero_left at 0
    rw value
    ring
  . have innerLeft := lcm.divides_left at a, b
    have innerRight := lcm.divides_right at a, b
    have reflexive := divides.reflexive at c
    have scaledLeft := divides.mul_mono at a, lcm(a, b), c, c
      with innerLeft, reflexive
    have scaledRight := divides.mul_mono at b, lcm(a, b), c, c
      with innerRight, reflexive
    have certificate : IsLCM(a * c, b * c, lcm(a, b) * c)
      refine ⟨scaledLeft, scaledRight, _⟩
      intros d dNat dA dB
      have cDivides := divides.of_mul_right at a, c, d with dA
      obtain ⟨e, eNat, eEquation⟩ := cDivides
      have shapeA : a * c ∣ e * c
        have commute : e * c = c * e by ring
        rw [commute, eEquation]
        exact dA
      have shapeB : b * c ∣ e * c
        have commute : e * c = c * e by ring
        rw [commute, eEquation]
        exact dB
      have cancelA := divides.mul_cancel_right at c, a, e with nonzero
      have cancelB := divides.mul_cancel_right at c, b, e with nonzero
      have eA := cancelA.forward with shapeA
      have eB := cancelB.forward with shapeB
      have least := lcm.least at a, b, e with eA, eB
      have scaled := divides.mul_mono at lcm(a, b), e, c, c
        with least, reflexive
      have commute : e * c = c * e by ring
      rw [commute, eEquation] at scaled
      exact scaled
    exact lcm.unique with certificate

theorem lcm.mul_left_distribute (a b c : Nat)
  shows lcm(c * a, c * b) = c * lcm(a, b)
proof
  have left : c * a = a * c by ring
  have right : c * b = b * c by ring
  have product : lcm(a, b) * c = c * lcm(a, b) by ring
  rw [left, right, ← product]
  exact lcm.mul_right_distribute at a, b, c