When proving theorems in Coq, knowing what tactics you have at your disposalis vital. In fact, sometimes it’s impossible to complete a proof if you don’tknow the right tactic to use!

Coq Cheat Sheet for CS3234 (Aquinas Hobor and Martin Henz) Note. This is not meant to be comprehensive or stand on its own, but just to give you some idea for what is going on in an informal manner, as well as give you a cheat sheet when you want to remind. How to Use The Ordinary skincare by Deciem. A lot of people write out their regimens or print out a spreadsheet to keep things organised. Labelling the bottles with a permanent marker also makes it easier to know what goes where- those dropper bottles can all blur into one first thing in the morning.

We provide this tactics cheatsheet as a reference. It contains all the tacticsused in the lecture slides, notes, and lab solutions.

Quick Overview

• COSC 4P42 - Cheat Sheet Natural deduction rules and Coq implementation φ φ^ ^I And Intro. Replaces the current goal A^Bby the two goals Aand B. Φ^ φ ^E1 And Elim 1 in H. Applies to an assumption of the form H: A^B and generates a new assumption H0: A φ^ ^E2 And Elim 2 in H. Applies to an assumption of the form H: A^B and generates a new.
• Coq cheatsheet General remarks:P (“notP”)isequivalenttoP!False. Simple commands Proof: Beginprovingatheorem. Proveagoaloftheforma = a.

Here is a brief overview of the tactics that we’ve covered. Click on any ofthe links for more details about how to use them.

• assumption: Solves the goal if it is already assumed in the context.
• reflexivity: Solves the goal if it is a trivial equality.
• trivial: Solves a variety of easy goals.
• auto: Solves a greater variety of easy goals.
• discriminate: Solves the goal if it is a trivial inequalityand solves any goal if the context contains a false equality.
• exact: Solves a goal if you know the exact proof term that provesthe goal.
• contradiction: Solves any goal if the context contains False or contradictory hypotheses.

• intros / intro: Introduces variables appearing with forallas well as the premises (left-hand side) of implications.
• simpl: Simplifies the goal or hypotheses in the context.
• unfold: Unfolds the definitions of terms.
• apply: Uses implications to transform goals and hypotheses.
• rewrite: Replaces a term with an equivalent term if theequivalence of the terms has already been proven.
• inversion: Deduces equalities that must be true given anequality between two constructors.
• left / right: Replaces a goal consisting of a disjunctionP / Q with just P or Q.
• replace: Replace a term with a equivalent term and generates asubgoal to prove that the equality holds.

• split: Replaces a goal consisting of a conjunction P / Q withtwo subgoals P and Q.
• destruct (and/or): Replaces a hypothesis P / Q with twohypotheses P and Q. Alternatively, if the hypothesis is a disjunctionP / Q, generates two subgoals, one where P holds and one where Q holds.
• destruct (case analysis): Generates a subgoal for everyconstructor of an inductive type.
• induction: Generates a subgoal for every constructor of aninductive type and provides an induction hypothesis for recursively definedconstructors.

• ring: Solves goals consisting of addition and multiplicationoperations.
• tauto: Solves goals consisting of tautologies that hold inconstructive logic.
• field: Solves goals consisting of addition, subtraction (theadditive inverse), multiplication, and division (the multiplicative inverse).

• ; (semicolon): Applies the tactic on the right to all subgoalsproduced by the tactic on the left.
• try: Attempts to apply the given tactic but does not fail even if thegiven tactic fails.
• || (or): Tries to apply the tactic on the left; if that fails, triesto apply the tactic on the right.
• all:: Applies the given tactic to all remaining subgoals.
• repeat: Applies the given tactic repeatedly until it fails.

Solving simple goals

The following tactics prove simple goals. Generally, your aim when writing Coqproofs is to transform your goal until it can be solved using one of thesetactics.

assumption

If the goal is already in your context, you can use the assumption tactic toimmediately prove the goal.

Example:

After introducing the hypothesis P_holds (which says that P is true) intothe context, we can use assumption to complete the proof.

reflexivity

