Failed to elaborate eliminator

Stream: lean4

[Arien Malec]

Have searched the Zulip on this, but not gotten a terribly clear answer.

I have a port in progress that's failing on a single error:

@[simp]
theorem rec.constant {α : Sort u} {β : Type v} (b : β) :
    (@PLift.rec α (fun _ => β) fun _ => b) = fun _ => b :=
        funext fun x => PLift.casesOn x fun a => Eq.refl (PLift.rec (fun a' => b) { down := a })

Fails with failed to elaborate eliminator, expected type is not available on PLift.rec (fun a' => b) { down := a } & I'm frankly not clear on where rec and casesOn come from here, despite crawling source.

[Arien Malec]

Working through https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.22Failed.20to.20elaborate.20eliminator.22/near/297811146

& switching to @Plift.rec gets me

application type mismatch
  @rec fun a' => b
argument
fun a' => b
has type
  ?m.3111 → β : Sort (max (v + 1) ?u.3110)
but is expected to have type
  Sort ?u.3108 : Type ?u.3108

Which I think leads me a bit along the path?

[Jireh Loreaux]

The issue (I think) is that Lean is failing to compute the motive properly. A few things:

1. PLift.rec and PLift.casesOn are autogenerated definitions created when you declare an inductive, in this case, PLift
2. You may want to follow the advice in the thread you linked and mark Plift.rec with the elabAsElim attribute. Normally you would just add this with @[elabAsEim] immediately prior to the declaration, but since this is autogenerated you can't do that. Instead, you can add it manually by adding the line attribute [elabAsElim] PLift.rec.
3. If that doesn't fix your problems (or if for some reason it is the wrong approach), then you'll need to provide the motive to Lean manually (or give it some extra information somehow to help it out). To do this, it helps to have the mathlib3 version of the file open so that you can inspect the motive in the tactic state.

[Jireh Loreaux]

(by the way, a structure is just an inductive with a single constructor with some extra special tooling, so it also gets the .rec and .casesOn)

[Arien Malec]

I think it's elab_as_elim now, but can't get either attribute to stick. Perhaps a missing import...

[Jireh Loreaux]

What error do you get?

[Arien Malec]

for elabAsElim, unknown attribute; for elab_as_elim, invalid attribute, declaration is in an imported module, which maybe means that since the definition is upstream, I can't modify the attribute?

[Mario Carneiro]

you can't apply elab_as_elim (or most attributes) to a declaration in another file

[Mario Carneiro]

but you can make a copy of the definition and tag that

[Mario Carneiro]

by the way, this works for the original proof:

@[simp]
theorem rec.constant {α : Sort u} {β : Type v} (b : β) :
    (@PLift.rec α (fun _ => β) fun _ => b) = fun _ => b :=
        funext fun x => PLift.casesOn x fun a => Eq.refl _

[Mario Carneiro]

or even just

@[simp] theorem rec.constant {α : Sort u} {β : Type v} (b : β) :
    (@PLift.rec α (fun _ => β) fun _ => b) = fun _ => b := rfl

[Kevin Buzzard]

Lean 4 seemed generally worse than lean 3 at guessing motives. I've been setting pp.all true in lean 3 and looking at the motive and then supplying it explicitly. I opened lean4#1841 about this and Leo fixed it yesterday. Does updating lean solve the problem here?

[Mario Carneiro]

I haven't tested the code but from reading the commit that fixed lean4#1841 I think we should expect elab_as_elim to act basically the same as it does in lean 3 now

[Mario Carneiro]

meaning that this issue should be fixed, assuming the relevant constants are in fact marked elab_as_elim