It’s not actually that hard to build the non-negative integers from scratch in Lean. Let’s call them
xnat, because Lean already has an inbuilt
nat. The code just looks like this:
| zero : xnat
| succ : xnat → xnat
and that’s it — now
xnat is a representation of the non-negative integers (computer scientists call them the “natural numbers”). Let me explain a bit about how this works.
inductive command creates a new type (think of it as a new set) called
xnat. Lean already has a copy of the non-negative integers, called
nat, so we’ve called the new ones
xnat to avoid confusion.
inductive command above also tells you that there are exactly two ways that you can construct an element of type
xnat. The two ways correspond to the two lines of code under the
inductive command, which are definitions of the
zero object and the
Firstly, you can just type
zero, and you’ll get an
And secondly, if you have an
a already, you can apply the function
succ to it, and get a new
xnat called, unsurprisingly,
succ a. As you can see, the
succ function above looks like a function from
xnat, and that’s exactly what it is.
Now let’s imagine we want to construct some things of type
xnat. At the beginning we don’t have anything at all of type
xnat, so the
succ function is useless to us. We have to use the
zero construction, giving us a natural number which we could call zero. Here’s the full code (together with some other stuff which you don’t need to worry about).
| zero : xnat
| succ : xnat → xnat
#check zero -- it's an xnat
You can run this code online in your browser by clicking here . Wait for a few seconds for everything to process, and then click on the
#check and see that
zero is an
Now we have one
xnat, we can build more using the
succ function. Add the below lines to your Lean session (before the
end xena line):
#check succ zero
#check succ (succ zero)
succ are the only ways to make elements of
xnat, it’s pretty clear that the only elements of
xnat are either zero or
succ (succ (... (succ zero)))...). If we think of
succ as meaning “successor”, or “add one”, then we can see that the only things of type
xnat are zero, one, two, three… . So indeed
xnat is a good model for the non-negative integers.
What next? We could define one and two:
definition one := succ zero
definition two := succ one
Now could we prove that one add one equals two? Well no we can’t yet, because we haven’t defined add yet! Let’s add a definition of add. We’ll define it by induction! Well, more precisely, by recursion. The idea is that
a+0 will just be
a+succ(b) will just be
definition add : xnat → xnat → xnat
| n zero := n
| n (succ p) := succ (add n p)
It would be nice to use the usual notation
+ for add:
notation a + b := add a b
Now let’s check that
one + one = two. This should just be a case of unravelling the definitions of two, of one, and of add.
theorem one_add_one_equals_two : one + one = two :=
It worked! In fact there is an easier way — the tactic
unravels everything and then checks that you’re left with something of the
example : one + one = two :=
[NB an example is just a theorem without a name — if you have two theorems with the same name then Lean complains].
There’s also a harder way. Instead of using
unfold, you can use
dunfold, which does nothing more than the unfolding, so you really have to push it across the line at the end:
theorem one_add_one_equals_two_again : one + one = two :=
Now what I’d really like to do is to prove that
a+b=b+a, because that’s a pretty important property of addition. To do that, we will only need to know a few Lean commands. This is why these calculations are not too hard to learn and to do, in stark contrast to M1F example sheets, which turn out to be insanely hard (indeed I am still only on sheet 2 and I am the lecturer).
So what exactly will we need to learn here? We will need to know about
unfold, which we’ve just seen. We’ll need to know how to prove things by induction, because to prove
a+b=b+a we will do it by induction. And we’ll need to know about the
rewrite command, which substitutes one equation or theorem into another. And that’s it. However the proof will involve several intermediate lemmas, so it does need some thought. I guide you through the proof in the exercises below (note: exercises are currently being written).
Our definition of addition is quite delicate. We can see that
n+zero=n by definition of add. Let’s prove this in Lean.
theorem add_zero (n : xnat) : n + zero = n :=
On the other hand, it is less obvious that
zero+n=n. We need to prove this by induction. Let’s do it!
theorem zero_add (n : xnat) : zero + n = n :=
induction n with t Ht,
I think it’s very hard to follow what is going on in the above code, unless you run the code in Lean and then put your cursor just before the
theorem and then move it up and down using the arrow keys. I’ll talk you through it — but here’s a link to everything we’ve done so far so you can follow along (remember you have to wait to let lean process the input for a few seconds before it all gets going — wait until it stops saying “running” at the top):
Online version of everything so far .
Put your cursor at the beginning of the line near the bottom that says
theorem zero_add... and then move down using the arrow keys to see the proof in action. Here’s what’s happening.
Induction turns one goal into two — a base case and an inductive step (complete with inductive hypothesis, with variable
t and hypothesis
Ht). The base case we can just prove by definition (you could replace
unfold add or even
dunfold add followed by
refl but don’t forget the commas). The inductive step can be proved in two lines. First we unfold the definition of addition. Then we notice that substituting in the hypothesis
Ht (the inductive hypothesis) will turn the goal into something of the form
x=x, which Lean proves automatically. That substitution can be done with the
So there are your four Lean commands : induction, unfold, refl, rewrite. We are going to be able to get a long way with these commands.
What next? We’re not quite ready for
a+b=b+a yet, but it’s not far off. Why not try these exercises? They will get you there, and beyond (when I’ve written them).
Can we prove “associativity of addition”? More precisely:
theorem add_assoc (a b c : xnat) : (a + b) + c = a + (b + c) :=
The “admit” there means “admit defeat”, i.e. give up and prove the answer. Can you delete that “admit” and replace it with an actual proof, by induction on
This exercise shows you that the
rewrite command can be used to apply previous theorems, as well as current hypotheses. It assumes that you already have proofs of
add_zero in your Lean session. Here is a link to an online session with everything set up just right.
Let’s prove that
zero + n = n + zero for all
theorem zero_add_eq_add_zero (n : xnat) : zero + n = n + zero :=
Replace admit with one line of code which finishes the job.
Bonus question: you can rewrite more than one theorem or hypothesis in one line, using e.g.
rewrite [A,B,C], or even
rw [A,B,C] if you get tired of writing
rewrite. Can you prove
zero_add_eq_add_zero in one line?
It’s nice to know that
succ n is
one+n and also
n+one. I’ll prove the easy one:
theorem add_one_eq_succ (n : xnat) : n + one = succ n :=
Now you prove the harder one.
theorem one_add_eq_succ (n : xnat) : one + n = succ n :=
Can you prove
theorem add_comm (a b : xnat) : a + b = b + a :=
? If you try, you might run into the following issue. Recall that we have already proved the case
theorem zero_add_eq_add_zero (n : xnat) : zero + n = n + zero
However if you try proving
add_comm by induction on
b, the base case is the other way around:
a+zero=zero+a. You might hence find that
is useful. To get that left-arrow use
\l (then a space) in VS Code. Another way of doing it:
zero_add_eq_add_zero is actually a function, which sends an xnat n to a proof of the fact that
zero+n=n+zero. So if you do induction on
a then one way of doing the base case is
exact zero_add_eq_add_zero b,
exact means that you’re giving an exact proof] and if you’re doing induction on
a then you need to switch around the sides of the equality, which you can do like this:
exact eq.symm (zero_add_eq_add_zero a),
eq.symm function changes a proof of
X=Y to a proof of
Y=X]. You don’t need to know about these things, I’m just explaining other approaches rather than using the
Can you prove cancellation? I’ll start you off with a proof which uses the
split command to break an
iff into two implications.
theorem eq_iff_succ_eq_succ (a b : xnat) : succ a = succ b ↔ a = b :=
assume H : a = b,
Now try cancellation:
theorem add_cancel_right (a b t : xnat) : a = b ↔ a+t = b+t :=
Take a look at the definition of addition. Do you think you can define multiplication in a similar way?
definition mul : xnat → xnat → xnat
| n zero := ???
| n (succ p) := ???
Note: to get the right arrow try
\r (then a space). Note that because addition is defined, we can use it to help us define multiplication. Can you also define notation
* for multiplication? Ask for help if you can’t do this, because if you can’t do it then you won’t get any further. Look at how I did all this with addition. Check you got it right either painstakingly with something like
example : one * one = one :=
or painlessly with
example : one * one = one :=
How many of the following can you prove:
theorem mul_zero (a : xnat) : a * zero = zero := sorry
theorem zero_mul (a : xnat) : zero * a = zero := sorry
theorem mul_one (a : xnat) : a * one = a := sorry
theorem one_mul (a : xnat) : one * a = a := sorry
theorem right_distrib (a b c : xnat) : a * (b + c) = a* b + a * c := sorry
If you’ve done all the ones above, here’s
left_distrib as a gift:
theorem left_distrib (a b c : xnat) : (a + b) * c = a * c + b * c :=
induction c with n Hn,
rw [add_assoc,←add_assoc (b*n),add_comm (b*n),←add_assoc,←add_assoc,←add_assoc],
Check you understand how it works. If you do then you should be able to manage
theorem mul_assoc (a b c : xnat) : (a * b) * c = a * (b * c) := sorry
theorem mul_comm (a b : xnat) : a * b = b * a := sorry
Let’s do inequalities!
definition lt : xnat → xnat → Prop
| zero zero := false
| (succ m) zero := false
| zero (succ p) := true
| (succ m) (succ p) := lt m p
notation a < b := lt a b
Can you see how that works? Can you prove inequality A1 that we assumed in lectures?
theorem inequality_A1 (a b t : xnat) : a < b → a + t < b + t := sorry
For the ultimate challenge (boss level), how about
theorem inequality_A2 (a b c : xnat) : a < b → b < c → a < c := sorry
theorem inequality_A3 (a b : xnat) : (a < b ∨ a = b ∨ b < a)
∧ (a < b → ¬ (a = b))
∧ (a < b → ¬ (b < a))
∧ (a = b → ¬ (b < a)) := sorry
theorem inequality_A4 (a b : xnat) : zero < a → zero < b → zero < a * b := sorry
These are the four standard inequalities that we assumed about the real numbers in M1F. I found some of these quite hard.
Can you define even / odd? Can you prove Lemma 1.1 of M1F? (recall: this said that
n^2 was even iff
n was even. Maybe just use
n^2 for now). Can you define a prime number? Can you define “a divides b”? Can you prove that every positive integer is uniquely the product of primes? Can you define powers? Can you prove basic things about powers like
pow x n * pow x m = pow x (n+m) or
x*x=pow x 2? Can you state Fermat’s Last Theorem in Lean? Nobody has ever proved Fermat’s Last Theorem in any computer proof verification system and this would be a very interesting goal for computer proof verification systems in general.