merging goals tactic

Stream: lean4

[Jakob von Raumer]

I'm considering writing a tactic that basically checks if the current goal list contains duplicates and "merges" them into a single mVar. Does anyone know if such a tactic exists in lean3 (or coq for that matter)?

[Mario Carneiro]

no, but it's a pretty easy tactic to write

[Jakob von Raumer]

My concern was more how to name it. The "hardest" part might be to compare the contexts...

[Marcus Rossel]

Unfortunately dedup is already a different tactic in Lean 3. So maybe collapse?

[Mario Carneiro]

I was thinking dedup_goals

[Mario Carneiro]

It's true that merging contexts complicates matters. What do you want to do about incompatible contexts? You could take the intersection of the contexts, but that could lose a lot of assumptions

[Eric Wieser]

I guess you could combine all the assumptions not present in all goals into a single assumption in the form of a pprod of psigmas?

[Jakob von Raumer]

I'd actually conservatively only merge those goals where contexts match up to reordering&defeq