Coq Tactics in Plain English

If you’re like me, one of the biggest shortcomings of the Coq ecosystem is the fairly complicated tactic reference documentation. It is exhaustive (which is better than lacking), but I have a few specific issues with it:

Entries are too verbose. I usually don’t need an exhaustive explanation of what a tactic does.
BNF grammar is not that easy to read. This one might be more controversial, but I would rather have examples of syntax.
There are not enough examples of tactics being used, and the examples that do exist are too often not representative of what a beginner might see.

For these reasons, I’ve decided to compile a reference document of every tactic that I’ve ever used, addressing the problems above via the following solutions.

Entries will be written at an undergraduate level, assuming a basic understanding of the Coq system. Sometimes, this will require reading the pages for other tactics before the one you really want to know about, but I think that’s a fair compromise. Explanations will focus on what configurations of goal states the tactic is useful or not useful for.
Entries will start general and become more specific as one reads on. This will ensure minimal maintenance is necessary as tactics change over time.
Entries will include syntax examples rather than BNF grammars.
Entries will contain multiple examples, including goal states before and after executing the tactics. Small MRE Coq scripts may be included.
As a fallback, links to other resources, at minimum the official documentation, will be included in each entry.

This guide doesn’t aim to replace the reference documentation, it aims to be a stepping stone into the reference documentation that reduces the apprehension of those new to Coq.

There are many other guides to Coq tactics, you should check them out too if I don’t have what you need:

Generalization
Simplification
Specific Solvers
Rewriting
Case Analysis
Automation
Tacticals

Generalization

This group of tactics is often found at the beginnings of proofs. Generalization and its counterpart Specialization (both are included here) are concepts used to fine-tune how strong of a theorem is needed to continue. Theorems that are too strong (specific) aren’t useful for many different kinds of goals. Theorems that are too weak (general) are frequently unprovable (even if their specified counterparts are!) and those that are provable are frequently harder to prove!

intros

Typically the first tactic a Coq user ever utilizes. intros looks for assumptions in your goal and moves them to the goal’s assumption space.

More specifically, intros specializes a goal by looking for type inhabitation and proposition assumptions and moving them into the assumption space. For example, if you write forall (n : nat), n + 0 = n, the forall is acting as an assumption that there is a value of type nat that we can call n. Calling intros here will provide you an assumption n that there is a value of type nat.

intros will not introduce variables that are contained in opaque/wrapped definitions.

A simpler tactic, intro, acts similarly but can only introduce one assumption, and will introduce variables contained in opaque/wrapped definitions.

Syntax

(* Simple usage - introduces all named assumptions *)
intros.

(* Give specific names to assumptions as you introduce *)
intros n m x.

(* Split a conjunction or existential assumption upon introducing *)
intros [A B].

Examples

Before

-------------------------
forall (n : nat), n + 0 = n

intros x.

After

x: nat
-------------------------
1/1
x + 0 = x

Before

-------------------------
forall (A B C : Prop), A /\ B -> C -> A /\ C

intros A B C [ATrue BTrue].

After

A, B, C: Prop
ATrue: A
BTrue: B
-------------------------
1/1
C -> A /\ C

Before (assume P := forall (n : nat), n = n)

-------------------------
1/1
P

intros.

After

-------------------------
1/1
P

Alternatively,

intro.

After

n: nat
-------------------------
1/1
n = n

Resources

Reference Documentation

clear

clear erases assumptions from the assumption space. Multiple assumptions may be erased in one tactic via a space-separated list of assumptions. clear will fail if an assumption passed into it contains as subterms other variables that still exist in the goal state.

Syntax

(* Simple usage *)
clear H.

(* Clear multiple assumptions *)
clear H Heq X Y n.

Examples

Before

n: nat
H, Hr1, Hr2: n = 0
IHn: n = 1
-------------------------
1/1
False

clear Hr1 Hr2.

After

n: nat
H: n = 0
IHn: n = 1
-------------------------
1/1
False

Resources

Reference Documentation

Simplification

This group of tactic aims to reduce the complexity of terms in a goal. They will not solve a goal, only convert it into what is a structurally smaller (although maybe not lexically smaller!) form of the original goal.

simpl

simpl evaluates terms that are constructed of constant values - not variables. simpl can also partially evaluate partially-constant values.

Syntax

(* Simplify the goal as much as possible *)
simpl.

(* Simplify a hypothesis *)
simpl in H.

(* Simplify in the entire proof state *)
simpl in *.

(* Only simplify a specific term in a specific hypothesis *)
simpl (2 + 2) in H.

Examples

Before

-------------------------
1/1
2 + 2 = 1 + 3

simpl (2 + 2).

After

-------------------------
1/1
4 = 1 + 3

Resources

Reference Documentation

