-- GCD and Bézout for arbitrary quotient integer inputs
-- 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.IntegerGCD
import ExtendedGCD

predicate IntegerDivides (x y : Integer) := ∃ q, Integer(q) ∧ x * q = y

theorem IntegerDivides.to_magnitudes (x y : Integer)
  requires divides : IntegerDivides(x, y)
  shows integerNatAbs(x) ∣ integerNatAbs(y)
proof
  obtain ⟨q, qInteger, equation⟩ := divides
  have qNat := integerNatAbs.natural at q with *
  have product := integerNatAbs.mul at x, q with *
  rw equation at product
  symm at product
  apply divides.definition.backward with *{2}
  refine ⟨integerNatAbs(q), qNat, product⟩

theorem IntegerDivides.of_magnitudes (x y : Integer)
  requires divides : integerNatAbs(x) ∣ integerNatAbs(y)
  shows IntegerDivides(x, y)
proof
  obtain ⟨k, kNat, equation⟩ := divides.definition.forward at integerNatAbs(x), integerNatAbs(y) with *
  have xSign := integerNatAbs.cases at x with *
  obtain ⟨v, vInteger, adjusted⟩ := integerMulValue.sign_adjust at integerOfNat(k), x, integerNatAbs(x) with *
  have embedded := integerOfNat.mul at k, integerNatAbs(x) with *
  have naturalProduct : k * integerNatAbs(x) = integerNatAbs(y)
  . ring
  rw naturalProduct at embedded
  rw ← embedded at adjusted
  have swapped := integerMulValue.commutative at x, v with *
  rw adjusted at swapped
  have ySign := integerNatAbs.cases at y with *
  unfold IntegerDivides
  cases ySign with positive | negative
  . rw ← positive at swapped
    refine ⟨v, vInteger, swapped⟩
  . have vNegative := integerNegValue.integer at v with *
    have changed := integerMulValue.neg_right at x, v with *
    have flipped := integerOfNat.neg at integerNatAbs(y) with *
    rw [swapped, flipped, ← negative] at changed
    refine ⟨-v, vNegative, changed⟩

theorem IntegerDivides.magnitude_iff (x y : Integer)
  shows IntegerDivides(x, y) ↔ integerNatAbs(x) ∣ integerNatAbs(y)
proof
  constructor
  . intro divides
    exact IntegerDivides.to_magnitudes with *
  . intro divides
    exact IntegerDivides.of_magnitudes with *

-- Return the canonical nonnegative GCD as a natural magnitude.
def integerGCD (x y : Integer) : Nat := gcd(integerNatAbs(x), integerNatAbs(y))

theorem integerGCD.natural (x y : Integer)
  shows Nat(integerGCD(x, y))
proof
  unfold integerGCD
  exact gcd.natural with *

theorem integerGCD.magnitudes (x y : Integer)
  shows IsGCD(integerNatAbs(x), integerNatAbs(y), integerGCD(x, y))
proof
  have correct := gcd.correct at integerNatAbs(x), integerNatAbs(y) with *
  simpa [integerGCD] using correct

theorem integerGCD.divides_left (x y : Integer)
  shows IntegerDivides(integerOfNat(integerGCD(x, y)), x)
proof
  have correct := integerGCD.magnitudes at x, y with *
  have divides := IsGCD.divides_left with *
  apply IntegerDivides.of_magnitudes with *{2}
  simpa [integerNatAbs.ofNat] using divides

theorem integerGCD.divides_right (x y : Integer)
  shows IntegerDivides(integerOfNat(integerGCD(x, y)), y)
proof
  have correct := integerGCD.magnitudes at x, y with *
  have divides := IsGCD.divides_right with *
  apply IntegerDivides.of_magnitudes with *{2}
  simpa [integerNatAbs.ofNat] using divides

theorem integerGCD.greatest (x y d : Integer)
  requires left : IntegerDivides(d, x)
  requires right : IntegerDivides(d, y)
  shows IntegerDivides(d, integerOfNat(integerGCD(x, y)))
proof
  have leftMagnitude := IntegerDivides.to_magnitudes at d, x with *
  have rightMagnitude := IntegerDivides.to_magnitudes at d, y with *
  have correct := integerGCD.magnitudes at x, y with *
  have divides := IsGCD.greatest with *
  apply IntegerDivides.of_magnitudes with *{2}
  simpa [integerNatAbs.ofNat] using divides

theorem integerGCD.bezout (x y : Integer)
  shows ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧ u * x + v * y = integerOfNat(integerGCD(x, y))
