## 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):

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.

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.

### 3 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

• xenaproject says:

Hi Ellen. I did do all of these but I can’t remember where I left the file

I have put up your solutions here:

Ellen’s solutions

Well done for getting to Q9! Can anyone do A2 to A4?

Kevin

Like

2. Pingback: Working with integers | Xena