18. The Natural Numbers and Induction in Lean

18.1. Induction and Recursion in Lean

Internally, in Lean, the natural numbers are defined as a type generated inductively from an axiomatically declared zero and succ operation:

inductive nat : Type
| zero : nat
| succ : nat  nat

If you click the button that copies this text into the editor in the online version of this textbook, you will see that we wrap it with the phrases namespace hide and end hide. This puts the definition into a new “namespace,” so that the identifiers that are defined are hide.nat, hide.nat.zero and hide.nat.succ, to avoid conflicting with the one that is in the Lean library. Below, we will do that in a number of places where our examples duplicate objects defined in the library. The unicode symbol , entered with \N or \nat, is a synonym for nat.

Declaring nat as an inductively defined type means that we can define functions by recursion, and prove theorems by induction. For example, these are the first two recursive definitions presented in the last chapter:

open nat

def two_pow :   
| 0        := 1
| (succ n) := 2 * two_pow n

def fact :   
| 0        := 1
| (succ n) := (succ n) * fact n

Addition and numerals are defined in such a way that Lean recognizes succ n and n + 1 as essentially the same, so we could instead write these definitions as follows:

def two_pow :   
| 0       := 1
| (n + 1) := 2 * two_pow n

def fact :   
| 0       := 1
| (n + 1) := (n + 1) * fact n

If we wanted to define the function m^n, we would do that by fixing m, and writing doing the recursion on the second argument:

def pow :     
| m 0        := 1
| m (n + 1)  := m * pow m n

Lean is also smart enough to interpret more complicated forms of recursion, like this one:

def fib :   
| 0        := 0
| 1        := 1
| (n + 2)  := fib (n + 1) + fib n

In addition to defining functions by recursion, we can prove theorems by induction. In Lean, each clause of a recursive definition results in a new identity. For example, the two clauses in the definition of pow above give rise to the following two theorems:

theorem pow_zero (n : ) : pow n 0 = 1 := rfl
theorem pow_succ (m n : ) : pow m (n+1) = m * pow m n := rfl

Notice that we could alternatively have used (pow m n) * m in the second clause of the definition of pow. Of course, we can prove that the two definitions are equivalent using the commutativity of multiplication, but, using a proof by induction, we can also prove it using only the associativity of multiplication, and the properties 1 * m = m and m * 1 = m. This is useful, because the power function is also often used in situations where multiplication is not commutative, such as with matrix multiplication. The theorem can be proved in Lean as follows:

theorem pow_succ' (m n : ) : pow m (succ n) = (pow m n) * m :=
nat.rec_on n
  (show pow m (succ 0) = pow m 0 * m, from calc
    pow m (succ 0) = m * pow m 0 : by rw pow_succ
               ... = m * 1       : by rw pow_zero
               ... = m           : by rw mul_one
               ... = 1 * m       : by rw one_mul
               ... = pow m 0 * m : by rw pow_zero)
  (assume n,
    assume ih : pow m (succ n) = pow m n * m,
    show pow m (succ (succ n)) = pow m (succ n) * m, from calc
      pow m (succ (succ n)) = m * (pow m (succ n)) : by rw pow_succ
                        ... = m * (pow m n * m)    : by rw ih
                        ... = (m * pow m n) * m    : by rw mul_assoc
                        ... = pow m (succ n) * m   : by rw pow_succ)

This is a typical proof by induction in Lean. It begins with the phrase nat.induction_on n, and is followed by the base case and the inductive hypothesis. The proof can be shortened using rewrite and simp:

theorem pow_succ' (m n : ) : pow m (succ n) = (pow m n) * m :=
nat.rec_on n
  (show pow m (succ 0) = pow m 0 * m,
    by rw [pow_succ, pow_zero, mul_one, one_mul])
  (assume n,
    assume ih : pow m (succ n) = pow m n * m,
    show pow m (succ (succ n)) = pow m (succ n) * m,
      by simp [pow_succ, ih])

Remember that you can write a rewrite proof incrementally, checking the error messages to make sure things are working so far, and to see how far Lean got.

In any case, the power function is already defined in the Lean library as pow_nat. (It is defined generically for any type that has a multiplication; the nat in pow_nat refers to the fact that the exponent is a natural number.) The definition is essentially the one above, and the theorems above are also there:

import algebra.group_power
local infix ` ^ ` := pow_nat

#check @pow_nat
#check @pow_zero
#check @pow_succ
#check @pow_succ'

variables m n : 

