Signature of `False.rec`

Stream: lean4

[Siddhartha Gadgil]

I am confused about the signature of False.rec. It seems to suggest that the motive is explicit, but the following example (and others) suggest it is implicit. Which is correct?

example (h: False)(P: Prop): P := False.rec h
#check False.rec -- False.rec.{u} (motive : False → Sort u) (t : False) : motive t

[Adam Topaz]

docs#False.rec (I don’t know why I expected that to work.)

[François G. Dorais]

Use False.elim instead.

[François G. Dorais]

False.rec is automatically generated, motive is explicit because it can't be inferred from any later argument.

[Siddhartha Gadgil]

Thanks.

The issue is that while the signature claims the motive is explicit, function application does not want the motive as an argument. On the other hand, the pretty-printer does print the motive.

This means in particular, the pretty-printed code is not valid. An example:

theorem silly (h: False)(P: Prop): P := False.rec h
#print silly /- theorem silly : False → ∀ (P : Prop), P :=
fun h P => False.rec (fun x => P) h -/

[Siddhartha Gadgil]

I am asking because I am refactoring code generated by the pretty-printer, so trying to understand what is happening.

[Kyle Miller]

It seems to be because of the elabAsElim code, where the motive argument is solved for, even if it's explicit.

@[elab_as_elim]
def False.rec' : (motive : False → Sort u_1) → (t : False) → motive t := sorry
#check fun (t : False) => (False.rec' t : Bool) -- OK

If you remove the attribute, then the #check gives the expected error message.

[Kyle Miller]

Maybe docs#Lean.Meta.getElimExprInfo should check that the motive is an implicit argument? (and maybe False.rec should have its motive be implicit?)

[Siddhartha Gadgil]

Thanks @Kyle Miller
It does seem to me that the motive being implicit is natural. In my case I can work around this issue quite easily, but wanted to understand what is happening (rather than hack a workaround based on observations, which could then break).

[Kyle Miller]

Following up on this @Siddhartha Gadgil, you now have to write

example (h: False) (P: Prop): P := False.rec _ h

I don't remember which release it was, but elabAsElim routine now respects explicit arguments. Thanks for bringing this up!