Building the non-negative integers from scratch

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:

inductive xnat
| 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.

This 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.

The 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 succ function.

Firstly, you can just type zero, and you’ll get an xnat.

And secondly, if you have an xnat called 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 to 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).

namespace xena

inductive xnat
| zero : xnat
| succ : xnat → xnat

open xnat

#check zero -- it's an xnat

end xena

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 xnat.

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)

Because zero and 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, and a+succ(b) will just be succ(a+b).

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 :=
begin
unfold two,
unfold one,
unfold add,
end

It worked! In fact there is an easier way — the tactic refl just
unravels everything and then checks that you’re left with something of the
form x=x:

example : one + one = two :=
begin
refl
end

[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 :=
begin
dunfold two,
dunfold one,
dunfold add,
refl,
end

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 refl and 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 :=
begin
unfold add
end

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 :=
begin
induction n with t Ht,
  refl,
unfold add,
rewrite [Ht],
end

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 t in 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 refl with 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 rewrite command.

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).

Exercise 1

Can we prove “associativity of addition”? More precisely:

theorem add_assoc (a b c : xnat) : (a + b) + c = a + (b + c) :=
begin
admit
end

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 c?

Exercise 2

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 zero_add and 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 n using zero_add and add_zero.

theorem zero_add_eq_add_zero (n : xnat) : zero + n = n + zero :=
begin
rewrite [zero_add],
admit
end

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?

Exercise 3

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 :=
begin
unfold one,
unfold add,
end

Now you prove the harder one.

theorem one_add_eq_succ (n : xnat) : one + n = succ n :=
begin
admit
end

Exercise 4

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 a=0:

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

rw [←zero_add_eq_add_zero],

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),


[the 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 rewrite command.

Exercise 5

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 :=
begin
split,
  exact succ.inj,
assume H : a = b,
rw [H]
end

Now try cancellation:

theorem add_cancel_right (a b t : xnat) :  a = b ↔ a+t = b+t :=

Exercise 6

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 := 
begin
dunfold one,
dunfold mul,
dunfold add,
refl
end

or painlessly with

example : one * one = one := 
begin
refl
end

Exercise 7

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

Exercise 8

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 :=
begin
induction c with n Hn,
  unfold mul,
  refl,
rw [←add_one_eq_succ,right_distrib,Hn,right_distrib,right_distrib],
rw [mul_one,mul_one,mul_one],
rw [add_assoc,←add_assoc (b*n),add_comm (b*n),←add_assoc,←add_assoc,←add_assoc],
end

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

Exercise 9

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

Exercise 10

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.

Further exercises
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*n for 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.

Advertisements

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.
This entry was posted in Learning Lean. Bookmark the permalink.

2 Responses to Building the non-negative integers from scratch

  1. Ellen says:

    Could you put up the solutions for inequalities A2 to A4, please?

    Like

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s