Grace/Cumulus/Nat/Mod.g17

Open in Workbench Download source

Imports

Core.Data · Core · Foundation

Declarations

Source

1-- Computable remainder arithmetic on natural numbers2-- 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.Nat.Mod8import Core.Data9import Core10import Foundation1112-- Boolean equality is computational evidence; propositional equality remains13-- the kernel relation used by proofs.14def isZero (n : Nat) → Bool15  | zero => Bool.true16  | succ(n) => Bool.false1718def equalNat (m n : Nat) → Bool19  | zero, n => isZero(n)20  | succ(m), n => BoolOps.and(BoolOps.not(isZero(n)), equalNat(m, predecessor(n)))2122def chooseNat (condition : Bool, yes no : Nat) → Nat23  | Bool.false, yes, no => no24  | Bool.true, yes, no => yes2526-- Advance a remainder, wrapping to zero exactly at the divisor.  With divisor27-- zero it never wraps, giving the conventional total equation n % 0 = n.28def nextRemainder (d r : Nat) : Nat :=29  chooseNat(equalNat(succ(r), d), 0, succ(r))3031def mod (n d : Nat) → Nat32  | zero, d => zero33  | succ(n), d => nextRemainder(d, mod(n, d))3435notation infixl 70 "%" => mod3637theorem equalNat.reflexive (n : Nat)38  shows equalNat(n, n) = Bool.true39proof40  induction n41  | zero => settle with equalNat, isZero42  | succ(k) using ih =>43    simp [equalNat, isZero, predecessor, BoolOps.not, BoolOps.and, ih]4445theorem equalNat.true_iff (a b : Nat)46  shows equalNat(a, b) = Bool.true ↔ a = b47proof48  induction a generalizing b49  | zero =>50    intros b naturalB51    have shape := natural.zero_or_successor with naturalB52    cases shape with equal | successor53    . rw equal54      simp [equalNat, isZero]55    . rcases successor with ⟨k, naturalK, bShape⟩56      rw bShape57      have distinct := Naturals.disjoint.zero.succ at k58      have computed : equalNat(0, succ(k)) = Bool.false by simp [equalNat, isZero]59      rw computed60      have boolDistinct := Bool.inductive.disjoint.false.true61      tauto62  | succ(k) using ih =>63    intros b naturalB64    have shape := natural.zero_or_successor with naturalB65    cases shape with equal | successor66    . rw equal67      have distinct : succ(k) ≠ 068        intro h69        have zeroNot := Naturals.disjoint.zero.succ at k70        apply zeroNot71        rw h72        rfl73      have computed : equalNat(succ(k), 0) = Bool.false74        settle with equalNat, isZero, predecessor, BoolOps.not, BoolOps.and75      rw computed76      have boolDistinct := Bool.inductive.disjoint.false.true77      tauto78    . rcases successor with ⟨j, naturalJ, bShape⟩79      rw bShape80      have inner := ih with j, naturalJ81      have reduced : equalNat(succ(k), succ(j)) = equalNat(k, j)82        settle with equalNat, isZero, predecessor, BoolOps.not, BoolOps.and83      rw reduced84      constructor85      . intro same86        have kj := inner.forward with same87        rw kj88        rfl89      . intro same90        have kj := Naturals.injective.succ with same91        exact inner.backward with kj9293theorem boolean.cases (b : Bool)94  shows b = Bool.false ∨ b = Bool.true95proof96  induction b97  | Bool.false =>98    left99    rfl100  | Bool.true =>101    right102    rfl103104theorem equalNat.boolean (a b : Nat)105  shows Bool(equalNat(a, b))106proof107  induction a generalizing b108  | zero =>109    intros b bNat110    have shape := natural.zero_or_successor with bNat111    cases shape with zero | successor112    . rw zero113      have computed : equalNat(0, 0) = Bool.true by simp [equalNat, isZero]114      rw computed115      exact Bool.inductive.constructor.true116    . rcases successor with ⟨k, hk, equal⟩117      rw equal118      have computed : equalNat(0, succ(k)) = Bool.false by simp [equalNat, isZero]119      rw computed120      exact Bool.inductive.constructor.false121  | succ(k) using ih =>122    intros b bNat123    have shape := natural.zero_or_successor with bNat124    cases shape with zero | successor125    . rw zero126      have computed : equalNat(succ(k), 0) = Bool.false127        settle with equalNat, isZero, BoolOps.not, BoolOps.and128      rw computed129      exact Bool.inductive.constructor.false130    . rcases successor with ⟨j, hj, equal⟩131      rw equal132      have computed : equalNat(succ(k), succ(j)) = equalNat(k, j)133        settle with equalNat, isZero, predecessor, BoolOps.not, BoolOps.and134      rw computed135      exact ih with j, hj136137theorem equalNat.false_iff (a b : Nat)138  shows equalNat(a, b) = Bool.false ↔ a ≠ b139proof140  have boolean := equalNat.boolean at a, b with *141  have shape := boolean.cases with boolean142  have truth := Grace.Cumulus.Nat.Mod.equalNat.true_iff at a, b with *143  have distinct := Bool.inductive.disjoint.false.true144  constructor145  . intros falseValue same146    have trueValue := truth.backward with same147    rw falseValue at trueValue148    exact distinct with trueValue149  . intro different150    cases shape with falseValue | trueValue151    . exact falseValue152    . have same := truth.forward with trueValue153      exfalso154      exact different with same155156theorem isZero.boolean (n : Nat)157  shows Bool(isZero(n))158proof159  induction n160  | zero =>161    simp [isZero]162    exact Bool.inductive.constructor.true163  | succ(k) using ih =>164    simp [isZero]165    exact Bool.inductive.constructor.false166167theorem chooseNat.natural (condition : Bool, yes no : Nat)168  shows Nat(chooseNat(condition, yes, no))169proof170  have shape := boolean.cases with *171  cases shape with falseValue | trueValue172  . rw falseValue173    simp [chooseNat]174  . rw trueValue175    simp [chooseNat]176177theorem mod.natural (d n : Nat)178  shows Nat(n % d)179proof180  induction n181  | zero =>182    simp [mod]183    typecheck184  | succ(k) using ih =>185    have boolean := equalNat.boolean at succ(k % d), d with *186    have natural := chooseNat.natural at equalNat(succ(k % d), d), 0, succ(k % d) with *187    simpa [mod, nextRemainder] using natural188189theorem mod.zero_left (d : Nat)190  shows 0 % d = 0191proof192  simp [mod]193194theorem mod.zero_right (n : Nat)195  shows n % 0 = n196proof197  induction n198  | zero => settle with mod199  | succ(k) using ih =>200    settle with mod, nextRemainder, equalNat, isZero,201      predecessor, BoolOps.not, BoolOps.and, chooseNat, ih202203theorem mod.one (n : Nat)204  shows n % 1 = 0205proof206  induction n207  | zero => settle with mod208  | succ(k) using ih =>209    settle with mod, nextRemainder, equalNat, isZero, predecessor,210      BoolOps.not, BoolOps.and, chooseNat, ih211212theorem mod.sample213  shows 100 % 7 = 2214proof215  compute216217eval 100 % 7218