;

The infix ; tactical is the sequencing tactical. It applies the right tactic to all of the goals generated by the left tactic.

The ; tactical is binary, so it takes two tactics (we will say A and B) as input. A is executed. If A does not fail and does not solve the goal, then B is executed for every goal that results from applying A. If A solves the goal, then B is never called and the entire tactic succeeds. This is useful when A generates lots of very simple subgoals (like preconditions of a theorem application) that can all be handled with another automation tactic.

The ; tactical is left-associative. Consider the tactic A; B; C. If A generates goals A1 and A2, then B will be applied to each. Let’s say that this results in a state with goals A1', A2', and B'. C will now be applied to each of these. This may not always be desired, and so parentheses can be used to force right-associativity. Consider the tactic A; (B; C). If A generates goals A1 and A2, then B; C will be applied to each. The difference may not be crystal-clear in an abstract example such as this one, so check out the script below. Keep in mind that the difference is in the resulting state tree from calling these tactics:

A; B; C
├── A1              /*  Call B  */
│   └── A1'         /*  Call C  */
│       └── A1''
└── A2              /*  Call B  */
    └── A2'         /*  Call C  */
        └── A2''

A;(B;C)             /*  Call A  */
├── A1              /* Call B;C */
│   └── A1''
└── A2              /* Call B;C */
    └── A2''

Also keep in mind that this behavior is extremely versatile, the above tree “shortening” use is only one example.

Compare this tactical with Prolog’s semicolon tactical and revel at some neat similarities! For example, in Coq, A;B will backtrack if B fails and A can succeed in a different way. The primary example of a tactic being able to succeed in multiple ways is the constructor tactic.

Syntax

(* Simple usage *)
split; reflexivity.

(* Left-associative chain *)
split; simpl; reflxivity.

(* Right-associative chain *)
split; (split; auto).

Examples

Before

P, Q: Prop
H: Q
-------------------------
1/1
P \/ Q

constructor; assumption.

After

Proof finished

Note the definition of or:

Inductive or (A B : Prop) : Prop :=
| or_introl : A -> A \/ B 
| or_intror : B -> A \/ B.

---