\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Tactics¶

Tactics specify how to transform the proof state of an incomplete proof to eventually generate a complete proof.

Proofs can be developed in two basic ways: In forward reasoning, the proof begins by proving simple statements that are then combined to prove the theorem statement as the last step of the proof. With forward reasoning, for example, the proof of A /\ B would begin with proofs of A and B, which are then used to prove A /\ B. Forward reasoning is probably the most common approach in human-generated proofs.

In backward reasoning, the proof begins with the theorem statement as the goal, which is then gradually transformed until every subgoal generated along the way has been proven. In this case, the proof of A /\ B begins with that formula as the goal. This can be transformed into two subgoals, A and B, followed by the proofs of A and B. Coq and its tactics use backward reasoning.

A tactic may fully prove a goal, in which case the goal is removed from the proof state. More commonly, a tactic replaces a goal with one or more subgoals. (We say that a tactic reduces a goal to its subgoals.)

Most tactics require specific elements or preconditions to reduce a goal; they display error messages if they can't be applied to the goal. A few tactics, such as auto, don't fail even if the proof state is unchanged.

Goals are identified by number. The current goal is number 1. Tactics are applied to the current goal by default. (The default can be changed with the Default Goal Selector option.) They can be applied to another goal or to multiple goals with a goal selector such as 2: tactic.

This chapter describes many of the most common built-in tactics. Built-in tactics can be combined to form tactic expressions, which are described in the Ltac chapter. Since tactic expressions can be used anywhere that a built-in tactic can be used, "tactic" may refer to both built-in tactics and tactic expressions.

Common elements of tactics¶

Reserved keywords¶

The tactics described in this chapter reserve the following keywords:

by using

Thus, these keywords cannot be used as identifiers. It also declares the following character sequences as tokens:

