CODEWITHSUNDEEP
automationcoqproof
Zheng Cheng
Zheng Cheng

Reputation: 400

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.

Upvotes: 2

Views: 224

Answers (4)

Zimm i48
Zimm i48

Reputation: 3081

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

Upvotes: 3

Vilhelm Sjöberg
Vilhelm Sjöberg

Reputation: 503

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.

Upvotes: 4

Vinz
Vinz

Reputation: 6057

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

Upvotes: 4

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23622

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.

Upvotes: 5

Related Questions