It seems like a rite of passage to create one of these because there are so many Coq tactic cheat sheets out there and there’s just so much to learn. Here’s mine.

This is mostly about tactics but I realized not really.

Links:

- Coq Tactics. Authoritative but dense.
- Logical Foundations (Software Foundations Volume 1). I think the order of ideas makes pedagogical sense but also makes it hard for me to look up particular tactics or concepts.
Other Coq cheat sheets found by Googling “Coq cheat sheets”:

- Coq Tactics Index (Joseph Redmon)
- Coq Tactics Cheatsheet (Cornell CS3110)
- Coq Tactics Quick Reference (Adam Chlipala) / the Formal Reasoning About Programs book also has a nice appendix
- Coq Tactics (UPenn ???)

Meta-notes: I cover a lot of weak tactics because I like knowing exactly what my tools are doing. I try to use the variants of tactics that explicitly name things produced when possible. I am sure there is nomenclature I don’t understand precisely and use sloppily in this list; I am also sloppy with metavariables. Even things that are correct might be horrible style. There are likely other errors and omissions. They might be fixed one day. I’m putting this up nevertheless because it’s personally useful.

### Things I wish I knew but didn’t learn from Software Foundations or Coq tactic cheat sheets

- The first two sections are not about tactics per se but how to find theorems to use and how to use them. Knowing how to use all of these query commands is super useful.
- To clean up repeating subexpressions with “local variables”, I find
`remember expr as X eqn:Hname.`

easier to work with than`set (X := expr).`

`pose proof expr as Hname.`

adds`expr`

to the context, with name`Hname`

. Modus ponens where you know`H1`

and`H2`

, which is “`H1`

implies`H3`

”, is just`pose proof (H2 H1) as H3`

.- Software Foundations covers bullets and curly braces early, but I like subgoal specification with
`1:`

,`2:`

etc., which can really help limit nesting depth.`2: (tactic that solves subgoal 2).`

If you want more bullets, there are infinitely many, not just three. After`-`

`+`

`*`

you can use`--`

`++`

`**`

`---`

etc.

### How to fish

- Use the queries.
`Search "foo".`

`Check foo.`

`About foo.`

`Compute foo.`

`Print foo.`

To look up notation (e.g. what does`<>`

mean?) use`Locate`

(e.g.`Locate "<>"`

). - To look up a simple abstract theorem about natural numbers or equality without knowing what it’s called,
`SearchPattern`

is useful. For example, I was looking to prove`x <> y`

given`y <> x`

.`SearchPattern (_ <> _ -> _ <> _).`

found the theorem for me (it was called`not_eq_sym`

). Similarly`SearchRewrite`

on some expression pattern searches for theorems you could use to rewrite that expression.

### How to use hypotheses

To use that example again: If you run `Check not_eq_sym.`

you’ll get:

```
not_eq_sym
: forall (A : Type) (x y : A), x <> y -> y <> x
```

Mathematically, `not_eq_sym`

says: for any type `A`

and any two things `x`

and `y`

of type `A`

, if `x <> y`

, then `y <> x`

.

However the literalist programmer view is more like: `not_eq_sym`

is a (fully curried) function that takes in a type `A`

, two things `x`

and `y`

of type `A`

, and finally a proof of the Prop `x <> y`

, and outputs a proof of the Prop `y <> x`

. So if you supplied these four arguments, just by writing `not_eq_sym A x y H`

where `H`

is a proof of `x <> y`

, you’d get a proof of `y <> x`

out.

Well, not quite; you’d actually write `@not_eq_sym A x y H`

. Here `@`

makes all *implicit* arguments of `not_eq_sym`

explicit. If you also run `About not_eq_sym.`

, you’ll see (among other text):

```
not_eq_sym : forall (A : Type) (x y : A), x <> y -> y <> x
Arguments A, x, y are implicit
```

Without the `@`

you only need to supply (and are only allowed to supply) the one non-implicit argument, `H`

, to `not_eq_sym`