#check m^n

As another example of a proof by induction, here is a proof of the identity m^(n + k) = m^n * m^k.

theorem pow_add (m n k : ) : m^(n + k) = m^n * m^k :=
nat.rec_on k
  (show m^(n + 0) = m^n * m^0, from calc
    m^(n + 0) = m^n       : by rw add_zero
          ... = m^n * 1   : by rw mul_one
          ... = m^n * m^0 : by rw pow_zero)
  (assume k,
    assume ih : m^(n + k) = m^n * m^k,
    show m^(n + succ k) = m^n * m^(succ k), from calc
      m^(n + succ k) = m^(succ (n + k)) : by rw nat.add_succ
                 ... = m^(n + k) * m    : by rw pow_succ'
                 ... = m^n * m^k * m    : by rw ih
                 ... = m^n * (m^k * m)  : by rw mul_assoc
                 ... = m^n * m^(succ k) : by rw pow_succ')

Notice the same pattern. This time, we do induction on k, and the base case and inductive step are routine. Once again, with a bit of cleverness, we can shorten the proof with rewrite:

theorem pow_add (m n k : ) : m^(n + k) = m^n * m^k :=
nat.rec_on k
  (show m^(n + 0) = m^n * m^0,
    by rewrite [add_zero, pow_zero, mul_one])
  (assume k,
    assume ih : m^(n + k) = m^n * m^k,
    show m^(n + succ k) = m^n * m^(succ k),
     by rewrite [nat.add_succ, pow_succ', ih, mul_assoc, pow_succ'])

You should not hesitate to use calc, however, to make the proofs more explicit. Remember that you can also use calc and rewrite together, using calc to structure the calculational proof, and using rewrite to fill in each justification step.

18.2. Defining the Arithmetic Operations in Lean

In fact, addition and multiplication are defined in Lean essentially as described in Section 17.4. The defining equations for addition hold by reflexivity, but they are also named add_zero and add_succ:

open nat

variables m n : 

example : m + 0 = m := add_zero m
example : m + succ n = succ (m + n) := add_succ m n

Similarly, we have the defining equations for the predecessor function and multiplication:

open nat

#check @pred_zero
#check @pred_succ
#check @mul_zero
#check @mul_succ

Here are the five propositions proved in Section 17.4.

theorem succ_pred (n : ) : n  0  succ (pred n) = n :=
nat.rec_on n
  (assume H : 0  0,
    show succ (pred 0) = 0, from absurd rfl H)
  (assume n,
    assume ih,
    assume H : succ n  0,
    show succ (pred (succ n)) = succ n,
      by rewrite pred_succ)

theorem zero_add (n : nat) : 0 + n = n :=
nat.rec_on n
  (show 0 + 0 = 0, from rfl)
  (assume n,
    assume ih : 0 + n = n,
    show 0 + succ n = succ n, from
      calc
    0 + succ n = succ (0 + n) : rfl
      ... = succ n : by rw ih)

theorem succ_add (m n : nat) : succ m + n = succ (m + n) :=
nat.rec_on n
  (show succ m + 0 = succ (m + 0), from rfl)
  (assume n,
    assume ih : succ m + n = succ (m + n),
    show succ m + succ n = succ (m + succ n), from
      calc
    succ m + succ n = succ (succ m + n) : rfl
      ... = succ (succ (m + n)) : by rw ih
      ... = succ (m + succ n) : rfl)

theorem add_assoc (m n k : nat) : m + n + k = m + (n + k) :=
nat.rec_on k
  (show m + n + 0 = m + (n + 0), by rw [add_zero, add_zero])
  (assume k,
    assume ih : m + n + k = m + (n + k),
    show m + n + succ k = m + (n + (succ k)), from calc
      m + n + succ k = succ (m + n + k)   : by rw add_succ
                 ... = succ (m + (n + k)) : by rw ih
                 ... = m + (n + succ k)   : by rw add_succ)

theorem add_comm (m n : nat) : m + n = n + m :=
nat.rec_on n
  (show m + 0 = 0 + m, by rewrite [add_zero, zero_add])
  (assume n,
    assume ih : m + n = n + m,
    show m + succ n = succ n + m, from calc
      m + succ n = succ (m + n) : by rw add_succ
             ... = succ (n + m) : by rw ih
             ... = succ n + m   : by rw succ_add)

18.3. Exercises

  1. Consider the theorems in Section 17.4 and Section 17.5. Formalize as many of them as you can in Lean.