← Contents · Ch 0 · Ch 1 · Ch 2 · Ch 3 · Ch 4
Described, implemented in Lean, visualised, and proved correct. repo
myMod is
literally (longDiv a b).2. What's new is modular arithmetic, reasoning about
remainders, so the proofs look different from the earlier place-value inductions.You can often tell whether one number divides another just by looking at its digits, with no division at all. A number is even exactly when its last digit is; divisible by 5 exactly when the last digit is 0 or 5; divisible by 3 or by 9 exactly when the sum of its digits is; and divisible by 11 exactly when the alternating sum of its digits is.
All of these come from one idea: modular arithmetic. It cares only about the remainder after division and throws the rest away.
Take 10 divided by 3. Since 10 = 3 × 3 + 1, the remainder is 1. We write that
10 ≡ 1 (mod 3), read "10 is congruent to 1, modulo 3" — all it means is that 10 and 1 leave the
same remainder when divided by 3.
Remainders earn this notation because they survive addition and multiplication:
You can replace a number by its remainder partway through a sum or a product, and the final remainder is
unchanged. That is what lets the tests work one digit at a time. Each place value 10ⁱ has a simple
remainder, so a number's remainder is built from its digits' remainders, each weighted by its place-value
remainder. That is why only the digits matter:
10 ≡ 0. Every place above the units is a multiple of 2 (and of 5), so
it contributes nothing to the remainder — only the units digit is left.10 ≡ 1, so 10ⁱ ≡ 1 for every i. Each digit
contributes its plain face value, and the whole number's remainder is the digit sum's remainder.10 ≡ −1, so 10ⁱ ≡ (−1)ⁱ — the place values alternate in sign.
Digits in even positions (counting from the units digit as position 0) add, digits in odd positions subtract: the alternating sum.%,
the chapter reuses the long division you already verified in Chapter 4 to define its own myMod,
then proves it agrees with Nat.mod. Each chapter standing on the one before it, rather than on
built-ins, is the through-line of the book (see the prologue).A test is a statement about remainders. So we need three pieces: a remainder function, a couple of digit summaries, and the tests themselves stated through them.
(…).1 / (…).2 are pair projections — the first and second components
of the (even, odd) pair altSums returns — not digits. Each test comes in two
forms: a pure number-theory statement (e.g. 9 ∣ toNat a ↔ 9 ∣ digitSum a) and a
myMod version that connects it to the actual remainder our long division computes.Pick a test, then step in from the units digit. At each suffix the panel checks the invariant that makes the rule work: the suffix's value and its digit summary leave the same remainder. It never breaks, and that is the inductive proof made visible.
For 3 and 9 the invariant is value % m = digitSum % m; for 11 it is
(value + O) % 11 = E % 11, with E the even-position sum
(green) and O the odd-position sum
(orange). Bringing in one more digit re-establishes the same
congruence, so by the end the whole number and its digit summary agree. That is the test.
Before reading the proof, predict its shape. Each test is a claim about remainders. Ask which fact about the number 10 powers it, and what equation the proof will actually establish.
The tests for 3 and 9 add up the digits. Which fact about 10 is doing the work?
For 9, before the divisibility ↔, there is a sharper equality the proof really turns on. Which?
Each layer comes in two parts. First the argument in plain words: read just these and you'll understand why every test is correct. Then, folded underneath, the full Lean proof, for anyone who wants the machine-checked details. You can follow the whole section without opening a single dropdown.
The tests share one backbone: reduce to a statement about %, then push the remainder through the
digits with the two modular laws Lean already provides, Nat.add_mod and Nat.mul_mod.
The digit-sum congruence is a clean place-value induction. The alternating-sum one is the same idea with
10 ≡ −1, carried by Nat.ModEq. One new notation: a ≡ b [MOD n] is Lean's
name for a % n = b % n — the congruence we have been writing all chapter, packaged as a relation
you can chain in a calc and add to on both sides (Nat.ModEq.add_left and friends).
Write each number as q·m + r. Under a remainder the
grey multiple of m always vanishes, and only the
remainders are left.
Nat.add_modNat.mul_modBoth are already in Lean's core, so the chapter cites them rather than reproving them.
The ÷2, ÷3 and ÷5 tests are also in the repo: 2 and 5 go by
a direct divisibility induction on the units digit — no mod laws needed — and 3 exactly like 9.
The ÷9 induction rewrites 10 · tail as tail + 9 · tail. What does that buy?
myMod_eq_natMod proves myMod a b = toNat a % b. Why does the chapter need it?
The tests are stated as ↔. What does the ← direction (digit sum divisible ⇒ number divisible) buy you?
A worksheet. Each cell has a starting goal with a gap for you to fill. Press Run and Lean compiles your
code on the server. Run all checks every cell in turn, Reset all restores the blank
cells, and every cell hides a reference solution you can reveal once you've tried.
(Requires the checker server — see web/checker/README.md. The myMod
cell needs native_decide (it runs the whole long division); altSums is small enough for
plain decide — the contrast is the point. The first run is slow.)
The real, machine-checked proofs are exactly those in §5 — clone the repo and run it in VS Code.