Need of @ in False.rec

Stream: lean4

[Filippo A. E. Nuccio]

I cannot understand why is @needed when trying to produce something out of false:

def foo (h : False) : ℕ := @False.rec (fun _ ↦ ℕ) h --works

while

def bar (h : False) : ℕ := False.rec (fun _ ↦ ℕ) h -- throws the error
/-
application type mismatch
  False.rec ?m.29 fun x ↦ ℕ
argument
  fun x ↦ ℕ
has type
  ?m.31 → Type : Sort (max 2 ?u.30)
but is expected to have type
  False : Prop
-/

When I look at

#check False.rec -- False.rec.{u} (motive : False → Sort u) (t : False) : motive t

everything seems explicit, so I cannot see why False.rec and @False.rec behave differently. As a bonus I would like to understand if/how I could have guess this behaviour while looking at the file where False is defined in an apparently innocuous way.

While playing the same game with Nat.rec (that looks defined in the same way, to me), I get

#check Nat.rec -- Nat.rec.{u} {motive : ℕ → Sort u} (zero : motive Nat.zero) (succ : (n : ℕ) → motive n → motive n.succ) (t : ℕ) :  motive t

and here the motive is implicit.

Since I can of course fix the first example by doing

def bar (h : False) : ℕ := False.rec (motive := fun _ ↦ ℕ) h

and I understand that without explicitly mentioning the motive Lean cannot go very far, I guess that my question really is: why do I see explicit, rather than implicit, variables when checking False.rec?

[Adam Topaz]

there was a similar question recently... it has to do with how False.rec is elaborated as an eliminator.

[Adam Topaz]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Signature.20of.20.60False.2Erec.60/near/441354391

[Kyle Miller]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Signature.20of.20.60False.2Erec.60/near/441354391

[Filippo A. E. Nuccio]

OK, thanks: I see that @Siddhartha Gadgil had the very same question indeed. But unfortunately I do not really understand the answers:

• "The motive cannot be inferred later" means that in the construction of Blob.rec, where Blob is any inductive type, Lean is able to understand if the way constructors are entangled with one another would allow to infer the type of the motive? For instance, in Nat.rec providing motive n in the second explicit variable (as second argument of succ) is enough? If so.. WOW!
• @Kyle Miller , can you be a bit more explicit about the "ElabAsElim code" explanation? I do not understand why it "explains" what is going on; the only thing I figure out is that False.rec' behaves more normally, is that right?

[Kyle Miller]

The situation is too confusing, so I've created an issue: lean4#4347

[Filippo A. E. Nuccio]

Wow, thanks! Let's wait and see :smiley:

[Kyle Miller]

That 'explanation' involving ElabAsElim isn't really intelligible to anyone who isn't acquainted with Lean 4 internals, sorry.

Here's another attempt: eliminators need special help during elaboration since their return type is the application of an unknown function. Somehow, given the expected type, False.rec needs to figure out what motive is. This is a "higher-order unification problem": unification needs to solve for a function rather than just a plain non-function value, and higher-order unification is undecidable, so Lean doesn't even try in most cases. So, special code kicks in for eliminators that identifies which argument needs to be solved for using higher-order unification (motive in this case) and then it completely takes over for that particular argument. It doesn't care whether or not that argument is explicit, and it will never look at positional arguments. I imagine this is an oversight.

There are two ways to turn off this special feature. The first is explicit application (@False.rec (fun _ ↦ ℕ) h as you observed). Another is to use a keyword argument for the motive (False.rec (motive := fun _ ↦ ℕ) h).

[Kyle Miller]

You can also turn it on for your own declarations by adding the @[elab_as_elim] attribute to them.

[Filippo A. E. Nuccio]

OK, thanks. I think I had a blurry picture in mind of what you describe much more neatly, so this really helps. I will try to play around with this attribute to see if I understand a bit better what is happening under the rug.

[Kevin Buzzard]

My impression with many of these higher order unification questions is that asker says "this higher order unification question is easy to solve and so why doesn't Lean's algorithm solve it" and the generic answer is "there will always be examples that any algorithm can't solve because the problem is undecidable". I think that what's surprising is that exanples of failure are so easy to come by, but there was an example in TPIL3 of a very simple problem which had four obvious solutions each one of which was right in one situation and wrong in the other three, and this was what made the penny drop that somehow the question is completely hopeless.