-- Bézout coefficients over the existing quotient integers
-- 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.Bezout
import Euclidean
import Int

def integerLinearCombination (u v : Integer, a b : Nat) : Integer :=
  u * integerOfNat(a) + v * integerOfNat(b)

theorem integerLinearCombination.classes (up un vp vn a b : Nat)
  shows integerLinearCombination(integerClass(up, un), integerClass(vp, vn), a, b) =
    integerClass(up * a + vp * b, un * a + vn * b)
proof
  simp [integerLinearCombination, integerOfNat, integerMulValue.classes, integerClassMul, integerAddValue.classes, integerClassSum, mul.right_zero, mul, add.right_unit, add]

-- If a = b*q+r, then u*b+v*r = v*a+(u-q*v)*b.
theorem integerLinearCombination.euclidean_step (u v : Integer, a b q r : Nat)
  requires equation : a = b * q + r
  shows integerLinearCombination(v, u + (-(integerOfNat(q) * v)), a, b) =
    integerLinearCombination(u, v, b, r)
proof
  simp [integerLinearCombination, integerOfNat.add, integerOfNat.mul]
  ring

-- The coefficient update can now use a computed quotient directly.
theorem integerLinearCombination.remainder_step (u v : Integer, a b : Nat)
  shows integerLinearCombination(v, u + (-(integerOfNat(quotientNat(a, b)) * v)), a, b) =
    integerLinearCombination(u, v, b, a % b)
proof
  have equation := quotientNat.equation at b, a with *
  exact integerLinearCombination.euclidean_step with *

theorem integerLinearCombination.unit_left (a b : Nat)
  shows integerLinearCombination(integerOfNat(1), integerOfNat(0), a, b) = integerOfNat(a)
proof
  simp [integerOfNat, integerLinearCombination.classes, mul.left_unit, mul.left_zero, add.right_unit]

-- Existential coefficients use the same sufficient bound as gcdSteps.correct.
-- No executable coefficient algorithm is claimed by this existence theorem.
theorem gcdSteps.bezout (fuel a b : Nat)
  shows b ≤ fuel → ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧
    integerLinearCombination(u, v, a, b) = integerOfNat(gcdSteps(fuel, a, b))
proof
  induction fuel generalizing a b
  | zero =>
    intros a b aNat bNat bound
    have bZero : b = 0
    . have lower := Grace.Cumulus.Nat.Order.LessEqual.zero at b with *
      exact LessEqual.antisymmetric at b, 0 with *
    have unit := integerLinearCombination.unit_left at a, b with *
    witness integerOfNat(1)
    witness integerOfNat(0)
    simpa [gcdSteps] using unit
  | succ(k) using ih =>
    intros a b aNat bNat bound
    have shape := natural.zero_or_successor at b with *
    cases shape with zero | successor
    . have unit := integerLinearCombination.unit_left at a, b with *
      witness integerOfNat(1)
      witness integerOfNat(0)
      simpa [gcdSteps.zero_right] using unit
    . obtain ⟨j, jNat, bShape⟩ := successor
      rw bShape at bound
      rw under bShape
      have nonzero : succ(j) ≠ 0
      . intro equal
        have distinct := Naturals.disjoint.zero.succ at j
        symm at equal
        exact distinct with equal
      have remainderNat := mod.natural at succ(j), a with *
      have remainderBound := mod.less at a, succ(j) with *
      have enough : a % succ(j) ≤ k
      . arith
      obtain ⟨u, uInteger, v, vInteger, coefficients⟩ := ih with succ(j), a % succ(j), assumption, remainderNat, enough
      obtain ⟨q, qNat, equation⟩ := mod.equation at a, succ(j) with *
      have preserved := integerLinearCombination.euclidean_step at u, v, a, succ(j), q, a % succ(j) with *
      have value := gcdSteps.successor at k, a, j with *
      witness v
      witness u + (-(integerOfNat(q) * v))
      rw [preserved, value]
      exact coefficients

theorem gcd.bezout (a b : Nat)
  shows ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧
    integerLinearCombination(u, v, a, b) = integerOfNat(gcd(a, b))
proof
  have bound := LessEqual.reflexive at b with *
  have coefficients := gcdSteps.bezout at b, a, b with bound
  simpa [gcd] using coefficients

theorem IsGCD.bezout (a b g : Nat)
  requires certificate : IsGCD(a, b, g)
  shows ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧
    integerLinearCombination(u, v, a, b) = integerOfNat(g)
proof
  have equal := gcd.unique with *
  have coefficients := gcd.bezout at a, b with *
  rwa under equal at coefficients