-- Further laws of the greatest common divisor: units and self, order bounds,
-- shifting by multiples, subtraction, distributivity over a common factor,
-- associativity, consecutive numbers, and coprimality under products and
-- powers
-- 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.GCDMore
import CoprimeCancel
import DivisibilityMore

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

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

theorem gcd.one_right (a : Nat)
  shows gcd(a, 1) = 1
proof
  have commute := gcd.commutative at a, 1
  rw commute
  exact gcd.one_left at a

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

theorem gcd.le_left (a b : Nat)
  requires nonzero : a ≠ 0
  shows gcd(a, b) ≤ a
proof
  have left := gcd.divides_left at a, b
  exact divides.le at gcd(a, b), a with left, nonzero

theorem gcd.le_right (a b : Nat)
  requires nonzero : b ≠ 0
  shows gcd(a, b) ≤ b
proof
  have right := gcd.divides_right at a, b
  exact divides.le at gcd(a, b), b with right, nonzero

theorem gcd.nonzero (a b : Nat)
  requires nonzero : a ≠ 0
  shows gcd(a, b) ≠ 0
proof
  intro zero
  have both := gcd.zero_iff at a, b
  have zeros := both.forward with zero
  exact nonzero with zeros.left

theorem gcd.nonzero_right (a b : Nat)
  requires nonzero : b ≠ 0
  shows gcd(a, b) ≠ 0
proof
  intro zero
  have both := gcd.zero_iff at a, b
  have zeros := both.forward with zero
  exact nonzero with zeros.right

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

theorem gcd.greatest_le (a b d : Nat)
  requires nonzero : a ≠ 0
  requires left : d ∣ a
  requires right : d ∣ b
  shows d ≤ gcd(a, b)
proof
  have common := gcd.greatest with left, right
  have distinct := gcd.nonzero at a, b with nonzero
  exact divides.le at d, gcd(a, b) with common, distinct

theorem gcd.divides_add (a b : Nat)
  shows gcd(a, b) ∣ a + b
proof
  have left := gcd.divides_left at a, b
  have right := gcd.divides_right at a, b
  exact divides.add at gcd(a, b), a, b with left, right

theorem gcd.divides_mul (a b c : Nat)
  shows gcd(a, b) ∣ a * c
proof
  have left := gcd.divides_left at a, b
  exact divides.multiply_right at gcd(a, b), a, c with left

theorem gcd.add_left (a b : Nat)
  shows gcd(a + b, b) = gcd(a, b)
proof
  have correct := gcd.correct at a, b
  have certificate := IsGCD.add_right_iff at a, b, gcd(a, b)
  have shifted := certificate.backward with correct
  exact gcd.unique with shifted

theorem gcd.add_left_swap (a b : Nat)
  shows gcd(b + a, b) = gcd(a, b)
proof
  have commute : b + a = a + b by ring
  rw commute
  exact gcd.add_left at a, b

theorem gcd.add_right (a b : Nat)
  shows gcd(a, a + b) = gcd(a, b)
proof
  have first := gcd.commutative at a, a + b
  have second := gcd.add_left_swap at b, a
  have third := gcd.commutative at b, a
  rw [first, second, third]
  rfl

theorem gcd.add_right_swap (a b : Nat)
  shows gcd(a, b + a) = gcd(a, b)
proof
  have commute : b + a = a + b by ring
  rw commute
  exact gcd.add_right at a, b

theorem gcd.add_mul_left (a b k : Nat)
  shows gcd(a + k * b, b) = gcd(a, b)
proof
  have correct := gcd.correct at a, b
  have swapped := IsGCD.symmetric with correct
  have equation : a + k * b = b * k + a by ring
  have certificate := IsGCD.euclidean_iff at a + k * b, b, k, a, gcd(a, b)
    with equation
  have shifted := certificate.backward with swapped
  exact gcd.unique with shifted

theorem gcd.add_mul_right (a b k : Nat)
  shows gcd(a, b + k * a) = gcd(a, b)
proof
  have first := gcd.commutative at a, b + k * a
  have second := gcd.add_mul_left at b, a, k
  have third := gcd.commutative at b, a
  rw [first, second, third]
  rfl

theorem gcd.sub_left (a b : Nat)
  requires below : b ≤ a
  shows gcd(a - b, b) = gcd(a, b)
proof
  have split := sub.add_cancel at a, b with below
  have shifted := gcd.add_left at a - b, b
  rw split at shifted
  symm
  exact shifted

