GCDStarter

A Euclidean certificate through the public number-theory entrypoint

Open in Workbench View on GitHub

1-- A Euclidean certificate through the public number-theory entrypoint.2-- 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 GCDStarter8import Grace.Cumulus.NumberTheory910-- Each step is a checked equality; no GCD computation is trusted.11theorem euclidean_example12  shows IsGCD(252, 198, 18)13proof14  have terminal := IsGCD.zero_right at 18 with *15  have last : 36 = 18 * 2 + 016  . compute17  have third := IsGCD.euclidean_backward at 36, 18, 2, 0, 18 with *18  have secondEquation : 54 = 36 * 1 + 1819  . compute20  have second := IsGCD.euclidean_backward at 54, 36, 1, 18, 18 with *21  have firstEquation : 198 = 54 * 3 + 3622  . compute23  have first := IsGCD.euclidean_backward at 198, 54, 3, 36, 18 with *24  have start : 252 = 198 * 1 + 5425  . compute26  exact IsGCD.euclidean_backward at 252, 198, 1, 54, 18 with *2728theorem all_common_divisors (d : Nat)29  requires left : d ∣ 25230  requires right : d ∣ 19831  shows d ∣ 1832proof33  exact IsGCD.greatest with *{4}, euclidean_example, left, right3435theorem zero_pair36  shows IsGCD(0, 0, 0)37proof38  exact IsGCD.zero_right at 0 with *3940theorem divisible_pair (a b : Nat)41  shows IsGCD(a, a * b, a)42proof43  have self := divides.reflexive at a with *44  have multiple := divides.multiply_right at a, a, b with *45  exact IsGCD.of_divides at a, a * b with *4647-- Preservation also holds for zero divisors and noncanonical remainders.48theorem add_multiple (a b q g : Nat)49  requires gcd : IsGCD(a, b, g)50  shows IsGCD(b * q + a, b, g)51proof52  have reversed := IsGCD.symmetric at a, b, g with *53  have equation : b * q + a = b * q + a54  . rfl55  exact IsGCD.euclidean_backward at b * q + a, b, q, a, g with *565758-- The executable function is now correct for all natural inputs.59theorem executable_example60  shows gcd(252, 198) = 1861proof62  compute6364theorem certificate_agrees65  shows gcd(252, 198) = 1866proof67  simp6869theorem consecutive (n : Nat)70  shows gcd(n, succ(n)) = 171proof72  have natural := gcd.natural at n, succ(n) with *73  have left := gcd.divides_left at n, succ(n) with *74  have right := gcd.divides_right at n, succ(n) with *75  exact divides.consecutive_one at gcd(n, succ(n)), n with *76