Zulip Chat Archive

Stream: new members

Topic: Defining recursive sequences


Ben Nale (Jun 16 2020 at 21:30):

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 (Jun 16 2020 at 21:33):

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

Dan Stanescu (Jun 16 2020 at 21:33):

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

Ben Nale (Jun 16 2020 at 21:34):

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 (Jun 16 2020 at 21:34):

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 (Jun 16 2020 at 21:37):

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

Jalex Stark (Jun 16 2020 at 21:38):

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 (Jun 16 2020 at 21:38):

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 (Jun 16 2020 at 21:39):

Nice! Thanks

Ethan (Jul 04 2020 at 02:14):

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 (Jul 04 2020 at 02:15):

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

Mario Carneiro (Jul 04 2020 at 02:15):

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

Mario Carneiro (Jul 04 2020 at 02:16):

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 (Jul 04 2020 at 03:15):

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 (Jul 04 2020 at 03:35):

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 (Jul 04 2020 at 03:36):

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?


Last updated: Dec 20 2023 at 11:08 UTC