. In practice arguments are usually implicit because they’re deducible from the others, so `not_eq_sym H`

is pretty good.

Implicits can appear in other ways and cause weird issues, such as when you’re trying to rewrite or do something else to an expression that seems to exactly match one side of the rule you’re rewriting with, but Coq refuses to operate on that expression even though it’s in plain sight. The expressions might actually be different because they have implicit arguments that differ. You can see those implicits in the expressions by issusing `Show Print Implicit.`

, or fiddling with your CoqIDE settings.

### Finishing a proof of something true

`reflexivity.`

proves something is equal to itself. It can handle some simplification.

Side note:`exact T.`

proves a Prop that’s exactly the same as theorem or hypothesis T. “Exactly the same” includes quantifiers! But you can apply arguments to T. For example if your theorem`all_foo`

says`forall x : foo x`

and you want to prove`foo y`

for a specific known`y`

, you could use`exact (all_foo y)`

.`I`

is the name for the unique thing of type`True`

, so if you end up with the goal`True`

after simplification and want to prove it with the weakest possible tactic, I think`exact I.`

fits the bill.`assumption.`

proves a Prop that is one of our hypotheses, i.e., is in our context. It’s`exact T.`

without needing to specify`T`

.`refine X.`

proves a Prop that’s exactly the same as`X`

, just like`exact X.`

, except that`X`

here can be an expression with*holes*, or`_`

. It opens up one subgoal for each`_`

.`apply H.`

proves a Prop that directly follows from a theorem or hypothesis`H`

(or, if the theorem is “P implies our goal”, sets the goal to P instead; see below). So`apply all_foo.`

would work instead of`exact (all_foo y).`

`trivial.`

is a weak tactic that proves some very easy goals, including the power of`reflexivity`

and`assumption`

at least.`easy.`

is slightly more powerful. It does`split`

too.There are a lot of automated tactics that can handle proving generally true math facts. We are told to use

`lia`

in 6.826.

### Finishing a proof of something false

`discriminate H.`

proves anything, given an equality`H`

that says something equals something structurally different (with different constructors). You don’t need to specify`H`

.`contradiction.`

proves anything if a hypothesis is false. Note that it has to be a hypothesis and not a thing before`->`

; if you want to do that,`intros`

it. It also searches for two contradictory hypotheses.`absurd P.`

proves anything by breaking into subgoals`P`

and`~P`

.

Sidebar: `congruence.`

generalizes `discriminate`

and `injection`

in some way.

### Modifying the goal with existing facts

`apply H.`

sets the goal to P if`H`

is “P implies our goal” (or, directly proves a Prop that directly follows from a theorem; see above).`H`

can also take more than one argument or premise, in which case`apply H.`

opens up one subgoal per premise. (So in fact, finishing a goal via “`apply H.`

” is just the special case where there are zero premises.)`eapply`

is similar to`apply`

, but it uses existential variables when it can’t figure out some of the variables, and just expects you to fill those in later. This was really hard for me for me to understand, but here’s an artificial example: let’s say you want to prove an equality`a = b`

by the transitive property.`a = b`

matches the conclusion of the built-in theorem`eq_trans`

, which is`x = y -> y = z -> x = z`

. However,`apply eq_trans.`

will fail, because Coq can’t figure out what you want`y`

to be. You could solve this by explicitly specifying what`y`

is by passing some arguments to`eq_trans`

. Alternatively, you can`eapply eq_trans.`

and Coq will create a new existential variable to pass as`y`

. Later, if you implicitly use any tactic that implies something about that variable, Coq will collapse or elaborate that variable.

`simpl.`

simplifies the expression. It’s often not necessary in a finished proof, but can help clarify what the goal looks like in the interactive process.`rewrite -> H.`

resp.`rewrite <- H.`

If H is something that says “A = B”, replace A with B in the goal, resp., B with A. If`H`

requires some hypotheses, it will open up those hypotheses as subgoals, coming last.`rewrite -> H by tactic.`

resp.`rewrite <- H by tactic.`

