Grace/Cumulus/Nat/Division.g17

Open in Workbench Download source

Imports

Mod · Order

Declarations

Source

1-- Division with remainder for 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.Division8import Mod9import Order1011theorem mod.division (d n : Nat)12  requires nonzero : d ≠ 013  shows (∃ q, Nat(q) ∧ n = d * q + n % d) ∧ n % d < d14proof15  induction n16  | zero =>17    have remainder := mod.zero_left at d with *18    rw remainder19    constructor20    . witness 021      ring22    . have positive := Less.add_positive at 0, d with *23      simpa [add] using positive24  | succ(k) using ih =>25    rcases ih with ⟨division, bound⟩26    obtain ⟨q, qNat, equation⟩ := division27    have split : succ(k % d) = d ∨ succ(k % d) ≠ d28    . tauto29    cases split with wraps | advances30    . have condition := equalNat.true_iff.backward at succ(k % d), d with *31      have remainder : succ(k) % d = 032      . simp [mod, nextRemainder, equalNat.reflexive, condition, chooseNat]33      rw remainder34      have increment := add.succ_right at k % d, d * q with *35      rw ← equation at increment36      symm at increment37      constructor38      . witness succ(q)39        rw remainder40        rw wraps at increment41        have product : d * succ(q) + 0 = d * q + d42        . ring43        rwa product44      . have positive := Less.add_positive at 0, d with *45        simpa [add] using positive46    . have condition := equalNat.false_iff.backward at succ(k % d), d with *47      have remainder : succ(k) % d = succ(k % d)48      . simp [mod, nextRemainder, equalNat.reflexive, condition, chooseNat]49      rw remainder50      have increment := add.succ_right at k % d, d * q with *51      rw ← equation at increment52      symm at increment53      constructor54      . witness q55        rw remainder56        exact increment57        have comparison := Less.trichotomy at succ(k % d), d with *58        rcases comparison with less | equal | greater59        . exact less60        . exfalso61          exact advances with equal62        . arith6364theorem mod.less (n d : Nat)65  requires nonzero : d ≠ 066  shows n % d < d67proof68  have division := mod.division at d, n with *69  tauto7071theorem mod.equation (n d : Nat)72  requires nonzero : d ≠ 073  shows ∃ q, Nat(q) ∧ n = d * q + n % d74proof75  have division := mod.division at d, n with *76  tauto7778-- Count exactly the same wraps as mod. Division by zero returns zero.79def quotientNat (n d : Nat) → Nat80  | zero, d => zero81  | succ(n), d => chooseNat(equalNat(succ(n % d), d), succ(quotientNat(n, d)), quotientNat(n, d))8283theorem quotientNat.natural (d n : Nat)84  shows Nat(quotientNat(n, d))85proof86  induction n87  | zero =>88    simp [quotientNat]89    typecheck90  | succ(k) using ih =>91    have boolean := equalNat.boolean at succ(k % d), d with *92    have natural := chooseNat.natural at equalNat(succ(k % d), d), succ(quotientNat(k, d)), quotientNat(k, d) with *93    simpa [quotientNat] using natural9495theorem quotientNat.equation (d n : Nat)96  shows n = d * quotientNat(n, d) + n % d97proof98  induction n99  | zero => simp [quotientNat, mod, mul.right_zero, add]100  | succ(k) using ih =>101    have split : succ(k % d) = d ∨ succ(k % d) ≠ d102    . tauto103    cases split with wraps | advances104    . have condition := equalNat.true_iff.backward at succ(k % d), d with *105      have remainder : succ(k) % d = 0106      . simp [mod, nextRemainder, condition, equalNat.reflexive, chooseNat]107      have quotient : quotientNat(succ(k), d) = succ(quotientNat(k, d))108      . simp [quotientNat, condition, equalNat.reflexive, chooseNat]109      have increment := add.succ_right at k % d, d * quotientNat(k, d) with *110      rw ← ih at increment111      symm at increment112      rw [quotient, remainder]113      rw wraps at increment114      have product : d * succ(quotientNat(k, d)) + 0 = d * quotientNat(k, d) + d115      . ring116      rwa product117    . have condition := equalNat.false_iff.backward at succ(k % d), d with *118      have remainder : succ(k) % d = succ(k % d)119      . simp [mod, nextRemainder, condition, equalNat.reflexive, chooseNat]120      have quotient : quotientNat(succ(k), d) = quotientNat(k, d)121      . simp [quotientNat, condition, equalNat.reflexive, chooseNat]122      have increment := add.succ_right at k % d, d * quotientNat(k, d) with *123      rw ← ih at increment124      symm at increment125      rw quotient126      rwa remainder127128theorem quotientNat.zero_right (n : Nat)129  shows quotientNat(n, 0) = 0130proof131  induction n132  | zero => simp [quotientNat]133  | succ(k) using ih =>134    have nonzero : succ(k % 0) ≠ 0135    . intro equal136      have distinct := Naturals.disjoint.zero.succ at k % 0137      symm at equal138      exact distinct with equal139    have condition := equalNat.false_iff.backward at succ(k % 0), 0 with *140    simp [quotientNat, condition, equalNat.reflexive, chooseNat]141142theorem quotientNat.division (n d : Nat)143  requires nonzero : d ≠ 0144  shows Nat(quotientNat(n, d)) ∧ n = d * quotientNat(n, d) + n % d ∧ n % d < d145proof146  simp [quotientNat.natural, quotientNat.equation, mod.less]147148-- Dividing a bound through by a positive coefficient: these two tightenings149-- keep linear arithmetic over the naturals exact when every coefficient of150-- an atom shares a factor. The coefficient is written succ(k) so that it is151-- visibly nonzero.152theorem LessEqual.quotient_floor (a b k d : Nat)153  requires bound : succ(k) * a ≤ succ(k) * b + d154  shows a ≤ b + quotientNat(d, succ(k))155proof156  have nonzero : succ(k) ≠ 0157    intro zero158    have disjoint := Naturals.disjoint.zero.succ at k159    apply disjoint160    symm at zero161    exact zero162  obtain ⟨qNat, equation, remainder⟩ := quotientNat.division at d, succ(k) with nonzero163  by_contra refuted164  have strict := Less.of_not_LessEqual with refuted165  have scaled := LessEqual.mul_left at succ(b + quotientNat(d, succ(k))), a, succ(k) with strict166  have expand : succ(k) * succ(b + quotientNat(d, succ(k))) = succ(k) * b + succ(k) * quotientNat(d, succ(k)) + succ(k)167    ring168  rw expand at scaled169  rw equation at bound170  have cycle : succ(k) * a < succ(k) * a by arith171  exact Less.irreflexive with *, cycle172173theorem LessEqual.quotient_ceiling (a b k e : Nat)174  requires bound : succ(k) * a + (e + 1) ≤ succ(k) * b175  shows a + (quotientNat(e, succ(k)) + 1) ≤ b176proof177  have nonzero : succ(k) ≠ 0178    intro zero179    have disjoint := Naturals.disjoint.zero.succ at k180    apply disjoint181    symm at zero182    exact zero183  obtain ⟨qNat, equation, remainder⟩ := quotientNat.division at e, succ(k) with nonzero184  by_contra refuted185  have strict := Less.of_not_LessEqual with refuted186  have scaled := LessEqual.mul_left at succ(b), a + (quotientNat(e, succ(k)) + 1), succ(k) with strict187  have left : succ(k) * succ(b) = succ(k) * b + succ(k) by ring188  have right : succ(k) * (a + (quotientNat(e, succ(k)) + 1)) = succ(k) * a + succ(k) * quotientNat(e, succ(k)) + succ(k)189    ring190  rw [left, right] at scaled191  rw equation at bound192  have cycle : succ(k) * b < succ(k) * b by arith193  exact Less.irreflexive with *, cycle194