rec_on works in tactic mode, but fails in a term

Stream: general

[Chris Wong]

The following code works:

import data.list.basic

variables {α : Type*}

open list

inductive palindrome : list α → Prop
| zero : palindrome []
| one : ∀ a, palindrome [a]
| many : ∀ a {l}, palindrome l → palindrome (a :: (l ++ [a]))

theorem to_reverse_eq {l : list α} (p : palindrome l) : reverse l = l :=
begin
  refine p.rec_on _ _ _,
  { refl },
  { intros a, refl },
  { intros a l p h, simp [h] },
end

But when I replace the begin ... end block with:

p.rec_on rfl (λ a, rfl) (λ a l p h, by simp [h])

I get this error:

type mismatch at application
  p.rec_on rfl (λ (a : α), rfl)
term
  λ (a : α), rfl
has type
  ∀ (a : α), ?m_2[a] = ?m_2[a]
but is expected to have type
  ∀ (a : α), nil = [a]

What's the reason for this discrepancy?

[Shing Tak Lam]

Change it to not use projection notation, so palindrome.rec_on p instead of p.rec_on then it works. There's an explanation somewhere, I'll try to find it

theorem to_reverse_eq {l : list α} (p : palindrome l) : reverse l = l :=
palindrome.rec_on p rfl (λ a, rfl) (λ a l p h, by simp [h])

[Shing Tak Lam]

Found it

You can't use projection notation with @[elab_as_eliminator] functions

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Natural.20Numbers.20Game/near/199965854

[Chris Wong]

Thanks! That does seem rather obscure.

I wonder if we can special case this – maybe warn when projection notation is used with an @[elab_as_eliminator]? Or even outright ban them, if it's never a good idea to call them this way.

[Mario Carneiro]

I think it's a bug in lean somewhere. There isn't any principled reason for it to be like that AFAICT