Unknown identifier in recursive function call

Stream: new members

[Paul Rowe]

I'm trying to write a recursive function and Lean is telling me it doesn't know the name of the function. The function deals with a structure exec that is a finite partial order (among other things), and the recursive call should replace one item in that structure with another that is strictly below it. I would have expected to have to convince Lean that this is an ok well-founded recursion, but it doesn't even give me the chance. It complains unknown identifier 'cs' at the site of the recursive call.

Can anybody help me figure out how to restructure such a function so Lean will accept it?

noncomputable def cs : Π (E : exec), E.evt → component → option cstate :=
λ E e c,
match (E.l e) with
| cor c := corrupt
| rep c := regular
| msp _ _ := dite (relevant E e c)
    (λ (r : relevant E e c),
      dite (∃ e' ∈ (ard E e c), ∀ e'' ∈ (ard E e c), e'' ≤ e')
      (λ (m : ∃ e' ∈ (ard E e c), ∀ e'' ∈ (ard E e c), e'' ≤ e'),
        cs E (max_adv E e c r m) c)
      (λ (m : ¬∃ e' ∈ (ard E e c), ∀ e'' ∈ (ard E e c), e'' ≤ e'), none))
    (λ (r : ¬relevant E e c), none)
| _ := none
end

[Patrick Massot]

Helping you would be much easier with a #mwe

[Paul Rowe]

Sorry. What's the norm around here? I could paste ~250 lines of code. Otherwise, I would have to work to extract something more minimal.

[Johan Commelin]

In that case, maybe paste it into a github gist.

[Johan Commelin]

The point is, to help we need to know preceding definitions, and whatever you import, etc

[Mario Carneiro]

You need to write it using the equation compiler if you want to write a recursive function by calling cs inside the body

[Mario Carneiro]

so something like this:

noncomputable def cs : Π (E : exec), E.evt → component → option cstate
| E e c :=
  match (E.l e) with
  | cor c := corrupt
  | rep c := regular
  | msp _ _ := dite (relevant E e c)
      (λ (r : relevant E e c),
        dite (∃ e' ∈ (ard E e c), ∀ e'' ∈ (ard E e c), e'' ≤ e')
        (λ (m : ∃ e' ∈ (ard E e c), ∀ e'' ∈ (ard E e c), e'' ≤ e'),
          cs E (max_adv E e c r m) c)
        (λ (m : ¬∃ e' ∈ (ard E e c), ∀ e'' ∈ (ard E e c), e'' ≤ e'), none))
      (λ (r : ¬relevant E e c), none)
  | _ := none
  end
using_well_founded {dec_tac := tactic.assumption} -- or something

[Paul Rowe]

@Mario Carneiro Thanks! That does the trick. It now is asking me to prove well-founded induction will work.

[Paul Rowe]

Which is, of course, what I was expecting to find in the first place.