## Stream: general

### Topic: rec_on works in tactic mode, but fails in a term

#### Chris Wong (Jul 23 2020 at 11:01):

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 (Jul 23 2020 at 11:04):

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 (Jul 23 2020 at 11:15):

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 (Jul 23 2020 at 11:25):

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 (Jul 23 2020 at 11:32):

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

Last updated: Aug 03 2023 at 10:10 UTC