theorem gcd.sub_right (a b : Nat)
  requires below : b ≤ a
  shows gcd(b, a - b) = gcd(a, b)
proof
  have first := gcd.commutative at b, a - b
  have second := gcd.sub_left at a, b with below
  rw [first, second]
  rfl

theorem gcd.eq_left_iff (a b : Nat)
  shows gcd(a, b) = a ↔ a ∣ b
proof
  constructor
  . intro same
    have right := gcd.divides_right at a, b
    rw same at right
    exact right
  . intro hab
    exact gcd.of_divides with hab

theorem gcd.eq_right_iff (a b : Nat)
  shows gcd(a, b) = b ↔ b ∣ a
proof
  have commute := gcd.commutative at a, b
  rw commute
  exact gcd.eq_left_iff at b, a

theorem gcd.mul_left_self (a b : Nat)
  shows gcd(a, a * b) = a
proof
  have factor := divides.mul_left_self at a, b
  exact gcd.of_divides with factor

theorem gcd.mul_right_self (a b : Nat)
  shows gcd(a, b * a) = a
proof
  have factor := divides.mul_right_self at a, b
  exact gcd.of_divides with factor

theorem gcd.mul_self_left (a b : Nat)
  shows gcd(a * b, a) = a
proof
  have commute := gcd.commutative at a * b, a
  rw commute
  exact gcd.mul_left_self at a, b

theorem gcd.idempotent_left (a b : Nat)
  shows gcd(gcd(a, b), b) = gcd(a, b)
proof
  have right := gcd.divides_right at a, b
  exact gcd.of_divides with right

theorem gcd.idempotent_right (a b : Nat)
  shows gcd(a, gcd(a, b)) = gcd(a, b)
proof
  have commute := gcd.commutative at a, gcd(a, b)
  rw commute
  have left := gcd.divides_left at a, b
  exact gcd.of_divides with left

theorem gcd.consecutive (n : Nat)
  shows gcd(n, n + 1) = 1
proof
  have shifted := gcd.add_right at n, 1
  rw shifted
  exact gcd.one_right at n

theorem gcd.consecutive_left (n : Nat)
  shows gcd(n + 1, n) = 1
proof
  have commute := gcd.commutative at n + 1, n
  rw commute
  exact gcd.consecutive at n

theorem gcd.associative (a b c : Nat)
  shows gcd(gcd(a, b), c) = gcd(a, gcd(b, c))
proof
  have innerLeft := gcd.divides_left at a, b
  have innerRight := gcd.divides_right at a, b
  have outerLeft := gcd.divides_left at gcd(a, b), c
  have outerRight := gcd.divides_right at gcd(a, b), c
  have dividesA := divides.transitive at gcd(gcd(a, b), c), gcd(a, b), a
    with outerLeft, innerLeft
  have dividesB := divides.transitive at gcd(gcd(a, b), c), gcd(a, b), b
    with outerLeft, innerRight
  have dividesBC := gcd.greatest at b, c, gcd(gcd(a, b), c)
    with dividesB, outerRight
  have certificate : IsGCD(a, gcd(b, c), gcd(gcd(a, b), c))
    apply IsGCD.intro
    . exact dividesA
    . exact dividesBC
    . intros d dNat dA dBC
      have left := gcd.divides_left at b, c
      have right := gcd.divides_right at b, c
      have dB := divides.transitive at d, gcd(b, c), b with dBC, left
      have dC := divides.transitive at d, gcd(b, c), c with dBC, right
      have dAB := gcd.greatest at a, b, d with dA, dB
      exact gcd.greatest at gcd(a, b), c, d with dAB, dC
  symm
  exact gcd.unique with certificate

-- A common factor comes out of the greatest common divisor; the greatest
-- property passes through Bézout's identity over the integers.
theorem gcd.mul_right_distribute (a b c : Nat)
  shows gcd(a * c, b * c) = gcd(a, b) * c
