Recursion

Working with Peano $~\mathbb{N}$

We already know a good deal about the natural numbers from life but how do we work with Peano natural numbers. The answer is recursion.

Theorem. Let $Y$ be a set. For all $y \in Y$ and $h : \mathbb{N} \times Y \to Y$, there is a unique function $f : \mathbb{N} \to Y$ such that $f(0) = y$ and $f(s(n)) = h(s(n),f(n))$ for all $n \in \mathbb{N}$.

Proof. (Expand to view)

For an natural number of the form $0$ or $s(n)$ for some other natural number where we know $f(n)$, we can define $f$ directly. $$ \begin{aligned} f(0) & := y \\ f(s(n)) & := h(s(n),f(n)) \text{ whenever $f(n)$ is defined } \end{aligned} $$ Is this a definition for every $n \in \mathbb{N}$? Let $$ X := \lbrace n \in \mathbb{N} \mid f(n) \text{ is defined} \rbrace $$ Then $0 \in X$. And, if $n \in X$, then $s(n) \in X$ from the definition of $f$. Peano's last axiom says that $\mathbb{N} \subseteq X$. Of course, in this case, $X \subseteq \mathbb{N}$. So $X = \mathbb{N}$ and $f(n)$ is defined for all $n$. Now we turn to uniqueness of $f$. Assume we have two different functions $f,g : \mathbb{N} \to Y$ satisfying the conditions of the theorem and set $$ X := \lbrace n \in \mathbb{N} \mid f(n) = g(n) $$ Then $0 \in X$ since $f(0) = y = g(0)$. Assume that $n \in X$, so $f(n) = g(n)$. Then, $$ f(s(n)) = h(s(n),f(n)) = h(s(n),g(n)) = g(s(n)) $$ so $s(n) \in X$. Thus, $\mathbb{N} = X$ as before and $f = g$. ■

Now, let’s see what this means and how to use it. The function $h$ allows for any way to combine the natural number $s(n)$ and value, we already know, for $f(n)$.

Example. Suppose $Y = \mathbb{N}$. Let’s take our initial value to $1$. And let $h(n,m) = nm$, the product of $n$ and $m$.

Then we want a function $f: \mathbb{N} \to \mathbb{N}$ which satisfies

$f(0) = 1$ and
$f(n+1) = (n+1)f(n)$

The function that satisfies this is the factorial $n \mapsto n!$. We write the value $n!$ purely in terms of $n$ alone: $n! = n \cdot (n-1) \cdot (n-2) \cdot \cdots 2 \cdot 1$ Writing function defined via recursion this way is called its closed form.

In Lean, we can build factorial as

def Factorial (n : Nat) : Nat := 
  match n with 
  | 0 => 1 
  | m+1 => (m+1)*(Factorial m)

The match n with tells Lean consider the different ways we can get a natural number from its constructors. Either we have 0 or the number is a successor n = m+1. In each case, we have provided a value output by Factorial.

We see also that Lean knows that 0 really means zero and n+1 is succ n. We might also overlook that we used multiplication of natural numbers. Lean knows multiplication already but what did someone tell it.

def Mult (n m : Nat) : Nat := 
  match n, m with 
  | _, 0 => 0 
  | _, m+1 => Mult n m + n

We use $n(m+1) = nm + n$ to define multiplication recursively.

But now you might have noticed that we added terms of Nat. What is addition?

def Plus : Nat → Nat → Nat 
  | n, Nat.zero => n 
  | n, Nat.succ m => Nat.succ (Plus n m)

where we explicitly used Nat.zero and Nat.succ.

You can find the actual definitions of addition and multiplication in Nat under Nat.add and Nat.mul.

We can check that with our definition Plus n 1 = Nat.succ n for all n.

theorem plus_one_eq_succ (n : Nat) : Plus n 1 = Nat.succ n := by rfl

If we try the other order for adding one, you get the following error.

theorem one_plus_eq_succ (n : Nat) : Plus 1 n = Nat.succ n := by rfl 
tactic 'rfl' failed, equality lhs
  Plus 1 n
is not definitionally equal to rhs
  Nat.succ n

Why is this? As a hint, we try to break it into the cases for constructing n.

theorem one_plus_eq_succ (n : Nat) : Plus 1 n = Nat.succ n :=  
  match n with 
  | 0 => by rfl -- ok 
  | Nat.succ m => by rfl 
tactic 'rfl' failed, equality lhs
  Plus 1 (Nat.succ m)
is not definitionally equal to rhs
  Nat.succ (Nat.succ m)

If we look at the definition we have

Plus 1 (Nat.succ m) = Nat.Succ (Plus 1 m)

These are not the same! But we can use the proof for case of m to finish. We rewrite the right-hand side of the goal using Plus 1 m = Nat.succ m. Then Lean sees defintional equality.

theorem one_plus_eq_succ (n : Nat) : Plus 1 n = Nat.succ n :=  
  match n with 
  | 0 => by rfl 
  | Nat.succ m => by 
    conv => rhs rw[←one_plus_eq_succ m]

This is the our first encounter with induction.