Home |
Github |
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:
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.
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:
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!
Typically the first tactics a Coq user ever utilizes.
intros finds assumptions builtin to your goal (usually in
the form of a forall quantifier) and moves them to the
goal’s context (a.k.a. hypothesis space, assumption space). This is
similar to the first step of many informal, paper proofs, when the
prover states “let there be some number n, …”
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 - unless an explicit name is
provided for them.
A simpler tactic, intro, acts similarly but can only
introduce one assumption, and will introduce variables contained in
opaque/wrapped definitions.
(* 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].Before
=========================
forall (n : nat), n + 0 = nintros x.After
x: nat
=========================
1/1
x + 0 = xBefore
=========================
forall (A B C : Prop), A /\ B -> C -> A /\ Cintros A B C [ATrue BTrue].After
A, B, C: Prop
ATrue: A
BTrue: B
=========================
1/1
C -> A /\ CBefore (assume P := forall (n : nat), n = n)
=========================
1/1
Pintros.After
=========================
1/1
PAlternatively,
intro.After
n: nat
=========================
1/1
n = nclear 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.
clear - ... can also be used to erase all assumptions
not depended on by a provided set of assumptions.
(* Simple usage *)
clear H.
(* Clear multiple assumptions *)
clear H Heq X Y n.
(* Clear anything that x, z, or c do not depend on *)
clear - x z c.Before
n: nat
H, Hr1, Hr2: n = 0
IHn: n = 1
=========================
1/1
Trueclear Hr1 Hr2.After
n: nat
H: n = 0
IHn: n = 1
=========================
1/1
TrueBefore
a, b, c, x, y, z: nat
H: a = z
=========================
1/1
Trueclear - a x H.After
a, x, z: nat
H: a = z
=========================
1/1
TrueThis 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 evaluates terms that are constructed of constant
values - not variables. simpl can also partially evaluate
partially-constant values.
(* 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.Before
=========================
1/1
2 + 2 = 1 + 3simpl (2 + 2).After
=========================
1/1
4 = 1 + 3unfold replaces definition identifiers with the
definition’s contents, simplifying along the way.
(* 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 *.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 :: lunfold 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 :: lsplit is primarily used to break a single goal of the
form A /\ B into two new goals A and
B.
You will often notice that split seems to solve some of
the subgoals that it generates. This is because split is
just shorthand for constructor 1 (see the constructor
tactic).
Looking at the definition of /\ (or
and):
Inductive and (A B : Prop) : Prop := conj : A -> B -> A /\ B.we can see that and has a single constructor called
conj - so constructor 1 simply reduces to
apply conj, which would give us goals A and
B due to the impliciations that it carries.
split.Before
=========================
1/1
True /\ Falsesplit.After
=========================
1/2
True
=========================
2/2
FalseEach 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 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.
(* Simple usage *)
reflexivity.Before
n: nat
=========================
1/1
n = nreflexivity.After
No more goals.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.
(* Simple usage *)
assumption.Before
P: Prop
H: P
=========================
1/1
Passumption.After
No more goals.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.
(* Simple usage *)
discriminate.Before
=========================
1/1
1 <> 2discriminate.After
No more goals.Before
=========================
1/1
"hello" <> "world"discriminate.After
No more goals.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.
(* Simple usage *)
exact I.Before
=========================
1/1
Trueexact I.After
No more goals.Before
n: nat
=========================
1/1
n + 5 = n + 5exact (eq_refl (n + 5)).After
No more goals.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.
(* Simple usage *)
contradiction.Before
H: False
=========================
1/1
Falsecontradiction.After
No more goals.Before
x, y: nat
H: x = y
H0: x <> y
=========================
1/1
x = x + ycontradiction.After
No more goals.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 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.
(* 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.Before
x, y: nat
H: x = y
=========================
x + y = y + yrewrite H.After
x, y: nat
H: x = y
=========================
y + y = y + yAlternatively,
rewrite <- H.x, y: nat
H: x = y
=========================
x + x = x + xrename changes the name of an introduced variable or
assumption.
(* Simple example *)
rename x into y.Before
n: nat
=========================
1/1
n = nrename n into x.After
x: nat
=========================
1/1
x = xremember 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.
(* Simple usage *)
remember (5 + x).
(* Provide a name for the remembered term *)
remember ("hello world") as s.Before
x, y: nat
H: x + y = x
=========================
1/1
y = 0remember (x + y) as sum.After
x, y, sum: nat
Heqsum: sum = x + y
H: sum = x
=========================
1/1
y = 0symmetry is used to swap the left and right sides of an
equality.
symmetry can be used on either the goal or a list of
hypotheses.
(* Usage on goal *)
symmetry.
(* Usage on hypotheses *)
symmetry in H.
symmetry in H1, H2.Before
=========================
1/1
5 = 2 + 3symmetry.After
=========================
1/1
2 + 3 = 5Case 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 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.
(* 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].Before
n: nat
=========================
n = 0 \/ 1 <= ndestruct n as [| n'] eqn:E.After (first goal generated)
n: nat
E: n = 0
=========================
1/2
0 = 0 \/ 1 <= 0After (second goal generated)
n, n': nat
E: n = S n'
=========================
2/2
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. 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.
(* Standard usage *)
inversion H.Before
n: nat
H: n <= 1
=========================
1/1
n = 0 \/ n = 1inversion H.After (first goal generated):
Note: this is the case of n <= 1 where
n = 1, hence H0.
n: nat
H: n <= 1
H0: n = 1
=========================
1/2
1 = 0 \/ 1 = 1After (second goal generated):
Note: this is the case of n <= 1 where
n < 1, equivalent to n <= 0, hence
H1.
n: nat
H: n <= 1
m: nat
H1: n <= 0
H0: m = 0
=========================
1/1
n = 0 \/ n = 1Script
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.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.
(* 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.Before
n: nat
=========================
n + 0 = ninduction n as [| n' IHn' ].After (first goal generated)
=========================
1/2
0 + 0 = 0After (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. “Induction Principles” - Logical Foundations
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 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 typeUnfold: auto will now try to unfold a
given definition - helpful when trivial simplification isn’t enoughResolve: auto will now try to
simple apply a given lemmaThe default hint database used by auto when no other
database is specified is core.
(* Simple usage *)
auto.
(* Using a specific database *)
auto with bool.
(* Using a specific lemma *)
auto using example.Before
P: Prop
H: P
=========================
1/1
0 = 0 /\ True /\ Pauto.After
No more goals.Script
Create HintDb automation.
Lemma mul_1_r : forall n, n * 1 = n.
Proof. induction n. auto. simpl. now rewrite IHn. Qed.
Hint Resolve mul_1_r : automation.
Lemma x : (forall n, n * 1 = n) /\ (true = true).
Proof. auto with automation. Qed.“More Automation” - Logical Foundations
“A Streamlined Treatment of Automation” - Logical Foundations
“Theory and Practice of Automation in Coq Proofs” - Programming Language Foundations
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.
(* Simple usage *)
trivial.
(* Using a specific database *)
trivial with bool.Script
Theorem trivial_example : forall {X : Type} (n : X),
n = n.
Proof.
trivial.
Qed.easy throws many common “closing tactics” at a goal to
solve a large category of simple problems. easy will
attempt to use:
easy is the base form of the now tactical.
easy.Before
P: Prop
H: P
=========================
1/1
True /\ 42 = 14 * 3 /\ Peasy.After
No more goals.idtac leaves a goal completely unchanged. This tactic
will never fail.
A term can be provided as an argument to print a message to the console. String and integers are printed literally rather than via their type’s pretty-printer.
idtac is sometimes useful when you have many goals
selected and only want to operate on some of them.
(* Simple usage *)
idtac.
(* Print a message *)
idtac "Hello World!".Before
=========================
1/1
Trueidtac.After
=========================
1/1
TrueBefore
n: nat
=========================
1/1
n + 0 = n(* Only apply reflexivity to the n = 0 case. Leave the n = S n' case unaffected *)
induction n; [reflexivity | idtac].After
n : nat
IHn : n + 0 = n
=========================
1/1
S n + 0 = S nfail always fails.
This is sometimes useful if you’re building a complex tactic with try-catch behavior.
(* Simple usage *)
fail.Before
=========================
1/1
Truefail.After
Error: Tactic failure.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.
The try tactical executes a provided tactic, catching
any errors and always succeeding.
(* Simple usage *)
try reflexivity.Before
n: nat
=========================
1/1
n + 0 = ntry reflexivity.After
n: nat
=========================
1/1
n + 0 = nAlternatively,
try apply add_0_r.No more goals.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.
(* Simple usage *)
split; reflexivity.
(* Left-associative chain *)
split; simpl; reflxivity.
(* Right-associative chain *)
split; (split; auto).Before
P, Q: Prop
H: Q
=========================
1/1
P \/ Qconstructor; 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 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 failspar: Applies the tactic to all goals in focus
in parallel. The tactic provided must solve all goals
or do nothing, otherwise this tactic failsn-m: Applies the tactic to goals with indices between
n and m, inclusiveall: simpl.
par: simpl; reflexivity; auto.
!: discriminate.
2-3: auto.Before
=========================
1/2
True
=========================
2/2
Trueall: 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.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.
(* Simple usage *)
repeat split.Before
P, Q, R, S: Prop
=========================
1/1
P /\ Q /\ R /\ Srepeat split.After
P, Q, R, S: Prop
=========================
1/4
P
=========================
2/4
Q
=========================
3/4
R
=========================
4/4
SThe 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.
(* Simple usage *)
reflexivity || assumption.Before
P: Prop
H: P
=========================
1/1
Preflexivity || assumption.After
No more goals.now tactic is simply notation for tactic;
easy.
now split.Before
=========================
1/1
True /\ 42 = 14 * 3now split.After
No more goals.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.
do 3 (split; [reflexivity | idtac]).Before
=========================
1/1
1 = 1 /\ 2 = 2 /\ 3 = 3 /\ 4 = 4do 3 (split; [reflexivity | idtac]).After
No more goals.