Proof automation

Question

Assuming having a list of sub-goals by applying tactic T:

______________________________________(1/10)
A
______________________________________(2/10)
A'
______________________________________(3/10)
A''

And assuming we know that Lemma L can be used to prove A and A'' but not A'.

My question is can we sequencing T with application result of L, which left me with just one sub-goal A'?

I tried T; apply L. without success, since sequencing seems require all branches/sub-goals proved.

I also tried controlled automation by using by T; apply L. from SSReflect, which suggested by this post. Unfortunately, Coq also get stuck, and report Ltac calls to ... last call failed.

Answer (Arthur Azevedo De Amorim)

You can use the try tactical, like this:

T; try by apply L.

This does the following. First, it applies T. Then, on each sub goal, it applies the tactic by apply L. If the tactic succeeds, good. Otherwise, if it fails, try does nothing.

Answer (Vinz)

I would recommend the T; try by apply L. from Arthur. But if you need more control, you can use

T; [ (* first goal *) now apply L
   | (* second goal *) now apply L
   | (* last goal *) idtac ].

Answer (Vilhelm Sjöberg)

Coq 8.6 also has goal selectors, so if T creates 4 subgoals you can write

T. 1-2,4: apply L.

to do apply L in all but the third subgoal.

Answer (Zimm i48)

As mentioned by Vilhelm, Coq 8.6 has goal selectors.

You can also do T; only 1,3: apply L. which has the advantage of numbering only the subgoals that were generated by the tactic T.

See https://coq.inria.fr/refman/proof-engine/ltac.html#goal-selectors