← Contents · Ch 0 · Ch 1 · Ch 2 · Ch 3
Described, implemented in Lean, visualised, and proved correct. repo
mulTable) to guess each quotient digit, and the multi-digit
extension sketched at the end reuses subtraction too. It is also the first algorithm that runs from the
most significant digit downward, and the first whose central step is a search. Take it
slowly. The visualiser and the "think like a verifier" questions are here to build the picture before the proof.Every algorithm so far has swept through the digits from the units upward, because that is the direction a carry or a borrow flows. Division goes the other way: you work from the top, the most significant digit, downward — exactly as you were taught to set out a long division.
At its centre is a small search, the step everyone remembers as the hard one: how many times does the divisor go in? You keep a running remainder, and at each column you do three things:
q (from 0 to 9) whose product
with the divisor still fits, q × b ≤ current value. That q is the next digit of the
quotient.q × b from the current value. What is left is the new remainder, which
you carry to the next column.You pick the largest digit that fits. That isn't fussiness; it's what makes the digit the right one.
If q is the largest digit with q × b ≤ value, then one more is too big:
value < (q + 1) × b. Subtracting q × b then leaves less than b, a
genuine remainder small enough for the division to continue. Anything smaller would leave a remainder of
b or more, which still has the divisor in it.
Once every digit has been brought down, the quotient written across the top and the remainder left in your hand satisfy the one equation that defines integer division:
dividend = quotient × divisor + remainder, with 0 ≤ remainder < divisor.
Take 158 ÷ 4, set out the long-division way. The quotient
grows across the top; each step subtracts q × 4 and carries down the
remainder.
Division comes with a precondition, just as subtraction did: the divisor must not be zero. Dividing by zero has no answer at all. So, like subtraction's "top must be at least the bottom", that restriction is written into the theorem as a hypothesis, and the proof gets to assume it throughout.
The build has three layers. This chapter formalises division by a single-digit divisor, which is enough to meet every new idea; a multi-digit version is sketched at the end of the source for the curious.
longDiv reverses the list, runs the helper, then
reverses the quotient back — the same double-reverse you would use to read a stack from the bottom. The final
trimTrailingZeros drops any high-place zeros the digit-by-digit process produced — whenever a
leading chunk is smaller than the divisor (as in 158 ÷ 4: the first column asks how many 4s fit in 1, writes 0,
and the trim removes it), the helper writes a 0 the written method never shows — without changing the value.Step through one dividend digit at a time. The quotient builds up across the top; the box beneath shows the
search and subtraction for the current digit; the panel tracks the invariant. Try a divisor of 0 — the
visualiser refuses it, for the same reason the theorem carries b ≠ 0 (the question below shows
what the raw code would do).
Watch the panel's second line. After each digit, the part of the dividend read so far equals the quotient so far
times the divisor, plus the current remainder, and that remainder is always below the divisor. That is the
invariant, and at the last digit it becomes exactly dividend = quotient × divisor + remainder. The
whole proof is the claim that this relationship survives every "bring down".
You have four proofs behind you now. Before reading this one, predict its shape. What must the statement assume? What does "correct" even mean for division? And why can the trial-digit search be trusted? These are the questions a verifier asks first.
Addition assumed nothing; subtraction assumed the top was at least the bottom. What must division's theorem
assume about the divisor b?
Forget the hypothesis for a moment: what does the code actually do when b = 0?
The theorem will say value = quotient × b + remainder and remainder < b. Why
both halves? Keep only the first, and an "algorithm" that always answers quotient 0, remainder
value would pass it — value = 0 × b + value is perfectly true — while having divided
nothing at all. The second clause, remainder < b, is what forces the quotient to be as large as it
should be. A specification that a broken program can satisfy is no specification; both clauses have to be there.
For addition it was toNat of the result equals the sum. What equation should the division theorem
end up proving?
The search returns the largest q with q × b ≤ current value. Why must it be the
largest, rather than just any digit that fits?
The same three layers as the code — but here each module comes in two parts. First the argument in plain words: read just these and you'll understand why the algorithm is correct. Then, folded underneath, the full Lean proof, for anyone who wants the machine-checked details. You can follow the whole chapter without opening a single dropdown.
The heart is a single induction that says the invariant from §3 survives each step. Two facts feed it: the trial
digit is correctly bracketed, and the running remainder stays below the divisor. The theorem states the invariant
about the digits remaining: whatever remainder acc you walk in with, processing the rest
gives back the value acc heads. Instantiated at the start — all digits remaining, acc = 0
— that is the whole dividend, and the §3 panel reappears.
The chain finishes at longDiv_correct: reversing to process from the top, running the helper from an
initial remainder of 0, and trimming the quotient all preserve the value, so the invariant at the end reads
toNat a = toNat quotient × b + remainder with remainder < b. That is integer
division, proved for every dividend and every non-zero single digit.
findQuotientDigit_correct proves q × b ≤ value < (q + 1) × b. What does the main
induction actually need from it?
Which earlier chapter's work does single-digit division reuse?
n < 10 × b bound?The trial-digit lemma assumes n < 10 × b. Why is that always true of one column, and why does it
matter?
What is findQuotientDigit 45 ⟨5,_⟩ — the largest digit q with q × 5 ≤ 45?
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 first run
cold-loads Mathlib, so it is slow.)
The real, machine-checked proof is exactly the one in §5 — clone the repo and run it in VS Code.