Apply to mvarid

Stream: lean4

[Moritz Doll]

What is the canonical way to apply a specific lemma to a metavariable? In mathlib4 I found

mvarId.apply (mkConst ``foo [])
mvarId.apply (← mkConstWithFreshMVarLevels ``foo)
mvarId.apply (← mkConst ``foo)
mvarId.apply (← `(foo))

Is there one good way or are several of these sensible in different situations (what are these situations?)

[Moritz Doll]

Are (1), (3) and (4) all just the same?

[Kyle Miller]

1 and 3 are not good since they don't set the universe levels (unless foo doesn't have universe level parameters, in which case they're fine)

[Kyle Miller]

Where did you see 4? I'm surprised that that would work since quotations create Syntax, not Exprs. (Were you looking at a use of evalApplyLikeTactic in test/runCmd.lean?)

[Kyle Miller]

Examples:

• propext doesn't have universe levels, so mvarId.apply (mkConst ``propext []) or mvarId.apply (mkConst ``propext) is fine
• pi_congr does, so you need mvarId.apply (← mkConstWithFreshMVarLevels ``pi_congr)
• if you know the levels already, you can do mvarId.apply (mkConst ``foo [u,v]) and set them manually

[Moritz Doll]

Thanks Kyle! Yes, it was in test/runCmd.lean, I was just searching for mvarid.apply

[Moritz Doll]

Is there a case where (2) is wrong when setting the universe levels by hand is the correct solution?

[Kyle Miller]

For mvarId.apply, it's probably never wrong to use (2). Manual universe variables are just a hint (I'd believe there are cases where you need to set them for apply to succeed, but I'm not sure that's in the realm of wrong behavior, just non-ideal).

[Thomas Murrills]

Maybe it'd be worth having .applyConst n somewhere (which would just be.apply (← mkConstWithFreshMVarLevels n)) to help avoid gotchas/ambiguity for future metaprogrammers?

[Moritz Doll]

I can put a version of that into mathlib when PRing congrm.