proof
  have identity := bezout.correct at integerNatAbs(x), integerNatAbs(y) with *
  have xSign := integerNatAbs.cases at x with *
  have ySign := integerNatAbs.cases at y with *
  obtain ⟨u, uInteger, leftProduct⟩ := integerMulValue.sign_adjust at bezoutLeft(integerNatAbs(x), integerNatAbs(y)), x, integerNatAbs(x) with *
  obtain ⟨v, vInteger, rightProduct⟩ := integerMulValue.sign_adjust at bezoutRight(integerNatAbs(x), integerNatAbs(y)), y, integerNatAbs(y) with *
  witness u
  witness v
  rw [leftProduct, rightProduct]
  simpa [integerLinearCombination, integerGCD] using identity

theorem integerGCD.ofNat (a b : Nat)
  shows integerGCD(integerOfNat(a), integerOfNat(b)) = gcd(a, b)
proof
  simp [integerGCD, integerNatAbs.ofNat]

theorem integerGCD.neg_left (x y : Integer)
  shows integerGCD(-x, y) = integerGCD(x, y)
proof
  simp [integerGCD, integerNatAbs.neg]

theorem integerGCD.neg_right (x y : Integer)
  shows integerGCD(x, -y) = integerGCD(x, y)
proof
  simp [integerGCD, integerNatAbs.neg]

theorem IntegerDivides.natural_left (d : Nat, x : Integer)
  shows IntegerDivides(integerOfNat(d), x) ↔ d ∣ integerNatAbs(x)
proof
  have equivalence := IntegerDivides.magnitude_iff at integerOfNat(d), x with *
  simpa [integerNatAbs.ofNat] using equivalence

predicate IsIntegerGCD (x y : Integer, g : Nat) :=
  IntegerDivides(integerOfNat(g), x) ∧ IntegerDivides(integerOfNat(g), y) ∧
    (∀ d, Integer(d) → IntegerDivides(d, x) → IntegerDivides(d, y) → IntegerDivides(d, integerOfNat(g)))

theorem integerGCD.correct (x y : Integer)
  shows IsIntegerGCD(x, y, integerGCD(x, y))
proof
  have left := integerGCD.divides_left at x, y with *
  have right := integerGCD.divides_right at x, y with *
  constructor
  . exact left
  . constructor
    . exact right
    . intros d dInteger dLeft dRight
      exact integerGCD.greatest with *

theorem IsIntegerGCD.magnitudes (x y : Integer, g : Nat)
  requires certificate : IsIntegerGCD(x, y, g)
  shows IsGCD(integerNatAbs(x), integerNatAbs(y), g)
proof
  rcases certificate with ⟨left, right, greatest⟩
  have leftMagnitude := IntegerDivides.natural_left.forward at g, x with *
  have rightMagnitude := IntegerDivides.natural_left.forward at g, y with *
  apply IsGCD.intro with leftMagnitude, rightMagnitude
  intros d dNat dLeft dRight
  have leftInteger := IntegerDivides.natural_left.backward at d, x with *
  have rightInteger := IntegerDivides.natural_left.backward at d, y with *
  have common := greatest with integerOfNat(d), leftInteger, rightInteger
  have magnitude := IntegerDivides.to_magnitudes at integerOfNat(d), integerOfNat(g) with *
  simpa [integerNatAbs.ofNat] using magnitude

theorem IsIntegerGCD.unique (x y : Integer, g h : Nat)
  requires first : IsIntegerGCD(x, y, g)
  requires second : IsIntegerGCD(x, y, h)
  shows g = h
proof
  have firstMagnitude := IsIntegerGCD.magnitudes at x, y, g with *
  have secondMagnitude := IsIntegerGCD.magnitudes at x, y, h with *
  exact IsGCD.unique with *

theorem integerGCD.unique (x y : Integer, g : Nat)
  requires certificate : IsIntegerGCD(x, y, g)
  shows integerGCD(x, y) = g
proof
  have correct := integerGCD.correct at x, y with *
  exact IsIntegerGCD.unique with *

theorem integerGCD.commutative (x y : Integer)
  shows integerGCD(x, y) = integerGCD(y, x)
proof
  have commute := gcd.commutative at integerNatAbs(x), integerNatAbs(y) with *
  simpa [integerGCD] using commute

theorem integerGCD.zero_right (x : Integer)
  shows integerGCD(x, integerZero) = integerNatAbs(x)
proof
  simp [integerGCD, integerNatAbs.zero, gcd.zero_right]

theorem integerGCD.zero_left (x : Integer)
  shows integerGCD(integerZero, x) = integerNatAbs(x)
proof
  simp [integerGCD, integerNatAbs.zero, gcd.zero_left]