If the goal contains an equality that looks obviously true, the reflexivitytactic can finish off the proof, doing some basic simplification if needed.

Example:

Both the left and right sides of the equality in the goal are clearly equal(after simplification), so we use reflexivity.

trivial

The trivial tactic can solve a variety of simple goals. It introducesvariables and hypotheses into the context and then tries to use various othertactics under the hood to solve the goal.

Any goal that can be solved with assumption or reflexivity can also besolved using trivial.

Unlike most of the other tactics in this section, trivial will not fail evenif it cannot solve the goal.

Example:

Previously, we proved this theorem using intros and assumption; however,trivial can actually take care of both those steps in one fell swoop.

auto

The auto tactic is a more advanced version of trivial that performs a recursive proof search.

Any goal that can be solved with trivial can also be solved using auto.

Like trivial, auto never fails even if it cannot do anything.

Example:

This proof is too complicated for trivial to handle on its own, but it can besolved with auto!

discriminate

The discriminate tactic proves that different constructors of an inductivetype cannot be equal. In other words, if the goal is an inequality consistingof two different constructors, discriminate will solve the goal.

discriminate also has another use: if the context contains a equalitybetween two different constructors (i.e. a false assumption), you can usediscriminate to prove any goal.

Example 1:

You may be surprised to learn that auto cannot solve this simple goal! However, discriminate takes care of this proof easily.

Example 2:

Recall that the natural numbers in Coq are defined as an inductive type withconstructors O (zero) and S (successor of). The constructors on both sidesof the false equality 0 = 1 are different, so we can use discriminate toprove our goal that any proposition P holds.

exact

If you know the exact proof term that proves the goal, you can provide itdirectly using the exact tactic.

Example:

Suppose we know that eq_refl 42 is a term with the type 42 = 42. Then, weprove that there exists a value that inhabits this type by supplying the termdirectly using exact, which proves the theorem.

(We could have also used reflexivity or other tactics to prove this goal.)

contradiction

If there is a hypothesis that is equivalent to False or two contradictoryhypotheses in the context, you can use the contradiction tactic to prove anygoal.

Example:

After destructing the hypothesis P / ~P, we obtain two hypotheses P and~P that contradict each other, so we use contradiction to complete theproof.

Transforming goals

While proving a theorem, you will typically need to transform your goalto introduce assumptions into the context, simplify the goal, make use ofassumptions, and so on. The following tactics allow you to make progress towardsolving a goal.

intros / intro

If there are universally quantified variables in the goal (i.e. forall), youcan introduce those variables into the context using the intros tactic. Youcan also use intros to introduce all propositions on the left side of an implication as assumptions.

If intros is used by itself, Coq will introduce all the variables andhypotheses that it can, and it will assign names to them automatically. You canprovide your own names (or introduce fewer things) by supplying those names inorder. See Example 2.

intros also has a sister tactic intro that introduces just one thing.

intros used by itself will never fail, even if there’s nothing to introduce.If you supply some names to intros, however, it will fail if a name isalready in use or if there’s not enough stuff left to introduce.

Example 1:

We can introduce the two variables P and Q, as well as the two hypotheses(P -> Q) and ~Q using intros.

Example 2:

The names that Coq chose for the hypotheses H and H0 aren’t very descriptive. We can provide more descriptive names instead. Note that we alsohave to give names to the two variables after the forall because introsintroduces things in order.

simpl

The simpl tactic reduces complex terms to simpler forms. You’ll find thatit’s not always necessary to use simpl because other tactics (e.g. discriminate) can do the simplification themselves, but it’s often helpful totry simpl to help you figure out what you, as the writer of the proof,should do next.

You can also use simpl on a hypothesis in the context with the syntaxsimpl in <hypothesis>.

simpl will never fail, even if no simplification can be done.

Example:

Let’s simplify that goal with simpl.

unfold

The unfold tactic replaces a defined term in the goal with its definition.

You can also use unfold on a hypothesis in the context with the syntaxunfold <term> in <hypothesis>.

Example 1:

This time, nothing happens if we try simpl. However, we can unfold and transform the goal into something that we can then simplify.

