-- Coprime cancellation and modular inverses from Bézout
-- 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.Coprime
import IntegerGCD

predicate IntegerCoprime (a b : Integer) := integerGCD(a, b) = 1
predicate IntegerCongruent (m a b : Integer) := IntegerDivides(m, a - b)

theorem IntegerDivides.linear_combination (d a b u v : Integer)
  requires left : IntegerDivides(d, a)
  requires right : IntegerDivides(d, b)
  shows IntegerDivides(d, u * a + v * b)
proof
  obtain ⟨p, pInteger, leftEquation⟩ := left
  obtain ⟨q, qInteger, rightEquation⟩ := right
  witness u * p + v * q
  rw [← leftEquation, ← rightEquation]
  ring

theorem IntegerCoprime.symmetric (a b : Integer)
  requires coprime : IntegerCoprime(a, b)
  shows IntegerCoprime(b, a)
proof
  unfold IntegerCoprime
  rw integerGCD.commutative
  exact coprime

theorem IntegerCoprime.bezout (a b : Integer)
  requires coprime : IntegerCoprime(a, b)
  shows ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧ u * a + v * b = integerOne
proof
  have identity := integerGCD.bezout at a, b with *
  unfold IntegerCoprime at coprime
  simpa [coprime, integerOne] using identity

-- Euclid's coprime cancellation lemma, with an explicit quotient witness.
theorem IntegerCoprime.cancel (a b c : Integer)
  requires coprime : IntegerCoprime(a, b)
  requires divides : IntegerDivides(a, b * c)
  shows IntegerDivides(a, c)
proof
  obtain ⟨u, uInteger, v, vInteger, identity⟩ := IntegerCoprime.bezout at a, b with *
  obtain ⟨q, qInteger, equation⟩ := divides
  have scaled : (u * a + v * b) * c = c
  . rw identity
    ring
  witness u * c + v * q
  linear_combination scaled + v * equation

theorem IntegerCongruent.reflexive (m a : Integer)
  shows IntegerCongruent(m, a, a)
proof
  witness integerZero
  ring

theorem IntegerCongruent.symmetric (m a b : Integer)
  requires congruent : IntegerCongruent(m, a, b)
  shows IntegerCongruent(m, b, a)
proof
  obtain ⟨q, qInteger, equation⟩ := congruent
  witness -q
  linear_combination -equation

theorem IntegerCongruent.transitive (m a b c : Integer)
  requires first : IntegerCongruent(m, a, b)
  requires second : IntegerCongruent(m, b, c)
  shows IntegerCongruent(m, a, c)
proof
  obtain ⟨p, pInteger, left⟩ := first
  obtain ⟨q, qInteger, right⟩ := second
  witness p + q
  linear_combination left + right

-- Every integer coprime to the modulus has a multiplicative inverse modulo it.
theorem IntegerCoprime.modular_inverse (a m : Integer)
  requires coprime : IntegerCoprime(a, m)
  shows ∃ u, Integer(u) ∧ IntegerCongruent(m, a * u, integerOne)
proof
  obtain ⟨u, uInteger, v, vInteger, identity⟩ := IntegerCoprime.bezout at a, m with *
  witness u
  witness -v
  linear_combination -identity

theorem IntegerCoprime.of_bezout (a b u v : Integer)
  requires identity : u * a + v * b = integerOne
  shows IntegerCoprime(a, b)
proof
  have left := integerGCD.divides_left at a, b with *
  have right := integerGCD.divides_right at a, b with *
  have divides := IntegerDivides.linear_combination at integerOfNat(integerGCD(a, b)), a, b, u, v with *
  rw identity at divides
  have magnitude := IntegerDivides.natural_left.forward at integerGCD(a, b), integerOne with *
  simp [integerOne, integerNatAbs.ofNat] at magnitude
  unfold IntegerCoprime
  exact divides.one_only with *

theorem IntegerCoprime.of_modular_inverse (a m u : Integer)
  requires inverse : IntegerCongruent(m, a * u, integerOne)
  shows IntegerCoprime(a, m)
proof
  obtain ⟨q, qInteger, equation⟩ := inverse
  apply IntegerCoprime.of_bezout at a, m, u, -q with *{4}
  linear_combination -equation

theorem IntegerCoprime.modular_inverse_iff (a m : Integer)
  shows IntegerCoprime(a, m) ↔ ∃ u, Integer(u) ∧ IntegerCongruent(m, a * u, integerOne)
proof
  constructor
  . intro coprime
    exact IntegerCoprime.modular_inverse with *
  . intro exists
    obtain ⟨u, uInteger, inverse⟩ := exists
    exact IntegerCoprime.of_modular_inverse with *

theorem IntegerCongruent.add (m a b c d : Integer)
  requires first : IntegerCongruent(m, a, b)
  requires second : IntegerCongruent(m, c, d)
  shows IntegerCongruent(m, a + c, b + d)
proof
  obtain ⟨p, pInteger, left⟩ := first
  obtain ⟨q, qInteger, right⟩ := second
  witness p + q
  linear_combination left + right

theorem IntegerCongruent.mul (m a b c d : Integer)
  requires first : IntegerCongruent(m, a, b)
  requires second : IntegerCongruent(m, c, d)
  shows IntegerCongruent(m, a * c, b * d)
proof
  obtain ⟨p, pInteger, left⟩ := first
  obtain ⟨q, qInteger, right⟩ := second
  witness p * c + b * q
  linear_combination c * left + b * right

theorem IntegerCongruent.cancel_coprime (m a b c : Integer)
  requires coprime : IntegerCoprime(m, a)
  requires congruent : IntegerCongruent(m, a * b, a * c)
  shows IntegerCongruent(m, b, c)
proof
  unfold IntegerCongruent at congruent
  have distribution : a * b - a * c = a * (b - c)
  . ring
  rw distribution at congruent
  unfold IntegerCongruent
  exact IntegerCoprime.cancel with *

theorem IntegerCongruent.inverse_unique (m a u v : Integer)
  requires first : IntegerCongruent(m, a * u, integerOne)
  requires second : IntegerCongruent(m, a * v, integerOne)
  shows IntegerCongruent(m, u, v)
proof
  have coprime := IntegerCoprime.of_modular_inverse at a, m, u with *
  have symmetric := IntegerCoprime.symmetric with *
  have reverse := IntegerCongruent.symmetric at m, a * v, integerOne with *
  have same := IntegerCongruent.transitive at m, a * u, integerOne, a * v with *
  exact IntegerCongruent.cancel_coprime with *

-- Ground natural arithmetic can certify a congruence of embedded integers.
theorem IntegerCongruent.of_natural_difference (m a b q : Nat)
  requires equation : a = b + m * q
  shows IntegerCongruent(integerOfNat(m), integerOfNat(a), integerOfNat(b))
proof
  witness integerOfNat(q)
  simp [integerOfNat.add, integerOfNat.mul]
  ring