ExtendedGCDStarter

Compute Bézout coefficients and use their general correctness theorem

Open in Workbench View on GitHub

1-- Compute Bézout coefficients and use their general correctness theorem2-- 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 Passmore67-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.8module ExtendedGCDStarter9import Grace.Cumulus.NumberTheory1011theorem all_inputs (a b : Nat)12  shows integerLinearCombination(bezoutLeft(a, b), bezoutRight(a, b), a, b) = integerOfNat(gcd(a, b))13proof14  exact bezout.correct at a, b with *1516-- The algorithm returns 4 and -5: 252*4 + 198*(-5) = 18.17theorem left_coefficient18  shows bezoutLeft(252, 198) = integerOfNat(4)19proof20  simp2122theorem right_coefficient23  shows bezoutRight(252, 198) = integerNegativeOfNat(5)24proof25  simp2627theorem gcd_value28  shows gcd(252, 198) = 1829proof30  compute3132theorem computed_identity33  shows integerLinearCombination(integerOfNat(4), integerNegativeOfNat(5), 252, 198) = integerOfNat(18)34proof35  have identity := bezout.correct at 252, 198 with *36  rw left_coefficient at identity37  rw right_coefficient at identity38  rw gcd_value at identity39  exact identity40