How to define a recursive sequence in Lean?

Question

Given a recursive sequence of the form $$ f_n = \begin{cases} c_n & n ≤ N\\ F(f_1, f_2, …, f_{n - 1}) & n > N \end{cases} $$ where $c_n$ are constants and $F$ is an arbitrary expression of $f_1, …, f_{n-1}$. What is the best way to define such a sequence in Lean?

Examples:

• The Fibonacci sequence with $f_0 = 0$, $f_1 = 1$, $f_{n + 2} = f_{n + 1} + f_{n}$
• $f_0 = 1$, $f_{n + 1} = \sum_{i = 0}^n f_i$

Answer 1

For Lean 3, I'd start out with something like:

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

or for your second example:

def foo : ℕ → ℕ
| 0 := 1
| (n + 1) := (foo n) + (foo n)

(I modified your second example to be easier to express recursively. You should be able to prove that foo 0 + ... + foo n = f (n+1), although I admit I don't know the lean notation off hand.)

If this becomes difficult to work with for your use case, then maybe ask another question with the example you are working on as there are other ways to define this which might have better properties for your particular use case.

In particular, we are treating the sequence 0, 1, 1, 2, 3,... as a function fib : ℕ → ℕ. This is a standard way to work with sequences, and is easy to prove things about.

If you also need your sequence to depend on a parameter, like maybe we are starting fib with two numbers a and b, then the notation is maybe a bit confusing at first:

def fib_general (a : ℕ) (b : ℕ) : ℕ → ℕ 
| 0 := a
| 1 := b
| (n + 2) := fib_general n + fib_general (n+1)

In particular notice that we don't pass a and b to the recursive call since they are in a sense fixed.

Here is a resource for more information: https://leanprover.github.io/logic_and_proof/the_natural_numbers_and_induction_in_lean.html

Answer 2

Here's an implementation of a more general n-step recurrence formula, using fin n → R as the type of n-tuples:

import data.fin.tuple
import data.fin.vec_notation
import algebra.big_operators

/-- A general $n$-step recurrence relation, `f = recurrence F c` is the sequence
starting with $f_i = c_i$ for $i ≤ n$ and proceeding with
$f_{i+1} = F(f_{i-n},...f_i)$.

With each step, we pop the first item from `c` and append `F c`. -/
def recurrence {n : ℕ} {R : Type*} (F : (fin n.succ → R) → R) : (fin n.succ → R) → ℕ → R
| c 0 := c 0
| c (i + 1) := recurrence (fin.snoc (fin.tail c) (F c)) i

We can use this to build the Fibonacci numbers as:

def fib : ℕ → ℕ := recurrence finset.univ.sum ![0, 1]

#eval (fib ∘ (coe : fin 10 → ℕ))  -- ![0, 1, 1, 2, 3, 5, 8, 13, 21, 34]

Note that ∘ (coe : fin 10 → ℕ) is a convenient trick to get lean to show us the first 10 items of the sequence when using #eval.