Consolidating duplicate goals

Stream: metaprogramming / tactics

[Brendan Seamas Murphy]

If I end up with two goals left, where both the hypotheses and the target are exactly the same, is there a tactic which consolidates them down to a single goal? Sometimes rw causes this scenario

[Damiano Testa]

Does using all_goals suffice for your use case?

[Brendan Seamas Murphy]

In my current situation yes, but in the general case no, since rw can produce multiple sets of duplicates

[Brendan Seamas Murphy]

You can use any_goals or all_goals try or something, but I think it would be nicer to not do that

[Damiano Testa]

any_goals?

[Damiano Testa]

I don't think that there is a systematic way of doing this, but there have been discussions of "delay" tactics.

[Adam Topaz]

It's not so trivial to consolidate goals in this way since the metavariables (and often the local contexts) are different even if the type of the goal is the same.

[Jovan Gerbscheid]

There is definitely room for improvement in the handling of goals in rw. It simply collects all metavariables in the expression and turns them into new goals, without checking whether a metavariable may already be a goal,

[Damiano Testa]

There was a previous thread that might be relevant.