** [= |-

Invocation of tactics¶

A tactic is applied as an ordinary command. It may be preceded by a goal selector (see Section Goal selectors). If no selector is specified, the default selector is used.

tactic_invocation::=toplevel_selector : tactic.|tactic.

Option Default Goal Selector "toplevel_selector"¶

This option controls the default selector, used when no selector is specified when applying a tactic. The initial value is 1, hence the tactics are, by default, applied to the first goal.

Using value all will make it so that tactics are, by default, applied to every goal simultaneously. Then, to apply a tactic tac to the first goal only, you can write 1:tac.

Using value ! enforces that all tactics are used either on a single focused goal or with a local selector (’’strict focusing mode’’).

Although other selectors are available, only all, ! or a single natural number are valid default goal selectors.

Bindings¶

Tactics that take a term as an argument may also accept bindings to instantiate some parameters of the term by name or position. The general form of a term with bindings is term_tac with bindings where bindings can take two different forms:

bindings::=( identnatural := term )+|one_term+

In the first form, if an ident is specified, it must be bound in the type of term and provides the tactic with an instance for the parameter of this name. If a natural is specified, it refers to the n-th non dependent premise of term_tac.

Error No such binder.¶
In the second form, the interpretation of the one_terms depend on which tactic they appear in. For induction, destruct, elim and case, the one_terms provide instances for all the dependent products in the type of term_tac while in the case of apply, or of constructor and its variants, only instances for the dependent products that are not bound in the conclusion of term_tac are required.

Error Not the right number of missing arguments.¶

Intro patterns¶

Intro patterns let you specify the name to assign to variables and hypotheses introduced by tactics. They also let you split an introduced hypothesis into multiple hypotheses or subgoals. Common tactics that accept intro patterns include assert, intros and destruct.

Note that the intro pattern syntax varies between tactics. Most tactics use simple_intropattern in the grammar. destruct, edestruct, induction, einduction, case, ecase and the various inversion tactics use or_and_intropattern_loc, while intros and eintros use intropattern_list. The eqn: construct in various tactics uses naming_intropattern.

Naming patterns

Use these elementary patterns to specify a name:

ident — use the specified name
? — let Coq choose a name
?ident — generate a name that begins with ident
_ — discard the matched part (unless it is required for another hypothesis)
if a disjunction pattern omits a name, such as [|H2], Coq will choose a name

Splitting patterns

The most common splitting patterns are:

split a hypothesis in the form A /\ B into two hypotheses H1: A and H2: B using the pattern (H1 & H2) or (H1, H2) or [H1 H2]. Example. This also works on A <-> B, which is just a notation representing (A -> B) /\ (B -> A).
split a hypothesis in the form A \/ B into two subgoals using the pattern [H1|H2]. The first subgoal will have the hypothesis H1: A and the second subgoal will have the hypothesis H2: B. Example
split a hypothesis in either of the forms A /\ B or A \/ B using the pattern [].

Patterns can be nested: [[Ha|Hb] H] can be used to split (A \/ B) /\ C.

Note that there is no equivalent to intro patterns for goals. For a goal A /\ B, use the split tactic to replace the current goal with subgoals A and B. For a goal A \/ B, use left to replace the current goal with A, or right to replace the current goal with B.

( simple_intropattern+, ) — matches a product over an inductive type with a single constructor. If the number of patterns equals the number of constructor arguments, then it applies the patterns only to the arguments, and ( simple_intropattern+, ) is equivalent to [simple_intropattern+]. If the number of patterns equals the number of constructor arguments plus the number of let-ins, the patterns are applied to the arguments and let-in variables.
( simple_intropattern+& ) — matches a right-hand nested term that consists of one or more nested binary inductive types such as a1 OP1 a2 OP2 ... (where the OPn are right-associative). (If the OPn are left-associative, additional parentheses will be needed to make the term right-hand nested, such as a1 OP1 (a2 OP2 ...).) The splitting pattern can have more than 2 names, for example (H1 & H2 & H3) matches A /\ B /\ C. The inductive types must have a single constructor with two parameters. Example
[ intropattern_list+| ] — splits an inductive type that has multiple constructors such as A \/ B into multiple subgoals. The number of intropattern_list must be the same as the number of constructors for the matched part.
[ intropattern+ ] — splits an inductive type that has a single constructor with multiple parameters such as A /\ B into multiple hypotheses. Use [H1 [H2 H3]] to match A /\ B /\ C.
[] — splits an inductive type: If the inductive type has multiple constructors, such as A \/ B, create one subgoal for each constructor. If the inductive type has a single constructor with multiple parameters, such as A /\ B, split it into multiple hypotheses.

Equality patterns

These patterns can be used when the hypothesis is an equality:

-> — replaces the right-hand side of the hypothesis with the left-hand side of the hypothesis in the conclusion of the goal; the hypothesis is cleared; if the left-hand side of the hypothesis is a variable, it is substituted everywhere in the context and the variable is removed. Example
<- — similar to ->, but replaces the left-hand side of the hypothesis with the right-hand side of the hypothesis.
[= intropattern*, ] — If the product is over an equality type, applies either injection or discriminate. If injection is applicable, the intropattern is used on the hypotheses generated by injection. If the number of patterns is smaller than the number of hypotheses generated, the pattern ? is used to complete the list. Example

Other patterns

* — introduces one or more quantified variables from the result until there are no more quantified variables. Example
** — introduces one or more quantified variables or hypotheses from the result until there are no more quantified variables or implications (->). intros ** is equivalent to intros. Example
simple_intropattern_closed % term* — first applies each of the terms with the apply … in tactic on the hypothesis to be introduced, then it uses simple_intropattern_closed. Example

Flag Bracketing Last Introduction Pattern¶: For intros intropattern_list, controls how to handle a conjunctive pattern that doesn't give enough simple patterns to match all the arguments in the constructor. If set (the default), Coq generates additional names to match the number of arguments. Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more similar to SSReflect's intro patterns.

Deprecated since version 8.10.

Note

A \/ B and A /\ B use infix notation to refer to the inductive types or and and. or has multiple constructors (or_introl and or_intror), while and has a single constructor (conj) with multiple parameters (A and B). These are defined in theories/Init/Logic.v. The "where" clauses define the infix notation for "or" and "and".

Inductive or (A B:Prop) : Prop := | or_introl : A -> A \/ B | or_intror : B -> A \/ B where "A \/ B" := (or A B) : type_scope. Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B where "A /\ B" := (and A B) : type_scope.

Note

intros p+ is not always equivalent to intros p; ... ; intros p if some of the p are _. In the first form, all erasures are done at once, while they're done sequentially for each tactic in the second form. If the second matched term depends on the first matched term and the pattern for both is _ (i.e., both will be erased), the first intros in the second form will fail because the second matched term still has the dependency on the first.

Examples:

Example: intro pattern for /\

Goal forall (A: Prop) (B: Prop), (A /\ B) -> True.
1 subgoal ============================ forall A B : Prop, A /\ B -> True

intros.
1 subgoal A, B : Prop H : A /\ B ============================ True

destruct H as (HA & HB).
1 subgoal A, B : Prop HA : A HB : B ============================ True

Example: intro pattern for \/

Goal forall (A: Prop) (B: Prop), (A \/ B) -> True.
1 subgoal ============================ forall A B : Prop, A \/ B -> True

intros.
1 subgoal A, B : Prop H : A \/ B ============================ True

destruct H as [HA|HB]. all: swap 1 2.
2 subgoals A, B : Prop HA : A ============================ True subgoal 2 is: True 2 subgoals A, B : Prop HB : B ============================ True subgoal 2 is: True

Example: -> intro pattern

Goal forall (x:nat) (y:nat) (z:nat), (x = y) -> (y = z) -> (x = z).
1 subgoal ============================ forall x y z : nat, x = y -> y = z -> x = z

intros * H.
1 subgoal x, y, z : nat H : x = y ============================ y = z -> x = z

intros ->.
1 subgoal x, z : nat H : x = z ============================ x = z

Example: [=] intro pattern

The first intros [=] uses injection to strip (S ...) from both sides of the matched equality. The second uses discriminate on the contradiction 1 = 2 (internally represented as (S O) = (S (S O))) to complete the goal.

Goal forall (n m:nat), (S n) = (S m) -> (S O)=(S (S O)) -> False.
1 subgoal ============================ forall n m : nat, S n = S m -> 1 = 2 -> False

intros *.
1 subgoal n, m : nat ============================ S n = S m -> 1 = 2 -> False

intros [= H].
1 subgoal n, m : nat H : n = m ============================ 1 = 2 -> False

intros [=].
No more subgoals.

Example: (A & B & ...) intro pattern

Parameters (A : Prop) (B: nat -> Prop) (C: Prop).
A is declared B is declared C is declared

Goal A /\ (exists x:nat, B x /\ C) -> True.
1 subgoal ============================ A /\ (exists x : nat, B x /\ C) -> True

intros (a & x & b & c).
1 subgoal a : A x : nat b : B x c : C ============================ True

Example: * intro pattern

Goal forall (A: Prop) (B: Prop), A -> B.
1 subgoal ============================ forall A B : Prop, A -> B

intros *.
1 subgoal A, B : Prop ============================ A -> B

Example: ** pattern ("intros **" is equivalent to "intros")

Goal forall (A: Prop) (B: Prop), A -> B.
1 subgoal ============================ forall A B : Prop, A -> B

intros **.
1 subgoal A, B : Prop H : A ============================ B

Example: compound intro pattern

Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
1 subgoal ============================ forall A B C : Prop, A \/ B /\ C -> (A -> C) -> C

intros * [a | (_,c)] f.
2 subgoals A, B, C : Prop a : A f : A -> C ============================ C subgoal 2 is: C

all: swap 1 2.
2 subgoals A, B, C : Prop c : C f : A -> C ============================ C subgoal 2 is: C

Example: combined intro pattern using [=] -> and %

Require Import Coq.Lists.List.

Section IntroPatterns.

Variables (A : Type) (xs ys : list A).
A is declared xs is declared ys is declared

Example ThreeIntroPatternsCombined : S (length ys) = 1 -> xs ++ ys = xs.
1 subgoal A : Type xs, ys : list A ============================ S (length ys) = 1 -> xs ++ ys = xs

intros [=->%length_zero_iff_nil].
1 subgoal A : Type xs : list A ============================ xs ++ nil = xs

intros would add H : S (length ys) = 1

intros [=] would additionally apply injection to H to yield H0 : length ys = 0

intros [=->%length_zero_iff_nil] applies the theorem, making H the equality l=nil, which is then applied as for ->.

Theorem length_zero_iff_nil (l : list A): length l = 0 <-> l=nil.

The example is based on Tej Chajed's coq-tricks

Occurrence clauses¶

An occurrence is a subterm of a goal or hypothesis that matches a pattern provided by a tactic. Occurrence clauses select a subset of the ocurrences in a goal and/or in one or more of its hypotheses.

occurrences::=at occs_nums|in goal_occurrencesoccs_nums::=-? nat_or_var+nat_or_var::=naturalidentgoal_occurrences::=hyp_occs+, |- concl_occs??|* |- concl_occs?||- concl_occs?|concl_occs?hyp_occs::=hypident at occs_nums?hypident::=ident|( type of ident )|( value of ident )concl_occs::=* at occs_nums?

occurrences
The first form of occurrences selects occurrences in the conclusion of the goal. The second form can select occurrences in the goal conclusion and in one or more hypotheses.

-? nat_or_var+
Selects the specified occurrences within a single goal or hypothesis. Occurrences are numbered starting with 1 following a depth-first traversal of the term's expression, including occurrences in implicit arguments and coercions that are not displayed by default. (Set the Printing All flag to show those in the printed term.)

For example, when matching the pattern _ + _ in the term (a + b) + c, occurrence 1 is (...) + c and occurrence 2 is (a + b). When matching that pattern with term a + (b + c), occurrence 1 is a + (...) and occurrence 2 is b + c.

Specifying - includes all occurrences except the ones listed.

hyp_occs*, |- concl_occs??
Selects occurrences in the specified hypotheses and the specified occurrences in the conclusion.

* |- concl_occs?
Selects all occurrences in all hypotheses and the specified occurrences in the conclusion.

|- concl_occs?
Selects the specified occurrences in the conclusion.

goal_occurrences ::= concl_occs?
Selects all occurrences in all hypotheses and in the specified occurrences in the conclusion.

hypident at occs_nums?
Omiting occs_nums selects all occurrences within the hypothesis.

hypident ::= ident
Selects the hypothesis named ident.

( type of ident )
Selects the type part of the named hypothesis (e.g. : nat).

( value of ident )
Selects the value part of the named hypothesis (e.g. := 1).

concl_occs ::= * at occs_nums?
Selects occurrences in the conclusion. '*' by itself selects all occurrences. occs_nums selects the specified occurrences.

Use in * to select all occurrences in all hypotheses and the conclusion, which is equivalent to in * |- *. Use * |- to select all occurrences in all hypotheses.

Tactics that select a specific hypothesis H to apply to other hypotheses, such as rewrite H in * |-, won't apply H to itself.

If multiple occurrences are given, such as in rewrite H at 1 2 3, the tactic must match at least one occurrence in order to succeed. The tactic will fail if no occurrences match. Occurrence numbers that are out of range (e.g. at 1 3 when there are only 2 occurrences in the hypothesis or conclusion) are ignored.

Tactics that use occurrence clauses include set, remember, induction and destruct.

Applying theorems¶

Tactic exact term¶

This tactic applies to any goal. It gives directly the exact proof term of the goal. Let T be our goal, let p be a term of type U then exact p succeeds iff T and U are convertible (see Conversion rules).

Error Not an exact proof.¶

Variant eexact term.¶: This tactic behaves like exact but is able to handle terms and goals with existential variables.

Tactic assumption¶

This tactic looks in the local context for a hypothesis whose type is convertible to the goal. If it is the case, the subgoal is proved. Otherwise, it fails.

Error No such assumption.¶

Variant eassumption¶: This tactic behaves like assumption but is able to handle goals with existential variables.

Tactic refine term¶

This tactic applies to any goal. It behaves like exact with a big difference: the user can leave some holes (denoted by _ or (_ : type)) in the term. refine will generate as many subgoals as there are remaining holes in the elaborated term. The type of holes must be either synthesized by the system or declared by an explicit cast like (_ : nat -> Prop). Any subgoal that occurs in other subgoals is automatically shelved, as if calling shelve_unifiable. The produced subgoals (shelved or not) are not candidates for typeclass resolution, even if they have a type-class type as conclusion, letting the user control when and how typeclass resolution is launched on them. This low-level tactic can be useful to advanced users.

Example

Inductive Option : Set := | Fail : Option | Ok : bool -> Option.: Option is defined Option_rect is defined Option_ind is defined Option_rec is defined Option_sind is defined
Definition get : forall x:Option, x <> Fail -> bool.: 1 subgoal ============================ forall x : Option, x <> Fail -> bool
refine (fun x:Option => match x return x <> Fail -> bool with | Fail => _ | Ok b => fun _ => b end).: 1 subgoal x : Option ============================ Fail <> Fail -> bool
intros; absurd (Fail = Fail); trivial.: No more subgoals.
Defined.

Error Invalid argument.¶: The tactic refine does not know what to do with the term you gave.

Error Refine passed ill-formed term.¶: The term you gave is not a valid proof (not easy to debug in general). This message may also occur in higher-level tactics that call refine internally.

Error Cannot infer a term for this placeholder.¶: There is a hole in the term you gave whose type cannot be inferred. Put a cast around it.

Variant simple refine term¶: This tactic behaves like refine, but it does not shelve any subgoal. It does not perform any beta-reduction either.

Variant notypeclasses refine term¶: This tactic behaves like refine except it performs type checking without resolution of typeclasses.

Variant simple notypeclasses refine term¶: This tactic behaves like the combination of simple refine and notypeclasses refine: it performs type checking without resolution of typeclasses, does not perform beta reductions or shelve the subgoals.

Flag Debug Unification¶: Enables printing traces of unification steps used during elaboration/typechecking and the refine tactic.

Tactic apply term¶

This tactic applies to any goal. The argument term is a term well-formed in the local context. The tactic apply tries to match the current goal against the conclusion of the type of term. If it succeeds, then the tactic returns as many subgoals as the number of non-dependent premises of the type of term. If the conclusion of the type of term does not match the goal and the conclusion is an inductive type isomorphic to a tuple type, then each component of the tuple is recursively matched to the goal in the left-to-right order.

The tactic apply relies on first-order unification with dependent types unless the conclusion of the type of term is of the form P (t₁ ... t_n) with P to be instantiated. In the latter case, the behavior depends on the form of the goal. If the goal is of the form (fun x => Q) u₁ ... u_n and the t_i and u_i unify, then P is taken to be (fun x => Q). Otherwise, apply tries to define P by abstracting over t_1 ... t__n in the goal. See pattern to transform the goal so that it gets the form (fun x => Q) u₁ ... u_n.

Error Unable to unify term with term.¶: The apply tactic failed to match the conclusion of term and the current goal. You can help the apply tactic by transforming your goal with the change or pattern tactics.

Error Unable to find an instance for the variables ident+.¶: This occurs when some instantiations of the premises of term are not deducible from the unification. This is the case, for instance, when you want to apply a transitivity property. In this case, you have to use one of the variants below:

Variant apply term with term+

Provides apply with explicit instantiations for all dependent premises of the type of term that do not occur in the conclusion and consequently cannot be found by unification. Notice that the collection term+ must be given according to the order of these dependent premises of the type of term.

Error Not the right number of missing arguments.¶

Variant apply term with bindings: This also provides apply with values for instantiating premises. Here, variables are referred by names and non-dependent products by increasing numbers (see Bindings).

Variant apply term+,: This is a shortcut for apply term₁; [.. | ... ; [ .. | apply term_n] ... ], i.e. for the successive applications of term_i+1 on the last subgoal generated by apply term_i , starting from the application of term₁.

Variant eapply term¶: The tactic eapply behaves like apply but it does not fail when no instantiations are deducible for some variables in the premises. Rather, it turns these variables into existential variables which are variables still to instantiate (see Existential variables). The instantiation is intended to be found later in the proof.

Variant rapply term¶

The tactic rapply behaves like eapply but it uses the proof engine of refine for dealing with existential variables, holes, and conversion problems. This may result in slightly different behavior regarding which conversion problems are solvable. However, like apply but unlike eapply, rapply will fail if there are any holes which remain in term itself after typechecking and typeclass resolution but before unification with the goal. More technically, term is first parsed as a constr rather than as a uconstr or open_constr before being applied to the goal. Note that rapply prefers to instantiate as many hypotheses of term as possible. As a result, if it is possible to apply term to arbitrarily many arguments without getting a type error, rapply will loop.

Note that you need to Require Import Coq.Program.Tactics to make use of rapply.

Variant simple apply term.

This behaves like apply but it reasons modulo conversion only on subterms that contain no variables to instantiate. For instance, the following example does not succeed because it would require the conversion of id ?foo and O.

Example

Definition id (x : nat) := x.: id is defined
Parameter H : forall x y, id x = y.: H is declared
Goal O = O.: 1 subgoal ============================ 0 = 0
Fail simple apply H.: The command has indeed failed with message: Unable to unify "id ?M160 = ?M161" with "0 = 0".

Because it reasons modulo a limited amount of conversion, simple apply fails quicker than apply and it is then well-suited for uses in user-defined tactics that backtrack often. Moreover, it does not traverse tuples as apply does.

Variant simple? apply term with bindings?+,¶
Variant simple? eapply term with bindings?+,¶: This summarizes the different syntaxes for apply and eapply.

Variant lapply term¶

This tactic applies to any goal, say G. The argument term has to be well-formed in the current context, its type being reducible to a non-dependent product A -> B with B possibly containing products. Then it generates two subgoals B->G and A. Applying lapply H (where H has type A->B and B does not start with a product) does the same as giving the sequence cut B. 2:apply H. where cut is described below.

Warning When term contains more than one non dependent product the tactic lapply only takes into account the first product.¶

Example

Assume we have a transitive relation R on nat:

Parameter R : nat -> nat -> Prop.: R is declared
Axiom Rtrans : forall x y z:nat, R x y -> R y z -> R x z.: Rtrans is declared
Parameters n m p : nat.: n is declared m is declared p is declared
Axiom Rnm : R n m.: Rnm is declared
Axiom Rmp : R m p.: Rmp is declared

Consider the goal (R n p) provable using the transitivity of R:

Goal R n p.: 1 subgoal ============================ R n p

The direct application of Rtrans with apply fails because no value for y in Rtrans is found by apply:

apply Rtrans.: Toplevel input, characters 6-12: > apply Rtrans. > ^^^^^^ Error: Unable to find an instance for the variable y.

A solution is to apply (Rtrans n m p) or (Rtrans n m).

apply (Rtrans n m p).: 2 subgoals ============================ R n m subgoal 2 is: R m p

Note that n can be inferred from the goal, so the following would work too.

apply (Rtrans _ m).: 2 subgoals ============================ R n m subgoal 2 is: R m p

More elegantly, apply Rtrans with (y:=m) allows only mentioning the unknown m:

apply Rtrans with (y := m).: 2 subgoals ============================ R n m subgoal 2 is: R m p

Another solution is to mention the proof of (R x y) in Rtrans

apply Rtrans with (1 := Rnm).: 1 subgoal ============================ R m p

... or the proof of (R y z).

apply Rtrans with (2 := Rmp).: 1 subgoal ============================ R n m

On the opposite, one can use eapply which postpones the problem of finding m. Then one can apply the hypotheses Rnm and Rmp. This instantiates the existential variable and completes the proof.

eapply Rtrans.: 2 focused subgoals (shelved: 1) ============================ R n ?y subgoal 2 is: R ?y p
apply Rnm.: 1 subgoal ============================ R m p
apply Rmp.: No more subgoals.

Note

When the conclusion of the type of the term to apply is an inductive type isomorphic to a tuple type and apply looks recursively whether a component of the tuple matches the goal, it excludes components whose statement would result in applying an universal lemma of the form forall A, ... -> A. Excluding this kind of lemma can be avoided by setting the following flag:

Flag Universal Lemma Under Conjunction¶: This flag, which preserves compatibility with versions of Coq prior to 8.4 is also available for apply term in ident (see apply … in).

Tactic apply term in ident¶

This tactic applies to any goal. The argument term is a term well-formed in the local context and the argument ident is an hypothesis of the context. The tactic apply term in ident tries to match the conclusion of the type of ident against a non-dependent premise of the type of term, trying them from right to left. If it succeeds, the statement of hypothesis ident is replaced by the conclusion of the type of term. The tactic also returns as many subgoals as the number of other non-dependent premises in the type of term and of the non-dependent premises of the type of ident. If the conclusion of the type of term does not match the goal and the conclusion is an inductive type isomorphic to a tuple type, then the tuple is (recursively) decomposed and the first component of the tuple of which a non-dependent premise matches the conclusion of the type of ident. Tuples are decomposed in a width-first left-to-right order (for instance if the type of H1 is A <-> B and the type of H2 is A then apply H1 in H2 transforms the type of H2 into B). The tactic apply relies on first-order pattern matching with dependent types.

Error Statement without assumptions.¶: This happens if the type of term has no non-dependent premise.

Error Unable to apply.¶: This happens if the conclusion of ident does not match any of the non-dependent premises of the type of term.

Variant apply term+, in ident+,: This applies each term in sequence in each hypothesis ident.

Variant apply term with bindings+, in ident+,: This does the same but uses the bindings to instantiate parameters of term (see Bindings).

Variant eapply term with bindings?+, in ident+,: This works as apply … in but turns unresolved bindings into existential variables, if any, instead of failing.

Variant apply term with bindings?+, in ident as simple_intropattern?+,¶: This works as apply … in but applying an associated simple_intropattern to each hypothesis ident that comes with such clause.

Variant simple apply term in ident+,: This behaves like apply … in but it reasons modulo conversion only on subterms that contain no variables to instantiate and does not traverse tuples. See the corresponding example.

Variant simple? apply term with bindings?+, in ident as simple_intropattern?+,
Variant simple? eapply term with bindings?+, in ident as simple_intropattern?+,: This summarizes the different syntactic variants of apply term in ident+, and eapply term in ident+,.

Tactic constructor natural¶

This tactic applies to a goal such that its conclusion is an inductive type (say I). The argument natural must be less or equal to the numbers of constructor(s) of I. Let c_i be the i-th constructor of I, then constructor i is equivalent to intros; apply c_i.

Error Not an inductive product.¶

Error Not enough constructors.¶

Variant constructor: This tries constructor 1 then constructor 2, ..., then constructor n where n is the number of constructors of the head of the goal.

Variant constructor natural with bindings: Let c be the i-th constructor of I, then constructor i with bindings is equivalent to intros; apply c with bindings.

Warning

The terms in bindings are checked in the context where constructor is executed and not in the context where apply is executed (the introductions are not taken into account).

Variant split with bindings?¶

This applies only if I has a single constructor. It is then equivalent to constructor 1 with bindings?. It is typically used in the case of a conjunction $A \wedge B$.

Variant exists bindings¶: This applies only if I has a single constructor. It is then equivalent to intros; constructor 1 with bindings. It is typically used in the case of an existential quantification $\exists x, P(x).$

Variant exists bindings+,: This iteratively applies exists bindings.

Error Not an inductive goal with 1 constructor.¶

Variant left with bindings?¶

Variant right with bindings?¶

These tactics apply only if I has two constructors, for instance in the case of a disjunction $A \vee B$. Then, they are respectively equivalent to constructor 1 with bindings? and constructor 2 with bindings?.

Error Not an inductive goal with 2 constructors.¶

Variant econstructor¶
Variant eexists¶
Variant esplit¶
Variant eleft¶
Variant eright¶: These tactics and their variants behave like constructor, exists, split, left, right and their variants but they introduce existential variables instead of failing when the instantiation of a variable cannot be found (cf. eapply and apply).

Flag Debug Tactic Unification¶: Enables printing traces of unification steps in tactic unification. Tactic unification is used in tactics such as apply and rewrite.

Managing the local context¶

Tactic intro¶

This tactic applies to a goal that is either a product or starts with a let-binder. If the goal is a product, the tactic implements the "Lam" rule given in Typing rules 1. If the goal starts with a let-binder, then the tactic implements a mix of the "Let" and "Conv".

If the current goal is a dependent product forall x:T, U (resp let x:=t in U) then intro puts x:T (resp x:=t) in the local context. The new subgoal is U.

If the goal is a non-dependent product $T \rightarrow U$, then it puts in the local context either Hn:T (if T is of type Set or Prop) or Xn:T (if the type of T is Type). The optional index n is such that Hn or Xn is a fresh identifier. In both cases, the new subgoal is U.

If the goal is an existential variable, intro forces the resolution of the existential variable into a dependent product $\forall$ x:?X, ?Y, puts x:?X in the local context and leaves ?Y as a new subgoal allowed to depend on x.

The tactic intro applies the tactic hnf until intro can be applied or the goal is not head-reducible.

Error No product even after head-reduction.¶

Variant intro ident

This applies intro but forces ident to be the name of the introduced hypothesis.

Error ident is already used.¶

Note

If a name used by intro hides the base name of a global constant then the latter can still be referred to by a qualified name (see Qualified identifiers).

Variant intros¶: This repeats intro until it meets the head-constant. It never reduces head-constants and it never fails.

Variant intros ident+.: This is equivalent to the composed tactic intro ident; ... ; intro ident.

Variant intros until ident

This repeats intro until it meets a premise of the goal having the form (ident : type) and discharges the variable named ident of the current goal.

Error No such hypothesis in current goal.¶

Variant intros until natural

This repeats intro until the natural-th non-dependent product.

Example

On the subgoal forall x y : nat, x = y -> y = x the tactic intros until 1 is equivalent to intros x y H, as x = y -> y = x is the first non-dependent product.

On the subgoal forall x y z : nat, x = y -> y = x the tactic intros until 1 is equivalent to intros x y z as the product on z can be rewritten as a non-dependent product: forall x y : nat, nat -> x = y -> y = x.

Error No such hypothesis in current goal.¶: This happens when natural is 0 or is greater than the number of non-dependent products of the goal.

Variant intro ident₁? after ident₂

Variant intro ident₁? before ident₂

Variant intro ident₁? at top

Variant intro ident₁? at bottom

These tactics apply intro ident₁? and move the freshly introduced hypothesis respectively after the hypothesis ident₂, before the hypothesis ident₂, at the top of the local context, or at the bottom of the local context. All hypotheses on which the new hypothesis depends are moved too so as to respect the order of dependencies between hypotheses. It is equivalent to intro ident₁? followed by the appropriate call to move … after …, move … before …, move … at top, or move … at bottom.

Note

intro at bottom is a synonym for intro with no argument.

Error No such hypothesis: ident.¶

Tactic intros intropattern_list¶: Introduces one or more variables or hypotheses from the goal by matching the intro patterns. See the description in Intro patterns.

Tactic eintros intropattern_list¶: Works just like intros … except that it creates existential variables for any unresolved variables rather than failing.

Tactic clear ident¶

This tactic erases the hypothesis named ident in the local context of the current goal. As a consequence, ident is no more displayed and no more usable in the proof development.

Error No such hypothesis.¶

Error ident is used in the conclusion.¶

Error ident is used in the hypothesis ident.¶

Variant clear ident+: This is equivalent to clear ident. ... clear ident.

Variant clear - ident+: This variant clears all the hypotheses except the ones depending in the hypotheses named ident+ and in the goal.

Variant clear: This variants clears all the hypotheses except the ones the goal depends on.

Variant clear dependent ident: This clears the hypothesis ident and all the hypotheses that depend on it.

Variant clearbody ident+¶

This tactic expects ident+ to be local definitions and clears their respective bodies. In other words, it turns the given definitions into assumptions.

Error ident is not a local definition.¶

Tactic revert ident+¶

This applies to any goal with variables ident+. It moves the hypotheses (possibly defined) to the goal, if this respects dependencies. This tactic is the inverse of intro.

Error No such hypothesis.¶

Error ident₁ is used in the hypothesis ident₂.¶

Variant revert dependent ident¶: This moves to the goal the hypothesis ident and all the hypotheses that depend on it.

Tactic move ident₁ after ident₂¶

This moves the hypothesis named ident₁ in the local context after the hypothesis named ident₂, where “after” is in reference to the direction of the move. The proof term is not changed.

If ident₁ comes before ident₂ in the order of dependencies, then all the hypotheses between ident₁ and ident₂ that (possibly indirectly) depend on ident₁ are moved too, and all of them are thus moved after ident₂ in the order of dependencies.

If ident₁ comes after ident₂ in the order of dependencies, then all the hypotheses between ident₁ and ident₂ that (possibly indirectly) occur in the type of ident₁ are moved too, and all of them are thus moved before ident₂ in the order of dependencies.

Variant move ident₁ before ident₂¶: This moves ident₁ towards and just before the hypothesis named ident₂. As for move … after …, dependencies over ident₁ (when ident₁ comes before ident₂ in the order of dependencies) or in the type of ident₁ (when ident₁ comes after ident₂ in the order of dependencies) are moved too.

Variant move ident at top¶: This moves ident at the top of the local context (at the beginning of the context).

Variant move ident at bottom¶: This moves ident at the bottom of the local context (at the end of the context).

Error No such hypothesis.¶

Error Cannot move ident₁ after ident₂: it occurs in the type of ident₂.¶

Error Cannot move ident₁ after ident₂: it depends on ident₂.¶

Example

Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x.: 1 subgoal ============================ forall x : nat, x = 0 -> nat -> forall y : nat, y = y -> 0 = x
intros x H z y H0.: 1 subgoal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
move x after H0.: 1 subgoal z, y : nat H0 : y = y x : nat H : x = 0 ============================ 0 = x
Undo.: 1 subgoal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
move x before H0.: 1 subgoal z, y, x : nat H : x = 0 H0 : y = y ============================ 0 = x
Undo.: 1 subgoal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
move H0 after H.: 1 subgoal x, y : nat H0 : y = y H : x = 0 z : nat ============================ 0 = x
Undo.: 1 subgoal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
move H0 before H.: 1 subgoal x : nat H : x = 0 y : nat H0 : y = y z : nat ============================ 0 = x

Tactic rename ident₁ into ident₂¶

This renames hypothesis ident₁ into ident₂ in the current context. The name of the hypothesis in the proof-term, however, is left unchanged.

Variant rename ident_i into ident_j+,: This renames the variables ident_i into ident_j in parallel. In particular, the target identifiers may contain identifiers that exist in the source context, as long as the latter are also renamed by the same tactic.

Error No such hypothesis.¶

Error ident is already used.¶

Tactic set (ident := term)¶

This replaces term by ident in the conclusion of the current goal and adds the new definition ident := term to the local context.

If term has holes (i.e. subexpressions of the form “_”), the tactic first checks that all subterms matching the pattern are compatible before doing the replacement using the leftmost subterm matching the pattern.

Error The variable ident is already defined.¶

Variant set (ident := term) in goal_occurrences: This notation allows specifying which occurrences of term have to be substituted in the context. The in goal_occurrences clause is an occurrence clause whose syntax and behavior are described in goal occurrences.

Variant set (ident binder* := term) in goal_occurrences?: This is equivalent to set (ident := fun binder* => term) in goal_occurrences?.

Variant set term in goal_occurrences?: This behaves as set (ident := term) in goal_occurrences? but ident is generated by Coq.

Variant eset (ident binder* := term) in goal_occurrences?¶
Variant eset term in goal_occurrences?¶: While the different variants of set expect that no existential variables are generated by the tactic, eset removes this constraint. In practice, this is relevant only when eset is used as a synonym of epose, i.e. when the term does not occur in the goal.

Tactic remember term as ident₁ eqn:naming_intropattern?¶

This behaves as set (ident := term) in *, using a logical (Leibniz’s) equality instead of a local definition. Use naming_intropattern to name or split up the new equation.

Variant remember term as ident₁ eqn:naming_intropattern? in goal_occurrences: This is a more general form of remember that remembers the occurrences of term specified by an occurrence set.

Variant eremember term as ident₁ eqn:naming_intropattern? in goal_occurrences?¶: While the different variants of remember expect that no existential variables are generated by the tactic, eremember removes this constraint.

Tactic pose (ident := term)¶

This adds the local definition ident := term to the current context without performing any replacement in the goal or in the hypotheses. It is equivalent to set (ident := term) in |-.

Variant pose (ident binder* := term): This is equivalent to pose (ident := fun binder* => term).

Variant pose term: This behaves as pose (ident := term) but ident is generated by Coq.

Variant epose (ident binder* := term)¶
Variant epose term¶: While the different variants of pose expect that no existential variables are generated by the tactic, epose removes this constraint.

Tactic decompose [qualid+] term¶

This tactic recursively decomposes a complex proposition in order to obtain atomic ones.

Example

Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.: 1 subgoal ============================ forall A B C : Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C
intros A B C H; decompose [and or] H.: 3 subgoals A, B, C : Prop H : A /\ B /\ C \/ B /\ C \/ C /\ A H1 : A H0 : B H3 : C ============================ C subgoal 2 is: C subgoal 3 is: C
all: assumption.: No more subgoals.
Qed.

Note

decompose does not work on right-hand sides of implications or products.

Variant decompose sum term: This decomposes sum types (like or).

Variant decompose record term: This decomposes record types (inductive types with one constructor, like and and exists and those defined with the Record command.

Controlling the proof flow¶

Tactic assert (ident : type)¶

This tactic applies to any goal. assert (H : U) adds a new hypothesis of name H asserting U to the current goal and opens a new subgoal U 2. The subgoal U comes first in the list of subgoals remaining to prove.

Error Not a proposition or a type.¶: Arises when the argument type is neither of type Prop, Set nor Type.

Variant assert type: This behaves as assert (ident : type) but ident is generated by Coq.

Variant assert type by tactic

This tactic behaves like assert but applies tactic to solve the subgoals generated by assert.

Error Proof is not complete.¶

Variant assert type as simple_intropattern: If simple_intropattern is an intro pattern (see Intro patterns), the hypothesis is named after this introduction pattern (in particular, if simple_intropattern is ident, the tactic behaves like assert (ident : type)). If simple_intropattern is an action introduction pattern, the tactic behaves like assert type followed by the action done by this introduction pattern.

Variant assert type as simple_intropattern by tactic: This combines the two previous variants of assert.

Variant assert (ident := term)

This behaves as assert (ident : type) by exact term where type is the type of term. This is equivalent to using pose proof. If the head of term is ident, the tactic behaves as specialize.

Error Variable ident is already declared.¶

Variant eassert type as simple_intropattern by tactic¶: While the different variants of assert expect that no existential variables are generated by the tactic, eassert removes this constraint. This lets you avoid specifying the asserted statement completely before starting to prove it.

Variant pose proof term as simple_intropattern?¶: This tactic behaves like assert type as simple_intropattern? by exact term where type is the type of term. In particular, pose proof term as ident behaves as assert (ident := term) and pose proof term as simple_intropattern is the same as applying the simple_intropattern to term.

Variant epose proof term as simple_intropattern?¶: While pose proof expects that no existential variables are generated by the tactic, epose proof removes this constraint.

Variant pose proof (ident := term): This is an alternative syntax for assert (ident := term) and pose proof term as ident, following the model of pose (ident := term) but dropping the value of ident.

Variant epose proof (ident := term): This is an alternative syntax for eassert (ident := term) and epose proof term as ident, following the model of epose (ident := term) but dropping the value of ident.

Variant enough (ident : type)¶: This adds a new hypothesis of name ident asserting type to the goal the tactic enough is applied to. A new subgoal stating type is inserted after the initial goal rather than before it as assert would do.

Variant enough type: This behaves like enough (ident : type) with the name ident of the hypothesis generated by Coq.

Variant enough type as simple_intropattern: This behaves like enough type using simple_intropattern to name or destruct the new hypothesis.

Variant enough (ident : type) by tactic
Variant enough type as simple_intropattern? by tactic: This behaves as above but with tactic expected to solve the initial goal after the extra assumption type is added and possibly destructed. If the as simple_intropattern clause generates more than one subgoal, tactic is applied to all of them.

Variant eenough type as simple_intropattern? by tactic?¶
Variant eenough (ident : type) by tactic?¶: While the different variants of enough expect that no existential variables are generated by the tactic, eenough removes this constraint.

Variant cut type¶: This tactic applies to any goal. It implements the non-dependent case of the “App” rule given in Typing rules. (This is Modus Ponens inference rule.) cut U transforms the current goal T into the two following subgoals: U -> T and U. The subgoal U -> T comes first in the list of remaining subgoal to prove.

Variant specialize (ident term*) as simple_intropattern?¶

Variant specialize ident with bindings as simple_intropattern?¶

This tactic works on local hypothesis ident. The premises of this hypothesis (either universal quantifications or non-dependent implications) are instantiated by concrete terms coming either from arguments term* or from Bindings. In the first form the application to term* can be partial. The first form is equivalent to assert (ident := ident term*). In the second form, instantiation elements can also be partial. In this case the uninstantiated arguments are inferred by unification if possible or left quantified in the hypothesis otherwise. With the as clause, the local hypothesis ident is left unchanged and instead, the modified hypothesis is introduced as specified by the simple_intropattern. The name ident can also refer to a global lemma or hypothesis. In this case, for compatibility reasons, the behavior of specialize is close to that of generalize: the instantiated statement becomes an additional premise of the goal. The as clause is especially useful in this case to immediately introduce the instantiated statement as a local hypothesis.

Error ident is used in hypothesis ident.¶

Error ident is used in conclusion.¶

Tactic generalize term¶: This tactic applies to any goal. It generalizes the conclusion with respect to some term.

Example

Goal forall x y:nat, 0 <= x + y + y.: 1 subgoal ============================ forall x y : nat, 0 <= x + y + y
Proof. intros *.: 1 subgoal x, y : nat ============================ 0 <= x + y + y

Show.: 1 subgoal x, y : nat ============================ 0 <= x + y + y
generalize (x + y + y).: 1 subgoal x, y : nat ============================ forall n : nat, 0 <= n

If the goal is G and t is a subterm of type T in the goal, then generalize t replaces the goal by forall (x:T), G′ where G′ is obtained from G by replacing all occurrences of t by x. The name of the variable (here n) is chosen based on T.

Variant generalize term+: This is equivalent to generalize term; ... ; generalize term. Note that the sequence of term _i 's are processed from n to 1.

Variant generalize term at natural+: This is equivalent to generalize term but it generalizes only over the specified occurrences of term (counting from left to right on the expression printed using the Printing All flag).

Variant generalize term as ident: This is equivalent to generalize term but it uses ident to name the generalized hypothesis.

Variant generalize term at natural+ as ident+,: This is the most general form of generalize that combines the previous behaviors.

Variant generalize dependent term: This generalizes term but also all hypotheses that depend on term. It clears the generalized hypotheses.

Tactic evar (ident : term)¶: The evar tactic creates a new local definition named ident with type term in the context. The body of this binding is a fresh existential variable.

Tactic instantiate (ident := term )¶: The instantiate tactic refines (see refine) an existential variable ident with the term term. It is equivalent to only [ident]: refine term (preferred alternative).

Note

To be able to refer to an existential variable by name, the user must have given the name explicitly (see Existential variables).

Note

When you are referring to hypotheses which you did not name explicitly, be aware that Coq may make a different decision on how to name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors.

Variant instantiate (natural := term): This variant selects an existential variable by its position. The natural argument is the position of the existential variable from right to left in the conclusion of the goal. (Use one of the variants below to select an existential variable in a hypothesis.) Counting starts at 1 and multiple occurrences of the same existential variable are counted multiple times. Because this variant is not robust to slight changes in the goal, its use is strongly discouraged.

Variant instantiate ( natural := term ) in ident
Variant instantiate ( natural := term ) in ( value of ident )
Variant instantiate ( natural := term ) in ( type of ident ): These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition (named ident).

Variant instantiate: Without argument, the instantiate tactic tries to solve as many existential variables as possible, using information gathered from other tactics in the same tactical. This is automatically done after each complete tactic (i.e. after a dot in proof mode), but not, for example, between each tactic when they are sequenced by semicolons.

Tactic admit¶: This tactic allows temporarily skipping a subgoal so as to progress further in the rest of the proof. A proof containing admitted goals cannot be closed with Qed but only with Admitted.

Variant give_up: Synonym of admit.

Tactic absurd term¶: This tactic applies to any goal. The argument term is any proposition P of type Prop. This tactic applies False elimination, that is it deduces the current goal from False, and generates as subgoals ∼P and P. It is very useful in proofs by cases, where some cases are impossible. In most cases, P or ∼P is one of the hypotheses of the local context.

Tactic contradiction¶

This tactic applies to any goal. The contradiction tactic attempts to find in the current context (after all intros) a hypothesis that is equivalent to an empty inductive type (e.g. False), to the negation of a singleton inductive type (e.g. True or x=x), or two contradictory hypotheses.

Error No such assumption.¶

Variant contradiction ident: The proof of False is searched in the hypothesis named ident.

Tactic contradict ident¶

This tactic allows manipulating negated hypothesis and goals. The name ident should correspond to a hypothesis. With contradict H, the current goal and context is transformed in the following way:

H:¬A ⊢ B becomes ⊢ A
H:¬A ⊢ ¬B becomes H: B ⊢ A
H: A ⊢ B becomes ⊢ ¬A
H: A ⊢ ¬B becomes H: B ⊢ ¬A

Tactic exfalso¶: This tactic implements the “ex falso quodlibet” logical principle: an elimination of False is performed on the current goal, and the user is then required to prove that False is indeed provable in the current context. This tactic is a macro for elimtype False.

Case analysis and induction¶

The tactics presented in this section implement induction or case analysis on inductive or co-inductive objects (see Theory of inductive definitions).

Tactic destruct term¶

This tactic applies to any goal. The argument term must be of inductive or co-inductive type and the tactic generates subgoals, one for each possible form of term, i.e. one for each constructor of the inductive or co-inductive type. Unlike induction, no induction hypothesis is generated by destruct.

Variant destruct ident

If ident denotes a quantified variable of the conclusion of the goal, then destruct ident behaves as intros until ident; destruct ident. If ident is not anymore dependent in the goal after application of destruct, it is erased (to avoid erasure, use parentheses, as in destruct (ident)).

If ident is a hypothesis of the context, and ident is not anymore dependent in the goal after application of destruct, it is erased (to avoid erasure, use parentheses, as in destruct (ident)).

Variant destruct natural: destruct natural behaves as intros until natural followed by destruct applied to the last introduced hypothesis.

Note

For destruction of a number, use syntax destruct (natural) (not very interesting anyway).

Variant destruct pattern: The argument of destruct can also be a pattern of which holes are denoted by “_”. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are compatible and performs case analysis using this subterm.

Variant destruct term+,: This is a shortcut for destruct term; ...; destruct term.

Variant destruct term as or_and_intropattern_loc: This behaves as destruct term but uses the names in or_and_intropattern_loc to name the variables introduced in the context. The or_and_intropattern_loc must have the form [p11 ... p1n | ... | pm1 ... pmn ] with m being the number of constructors of the type of term. Each variable introduced by destruct in the context of the i-th goal gets its name from the list pi1 ... pin in order. If there are not enough names, destruct invents names for the remaining variables to introduce. More generally, the pij can be any introduction pattern (see intros). This provides a concise notation for chaining destruction of a hypothesis.

Variant destruct term eqn:naming_intropattern¶: This behaves as destruct term but adds an equation between term and the value that it takes in each of the possible cases. The name of the equation is specified by naming_intropattern (see intros), in particular ? can be used to let Coq generate a fresh name.

Variant destruct term with bindings: This behaves like destruct term providing explicit instances for the dependent premises of the type of term.

Variant edestruct term¶: This tactic behaves like destruct term except that it does not fail if the instance of a dependent premises of the type of term is not inferable. Instead, the unresolved instances are left as existential variables to be inferred later, in the same way as eapply does.

Variant destruct term using term with bindings?: This is synonym of induction term using term with bindings?.

Variant destruct term in goal_occurrences: This syntax is used for selecting which occurrences of term the case analysis has to be done on. The in goal_occurrences clause is an occurrence clause whose syntax and behavior is described in occurrences sets.

Variant destruct term with bindings? as or_and_intropattern_loc? eqn:naming_intropattern? using term with bindings?? in goal_occurrences?
Variant edestruct term with bindings? as or_and_intropattern_loc? eqn:naming_intropattern? using term with bindings?? in goal_occurrences?: These are the general forms of destruct and edestruct. They combine the effects of the with, as, eqn:, using, and in clauses.

Tactic case term¶: The tactic case is a more basic tactic to perform case analysis without recursion. It behaves as elim term but using a case-analysis elimination principle and not a recursive one.

Variant case term with bindings: Analogous to elim term with bindings above.

Variant ecase term with bindings?¶: In case the type of term has dependent premises, or dependent premises whose values are not inferable from the with bindings clause, ecase turns them into existential variables to be resolved later on.

Variant simple destruct ident¶: This tactic behaves as intros until ident; case ident when ident is a quantified variable of the goal.

Variant simple destruct natural: This tactic behaves as intros until natural; case ident where ident is the name given by intros until natural to the natural -th non-dependent premise of the goal.

Variant case_eq term: The tactic case_eq is a variant of the case tactic that allows to perform case analysis on a term without completely forgetting its original form. This is done by generating equalities between the original form of the term and the outcomes of the case analysis.

Tactic induction term¶

This tactic applies to any goal. The argument term must be of inductive type and the tactic induction generates subgoals, one for each possible form of term, i.e. one for each constructor of the inductive type.

If the argument is dependent in either the conclusion or some hypotheses of the goal, the argument is replaced by the appropriate constructor form in each of the resulting subgoals and induction hypotheses are added to the local context using names whose prefix is IH.

There are particular cases:

If term is an identifier ident denoting a quantified variable of the conclusion of the goal, then inductionident behaves as intros until ident; induction ident. If ident is not anymore dependent in the goal after application of induction, it is erased (to avoid erasure, use parentheses, as in induction (ident)).
If term is a natural, then induction natural behaves as intros until natural followed by induction applied to the last introduced hypothesis.

Note

For simple induction on a number, use syntax induction (number) (not very interesting anyway).
In case term is a hypothesis ident of the context, and ident is not anymore dependent in the goal after application of induction, it is erased (to avoid erasure, use parentheses, as in induction (ident)).
The argument term can also be a pattern of which holes are denoted by “_”. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are compatible and performs induction using this subterm.

Example

Lemma induction_test : forall n:nat, n = n -> n <= n.: 1 subgoal ============================ forall n : nat, n = n -> n <= n
intros n H.: 1 subgoal n : nat H : n = n ============================ n <= n
induction n.: 2 subgoals H : 0 = 0 ============================ 0 <= 0 subgoal 2 is: S n <= S n
exact (le_n 0).: 1 subgoal n : nat H : S n = S n IHn : n = n -> n <= n ============================ S n <= S n

Error Not an inductive product.¶

Error Unable to find an instance for the variables ident ... ident.¶: Use in this case the variant elim … with below.

Variant induction term as or_and_intropattern_loc: This behaves as induction but uses the names in or_and_intropattern_loc to name the variables introduced in the context. The or_and_intropattern_loc must typically be of the form [ p ₁₁ ... p _1n | ... | p_m1 ... p_mn ] with m being the number of constructors of the type of term. Each variable introduced by induction in the context of the i-th goal gets its name from the list p_i1 ... p_in in order. If there are not enough names, induction invents names for the remaining variables to introduce. More generally, the p_ij can be any disjunctive/conjunctive introduction pattern (see intros …). For instance, for an inductive type with one constructor, the pattern notation (p₁ , ... , p_n ) can be used instead of [ p₁ ... p_n ].

Variant induction term with bindings: This behaves like induction providing explicit instances for the premises of the type of term (see Bindings).

Variant einduction term¶: This tactic behaves like induction except that it does not fail if some dependent premise of the type of term is not inferable. Instead, the unresolved premises are posed as existential variables to be inferred later, in the same way as eapply does.

Variant induction term using term¶: This behaves as induction but using term as induction scheme. It does not expect the conclusion of the type of the first term to be inductive.

Variant induction term using term with bindings: This behaves as induction … using … but also providing instances for the premises of the type of the second term.

Variant induction term+, using qualid: This syntax is used for the case qualid denotes an induction principle with complex predicates as the induction principles generated by Function or Functional Scheme may be.

Variant induction term in goal_occurrences

This syntax is used for selecting which occurrences of term the induction has to be carried on. The in goal_occurrences clause is an occurrence clause whose syntax and behavior is described in occurrences sets. If variables or hypotheses not mentioning term in their type are listed in goal_occurrences, those are generalized as well in the statement to prove.

Example

Lemma comm x y : x + y = y + x.: 1 subgoal x, y : nat ============================ x + y = y + x
induction y in x |- *.: 2 subgoals x : nat ============================ x + 0 = 0 + x subgoal 2 is: x + S y = S y + x
Show 2.: subgoal 2 is: x, y : nat IHy : forall x : nat, x + y = y + x ============================ x + S y = S y + x

Variant induction term with bindings as or_and_intropattern_loc using term with bindings in goal_occurrences
Variant einduction term with bindings as or_and_intropattern_loc using term with bindings in goal_occurrences: These are the most general forms of induction and einduction. It combines the effects of the with, as, using, and in clauses.

Variant elim term¶: This is a more basic induction tactic. Again, the type of the argument term must be an inductive type. Then, according to the type of the goal, the tactic elim chooses the appropriate destructor and applies it as the tactic apply would do. For instance, if the local context contains n:nat and the current goal is T of type Prop, then elim n is equivalent to apply nat_ind with (n:=n). The tactic elim does not modify the context of the goal, neither introduces the induction loading into the context of hypotheses. More generally, elim term also works when the type of term is a statement with premises and whose conclusion is inductive. In that case the tactic performs induction on the conclusion of the type of term and leaves the non-dependent premises of the type as subgoals. In the case of dependent products, the tactic tries to find an instance for which the elimination lemma applies and fails otherwise.

Variant elim term with bindings¶: Allows to give explicit instances to the premises of the type of term (see Bindings).

Variant eelim term¶: In case the type of term has dependent premises, this turns them into existential variables to be resolved later on.

Variant elim term using term
Variant elim term using term with bindings: Allows the user to give explicitly an induction principle term that is not the standard one for the underlying inductive type of term. The bindings clause allows instantiating premises of the type of term.

Variant elim term with bindings using term with bindings
Variant eelim term with bindings using term with bindings: These are the most general forms of elim and eelim. It combines the effects of the using clause and of the two uses of the with clause.

Variant elimtype type¶: The argument type must be inductively defined. elimtype I is equivalent to cut I. intro Hn; elim Hn; clear Hn. Therefore the hypothesis Hn will not appear in the context(s) of the subgoal(s). Conversely, if t is a term of (inductive) type I that does not occur in the goal, then elim t is equivalent to elimtype I; 2:exact t.

Variant simple induction ident¶: This tactic behaves as intros until ident; elim ident when ident is a quantified variable of the goal.

Variant simple induction natural: This tactic behaves as intros until natural; elim ident where ident is the name given by intros until natural to the natural-th non-dependent premise of the goal.

Tactic double induction ident ident¶: This tactic is deprecated and should be replaced by induction ident; induction ident (or induction ident ; destruct ident depending on the exact needs).

Variant double induction natural₁ natural₂: This tactic is deprecated and should be replaced by induction num1; induction num3 where num3 is the result of num2 - num1

Tactic dependent induction ident¶: The experimental tactic dependent induction performs induction- inversion on an instantiated inductive predicate. One needs to first require the Coq.Program.Equality module to use this tactic. The tactic is based on the BasicElim tactic by Conor McBride [McB00] and the work of Cristina Cornes around inversion [CT95]. From an instantiated inductive predicate and a goal, it generates an equivalent goal where the hypothesis has been generalized over its indexes which are then constrained by equalities to be the right instances. This permits to state lemmas without resorting to manually adding these equalities and still get enough information in the proofs.

Example

Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.: 1 subgoal ============================ forall n : nat, n < 1 -> n = 0
intros n H ; induction H.: 2 subgoals n : nat ============================ n = 0 subgoal 2 is: n = 0

Here we did not get any information on the indexes to help fulfill this proof. The problem is that, when we use the induction tactic, we lose information on the hypothesis instance, notably that the second argument is 1 here. Dependent induction solves this problem by adding the corresponding equality to the context.

Require Import Coq.Program.Equality.
Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.: 1 subgoal ============================ forall n : nat, n < 1 -> n = 0
intros n H ; dependent induction H.: 2 subgoals ============================ 0 = 0 subgoal 2 is: n = 0

The subgoal is cleaned up as the tactic tries to automatically simplify the subgoals with respect to the generated equalities. In this enriched context, it becomes possible to solve this subgoal.

reflexivity.: 1 subgoal n : nat H : S n <= 0 IHle : 0 = 1 -> n = 0 ============================ n = 0

Now we are in a contradictory context and the proof can be solved.

inversion H.: No more subgoals.

This technique works with any inductive predicate. In fact, the dependent induction tactic is just a wrapper around the induction tactic. One can make its own variant by just writing a new tactic based on the definition found in Coq.Program.Equality.

Variant dependent induction ident generalizing ident+: This performs dependent induction on the hypothesis ident but first generalizes the goal by the given variables so that they are universally quantified in the goal. This is generally what one wants to do with the variables that are inside some constructors in the induction hypothesis. The other ones need not be further generalized.

Variant dependent destruction ident¶: This performs the generalization of the instance ident but uses destruct instead of induction on the generalized hypothesis. This gives results equivalent to inversion or dependent inversion if the hypothesis is dependent.

See also the larger example of dependent induction and an explanation of the underlying technique.

Checking properties of terms¶

Each of the following tactics acts as the identity if the check succeeds, and results in an error otherwise.

Tactic constr_eq term term¶: This tactic checks whether its arguments are equal modulo alpha conversion, casts and universe constraints. It may unify universes.

Error Not equal.¶

Error Not equal (due to universes).¶

Tactic constr_eq_strict term term¶: This tactic checks whether its arguments are equal modulo alpha conversion, casts and universe constraints. It does not add new constraints.

Error Not equal.¶

Error Not equal (due to universes).¶

Tactic unify term term¶: This tactic checks whether its arguments are unifiable, potentially instantiating existential variables.

Error Unable to unify term with term.¶

Variant unify term term with ident: Unification takes the transparency information defined in the hint database ident into account (see the hints databases for auto and eauto).

Tactic is_evar term¶: This tactic checks whether its argument is a current existential variable. Existential variables are uninstantiated variables generated by eapply and some other tactics.

Error Not an evar.¶

Tactic has_evar term¶: This tactic checks whether its argument has an existential variable as a subterm. Unlike context patterns combined with is_evar, this tactic scans all subterms, including those under binders.

Error No evars.¶

Tactic is_var term¶: This tactic checks whether its argument is a variable or hypothesis in the current local context.

Error Not a variable or hypothesis.¶

Equality¶

Tactic f_equal¶: This tactic applies to a goal of the form f a₁ ... a_n = f′a′₁ ... a′_n. Using f_equal on such a goal leads to subgoals f=f′ and a₁ = a′₁ and so on up to a_n = a′_n. Amongst these subgoals, the simple ones (e.g. provable by reflexivity or congruence) are automatically solved by f_equal.

Tactic reflexivity¶

This tactic applies to a goal that has the form t=u. It checks that t and u are convertible and then solves the goal. It is equivalent to apply refl_equal.

Error The conclusion is not a substitutive equation.¶

Error Unable to unify ... with ...¶

Tactic symmetry¶: This tactic applies to a goal that has the form t=u and changes it into u=t.

Variant symmetry in ident: If the statement of the hypothesis ident has the form t=u, the tactic changes it to u=t.

Tactic transitivity term¶

This tactic applies to a goal that has the form t=u and transforms it into the two subgoals t=term and term=u.

Variant etransitivity: This tactic behaves like transitivity, using a fresh evar instead of a concrete term.

Equality and inductive sets¶

We describe in this section some special purpose tactics dealing with equality and inductive sets or types. These tactics use the equality eq:forall (A:Type), A->A->Prop, simply written with the infix symbol =.

Tactic decide equality¶: This tactic solves a goal of the form forall x y : R, {x = y} + {~ x = y}, where R is an inductive type such that its constructors do not take proofs or functions as arguments, nor objects in dependent types. It solves goals of the form {x = y} + {~ x = y} as well.

Tactic compare term term¶: This tactic compares two given objects term and term of an inductive datatype. If G is the current goal, it leaves the sub- goals term =term -> G and ~ term = term -> G. The type of term and term must satisfy the same restrictions as in the tactic decide equality.

Tactic simplify_eq term¶: Let term be the proof of a statement of conclusion term = term. If term and term are structurally different (in the sense described for the tactic discriminate), then the tactic simplify_eq behaves as discriminate term, otherwise it behaves as injection term.

Note

If some quantified hypothesis of the goal is named ident, then simplify_eq ident first introduces the hypothesis in the local context using intros until ident.

Variant simplify_eq natural: This does the same thing as intros until natural then simplify_eq ident where ident is the identifier for the last introduced hypothesis.

Variant simplify_eq term with bindings: This does the same as simplify_eq term but using the given bindings to instantiate parameters or hypotheses of term.

Variant esimplify_eq natural¶
Variant esimplify_eq term with bindings?¶: This works the same as simplify_eq but if the type of term, or the type of the hypothesis referred to by natural, has uninstantiated parameters, these parameters are left as existential variables.

Variant simplify_eq: If the current goal has form t1 <> t2, it behaves as intro ident; simplify_eq ident.

Tactic dependent rewrite -> ident¶: This tactic applies to any goal. If ident has type (existT B a b)=(existT B a' b') in the local context (i.e. each term of the equality has a sigma type { a:A & (B a)}) this tactic rewrites a into a' and b into b' in the current goal. This tactic works even if B is also a sigma type. This kind of equalities between dependent pairs may be derived by the injection and inversion tactics.

Variant dependent rewrite <- ident¶: Analogous to dependent rewrite -> but uses the equality from right to left.

Classical tactics¶

In order to ease the proving process, when the Classical module is loaded, a few more tactics are available. Make sure to load the module using the Require Import command.

Tactic classical_left¶
Tactic classical_right¶: These tactics are the analog of left and right but using classical logic. They can only be used for disjunctions. Use classical_left to prove the left part of the disjunction with the assumption that the negation of right part holds. Use classical_right to prove the right part of the disjunction with the assumption that the negation of left part holds.

Delaying solving unification constraints¶

Tactic solve_constraints¶

Flag Solve Unification Constraints¶: By default, after each tactic application, postponed typechecking unification problems are resolved using heuristics. Unsetting this flag disables this behavior, allowing tactics to leave unification constraints unsolved. Use the solve_constraints tactic at any point to solve the constraints.

Proof maintenance¶

Experimental. Many tactics, such as intros, can automatically generate names, such as "H0" or "H1" for a new hypothesis introduced from a goal. Subsequent proof steps may explicitly refer to these names. However, future versions of Coq may not assign names exactly the same way, which could cause the proof to fail because the new names don't match the explicit references in the proof.

The following "Mangle Names" settings let users find all the places where proofs rely on automatically generated names, which can then be named explicitly to avoid any incompatibility. These settings cause Coq to generate different names, producing errors for references to automatically generated names.

Flag Mangle Names¶: When set, generated names use the prefix specified in the following option instead of the default prefix.

Option Mangle Names Prefix string¶: Specifies the prefix to use when generating names.

Performance-oriented tactic variants¶

Tactic exact_no_check term¶

For advanced usage. Similar to exact term, but as an optimization, it skips checking that term has the goal's type, relying on the kernel check instead. See change_no_check for more explanation.

Example

Goal False.: 1 subgoal ============================ False
exact_no_check I.: No more subgoals.
Fail Qed.: The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False".

Variant vm_cast_no_check term¶

For advanced usage. Similar to exact_no_check term, but additionally instructs the kernel to use vm_compute to compare the goal's type with the term's type.

Example

Goal False.: 1 subgoal ============================ False
vm_cast_no_check I.: No more subgoals.
Fail Qed.: The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False".

Variant native_cast_no_check term¶

for advanced usage. similar to exact_no_check term, but additionally instructs the kernel to use native_compute to compare the goal's type with the term's type.

Example

Goal False.: 1 subgoal ============================ False
native_cast_no_check I.: No more subgoals.
Fail Qed.: The command has indeed failed with message: Native compiler is disabled, falling back to VM conversion test. [native-compiler-disabled,native-compiler]

1: Actually, only the second subgoal will be generated since the other one can be automatically checked.
2: This corresponds to the cut rule of sequent calculus.
3: Reminder: opaque constants will not be expanded by δ reductions.