As above but immediately solve the subgoals.`subst x.`

substitutes`x`

everywhere it appears. If you defined`x := expr`

or got an equation like`x = expr`

then this will replace`x`

with`expr`

everywhere and then get rid of`x`

. This is useful if you had two variables`x`

and`y`

introduced in different places in your proof, proved they were equal, and want to fully get rid of one from your context. You can write`subst.`

without`x`

and it will do it automatically.`unfold f.`

Unfold some function f in the goal; approximately, inline it. This may be required if`f`

is a`match`

expression; Coq won’t automatically “simplify” expressions with`f`

since they might actually get more complicated.`replace term with term'.`

Replace`term`

with`term'`

in the goal, and adds a new goal to prove that`term = term'`

, putting it last.`replace term with term' by tactic.`

Same, but prove that new goal immediately with a tactic.`change term with term'.`

Roughly same as`replace`

without opening subgoals, if the terms are “convertible”. I was told this means something like “you can prove they’re equal by`reflexivity`

”.`symmetry.`

swaps the goal`a = b`

with`b = a`

.`exfalso.`

explicitly sets the goal to`False`

; sometimes this makes applying theorems easier.

### Adding intermediate goals

`assert U as Name.`

adds hypothesis U with name`Name`

to context; immediately opens subgoal U.`Name`

can be a destruct pattern.`assert U as Name by tactic.`

Same, but immediately prove the subgoal with a tactic instead.`enough U as Name.`

is the same, but U is proved afterwards.`cut P.`

splits the goal into`P -> goal`

and`P`

.`transitivity X.`

lets you prove`A = B`

through subgoals`A = X`

and`X = B`

.

(There’s also an `assert (Name : U)`

syntax but I never remember the order.)

### Splitting into cases

`constructor.`

splits the goal into cases if it’s some kind of product type. It’s actually basically just`apply`

ing the constructor. When the goal is a sum type,`constructor N.`

for some number`N`

more precisely chooses to prove the`N`

th constructor.`f_equal.`

, when the goal is to prove that two calls to the same function are equal, splits into proving that each of the corresponding arguments are equal. (Note that the original goal being true very much doesn’t imply these goals are all true, although it does if the function is a constructor.)`destruct expr as [pattern].`

splits`expr`

apart, possibly breaking into cases, depending on what constructor`expr`

is. Here`[pattern]`

should be an “intro pattern of disjunctions and conjunctions”. If`expr`

is a product then`[pattern]`

could be`[H1 H2]`

; if`expr`

is a sum then`[pattern]`

could be`[H1 | H2]`

; this could be nested, e.g.`[H1 H2 | H3 H4 H5 | ]`

if it’s a sum of cases with 2, 3, and 0 fields, respectively (and this is what I mean elsewhere by`[pattern]`

). You can even omit “as …” if there’s nothing to destruct to.`destruct expr eqn:Hname.`

does the same, but also giving you a hypothesis with name`Hname`

that states that`expr`

equals what the case is.`induction n as [pattern].`

splits into base case and induction hypothesis based on what constructor`n`

is. Every branch of the pattern comes with an induction hypothesis. Note:`induction`

behind the scenes is just`apply`

on the “inductive principle” Coq generated when it or you declared the type of`n`

. It seems to have the name of the type of`n`

concatenated with`_ind`

.

Coq is constructive, so you can’t assume `P \/ ~P`

(“P or not P”) in full generality. However you can do this for many common cases of `P`

. Theorems that prove this often have `dec`

in their name for “decidable”. Consider `SearchPattern`

for not just `_ \/ _`

, but also `{_} + {_}`

(where either `_`

could be further refined depending on what you’re looking for).

The difference, based on my limited understanding and a Piazza answer: `_ \/ _`

is a Prop but `{_} + {_}`

is a Type. Prop and Type belong to different “universes”, approximately proof stuff and computable stuff, and Coq enforces that information can’t flow from the proof universe to the computable universe. So a `{_} + {_}`

