apply doesn't like `fun x => _`

Stream: mathlib4

[Johan Commelin]

Is this expected/known behaviour?

def foo : Nat → Nat → Nat → Nat := by
  apply fun x y ↦ _
  /-
  Where are my `x` and `y`?
  -------------------------
  Goal state:
  ```
  case y
  ⊢ ?m.153 ?x
  case x
  ⊢ ?m.145
  ⊢ Sort ?u.144
  ⊢ ?m.145 → Sort ?u.147
  ⊢ (x : ?m.145) → ?m.153 x → Nat → Nat → Nat → Nat
  ```
  -/

[Johan Commelin]

This is one hiccup in the output of mathport.

[Mario Carneiro]

this is known behavior

[Mario Carneiro]

it seems that lean 4 generalizes metavariables / forgets what was introduced and what wasn't, esp. when using _

[Johan Commelin]

(And using ?_ doesn't help either.)

[Johan Commelin]

Is it considered a bug or a feature?

[Mario Carneiro]

it works for me with ?_

[Mario Carneiro]

I think it is a bug

[Johan Commelin]

Ooh, right! I do get an x and y. But Lean has no clue at all about the types.

[Johan Commelin]

case y
⊢ ?m.19 ?x
case x
⊢ ?m.11
⊢ Sort ?u.10
⊢ ?m.11 → Sort ?u.13
x: ?m.11
y: ?m.19 x
⊢ Nat → Nat → Nat → Nat

[Mario Carneiro]

but it could be the consequence of some hard to change design things

[Mario Carneiro]

yeah that is expected, it did refine (fun x y ↦ ?_) _ _ because why not

[Johan Commelin]

apply should become an agda-style macro that replaces itself with refine and a suitable extra number of underscores.

[Mario Carneiro]

it did exactly that

[Mario Carneiro]

2 is suitable too

[Johan Commelin]

No, I mean an editor-level macro.

[Mario Carneiro]

aha

[Johan Commelin]

We should ban apply from checked-in source code.

[Mario Carneiro]

show_term could be a code action for any tactic

[Johan Commelin]

also that

[Mario Carneiro]

there are more occurrences of apply than refine in mathlib4

[Mario Carneiro]

If you found this in mathlib btw this is a weird way to spell intros x y

[Siddhartha Gadgil]

As an unskilled tactic user, let me say apply is far easier for me to understand. Also it is one step away from a declarative proof, essentially := my_theorem _ with unification.

[Johan Commelin]

It was highly minimized

[Johan Commelin]

@Siddhartha Gadgil refine is what you say. apply does more magic.

[Johan Commelin]

@Mario Carneiro The actual use case was more like

apply my_lemma x y z (fun a b => _) h1 h2

[Mario Carneiro]

ok so using ?_ should do what you want there

[Mario Carneiro]

mathport isn't good at inserting ?_ which is why it uses refine'

[Johan Commelin]

Maybe unless you need an unknown extra number of ?_ at the end of the apply call as well?

[Johan Commelin]

Because otherwise it might still mess up the goal state, like in the MWE

[Mario Carneiro]

is that a response to me or siddhartha?

[Johan Commelin]

To you

[Johan Commelin]

Mario Carneiro said:

yeah that is expected, it did refine (fun x y ↦ ?_) _ _ because why not

You might be bitten by a variant of this, unexpectedly, I guess

[Johan Commelin]

Where "You" means "me" and not you

[Mario Carneiro]

I won't be bit by it because I never use apply except as a golfed version of refine

[Johan Commelin]

"Lean does not unexpectedly bite Mario. Mario unexpectedly bites Lean."

[Mario Carneiro]

Does lean 3 really not introduce _ in the apply fun x y ↦ _ example?

[Mario Carneiro]

maybe this is an unintended consequence of the apply bug

[Mario Carneiro]

it seems like weird enough code that I think it shouldn't occur in the wild

[Reid Barton]

Maybe this makes more sense in context but apply (fun x y => _) seems like really weird style unless you intended what Lean 4 does

[Reid Barton]

Did whoever wrote that mean refine instead of apply and just forget?

[Johan Commelin]

probably

[Johan Commelin]

I think there are plenty of examples in mathlib where apply is used, even if refine makes more sense in both a technical and semantical sense.

[Mario Carneiro]

that wouldn't be hard to lint

[Mario Carneiro]

"used apply where exact/refine would work"

[Mario Carneiro]

for the case where zero _ are inserted

[Johan Commelin]

I guess in 99% of the cases, that would also be a semantic improvement?

[Mario Carneiro]

it could cause an elaboration change, usually for the better

[Mario Carneiro]

I wish we had something like rust clippy though for these kind of borderline pedantic lints

[Ruben Van de Velde]

I vaguely recall that there were cases in mathlib 3 where apply was a significant speedup over exact or term mode proofs

[Mario Carneiro]

we also have exact (e :) for when we want to actively forget about the expected type when elaborating e, which roughly corresponds to what apply e does in the 0-_ case

[Yaël Dillies]

Mario Carneiro said:

it could cause an elaboration change, usually for the better

I recently had a case where I needed the apply elaboration order (due to Lean trying to pick up a typeclass assumption throguh TC inference rather than unification), hence I introduced a "no _ inserted"-apply call.

[Mario Carneiro]

yep that's what (e :) is for

[Mario Carneiro]

I think it is more explicit that you are doing funny business

[Yaël Dillies]

I didn't even know that was correct syntax. I thought you had to do exact (e : _)

[Mario Carneiro]

that's the lean 3 syntax

[Yaël Dillies]

Mario Carneiro said:

I think it is more explicit that you are doing funny business

In that case I left a note in the proof anyway

[Mario Carneiro]

it doesn't have the desired effect in lean 4 so (e :) is the replacement

[Yaël Dillies]

Oh okay!

[Mario Carneiro]

Yaël Dillies said:

Mario Carneiro said:

it could cause an elaboration change, usually for the better

I recently had a case where I needed the apply elaboration order (due to Lean trying to pick up a typeclass assumption throguh TC inference rather than unification), hence I introduced a "no _ inserted"-apply call.

(although I think that trick won't work in lean 4 anyway, since it doesn't like to get typeclasses by unification)