Recurrence relations as theorems

Stream: lean4

[Mitchell Lee]

Suppose that I define the following recursive function.

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

There are three associated recurrence relations, all of which can be proved with rfl:

theorem fib_zero : fib 0 = 0 := rfl
theorem fib_one : fib 1 = 1 := rfl
theorem fib_add_two : fib (n + 2) = fib n + fib (n + 1) := rfl

Is there a way to define the function and generate these three theorems at the same time? For example, I tried this, but it didn't work.

def fib : Nat → Nat
  | fib_zero : 0 => 0
  | fib_one : 1 => 1
  | fib_add_two : n + 2 => fib n + fib (n + 1)

[Joachim Breitner]

Yes, you can! In fact lean already does that for you. The theorems you want are called fib.eq_1, fib.eq_2 and fib.eq_3 (from lean 4.8 on, before they also exist but aren't that easily accessible).
Unfortunately we don't allow the user to name them yet within the function definition, but you can use def fib_zero := @fib.eq_1 afterwards.

[Mitchell Lee]

Thank you!