# How to define a recursive sequence in Lean?

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$$
• Do you plan to compute with f or just do math with it? That probably makes a difference. fib is defined with a stream in mathlib for performance. I'm not sure if that is recommended though. Feb 12, 2022 at 19:02
• Are you trying to define a specific sequence, or the class of such sequences? Feb 12, 2022 at 19:25
• @JasonRute I intend to do math with it, think of proving properties of the fibonacci sequence using its recursion formula. Nevertheless, it would be interesting to hear about the computational aspect as well. Feb 12, 2022 at 19:27
• @AlexJBest a specific sequence Feb 12, 2022 at 19:29
• @Eric with $F$ I did not want to have an explicit function, but any expression of some kind. So it is not necessarily required to include $N$. For instance, see the second example. Feb 19, 2022 at 10:03

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

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.