← Contents · Ch 0 · Ch 1
Described, implemented in Lean, visualised, and proved correct. repo
Subtraction has the same column-by-column shape as addition, but in place of a carry it uses a borrow. You line the two numbers up by their right edge and subtract column by column from the units. When the top digit in a column is too small, ten is taken from the column to its left before subtracting, and that column is then short by one. The borrow is the only thing that passes between columns. It's the carry's mirror image.
Addition had nothing like this next part. Subtraction is defined only when the top number is at least the bottom one; otherwise the true result is negative, which a list of digits cannot represent. That is a real precondition, and the whole proof turns on it.
Take 452 − 27. Working from the units, when a column can't subtract you take ten from the column to
its left: that column's digit is crossed out and rewritten one smaller,
and the borrowing column gains +10.
Nat
subtraction does. Keeping the precondition honest is what lets the theorem mean what we want — see
the prologue's note.Subtraction is built in the same three layers as addition, each proved correct before the next is placed on top, with a borrow wherever addition had a carry.
5 − 05), in which case
[] (value 0) is exactly the right answer. The theorem's hypothesis keeps the branch honest: it
forces the remaining bottom value to 0. Termination, exactly as for addition, follows from the combined list
length decreasing at each call.Step through a column at a time, the way you would borrow on paper: when a column can't subtract, it takes ten from its left neighbour — that neighbour's digit is crossed out and dropped by one, and the borrowing column is marked +10. On paper you edit the neighbour's digit; the code never edits — it hands the next column a borrow flag, and subtracting that 1 there is the same act. When the neighbour is 0 the strike chains: 0 becomes 9 and the borrow moves one more column left (try 100 − 1 below). The panel states subtraction's invariant; entering a top number smaller than the bottom brings the precondition into play.
After the lowest k columns, the top digits read so far, plus any borrow still owed at its place value
10ᵏ, equal the result digits plus the bottom digits read so far:
aₖ + borrow × 10ᵏ = resultₖ + bₖ.
This is the invariant, the borrow-shaped counterpart of addition's. Each column re-establishes
it. At the end no digits and no borrow remain, and provided the borrow never escaped past the top
number, it collapses to exactly a − b = result. That proviso is the precondition again.
One caution before §5: there the borrow will change sides. In the panel the borrow sits with a, because
the columns already read have taken ten from the ones still to come; the theorem views the same debt from the
other side — an incoming borrow the remaining columns must pay, so it joins output + b. Two views
of one ledger.
One column of subDigits takes two digits and an incoming borrow, and returns a difference digit and
a borrow-out. With a borrow coming in, what does subDigits 5 5 true return?
You have read one of these proofs already, back in the addition chapter, so this time see how much of it you can anticipate before reading it. A verification mindset is less about Lean syntax than about a few habits: pin down for which inputs the claim is even meant to hold, account for every branch the code can take (including the ones that look wrong), and check that each assumption you rely on still holds the next time around. The questions below are those habits, applied to subtraction.
Addition's theorem held for all inputs. Subtraction by hand can fail — try 3 − 7 with
whole numbers. So what has to appear in verticalSub_correct that addition's statement never needed?
The [], _ :: _ case returns [] — on its face a wrong difference. If the algorithm can
reach that branch, how can the theorem still be true?
The proof is an induction: it assumes the algorithm is correct on the shorter tails, then handles one more column. But the inductive hypothesis only applies when its own precondition holds. What extra work does that force at each step?
Same shape as the algorithm, and told the same way as addition's proof. 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 section without opening a single dropdown.
The single-column facts are settled case by case; verticalSub_correct is then proved by induction.
What sets it apart from addition is the point the questions above were circling: the precondition
b ≤ a has to be re-earned before each recursive call — that is the whole job of the small
hpre sub-proofs. Notice h is slightly stronger than §4's answer: the owed borrow joins
the bottom side, deliberately, because each recursive call passes a new borrow inward, so the inequality the
induction maintains must mention it. That is what keeps the borrow from ever asking a column to subtract more
than it holds, and it is why the empty-list "undefined" branch can be discharged rather than feared. A short
corollary, verticalSub_correct', then drops the borrow for the everyday no-borrow case.
In the Lean, goal states in the tooltips are lightly abbreviated — · for *, and b' names this column's borrow-out — the shapes are what matter.
A few questions about the pieces that make the proof work, plus one design choice in the definition it leans on. These are no longer predictions. They ask whether the moving parts are clear now that you have read it.
subDigits_correct does inside the inductionhpre get its ammunition?The statement reads output + b + borrow = a. Why avoid stating output = a − b?
The proof inducts on a, and again on b inside each case. Why this nested, two-list
structure?
subTableThe table ends with | ⟨n+10, h⟩, _ => absurd h (by omega). Why is that line there at all?
Addition's first base case was | [], [], true => [⟨1, …⟩], but subtraction's is
| [], [], true => []. Both lists are empty with a leftover bit — why does addition produce a
digit while subtraction produces nothing?
A worksheet. Each cell has a starting goal with a gap for you to fill. Press Run and your code is
compiled by Lean 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.
In the listings digit literals are written 0, 1 for readability; the server spells
them ⟨0, by omega⟩ — either compiles.
(Requires the checker server — see web/checker/README.md. The first run is
slow: Lean is cold-loading Mathlib.)
The real, machine-checked proof is exactly the one in §5 — clone the repo and run it in VS Code.