Grace/Cumulus/NumberTheory/ChineseRemainder.g17

Open in Workbench Download source

Imports

Coprime

Declarations

• IntegerDivides.coprime_product theorem derivation
• chineseCombination def
• chineseCombination.correct theorem derivation
• ChineseRemainder.exists theorem derivation
• ChineseRemainder.unique theorem derivation

Source

1-- The two-modulus Chinese remainder theorem over quotient integers2-- 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.ChineseRemainder8import Coprime910theorem IntegerDivides.coprime_product (m n z : Integer)11  requires coprime : IntegerCoprime(m, n)12  requires left : IntegerDivides(m, z)13  requires right : IntegerDivides(n, z)14  shows IntegerDivides(m * n, z)15proof16  obtain ⟨q, qInteger, equation⟩ := left17  have symmetric := IntegerCoprime.symmetric with *18  rw ← equation at right19  have quotient := IntegerCoprime.cancel with *20  obtain ⟨k, kInteger, factor⟩ := quotient21  witness k22  rw [← equation, ← factor]23  ring2425-- If u*m+v*n=1, then a*v*n+b*u*m has the prescribed residues.26def chineseCombination (m n a b u v : Integer) : Integer := a * v * n + b * u * m2728theorem chineseCombination.correct (m n a b u v : Integer)29  requires identity : u * m + v * n = integerOne30  shows IntegerCongruent(m, chineseCombination(m, n, a, b, u, v), a) ∧31    IntegerCongruent(n, chineseCombination(m, n, a, b, u, v), b)32proof33  constructor34    witness u * (b - a)35    unfold chineseCombination36    linear_combination -a * identity37    witness v * (a - b)38    unfold chineseCombination39    linear_combination -b * identity4041theorem ChineseRemainder.exists (m n a b : Integer)42  requires coprime : IntegerCoprime(m, n)43  shows ∃ x, Integer(x) ∧ IntegerCongruent(m, x, a) ∧ IntegerCongruent(n, x, b)44proof45  obtain ⟨u, uInteger, v, vInteger, identity⟩ := IntegerCoprime.bezout at m, n with *46  have integer := chineseCombination.type at m, n, a, b, u, v with *47  have residues := chineseCombination.correct at m, n, a, b, u, v with *48  witness chineseCombination(m, n, a, b, u, v)49  exact residues5051theorem ChineseRemainder.unique (m n a b x y : Integer)52  requires coprime : IntegerCoprime(m, n)53  requires xm : IntegerCongruent(m, x, a)54  requires xn : IntegerCongruent(n, x, b)55  requires ym : IntegerCongruent(m, y, a)56  requires yn : IntegerCongruent(n, y, b)57  shows IntegerCongruent(m * n, x, y)58proof59  have reverseM := IntegerCongruent.symmetric at m, y, a with *60  have reverseN := IntegerCongruent.symmetric at n, y, b with *61  have sameM := IntegerCongruent.transitive at m, x, a, y with *62  have sameN := IntegerCongruent.transitive at n, x, b, y with *63  unfold IntegerCongruent at sameM64  unfold IntegerCongruent at sameN65  unfold IntegerCongruent66  exact IntegerDivides.coprime_product with *67