Grace/Cumulus/NumberTheory/GCD.g17

Open in Workbench Download source

Imports

Divisibility

Declarations

Source

1-- Greatest common divisors and Euclidean transformations2-- 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.GCD8import Divisibility910-- Greatest in the divisibility order. This includes IsGCD(0, 0, 0).11-- Existence and an executable algorithm are separate from this specification.12predicate IsGCD (a b g : Nat) :=13  g ∣ a ∧ g ∣ b ∧ (∀ d, Nat(d) → d ∣ a → d ∣ b → d ∣ g)1415theorem IsGCD.divides_left (a b g : Nat)16  requires gcd : IsGCD(a, b, g)17  shows g ∣ a18proof19  simp [IsGCD]2021theorem IsGCD.divides_right (a b g : Nat)22  requires gcd : IsGCD(a, b, g)23  shows g ∣ b24proof25  simp [IsGCD]2627theorem IsGCD.greatest (a b g d : Nat)28  requires gcd : IsGCD(a, b, g)29  requires left : d ∣ a30  requires right : d ∣ b31  shows d ∣ g32proof33  simp [IsGCD]3435theorem IsGCD.intro (a b g : Nat)36  requires left : g ∣ a37  requires right : g ∣ b38  requires greatest : ∀ d, Nat(d) → d ∣ a → d ∣ b → d ∣ g39  shows IsGCD(a, b, g)40proof41  simp [IsGCD]4243theorem IsGCD.unique (a b g h : Nat)44  requires first : IsGCD(a, b, g)45  requires second : IsGCD(a, b, h)46  shows g = h47proof48  have ga := IsGCD.divides_left at a, b, g with *49  have gb := IsGCD.divides_right at a, b, g with *50  have ha := IsGCD.divides_left at a, b, h with *51  have hb := IsGCD.divides_right at a, b, h with *52  have gh := IsGCD.greatest at a, b, h, g with *53  have hg := IsGCD.greatest at a, b, g, h with *54  exact divides.antisymmetric with *5556theorem IsGCD.symmetric (a b g : Nat)57  requires gcd : IsGCD(a, b, g)58  shows IsGCD(b, a, g)59proof60  have left := IsGCD.divides_left with *61  have right := IsGCD.divides_right with *62  apply IsGCD.intro with right, left63  intros d dNat db da64  exact IsGCD.greatest with *6566theorem IsGCD.zero_right (a : Nat)67  shows IsGCD(a, 0, a)68proof69  have self := divides.reflexive with *70  have zero := divides.zero with *71  apply IsGCD.intro with self, zero72  intros d dNat da dz73  exact da7475theorem IsGCD.zero_left (a : Nat)76  shows IsGCD(0, a, a)77proof78  have right := IsGCD.zero_right with *79  exact IsGCD.symmetric with *8081theorem IsGCD.of_divides (a b : Nat)82  requires divides : a ∣ b83  shows IsGCD(a, b, a)84proof85  have self := divides.reflexive at a with *86  apply IsGCD.intro with self, divides87  intros d dNat da db88  exact da8990-- A single invariant covers subtraction and quotient/remainder algorithms.91-- No remainder bound is needed for preservation, only for termination.92theorem IsGCD.euclidean_forward (a b q r g : Nat)93  requires equation : a = b * q + r94  requires gcd : IsGCD(a, b, g)95  shows IsGCD(b, r, g)96proof97  have ga := IsGCD.divides_left with *98  have gb := IsGCD.divides_right with *99  have equivalence := divides.remainder_iff with *100  have gr : g ∣ r101  . tauto102  apply IsGCD.intro with gb, gr103  intros d dNat db dr104  have commonDivisor := divides.remainder_iff at d, a, b, q, r with *105  have da : d ∣ a106  . tauto107  exact IsGCD.greatest with *108109theorem IsGCD.euclidean_backward (a b q r g : Nat)110  requires equation : a = b * q + r111  requires gcd : IsGCD(b, r, g)112  shows IsGCD(a, b, g)113proof114  have gb := IsGCD.divides_left with *115  have gr := IsGCD.divides_right with *116  have equivalence := divides.remainder_iff with *117  have ga : g ∣ a118  . tauto119  apply IsGCD.intro with ga, gb120  intros d dNat da db121  have commonDivisor := divides.remainder_iff at d, a, b, q, r with *122  have dr : d ∣ r123  . tauto124  exact IsGCD.greatest with *125126theorem IsGCD.euclidean_iff (a b q r g : Nat)127  requires equation : a = b * q + r128  shows IsGCD(a, b, g) ↔ IsGCD(b, r, g)129proof130  constructor131  . intro gcd132    exact IsGCD.euclidean_forward with *133  . intro gcd134    exact IsGCD.euclidean_backward with *135136theorem IsGCD.add_right_iff (a b g : Nat)137  shows IsGCD(a + b, b, g) ↔ IsGCD(a, b, g)138proof139  have equation : a + b = b * 1 + a140  . ring141  have step := IsGCD.euclidean_iff at a + b, b, 1, a, g with *142  constructor143  . intro gcd144    have reversed : IsGCD(b, a, g)145    . tauto146    exact IsGCD.symmetric with *147  . intro gcd148    have reversed := IsGCD.symmetric with *149    tauto150