proof
  have left := gcd.divides_left at a, b
  have right := gcd.divides_right at a, b
  have reflexive := divides.reflexive at c
  have scaledLeft := divides.mul_mono at gcd(a, b), a, c, c with left, reflexive
  have scaledRight := divides.mul_mono at gcd(a, b), b, c, c
    with right, reflexive
  have certificate : IsGCD(a * c, b * c, gcd(a, b) * c)
    apply IsGCD.intro
    . exact scaledLeft
    . exact scaledRight
    . intros d dNat dA dB
      obtain ⟨u, uInteger, v, vInteger, identity⟩ := gcd.bezout at a, b
      have bridgeA := IntegerDivides.natural_left at d, integerOfNat(a * c)
      have bridgeB := IntegerDivides.natural_left at d, integerOfNat(b * c)
      have bridgeG := IntegerDivides.natural_left at d, integerOfNat(gcd(a, b) * c)
      have magnitudeA := integerNatAbs.ofNat at a * c
      have magnitudeB := integerNatAbs.ofNat at b * c
      have magnitudeG := integerNatAbs.ofNat at gcd(a, b) * c
      rw magnitudeA at bridgeA
      rw magnitudeB at bridgeB
      rw magnitudeG at bridgeG
      have integerA := bridgeA.backward with dA
      have integerB := bridgeB.backward with dB
      have combination : IntegerDivides(integerOfNat(d),
          u * integerOfNat(a * c) + v * integerOfNat(b * c))
        exact IntegerDivides.linear_combination with integerA, integerB
      have value : u * integerOfNat(a * c) + v * integerOfNat(b * c) =
          integerOfNat(gcd(a, b) * c)
        have productA := integerOfNat.mul at a, c
        have productB := integerOfNat.mul at b, c
        have productG := integerOfNat.mul at gcd(a, b), c
        unfold integerLinearCombination at identity
        rw [productA, productB, productG, ← identity]
        ring
      rw value at combination
      exact bridgeG.forward with combination
  exact gcd.unique with certificate

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

theorem gcd.coprime_mul (a b c : Nat)
  requires coprimeAB : gcd(a, b) = 1
  shows gcd(a, b * c) = gcd(a, c)
proof
  have left := gcd.divides_left at a, c
  have right := gcd.divides_right at a, c
  have scaled := divides.multiply_left at gcd(a, c), c, b with *
  have certificate : IsGCD(a, b * c, gcd(a, c))
    apply IsGCD.intro
    . exact left
    . exact scaled
    . intros d dNat dA dBC
      have dividesB := gcd.divides_left at b, d
      have dividesD := gcd.divides_right at b, d
      have dividesA := divides.transitive at gcd(b, d), d, a with dividesD, dA
      have common := gcd.greatest at a, b, gcd(b, d) with dividesA, dividesB
      rw coprimeAB at common
      have one := divides.one_only at gcd(b, d) with *
      have cancelled := coprime.cancel at b, d, c with one, dBC
      exact gcd.greatest at a, c, d with dA, cancelled
  exact gcd.unique with certificate

theorem gcd.coprime_mul_left (a b c : Nat)
  requires coprimeAB : gcd(a, b) = 1
  shows gcd(a * c, b) = gcd(c, b)
proof
  have first := gcd.commutative at a * c, b
  have swapped := gcd.commutative at a, b
  rw swapped at coprimeAB
  have second := gcd.coprime_mul at b, a, c with coprimeAB
  have third := gcd.commutative at b, c
  rw [first, second, third]
  rfl

theorem gcd.eq_one_iff (a b : Nat)
  shows gcd(a, b) = 1 ↔ ∀ d, Nat(d) → d ∣ a → d ∣ b → d = 1
proof
  constructor
  . intros one d dNat left right
    have common := gcd.greatest at a, b, d with left, right
    rw one at common
    exact divides.one_only at d with *
  . intro every
    have left := gcd.divides_left at a, b
    have right := gcd.divides_right at a, b
    exact every with gcd(a, b), left, right

theorem coprime.symmetric (a b : Nat)
  requires coprimeAB : gcd(a, b) = 1
  shows gcd(b, a) = 1
proof
  have commute := gcd.commutative at b, a
  rw commute
  exact coprimeAB

theorem coprime.divisor_one (a b d : Nat)
  requires coprimeAB : gcd(a, b) = 1
  requires left : d ∣ a
  requires right : d ∣ b
  shows d = 1
proof
  have every := gcd.eq_one_iff at a, b
  exact every.forward with coprimeAB, d, left, right

theorem coprime.cancel_right (a n t : Nat)
  requires coprimeAN : gcd(a, n) = 1
  requires product : n ∣ t * a
  shows n ∣ t
proof
  have commute : t * a = a * t by ring
  rw commute at product
  exact coprime.cancel at a, n, t with coprimeAN, product

theorem coprime.mul_of_coprime (a b n : Nat)
  requires first : gcd(a, n) = 1
  requires second : gcd(b, n) = 1
  shows gcd(a * b, n) = 1
