# Peano numbers in Lean

## Table of Contents

In this post, I will define the natural numbers using the Peano axioms, which will be referred to here as Peano numbers, and prove that the set of natural numbers $\N$ equipped with ordinary addition and multiplication is a commutative semiring, i.e., that $(\N, +, 0)$ and $(\N, \cdot, 1)$ are both commutative monoids such that $a \cdot 0 = 0$ and $a \cdot (b + c) = a \cdot b + a \cdot c$.

The purpose of this post is to explore Lean’s capabilities in helping prove some simple theorems related to algebra.

## Defining the Peano numbers #

In Lean, the Peano numbers can be defined as an inductive type. In fact, the natural numbers in Lean are defined exactly like this. Likewise, I will define them like this:

```
inductive Peano : Type
| _0 : Peano
| S : Peano → Peano
```

Here, `_0`

represents the natural number 0 and `S`

represents the successor operation, and both are constructors for the type `Peano`

. I will also define the natural number 1 with `def _1 := S _0`

, which will be used to show some properties of the addition and multiplication operations.

## Forming a commutative semiring with the natural numbers #

As stated at the introduction of this post, the natural numbers equipped with ordinary addition and multiplication can be described as the commutative semiring $(\N, +, 0, \cdot, 1)$, which has the following properties:

- $(\N, +, 0)$ is the commutative monoid of $\N$ under addition, with identity element 0:
- Addition associativity: $(a + b) + c = a + (b + c)$.
- Addition identity element: $a + 0 = a$.
- Addition commutativity: $a + b = b + a$.

- $(\N, \cdot, 1)$ is the commutative monoid of $\N$ under multiplication, with identity element 1:
- Multiplication associativity: $(a \cdot b) \cdot c = a \cdot (b \cdot c)$.
- Multiplication identity element: $a \cdot 1 = a$.
- Multiplication commutativity: $a \cdot b = b \cdot a$.

- Multiplication absorbing element $\N$: $a \cdot 0 = 0$.
- Multiplication distributes over addition: $a \cdot (b + c) = a \cdot b + a \cdot c$.

This is because we would have to define the additive inverse $-a$ s.t. $a - a = 0$ and also define the multiplicative inverse $a^{-1}$ s.t. $aa^{-1} = 1$, both impossible given that we are working with the set of natural numbers.

## Proving the properties in Lean #

Now, we can start to prove all the described properties in Lean. I will not make the use of any library, like mathlib4, so everything will be done in vanilla Lean 4.

### Addition-related properties #

In this section, I will show the proofs for associativity, the identity element and commutativity, mostly inspired by the Wikipedia article with proofs involving addition. To start the proof, I will register the `Add`

instance for the `Peano`

type, allowing us to use the binary operator `+`

for addition:

```
instance : Add Peano where
add a b := _add a b
where _add a b := match b with
| _0 => a
| S b' => S (_add a b')
```

#### Associativity #

The associative property $(a + b) + c = a + (b + c)$ can be proven by induction on the number $c$:

```
@[simp]
theorem add_associativity (a b c : Peano) : (a + b) + c = a + (b + c) := by
induction c with
| _0 => rfl
| S c' ih => calc
a + b + S c' = S (a + b + c') := by rfl
_ = S (a + (b + c')) := by rw [ih]
_ = a + (b + S c') := by rfl
```

Here, `rfl`

stands for reflexivity, a Lean tactic that tries to close the current goal using the reflexive property, and `ih`

is the inductive hypothesis, defined as $a + b + c' = a + (b + c')$, where $c'$ is a natural number s.t. its successor is equal to $c$. I also defined this theorem with `@[simp]`

, which states that this theorem can be used by the `simp`

tactic to simplify the main goal.

#### Identity element #

The identity element for addition is 0, so we have to prove that $a + 0 = a$. I will also prove that $0 + a = a$, which will be useful when showing the proof for the addition commutativity.

For the right-identity, we can simply use the `rfl`

tactic, because Lean will match $a + 0$ with the addition definition:

```
@[simp]
theorem right_add_identity (a : Peano) : a + _0 = a := by
rfl
```

For the left-identity, the proof can be easily done by induction on $a$:

```
@[simp]
theorem left_add_identity (a : Peano) : _0 + a = a := by
induction a with
| _0 => rfl
| S a' ih => calc
_0 + S a' = S (_0 + a') := by rfl
_ = S a' := by rw [ih]
```

#### Commutativity #

The commutative property of addition can be divided into two steps:

- prove the property for a natural number $a$ and $1$ ($a + 1 = 1 + a$).
- From the last property, prove the same but for all pairs of natural numbers ($a + b = b + a$).

The first step can be done with induction on the number $a$, very similar to the `left_add_identity`

proof:

```
@[simp]
theorem add_commutativity_1 (a : Peano) : a + _1 = _1 + a := by
induction a with
| _0 => rfl
| S a' ih => calc
S a' + _1 = S (a' + _1) := by rfl
_ = S (_1 + a') := by rw [ih]
_ = _1 + S a' := by rfl
```

Finally, we can show the addition commutativity with the `simp`

tactic, that will apply all the theorems defined previously when possible.

```
@[simp]
theorem add_commutativity (a b : Peano) : a + b = b + a := by
induction b with
| _0 => simp
| S b' ih => calc
a + S b' = a + b' + _1 := by rfl
_ = b' + _1 + a := by simp [ih]
_ = S b' + a := by rfl
```