is stronger than a `_ \/ _`

in that (after specifying any variables needed) you can explicitly compute which branch of the `{_} + {_}`

you have evidence for, and use that information in a function that computes something.

In proofs, you use them in the same way, though: `destruct`

into two cases to do case analysis. Example of theorems of two kinds:

```
Nat.eq_dec: forall n m : nat, {n = m} + {n <> m}
le_gt_dec: forall n m : nat, {n <= m} + {n > m}
le_dec: forall n m : nat, {n <= m} + {~ n <= m}
```

```
Nat.eq_0_gt_0_cases: forall n : nat, n = 0 \/ 0 < n
gt_0_eq: forall n : nat, n > 0 \/ 0 = n
Nat.lt_trichotomy: forall n m : nat, n < m \/ n = m \/ m < n
```

Note that you probably `destruct`

these into patterns to name the proofs of things, and won’t want `eqn:`

.

### Modifying hypotheses

`apply H in H2 as Hname.`

If H is “P implies Q” and H2 is “P”, conclude Q, with name`Hname`

.`pose proof H as Hname.`

Add`H`

to the context, with name`Hname`

. Typically`H`

will be an expression. Concrete applications: if`H1`

is a theorem “P implies Q” and`H2`

is a hypothesis in the context that “P”,`pose proof (H1 H2) as Hname.`

`specialize (H1 H2).`

Kind of like`pose proof`

specifically for plugging arguments into a local hypothesis`H1`

. The name “specialize” makes the most sense if the arguments are universally quantified variables, e.g. the hypothesis`H`

says`forall x : T, foo x`

and you have a specific`y`

for which you want to know`foo y`

, so you`specialize (H y).`

On the other hand this is more reliably useful when`H2`

is a premise of`H1`

, since you get a strictly stronger result. Note that the result replaces`H`

with the result of specialization, which makes more sense in the universally quantified variable interpretation but is more reliably useful in the premise interpretation. If you want to get a specialized version without losing the generalized version, use`pose proof`

above.`rewrite -> H in H2.`

/`rewrite <- H in H2.`

/`replace term with term' in H2.`

/`replace term with term' in H2 by tactic.`

/`change term with term' in H2.`

/`unfold X in H.`

/`simpl in H.`

/`symmetry in H.`

all do the same rewriting you’d expect in a hypothesis instead of the goal.`inversion H.`

analyzes H using constructor injectivity and disjointness. That is, it unwraps a constructor from both sides: e.g. if H is`S x = S y`

, conclude`x = y`

; or, if H claims the equality of different constructors, it explodes the case.`clear H.`

deletes something.`rename Hold into Hnew.`

renames a hypothesis in the context.`remember expr as X eqn:Hname.`

introduces a new variable`X`

equal to the expression and an equation that the variable`X`

equals the expression. (There’s also`set (X := expr).`

but this gives you a definition instead of an equation, which seems a bit harder to work with; you can`unfold`

the newly defined variable, but can’t directly refer to the definition by name to rewrite the expression into the variable if it comes up later.)

### Introducing universally quantified variables or LHS’s of implications

`intros n.`

introduce universally quantified variables or LHS’s of implications into the context.`intros [pattern].`

combines it with a`destruct`

.

`revert m.`

basically undoes an`intros`

when it’s simple.`generalize m.`

undoes an`intro`

in more cases, replacing`m`

with a universally quantified variable. But`m`

can be an expression.`generalize dependent m.`

undoes an`intro`

in even more cases. It clears hypotheses depending on`m`

.

### Working with Ands and Ors

`split.`

when trying to prove`A /\ B`

, split into subgoals`A`

and`B`

. (This actually works for any goal with one constructor, and is basically just`constructor 1.`

)`left.`

when trying to prove`A \/ B`

, specifically prove`A`

. (This actually works for any goal with two constructors, and is basically just`constructor 1.`

)`right.`

when trying to prove`A \/ B`

, specifically prove`B`

