What is the most ergonomic way to eliminate multiple similar goals in Coq?

Question

I recently bumped into some theorems that can be proved easily but not very elegantly. It is not elegant because when I was doing case analysis, Coq discharged many goals, but most of them can be solved with a simple combination of tactics while each group of sub-goals requires a different one.

For example, now we have nine goals numbered from 1-9 where I solve 1, 4, 7 with foo, 2, 5, 8 with bar, and 3, 6, 9 with baz, how do we eliminate these 9 goals?

Using ; won't work very well for me because if the tactic is applied to each goal there is no way to "reverse" the applied tactics if other tactics may succeed. In other words, when foo fails, the goal has been changed and the context is lost so we cannot just append bar behind foo.

I am seeking some kind of || thing that tries several options of tactics provided by the user and see if any of the tactics succeed, but "||" works somehow differently: it tries another tactic only if the current one fails while there might be cases where the proof neither succeeds nor fails.

Coq also has a syntax like 1-10: do something. that applies the tactic do somthing to goal numbered 1 to 10 but this requires users to know in advance what each goal looks like. It may thus not be very useful if there are multiple (different) goals generated by the case analysis.

Is there a clever Ltac thing for doing this?

Answer 1

Perhaps you are looking for the solve tactic. It will apply the first tactic that works for each subgoal.

I would do something along the following lines:

tac. all: try solve [ foo | bar | baz ].

Instead of using semicolon, I use the all goal selector to let me see what goals have been generated before applying my tactics.

Answer 2

The ssreflect by terminating tactical will fail if the provided tactic doesn't completely solve the goal.