have'

Stream: lean4

[Patrick Massot]

Mario Carneiro said:

refine and have complain when they can't figure out metavariables instead of making them new goals (this is particularly harmful when figuring out a proof)

you can use refine' and have' , these are core tactics intended for the purpose

Could you elaborate on this? In Lean 3 I can type:

import analysis.inner_product_space.dual

example : true :=
begin
  have := inner_product_space.to_dual_symm_apply,
  all_goals { sorry }
end

while the Lean 4 version

import Mathlib.Analysis.InnerProductSpace.Dual

example : true := by
  have' := InnerProductSpace.toDual_symm_apply
  all_goals { sorry }

while the same with or without prime after have. The question is: can we get back Lean 3 behavior?

[Patrick Massot]

This example isn't great because there are no explicit arguments at all, but it still shows the difference between Lean 3 and Lean 4.

[Kevin Buzzard]

@Bhavik Mehta weren't you flagging this issue on Xena recently?

[Bhavik Mehta]

Yes - Patrick's example is precisely the sort of thing that was making my life difficult

[Yaël Dillies]

@Patrick Massot, yes: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/lean3.20support/near/388917291

[Yaël Dillies]

Again, the best way to get anything done is whining about it to Kyle :innocent:

[Patrick Massot]

I know, but I have this schizophrenia issue where I keep complaining everybody keeps distracting Kyle from working on our informal Lean project and then the next minute I distract him with a new metaprogramming request.

[Patrick Massot]

And my question is: why isn't this the default behavior of have?

[Kyle Miller]

I actually extracted :-( from the convert tactic, so abusing convert here's a have that creates new goals:

macro "refine_lift'' " e:term : tactic => `(tactic| focus (convert no_implicit_lambda% $e using 0; rotate_right))
macro "have'' " d:haveDecl : tactic => `(tactic| refine_lift'' have $d:haveDecl; ?_)

set_option trace.Elab.let true
example : true := by
  have'' := InnerProductSpace.toDual_symm_apply
  all_goals { sorry }

The reason why have/have' throw an error (I don't mean the rationale why, just why it happens) is that docs#Lean.Elab.Tactic.elabTermEnsuringType ends up elaborating a term in a way where stuck TC is an error, vs allowing stuck TC problems to turn into a metavariables.

[Alex Kontorovich]

I have similarly been struggling with this, constantly needing to put have := @whatever, and then specifying what I can with (G := G) etc, and putting underscores for the rest. When that's all done, and I get the theorem I want, I have to go back and remove the @ and underscores...