. (This actually works for any goal with two constructors, and is basically just`constructor 2.`

)`destruct Hand as [Hleft Hright].`

turns a hypothesis`A /\ B`

into hypotheses`A`

and`B`

.`destruct Hor as [Hleft | Hright].`

uses a hypothesis`A \/ B`

by splitting into cases where either`A`

(named`Hleft`

) or`B`

(named`Hright`

) is true.

The underlying proof objects, for the curious:

```
conj : forall A B : Prop, A -> B -> A /\ B
or_introl : forall A B : Prop, A -> A \/ B
or_intror : forall A B : Prop, B -> A \/ B
```

Projecting clauses from a conjunction:

```
proj1: forall A B : Prop, A /\ B -> A
proj2: forall A B : Prop, A /\ B -> B
```

### Working with Existence

`exists x.`

is how you prove an`exists a, (something about a)`

, by explicitly exhibiting an`x`

satisfying that something.`destruct Hexists as [x H].`

turns an existence result into the explicit example (“witness”) satisfying that result and the hypothesis stating that the result does hold for the witness.

`ex_intro : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists y, P y`

What *is* this `exists y, P y`

business anyway? It’s special notation for `ex`

:

```
"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope (default interpretation)
"'exists' ! x .. y , p" := ex (unique (fun x => .. (ex (unique (fun y => p))) ..)) : type_scope (default interpretation)
```

```
ex : forall A : Type, (A -> Prop) -> Prop
Argument A is implicit
```

And `ex_intro`

above is the one constructor of this type.

### Equality and negation, while we’re at it

```
eq_refl : forall (A : Type) (x : A), x = x
"x = y" := eq x y : type_scope (default interpretation)
"x <> y" := not (eq x y) : type_scope (default interpretation)
```

### Working with subgoals

These are the things that come out of case-splitting tactics.

Bullets. Basically when you’ve spilt your goal into N subgoals, you make a list with N items, one per subgoal, each with the same bullet. It’s checked that you’ve totally finished a subgoal before you go to the next bullet on the same level. Nested levels must have different bullet types.

`(* some tactic that splits into three cases *) - (* handle case 1 *) + (* handle case 1.1 *) + (* handle case 1.2 *) - (* handle case 2 *) - (* handle case 3 *)`

Software Foundations introduces you to the three bullets

`-`

,`+`

, and`*`

, but you can get more by repeating any of these:`--`

,`++`

,`**`

,`---`

, etc. Whether you’d want to is another matter.`{`

`}`

serve a similar goal.`{`

narrows down to a single subgoal;`}`

forces you to have finished it. They can be arbitrarily nested, and reset the bullet context so you can reuse the same bullets inside and outside`{}`

s. Also note that finishing one subgoal with`}`

doesn’t require you to start the next one with`{`

. Sometimes something like this will make sense, especially if the tactic splits into two cases with really different “weight” (e.g.`assert`

ing a relatively easy lemma before continuing).`(* some tactic that splits into two cases *) { (* handle case 1 *) } (* handle case 2 *)`

`1:`

,`2:`

, etc. solves a specifically numbered subgoal with a tactic or bracketed logic. I like to use this when my goal splits into two or more cases where a particular case is very easy and I don’t want to spend a layer of bullets on this split. I have no idea whether this is good style. For example, if my goal splits into two cases and the second case can be proven with`reflexivity`

but the first case is very complex, I might do`split. 2: reflexivity.`

and then continue with the proof of case 1. Comma-separated numbers and ranges denoted with hyphens both work. Cases are 1-indexed.`;`

(semicolon) solves all subgoals with the same tactic. For example, you could use`split; reflexivity.`

to prove something like`a = a /\ b = b`

.`repeat`

some tacic e.g.`repeat rewrite -> H.`

repeats a tactic until it fails.`all:`

applies a tactic to all subgoals. This is like`;`

but you get to pause beforehand, and also is how you use goal-reordering tactics.

You can try tactics but not fail if they don’t apply. This is likely only useful acting on multiple subgoals at once, so most likely after `;`

