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.
* Keep in mind that x <> y is actually shorthand for x = y -> False! This means that discriminate actually searches for trivial inequalities in assumptions.
(* Simple usage *)
discriminate.Before
=========================
1/1
1 <> 2discriminate.After
No more goals.Before
=========================
1/1
"hello" <> "world"discriminate.After
No more goals.Before
H: S n = O
==========================
1/1
Falsediscriminate.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.