proof
  have swapped := coprime.symmetric at a, n with first
  have reduced := gcd.coprime_mul at n, a, b with swapped
  have commute := gcd.commutative at a * b, n
  rw [commute, reduced]
  exact coprime.symmetric at b, n with second

theorem coprime.of_mul_left (a b n : Nat)
  requires product : gcd(a * b, n) = 1
  shows gcd(a, n) = 1
proof
  have left := gcd.divides_left at a, n
  have right := gcd.divides_right at a, n
  have scaled := divides.multiply_right at gcd(a, n), a, b with left
  have common := gcd.greatest at a * b, n, gcd(a, n) with scaled, right
  rw product at common
  exact divides.one_only at gcd(a, n) with *

theorem coprime.of_mul_right (a b n : Nat)
  requires product : gcd(a * b, n) = 1
  shows gcd(b, n) = 1
proof
  have commute : a * b = b * a by ring
  rw commute at product
  exact coprime.of_mul_left at b, a, n with product

theorem coprime.mul_iff (a b n : Nat)
  shows gcd(a * b, n) = 1 ↔ gcd(a, n) = 1 ∧ gcd(b, n) = 1
proof
  constructor
  . intro product
    constructor
    . exact coprime.of_mul_left at a, b, n with product
    . exact coprime.of_mul_right at a, b, n with product
  . intro both
    rcases both with ⟨first, second⟩
    exact coprime.mul_of_coprime at a, b, n with first, second

theorem coprime.pow_left (a b n : Nat)
  requires coprimeAB : gcd(a, b) = 1
  shows gcd(a ^ n, b) = 1
proof
  induction n
  | zero =>
    have zero := pow.zero at a
    rw zero
    exact gcd.one_left at b
  | k + 1 using ih =>
    have expand := pow.add_one at a, k
    rw expand
    exact coprime.mul_of_coprime at a, a ^ k, b with coprimeAB, ih

theorem coprime.pow_right (a b n : Nat)
  requires coprimeAB : gcd(a, b) = 1
  shows gcd(a, b ^ n) = 1
proof
  have swapped := coprime.symmetric at a, b with coprimeAB
  have power := coprime.pow_left at b, a, n with swapped
  exact coprime.symmetric at b ^ n, a with power

theorem coprime.pow (a b m n : Nat)
  requires coprimeAB : gcd(a, b) = 1
  shows gcd(a ^ m, b ^ n) = 1
proof
  have left := coprime.pow_left at a, b, m with coprimeAB
  exact coprime.pow_right at a ^ m, b, n with left

theorem coprime.mul_divides (a b n : Nat)
  requires coprimeAB : gcd(a, b) = 1
  requires left : a ∣ n
  requires right : b ∣ n
  shows a * b ∣ n
proof
  obtain ⟨k, kNat, equation⟩ := left
  have scaled : b ∣ a * k
    rw equation
    exact right
  have cancelled := coprime.cancel at a, b, k with coprimeAB, scaled
  obtain ⟨m, mNat, kEquation⟩ := cancelled
  witness m
  rw [← equation, ← kEquation]
  ring

theorem Prime.gcd_of_not_divides (p a : Nat)
  requires prime : Prime(p)
  requires notDivides : ¬(p ∣ a)
  shows gcd(p, a) = 1
proof
  have certificate := Prime.coprime_of_not_divides with prime, notDivides
  exact gcd.unique with certificate

theorem Prime.coprime_or_divides (p a : Nat)
  requires prime : Prime(p)
  shows gcd(p, a) = 1 ∨ p ∣ a
proof
  have split : p ∣ a ∨ ¬(p ∣ a) by tauto
  cases split with yes | no
  . right
    exact yes
  . left
    exact Prime.gcd_of_not_divides with prime, no

theorem Prime.divides_pow (p a n : Nat)
  requires prime : Prime(p)
  requires power : p ∣ a ^ n
  shows p ∣ a
proof
  induction n
  | zero =>
    intro power
    exfalso
    have zero := pow.zero at a
    rw zero at power
    have one := divides.one_only at p with *
    have above := Prime.greater_than_one with prime
    rw one at above
    exact Less.irreflexive at 1 with above
  | k + 1 using ih =>
    intro power
    have expand := pow.add_one at a, k
    rw expand at power
    have split := Prime.divides_mul at p, a, a ^ k with prime, power
    cases split with base | rest
    . exact base
    . exact ih with rest