unfold

unfold replaces definition identifiers with the definition’s contents, simplifying along the way.

Syntax

(* Simple example *)
unfold plus.

(* Unfolding a definition in a hypothesis *)
unfold X in H.

(* Unfolding a definition in all hypotheses and the goal *)
unfold X in *.

Examples

Given

Fixpoint bitlist (n : nat) : list bool :=
    match n with
    | O =>    true  :: nil
    | S n' => false :: (bitlist n')
    end.

Before

n: nat
l: list bool
H: bitlist (S (S n)) = false :: false :: l
-------------------------
1/1
bitlist (S n) = false :: l

unfold bitlist in *.

After

n: nat
l: list bool
H: false
     :: false
        :: (fix bitlist (n : nat) : list bool :=
              match n with
              | 0 => true :: nil
              | S n' => false :: bitlist n'
              end) n =
    false :: false :: l
-------------------------
1/1
false
 :: (fix bitlist (n0 : nat) : list bool :=
       match n0 with
       | 0 => true :: nil
       | S n' => false :: bitlist n'
       end) n = false :: l

Resources

Reference Documentation

Specific Solvers

Each tactic in this group exists to solve a very specific kind of goal. They’re fairly simple to learn about and use, because their goal targets are such small groups that there are hardly any degrees of freedom for automation to be required. Essentially all Coq proofs include some of these (whether they’re written by the programmer or called by more complex tactics).

reflexivity

reflexivity solves goals which state that a term is equal to itself. reflexivity has some simplification power, but not as much as simpl. This tactic will fail if it cannot solve the goal.

reflexivity makes an attempt to simplify the goal and then apply eq_refl, where eq_refl is the sole constructor of the eq Inductive Proposition, stating that forall {A : Type} (a : A), eq a a.

Syntax

(* Simple usage *)
reflexivity.

Examples

Before

n: nat
-------------------------
1/1
n = n

reflexivity.

After

Proof finished

Resources

Reference Documentation

assumption

assumption solves goals in which there exists an assumption that directly proves the goal (no simplification). This tactic will fail if there does not exist such an assumption.

Syntax

(* Simple usage *)
assumption.

Examples

Before

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

assumption

After

Proof finished

Resources

Reference Documentation

discriminate

discriminate solves goals that are trivial inequalities (something of the form x <> y). This tactic will fail if the goal is not an inequality or is non-trivial.

Syntax

(* Simple usage *)
discriminate.

Examples

Before

-------------------------
1/1
1 <> 2

discriminate.

After

Proof finished

Before

-------------------------
1/1
"hello" <> "world"

discriminate.

After

Proof finished

Resources

Reference Documentation

exact

exact allows users to solve goals by providing a proof object directly. This tactic will fail if the provided proof object does not prove the goal.

Syntax

(* Simple usage *)
exact I.

Examples

Before

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

exact I.

After

Proof finished

Before

n: nat
-------------------------
1/1
n + 5 = n + 5

exact (eq_refl (n + 5)).

After

Proof finished

Resources

Reference Documentation

contradiction

contradiction solves goals in which there exist contradictory hypotheses. These contradictions generally take the form of a False hypothesis or a pair of hypotheses that state P and ~ P for some proposition. This tactic will fail if no such contradictions exist.

Syntax

(* Simple usage *)
contradiction.

Examples

Before

H: False
-------------------------
1/1
False

contradiction.

After

Proof finished

Before

x, y: nat
H: x = y
H0: x <> y
-------------------------
1/1
x = x + y

contradiction.

After

Proof finished

Resources

Reference Documentation

Rewriting

This group of tactics is very frequently used in the middles of proofs. Rewriting in all of its forms is an efficient way to bring together previously-independent parts of a goal.

rewrite

rewrite takes an equivalence proof as input, like t1 = t2, and replaces all occurances of t1 with t2. Replacement of t2 with t1 can be achieved with the variant rewrite <- (rewrite backwards). Multiple rewrites can be chained with one tactic via a list of comma-separated equivalence proofs. Each of the equivalence proofs in the chain may be rewritten backwards. rewrite will fail if there are no t1’s (in this example) to replace.

Syntax

(* Replace t1 with t2 in the goal *)
rewrite t1_eq_t2.

(* Rewrite in an assumption *)
rewrite Eq in H.

(* Rewrite in the goal and all assumptions *)
rewrite HEq in *.

(* Rewrite multiple values *)
rewrite t1_eq_t2, <- x_eq_y, ht_eq_ht.

Examples

Before

x, y: nat
H: x = y
-------------------------
x + y = y + y

rewrite H.

After

x, y: nat
H: x = y
-------------------------
y + y = y + y

Alternatively,

rewrite <- H.

