<**
- [assumption](#assumption): Solves the goal if it is already assumed in the
context.
- [reflexivity](#reflexivity): Solves the goal if it is a trivial equality.
- [trivial](#trivial): Solves a variety of easy goals.
- [auto](#auto): Solves a greater variety of easy goals.
- [discriminate](#discriminate): Solves the goal if it is a trivial inequality
and solves any goal if the context contains a false equality.
- [exact](#exact): Solves a goal if you know the exact proof term that proves
the goal.
- [contradiction](#contradiction): Solves any goal if the context contains
`False` or contradictory hypotheses.
**[Transforming goals:](#transform)**
- [intros / intro](#intros): Introduces variables appearing with `forall`
as well as the premises (left-hand side) of implications.
- [simpl](#simpl): Simplifies the goal or hypotheses in the context.
- [unfold](#unfold): Unfolds the definitions of terms.
- [apply](#apply): Uses implications to transform goals and hypotheses.
- [rewrite](#rewrite): Replaces a term with an equivalent term if the
equivalence of the terms has already been proven.
- [inversion](#inversion): Deduces equalities that must be true given an
equality between two constructors.
- [left / right](#leftright): Replaces a goal consisting of a disjunction
`P \/ Q` with just `P` or `Q`.
- [replace](#replace): Replace a term with a equivalent term and generates a
subgoal to prove that the equality holds.
**[Breaking apart goals and hypotheses:](#breakapart)**
- [split](#split): Replaces a goal consisting of a conjunction `P /\ Q` with
two subgoals `P` and `Q`.
- [destruct (and/or)](#destructandor): Replaces a hypothesis `P /\ Q` with two
hypotheses `P` and `Q`. Alternatively, if the hypothesis is a disjunction
`P \/ Q`, generates two subgoals, one where `P` holds and one where `Q` holds.
- [destruct (case analysis)](#destructcase): Generates a subgoal for every
constructor of an inductive type.
- [induction](#induction): Generates a subgoal for every constructor of an
inductive type and provides an induction hypothesis for recursively defined
constructors.
**[Solving specific types of goals:](#specificgoals)**
- [ring](#ring): Solves goals consisting of addition and multiplication
operations.
- [tauto](#tauto): Solves goals consisting of tautologies that hold in
constructive logic.
- [field](#field): Solves goals consisting of addition, subtraction (the
additive inverse), multiplication, and division (the multiplicative inverse).
**[Tacticals (tactics that act on other tactics):](#tacticals)**
- [; (semicolon)](#semicolon): Applies the tactic on the right to all subgoals
produced by the tactic on the left.
- [try](#try): Attempts to apply the given tactic but does not fail even if the
given tactic fails.
- [|| (or)](#or): Tries to apply the tactic on the left; if that fails, tries
to apply the tactic on the right.
- [all:](#all): Applies the given tactic to all remaining subgoals.
- [repeat](#repeat): Applies the given tactic repeatedly until it fails.
<br>
<a name="simplegoals"></a>
## Solving simple goals
The following tactics prove simple goals. Generally, your aim when writing Coq
proofs is to transform your goal until it can be solved using one of these
tactics.
<a name="assumption"></a>
### assumption
If the goal is already in your context, you can use the `assumption` tactic to
immediately prove the goal.
<!-- `assumption` will fail if it cannot prove the goal. -->
**Example:**
<pre class="example">
<code class="coq code">Theorem p_implies_p : forall P : Prop,
P -> P.
Proof.
intros P P_holds.
</code>
<div class="context">1 subgoal
P : Prop
P_holds : P
-------------------(1/1)
P
</div>
</pre>
After introducing the hypothesis `P_holds` (which says that `P` is true) into
the context, we can use `assumption` to complete the proof.
<pre class="example">
<code class="coq code">Theorem p_implies_p : forall P : Prop,
P -> P.
Proof.
intros P P_holds.
assumption.
</code>
<div class="context">No more subgoals.
</div>
</pre>
<br>
<br>
<a name="reflexivity"></a>
### reflexivity
If the goal contains an equality that looks obviously true, the `reflexivity`
tactic can finish off the proof, doing some basic simplification if needed.
<!-- `reflexivity` will fail if it cannot prove the goal. -->
**Example:**
<pre class="example">
<code class="coq code">Theorem forty_two : 41 + 1 = 42.
Proof.
</code>
<div class="context">1 subgoal
-------------------(1/1)
41 + 1 = 42
</div>
</pre>
Both the left and right sides of the equality in the goal are clearly equal
(after simplification), so we use `reflexivity`.
<pre class="example">
<code class="coq code">Theorem forty_two : 41 + 1 = 42.
Proof.
reflexivity.
</code>
<div class="context">No more subgoals.
</div>
</pre>
<br>
<br>
<a name="trivial"></a>
### trivial
The `trivial` tactic can solve a variety of simple goals. It introduces
variables and hypotheses into the context and then tries to use various other
tactics under the hood to solve the goal.
Any goal that can be solved with `assumption` or `reflexivity` can also be
solved using `trivial`.
Unlike most of the other tactics in this section, `trivial` will not fail even
if it cannot solve the goal.
**Example:**
<pre class="example">
<code class="coq code">Theorem p_implies_p : forall P : Prop,
P -> P.
Proof.
</code>
<div class="context">1 subgoal
-------------------(1/1)
P -> P
</div>
</pre>
Previously, we proved this theorem using `intros` and `assumption`; however,
`trivial` can actually take care of both those steps in one fell swoop.
<pre class="example">
<code class="coq code">Theorem p_implies_p : forall P : Prop,
P -> P.
Proof.
trivial.
</code>
<div class="context">No more subgoals.
</div>
</pre>
<br>
<br>
<a name="auto"></a>
### 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:**
<pre class="example">
<code class="coq code">Theorem modus_tollens: forall (P Q : Prop),
(P -> Q) -> ~Q -> ~P.
Proof.
</code>
<div class="context">1 subgoal
-------------------(1/1)
forall P Q : Prop, (P -> Q) -> ~ Q -> ~ P
</div>
</pre>
This proof is too complicated for `trivial` to handle on its own, but it can be
solved with `auto`!
<pre class="example">
<code class="coq code">Theorem modus_tollens: forall (P Q : Prop),
(P -> Q) -> ~Q -> ~P.
Proof.
auto.
</code>
<div class="context">No more subgoals.
</div>
</pre>
<br>
<br>
<a name="discriminate"></a>
### discriminate
The `discriminate` tactic proves that different constructors of an inductive
type cannot be equal. In other words, if the goal is an inequality consisting
of two different constructors, `discriminate` will solve the goal.
`discriminate` also has another use: if the context contains a equality
between two different constructors (i.e. a false assumption), you can use
`discriminate` to prove any goal.
<!-- `discriminate` will fail if it cannot prove the goal. -->
**Example 1:**
<pre class="example">
<code class="coq code">Inductive element :=
| grass : element
| fire : element
| water : element.
Theorem fire_is_not_water : fire <> water.
Proof.
</code>
<div class="context">1 subgoal
-------------------(1/1)
fire <> water
</div>
</pre>
You may be surprised to learn that `auto` cannot solve this simple goal!
However, `discriminate` takes care of this proof easily.
<pre class="example">
<code class="coq code">Inductive element :=
| grass : element
| fire : element
| water : element.
Theorem fire_is_not_water : fire <> water.
Proof.
discriminate.
</code>
<div class="context">No more subgoals.
</div>
</pre>
**Example 2:**
<pre class="example">
<code class="coq code">Theorem false_implies_anything : forall P : Prop,
0 = 1 -> P.
Proof.
intros P zero_equals_one.
</code>
<div class="context">1 subgoal
P : Prop
zero_equals_one : 0 = 1
-------------------(1/1)
P
</div>
</pre>
Recall that the natural numbers in Coq are defined as an inductive type with
constructors `O` (zero) and `S` (successor of). The constructors on both sides
of the false equality `0 = 1` are different, so we can use `discriminate` to
prove our goal that any proposition `P` holds.
<pre class="example">
<code class="coq code">Theorem false_implies_anything : forall P : Prop,
0 = 1 -> P.
Proof.
intros P zero_equals_one.
discriminate.
</code>
<div class="context">No more subgoals.
</div>
</pre>
<br>
<br>
<a name="exact"></a>
### exact
If you know the exact proof term that proves the goal, you can provide it
directly using the `exact` tactic.
<!-- `exact` will fail if it cannot prove the goal. -->
**Example:**
<pre class="example">
<code class="coq code">Theorem everything : 42 = 42.
Proof.
</code>
<div class="context">1 subgoal
-------------------(1/1)
42 = 42
</div>
</pre>
Suppose we know that `eq_refl 42` is a term with the type `42 = 42`. Then, we
prove that there exists a value that inhabits this type by supplying the term
directly using `exact`, which proves the theorem.
(We could have also used `reflexivity` or other tactics to prove this goal.)
<pre class="example">
<code class="coq code">Theorem everything : 42 = 42.
Proof.
exact (eq_refl 42).
</code>
<div class="context">No more subgoals.
</div>
</pre>
<br>
<br>
<a name="contradiction"></a>
### contradiction
If there is a hypothesis that is equivalent to `False` or two contradictory
hypotheses in the context, you can use the `contradiction` tactic to prove any
goal.
<!-- `contradiction` will fail if it cannot find the appropriate hypotheses in the
context. -->
**Example:**
<pre class="example">
<code class="coq code">Theorem law_of_contradiction : forall (P Q : Prop),
P /\ ~P -> Q.
Proof.
intros P Q P_and_not_P.
destruct P_and_not_P as [P_holds not_P].
</code>
<div class="context">1 subgoal
P, Q : Prop
P_holds : P
not_P : ~ P
-------------------(1/1)
Q
</div>
</pre>
After destructing the hypothesis `P /\ ~P`, we obtain two hypotheses `P` and
`~P` that contradict each other, so we use `contradiction` to complete the
proof.
<pre class="example">
<code class="coq code">Theorem law_of_contradiction : forall (P Q : Prop),
P /\ ~P -> Q.
Proof.
intros P Q P_and_not_P.
destruct P_and_not_P as [P_holds not_P].
contradiction.
</code>
<div class="context">No more subgoals.
</div>
</pre>
<a name="transform"></a>
## Transforming goals
While proving a theorem, you will typically need to transform your goal
to introduce assumptions into the context, simplify the goal, make use of
assumptions, and so on. The following tactics allow you to make progress toward
solving a goal.
<a name="intros"></a>
### intros / intro
If there are universally quantified variables in the goal (i.e. `forall`), you
can introduce those variables into the context using the `intros` tactic. You
can 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 and
hypotheses that it can, and it will assign names to them automatically. You can
provide your own names (or introduce fewer things) by supplying those names in
order. 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 is
already in use or if there's not enough stuff left to introduce.
**Example 1:**
<pre class="example">
<code class="coq code">Theorem modus_tollens : forall (P Q : Prop),
(P -> Q) -> ~Q -> ~P.
Proof.
</code>
<div class="context">1 subgoal
-------------------(1/1)
forall P Q : Prop, (P -> Q) -> ~ Q -> ~ P
</div>
</pre>
We can introduce the two variables `P` and `Q`, as well as the two hypotheses
`(P -> Q)` and `~Q` using `intros`.
<pre class="example">
<code class="coq code">Theorem modus_tollens : forall (P Q : Prop),
(P -> Q) -> ~Q -> ~P.
Proof.
intros.
</code>
<div class="context">1 subgoal
P, Q : Prop
H : P -> Q
H0 : ~ Q
-------------------(1/1)
~ P
</div>
</pre>
**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 also
have to give names to the two variables after the `forall` because `intros`
introduces things in order.
<pre class="example">
<code class="coq code">Theorem modus_tollens : forall (P Q : Prop),
(P -> Q) -> ~Q -> ~P.
Proof.
intros P Q P_implies_Q not_Q.
</code>
<div class="context">1 subgoal
P, Q : Prop
P_implies_Q : P -> Q
not_Q : ~ Q
-------------------(1/1)
~ P
</div>
</pre>
<br>
<br>
<a name="simpl"></a>
### simpl
The `simpl` tactic reduces complex terms to simpler forms. You'll find that
it's not always necessary to use `simpl` because other tactics (e.g.
`discriminate`) can do the simplification themselves, but it's often helpful to
try `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 syntax
`simpl in <hypothesis>`.
`simpl` will never fail, even if no simplification can be done.
**Example:**
<pre class="example">
<code class="coq code">Theorem switch_to_honors : 2110 + 2 = 2112.
Proof.
</code>
<div class="context">1 subgoal
-------------------(1/1)
2110 + 2 = 2112
</div>
</pre>
Let's simplify that goal with `simpl`.
<pre class="example">
<code class="coq code">Theorem switch_to_honors : 2110 + 2 = 2112.
Proof.
simpl.
</code>
<div class="context">1 subgoal
-------------------(1/1)
2112 = 2112
</div>
</pre>
<br>
<br>
<a name="unfold"></a>
### 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 syntax
`unfold <term> in <hypothesis>`.
<!-- `unfold <term>` will fail if the term does not have a corresponding
definition. -->
**Example 1:**
<pre class="example">
<code class="coq code">Definition plus_two (x : nat) : nat :=
x + 2.
Theorem switch_to_honors_again :
plus_two 2110 = 2112.
Proof.
</code>
<div class="context">1 subgoal
-------------------(1/1)
plus_two 2110 = 2112
</div>
</pre>
This time, nothing happens if we try `simpl`. However, we can `unfold` and
transform the goal into something that we can then simplify.
<pre class="example">
<code class="coq code">Theorem switch_to_honors_again :
plus_two 2110 = 2112.
Proof.
unfold plus_two.
</code>
<div class="context">1 subgoal
-------------------(1/1)
2110 + 2 = 2112
</div>
</pre>
**Example 2:**
<pre class="example">
<code class="coq code">Theorem demorgan : forall (P Q : Prop),
~(P \/ Q) -> ~P /\ ~Q.
Proof.
intros P Q not_P_or_Q.
unfold not.
</code>
<div class="context">1 subgoal
P, Q : Prop
not_P_or_Q : ~ (P \/ Q)
-------------------(1/1)
(P -> False) /\ (Q -> False)
</div>
</pre>
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 unfold
all the negations at once.)
<pre class="example">
<code class="coq code">Theorem demorgan : forall (P Q : Prop),
~(P \/ Q) -> ~P /\ ~Q.
Proof.
intros P Q not_P_or_Q.
unfold not.
unfold not in not_P_or_Q.
</code>
<div class="context">1 subgoal
P, Q : Prop
not_P_or_Q : P \/ Q -> False
-------------------(1/1)
(P -> False) /\ (Q -> False)
</div>
</pre>
<br>
<br>
<a name="apply"></a>
### apply
The `apply` tactic has a variety of uses.
If your goal is some proposition `B` and you know that `A -> B`, then in order
to prove that `B` holds, it suffices to show `A` holds. `apply` uses this
reasoning to transform the goal from `B` to `A`. See Example 1.
`apply` can also be used on hypotheses. If you have some hypothesis that states
that `A` holds, as well as another hypothesis `A -> B`, you can use `apply` to
transform 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.
<!-- `apply` will fail if Coq cannot figure out a way to match the given term with
the goal or hypothesis. -->
**Example 1:**
<pre class="example">
<code class="coq code">Theorem modus_ponens : forall (P Q : Prop),
(P -> Q) -> P -> Q.
Proof.
intros P Q P_implies_Q P_holds.
</code>
<div class="context">1 subgoal
P, Q : Prop
P_implies_Q : P -> Q
P_holds : P
-------------------(1/1)
Q
</div>
</pre>
Since we know that `P -> Q`, proving that `P` holds would also prove that
`Q` holds. Therefore, we use `apply` to transform our goal.
<pre class="example">
<code class="coq code">Theorem modus_ponens : forall (P Q : Prop),
(P -> Q) -> P -> Q.
Proof.
intros P Q P_implies_Q P_holds.
apply P_implies_Q.
</code>
<div class="context">1 subgoal
P, Q : Prop
P_implies_Q : P -> Q
P_holds : P
-------------------(1/1)
P
</div>
</pre>
**Example 2:**
Alternatively, we notice that `P` holds in our context, and because we know
that `P -> Q`, we can apply that implication to our hypothesis that `P` holds
to transform it.
<pre class="example">
<code class="coq code">Theorem modus_ponens : forall (P Q : Prop),
(P -> Q) -> P -> Q.
Proof.
intros P Q P_implies_Q P_holds.
apply P_implies_Q in P_holds.
</code>
<div class="context">1 subgoal
P, Q : Prop
P_implies_Q : P -> Q
P_holds : Q
-------------------(1/1)
P
</div>
</pre>
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 own
name using the `apply..in..as..` syntax.
<pre class="example">
<code class="coq code">Theorem modus_ponens : forall (P Q : Prop),
(P -> Q) -> P -> Q.
Proof.
intros P Q P_implies_Q P_holds.
apply P_implies_Q in P_holds as Q_holds.
</code>
<div class="context">1 subgoal
P, Q : Prop
P_implies_Q : P -> Q
P_holds : P
Q_holds : Q
-------------------(1/1)
P
</div>
</pre>
**Example 3:**
<pre class="example">
<code class="coq code">Lemma modus_ponens'' : forall (P Q : Prop),
P -> (P -> Q) -> Q.
Proof.
auto.
Qed.
Theorem double_negation : forall (P : Prop),
P -> ~~P.
Proof.
unfold not. intro P.
</code>
<div class="context">1 subgoal
P : Prop
-------------------(1/1)
P -> (P -> False) -> False
</div>
</pre>
We notice that our goal is just an instance of `P -> (P -> Q) -> Q`, which
we already proved is true. Therefore, we can use `apply` to apply our lemma,
which finishes the proof.
<pre class="example">
<code class="coq code">Lemma modus_ponens'' : forall (P Q : Prop),
P -> (P -> Q) -> Q.
Proof.
auto.
Qed.
Theorem double_negation : forall (P : Prop),
P -> ~~P.
Proof.
unfold not. intro P.
apply modus_ponens''.
</code>
<div class="context">No more subgoals.
</div>
</pre>
<br>
<br>
<a name="rewrite"></a>
### rewrite
Given some known equality `a = b`, the `rewrite` tactic lets you replace `a`
with `b` or vice versa in a goal or hypothesis
The syntax is `rewrite -> <equality>` to replace `a` with `b` in the goal or
`rewrite <- <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.
<!-- `rewrite` will fail if there's no applicable term to rewrite. -->
**Example:**
<pre class="example">
<code class="coq code">Theorem add_comm : forall (x y : nat),
x + y = y + x.
Proof.
intros. induction x.
- trivial.
- simpl.
</code>
<div class="context">1 subgoal
x, y : nat
IHx : x + y = y + x
-------------------(1/1)
S (x + y) = y + S x
</div>
</pre>
We can try using `auto` to see if Coq can figure out the rest of the proof for
us, but it can't because it doesn't know that addition is commutative (that's
what we're trying to prove!).
However, we can apply our inductive hypothesis `x + y = y + x` by rewriting
the `x + y` in the goal as `y + x` using `rewrite`:
<pre class="example">
<code class="coq code">Theorem add_comm : forall (x y : nat),
x + y = y + x.
Proof.
intros. induction x.
- trivial.
- simpl. rewrite -> IHx.
</code>
<div class="context">1 subgoal
x, y : nat
IHx : x + y = y + x
-------------------(1/1)
S (y + x) = y + S x
</div>
</pre>
Now you can finish the proof by simply using `trivial` or `auto`.
<br>
<br>
<a name="inversion"></a>
### inversion
Suppose you have a hypothesis `S m = S n`, where `m` and `n` are `nats`. The
`inversion` tactic allows you to conclude that `m = n`. In general, if you
have a hypothesis that states an equality between two constructors and
the constructors are the same, `inversion` helps you figure out that all
the arguments to those constructors must be equal as well, and it tries
to rewrite the goal using that information.
**Example:**
<pre class="example">
<code class="coq code">Theorem succ_eq_implies_eq : forall (x y : nat),
S x = S y -> x = y.
Proof.
intros x y succ_eq.
</code>
<div class="context">1 subgoal
x, y : nat
succ_eq : S x = S y
-------------------(1/1)
x = y
</div>
</pre>
Since `S x = S y`, we use `inversion` to extract a new hypothesis that states
`x = y`. `inversion` actually goes one step further and rewrites the goal
using that equality.
<pre class="example">
<code class="coq code">Theorem succ_eq_implies_eq : forall (x y : nat),
S x = S y -> x = y.
Proof.
intros x y succ_eq.
inversion succ_eq.
</code>
<div class="context">1 subgoal
x, y : nat
succ_eq : S x = S y
H0 : x = y
-------------------(1/1)
y = y
</div>
</pre>
<br>
<br>
<a name="leftright"></a>
### left / right
If the goal is a disjunction `A \/ B`, the `left` tactic replaces the goal
with the left side of the disjunction `A`, and the `right` tactic replaces
the goal with the right side `B`.
<!-- `left` and `right` will fail if the goal is not a disjunction. -->
**Example 1:**
<pre class="example">
<code class="coq code">Theorem or_left : forall (P Q : Prop),
P -> P \/ Q.
Proof.
intros P Q P_holds.
</code>
<div class="context">1 subgoal
P, Q : Prop
P_holds : P
-------------------(1/1)
P \/ Q
</div>
</pre>
Since we know that `P` holds, it makes sense to change the goal to the left
side of the disjunction using `left`.
<pre class="example">
<code class="coq code">Theorem or_left : forall (P Q : Prop),
P -> P \/ Q.
Proof.
intros P Q P_holds.
left.
</code>
<div class="context">1 subgoal
P, Q : Prop
P_holds : P
-------------------(1/1)
P
</div>
</pre>
**Example 2:**
<pre class="example">
<code class="coq code">Theorem or_right : forall (P Q : Prop),
Q -> P \/ Q.
Proof.
intros P Q Q_holds.
</code>
<div class="context">1 subgoal
P, Q : Prop
Q_holds : Q
-------------------(1/1)
P \/ Q
</div>
</pre>
This time, we know that `Q` holds, so we replace the goal with its right
side using `right`.
<pre class="example">
<code class="coq code">Theorem or_right : forall (P Q : Prop),
Q -> P \/ Q.
Proof.
intros P Q Q_holds.
right.
</code>
<div class="context">1 subgoal
P, Q : Prop
Q_holds : Q
-------------------(1/1)
Q
</div>
</pre>
<br>
<br>
<a name="replace"></a>
### replace
The `replace` tactic allows you to replace a term in the goal with another
term and produces a new subgoal that asks you to prove that those two terms are
equal. The syntax is `replace <term> with <term>`.
**Example:**
<pre class="example">
<code class="coq code">Theorem one_x_one : forall (x : nat),
1 + x + 1 = 2 + x.
Proof.
intro. simpl.
</code>
<div class="context">1 subgoal
x : nat
-------------------(1/1)
S (x + 1) = S (S x)
</div>
</pre>
We believe that `x + 1` and `S x` are equal, so we can use `replace` to assert
that this equality is true and then prove it later.
<pre class="example">
<code class="coq code">Theorem one_x_one : forall (x : nat),
1 + x + 1 = 2 + x.
Proof.
intro. simpl.
replace (x + 1) with (S x).
</code>
<div class="context">2 subgoals
x : nat
-------------------(1/2)
S (S x) = S (S x)
-------------------(2/2)
S x = x + 1
</div>
</pre>
<br>
<br>
<a name="breakapart"></a>
## Breaking apart goals and hypotheses
The following tactics break apart goals (or hypotheses) into several simpler
subgoals (or hypotheses).
<a name="split"></a>
### split
If the goal is a conjunction `A /\ B`, the `split` tactic replaces the goal
with two subgoals `A` and `B`.
<!-- `split` will fail if the goal is not a conjunction. -->
**Example:**
<pre class="example">
<code class="coq code">Theorem implies_and : forall (P Q R : Prop),
P -> (P -> Q) -> (P -> R) -> (Q /\ R).
Proof.
intros P Q R P_holds.
intros P_implies_Q P_implies_R.
</code>
<div class="context">1 subgoal
P, Q, R : Prop
P_holds : P
P_implies_Q : P -> Q
P_implies_R : P -> R
-------------------(1/1)
Q /\ R
</div>
</pre>
In order to make progress in the proof, we use `split` to break up
`Q /\ R` into two subgoals.
<pre class="example">
<code class="coq code">Theorem implies_and : forall (P Q R : Prop),
P -> (P -> Q) -> (P -> R) -> (Q /\ R).
Proof.
intros P Q R P_holds.
intros P_implies_Q P_implies_R.
split.
</code>
<div class="context">2 subgoals
P, Q, R : Prop
P_holds : P
P_implies_Q : P -> Q
P_implies_R : P -> R
-------------------(1/2)
Q
-------------------(2/2)
R
</div>
</pre>
<br>
<br>
<a name="destructandor"></a>
### destruct (and / or)
If there is a hypothesis containing a conjunction or a disjunction in the
context, 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 destructed
into 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 `B`
holds, so in order to make use of this hypothesis, you must prove that the goal
holds when `A` is true (and `B` may not be) and when `B` is true (and `A` may
not be). You can also use the `destruct..as [... | ...]` syntax to provide
your own names to the hypotheses that are generated (note the presence of the
the vertical bar). See Example 2.
**Example 1:**
<pre class="example">
<code class="coq code">Theorem and_left : forall (P Q : Prop),
(P /\ Q) -> P.
Proof.
intros P Q P_and_Q.
</code>
<div class="context">1 subgoal
P, Q : Prop
P_and_Q : P /\ Q
-------------------(1/1)
P
</div>
</pre>
Since there's a conjunction `P /\ Q` in our context, using `destruct` on it
will give us both `P` and `Q` as separate hypotheses.
<pre class="example">
<code class="coq code">Theorem and_left : forall (P Q : Prop),
(P /\ Q) -> P.
Proof.
intros P Q P_and_Q.
destruct P_and_Q.
</code>
<div class="context">1 subgoal
P, Q : Prop
H : P
H0 : Q
-------------------(1/1)
P
</div>
</pre>
The names that Coq chose for the new hypotheses aren't very descriptive, so
let's provide our own.
<pre class="example">
<code class="coq code">Theorem and_left : forall (P Q : Prop),
(P /\ Q) -> P.
Proof.
intros P Q P_and_Q.
destruct P_and_Q as [P_holds Q_holds].
</code>
<div class="context">1 subgoal
P, Q : Prop
P_holds : P
Q_holds : Q
-------------------(1/1)
P
</div>
</pre>
**Example 2:**
<pre class="example">
<code class="coq code">Theorem or_comm : forall (P Q : Prop),
P \/ Q -> Q \/ P.
Proof.
intros P Q P_or_Q.
</code>
<div class="context">1 subgoal
P, Q : Prop
P_or_Q : P \/ Q
-------------------(1/1)
Q \/ P
</div>
</pre>
We can `destruct` the hypothesis `P \/ Q` to replace our current goal with two
new subgoals `P \/ Q` with different contexts: one in which `P` holds and one
in which `Q` holds.
<pre class="example">
<code class="coq code">Theorem or_comm : forall (P Q : Prop),
P \/ Q -> Q \/ P.
Proof.
intros P Q P_or_Q.
destruct P_or_Q as [P_holds | Q_holds].
</code>
<div class="context">2 subgoals
P, Q : Prop
P_holds : P
-------------------(1/2)
Q \/ P
-------------------(2/2)
Q \/ P
</div>
</pre>
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.
<pre class="example">
<code class="coq code">Theorem or_comm : forall (P Q : Prop),
P \/ Q -> Q \/ P.
Proof.
intros P Q P_or_Q.
destruct P_or_Q as [P_holds | Q_holds].
- right. assumption.
-
</code>
<div class="context">1 subgoal
P, Q : Prop
Q_holds : Q
-------------------(1/1)
Q \/ P
</div>
</pre>
<br>
<br>
<a name="destructcase"></a>
### 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:**
<pre class="example">
<code class="coq code">Inductive element :=
| grass : element
| fire : element
| water : element.
Definition weakness (e : element) : element :=
match e with
| grass => fire
| fire => water
| water => grass
end.
Theorem never_weak_to_self : forall (e : element),
weakness e <> e.
Proof.
</code>
<div class="context">1 subgoal
-------------------(1/1)
forall e : element, weakness e <> e
</div>
</pre>
In order to proceed with this proof, we need to prove that it holds for each
constructor of `element` case-by-case, so we use `destruct`.
<pre class="example">
<code class="coq code">Theorem never_weak_to_self : forall (e : element),
weakness e <> e.
Proof.
destruct e.
</code>
<div class="context">3 subgoals
-------------------(1/3)
weakness grass <> grass
-------------------(2/3)
weakness fire <> fire
-------------------(3/3)
weakness water <> water
</div>
</pre>
<br>
<br>
<a name="induction"></a>
### induction
Using the `induction` tactic is the same as using the `destruct` tactic, except
that it also introduces induction hypotheses as appropriate.
Once again, you can use the `induction..as [...]` syntax to give names to the
terms and hypotheses produced in the different cases.
See lecture, notes, and lab 22 for more on induction.
**Example:**
<pre class="example">
<code class="coq code">Theorem n_plus_n : forall (n : nat),
n + n = n * 2.
Proof.
induction n as [| x IH].
</code>
<div class="context">2 subgoals
-------------------(1/2)
0 + 0 = 0 * 2
-------------------(2/2)
S x + S x = S x * 2
</div>
</pre>
The base case `0` doesn't produce anything new, so we don't need to provide any
names there. The inductive case `S x` produces a new term `x` and a new
hypothesis, 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 came
up with the correct induction hypothesis for us. Thanks, Coq!
<pre class="example">
<code class="coq code">Theorem n_plus_n : forall (n : nat),
n + n = n * 2.
Proof.
induction n as [| x IH].
- reflexivity.
- simpl.
</code>
<div class="context">1 subgoal
x : nat
IH : x + x = x * 2
-------------------(1/1)
S (x + S x) = S (S (x * 2))
</div>
</pre>
From here, we can make use of the induction hypothesis with `rewrite` and then
apply `auto` to knock out the rest of the proof.
<pre class="example">
<code class="coq code">Theorem n_plus_n : forall (n : nat),
n + n = n * 2.
Proof.
induction n as [| x IH].
- reflexivity.
- simpl. rewrite <- IH. auto.
</code>
<div class="context">No more subgoals.
</div>
</pre>
<br>
<br>
<a name="specificgoals"></a>
## Solving specific types of goals
The tactics in this section are automated tactics that are specialized for
solving certain types of goals.
<a name="ring"></a>
### ring
The `ring` tactic can solve any goal that contains only addition and
multiplication operations.
You must first use the command `Require Import Arith.` in order to use `ring`.
**Example:**
<pre class="example">
<code class="coq code">Require Import Arith.
Theorem foil : forall a b c d,
(a + b) * (c + d) = a*c + b*c + a*d + b*d.
Proof.
intros. ring.
</code>
<div class="context">No more subgoals.
</div>
</pre>
It would be pretty painful to prove this using simpler tactics, but fortunately
`ring` is here to save the day.
<br>
<br>
<a name="tauto"></a>
### 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 the
values of the variables in it.
**Example:**
<pre class="example">
<code class="coq code">Theorem demorgan : forall (P Q : Prop),
~(P \/ Q) -> ~P /\ ~Q.
Proof.
tauto.
</code>
<div class="context">No more subgoals.
</div>
</pre>
DeMorgan's law is a tautology, so it can be proven by applying `tauto`.
<br>
<br>
<a name="field"></a>
### field
The `field` tactic can solve any goal that contains addition, subtraction
(the additive inverse), multiplication, and division (the multiplicative
inverse).
Note that `field` cannot be used on the natural numbers or integers, because
integer division is not the inverse of multiplication (e.g. `(1 / 2) * 2` does
not equal 1).
You must first use the command `Require Import Field.` in order to use `field`.
See [lecture notes 22][notes22] for more information on `field`.
[notes22]: http://www.cs.cornell.edu/courses/cs3110/2017fa/l/22-coq-induction/notes.v
<br>
<br>
<a name="tacticals"></a>
## Tacticals
The following *tacticals* are "higher-order tactics" that operate on tactics.
<a name="semicolon"></a>
### ; (semicolon)
The `;` tactical applies the tactic on the right side of the semicolon to all
the subgoals produced by tactic on the left side.
**Example:**
<pre class="example">
<code class="coq code">Theorem and_comm : forall (P Q : Prop),
P /\ Q -> Q /\ P.
Proof.
intros P Q P_and_Q.
destruct P_and_Q.
split.
- assumption.
- assumption.
Qed.
</code>
<div class="context">
</div>
</pre>
The two subgoals generated by `split` were solved using the same tactic. We can
use `;` to make the code more concise.
<pre class="example">
<code class="coq code">Theorem and_comm : forall (P Q : Prop),
P /\ Q -> Q /\ P.
Proof.
intros P Q P_and_Q.
destruct P_and_Q.
split; assumption.
Qed.
</code>
<div class="context">
</div>
</pre>
<br>
<br>
<a name="try"></a>
### try
Many tactics will fail if they are not applicable. The `try` tactical lets you
attempt to use a tactic and allows the tactic to go through even if it
fails. This can be particularly useful when chaining tactics together using
`;`.
**Example:**
<pre class="example">
<code class="coq code">Inductive element :=
| grass : element
| fire : element
| water : element.
Definition weakness (e : element) : element :=
match e with
| grass => fire
| fire => water
| water => grass
end.
Theorem fire_weak_implies_grass :
forall (e : element),
weakness e = fire -> e = grass.
Proof.
destruct e.
</code>
<div class="context">3 subgoals
-------------------(1/3)
weakness grass = fire -> grass = grass
-------------------(2/3)
weakness fire = fire -> fire = grass
-------------------(3/3)
weakness water = fire -> water = grass
</div>
</pre>
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 `discriminate`
will fail when Coq tries to apply it to the first subgoal. This is where the
`try` tactic comes in handy.
<pre class="example">
<code class="coq code">Theorem fire_weak_implies_grass :
forall (e : element),
weakness e = fire -> e = grass.
Proof.
destruct e; try discriminate.
</code>
<div class="context">1 subgoal
-------------------(1/1)
weakness grass = fire -> grass = grass
</div>
</pre>
<br>
<br>
<a name="or"></a>
### || (or)
The `||` tactical first tries the tactic on the left side; if it fails, then it
applies the tactic on the right side.
**Example:**
<pre class="example">
<code class="coq code">Theorem fire_weak_implies_grass :
forall (e : element),
weakness e = fire -> e = grass.
Proof.
destruct e; try discriminate.
</code>
<div class="context">1 subgoal
-------------------(1/1)
weakness grass = fire -> grass = grass
</div>
</pre>
Let's use this theorem from the last section again. `discriminate` took care
of the other two subgoals, and we know that `trivial` can solve this one. In
other words, we apply either `discriminate` or `trivial` to the subgoals
generated by `destruct e`, so we can use `||` to shorten the proof.
<pre class="example">
<code class="coq code">Theorem fire_weak_implies_grass :
forall (e : element),
weakness e = fire -> e = grass.
Proof.
destruct e; discriminate || trivial.
</code>
<div class="context">No more subgoals.
</div>
</pre>
<br>
<br>
<a name="all"></a>
### all:
The `all:` tactical applies a tactic to all the remaining subgoals in the
proof.
**Example:**
<pre class="example">
<code class="coq code">Theorem fire_weak_implies_grass :
forall (e : element),
weakness e = fire -> e = grass.
Proof.
destruct e.
all: discriminate || trivial.
</code>
<div class="context">1 subgoal
-------------------(1/1)
weakness grass = fire -> grass = grass
</div>
</pre>
An alternative proof for the previous theorem using `all:`.
<br>
<br>
<a name="repeat"></a>
### 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:**
<pre class="example">
<code class="coq code">Require Import Arith.
Theorem add_assoc_4 : forall (a b c d : nat),
(a + b + c) + d = a + (b + c + d).
Proof.
intros.
</code>
<div class="context">1 subgoal
a, b, c, d : nat
-------------------(1/1)
a + b + c + d = a + (b + c + d)
</div>
</pre>
Coq provides a theorem
`Nat.add_assoc : forall n m p : nat, n + (m + p) = n + m + p`
in the `Arith` library that we can make use of two times for this proof.
<pre class="example">
<code class="coq code">Require Import Arith.
Theorem add_assoc_4 : forall (a b c d : nat),
(a + b + c) + d = a + (b + c + d).
Proof.
intros.
repeat rewrite -> Nat.add_assoc.
</code>
<div class="context">1 subgoal
a, b, c, d : nat
-------------------(1/1)
a + b + c + d = a + b + c + d
</div>
</pre>
<br>
<br>
* * *
**Acknowledgement:** Inspired by the [Coq Tactic Index][tacticsindex] by Joseph
Redmon.
[tacticsindex]: https://pjreddie.com/coq-tactics/
]]>