Home

Github

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 utilize tacticals to contain only one proof step) - 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

n: nat
=========================
1/1
n + 0 = n
try reflexivity.

After

n: nat
=========================
1/1
n + 0 = n

Alternatively,

try apply add_0_r.
No more goals.

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 operator 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

No more goals.

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:

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

No more goals.

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.

Be careful: if the input tactic never fails, repeat will cause an infinite loop! For example, repeat symmetry or repeat idtac will always result in an infinite loop.

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

No more goals.

Resources

Reference Documentation

now

now tactic is simply notation for tactic; easy.

Syntax

now split.

Examples

Before

=========================
1/1
True /\ 42 = 14 * 3
now split.

After

No more goals.

Resources

Reference Documentation

do

The do tactical accepts a tactic t and a natural number n, applying t to the goal n times. do fails if one of the applications of t fails before n applications have occurred.

In my opinion, do is a difficult tactic to justify. I find myself using it when using repeat tends to be overzealous. For example, if I have a goal with 100 subterms, and I’d like to apply a tactic t only to 30 of the subterms (assuming t works on individual subterms and not the whole goal), I’m more likely to use do 30 t than repeat t to prevent the remaining 70 subterms from being affected.

Syntax

do 3 (split; [reflexivity | idtac]).

Examples

Before

=========================
1/1
1 = 1 /\ 2 = 2 /\ 3 = 3 /\ 4 = 4
do 3 (split; [reflexivity | idtac]).

After

No more goals.

Resources

Reference Documentation