Example 2:

We’d like to unfold the ~(P / Q) in our context as well, so we use unfold..in...

(In thie case, we could have also applied unfold before intros to unfoldall the negations at once.)

apply

The apply tactic has a variety of uses.

If your goal is some proposition B and you know that A -> B, then in orderto prove that B holds, it suffices to show A holds. apply uses thisreasoning to transform the goal from B to A. See Example 1.

apply can also be used on hypotheses. If you have some hypothesis that statesthat A holds, as well as another hypothesis A -> B, you can use apply totransform the first hypothesis into B. The syntax is apply <term> in <hypothesis> or apply <term> in <hypothesis> as <new-hypothesis>. See Example 2.

You can even apply previously proven theorems. See Example 3.

Example 1:

Since we know that P -> Q, proving that P holds would also prove that Q holds. Therefore, we use apply to transform our goal.

Example 2:

Alternatively, we notice that P holds in our context, and because we knowthat P -> Q, we can apply that implication to our hypothesis that P holdsto transform it.

Note that this replaces our previous hypothesis (and now its name is no longer very applicable)! To prevent this, we can give our new hypothesis its ownname using the apply..in..as.. syntax.

Example 3:

We notice that our goal is just an instance of P -> (P -> Q) -> Q, whichwe already proved is true. Therefore, we can use apply to apply our lemma,which finishes the proof.

rewrite

Given some known equality a = b, the rewrite tactic lets you replace awith b or vice versa in a goal or hypothesis

The syntax is rewrite -> <equality> to replace a with b in the goal orrewrite <- <equality> to replace b with a. Note that rewrite <equality> is identical to rewrite -> <equality>.

You can also rewrite terms in hypotheses with the rewrite..in.. syntax.

Example:

We can try using auto to see if Coq can figure out the rest of the proof forus, but it can’t because it doesn’t know that addition is commutative (that’swhat we’re trying to prove!).

However, we can apply our inductive hypothesis x + y = y + x by rewritingthe x + y in the goal as y + x using rewrite:

Now you can finish the proof by simply using trivial or auto.

inversion

Suppose you have a hypothesis S m = S n, where m and n are nats. Theinversion tactic allows you to conclude that m = n. In general, if youhave a hypothesis that states an equality between two constructors andthe constructors are the same, inversion helps you figure out that allthe arguments to those constructors must be equal as well, and it triesto rewrite the goal using that information.

Example:

Since S x = S y, we use inversion to extract a new hypothesis that statesx = y. inversion actually goes one step further and rewrites the goalusing that equality.

left / right

If the goal is a disjunction A / B, the left tactic replaces the goalwith the left side of the disjunction A, and the right tactic replacesthe goal with the right side B.

Example 1:

Since we know that P holds, it makes sense to change the goal to the leftside of the disjunction using left.

Example 2:

This time, we know that Q holds, so we replace the goal with its rightside using right.

replace

The replace tactic allows you to replace a term in the goal with anotherterm and produces a new subgoal that asks you to prove that those two terms areequal. The syntax is replace <term> with <term>.

Example:

We believe that x + 1 and S x are equal, so we can use replace to assertthat this equality is true and then prove it later.

Breaking apart goals and hypotheses

The following tactics break apart goals (or hypotheses) into several simplersubgoals (or hypotheses).

split

If the goal is a conjunction A / B, the split tactic replaces the goalwith two subgoals A and B.

Example:

In order to make progress in the proof, we use split to break up Q / R into two subgoals.

destruct (and / or)

If there is a hypothesis containing a conjunction or a disjunction in thecontext, you can use the destruct tactic to break them apart.

A hypothesis A / B means that both A and B hold, so it can be destructedinto two new hypotheses A and B. You can also use the destruct..as [...]syntax to give your own name to these new hypotheses. See Example 1.

On the other hand, a hypothesis A / B means that at least one of A and Bholds, so in order to make use of this hypothesis, you must prove that the goalholds when A is true (and B may not be) and when B is true (and A maynot be). You can also use the destruct..as [... | ...] syntax to provideyour own names to the hypotheses that are generated (note the presence of thethe vertical bar). See Example 2.

