instance arguments in eqn compiler

Stream: new members

[Horatiu Cheval]

The following doesn't work, and instead of prime p I need to use @prime p _. Is it the case that the equation compiler doesn't know how to deal with instance arguments, or why is this happening?

inductive formula
| prime (p : Prop) [decidable p] : formula

open formula

def interpret : formula → Prop
| (prime p) := sorry
/-
infer type failed, unknown variable
  __mlocal__fresh_115_16
-/

[Eric Wieser]

Does it work if you add an _ after p?

[Horatiu Cheval]

prime p _ does not, I get function expected at ... so the argument is indeed implicit.
@prime p _ does. What I don't understand is why lean manages to fill in the argument when given as an explicit _ and not when left implicit.

[Damiano Testa]

I cannot answer your question, but my approach is the following.

Finding arguments is an art and its automation uses several heuristics, depending on previous assumptions. Normally, these heuristics work very well and you need not worry about them. In some cases, you shake the system a bit to change the starting point of the heuristics and then you have chances to extend the magic working in a place where they did not work before.

From this point of view, tricks like

• use apply instead of refine
• use @
• use (_ : _)
• use by exact or by convert or by apply

may appear to be useless, but can be really a game changer when wanting lean to prove something that it should!

[Horatiu Cheval]

Hm, I get your point, thanks for offering your insights. I guess my confusion is due to the fact that in my naive mental model, with an f of signature def f {x : α} (y : α) : α, f y works like an abbreviation for @f _ y. But as you point out, this is an oversimplification that doesn't always work, and this probably becomes apparent in my example.

[Kevin Buzzard]

I guess what's happening is that the Lean 3 equation compiler has not been designed with type class inference in mind.

inductive formula
| prime (p : Prop) [Decidable p] : formula

open formula

def interpret : formula → Prop
| (prime p) => sorry

works in Lean 4

[Horatiu Cheval]

I see, good to know it will work with Lean4

[Floris van Doorn]

I think this is just a bug in the equation compiler, it's uncommon for the last argument of a constructor to be implicit, so it probably hasn't ever come up before.

[Eric Wieser]

Presumably this is also broken for {} instead of []?

[Horatiu Cheval]

I couldn't think of a natural example where you would have an {} at the end, but just modifying the above, it actually works for {}.

inductive formula
| prime (p : Prop) {h : decidable p} : formula

open formula

def interpret : formula → Prop
| (prime p) := sorry

def φ := @prime (0 = 0) (by apply_instance)