x, y: nat
H: x = y
-------------------------
x + x = x + x

Resources

Reference Documentation

rename

rename changes the name of an introduced variable or assumption.

Syntax

(* Simple example *)
rename x into y.

Examples

Before

n: nat
-------------------------
1/1
n = n

rename n into x.

After

x: nat
-------------------------
1/1
x = x

Resources

Reference Documentation

remember

remember gives a name to complex terms. Specifically, remember t (where t has type T) introduces an assumption that there exists a member of type T, gives it a name such as t0, and provides another assumption that t = t0.

Syntax

(* Simple usage *)
remember (5 + x).

(* Provide a name for the remembered term *)
remember ("hello world") as s.

Examples

Before

x, y: nat
H: x + y = x
-------------------------
1/1
y = 0

remember (x + y) as sum.

After

x, y, sum: nat
Heqsum: sum = x + y
H: sum = x
-------------------------
1/1
y = 0

Resources

Reference Documentation

Case Analysis

Case analysis is a core aspect of constructivist logic. Although for many kinds of problems it is a low-level tool, it is ubiquitous among the foundations of all problems formalized in the Coq system. The core idea is: “if I want to prove a property P holds for a term t, I can do so by writing multiple sub-proofs stating that for each form that t can have, P holds.”

destruct

destruct allows for case analysis on inductive terms or assumptions. It can be used to split assumptions with conjunctions and disjunctions, as well as existential assumptions. The arguments of destruct are patterns.

Syntax

(* Simple usage *)
destruct H.

(* Destruct a term and introduce a hypothesis E showing its equivalence to the form it took *)
destruct n eqn:E.

(* Providing names for newly-introduced terms *)
destruct H as [H0 [H1 H2]].

(* Providing only some names for newly-introduced terms *)
destruct H as [H0 [? H1]].

(* Destructing multiple terms/hypotheses *)
destruct x as [| x0 x1], H as [[H1 H0] H2].

(* Providing names for newly-introduced terms in different generated subgoals *)
destruct H as [H1 | H2].

Examples

Before

n: nat
-------------------------
n = 0 \/ 1 <= n

