The following is the famous Fibonacci sequence.
$$ 1,\;1,\;2,\;3,\;5,\;8,\;13,\;21,\;\ldots $$
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.
$$f_{n}=\begin{cases}\:0 & \;\text{if }n=0\\\:2n-1+f_{n-1} & \;\text{otherwise}\end{cases}\tag{1}\label{22.1}$$
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\cdot1-1+f_{0}$. Using $f_{0}=0$, this becomes $f_{1}=1$.
- For $n=2$, the definition tells us $f_{2}=2\cdot2-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)\implies 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)\implies 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{align}P(n):f_{n}&=n^{2}&&\text{proof objective}\\&&&\\\text{base case }P(0)&&&\\&&&\\f(0)&=0&&\text{by definition }(\ref{22.1})\\&=0^{2}&&\text{so }P(0)\text{ is true}\\&&&\\\text{inductive step }P(n)&\implies P(n+1)&&\\&&&\\P(n):f_{n}&=n^{2}&&\text{induction hypothesis}\tag{2}\label{22.2}\\&&&\\f_{n+1}&=2\cdot n-1+f_{n}&&\text{by definition }(\ref{22.1})\\&=2\cdot n-1+n^{2}&&\text{by }(\ref{22.2})\\&=(n+1)^{2}&&\text{so }P(n+1)\text{ is true}\\&&&\\P(n):f_{n}&=n^{2}&&\text{by induction}\tag*{\(\Box\)}\end{align}$$
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\mapsto2n-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\mapsto2n+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 induction process and a recursively defined function.
We now see the similarity between an induction proof and a recursively defined function.
The two are clearly linked, and it may not surprise you that inside Lean, induction and recursion are unified.
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{cases}\:1 & \;\text{if }n=0\\\:(-1)\cdot g_{n-1} & \;\text{otherwise}\end{cases}$$
Write a recursive definition for $g_n$ in Lean, then show, by induction, that $g_{n}=(-1)^{n}$.