Here, the first `simp`

is applying both `right_add_identity`

and `left_add_identity`

to reduce the base statement $a + 0 = 0 + a$ to $a = a$. Moreover, the second `simp`

, written as `simp [ihb]`

, tells Lean that the inductive hypothesis defined in `ih`

should also be considere in the simplification process.

### Multiplication-related properties #

Now, I will do an analogous process from the last section. First, I will also register the `Mul`

instance, allowing us to use the binary operator `*`

for multiplication:

```
instance : Mul Peano where
mul a b := _mul a b
where _mul a b := match b with
| _0 => _0
| S b' => a + _mul a b'
```

#### Identity and annihilating elements #

Similar to the addition identity element proofs, I will show the identity ($a \cdot 1 = 1$) and annihilating ($a \cdot 0 = 0$) element property for both sides:

```
@[simp]
theorem right_mul_identity (a : Peano) : a * _1 = a := by
rfl
@[simp]
theorem left_mul_identity (a : Peano) : _1 * a = a := by
induction a with
| _0 => rfl
| S a' ih => calc
_1 * S a' = _1 + _1 * a' := by rfl
_ = a' + _1 := by rw [ih, add_commutativity]
```

```
@[simp]
theorem right_mul_annihilating (a : Peano) : a * _0 = _0 := by
rfl
@[simp]
theorem left_mul_annihilating (a : Peano) : _0 * a = _0 := by
induction a with
| _0 => rfl
| S a' ih => calc
_0 * S a' = _0 + _0 * a' := by rfl
_ = _0 := by rw [ih]; rfl
```

#### Distributivity #

The distributive property was a bit tricky for me, because it would be much easier to prove it with the associative property of multiplication, and I couldn’t find a way elaborate a proof for associativity without depending on the on the distributive property.

However, I think I landed on a satisfactory proof. For the right-distributivity, where we want to show that $(b + c) \cdot a = b \cdot a + c \cdot a$, I used the main properties defined for addition, with emphasis to the addition associativity, which I used with the `repeat`

property, that applies a tactic until until it fails:

```
@[simp]
theorem right_mul_distributivity (a b c : Peano) : (b + c) * a = b * a + c * a := by
induction a with
| _0 => simp
| S a' ih => calc
(b + c) * S a' = (b + c) + (b + c) * a' := by rfl
_ = b + (b * a' + c + c * a') := by simp [ih]
_ = (b + b * a') + (c + c * a') := by repeat (rw [add_associativity])
_ = b * S a' + c * S a' := by rfl
```

For the left-distributivity, where we want to show that $a \cdot (b + c) = a \cdot b + a \cdot c$, I had a hard time with the `simp`

tactic, because it started to run very slowly when I used it without any arguments. Because of this, I had to pass the `only`

option, that limits `simp`

to just use the expressions inside the brackets:

```
@[simp]
theorem left_mul_distributivity (a b c : Peano) : a * (b + c) = a * b + a * c := by
induction a with
| _0 => simp
| S a' ih => calc
S a' * (b + c) = (a' + _1) * (b + c) := by rfl
_ = a' * (b + c) + _1 * (b + c) := by rw [right_mul_distributivity]
_ = a' * (b + c) + b + c := by rw [left_mul_identity, add_associativity]
_ = b + a' * b + c + a' * c := by simp [ih]
_ = (_1 + a') * b + (_1 + a') * c := by simp only [left_mul_identity, right_mul_distributivity, add_associativity]
_ = S a' * b + S a' * c := by simp only [add_commutativity]; rfl
```

#### Associativity #

Basically, the associative property of multiplication, $(a \cdot b) \cdot c = a \cdot (b \cdot c)$, can be proved by induction on $c$, where we have to use the left-distributivity of multiplication, proved in the last subsection:

```
@[simp]
theorem mul_associativity (a b c : Peano) : (a * b) * c = a * (b * c) := by
induction c with
| _0 => rfl
| S c' ih => calc
a * b * S c' = a * b + a * b * c' := by rfl
_ = a * (b + b * c') := by rw [ih, left_mul_distributivity]
_ = a * (b * S c') := by rfl
```

#### Commutativity #

Finally, we can prove the last property related to multiplication, the commutativity. Because we have all the previous properties already defined, prove this property is very simple:

```
@[simp]
theorem mul_commutativity (a b: Peano) : a * b = b * a := by
induction b with
| _0 => rw [left_mul_annihilating, right_mul_annihilating]
| S b' ih => calc
a * S b' = a * (b' + _1) := by rfl
_ = a * b' + a * _1 := by rw [left_mul_distributivity]
_ = _1 * a + b' * a := by simp [ih]
_ = (b' + _1) * a := by rw [right_mul_distributivity, add_commutativity]
```

## Conclusion #

For some months until now, I had the wish to learn a proof assistant language, and I have considered some languages like Coq (now Rocq), Agda, Idris, etc. However, in the last weeks, I saw that Lean, specially at the version 4, is a very capable and developed language for interactive theorem proving with a very passionate community, and proving all the theorems of this post was a fun exercise to see what I could do in the language. In the future, I hope to learn more about Lean and even start to prove things that are relevant for projects that I will be working.

If you want to see the full code, I recommend to see the gist I created. I will be updating it if I find simpler or more elegant proofs for the theorems (because I don’t know if I will update this blog post with the modifications).