Zulip Chat Archive

Stream: general

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


view this post on Zulip 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?

view this post on Zulip 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])

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: May 10 2021 at 00:31 UTC