Merging duplicate goals

Stream: Is there code for X?

[David Loeffler]

Is there a goal-management tactic that can be used to recognise that two (or more) of the goals in the current goal list are identical, and merge them together, so you don't have to give two copies of the same sub-proof?

(I know about "all_goals", "any_goal" etc, which would allow you to only write the goal once; but it would still be getting processed multiple times. I want something which would halve the tactic compilation time, as well as the writing time.)

[Edward van de Meent]

I remember this being asked before, and then the answer was no, iirc

[Damiano Testa]

Are your goals "identical"? I.e. same local variables and same types?

[Damiano Testa]

(Internally, they will not be identical since, for instance, each metavariable has a new name, but I am wondering if they are identical for a human, at least.)

[David Loeffler]

The goals are literally identical up to naming of bound variables. (But they are quite lengthy to type, so I want to avoid have-ing them beforehand.)

[Damiano Testa]

Ok, I wonder if a tactic could create a new metavariable that is defeq to the current goal, use that to close all goals that it can and leave just the "new" metavariable as a remaining goal (plus whatever goals it was not able to solve automatically).

[Damiano Testa]

(I won't have time to actually think about this for a while, but it seems like a good metaprogramming task.)

[David Loeffler]

In lean 3 there was a hack resembling have foo := ?_; rotate that could push a goal whose type was an unconstrained meta variable, which you could use to close multiple proof branches; but that is not legal lean 4 syntax.

[David Loeffler]

Damiano Testa said:

Ok, I wonder if a tactic could create a new metavariable that is defeq to the current goal, use that to close all goals that it can and leave just the "new" metavariable as a remaining goal (plus whatever goals it was not able to solve automatically).

Possibly easier would be to take a list of goals as an argument - merge_goals 3 5 or something – rather than automating the search. I’m concerned about it taking a long time to fail on some goals that aren’t defeq.

[Junyan Xu]

Still possible in Lean 4, just make the type a metavariable too:

example : True := by
  have : ?_ := ?_
  · exact this
  · trivial