destruct n as [| n'] eqn:E.

After (first goal generated)

n: nat
E: n = 0
-------------------------
1/2
0 = 0 \/ 1 <= 0

After (second goal generated)

n, n': nat
E: n = S n'
-------------------------
1/1
S n' = 0 \/ 1 <= S n'

Script

Theorem destruct_example1 : forall n : nat,
    n = 0 \/ 1 <= n.
Proof.
    intros. destruct n as [| n'] eqn:E.
    - left. reflexivity.
    - right. apply le_n_S, le_0_n.
Qed.

Script

Theorem destruct_example2 : forall (P Q R : Prop),
    ((P /\ Q) /\ R) -> P /\ (Q /\ R).
Proof.
    intros P Q R H.
    destruct H as [[PTrue QTrue] RTrue]. split.
    - apply PTrue.
    - split. 
        -- apply QTrue.
        -- apply RTrue.
Qed.

Script

Theorem destruct_example3 : 
    forall (P Q R : Prop),
    (P \/ Q) -> P \/ Q \/ R.
Proof.
    intros. destruct H as [PTrue | QTrue].
    - left. assumption.
    - right. left. assumption.
Qed.

Resources

Reference Documentation

inversion

inversion looks at a given piece of structural evidence and draws conclusions from it. If there are multiple sets of conclusions, inversion will generate a new proof obligation for each one. Informally, inversion is doing a more specific form of the case analysis provided by destruct - where destruct essentially says “I don’t know what this term is, so I’ll prove a property for all of the possible forms of it,” inversion says “I know exactly what terms could construct this hypothesis because of its definition, so I’ll only prove a property for those terms.”

This tactic often generates many trivial equality assumptions that may clutter the assumption space. I recommend almost always following inversion with subst to immediately substitute away these equalities.

Syntax

(* Standard usage *)
inversion H.

Examples

Before

n: nat
H: n <= 1
-------------------------
1/1
n = 0 \/ n = 1

inversion H.

After (first goal generated)

n: nat
H: n <= 1
H0: n = 1
-------------------------
1/2
1 = 0 \/ 1 = 1

After (second goal generated)

n: nat
H: n <= 1
m: nat
H1: n <= 0
H0: m = 0
-------------------------
1/1
n = 0 \/ n = 1

Script

Theorem inversion_example1 : 
    forall n, n <= 1 -> n = 0 \/ n = 1.
Proof.
    intros. inversion H. 
    - right. reflexivity.
    - inversion H1. left. reflexivity.
Qed.

Script

Inductive color : Type :=
| Red | Blue | Green | Cyan | Magenta | Yellow.

Inductive makes_white : color -> color -> color -> Prop :=
| RBG : makes_white Red Blue Green
| CMY : makes_white Cyan Magenta Yellow.

Theorem inversion_example2 : 
    forall (c1 c2 c3 : color),
    makes_white c1 c2 c3 ->
    (c1 = Red /\ c2 = Blue /\ c3 = Green) \/
    (c1 = Cyan /\ c2 = Magenta /\ c3 = Yellow).
Proof.
    intros c1 c2 c3 Hmw. inversion Hmw. 
    - left. repeat split.
    - right. repeat split.
Qed.

Resources

Reference Documentation

induction

induction is an extension of destruct that allows for case analysis on inductive terms, gaining an inductive hypothesis for each recursive subterm generated by the term destruction. The arguments of induction are patterns.

If the goal still contains named impliciations, induction can be used before introducing them with intros. In this case, if the argument to induction is not the first impliciation in the chain, all implications before it will be introduced to the goal’s assumption space.

induction can act similarly to inversion under specific circumstances. If you induct over an object that already contains subterms, you can remember the subterm(s) and induct on the root object. Then, by an easy inversion on the hypothesis generated by remember, all cases that don’t match the required form generated by the case analysis will be automatically solved by the principle of explosion.

Sometimes, the automatically-generated induction principles for a type are not sufficient to prove some properties about terms with that type. In this case, it is possible to write a custom induction principle for a type and then use it with the induction tactic.

Syntax

(* Simple usage *)
induction n.

(* Induct over a term and introduce a hypothesis E showing its equivalence to the form it took *)
induction n eqn:E.

(* Providing names for newly-introduced terms *)
induction n as [| n' IHn' ].

(* Using a custom induction principle *)
induction z using peano_ind.

Examples

Before

n: nat
-------------------------
n + 0 = n

induction n as [| n' IHn' ].

After (first goal generated)

-------------------------
1/2
0 + 0 = 0

After (second goal generated)

n': nat
IHn' : n' + 0 = n'
-------------------------
1/1
S n' + 0 = S n'

Script

Theorem induction_example1 : forall (n : nat),
    n + 0 = n.
Proof.
    induction n.
    - reflexivity.
    - simpl. rewrite IHn. reflexivity.
Qed.

Script

Require Import ZArith.
Open Scope Z.
Theorem induction_example2 : forall (x y : Z),
    x + y = y + x.
Proof.
    induction x using Z.peano_ind.
    - intros. simpl. rewrite Z.add_0_r. reflexivity.
    - intros. rewrite Z.add_succ_l. rewrite IHx.
      rewrite Z.add_comm. rewrite <- Z.add_succ_l.
      rewrite Z.add_comm. reflexivity.
    - intros. rewrite Z.add_pred_l. rewrite IHx.
      rewrite Z.add_comm. rewrite <- Z.add_pred_l.
      rewrite Z.add_comm. reflexivity.
Qed.

Resources

Reference Documentation

Automation

This is basically a catch-all category for tactics that do a lot of things at once. This category of tactics generally intends to solve a large category of simple goals to reduce the load of the proof writer.

auto

auto does a recursive search through a specified knowledge base in order to solve goals. If auto cannot completely solve a goal, it succeeds with no changes to the goal.

The knowledge bases that auto uses are called Hint Databases. Hint databases are provided by the standard library, and can also be created and added to by users. Hint databases can contain a variety of hint types, including but not limited to:

Constructors: auto will now try to apply each of the constructors for a given Inductive type
Unfold: auto will now try to unfold a given definition - helpful when trivial simplification isn’t enough
Resolve: auto will now try to simple apply a given lemma

The default hint database used by auto when no other database is specified is core.

Syntax

(* Simple usage *)
auto.

(* Using a specific database *)
auto with bool.

(* Using a specific lemma *)
auto using example.

Examples

Before

-------------------------
1/1
0 = 0

auto.

After

Proof finished

Script

Create HintDb automation.
Lemma add_0_r : forall n, n * 1 = n. 
Proof. induction n. auto. simpl. now rewrite IHn. Qed.
Hint Resolve add_0_r : automation.

Lemma x : (forall n, n * 1 = n) /\ (true = true). 
Proof. auto with automation. Qed.

Resources

Reference Documentation

Hint Databases

trivial

trivial is essentially a non-recursive auto. trivial is best utilized when a lemma that exactly matches the goal already exists in the hint database.

Syntax

(* Simple usage *)
trivial.

(* Using a specific database *)
trivial with bool.

Examples

Script

Theorem trivial_example : forall {X : Type} (n : X), 
    n = n.
Proof.
    trivial.
Qed.

Resources

Reference Documentation

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

Table of Contents

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Syntax

Examples

Resources

Syntax

Examples

Resources

Syntax

Examples

Resources