working with `let rec` in proofs

Stream: new members

[Yannick Seurin]

import Mathlib

def my_fac : ℕ → ℕ
  | 0 => 1
  | n + 1 => (n + 1) * my_fac n

example : my_fac 0 = 1 :=
  rfl

example : 1 + 1 = 2 := by
  let rec my_fac' : ℕ → ℕ
    | 0 => 1
    | n + 1 => (n + 1) * my_fac' n
  have h : my_fac' 0 = 1 := rfl -- Type mismatch
  sorry

I'm confused about why I can't prove h with rfl here. I can't use rw [my_fac'] either. How can I prove h then?

[Aaron Liu]

it's not possible to refer to the insides of the let rec until you've finished the definition or theorem it was attached to

[Anthony Wang]

Out of curiosity, why is it not possible to do that?

[Aaron Liu]

it elaborates as a mutual block

[Yannick Seurin]

Thanks. So let's say I want to prove a theorem and in the course of the proof I need to define a recursive function f and prove intermediate results about f. Does that mean I have to define f outside the theorem? Or is there some other way?

[Eric Wieser]

Either outside the theorem, or without using Lean's pattern matching

[Yannick Seurin]

Sorry, what do you mean by "without using Lean's pattern matching"? How would it look like for my_fac' for example?

[Kenny Lau]

@Yannick Seurin use Nat.rec

[Yannick Seurin]

Like this?

import Mathlib

example : 1 + 1 = 2 := by
  let my_fac' (n : ℕ) : ℕ :=
    Nat.recOn n
      (1)
      (fun n ih => (n + 1) * ih)
  have h : my_fac' 0 = 1 := rfl
  have h' (n : ℕ) : my_fac' (n + 1) = (n + 1) * my_fac' n := rfl
  sorry

[Kenny Lau]

yes