The Coq mailing list

[Saint Wesonga <saintwesonga AT gmail.com>]

Sorry, I should have been clearer - I ended up with all those goals after using "inversion; try whatever." The remaining ones can still be dispatched by repeated applying the same tactic. I have just found that what I needed was "inversion; try whatever || congruence." Thanks guys!

On Wed, Apr 25, 2012 at 11:48 AM, Stefan Ciobaca <stefan.ciobaca AT gmail.com> wrote:

Hello,

Try to add "; congruence" to the tactic which generates your 50 subgoals.

E.g. if the 50 subgoals as generated by "induction x", you should do

"induction x; congruence."

The ";" is a tactical which calls the second tactic on all goals
generated by the first tactic.

You might also want to do "induction x; try congruence." to manually
handle subcases which can't be solved by congruence.

Cheers,
Stefan

On Wed, Apr 25, 2012 at 8:34 PM, Saint Wesonga <saintwesonga AT gmail.com> wrote:
> Hello All,
>
> I have a proof with 50 subgoals. Most of them can be dispatched with the
> "congruence" tactic, but I don't want to have 50 separate congruence
> commands. I have tried using "do" and "repeat" but those only seem to solve
> 1 goal. Is there a better way to do this?
>
> Saint.