Tacticals

This category refers to tactics that modify the behavior of other tactics. Important phrasing note for this section: a tactical is only a tactical when it doesn’t have all of its arguments. A tactical with all of its arguments is a tactic. Tacticals are heavily utilized in automation because they broaden the capabilities of the tactic language significantly, making it much more expressive.

For an interesting perspective on automation - and good examples of building “one shot proofs” (proofs that only contain one tactic) - check out this post by Adam Chlipala.

try

The try tactical executes a provided tactic, catching any errors and always succeeding.

Syntax

(* Simple usage *)
try reflexivity.

Examples

Before

-------------------------
1/1
1 = 2

try reflexivity.

After

-------------------------
1/1
1 = 2

Resources

Reference Documentation

---

;

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.

---

Goal Selectors

Goal selectors are a category of tacticals that apply a tactic to a specific goal or goals.

There are a number of goal selectors:

• all: Applies the tactic to all goals in focus in series
• !: If only one goal is in focus, apply the tactic. If not, this tactic fails
• par: Applies the tactic to all goals in focus in parallel. The tactic provided must solve all goals or do nothing, otherwise this tactic fails
• n-m: Applies the tactic to goals with indices between n and m, inclusive

Syntax

all: simpl.

par: simpl; reflexivity; auto.

!: discriminate.

2-3: auto.

Examples

Before

-------------------------
1/2
True
-------------------------
2/2
True

all: exact I.
(* or *)
1-2: exact I.

After

Proof finished

Alternatively,

!: exact I.

Error: Expected a single focused goal but 2 goals are focused.

Resources

Reference Documentation

---

repeat

The repeat tactical repeatedly executes a tactic until it either fails or causes no change in the goal. If the tactic provided succeeds, it will be recursively applied to each generated subgoal.

Syntax

(* Simple usage *)
repeat split.

Examples

Before

P, Q, R, S: Prop
-------------------------
1/1
P /\ Q /\ R /\ S

repeat split.

After

P, Q, R, S: Prop
-------------------------
1/4
P
-------------------------
2/4
Q
-------------------------
3/4
R
-------------------------
4/4
S

Resources

Reference Documentation

---

||

The infix || tactical tries the first tactic and only tries the second if the first failed. In other words, || executes the first tactic that makes progress on the goal.

Syntax

(* Simple usage *)
reflexivity || assumption.

Examples

Before

P: Prop
H: P
-------------------------
1/1
P

reflexivity || assumption.

After

Proof finished

Resources

Reference Documentation

---

---