-- Coprime factors cancel: if n is coprime to a then n divides a·t only when
-- it divides t, so multiplication by a is injective on residues mod n; a
-- product of numbers coprime to n is coprime to n, and reducing mod n keeps
-- the greatest common divisor with n
-- 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.CoprimeCancel
import Modular
import Coprime
import Factorization

theorem coprime.cancel (a n t : Nat)
  requires coprime : gcd(a, n) = 1
  requires divides : n ∣ a * t
  shows n ∣ t
proof
  have integerCoprime : IntegerCoprime(integerOfNat(n), integerOfNat(a))
    unfold IntegerCoprime
    have same := integerGCD.ofNat at n, a
    have commute := gcd.commutative at n, a
    rwa [same, commute]
  have product := integerOfNat.mul at a, t
  have magnitude := integerNatAbs.ofNat at a * t
  have bridge := IntegerDivides.natural_left at n, integerOfNat(a * t)
  have integerDivides : IntegerDivides(integerOfNat(n), integerOfNat(a) * integerOfNat(t))
    rw ← product
    apply bridge.backward
    rwa magnitude
  have cancelled := IntegerCoprime.cancel with integerCoprime, integerDivides
  have back := IntegerDivides.natural_left at n, integerOfNat(t)
  have result := back.forward with cancelled
  have magnitudeT := integerNatAbs.ofNat at t
  rwa magnitudeT at result

-- Multiplication by a coprime factor is injective on remainders.
theorem coprime.mul_cancel_mod_le (a n x y : Nat)
  requires nonzero : n ≠ 0
  requires coprime : gcd(a, n) = 1
  requires below : x ≤ y
  requires same : (a * x) % n = (a * y) % n
  shows x % n = y % n
proof
  obtain ⟨t, tNat, shape⟩ := below
  rw ← shape at same
  have expand : a * (x + t) = a * x + a * t by ring
  rw expand at same
  symm at same
  have dividesProduct := mod.add_cancel with nonzero, same
  obtain ⟨s, sNat, form⟩ := coprime.cancel at a, n, t with coprime, dividesProduct
  rw [← shape, ← form]
  have shifted := mod.add_multiple at n, x, s with nonzero
  symm at shifted
  exact shifted

theorem coprime.mul_cancel_mod (a n x y : Nat)
  requires nonzero : n ≠ 0
  requires coprime : gcd(a, n) = 1
  requires same : (a * x) % n = (a * y) % n
  shows x % n = y % n
proof
  have total := LessEqual.total at x, y
  cases total with below | above
  . exact coprime.mul_cancel_mod_le with nonzero, coprime, below, same
  . symm at same
    have flipped := coprime.mul_cancel_mod_le with nonzero, coprime, above, same
    symm at flipped
    exact flipped

-- Reducing mod n does not change the greatest common divisor with n.
theorem coprime.mod (a n : Nat)
  requires nonzero : n ≠ 0
  shows gcd(a % n, n) = gcd(a, n)
proof
  have first := gcd.euclidean at a, n with nonzero
  have second := gcd.euclidean at a % n, n with nonzero
  have idempotent := mod.mod at n, a with nonzero
  rw [second, idempotent, first]
  rfl

-- A product of numbers coprime to n is coprime to n.
theorem coprime.mul (a b n : Nat)
  requires nonzero : n ≠ 0
  requires coprimeA : gcd(a, n) = 1
  requires coprimeB : gcd(b, n) = 1
  shows gcd(a * b, n) = 1
proof
  have gNat := gcd.natural at a * b, n
  have dividesN := gcd.divides_right at a * b, n
  have dividesProduct := gcd.divides_left at a * b, n
  have gNonzero : gcd(a * b, n) ≠ 0
    intro zero
    rw zero at dividesN
    have nZero := zero.divides_only_zero with dividesN
    exact nonzero with nZero
  have trichotomy := Less.trichotomy at 1, gcd(a * b, n)
  rcases trichotomy with above | equal | below
  . exfalso
    obtain ⟨p, prime, dividesG⟩ := natural.exists_prime_divisor with above
    have pNat := Prime.natural with prime
    have pDividesProduct := divides.transitive with dividesG, dividesProduct
    have pDividesN := divides.transitive with dividesG, dividesN
    have pAboveOne := Prime.greater_than_one with prime
    have split := Prime.divides_mul with prime, pDividesProduct
    cases split with dividesA | dividesB
    . have dividesGcd := gcd.greatest with dividesA, pDividesN
      rw coprimeA at dividesGcd
      have pOne := divides.one_only with pNat, dividesGcd
      rw pOne at pAboveOne
      exact Less.irreflexive with *, pAboveOne
    . have dividesGcd := gcd.greatest with dividesB, pDividesN
      rw coprimeB at dividesGcd
      have pOne := divides.one_only with pNat, dividesGcd
      rw pOne at pAboveOne
      exact Less.irreflexive with *, pAboveOne
  . symm at equal
    exact equal
  . exfalso
    have atMostZero := Less.successor_upper at gcd(a * b, n), 0 with below
    have zeroLe := Grace.Cumulus.Nat.Order.LessEqual.zero at gcd(a * b, n)
    have zero := LessEqual.antisymmetric with atMostZero, zeroLe
    exact gNonzero with zero

theorem coprime.mul_mod (a b n : Nat)
  requires nonzero : n ≠ 0
  requires coprimeA : gcd(a, n) = 1
  requires coprimeB : gcd(b, n) = 1
  shows gcd((a * b) % n, n) = 1
proof
  have reduce := coprime.mod at a * b, n with nonzero
  rw reduce
  exact coprime.mul with nonzero, coprimeA, coprimeB