Type Theory Part II: Proving Natural Addition Commutes from First Principles
All the code snippets in this article are compiled into a fully working proof accessible here
You can read Part I here
Foreword
I believe proving that natural addition commutes is a good exercise in mathematical foundations and it is usually required in a set theory class. I recently completed a textbook on set theory and while I enjoyed it and found the content sufficiently rigorous I was generally unsatisfied with the degree of ‘fundamentality’ of set theoretic constructions. I went into the book under the assumption everything would be from the ground up. And that was largely the case. But when it came to the first induction-based proofs I couldn’t help but feel that I was being pushed in a certain direction when defining and proving things. In my opinion the motivation for steps in a proof or for a new concept should be self evident and if not the exercise should be revisited retroactively once it becomes so. In addition to this I felt that I could not draw the line between ‘pure’ symbolic manipulation and ‘flawed’ non-rigorous logical justification. Was my proof that \(0 + n = n\) for natural \(n\) correct or did I assume something I shouldn’t have? We have exactly the right tools to solve both of these problems now. We’ll build everything from the ground up in a way that is both impartial and necessary and the type checker will catch any logical mistakes. Our weapon of choice will be the CIC-based dependently typed programming language and proof assistant, lean4.
Defining the Naturals
We’ll be assuming the Peano axioms to define the naturals. This has been standard practice for centuries. We won’t use all of them and importantly no other assumptions will be made! I’ll document which axioms correspond to which ‘boilerplate code’, which in this case is code that we need/features we rely on separate to the math we create.
Only the first 5 axioms are real Peano axioms. Equality precedes the axioms and is built into ZFC itself. This means the orthodox definition of equality does not require that ‘objects’ in an equivalence relation be naturals, and there is typically no need to introduce this definition when discussing the Peano axioms. In these cases, there is a fourth equality axiom introduced specifically for the naturals stating that they are closed under equality. Since we are ‘skipping’ sets and only constructing naturals (via types) it is appropriate to axiomise equality. Natural addition is usually constructed by the mathematician for their own needs; it is not inherently part of the Peano axioms. Since we are assuming addition exists to prove commutativity we will axiomize the standard definition.
To define a new data type, the naturals, we use the inductive keyword.
1
2
3
inductive MyNat : Type where
| zero : MyNat -- by 1.
| succ : MyNat → MyNat -- by 2.
We’ll call our naturals MyNats to avoid naming conflicts and potential ambiguity when talking about the real lean Nats, which have more structure than the minimal skeleton we define here. The axioms tell us that \(0\) is a MyNat and we have an abstract \(S\) unary operation we can apply to a MyNat to yield another MyNat. The first line tells us the kind of MyNat is Type- so MyNat is not indexed by other types. In that sense it is ‘simple’ as you would expect the naturals to be. MyNat has two data constructors- zero corresponds to \(0\) and produces a MyNat for us automatically, while succ corresponds to \(S\) and requires a MyNat to iterate on. Hence it has the type MyNat → MyNat. Lean4 tries to be idiomatic with mathematical expressions, so many functional programming syntaxes are replaced with the unicode symbols that inspired them (e.g. -> becoming →.)
Addition
1
2
3
def myAdd : MyNat → MyNat → MyNat
| a, .zero => a -- by 9.
| a, .succ b => MyNat.succ (myAdd a b) -- by 10.
Note we have used .zero to refer to MyNat.zero and .succ to refer to MyNat.succ, and that we’ve called our function myAdd to keep it distinct from anything preexisting or floating around in the namespace.
These two recursive rules for computing addition result in a definition of addition that is both intuitively correct and has been shown to be consistent. That is, we cannot derive a contradiction within the system such as \(0 = 1\). While Godel’s second incompleteness thoerem shows that we cannot verify the Peano axioms are consistent from within them, Godel himself published a method for showing the consistency of arithmetic using type theory! An important thing to note is that the 10th axiom assumes recursion has been shown to be valid which we have not shown here. Languages like lean are able to calculate the recursive call will always terminate (which is important if we want our program to type check!) by requiring that recursive functions are defined structurally. This means that it is easy to see that recursion proceeds on ‘structurally smaller’ inputs. It also explains why we cannot piggyback off the termination checker to verify longstanding unsolved conjectures founded on recursive definitions. Since addition transforms taking the sum of a and succ b to the sum of a and b, which is definitionally smaller, lean knows addition will terminate.
First Theorems
1
2
3
4
5
theorem add_zero (a : MyNat) : myAdd a .zero = a := by
rfl -- by 6.
theorem add_succ (a b : MyNat) : myAdd a (MyNat.succ b) = MyNat.succ (myAdd a b) := by
rfl -- by 6.
Our first theorems have no substance- we are just giving definitionally equal terms a name for easy future reference. Theorems are semantically identical to functions, the main difference being the return type of a theorem must be some kind of proposition- which a = b is and TwoPlusTwoEqualsFour (from Part I) isn’t.
add_zero is otherwise a function that accepts a parameter a of type MyNat and returns a value of type myAdd a .zero = a. Look at how the proposition is formulated. The lhs inside the proposition appears to calls the function myAdd on an unknown input a whose type is MyNat. However, this function call does not ever run since we are only concerned with type checking, which occurs at runtime. In this context myAdd does not refer to the concrete subroutine but an abstract named hypothetical transformation on a- the term a will never exist, all we want is the type of a. This can be thought of logically as a hypothetical, or an ‘if-then’. ‘If’ a is provided ‘then’ the following proposition must hold. This is the motivation behind the arrow syntax in FP, to be consistent with logical implication.
Remember the only tool we have so far for constructing proofs of equality is Refl, known as rfl in lean (refl with a lowercase ‘r’ also exists but has a different meaning). Remember that rfl takes a term x implicitly and constructs a term of the type x = x. We didn’t provide this term- it is implicit and the lean4 elaborator (part of the compiler) simply guessed that it should use a as x and return an a = a. Lean remembers the definition for myAdd which says that myAdd a MyNat.zero is definitionally equal to a. So it is able to use that rule to reduce the required type from myAdd a .zero = a to a = a which is constructed by invoking rfl. This process of changing the required type is known as manipulating the ‘goal’ and is a central part of proofs. In this case the manipulation was trivial and applied automatically but in the next example there will be manual steps. We can manipulate goals in all kinds of complex ways such as splitting them up into cases, proving things via contradiction, introducing hypotheticals etc. Techniques for doing so are called ‘tactics’- we just used the refl tactic. For the theorem add_succ lean does something similar, this time using the myAdd definition for a, MyNat.succ b. Every time we invoke rfl we are using the 6th axiom- we are assuming a = a is true to show that a = a is inhabited.
Before we can prove commutativity (we will refer to this theorem from now on as add_comm) we need to prove some supporting theorems. Unfortunately I can’t just explain why we need these particular lemmas. Halmos’ text quite literally gave instruction to prove exactly these specific supporting theorems and use them in the commutativity proof, which (as mentioned) I found unsatisfying. With the convenience of an instant type checker, I was able to explore freely trying to prove add_comm and was warned whenever I skipped a step or assumed something incorrectly. It felt good to arrive at a conclusion on my own: I ended up figuring out it was easiest to use exactly the theorems that Halmos laid out. Let’s prove them.
Mathematical Induction
1
2
3
4
5
theorem zero_add (a : MyNat) : myAdd .zero a = a := by -- the 'by' keyword precedes 'induction' to enter induction
induction a with -- by 5.
| zero => rfl -- by 6.
| succ b ih => -- by 5.
rw [add_succ, ih] -- by 8.
Side note: notating each step to declare exactly how we were able to get to that step reminds me of the style of proof when proving logical equivalence in discrete math. After all, that’s exactly what we’re doing- ‘rigid symbol manipulation’.
Now we declare a non trivial theorem. zero_add is the theorem that \(\forall n \in \mathbb{N} : 0 + n = n\), not to be confused with add_zero which is definitionally true. Since we’re not working exclusively with theorems where lhs = rhs, we need a new rule. We’ll use the axiom 5., induction. The premise of mathematical induction is simple. Let \(P(x)\) be a proposition on a natural, \(x\). If \(P(0)\), and \(P(n)\) implies \(P(n + 1)\) for all \(n\), there is a natural cascading effect which proves \(P\) for all naturals- \(P(0)\) implies \(P(1)\) which implies \(P(2)\) and so on. Much like a toppling domino chain, each domino triggering the next one in the sequence.
The amazing thing about induction in lean is that there is no inhererent logic in the induction keyword itself. Remember that in lean the elaborator knows about all the finitely many ways to construct an object. So if you can prove that no matter how an object \(x\) is constructed, that \(P(x)\) holds, you have proved \(P\) for all \(x\)! This is why GADTs in lean are known as ‘inductive’ data types- because they are defined inductively. The data type itself is where the induction ‘comes from’- which means you can use the induction tactic on any data type, like List or Tree. Consider the fact that to construct a MyNat using the .succ data constructor you need another MyNat. This naturally corresponds to the induction hypothesis, that \(P\) holds for some \(k\), a usable assumption when proving \(P\) holds for \(k + 1\), which is incredible!
What the induction tactic does is, for each data constructor, provide us with the relevant inductive hypotheses. These constructors must be handled one by one in the pattern match syntax using | (if) and => (then). Since .zero is constructed from nothing, it must be proven in a vacuum with no hypotheses. Luckily for us, the zero case is trivially true (from the definition of myAdd in case you forgot.) For .succ we are provided ih (the inductive hypothesis)- which is a theorem we can use exclusively inside the succ block in zero_add. The VS Code lean extension is fantastic when it comes to elucidating goals and the types of variables. On hover, we can see the type of the inductive hypothesis is the goal of zero_add and the mini-goal inside this pattern match case is the sae as the overall goal of zero_add with b replaced by .succ b.
This makes our working expression myAdd .zero (.succ b) = .succ b which we hope to manipulate into something we know is definitionally true- so we can use rfl (which is still the only way we really know how to close a proof). Notice how we’ve abstracted beyond producing terms of a type now- we’re able to interpret what we’re doing purely as algebraic/logical manipulation and rearrangement. To manipulate our working expression into the expected expression, we will introduce another tactic: rw. rw stands for rewrite- it takes an equality proposition e.g. a = b and replaces all instances of a with b in the working expression. rw also tries to close the goal with rfl and fails silently if it cannot. rw can also chain multiple rewrites together as we will do. By invoking rw on add_succ (which states that myAdd x (.succ y) is the same as .succ (myAdd x y)) we rewrite myAdd .zero (.succ b) = .succ b into .succ (myAdd .zero b) = .succ b. ih states that myAdd .zero a = a. Applying this, our goal not only becomes .succ b = .succ b but is closed by rfl since lhs and rhs have been shown to be definitionally equal.
You might start to notice that despite all these fancy keywords and tactics, we are still proving things basically the same way we would on paper. Fundamentally, a proof assistant is only an assistant and a human operator must do the work of writing out the definitions and proofs. But we will hopefully see in future proofs just how advanced and automatic tactics can get. When coupled with copilot, proof writing becomes not just more formally correct but much faster than it could ever be on paper.
1
2
3
4
5
6
theorem succ_add (a b : MyNat) : myAdd (MyNat.succ a) b = MyNat.succ (myAdd a b) := by
induction b with -- by 5.
| zero => rfl -- by 6.
| succ b ih => -- by 5.
rw [add_succ, ih] -- by 8.
rw [← add_succ] -- by 7.
The proof of succ_add is similarly straightforward. The only new addition is the backwards arrow ← in rw [← add_succ]. rw a = b has a very specific, algorithmic purpose- it substitutes b in every place where there was previously an a in the working expression. ← reverses the substitution, writing a in every place where there was previously a b. This is an application of the symmetry of equality (axiom 7.)- if a is equal to and replaceable by b, b is equal to and replaceable by a.
Putting It All Together
1
2
3
4
5
6
theorem add_comm (a b : MyNat) : myAdd a b = myAdd b a := by
induction b with -- by 5.
| zero => -- by 5.
rw [add_zero, zero_add] -- by 8.
| succ b ih => -- by 5.
rw [add_succ, succ_add, ih] -- by 8.
Having meticulously defined and practiced all the tactics and constructs we need in previous theorems, the proof for add_comm becomes simple. This proof is verified at compile time with a double blue tick in the editor- without ever needing to call the theorem as a function to execute it. That was rewarding! We chunked down a (relatively) complex proof into manageble lemmas, cracking them one by one before finally tackling the final boss. And it was so satisfying when we needed a nonobvious substitution midway through an advanced manipulation and had it readily available. I hope I have both equipped you with the tools and knowledge necessary to start proving things on your own, as well as provided you with inspiration to do so.
As a parting gift, here’s the proof for associativity of natural addition for comparison. You can see the rewrites it uses all come for free from myAdd, even though there are more rewrites. This is why associativity is proven before commutativity, it doesn’t need as many supporting lemmas.
1
2
3
4
5
6
theorem add_assoc (a b c : MyNat) : myAdd (myAdd a b) c = myAdd a (myAdd b c) := by
induction c with
| zero =>
rw [add_zero, add_zero]
| succ c ih =>
rw [add_succ, add_succ, add_succ, ih]
Ending Note
This article was a ton of fun to write. I wrote it at the same time as Part I and decided at the last minute to cut them up since they sort of fell into two halves naturally. I’ve been studying type theory in an academic context for about a year now and I’ve recently starting proving my software specifications with lean, so I felt comfortable writing about type theory without dedicated research. If you have any suggestions for which direction to take this series in, submit a PR with your request here. For now I’ll give type theory a break and move on to some more artsy subjects.