Search code examples
automationcoqproof

Proof automation

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.

Solution

  • 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.