Grace/Cumulus/NumberTheory/Bezout.g17

Open in Workbench Download source

Imports

Euclidean · Int

Declarations

Source

1-- Bézout coefficients over the existing quotient integers2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.NumberTheory.Bezout8import Euclidean9import Int1011def integerLinearCombination (u v : Integer, a b : Nat) : Integer :=12  u * integerOfNat(a) + v * integerOfNat(b)1314theorem integerLinearCombination.classes (up un vp vn a b : Nat)15  shows integerLinearCombination(integerClass(up, un), integerClass(vp, vn), a, b) =16    integerClass(up * a + vp * b, un * a + vn * b)17proof18  simp [integerLinearCombination, integerOfNat, integerMulValue.classes, integerClassMul, integerAddValue.classes, integerClassSum, mul.right_zero, mul, add.right_unit, add]1920-- If a = b*q+r, then u*b+v*r = v*a+(u-q*v)*b.21theorem integerLinearCombination.euclidean_step (u v : Integer, a b q r : Nat)22  requires equation : a = b * q + r23  shows integerLinearCombination(v, u + (-(integerOfNat(q) * v)), a, b) =24    integerLinearCombination(u, v, b, r)25proof26  simp [integerLinearCombination, integerOfNat.add, integerOfNat.mul]27  ring2829-- The coefficient update can now use a computed quotient directly.30theorem integerLinearCombination.remainder_step (u v : Integer, a b : Nat)31  shows integerLinearCombination(v, u + (-(integerOfNat(quotientNat(a, b)) * v)), a, b) =32    integerLinearCombination(u, v, b, a % b)33proof34  have equation := quotientNat.equation at b, a with *35  exact integerLinearCombination.euclidean_step with *3637theorem integerLinearCombination.unit_left (a b : Nat)38  shows integerLinearCombination(integerOfNat(1), integerOfNat(0), a, b) = integerOfNat(a)39proof40  simp [integerOfNat, integerLinearCombination.classes, mul.left_unit, mul.left_zero, add.right_unit]4142-- Existential coefficients use the same sufficient bound as gcdSteps.correct.43-- No executable coefficient algorithm is claimed by this existence theorem.44theorem gcdSteps.bezout (fuel a b : Nat)45  shows b ≤ fuel → ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧46    integerLinearCombination(u, v, a, b) = integerOfNat(gcdSteps(fuel, a, b))47proof48  induction fuel generalizing a b49  | zero =>50    intros a b aNat bNat bound51    have bZero : b = 052    . have lower := Grace.Cumulus.Nat.Order.LessEqual.zero at b with *53      exact LessEqual.antisymmetric at b, 0 with *54    have unit := integerLinearCombination.unit_left at a, b with *55    witness integerOfNat(1)56    witness integerOfNat(0)57    simpa [gcdSteps] using unit58  | succ(k) using ih =>59    intros a b aNat bNat bound60    have shape := natural.zero_or_successor at b with *61    cases shape with zero | successor62    . have unit := integerLinearCombination.unit_left at a, b with *63      witness integerOfNat(1)64      witness integerOfNat(0)65      simpa [gcdSteps.zero_right] using unit66    . obtain ⟨j, jNat, bShape⟩ := successor67      rw bShape at bound68      rw under bShape69      have nonzero : succ(j) ≠ 070      . intro equal71        have distinct := Naturals.disjoint.zero.succ at j72        symm at equal73        exact distinct with equal74      have remainderNat := mod.natural at succ(j), a with *75      have remainderBound := mod.less at a, succ(j) with *76      have enough : a % succ(j) ≤ k77      . arith78      obtain ⟨u, uInteger, v, vInteger, coefficients⟩ := ih with succ(j), a % succ(j), assumption, remainderNat, enough79      obtain ⟨q, qNat, equation⟩ := mod.equation at a, succ(j) with *80      have preserved := integerLinearCombination.euclidean_step at u, v, a, succ(j), q, a % succ(j) with *81      have value := gcdSteps.successor at k, a, j with *82      witness v83      witness u + (-(integerOfNat(q) * v))84      rw [preserved, value]85      exact coefficients8687theorem gcd.bezout (a b : Nat)88  shows ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧89    integerLinearCombination(u, v, a, b) = integerOfNat(gcd(a, b))90proof91  have bound := LessEqual.reflexive at b with *92  have coefficients := gcdSteps.bezout at b, a, b with bound93  simpa [gcd] using coefficients9495theorem IsGCD.bezout (a b g : Nat)96  requires certificate : IsGCD(a, b, g)97  shows ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧98    integerLinearCombination(u, v, a, b) = integerOfNat(g)99proof100  have equal := gcd.unique with *101  have coefficients := gcd.bezout at a, b with *102  rwa under equal at coefficients103