Let rec missing from context

Stream: new members

[Stefan Volz]

Hey (first time writing here - I hope I didn't miss anything and this is the right place to post). I have a small problem with an index proof involving a locally defined function. I currently have this code

structure PcwFn (δ α : Type) [Preorder δ] (n : ℕ) where
  borders: Vector δ n
  fns: Vector α (n + 1)
  bordersOrdered: List.Sorted (·<·) borders.toList

def PcwFn.func_at [Preorder δ] (f : PcwFn δ α n) (x : δ) {xComparisonDec : DecidablePred (x<·) } : α :=
  let rec helper (i : ℕ) : List δ -> ℕ
    | [] => i
    | (t :: ts) => if x < t then i else helper (i+1) ts
  let j: ℕ := helper 0 (f.borders.toList)
  let h: j < n + 1 := by
    induction n
    {
      simp
      unfold helper
    }
    {

    }
  f.fns[j]'h

and my problem is that helper is not part of the current context inside of the proof of h - in particular the unfold helper isn't valid because of that. I've tried a few different things but can't get it to work. Any pointer would be very much appreciated, thanks.

[Timo Carlin-Burns]

I'm no expert, but from playing around with it, it seems like as soon as you define something with let rec, Lean forgets the equations you used to define it. The following small example fails too:

example : True :=
  let rec fac : Nat → Nat
    | 0 => 1
    | (n + 1) => (n + 1) * fac n
  have : fac 0 = 1 := rfl -- error; lean seems to have no idea how fac is defined

  trivial

There may be a workaround still using let rec, but another option is to create a (private) top-level definition instead:

private def linearSearch [Preorder δ] (x : δ) [DecidablePred (x < ·)] (i : ℕ) : List δ -> ℕ
  | [] => i
  | (t :: ts) => if x < t then i else linearSearch x (i+1) ts

def PcwFn.func_at [Preorder δ] (f : PcwFn δ α n) (x : δ) {xComparisonDec : DecidablePred (x<·) } : α :=
  let j: ℕ := linearSearch x 0 (f.borders.toList)
  have h: j < n + 1 := by
    induction' n
    {
      simp [linearSearch]
    }
    {

    }
  f.fns[j]'h

[Stefan Volz]

That works - thanks!