\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \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}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \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{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#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 primarily 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¶

Tactics 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.

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 specify the values to assign unbound variables in a term. Bindings can be given by position or name. Generally these appear in the form one_term_with_bindings or with bindings, depending on the tactic.

one_term_with_bindings::=one_term with bindings?bindings::=one_term+|( identnatural := term )+

one_term with bindings? — bindings for variables in one_term are typically determined by unifying one_term with a tactic-dependent part of the context, with any remaining unbound variables provided by the bindings.
one_term+ — binds free variables in the left-to-right order of their first appearance in the relevant term.

For some tactics, bindings for all free variables must be provided, such as for induction, destruct, elim and case. Other tactics automatically generate some or all of the bindings from the conclusion or a hypothesis, such as apply and constructor and its variants. In this case, only instances for the dependent premises that are not bound in the conclusion of the relevant term are required (and permitted).
( identnatural := term )+ — binds variables by name (if ident is given), or by unifying with the n-th premise of the relevant term (if natural is given).

Error No such binder.¶: natural is 0 or more than the number of unbound variables.

Error No such bound variable ident (no bound variables at all in the expression).¶

Error No such bound variable ident₁ (possible names are: ident₂ ...).¶: The specified binder name ident₁ is not used in the one_term. ident₂ ... lists all the valid binder names.

Error Not the right number of missing arguments (expected natural).¶: Generated when the first form of bindings doesn't have the expected number of 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, while intros and eintros use intropattern*. 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 generate a fresh 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*+| ] — splits an inductive type that has multiple constructors such as A \/ B into multiple subgoals. The number of intropatterns 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 dependent premises from the result until there are no more. Example
** — introduces one or more dependent or non-dependent premises from the result until there are no more premises. intros ** is equivalent to intros. Example
simple_intropattern_closed % term* — first applies each of the terms with the apply tactic on the hypothesis to be introduced, then it uses simple_intropattern_closed. Example

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 goal ============================ forall A B : Prop, A /\ B -> True

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

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

Example: intro pattern for \/

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

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

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

Example: -> intro pattern

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

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

intros ->.
1 goal 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 goal ============================ forall n m : nat, S n = S m -> 1 = 2 -> False

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

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

intros [=].
No more goals.

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 goal ============================ A /\ (exists x : nat, B x /\ C) -> True

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

Example: * intro pattern

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

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

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

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

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

Example: compound intro pattern

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

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

all: swap 1 2.
2 goals A, B, C : Prop c : C f : A -> C ============================ C goal 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 goal A : Type xs, ys : list A ============================ S (length ys) = 1 -> xs ++ ys = xs

intros [=->%length_zero_iff_nil].
1 goal 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_occurrencessimple_occurrences::=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.

simple_occurrences
A semantically restricted form of occurrences that doesn't allow the at clause anywhere within it.

-? 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.

When rewriting in multiple hypotheses, they must not appear in the term to rewrite. For instance rewrite H in H,H' is an error. If an hypothesis appears only through a hole, it will be removed from that hole's context.

With rewrite term in *, hypotheses on which the dependency cannot be avoided are skipped, for instance rewrite H in * skips rewriting in H. This is the case even if only one hypothesis ends up rewritten.

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.

Error No such hypothesis: ident.¶

Applying theorems¶

Tactic exact one_term¶

Directly gives the exact proof term for the goal. exact p succeeds if and only if one_term and the type of p are unifiable (see Conversion rules).

Error Not an exact proof.¶

Tactic eexact one_term¶: Behaves like exact but can 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.¶

Tactic eassumption¶: Behaves like assumption but is able to process goals and hypotheses with existential variables. It can also resolve existential variables, which assumption will not.

Tactic simple? notypeclasses? refine one_term¶

Behaves like exact but allows holes (denoted by _ or (_ : type)) in one_term. refine generates as many subgoals as there are remaining holes in the elaborated term. Any subgoal that occurs in other subgoals is automatically shelved, as if calling shelve_unifiable.

simple: If specified, don't shelve any subgoals or perform beta reduction.
notypeclasses: If specified, do checking without resolving typeclasses. The generated subgoals (shelved or not) are not candidates for typeclass resolution, even if they have a typeclass type as their conclusion.

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 goal ============================ forall x : Option, x <> Fail -> bool
refine (fun x:Option => match x return x <> Fail -> bool with | Fail => _ | Ok b => fun _ => b end).: 1 goal x : Option ============================ Fail <> Fail -> bool
intros; absurd (Fail = Fail); trivial.: No more goals.
Defined.

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.

Setting Debug "unification" enables printing traces of unification steps used during elaboration/typechecking and the refine tactic. "ho-unification" prints information about higher order heuristics.

Tactic apply one_term_with_bindings+, in_hyp_as?¶

in_hyp_as::=in ident as_ipat?+,as_ipat::=as simple_intropattern

Uses unification to match the type of each one_term (in one_term_with_bindings) with the goal (to do backward reasoning) or with a hypothesis (to do forward reasoning). Specifying multiple one_term_with_bindings is equivalent to giving each one serially, left to right, as separate apply tactics.

The type of one_term contains zero or more premises followed by a conclusion, i.e. it typically has the form forall open_binders ,? term_premise ->* term_conclusion. (The foralls may also be interleaved with the premises, but common usage is to equivalently gather them at the beginning of the one_term.) Backward reasoning with a one_term whose type is, for example, A -> B replaces an as-yet unproven goal B with A. Forward reasoning with the same one_term changes a hypothesis with type A to B. (Hypotheses are considered proven propositions within the context that contains them.)

Unification creates a map from the variables in the type of one_term to matching subterms of the goal or hypothesis. The matching subterms are then substituted into the type of one_term when generating the updated goal or hypothesis. Unmatched premises become new subgoals with similar substitutions. If no match is found, the tactic fails.

Setting Debug "tactic-unification" enables printing traces of unification steps in tactic unification. Tactic unification is used in tactics such as apply and rewrite.

The goal and hypothesis cases are described separately for clarity.

one_term (inside one_term_with_bindings)
If one_term is an ident, it is the name of a theorem, lemma or hypothesis whose type is given in the theorem statement or shown in the context. Otherwise it is a proof term whose type can be displayed with Check one_term.

Without in_hyp_as (the goal case)
If the goal matches all of the type of one_term (both premises and the conclusion), the tactic proves the goal. Otherwise, the tactic matches the goal against the conclusion of one_term and, if possible, one or more premises (from right to left). If the match succeeds, the tactic replaces the current goal with a subgoal for each unmatched premise of the type of one_term. This example matches only the conclusion, while this one also matches a premise.

If the conclusion of the type of one_term does not match the goal and the conclusion is an inductive type with a single constructor, then each premise in the constructor is recursively matched to the goal in right-to-left order and the first match is used. In this case, the tactic will not match premises that would result in applying a lemma of the form forall A, … -> A. See example here.

The goal case uses 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 target. If the target is of the form Q u₁ … u_n and the t_i and u_i unify, then P is instantiated into Q. Otherwise, apply tries to define P by abstracting over t₁ … t_n in the target. You can use pattern to transform the target so that it gets the form (fun x₁ … x_n => Q) u₁ … u_n. See the example here.

in_hyp_as (the hypothesis case)
Proceeding from right to left, find the first premise of the type of one_term that matches the specified hypothesis. If a match is found, the hypothesis is replaced with the conclusion of the type of one_term (substituting for the unified variables) and the tactic creates a new subgoal for each unmatched premise. See the example here.

If specified, as simple_intropattern is applied to the conclusion of the type of one_term. In this case, the selected hypothesis is left unchanged if its name is not reused.

If the type of one_term is an inductive type with a single constructor, then each premise in the constructor is recursively matched to the conclusion of the hypothesis in right-to-left order and the first match is used. See example here.

For the hypothesis case, matching is done only with first-order unification.

with bindings (in one_term_with_bindings)
Gives explicit instantiations for variables used in the type of one_term. There are 3 cases:

Bindings for variables can be provided in a list of one_terms in the left-to-right order of their first appearance in the type of one_term. For the goal case (example), the list should give bindings only for variables that aren't bound by unification. However, in the hypothesis case (example), the list must include bindings for all variables.

Bindings for unbound variables can be given by name with the (ident := term) form.

The form (natural := term) binds additional variables by unifying the Nth premise of the type of one_term with term. (Use 1 for the first premise.)

Error Unable to unify one_term with one_term.¶

The apply tactic failed to match the conclusion of one_term. You can help apply by transforming your goal with the change or pattern tactics.

Error Unable to apply lemma of type "..." on hypothesis of type "...".¶

This happens if the conclusion of ident does not match any of the premises of the type of one_term.

Error Unable to find an instance for the variables ident+.¶

This occurs when some instantiations of the premises of one_term are not deducible from the unification. This is the case, for instance, when you want to apply a transitivity property. To fix this, add bindings for the idents using to with bindings or use eapply.

Example: Backward reasoning in the goal with apply

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

intros A B C H.
1 goal A, B, C : Prop H : A -> B -> C ============================ C

apply H. (* replace goal with new goals for unmatched premises of H *)
2 goals A, B, C : Prop H : A -> B -> C ============================ A goal 2 is: B

Example: Backward reasoning in the goal with apply including a premise

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

intros A B C H.
1 goal A, B, C : Prop H : A -> B -> C ============================ B -> C

apply H. (* match on "B -> C", replace goal with "A" *)
1 goal A, B, C : Prop H : A -> B -> C ============================ A

Example: Forward reasoning in hypotheses with apply

Goal forall A B C: Prop, B -> (A -> B -> C) -> True.
1 goal ============================ forall A B C : Prop, B -> (A -> B -> C) -> True

intros A B C H0 H1.
1 goal A, B, C : Prop H0 : B H1 : A -> B -> C ============================ True

apply H1 in H0. (* change H0, create new goals for unmatched premises of H1 *)
2 goals A, B, C : Prop H0 : C H1 : A -> B -> C ============================ True goal 2 is: A

Example: Apply a theorem with a binding in a goal

apply unifies the conclusion n <= p of the theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p with the goal, assigning x * x and y * y in the goal to, repectively, n and p in theorem (backward reasoning). The with clause provides the binding for m:

Require Import PeanoNat.

Goal forall (x y : nat), x <= y -> x * x <= y * y.
1 goal ============================ forall x y : nat, x <= y -> x * x <= y * y

intros x y H0.
1 goal x, y : nat H0 : x <= y ============================ x * x <= y * y

apply Nat.le_trans with (y * x).
2 goals x, y : nat H0 : x <= y ============================ x * x <= y * x goal 2 is: y * x <= y * y

Example: Apply a theorem with a binding in a hypothesis

When applying a theorem in a hypothesis, apply unifies the hypothesis with one of the premises of the theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. In this case, it unifies with the first premise (n <= m) and assigns x * x and y * y to, respectively, n and m in the theorem (forward reasoning). The with clause provides the binding for p.

In addition, apply in a hypothesis isn't as flexible as apply in the goal: for hypotheses, the unbound variable can be bound by name (as shown) or values for all the variables can be given positionally, i.e. apply Nat.le_trans with (x * x) (y * y) (y * x) in H.

Require Import PeanoNat.

Goal forall (x y : nat), x * x <= y * y -> x <= y.
1 goal ============================ forall x y : nat, x * x <= y * y -> x <= y

intros x y H.
1 goal x, y : nat H : x * x <= y * y ============================ x <= y

apply Nat.le_trans with (p := y * x) in H.
2 goals x, y : nat H : x * x <= y * x ============================ x <= y goal 2 is: y * y <= y * x

Example: Applying theorems with <->

A <-> B is defined as (A -> B) /\ (B -> A). /\ represents an inductive type with a single constructor: Inductive and (C D:Prop) : Prop := conj : C -> D -> D /\ C. The premises of conj are C and D. The tactic uses the first matching constructor premise in right-to-left order.

Theorems that use <-> to state a logical equivalence behave consistently when applied to goals and hypotheses.

Goal forall (A B: Prop) (H1: A <-> B) (H: A), A.
1 goal ============================ forall A B : Prop, A <-> B -> A -> A

intros A B H1 H.
1 goal A, B : Prop H1 : A <-> B H : A ============================ A

apply H1.
1 goal A, B : Prop H1 : A <-> B H : A ============================ B

apply H1 in H.
1 goal A, B : Prop H1 : A <-> B H : B ============================ B

Example: Special case of second-order unification in apply

Shows the use of the special case second-order unification described here (after "unless").

Note that we usually use induction rather than applying nat_ind directly.

Goal forall x y, x + y = y + x.
1 goal ============================ forall x y : nat, x + y = y + x

intros.
1 goal x, y : nat ============================ x + y = y + x

Check nat_ind.
nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

apply nat_ind. (* Notice the goals are unprovable. *)
2 goals x, y : nat ============================ x + y = 0 goal 2 is: forall n : nat, x + y = n -> x + y = S n

Show Proof. (* apply has instantiated P with (eq (x + y)) because the goal was (eq (x + y) (y + x)) and n could be unified with (y + x) *)
(fun x y : nat => nat_ind (eq (x + y)) ?Goal ?Goal0 (y + x))

(* However, we can use the pattern tactic to get the instantiation we want: *)
Undo.
1 goal x, y : nat ============================ x + y = y + x

pattern x.
1 goal x, y : nat ============================ (fun n : nat => n + y = y + n) x

apply nat_ind.
2 goals x, y : nat ============================ 0 + y = y + 0 goal 2 is: forall n : nat, n + y = y + n -> S n + y = y + S n

Show Proof. (* apply has instantiated P with (fun n : nat => n + y = y + n) and the goal can be proven *)
(fun x y : nat => nat_ind (fun n : nat => n + y = y + n) ?Goal ?Goal0 x : x + y = y + x)

Tactic eapply one_term_with_bindings+, in_hyp_as?¶

Behaves like apply, but creates existential variables when Coq is unable to deduce instantiations for variables, rather than failing.

Tactic rapply one_term¶

Behaves like eapply but uses the proof engine of refine to handle existential variables, holes and conversion problems. This may result in slightly different behavior regarding which conversion problems are solvable. However, rapply fails if any holes remain in one_term itself after typechecking and typeclass resolution but before unification with the goal. Note that rapply tries to instantiate as many hypotheses of one_term as possible. As a result, if it is possible to apply one_term to arbitrarily many arguments without getting a type error, rapply will loop.

Note that you must Require Import Coq.Program.Tactics to use rapply.

Tactic simple apply one_term_with_bindings+, in_hyp_as?¶

Behaves like apply but it reasons modulo conversion only on subterms that contain no variables to instantiate and does not traverse tuples. For instance, the following example fails because it would require converting 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 goal ============================ 0 = 0

Fail simple apply H.
The command has indeed failed with message: Unable to unify "id ?M150 = ?M151" with "0 = 0".

Because it reasons modulo a limited amount of conversion, simple apply fails faster than apply and it is thus well-suited for use in user-defined tactics that backtrack often.

Tactic simple eapply one_term_with_bindings+, in_hyp_as?¶

Tactic lapply one_term¶

Splits a one_term in the goal reducible to the form A -> B, replacing it with two new subgoals A and B -> G. lapply H (where H is A -> B and B does not start with a product) is equivalent to cut B. 2:apply H..

Error lapply needs a non-dependent 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 goal ============================ 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 goals ============================ R n m goal 2 is: R m p

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

apply (Rtrans _ m).: 2 goals ============================ R n m goal 2 is: R m p

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

apply Rtrans with (y := m).: 2 goals ============================ R n m goal 2 is: R m p

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

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

… or the proof of (R y z).

apply Rtrans with (2 := Rmp).: 1 goal ============================ 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 goals (shelved: 1) ============================ R n ?y goal 2 is: R ?y p
apply Rnm.: 1 goal ============================ R m p
apply Rmp.: No more goals.

Managing the local context¶

Tactic intro ident? where?¶

Applies the hnf tactic until it finds an item that can be introduced in the context by removing certain constructs in the goal. If no item is found, the tactic fails. The name used is ident (if specified) or from the construct, except that if the name from the construct already exists in the local context, Coq uses a fresh name instead. The constructs have these forms: (See examples here.)

forall x : T, term: x : T is a dependent premise. Removes forall x : T, from the goal and adds x : T to the context.
A -> …: A is a non-dependent premise. Removes A -> from the goal and adds H : A to the context.
let x := c, term: Removes let x := c, from the goal and adds x := c : T to the context.

We recommend always specifying ident so that the names of hypotheses don't change as the proof is updated, making your proof easier to maintain. For example, if H exists in the context, Coq will consider using H0, H1, ... until it finds an unused name. Modifications to a proof can change automatically assigned names that subsequent tactics likely refer to, making the proofs harder to maintain. The Mangle Names flag gives some control over how fresh names are generated (see Proof maintenance).

Note that intros lets you introduce multiple items into the context with a single tactic.

ident
The name to give to the introduced item. If not given, Coq uses the variable name from the forall or H for premises. If a name such as H is already in use, Coq will consider using H0, H1, ... until it finds a fresh name.

Note

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

where
Indicates where to place the introduced hypothesis: at the top or bottom of the context or before or after another specified hypothesis. The default is at bottom.

Error ident is already used.¶

The provided ident is already used in the local context.

Error No product even after head-reduction.¶

There is nothing to introduce even after hnf has been completely applied.

Example: intro and intros

Goal forall m n, m < n -> (let x := 0 in True).
1 goal ============================ forall m n : nat, m < n -> let x := 0 in True

intro m.
1 goal m : nat ============================ forall n : nat, m < n -> let x := 0 in True

intro n.
1 goal m, n : nat ============================ m < n -> let x := 0 in True

intro H.
1 goal m, n : nat H : m < n ============================ let x := 0 in True

intro x.
1 goal m, n : nat H : m < n x := 0 : nat ============================ True

This single intros tactic is equivalent to the 4 preceding intro tactics:

Goal forall m n, m < n -> (let x := 0 in True).
1 goal ============================ forall m n : nat, m < n -> let x := 0 in True

intros m n H x.
1 goal m, n : nat H : m < n x := 0 : nat ============================ True

Tactic intros intropattern*¶

Tactic intros until identnatural¶

The first form introduces zero or more items into the context from the constructs listed in intro. If intropattern is not specified, the tactic introduces items until it reaches the head constant; it never fails and may leave the context unchanged.

If intropattern is specified, the hnf tactic is applied until it finds an item that can be introduced into the context. The intropattern is often just a list of idents, but other forms can also be specified in order to, for example, introduce all dependent premises (*); introduce all dependent and non-dependent premises (**); split terms such as A /\ B ([]) and pick a fresh name with a given prefix (?X). See Intro patterns.

The second form repeats intro until it has introduced a dependent premise with the name ident or has introduced natural premises (like A in A -> B).

We recommend explicitly naming items with intros instead of using intros until natural. See the explanation here.

Example: intros until

Goal forall x y : nat, x = y -> y = x.: 1 goal ============================ forall x y : nat, x = y -> y = x

intros until y.: 1 goal x, y : nat ============================ x = y -> y = x

Or:

Goal forall x y : nat, x = y -> y = x.: 1 goal ============================ forall x y : nat, x = y -> y = x

intros until 1.: 1 goal x, y : nat H : x = y ============================ y = x

Error No quantified hypothesis named ident in current goal even after head-reduction.¶: The ident in the until clause doesn't appear as a dependent premise.

Error No natural-th non dependent hypothesis in current goal even after head-reduction.¶: There are fewer than natural premises in the goal.

Tactic eintros intropattern*¶: Works just like intros except that it creates existential variables for any unresolved variables rather than failing. Typically this happens when using a % intropattern (see simple_intropattern).

Tactic clear -? ident+?¶

Erases unneeded hypotheses from the context of the current goal. "Unneeded" means that the unselected hypotheses and the goal don't depend directly or indirectly on the erased hypotheses. That means the hypotheses will no longer appear in the context and therefore can't be used in subsequent proof steps. Note that erasing an uneeded hypothesis may turn a goal that was provable into an unprovable goal.

clear

All unneeded hypotheses are erased. This may leave the context unchanged; this form never fails.

clear ident+

Erases the named hypotheses if they are unneeded and fails otherwise.

Error ident is used in the conclusion.¶

Error ident is used in the hypothesis ident.¶

clear - ident+

Selects all hypotheses that are not named by the idents, then erases those that are unneeded. This may leave the context unchanged; this form never fails as long as the idents name hypotheses in the context.

Tactic 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 clear dependent ident¶: Clears the hypothesis ident and all the hypotheses that depend on it.

Tactic revert ident+¶

Moves the specified hypotheses and local definitions to the goal, if this respects dependencies. This is the inverse of intro.

Tactic revert dependent ident¶: Deprecated since version 8.18.

An alias for generalize dependent.

Tactic move ident_from where¶

where::=at top|at bottom|before ident|after ident

Moves a hypothesis ident_from and hypotheses that directly or indirectly refer to ident_from that appear between ident_from and ident. at top and at bottom are equivalent to giving the name of the first or last hypotheses in the context. The dependent hypotheses will appear after ident_from, appearing in dependency order. This lets users show and group hypotheses in the order they prefer. It doesn't change the goal or the proof term.

Note

Perhaps confusingly, "before" and "after" are interpeted with respect to the direction in which the hypotheses are moved rather than in the order of the resulting list of hypotheses. If ident_from is before ident in the context, these notions are the same: for hypotheses A B C, move A after B gives B A C, whereas if ident_from is after ident in the context, they are the opposite: move C after A gives C A B because the direction of movement is reversed.

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

Error Cannot move ident_from after ident: it depends on ident.¶

Example: move

Goal forall x :nat, x = 0 -> forall y z:nat, y=y-> 0=x.: 1 goal ============================ forall x : nat, x = 0 -> forall y : nat, nat -> y = y -> 0 = x

intros x Hx y z Hy.: 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x

(* x Hx y z Hy *)
move y after z. (* x Hx z y Hy (z was left of y, intuitive case) *): 1 goal x : nat Hx : x = 0 z, y : nat Hy : y = y ============================ 0 = x
Undo.: 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x
move z after y. (* x Hx z y Hy (z was right of y, see Note above) *): 1 goal x : nat Hx : x = 0 z, y : nat Hy : y = y ============================ 0 = x
Undo.: 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x
move x after Hy. (* y z Hy x Hx (Hx depends on x, so moved) *): 1 goal y, z : nat Hy : y = y x : nat Hx : x = 0 ============================ 0 = x
Undo.: 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x
move x before Hy. (* y z x Hx Hy *): 1 goal y, z, x : nat Hx : x = 0 Hy : y = y ============================ 0 = x
Undo.: 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x
move Hy after Hx. (* x y Hy Hx z *): 1 goal x, y : nat Hy : y = y Hx : x = 0 z : nat ============================ 0 = x
Undo.: 1 goal x : nat Hx : x = 0 y, z : nat Hy : y = y ============================ 0 = x
move Hy before Hx. (* x Hx y Hy z *): 1 goal x : nat Hx : x = 0 y : nat Hy : y = y z : nat ============================ 0 = x

Tactic rename ident₁ into ident₂+,¶: Renames hypothesis ident₁ into ident₂ for each pair of idents. Renaming is done simultaneously, which permits swapping the names of 2 hypotheses. (Note that the renaming is applied in the context and the existential variables, but the proof term doesn't change.)

Tactic set alias_definition occurrences?¶

Tactic set one_term as_name? occurrences?¶

alias_definition::=( ident simple_binder* := term )simple_binder::=name|( name+ : term )as_name::=as ident

The first form adds a new local definition ident := …. If simple_binder is not specified, the definition body is term and otherwise fun simple_binder* => term. Then the tactic replaces the body expression with the new variable ident in the goal or as specified by occurrences. The tactic may succeed and add the local definition even if no replacements are made.

The second form is equivalent to set (ident := one_term) occurrences? using ident, if present, or an auto-generated name if not provided.

If term or one_term has holes (i.e. subexpressions with 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 declared.¶

Example: set with a simple_binder

set does a simple syntactic replacement in the goal:

Goal forall n, n = 0.: 1 goal ============================ forall n : nat, n = 0

intros.: 1 goal n : nat ============================ n = 0

pattern n. (* without this, "set" won't replace anything in the goal *): 1 goal n : nat ============================ (fun n0 : nat => n0 = 0) n
set (f x := x = 0).: 1 goal n : nat f := fun x : nat => x = 0 : nat -> Prop ============================ f n

Tactic eset alias_definition occurrences?¶
Tactic eset one_term as_name? occurrences?¶: Similar to set, but instead of failing because of uninstantiated variables, generates existential variables for them. 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 one_term as_name? eqn : naming_intropattern? in goal_occurrences?¶

Similar to set (ident := one_term) in * but creates a hypothesis using Leibniz equality to remember the relation between the introduced variable and the term rather than creating a local definition. If as_name is not specified a fresh name is used. Use naming_intropattern to name the new equation.

Tactic eremember one_term as_name? eqn : naming_intropattern? in goal_occurrences?¶: Similar to remember, but instead of failing because of uninstantiated variables, generates existential variables for them.

Tactic pose alias_definition¶

Tactic pose one_term as_name?¶

Similar to set. Adds a local definition to the context but without doing any replacement.

Tactic epose alias_definition¶
Tactic epose one_term as_name?¶: Similar to pose, but instead of failing because of uninstantiated variables, generates existential variables for them.

Controlling the proof flow¶

Tactic assert ( ident : type ) by ltac_expr3?¶

Tactic assert ( ident := term )¶

Tactic assert one_type as_ipat? by ltac_expr3?

Adds a new hypothesis to the current subgoal and a new subgoal before it to prove the hypothesis. Then, if ltac_expr3 is specified, it applies that tactic to fully prove the new subgoal (and otherwise fails).

The first form adds a new hypothesis named ident of type type. (This corresponds to the cut rule of sequent calculus.)

The second form is equivalent to assert (ident : type) by exact (term) where type is the type of term. It is also equivalent to using pose proof. If the head of term is ident, the tactic is equivalent to specialize.

In the third form, if as_ipat isn't specified, the tactic adds the hypothesis one_type with a fresh name. Otherwise, it transforms the hypothesis as specified by as_ipat and adds the resulting new hypotheses and goals. See Intro patterns.

Error The term "type" has type "type₁" which should be Set, Prop or Type.¶: Occurs when the argument type (in the first form) or one_type (in the third form) is not of type Prop, Set nor Type.

Error Proof is not complete.¶: ltac_expr3 was not able to prove the new hypothesis.

Tactic eassert ( ident : type ) by ltac_expr3?¶
Tactic eassert ( ident := term )¶
Tactic eassert one_type as_ipat? by ltac_expr3?: Unlike assert, the type, term or one_type in eassert may contain holes, denoted by _, for which the tactic will create existential variables. This lets you avoid specifying the asserted statement completely before starting to prove it.

Tactic enough ( ident : type ) by ltac_expr3?¶

Tactic enough one_type as_ipat? by ltac_expr3?¶

Adds a new hypothesis to the current subgoal and a new subgoal after it to prove the hypothesis.

The first form adds a new hypothesis ident : type and type as the new subgoal. Then, if ltac_expr3 is specified, it applies that tactic to prove the current subgoal with the added hypothesis (and otherwise fails).

In the second form, if as_ipat isn't specified, the tactic adds a new hypothesis one_type with a name chosen by Coq. Otherwise, it transforms one_type as specified by as_ipat and adds the resulting new hypotheses. The as_ipat may also expand the current subgoal into multiple subgoals. Then, if ltac_expr3 is specified, it is applied to and must succeed on all of them.

Tactic eenough ( ident : type ) by ltac_expr3?¶
Tactic eenough one_type as_ipat? by ltac_expr3?¶: Unlike enough, the type and one_type in eenough may contain holes, denoted by _, for which the tactic will create existential variables. This lets you avoid specifying the asserted statement completely until you start to use the hypothesis or later start to prove the statement.

Tactic cut one_type¶: Implements the non-dependent case of the App typing rule, the Modus Ponens inference rule. It is equivalent to enough (ident: one_type). revert ident. This tactic is generally considered obsolete but it is still widely used in old scripts.

Tactic pose proof term as_ipat?¶

Tactic pose proof ( ident := term )¶

The first form behaves like assert one_type as_ipat? by exact term where one_type is the type of term.

The second form is equivalent to assert (ident := term).

Tactic epose proof term as_ipat?¶
Tactic epose proof ( ident := term )¶: While pose proof expects that no existential variables are generated by the tactic, epose proof removes this constraint.

Tactic specialize one_term_with_bindings as_ipat?¶

Specializes a term (typically a hypothesis or a lemma) by applying arguments to it.

First, the tactic generates a modified term: If the head constant of one_term (in one_term_with_bindings) has the type forall ..., the tactic replaces one or more of the quantified variables in the type with arguments provided by one_term_with_bindings, either in the form of a function application (which may be partial), such as (H 1), or with named or numbered binders, such as H with (n:=1).

If the head constant has a non-dependent product type such as A -> B -> C, the tactic eliminates one or more of the premises (doing forward reasoning).

Uninstantiated arguments are inferred by unification, if possible, or otherwise left quantified in the resulting term.

Then, If the head constant is a hypothesis H, the resulting term replaces that hypothesis. Specifying as_ipat will leave the original hypothesis unchanged and will introduce new hypotheses as specified by the simple_intropattern. If H appears in the conclusion or another hypothesis, you must use as_ipat to give a fresh hypothesis name.

If the head constant is a lemma or theorem, the resulting term is added as a new premise of the goal so that the behavior is similar to that of generalize. In this case, you can use as_ipat to immediately introduce the modified term as one or more hypotheses.

Error Cannot change ident, it is used in hypothesis ident.¶

Error Cannot change ident, it is used in conclusion.¶

Example: partial application in specialize

Goal (forall n m: nat, n + m = m + n) -> True.: 1 goal ============================ (forall n m : nat, n + m = m + n) -> True

intros.: 1 goal H : forall n m : nat, n + m = m + n ============================ True

specialize (H 1). (* equivalent to: specialize H with (n := 1) *): 1 goal H : forall m : nat, 1 + m = m + 1 ============================ True

Example: specialize with a non-dependent product

Compare this to a similar example that uses apply. specialize won't introduce new goals as apply can.

Goal forall A B C: Prop, B -> (A -> B -> C) -> True.: 1 goal ============================ forall A B C : Prop, B -> (A -> B -> C) -> True
Proof.

intros A B C H0 H1.: 1 goal A, B, C : Prop H0 : B H1 : A -> B -> C ============================ True

specialize H1 with (2:=H0).: 1 goal A, B, C : Prop H0 : B H1 : A -> C ============================ True

Tactic specialize_eqs ident¶

Tactic generalize one_term+¶

Tactic generalize pattern_occs as_name?+,¶

For each one_term (which may be in the pattern_occs), replaces the goal G with forall (x:T), G', where one_term is a subterm of G of type T and G' is obtained by replacing all occurrences of one_term with x within G. x is a fresh variable chosen based on T. Specifying multiple one_terms is equivalent to generalize one_term_n; … ; generalize one_term₁. (Note they are processed right to left.)

as_name: The name to use for x instead of a fresh name.

Example

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

Show.: 1 goal x, y : nat ============================ 0 <= x + y + y

generalize (x + y + y). (* get a simpler goal that can be proven by induction *): 1 goal x, y : nat ============================ forall n : nat, 0 <= n

Tactic generalize dependent one_term¶: Generalizes one_term and all hypotheses that depend on one_term. It clears the generalized hypotheses.

Tactic dependent generalize_eqs ident¶

Tactic dependent generalize_eqs_vars ident¶

Tactic generalize_eqs ident¶

Tactic generalize_eqs_vars ident¶

Tactic evar ( ident : type )¶
Tactic evar one_type¶: The evar tactic creates a new local definition named ident with type type or one_type in the context. The body of this binding is a fresh existential variable. If the second form is used, Coq chooses the name.

Tactic instantiate ( ident := term )¶

Tactic instantiate ( natural := term ) hloc?¶

hloc::=in |- *|in ident|in ( type of ident )|in ( value of ident )

The first form refines (see refine) an existential variable ident with the term term. It is equivalent to only [ident]: refine term.

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.

The second form refines an existential variable selected by its position. The natural argument is the position of the existential variable from right to left in the goal. (Use the hloc clause to select an existential variable in a hypothesis.) Counting starts at 1 and multiple occurrences of the same existential variable are counted multiple times. Using this form is discouraged because slight changes to the goal may change the needed index, causing a maintenance issue.

Advanced users may want to define and use an Ltac tactic to get more consistent behavior, such as:

Ltac instantiate_ltac_variable ev term := let H := fresh in pose ev as H; instantiate (1 := term) in (value of H); clear H.

in ident: Selects the hypothesis ident.
in |- *: Selects the goal. This is the default behavior.
in ( type of ident ): Selects existential variables in the type of the local definition ident. (The body is not included.)
in ( value of ident ): Selects existential variables in the body of the local definition ident. (The type is not included.)

Tactic absurd one_type¶: one_type 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 one_term_with_bindings?¶

Tries to prove the current goal by finding a contradiction.

If one_term_with_bindings is not provided (the most common use case), the tactic first does an intros. The tactic then proves the goal if

the updated context has a pair of hypotheses where one is the negation of the other (e.g. P and not ~P), or
there is a hypothesis with an empty inductive type (e.g. False), or
there is a hypothesis ~P where P is a singleton inductive type (e.g. True or x=x) provable by Goal P. constructor.

If one_term_with_bindings is provided, its type must be a negation, such as ~P, or an empty inductive type, such as False. If the type is a negation and P is a hypothesis in the context, the goal is proven. If the type is a negation and P is not in the context, the goal is replaced with P. If the type is False or another empty inductive type, the goal is proven. Otherwise the tactic fails. (If there is a hypothesis P and you want to replace the goal with ~P, use the contradict tactic. If there are hypotheses H1 : P and H2 : ~P, use contradiction without arguments or contradiction H2 since contradiction H1 won't work.)

Use the discriminate tactic to prove the current goal when there is a hypothesis with an impossible structural equality such as 0 = 1.

Example: contradiction tactic

Simple examples. To see more detail, add intros after each Goal.

Inductive F :=. (* Another empty inductive type *): F is defined F_rect is defined F_ind is defined F_rec is defined F_sind is defined
Goal F -> False.: 1 goal ============================ F -> False
contradiction.: No more goals.
Qed.
Goal forall (A : Prop), A -> ~A -> False.: 1 goal ============================ forall A : Prop, A -> ~ A -> False
contradiction.: No more goals.
Qed.
Goal forall (A : Type) (x : A), ~(x = x) -> False.: 1 goal ============================ forall (A : Type) (x : A), x <> x -> False
contradiction.: No more goals.
Qed.

Apply a fact from the standard library:

Require Import Arith.: [Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Goal forall (A : Prop), 0 < 0 -> A.: 1 goal ============================ forall A : Prop, 0 < 0 -> A

intros.: 1 goal A : Prop H : 0 < 0 ============================ A
contradiction (Nat.lt_irrefl 0).: No more goals.
Qed.

Tactic contradict ident¶

Transforms the specified hypothesis ident and the goal in order to prove that the hypothesis is false. For contradict H, the current goal and context are transformed as shown. (For brevity, ⊢ is used to separate hypotheses from the goal; it is equivalent to the dividing line shown in a context.):

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¶: 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.

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.

Performance-oriented tactic variants¶

Tactic exact_no_check one_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 goal ============================ False
exact_no_check I.: No more goals.
Fail Qed.: The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False".

Tactic vm_cast_no_check one_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 goal ============================ False
vm_cast_no_check I.: No more goals.
Fail Qed.: The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False".

Tactic native_cast_no_check one_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 goal ============================ False
native_cast_no_check I.: No more goals.
Fail Qed.: The command has indeed failed with message: Native compiler is disabled, falling back to VM conversion test. [native-compiler-disabled,native-compiler,default]