Grace/Cumulus/NumberTheory/IntegerGCD.g17

Open in Workbench Download source

Imports

ExtendedGCD

Declarations

Source

1-- GCD and Bézout for arbitrary quotient integer inputs2-- 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.IntegerGCD8import ExtendedGCD910predicate IntegerDivides (x y : Integer) := ∃ q, Integer(q) ∧ x * q = y1112theorem IntegerDivides.to_magnitudes (x y : Integer)13  requires divides : IntegerDivides(x, y)14  shows integerNatAbs(x) ∣ integerNatAbs(y)15proof16  obtain ⟨q, qInteger, equation⟩ := divides17  have qNat := integerNatAbs.natural at q with *18  have product := integerNatAbs.mul at x, q with *19  rw equation at product20  symm at product21  apply divides.definition.backward with *{2}22  refine ⟨integerNatAbs(q), qNat, product⟩2324theorem IntegerDivides.of_magnitudes (x y : Integer)25  requires divides : integerNatAbs(x) ∣ integerNatAbs(y)26  shows IntegerDivides(x, y)27proof28  obtain ⟨k, kNat, equation⟩ := divides.definition.forward at integerNatAbs(x), integerNatAbs(y) with *29  have xSign := integerNatAbs.cases at x with *30  obtain ⟨v, vInteger, adjusted⟩ := integerMulValue.sign_adjust at integerOfNat(k), x, integerNatAbs(x) with *31  have embedded := integerOfNat.mul at k, integerNatAbs(x) with *32  have naturalProduct : k * integerNatAbs(x) = integerNatAbs(y)33  . ring34  rw naturalProduct at embedded35  rw ← embedded at adjusted36  have swapped := integerMulValue.commutative at x, v with *37  rw adjusted at swapped38  have ySign := integerNatAbs.cases at y with *39  unfold IntegerDivides40  cases ySign with positive | negative41  . rw ← positive at swapped42    refine ⟨v, vInteger, swapped⟩43  . have vNegative := integerNegValue.integer at v with *44    have changed := integerMulValue.neg_right at x, v with *45    have flipped := integerOfNat.neg at integerNatAbs(y) with *46    rw [swapped, flipped, ← negative] at changed47    refine ⟨-v, vNegative, changed⟩4849theorem IntegerDivides.magnitude_iff (x y : Integer)50  shows IntegerDivides(x, y) ↔ integerNatAbs(x) ∣ integerNatAbs(y)51proof52  constructor53  . intro divides54    exact IntegerDivides.to_magnitudes with *55  . intro divides56    exact IntegerDivides.of_magnitudes with *5758-- Return the canonical nonnegative GCD as a natural magnitude.59def integerGCD (x y : Integer) : Nat := gcd(integerNatAbs(x), integerNatAbs(y))6061theorem integerGCD.natural (x y : Integer)62  shows Nat(integerGCD(x, y))63proof64  unfold integerGCD65  exact gcd.natural with *6667theorem integerGCD.magnitudes (x y : Integer)68  shows IsGCD(integerNatAbs(x), integerNatAbs(y), integerGCD(x, y))69proof70  have correct := gcd.correct at integerNatAbs(x), integerNatAbs(y) with *71  simpa [integerGCD] using correct7273theorem integerGCD.divides_left (x y : Integer)74  shows IntegerDivides(integerOfNat(integerGCD(x, y)), x)75proof76  have correct := integerGCD.magnitudes at x, y with *77  have divides := IsGCD.divides_left with *78  apply IntegerDivides.of_magnitudes with *{2}79  simpa [integerNatAbs.ofNat] using divides8081theorem integerGCD.divides_right (x y : Integer)82  shows IntegerDivides(integerOfNat(integerGCD(x, y)), y)83proof84  have correct := integerGCD.magnitudes at x, y with *85  have divides := IsGCD.divides_right with *86  apply IntegerDivides.of_magnitudes with *{2}87  simpa [integerNatAbs.ofNat] using divides8889theorem integerGCD.greatest (x y d : Integer)90  requires left : IntegerDivides(d, x)91  requires right : IntegerDivides(d, y)92  shows IntegerDivides(d, integerOfNat(integerGCD(x, y)))93proof94  have leftMagnitude := IntegerDivides.to_magnitudes at d, x with *95  have rightMagnitude := IntegerDivides.to_magnitudes at d, y with *96  have correct := integerGCD.magnitudes at x, y with *97  have divides := IsGCD.greatest with *98  apply IntegerDivides.of_magnitudes with *{2}99  simpa [integerNatAbs.ofNat] using divides100101theorem integerGCD.bezout (x y : Integer)102  shows ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧ u * x + v * y = integerOfNat(integerGCD(x, y))103proof104  have identity := bezout.correct at integerNatAbs(x), integerNatAbs(y) with *105  have xSign := integerNatAbs.cases at x with *106  have ySign := integerNatAbs.cases at y with *107  obtain ⟨u, uInteger, leftProduct⟩ := integerMulValue.sign_adjust at bezoutLeft(integerNatAbs(x), integerNatAbs(y)), x, integerNatAbs(x) with *108  obtain ⟨v, vInteger, rightProduct⟩ := integerMulValue.sign_adjust at bezoutRight(integerNatAbs(x), integerNatAbs(y)), y, integerNatAbs(y) with *109  witness u110  witness v111  rw [leftProduct, rightProduct]112  simpa [integerLinearCombination, integerGCD] using identity113114theorem integerGCD.ofNat (a b : Nat)115  shows integerGCD(integerOfNat(a), integerOfNat(b)) = gcd(a, b)116proof117  simp [integerGCD, integerNatAbs.ofNat]118119theorem integerGCD.neg_left (x y : Integer)120  shows integerGCD(-x, y) = integerGCD(x, y)121proof122  simp [integerGCD, integerNatAbs.neg]123124theorem integerGCD.neg_right (x y : Integer)125  shows integerGCD(x, -y) = integerGCD(x, y)126proof127  simp [integerGCD, integerNatAbs.neg]128129theorem IntegerDivides.natural_left (d : Nat, x : Integer)130  shows IntegerDivides(integerOfNat(d), x) ↔ d ∣ integerNatAbs(x)131proof132  have equivalence := IntegerDivides.magnitude_iff at integerOfNat(d), x with *133  simpa [integerNatAbs.ofNat] using equivalence134135predicate IsIntegerGCD (x y : Integer, g : Nat) :=136  IntegerDivides(integerOfNat(g), x) ∧ IntegerDivides(integerOfNat(g), y) ∧137    (∀ d, Integer(d) → IntegerDivides(d, x) → IntegerDivides(d, y) → IntegerDivides(d, integerOfNat(g)))138139theorem integerGCD.correct (x y : Integer)140  shows IsIntegerGCD(x, y, integerGCD(x, y))141proof142  have left := integerGCD.divides_left at x, y with *143  have right := integerGCD.divides_right at x, y with *144  constructor145  . exact left146  . constructor147    . exact right148    . intros d dInteger dLeft dRight149      exact integerGCD.greatest with *150151theorem IsIntegerGCD.magnitudes (x y : Integer, g : Nat)152  requires certificate : IsIntegerGCD(x, y, g)153  shows IsGCD(integerNatAbs(x), integerNatAbs(y), g)154proof155  rcases certificate with ⟨left, right, greatest⟩156  have leftMagnitude := IntegerDivides.natural_left.forward at g, x with *157  have rightMagnitude := IntegerDivides.natural_left.forward at g, y with *158  apply IsGCD.intro with leftMagnitude, rightMagnitude159  intros d dNat dLeft dRight160  have leftInteger := IntegerDivides.natural_left.backward at d, x with *161  have rightInteger := IntegerDivides.natural_left.backward at d, y with *162  have common := greatest with integerOfNat(d), leftInteger, rightInteger163  have magnitude := IntegerDivides.to_magnitudes at integerOfNat(d), integerOfNat(g) with *164  simpa [integerNatAbs.ofNat] using magnitude165166theorem IsIntegerGCD.unique (x y : Integer, g h : Nat)167  requires first : IsIntegerGCD(x, y, g)168  requires second : IsIntegerGCD(x, y, h)169  shows g = h170proof171  have firstMagnitude := IsIntegerGCD.magnitudes at x, y, g with *172  have secondMagnitude := IsIntegerGCD.magnitudes at x, y, h with *173  exact IsGCD.unique with *174175theorem integerGCD.unique (x y : Integer, g : Nat)176  requires certificate : IsIntegerGCD(x, y, g)177  shows integerGCD(x, y) = g178proof179  have correct := integerGCD.correct at x, y with *180  exact IsIntegerGCD.unique with *181182theorem integerGCD.commutative (x y : Integer)183  shows integerGCD(x, y) = integerGCD(y, x)184proof185  have commute := gcd.commutative at integerNatAbs(x), integerNatAbs(y) with *186  simpa [integerGCD] using commute187188theorem integerGCD.zero_right (x : Integer)189  shows integerGCD(x, integerZero) = integerNatAbs(x)190proof191  simp [integerGCD, integerNatAbs.zero, gcd.zero_right]192193theorem integerGCD.zero_left (x : Integer)194  shows integerGCD(integerZero, x) = integerNatAbs(x)195proof196  simp [integerGCD, integerNatAbs.zero, gcd.zero_left]197