Grace/Cumulus/NumberTheory/Euclidean.g17

Open in Workbench Download source

Imports

GCD · Nat.Division

Declarations

• gcdSteps def
• gcd def
• gcdSteps.zero_right theorem derivation
• gcdSteps.successor theorem derivation
• gcdSteps.natural theorem derivation
• gcdSteps.correct theorem derivation
• gcd.natural theorem derivation
• gcd.correct theorem derivation
• gcd.unique theorem derivation
• IsGCD.exists theorem derivation
• gcd.zero_right theorem derivation
• gcd.zero_left theorem derivation
• gcd.commutative theorem derivation
• gcd.divides_left theorem derivation
• gcd.divides_right theorem derivation
• gcd.greatest theorem derivation
• gcd.euclidean theorem derivation
• gcd.of_divides theorem derivation
• gcd.zero_iff theorem derivation

Source

1-- Executable Euclidean GCD with a proved sufficient iteration bound2-- 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.Euclidean8import GCD9import Nat.Division1011-- The second input strictly decreases on each nonterminal Euclidean step.12-- The public function uses b steps; correctness below proves this sufficient.13def gcdSteps (fuel a b : Nat) → Nat14  | zero, a, b => a15  | succ(fuel), a, b => chooseNat(isZero(b), a, gcdSteps(fuel, b, a % b))1617def gcd (a b : Nat) : Nat := gcdSteps(b, a, b)1819theorem gcdSteps.zero_right (a fuel : Nat)20  shows gcdSteps(fuel, a, 0) = a21proof22  induction fuel23  | zero => settle with gcdSteps24  | succ(k) using ih => settle with gcdSteps, isZero, chooseNat2526theorem gcdSteps.successor (fuel a b : Nat)27  shows gcdSteps(succ(fuel), a, succ(b)) = gcdSteps(fuel, succ(b), a % succ(b))28proof29  simp [gcdSteps, isZero, chooseNat]3031theorem gcdSteps.natural (fuel a b : Nat)32  shows Nat(gcdSteps(fuel, a, b))33proof34  induction fuel generalizing a b35  | zero =>36    intros a b aNat bNat37    simp [gcdSteps, isZero, chooseNat]38  | succ(k) using ih =>39    intros a b aNat bNat40    have remainderNat := mod.natural at b, a with *41    have recursive := ih with b, a % b, bNat, remainderNat42    have boolean := isZero.boolean at b with *43    have natural := chooseNat.natural at isZero(b), a, gcdSteps(k, b, a % b) with *44    simpa [gcdSteps] using natural4546theorem gcdSteps.correct (fuel a b : Nat)47  shows b ≤ fuel → IsGCD(a, b, gcdSteps(fuel, a, b))48proof49  induction fuel generalizing a b50  | zero =>51    intros a b aNat bNat bound52    have bZero : b = 053    . have lower := Grace.Cumulus.Nat.Order.LessEqual.zero at b with *54      exact LessEqual.antisymmetric at b, 0 with *55    rw bZero56    have terminal := IsGCD.zero_right at a with *57    simpa [gcdSteps, isZero, chooseNat] using terminal58  | 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    . rw zero63      have terminal := IsGCD.zero_right at a with *64      have value := gcdSteps.zero_right at a, succ(k) with *65      rwa value66    . obtain ⟨j, jNat, bShape⟩ := successor67      rw bShape at bound68      rw 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      have recursive := ih with succ(j), a % succ(j), assumption, remainderNat, enough79      obtain ⟨q, qNat, equation⟩ := mod.equation at a, succ(j) with *80      have preserved := IsGCD.euclidean_backward at a, succ(j), q, a % succ(j), gcdSteps(k, succ(j), a % succ(j)) with *81      have value := gcdSteps.successor at k, a, j with *82      rwa value8384theorem gcd.natural (a b : Nat)85  shows Nat(gcd(a, b))86proof87  unfold gcd88  exact gcdSteps.natural with *8990theorem gcd.correct (a b : Nat)91  shows IsGCD(a, b, gcd(a, b))92proof93  have bound := LessEqual.reflexive at b with *94  have correct := gcdSteps.correct at b, a, b with *, bound95  simpa [gcd] using correct9697theorem gcd.unique (a b g : Nat)98  requires certificate : IsGCD(a, b, g)99  shows gcd(a, b) = g100proof101  have correct := gcd.correct at a, b with *102  exact IsGCD.unique with *103104theorem IsGCD.exists (a b : Nat)105  shows ∃ g, Nat(g) ∧ IsGCD(a, b, g)106proof107  have natural := gcd.natural at a, b with *108  have correct := gcd.correct at a, b with *109  refine ⟨gcd(a, b), natural, correct⟩110111theorem gcd.zero_right (a : Nat)112  shows gcd(a, 0) = a113proof114  have certificate := IsGCD.zero_right with *115  exact gcd.unique with *116117theorem gcd.zero_left (a : Nat)118  shows gcd(0, a) = a119proof120  have certificate := IsGCD.zero_left with *121  exact gcd.unique with *122123theorem gcd.commutative (a b : Nat)124  shows gcd(a, b) = gcd(b, a)125proof126  have reverse := gcd.correct at b, a with *127  have certificate := IsGCD.symmetric with *128  exact gcd.unique with *129130theorem gcd.divides_left (a b : Nat)131  shows gcd(a, b) ∣ a132proof133  have correct := gcd.correct at a, b with *134  exact IsGCD.divides_left with *135136theorem gcd.divides_right (a b : Nat)137  shows gcd(a, b) ∣ b138proof139  have correct := gcd.correct at a, b with *140  exact IsGCD.divides_right with *141142theorem gcd.greatest (a b d : Nat)143  requires left : d ∣ a144  requires right : d ∣ b145  shows d ∣ gcd(a, b)146proof147  have correct := gcd.correct at a, b with *148  exact IsGCD.greatest with *149150theorem gcd.euclidean (a b : Nat)151  requires nonzero : b ≠ 0152  shows gcd(a, b) = gcd(b, a % b)153proof154  have recursive := gcd.correct at b, a % b with *155  obtain ⟨q, qNat, equation⟩ := mod.equation at a, b with *156  have certificate := IsGCD.euclidean_backward with *157  exact gcd.unique with *158159theorem gcd.of_divides (a b : Nat)160  requires divides : a ∣ b161  shows gcd(a, b) = a162proof163  have certificate := IsGCD.of_divides with *164  exact gcd.unique with *165166theorem gcd.zero_iff (a b : Nat)167  shows gcd(a, b) = 0 ↔ (a = 0 ∧ b = 0)168proof169  constructor170  . intro zero171    have left := gcd.divides_left at a, b with *172    have right := gcd.divides_right at a, b with *173    rw zero at left174    rw zero at right175    have aZero := zero.divides_only_zero at a with *176    have bZero := zero.divides_only_zero at b with *177    tauto178  . intro zeros179    rcases zeros with ⟨aZero, bZero⟩180    rw [aZero, bZero]181    exact gcd.zero_right with *182