or `all:`

. I think they should probably be used sparingly. Or maybe in custom tactics.

`try`

tries a tactic but doesn’t fail if it fails.`||`

combines two tactics, trying the left tactic before trying the right tactic.

### “Cheating”

`admit.`

lets you pretend a subgoal is proved and move on. The proof will need to end with`Admitted.`

instead of`Qed.`

### Custom tactics and hint databases

Let’s say you’re building a hint database called `foo`

. If you got a theorem `bar`

that you want to rewrite rightwards automatically, you can add it like:

`Hint Rewrite bar : foo.`

Probably only do this if `bar`

doesn’t take any premises. If you want to autorewrite using a theorem `bar`

with premises that might not always be true, and you only want to autorewrite when the premises can be automatically proven, you can say that the premises must be solved with `auto`

to use the hint:

`Hint Rewrite bar2 using (solve [ auto ]) : foo.`

After all that you can use `autorewrite with foo.`

The simplest way to build a custom tactic just looks like:

`Ltac my_tactic := tactic1; tactic2; tactic3.`

More interesting tactics will pattern match on the goal or on hypotheses. Use the syntax `match goal with ...`

. The pattern has `|-`

to separate hypotheses from the goal.

You can name hypotheses. To name variables or expressions that might appear in the hypotheses or goal but might vary and that you want to use in the tactic, use a question mark in front of a name in the pattern. Don’t use that question mark in the body of the tactic. Example:

```
Ltac subst_Some_eq :=
match goal with
| H : Some ?a = Some ?b |- _ =>
inversion H; subst b
end.
```

If you want to pattern-match on any expression anywhere, use `context[ ]`

.

```
Ltac destruct_if :=
match goal with
| |- context[if ?a then _ else _] => destruct a
end.
```

If you only want to do something if some variable `?x`

is a variable, you can use `is_var x`

before the tactic. `match`

backtracks and tries matching its pattern to more hypotheses; it also tries the next branch if the branch pattern doesn’t match or if the tactics fail. Alternate: `lazymatch`

doesn’t backtrack from tactic failures.

`progress`

on some tactic only works if the tactic makes progress.

`idtac`

is a tactic that does nothing, plus you can pass arguments to debug.

The `fail`

tactic takes a number, the number of levels to propagate the failure up, and then extra debugging stuff.

`first [ t1 | t2 | ... ]`

takes some tactics and does the first one that succeeds.

`type of X`

gives the, well, type of `X`

Ltac is also a functional programming language! Use `constr:(...)`

to break back into Gallina. Note that `match`

patterns are implicitly Gallina.

```
(* can't infer T sad *)
Ltac map T f l :=
let rec map_impl l :=
match l with
| nil => constr:(@nil T)
| ?h :: ?t => let h' := f h in let t' := map_impl t in constr:(h' :: t')
end in map_impl.
Goal False.
let ls := map (nat * nat)%type ltac:(fun x -> constr:((x, x))) (1 :: 2 :: 3 :: nil) in pose ls.
```

You can’t do `;`

in functional programming Ltac, it turns into a procedure thing.

Brackets are super precise. This applies these three tactics respectively to the three focused goals. There must be exactly three. You can omit tactics to do `idtac`

, the identity tactic.

`[> tactic1 | tactic2 | tactic3 ]`

Note that in a proof script you have to apply to all focused goals so it would look like `all: [> tactic1 | tactic2 | tactic3 ]`

although this is a silly way to do it. If you’re putting this after a semicolon, you can drop the `>`

. I’m not sure how this works.

### FRAP tactics

`simplify.`

improves on`simpl.`

`cases expr.`

improves on`destruct expr.`

(No patterns though.)`invert x.`

improves on`inversion x.`

`linear_arithmetic.`

improves on`lia.`

`propositional.`

handles and simplifies things based on propositional logic: conjunctions, disjunctions, implications…`first_order.`

handles and simplifies things based on first order logic. It’s more powerful, but riskier; it might run forever.