Example 1:

Since there’s a conjunction P / Q in our context, using destruct on itwill give us both P and Q as separate hypotheses.

The names that Coq chose for the new hypotheses aren’t very descriptive, solet’s provide our own.

Example 2:

We can destruct the hypothesis P / Q to replace our current goal with twonew subgoals P / Q with different contexts: one in which P holds and onein which Q holds.

After we’ve proven the first subgoal, we observe that, in the context for the second subgoal, we have the hypothesis that Q holds instead.

destruct (case analysis)

The destruct tactic can also be used for more general case analysis by destructing on a term or variable whose type is an inductive type.

Example:

In order to proceed with this proof, we need to prove that it holds for eachconstructor of element case-by-case, so we use destruct.

induction

Using the induction tactic is the same as using the destruct tactic, exceptthat it also introduces induction hypotheses as appropriate.

Once again, you can use the induction..as [...] syntax to give names to theterms and hypotheses produced in the different cases.

See lecture, notes, and lab 22 for more on induction.

Example:

The base case 0 doesn’t produce anything new, so we don’t need to provide anynames there. The inductive case S x produces a new term x and a newhypothesis, so we give those names. The vertical bar separates the two cases.

After proving the base case, we move on to the inductive case. Hey, Coq cameup with the correct induction hypothesis for us. Thanks, Coq!

From here, we can make use of the induction hypothesis with rewrite and thenapply auto to knock out the rest of the proof.

Solving specific types of goals

The tactics in this section are automated tactics that are specialized forsolving certain types of goals.

ring

The ring tactic can solve any goal that contains only addition andmultiplication operations.

You must first use the command Require Import Arith. in order to use ring.

Example:

It would be pretty painful to prove this using simpler tactics, but fortunatelyring is here to save the day.

tauto

The tauto tactic can solve any goal that’s a tautology (in constructive logic). A tautology is a logical formula that’s always true, regardless of thevalues of the variables in it.

Example:

DeMorgan’s law is a tautology, so it can be proven by applying tauto.

field

The field tactic can solve any goal that contains addition, subtraction(the additive inverse), multiplication, and division (the multiplicativeinverse).

Note that field cannot be used on the natural numbers or integers, becauseinteger division is not the inverse of multiplication (e.g. (1 / 2) * 2 doesnot equal 1).

You must first use the command Require Import Field. in order to use field.

See lecture notes 22 for more information on field.

Tacticals

The following tacticals are “higher-order tactics” that operate on tactics.

; (semicolon)

The ; tactical applies the tactic on the right side of the semicolon to allthe subgoals produced by tactic on the left side.

Example:

The two subgoals generated by split were solved using the same tactic. We canuse ; to make the code more concise.

try

Many tactics will fail if they are not applicable. The try tactical lets youattempt to use a tactic and allows the tactic to go through even if itfails. This can be particularly useful when chaining tactics together using;.

Example:

We’d like to use discriminate to take care of the second and third subgoals,but we can’t simply write destruct e; discriminate. because discriminatewill fail when Coq tries to apply it to the first subgoal. This is where thetry tactic comes in handy.

|| (or)

The || tactical first tries the tactic on the left side; if it fails, then itapplies the tactic on the right side.

Example:

Let’s use this theorem from the last section again. discriminate took careof the other two subgoals, and we know that trivial can solve this one. Inother words, we apply either discriminate or trivial to the subgoals generated by destruct e, so we can use || to shorten the proof.

all:

The all: tactical applies a tactic to all the remaining subgoals in the proof.

Example:

An alternative proof for the previous theorem using all:.

repeat

The repeat tactical repeatedly applies a tactic until it fails.

Note that repeat will never fail, even if it applies the given tactic zero times.

Example:

Coq Tactic

Coq provides a theorem Nat.add_assoc : forall n m p : nat, n + (m + p) = n + m + pin the Arith library that we can make use of two times for this proof.

Coq Cheat Sheet Template

Acknowledgement: Inspired by the Coq Tactic Index by JosephRedmon.