Grace/Cumulus/NumberTheory/Coprime.g17

Open in Workbench Download source

Imports

IntegerGCD

Declarations

• IntegerCoprime predicate
• IntegerCongruent predicate
• IntegerDivides.linear_combination theorem derivation
• IntegerCoprime.symmetric theorem derivation
• IntegerCoprime.bezout theorem derivation
• IntegerCoprime.cancel theorem derivation
• IntegerCongruent.reflexive theorem derivation
• IntegerCongruent.symmetric theorem derivation
• IntegerCongruent.transitive theorem derivation
• IntegerCoprime.modular_inverse theorem derivation
• IntegerCoprime.of_bezout theorem derivation
• IntegerCoprime.of_modular_inverse theorem derivation
• IntegerCoprime.modular_inverse_iff theorem derivation
• IntegerCongruent.add theorem derivation
• IntegerCongruent.mul theorem derivation
• IntegerCongruent.cancel_coprime theorem derivation
• IntegerCongruent.inverse_unique theorem derivation
• IntegerCongruent.of_natural_difference theorem derivation

Source

1-- Coprime cancellation and modular inverses from Bézout2-- 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.Coprime8import IntegerGCD910predicate IntegerCoprime (a b : Integer) := integerGCD(a, b) = 111predicate IntegerCongruent (m a b : Integer) := IntegerDivides(m, a - b)1213theorem IntegerDivides.linear_combination (d a b u v : Integer)14  requires left : IntegerDivides(d, a)15  requires right : IntegerDivides(d, b)16  shows IntegerDivides(d, u * a + v * b)17proof18  obtain ⟨p, pInteger, leftEquation⟩ := left19  obtain ⟨q, qInteger, rightEquation⟩ := right20  witness u * p + v * q21  rw [← leftEquation, ← rightEquation]22  ring2324theorem IntegerCoprime.symmetric (a b : Integer)25  requires coprime : IntegerCoprime(a, b)26  shows IntegerCoprime(b, a)27proof28  unfold IntegerCoprime29  rw integerGCD.commutative30  exact coprime3132theorem IntegerCoprime.bezout (a b : Integer)33  requires coprime : IntegerCoprime(a, b)34  shows ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧ u * a + v * b = integerOne35proof36  have identity := integerGCD.bezout at a, b with *37  unfold IntegerCoprime at coprime38  simpa [coprime, integerOne] using identity3940-- Euclid's coprime cancellation lemma, with an explicit quotient witness.41theorem IntegerCoprime.cancel (a b c : Integer)42  requires coprime : IntegerCoprime(a, b)43  requires divides : IntegerDivides(a, b * c)44  shows IntegerDivides(a, c)45proof46  obtain ⟨u, uInteger, v, vInteger, identity⟩ := IntegerCoprime.bezout at a, b with *47  obtain ⟨q, qInteger, equation⟩ := divides48  have scaled : (u * a + v * b) * c = c49  . rw identity50    ring51  witness u * c + v * q52  linear_combination scaled + v * equation5354theorem IntegerCongruent.reflexive (m a : Integer)55  shows IntegerCongruent(m, a, a)56proof57  witness integerZero58  ring5960theorem IntegerCongruent.symmetric (m a b : Integer)61  requires congruent : IntegerCongruent(m, a, b)62  shows IntegerCongruent(m, b, a)63proof64  obtain ⟨q, qInteger, equation⟩ := congruent65  witness -q66  linear_combination -equation6768theorem IntegerCongruent.transitive (m a b c : Integer)69  requires first : IntegerCongruent(m, a, b)70  requires second : IntegerCongruent(m, b, c)71  shows IntegerCongruent(m, a, c)72proof73  obtain ⟨p, pInteger, left⟩ := first74  obtain ⟨q, qInteger, right⟩ := second75  witness p + q76  linear_combination left + right7778-- Every integer coprime to the modulus has a multiplicative inverse modulo it.79theorem IntegerCoprime.modular_inverse (a m : Integer)80  requires coprime : IntegerCoprime(a, m)81  shows ∃ u, Integer(u) ∧ IntegerCongruent(m, a * u, integerOne)82proof83  obtain ⟨u, uInteger, v, vInteger, identity⟩ := IntegerCoprime.bezout at a, m with *84  witness u85  witness -v86  linear_combination -identity8788theorem IntegerCoprime.of_bezout (a b u v : Integer)89  requires identity : u * a + v * b = integerOne90  shows IntegerCoprime(a, b)91proof92  have left := integerGCD.divides_left at a, b with *93  have right := integerGCD.divides_right at a, b with *94  have divides := IntegerDivides.linear_combination at integerOfNat(integerGCD(a, b)), a, b, u, v with *95  rw identity at divides96  have magnitude := IntegerDivides.natural_left.forward at integerGCD(a, b), integerOne with *97  simp [integerOne, integerNatAbs.ofNat] at magnitude98  unfold IntegerCoprime99  exact divides.one_only with *100101theorem IntegerCoprime.of_modular_inverse (a m u : Integer)102  requires inverse : IntegerCongruent(m, a * u, integerOne)103  shows IntegerCoprime(a, m)104proof105  obtain ⟨q, qInteger, equation⟩ := inverse106  apply IntegerCoprime.of_bezout at a, m, u, -q with *{4}107  linear_combination -equation108109theorem IntegerCoprime.modular_inverse_iff (a m : Integer)110  shows IntegerCoprime(a, m) ↔ ∃ u, Integer(u) ∧ IntegerCongruent(m, a * u, integerOne)111proof112  constructor113  . intro coprime114    exact IntegerCoprime.modular_inverse with *115  . intro exists116    obtain ⟨u, uInteger, inverse⟩ := exists117    exact IntegerCoprime.of_modular_inverse with *118119theorem IntegerCongruent.add (m a b c d : Integer)120  requires first : IntegerCongruent(m, a, b)121  requires second : IntegerCongruent(m, c, d)122  shows IntegerCongruent(m, a + c, b + d)123proof124  obtain ⟨p, pInteger, left⟩ := first125  obtain ⟨q, qInteger, right⟩ := second126  witness p + q127  linear_combination left + right128129theorem IntegerCongruent.mul (m a b c d : Integer)130  requires first : IntegerCongruent(m, a, b)131  requires second : IntegerCongruent(m, c, d)132  shows IntegerCongruent(m, a * c, b * d)133proof134  obtain ⟨p, pInteger, left⟩ := first135  obtain ⟨q, qInteger, right⟩ := second136  witness p * c + b * q137  linear_combination c * left + b * right138139theorem IntegerCongruent.cancel_coprime (m a b c : Integer)140  requires coprime : IntegerCoprime(m, a)141  requires congruent : IntegerCongruent(m, a * b, a * c)142  shows IntegerCongruent(m, b, c)143proof144  unfold IntegerCongruent at congruent145  have distribution : a * b - a * c = a * (b - c)146  . ring147  rw distribution at congruent148  unfold IntegerCongruent149  exact IntegerCoprime.cancel with *150151theorem IntegerCongruent.inverse_unique (m a u v : Integer)152  requires first : IntegerCongruent(m, a * u, integerOne)153  requires second : IntegerCongruent(m, a * v, integerOne)154  shows IntegerCongruent(m, u, v)155proof156  have coprime := IntegerCoprime.of_modular_inverse at a, m, u with *157  have symmetric := IntegerCoprime.symmetric with *158  have reverse := IntegerCongruent.symmetric at m, a * v, integerOne with *159  have same := IntegerCongruent.transitive at m, a * u, integerOne, a * v with *160  exact IntegerCongruent.cancel_coprime with *161162-- Ground natural arithmetic can certify a congruence of embedded integers.163theorem IntegerCongruent.of_natural_difference (m a b q : Nat)164  requires equation : a = b + m * q165  shows IntegerCongruent(integerOfNat(m), integerOfNat(a), integerOfNat(b))166proof167  witness integerOfNat(q)168  simp [integerOfNat.add, integerOfNat.mul]169  ring170