Grace/Cumulus/NumberTheory/ExtendedGCD.g17

Open in Workbench Download source

Imports

Bezout

Declarations

Source

1-- Executable Bézout coefficients and arbitrary-input correctness2-- 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.ExtendedGCD8import Bezout910-- Each integer already has natural-pair representatives. Compute their four11-- components together through one structurally recursive function. `first`12-- selects the coefficient of a; `negative` selects its subtracted component.13def bezoutBase (negative first : Bool) : Nat :=14  chooseNat(first, chooseNat(negative, 0, 1), 0)1516def bezoutComponent (fuel a b : Nat, negative first : Bool) → Nat17  | zero, a, b, negative, first => bezoutBase(negative, first)18  | succ(fuel), a, b, negative, first =>19      chooseNat(isZero(b), bezoutBase(negative, first),20        chooseNat(first,21          bezoutComponent(fuel, b, a % b, negative, Bool.false),22          bezoutComponent(fuel, b, a % b, negative, Bool.true) +23            quotientNat(a, b) * bezoutComponent(fuel, b, a % b, BoolOps.not(negative), Bool.false)))2425theorem bezoutBase.natural (negative first : Bool)26  shows Nat(bezoutBase(negative, first))27proof28  have result := chooseNat.natural at first, chooseNat(negative, 0, 1), 0 with *29  simpa [bezoutBase] using result3031theorem bezoutComponent.natural (fuel a b : Nat, negative first : Bool)32  shows Nat(bezoutComponent(fuel, a, b, negative, first))33proof34  induction fuel generalizing a b negative first35  | zero =>36    intros a b negative first aNat bNat negativeBool firstBool37    have result := bezoutBase.natural at negative, first with *38    simpa [bezoutComponent] using result39  | succ(k) using ih =>40    intros a b negative first aNat bNat negativeBool firstBool41    have flipped := BoolOps.not.boolean at negative with *42    have remainderNat := mod.natural at b, a with *43    have rightNat := ih with b, a % b, negative, Bool.false, bNat, remainderNat, negativeBool, Bool.inductive.constructor.false44    have leftNat := ih with b, a % b, negative, Bool.true, bNat, remainderNat, negativeBool, Bool.inductive.constructor.true45    have oppositeNat := ih with b, a % b, BoolOps.not(negative), Bool.false, bNat, remainderNat, flipped, Bool.inductive.constructor.false46    have condition := isZero.boolean at b with *47    have result := chooseNat.natural at isZero(b), bezoutBase(negative, first), chooseNat(first, bezoutComponent(k, b, a % b, negative, Bool.false), bezoutComponent(k, b, a % b, negative, Bool.true) + quotientNat(a, b) * bezoutComponent(k, b, a % b, BoolOps.not(negative), Bool.false)) with *48    simpa [bezoutComponent] using result4950def bezoutLeftSteps (fuel a b : Nat) : Integer :=51  integerClass(bezoutComponent(fuel, a, b, Bool.false, Bool.true), bezoutComponent(fuel, a, b, Bool.true, Bool.true))5253def bezoutRightSteps (fuel a b : Nat) : Integer :=54  integerClass(bezoutComponent(fuel, a, b, Bool.false, Bool.false), bezoutComponent(fuel, a, b, Bool.true, Bool.false))5556theorem bezoutLeftSteps.integer (fuel a b : Nat)57  shows Integer(bezoutLeftSteps(fuel, a, b))58proof59  unfold bezoutLeftSteps60  exact integerClass.integer with *6162theorem bezoutRightSteps.integer (fuel a b : Nat)63  shows Integer(bezoutRightSteps(fuel, a, b))64proof65  unfold bezoutRightSteps66  exact integerClass.integer with *6768theorem bezoutComponent.zero_right (a fuel : Nat, negative first : Bool)69  shows bezoutComponent(fuel, a, 0, negative, first) = bezoutBase(negative, first)70proof71  induction fuel72  | zero => simp [bezoutComponent]73  | succ(k) using ih => simp [bezoutComponent, isZero, chooseNat]7475theorem bezoutLeftSteps.zero_right (a fuel : Nat)76  shows bezoutLeftSteps(fuel, a, 0) = integerOfNat(1)77proof78  simp [bezoutLeftSteps, bezoutComponent.zero_right, bezoutBase, chooseNat, integerOfNat]7980theorem bezoutRightSteps.zero_right (a fuel : Nat)81  shows bezoutRightSteps(fuel, a, 0) = integerOfNat(0)82proof83  simp [bezoutRightSteps, bezoutComponent.zero_right, bezoutBase, chooseNat, integerOfNat]8485theorem bezoutLeftSteps.successor (fuel a b : Nat)86  shows bezoutLeftSteps(succ(fuel), a, succ(b)) = bezoutRightSteps(fuel, succ(b), a % succ(b))87proof88  simp [bezoutLeftSteps, bezoutRightSteps, bezoutComponent, isZero, chooseNat]8990theorem bezoutRightSteps.successor (fuel a b : Nat)91  shows bezoutRightSteps(succ(fuel), a, succ(b)) =92    bezoutLeftSteps(fuel, succ(b), a % succ(b)) +93      (-(integerOfNat(quotientNat(a, succ(b))) * bezoutRightSteps(fuel, succ(b), a % succ(b))))94proof95  simp [bezoutLeftSteps, bezoutRightSteps, bezoutComponent, isZero, chooseNat, BoolOps.not, integerOfNat, integerMulValue.classes, integerClassMul, integerNegValue.classes, integerClassNeg, integerAddValue.classes, integerClassSum, mul.right_zero, mul, add.right_unit, add]9697theorem bezoutSteps.correct (fuel a b : Nat)98  shows integerLinearCombination(bezoutLeftSteps(fuel, a, b), bezoutRightSteps(fuel, a, b), a, b) =99      integerOfNat(gcdSteps(fuel, a, b))100proof101  induction fuel generalizing a b102  | zero =>103    intros a b aNat bNat104    have unit := integerLinearCombination.unit_left at a, b with *105    simpa [bezoutLeftSteps, bezoutRightSteps, bezoutComponent, bezoutBase, chooseNat, gcdSteps, integerOfNat] using unit106  | succ(k) using ih =>107    intros a b aNat bNat108    have shape := natural.zero_or_successor at b with *109    cases shape with zero | successor110    . rw zero111      have unit := integerLinearCombination.unit_left at a, 0 with *112      simpa [bezoutLeftSteps.zero_right, bezoutRightSteps.zero_right, gcdSteps.zero_right] using unit113    . obtain ⟨j, jNat, bShape⟩ := successor114      rw bShape115      have remainderNat := mod.natural at succ(j), a with *116      have recursive := ih with succ(j), a % succ(j), assumption, remainderNat117      have preserved := integerLinearCombination.remainder_step at bezoutLeftSteps(k, succ(j), a % succ(j)), bezoutRightSteps(k, succ(j), a % succ(j)), a, succ(j) with *118      have leftValue := bezoutLeftSteps.successor at k, a, j with *119      have rightValue := bezoutRightSteps.successor at k, a, j with *120      have gcdValue := gcdSteps.successor at k, a, j with *121      rw [leftValue, rightValue, gcdValue, preserved]122      exact recursive123124-- Public coefficients use the same proved sufficient bound as gcd.125def bezoutLeft (a b : Nat) : Integer := bezoutLeftSteps(b, a, b)126def bezoutRight (a b : Nat) : Integer := bezoutRightSteps(b, a, b)127128theorem bezoutLeft.integer (a b : Nat)129  shows Integer(bezoutLeft(a, b))130proof131  unfold bezoutLeft132  exact bezoutLeftSteps.integer with *133134theorem bezoutRight.integer (a b : Nat)135  shows Integer(bezoutRight(a, b))136proof137  unfold bezoutRight138  exact bezoutRightSteps.integer with *139140theorem bezout.correct (a b : Nat)141  shows integerLinearCombination(bezoutLeft(a, b), bezoutRight(a, b), a, b) = integerOfNat(gcd(a, b))142proof143  have result := bezoutSteps.correct at b, a, b with *144  simpa [bezoutLeft, bezoutRight, gcd] using result145146theorem bezout.certificate (a b : Nat)147  shows IsGCD(a, b, gcd(a, b)) ∧148    integerLinearCombination(bezoutLeft(a, b), bezoutRight(a, b), a, b) = integerOfNat(gcd(a, b))149proof150  have gcd := gcd.correct at a, b with *151  have identity := bezout.correct at a, b with *152  refine ⟨gcd, identity⟩153154theorem bezoutLeft.zero_right (a : Nat)155  shows bezoutLeft(a, 0) = integerOfNat(1)156proof157  simp [bezoutLeft, bezoutLeftSteps.zero_right]158159theorem bezoutRight.zero_right (a : Nat)160  shows bezoutRight(a, 0) = integerOfNat(0)161proof162  simp [bezoutRight, bezoutRightSteps.zero_right]163164-- Bridge executable natural components to their existing quotient classes.165theorem bezoutLeft.representatives (a b p n : Nat)166  requires positive : bezoutComponent(b, a, b, Bool.false, Bool.true) = p167  requires negative : bezoutComponent(b, a, b, Bool.true, Bool.true) = n168  shows bezoutLeft(a, b) = integerClass(p, n)169proof170  simp [bezoutLeft, bezoutLeftSteps]171172theorem bezoutRight.representatives (a b p n : Nat)173  requires positive : bezoutComponent(b, a, b, Bool.false, Bool.false) = p174  requires negative : bezoutComponent(b, a, b, Bool.true, Bool.false) = n175  shows bezoutRight(a, b) = integerClass(p, n)176proof177  simp [bezoutRight, bezoutRightSteps]178