22 - Recursion

The following is the famous Fibonacci sequence. 

$$1,1,2,3,5,8,13,21,\dots$$

From 2 onwards, each number is the sum of the previous two. This is an example of a recursive definition.

Here we'll see how to define and work with a recursively defined function.

Task

The following is a recursively defined function $f_n$. It takes a natural number n, and returns a natural number.

$$\begin{array}{}\text{(1)}& f_n=\{\begin{array}{ll}0& \text{if }n=0\\ 2n-1+f_{n-1}& \text{otherwise}\end{array}\end{array}$$

Let's see how it works.

• For $n=0$, the definition tells us $f_0=0$.
• For $n=1$, the definition tells us $f_1=2\cdot 1-1+f_0$. Using $f_0=0$, this becomes $f_1=1$.
• For $n=2$, the definition tells us $f_2=2\cdot 2-1+f_1$. Using $f_1=1$, this gives us $f_2=4$.
• Try $n=3$ yourself. You should get $f_3=9$.

What makes the definition recursive is that, apart from $f_0$, each value of the function $f_n$ is defined in terms of an earlier value $f_{n-1}$. Informally, the function is defined in terms of itself.

Our task is to prove this recursively defined function has a much neater closed form,

$$f_n=n^2$$

Similarity To Induction

It is worth pausing to reflect on the process of calculating each $f_n$. 

It looks very similar to the process of induction we saw in the last chapter.

Maths

We'll try a proof by induction. Let $P(n)$ be the proposition $f_n=n^2$. 

The base case $P(0)$ is the proposition $f_0=0^2$. The definition tells us $f_0=0$ so the base case $P(0)$ is indeed true.

The inductive step is the implication $P(n)⟹P(n+1)$. To prove this we assume $P(n)$ is true and derive $P(n+1)$. That is, we assume $f_n=n^2$ and derive $f_{n+1}=(n+1{)}^2$.

• The definition (1) tells us $f_{n+1}=2(n+1)-1+f_n$. 
• By assumption $f_n=n^2$, so $f_{n+1}=2(n+1)-1+n^2$.
• That $2(n+1)-1+n^2$ simplifies to $(n+1{)}^2$.
• Putting all this together, we have $f_{n+1}=(n+1{)}^2$.

We have shown the base case $P(0)$ and the inductive step $P(n)⟹P(n+1)$ are true, and so, by induction, $P(n)$ is true for all natural numbers $n$. That is, $f_n=n^2$ is true for all $n$.

Let's write this out as preparation for a Lean proof. 

$$\begin{array}{rlrl}P(n):f_n& =n^2& & \text{proof objective}\\ & & & \\ \text{base case }P(0)& & & \\ & & & \\ f(0)& =0& & \text{by definition }(\text{1})\\ & =0^2& & \text{so }P(0)\text{ is true}\\ & & & \\ \text{inductive step }P(n)& ⟹P(n+1)& & \\ & & & \\ \text{(2)}& P(n):f_n& =n^2& & \text{induction hypothesis}& & & \\ f_{n+1}& =2\cdot n-1+f_n& & \text{by definition }(\text{1})\\ & =2\cdot n-1+n^2& & \text{by }(\text{2})\\ & =(n+1{)}^2& & \text{so }P(n+1)\text{ is true}\\ & & & \\ ◻& P(n):f_n& =n^2& & \text{by induction}\end{array}$$

Code

The following Lean program proves, by induction, that $f_n=n^2$.

-- 22 - Recursion

import Mathlib.Tactic

def f : ℕ → ℕ
  | 0 => 0
  | n + 1 => 2 * n + 1 + f n

#eval f 2

example {n: ℕ} : f n = n^2 := by
  induction n with
  | zero =>
    calc
      f 0 = 0 := by rw [f]
      _ = 0^2 := by norm_num
  | succ n ih =>
    calc
      f (n + 1) = 2 * n + 1 + f n := by rw [f]
      _ = 2 * n + 1 + n^2 := by rw [ih]
      _ = (n + 1)^2 := by ring

This code is in three parts. Let's look at each in turn.

Definition

The first part is the recursive definition of f.

The f : ℕ → ℕ declares f as a function which maps natural numbers to natural numbers. 

Even though the code is new, we can see how it maps 0 to 0, and n + 1 to 2 * n + 1 + f n. Here f n means “f applied to n”, which is just $f_n$.

Our earlier definition (1) mapped $n\mapsto 2n-1+f_{n-1}$. We can't use $f_{n-1}$ in the Lean definition because $(n-1)$ does not exist for all natural numbers $n$. By replacing $n$ with $n+1$, we get the equivalent $n+1\mapsto 2n+1+f_n$. 

Evaluation

The second part tests our function behaves as we expect.

The #eval is a special instruction which evaluates an expression and prints the answer in the Infoview. Just as #eval 2 + 3 will print 5, #eval f 2 will evaluate the function f applied to 2, and print the answer. Try evaluating f with other parameters.

Proof

The third part is the proof of the proposition f n = n^2. 

This proof by induction is not very different to the one we saw in the last chapter.

• The base case needs to prove f 0 = 0 ^ 2. We do this with a calc section. The first step f 0 = 0 is justified by rw [f] which uses the first part of the recursive definition | 0 => 0.
• The inductive step needs to prove f (n + 1) = (n + 1) ^ 2, and also uses a calc section. The first step which equates f (n + 1) with 2 * n + 1 + f n is similarly justified by rw [f], which this time uses the recursive part of the definition.

Recursion & Induction

We saw earlier the similarity between the process of induction and the evaluation of a recursively defined function.

We now see the similarity between the structure of an induction proof and the definition of a recursively defined function.

These similarities are not a coincidence. If you're curious to find out more, search the more advanced guides for recursive types.

Infoview

Placing the cursor after #eval f 2 shows the result of the function f applied to 2.

4

Changing the code to #eval f 3 shows the result of the function f applied to 3.

9

---

Exercise

The following is a recursively defined function $g_n$, which maps natural numbers to integers,

$$g_n=\{\begin{array}{ll}1& \text{if }n=0\\ (-1)\cdot g_{n-1}& \text{otherwise}\end{array}$$

Write a recursive definition for $g_n$ in Lean, then show, by induction, that $g_n=(-1{)}^n$.