Defining recursive sequences

Stream: new members

[Ben Nale]

Hi. I need help defining sequences in Lean like a_n = n *a_{n-1} and a_1=1. How do I do this?
And for future references, where do I learn such things on my own. Like, for instance how do I see how the successor function (natural numbers) is defined?

[Jalex Stark]

Have you looked at a tutorial? maybe #mil or the natural number game?

[Dan Stanescu]

Section 7.4 here for the natural numbers
https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html

[Ben Nale]

Jalex Stark said:

Have you looked at a tutorial? maybe #mil or the natural number game?

I finished the natural number game. And also couldn't find it in the tutorial :/

[Ben Nale]

Dan Stanescu said:

Section 7.4 here for the natural numbers
https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html

Thank you

[Kevin Buzzard]

You can make this definition using the equation compiler. Maybe chapter 8 of #tpil ?

[Jalex Stark]

https://leanprover.github.io/reference/declarations.html#the-equation-compiler

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

[Bryan Gin-ge Chen]

To answer your original question, a sequence of natural numbers is just a function from natural numbers to the natural numbers. Chapter 8 of "Theorem Proving in Lean" will explain how to write recursive definitions by pattern matching, e.g.:

def a : ℕ → ℕ
| 0 := 0 -- junk value
| 1 := 1 -- base case
| (n+1) := (n + 1) * a n

#eval a 40

[Ben Nale]

Nice! Thanks

[Ethan]

Is there any intuition for the difference between:

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

and

def fib2 : ℕ → ℕ := λ n, match n with
| 0     := 1
| 1     := 1
| (n+2) := fib2 (n+1) + fib2 n
end

fib works, but fib2 is not in scope.

[Mario Carneiro]

You can't define recursive functions using a regular definition, you have to use the equation compiler form (like fib)

[Mario Carneiro]

If you write def foo : type := ... then foo is not in scope in ...

[Mario Carneiro]

but with def foo : type | case := ... then foo is in scope (although it is fake), and the equation compiler figures out how to turn it into a definition using recursors

[Pedro Minicz]

Mario Carneiro said:

You can't define recursive functions using a regular definition, you have to use the equation compiler form (like fib)

"Equation compiler form" is rather suggestive, but I will ask anyways: why is that so? What does it facilitate not permitting fib2?

[Bryan Gin-ge Chen]

The "equation compiler" is a part of Lean's elaborator that is able to generate certain types of recursive functions automatically from some special "pattern-matching" syntax. Match expressions also use pattern-matching syntax, but just don't have access to the equation compiler. The equation compiler / pattern-matching syntax is discussed in most of chapter 8 of #tpil and match expressions are discussed in 8.8.

[Bryan Gin-ge Chen]

Oh, I see that I already mentioned that chapter of TPIL a few times above. Apologies if you already read it. Maybe I misunderstood your question?