Grace/Cumulus/NumberTheory/Modular.g17

Open in Workbench Download source

Imports

Nat.Division · Divisibility

Declarations

• mod.succ_wrap theorem derivation
• mod.succ_advance theorem derivation
• mod.unique_aux theorem derivation
• mod.unique theorem derivation
• mod.of_less theorem derivation
• mod.mod theorem derivation
• mod.add_multiple theorem derivation
• mod.add theorem derivation
• mod.mul theorem derivation
• mod.mul_left theorem derivation
• mod.mul_right theorem derivation
• mod.zero_iff theorem derivation
• mod.add_cancel theorem derivation

Source

1-- Modular arithmetic on the natural numbers: the remainder is determined by2-- the division equation, so remainders of sums and products reduce to the3-- remainders of their parts, and a vanishing remainder means divisibility4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.NumberTheory.Modular10import Nat.Division11import Divisibility1213-- One step of the remainder: it wraps to zero exactly at the modulus.14theorem mod.succ_wrap (n k : Nat)15  requires wraps : succ(k % n) = n16  shows succ(k) % n = 017proof18  have condition := equalNat.true_iff.backward with wraps19  simp [mod, nextRemainder, equalNat.reflexive, condition, chooseNat]2021theorem mod.succ_advance (n k : Nat)22  requires advances : succ(k % n) ≠ n23  shows succ(k) % n = succ(k % n)24proof25  have condition := equalNat.false_iff.backward with advances26  simp [mod, nextRemainder, equalNat.reflexive, condition, chooseNat]2728-- The remainder is the unique r < n with a = n·q + r.29theorem mod.unique_aux (n a : Nat)30  requires nonzero : n ≠ 031  shows ∀ q, Nat(q) → ∀ r, Nat(r) → a = n * q + r → r < n → a % n = r32proof33  induction a34  | zero =>35    intros q qNat r rNat equation bound36    have parts := add.eq_zero at r, n * q37    symm at equation38    have both := parts with equation39    have rZero := both.right40    rw rZero41    exact mod.zero_left at n42  | succ(k) using ih =>43    intros q qNat r rNat equation bound44    have shape := natural.zero_or_successor at r45    cases shape with rZero | rSucc46    . have qShape := natural.zero_or_successor at q47      cases qShape with qZero | qSucc48      . exfalso49        rw [rZero, qZero] at equation50        have zero : n * 0 + 0 = 0 by ring51        rw zero at equation52        have notSucc : succ(k) ≠ 0 by arith53        exact notSucc with equation54      . obtain ⟨qB, qBNat, qForm⟩ := qSucc55        have nShape := natural.zero_or_successor at n56        cases nShape with nZero | nSucc57        . exfalso58          exact nonzero with nZero59        . obtain ⟨p, pNat, nForm⟩ := nSucc60          rw [rZero, qForm] at equation61          have expand : n * succ(qB) + 0 = (n * qB + p) + 162            rw nForm63            ring64          rw expand at equation65          have unfoldK : succ(k) = k + 1 by ring66          rw unfoldK at equation67          have cancel := add.right_cancel at k, n * qB + p, 168          have previous := cancel with equation69          have pBelow : p < n70            rw nForm71            arith72          have remainder := ih with qB, qBNat, p, pNat, previous, pBelow73          have wraps : succ(k % n) = n74            rw [remainder, nForm]75            rfl76          have wrap := mod.succ_wrap at n, k with wraps77          rw [wrap, rZero]78          rfl79    . obtain ⟨rP, rPNat, rForm⟩ := rSucc80      rw rForm at equation81      rw rForm at bound82      have unfoldK : succ(k) = k + 1 by ring83      have unfoldR : n * q + succ(rP) = (n * q + rP) + 1 by ring84      rw [unfoldK, unfoldR] at equation85      have cancel := add.right_cancel at k, n * q + rP, 186      have previous := cancel with equation87      have rPBelow : rP < n by arith88      have remainder := ih with q, qNat, rP, rPNat, previous, rPBelow89      have different : succ(k % n) ≠ n90        intro same91        rw remainder at same92        rw same at bound93        exact Less.irreflexive at n with *, bound94      have advance := mod.succ_advance at n, k with different95      rw [advance, remainder, rForm]96      rfl9798theorem mod.unique (n a q r : Nat)99  requires nonzero : n ≠ 0100  requires equation : a = n * q + r101  requires bound : r < n102  shows a % n = r103proof104  have all := mod.unique_aux at n, a with nonzero105  have qNat : Nat(q) by typecheck106  have rNat : Nat(r) by typecheck107  exact all with q, r, equation, bound108109theorem mod.of_less (n a : Nat)110  requires bound : a < n111  shows a % n = a112proof113  have nonzero : n ≠ 0114    intro zero115    rw zero at bound116    have impossible : ¬a < 0 by arith117    exact impossible with bound118  have equation : a = n * 0 + a by ring119  exact mod.unique with nonzero, equation, bound120121theorem mod.mod (n a : Nat)122  requires nonzero : n ≠ 0123  shows (a % n) % n = a % n124proof125  have bound := mod.less at a, n with nonzero126  exact mod.of_less with bound127128theorem mod.add_multiple (n a s : Nat)129  requires nonzero : n ≠ 0130  shows (a + n * s) % n = a % n131proof132  obtain ⟨q, qNat, equation⟩ := mod.equation at a, n with nonzero133  have bound := mod.less at a, n with nonzero134  have shifted : a + n * s = n * (q + s) + a % n135    have same : a + n * s = (n * q + a % n) + n * s136      rw ← equation137      rfl138    rw same139    ring140  exact mod.unique with nonzero, shifted, bound141142theorem mod.add (n a b : Nat)143  requires nonzero : n ≠ 0144  shows (a + b) % n = (a % n + b % n) % n145proof146  obtain ⟨q, qNat, eqA⟩ := mod.equation at a, n with nonzero147  obtain ⟨qB, qBNat, eqB⟩ := mod.equation at b, n with nonzero148  obtain ⟨qS, qSNat, eqS⟩ := mod.equation at a % n + b % n, n with nonzero149  have bound := mod.less at a % n + b % n, n with nonzero150  have combined : a + b = n * (q + qB + qS) + (a % n + b % n) % n151    have same : a + b = (n * q + a % n) + (n * qB + b % n)152      rw [← eqA, ← eqB]153      rfl154    have expand : n * (q + qB + qS) + (a % n + b % n) % n = n * q + n * qB + (n * qS + (a % n + b % n) % n) by ring155    rw [same, expand, ← eqS]156    ring157  exact mod.unique with nonzero, combined, bound158159theorem mod.mul (n a b : Nat)160  requires nonzero : n ≠ 0161  shows (a * b) % n = ((a % n) * (b % n)) % n162proof163  obtain ⟨q, qNat, eqA⟩ := mod.equation at a, n with nonzero164  obtain ⟨qB, qBNat, eqB⟩ := mod.equation at b, n with nonzero165  obtain ⟨qS, qSNat, eqP⟩ := mod.equation at (a % n) * (b % n), n with nonzero166  have bound := mod.less at (a % n) * (b % n), n with nonzero167  have combined : a * b = n * (n * q * qB + q * (b % n) + (a % n) * qB + qS) + ((a % n) * (b % n)) % n168    have same : a * b = (n * q + a % n) * (n * qB + b % n)169      rw [← eqA, ← eqB]170      rfl171    have expand : n * (n * q * qB + q * (b % n) + (a % n) * qB + qS) + ((a % n) * (b % n)) % n = n * (n * q * qB + q * (b % n) + (a % n) * qB) + (n * qS + ((a % n) * (b % n)) % n) by ring172    rw [same, expand, ← eqP]173    ring174  exact mod.unique with nonzero, combined, bound175176theorem mod.mul_left (n a b : Nat)177  requires nonzero : n ≠ 0178  shows ((a % n) * b) % n = (a * b) % n179proof180  have first := mod.mul at n, a % n, b with nonzero181  have second := mod.mul at n, a, b with nonzero182  have idempotent := mod.mod at n, a with nonzero183  rw [first, idempotent, second]184  rfl185186theorem mod.mul_right (n a b : Nat)187  requires nonzero : n ≠ 0188  shows (a * (b % n)) % n = (a * b) % n189proof190  have first := mod.mul at n, a, b % n with nonzero191  have second := mod.mul at n, a, b with nonzero192  have idempotent := mod.mod at n, b with nonzero193  rw [first, idempotent, second]194  rfl195196theorem mod.zero_iff (n a : Nat)197  requires nonzero : n ≠ 0198  shows a % n = 0 ↔ n ∣ a199proof200  constructor201  . intro zero202    obtain ⟨q, qNat, equation⟩ := mod.equation at a, n with nonzero203    rw zero at equation204    witness q205    rw equation206    ring207  . intro divides208    obtain ⟨k, kNat, equation⟩ := divides209    have shape : a = n * k + 0210      rw ← equation211      ring212    have positive : 0 < n213      have alternatives := natural.zero_or_successor at n214      cases alternatives with zero | successor215      . exfalso216        exact nonzero with zero217      . obtain ⟨p, pNat, form⟩ := successor218        rw form219        arith220    exact mod.unique with nonzero, shape, positive221222-- Adding c does not change the remainder exactly when n divides c.223theorem mod.add_cancel (n b c : Nat)224  requires nonzero : n ≠ 0225  requires same : (b + c) % n = b % n226  shows n ∣ c227proof228  obtain ⟨q, qNat, eqB⟩ := mod.equation at b, n with nonzero229  obtain ⟨qB, qBNat, eqS⟩ := mod.equation at b + c, n with nonzero230  rw same at eqS231  have expanded : (n * q + c) + b % n = n * qB + b % n232    have arranged : (n * q + c) + b % n = (n * q + b % n) + c by ring233    rwa [arranged, ← eqB]234  have cancel := add.right_cancel at n * q + c, n * qB, b % n235  have reduced := cancel with expanded236  have total := LessEqual.total at q, qB237  cases total with below | above238  . obtain ⟨d, dNat, shape⟩ := below239    rw ← shape at reduced240    have expand : n * (q + d) = n * q + n * d by ring241    rw expand at reduced242    have cancel2 := add.left_cancel at c, n * d, n * q243    have form := cancel2 with reduced244    witness d245    rw form246    rfl247  . obtain ⟨d, dNat, shape⟩ := above248    rw ← shape at reduced249    have expand : n * (qB + d) = n * qB + n * d by ring250    rw expand at reduced251    have shifted : n * qB + (n * d + c) = n * qB + 0252      have arranged : n * qB + (n * d + c) = n * qB + n * d + c by ring253      have zeroSum : n * qB + 0 = n * qB by ring254      rwa [arranged, zeroSum]255    have cancel2 := add.left_cancel at n * d + c, 0, n * qB256    have sumZero := cancel2 with shifted257    have parts := add.eq_zero at c, n * d258    have both := parts with sumZero259    rw both.right260    exact divides.zero261