3
$\begingroup$

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?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
6
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ Yes, this is exactly what I am looking for! Thank you so much :) $\endgroup$
    – Hiroki Chen
    Commented Apr 6 at 1:49
1
$\begingroup$

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

Improve this answer
$\endgroup$
3
  • $\begingroup$ Although I avoid using ssreflect in my project, thanks for pointing this out! $\endgroup$
    – Hiroki Chen
    Commented Apr 6 at 1:53
  • 2
    $\begingroup$ There is a non-ssreflect equivalent: now <tactic> $\endgroup$
    – djao
    Commented Apr 6 at 4:00
  • 2
    $\begingroup$ by and now are also doing some automation to try and close the goal. $\endgroup$
    – Théo Winterhalter
    Commented Apr 6 at 8:48

Not the answer you're looking for? Browse other questions tagged or ask your own question.