Peano numbers in Lean

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:

1. prove the property for a natural number $a$ and $1$ ($a + 1 = 1 + a$).
2. 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).