A subset of Coq's tactic reference

Source:https://coq.inria.fr/distrib/current/refman/tactics.html
Converted by:Clément Pit-Claudel

Tip

In this documentation, italics indicate holes to fill; the rest is fixed syntax. Boxes indicate repeatable blocks. The top-right symbol indicates the number of repetitions:

  • 0 or 1? (an optional block)
  • one or more+ (a repeatable block)
  • any number of times* (an optional, repeatable block)

The bottom symbol indicates the separator to use between repeated blocks. For example, “rewrite H”, “rewrite → H”, and “rewrite H1, H2” are all matches for rewrite →? term+,.

Note

Scroll down for examples of coqtop output. The bottom of this page lists all Coq forms that include repetitions, semi-automatically reverse-engineered from the manual.

fix ident num

This tactic is a primitive tactic to start a proof by induction. In general, it is easier to rely on higher-level induction tactics such as the ones described in Section 8.5.2.

In the syntax of the tactic, the identifier ident is the name given to the induction hypothesis. The natural number num tells on which premise of the current goal the induction acts, starting from 1 and counting both dependent and non dependent products. Especially, the current lemma must be composed of at least num products.

Like in a fix expression, the induction hypotheses have to be used on structurally smaller arguments. The verification that inductive proof arguments are correct is done only at the time of registering the lemma in the environment. To know if the use of induction hypotheses is correct at some time of the interactive development of a proof, use the command Guarded (see Section 7.3.2).

Variant fix ident num with (ident binder+ {struct ident'}? : type)+

This starts a proof by mutual induction. The statements to be simultaneously proved are each of the type forall binder+, type. The identifiers ident are the names of the induction hypotheses. The identifiers ident' are the respective names of the premises on which the induction is performed in the statements to be simultaneously proved (if not given, the system tries to guess itself what they are).

unfold qualid

This tactic applies to any goal. The argument qualid must denote a defined transparent constant or local definition (see Sections 1.3.2 and 6.10.2). The tactic unfold applies the δ rule to each occurrence of the constant to which qualid refers in the current goal and then replaces it with its βι normal form.

Error qualid does not denote an evaluable constant
Variant unfold qualid+

Replaces simultaneously each of the qualid with their definitions and replaces the current goal with its βι normal form.

Variant unfold qualid at num+,+,

The lists of num specify the occurrences of qualid to be unfolded. Occurrences are located from left to right.

Error bad occurrence number of qualid
Error qualid does not occur
Variant unfold string

If string denotes the discriminating symbol of a notation (e.g. "+") or an expression defining a notation (e.g. "_ + _"), and this notation refers to an unfoldable constant, then the tactic unfolds it.

Variant unfold string%key

This is variant of unfold string where string gets its interpretation from the scope bound to the delimiting key key instead of its default interpretation (see Section 12.2.2).

Variant unfold qualid|string at num+,+,

This is the most general form, where qualid_or_string is either a qualid or a string referring to a notation.

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 t1 … tn) 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) u1 … un and the ti and ui unifies, then P is taken to be (fun x => Q). Otherwise, apply tries to define P by abstracting over t1 …  tn in the goal. See pattern in Section 8.7.7 to transform the goal so that it gets the form (fun x => Q) u1 … un.

Error Impossible to unify … with …

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 (see sections 8.7.7, 8.6.5).

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 (ref := term)+

This also provides apply with values for instantiating premises. Here, variables are referred by names and non-dependent products by increasing numbers (see syntax in Section 8.1.3).

Variant apply term+,

This is a shortcut for apply term1 ; [ .. | … ; [ .. | apply termn ] … ], i.e. for the successive applications of termi+1 on the last subgoal generated by apply termi, starting from the application of term1.

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 Section 2.11). The instantiation is intended to be found later in the proof.

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.

Definition id (x : nat) := x.
id is defined
Hypothesis H : forall y, id y = y.
Toplevel input, characters 0-34: > Hypothesis H : forall y, id y = y. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: H is declared as a local axiom [local-declaration,scope] 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 ?M158 = ?M158" with "0 = 0". 1 subgoal ============================ 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 used-defined tactics that backtrack often. Moreover, it does not traverse tuples as apply does.

Variant simple? apply term with (id := val)+?+, in ident as intro_pattern?

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:

Variable R : nat -> nat -> Prop.
Toplevel input, characters 0-32: > Variable R : nat -> nat -> Prop. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: R is declared as a local axiom [local-declaration,scope] R is declared
Hypothesis Rtrans : forall x y z:nat, R x y -> R y z -> R x z.
Toplevel input, characters 0-62: > Hypothesis Rtrans : forall x y z:nat, R x y -> R y z -> R x z. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Rtrans is declared as a local axiom [local-declaration,scope] Rtrans is declared
Variables n m p : nat.
Toplevel input, characters 0-22: > Variables n m p : nat. > ^^^^^^^^^^^^^^^^^^^^^^ Warning: n is declared as a local axiom [local-declaration,scope] n is declared Toplevel input, characters 0-22: > Variables n m p : nat. > ^^^^^^^^^^^^^^^^^^^^^^ Warning: m is declared as a local axiom [local-declaration,scope] m is declared Toplevel input, characters 0-22: > Variables n m p : nat. > ^^^^^^^^^^^^^^^^^^^^^^ Warning: p is declared as a local axiom [local-declaration,scope] p is declared
Hypothesis Rnm : R n m.
Toplevel input, characters 0-23: > Hypothesis Rnm : R n m. > ^^^^^^^^^^^^^^^^^^^^^^^ Warning: Rnm is declared as a local axiom [local-declaration,scope] Rnm is declared
Hypothesis Rmp : R m p.
Toplevel input, characters 0-23: > Hypothesis Rmp : R m p. > ^^^^^^^^^^^^^^^^^^^^^^^ Warning: Rmp is declared as a local axiom [local-declaration,scope] 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:

Fail apply Rtrans.
The command has indeed failed with message: Unable to find an instance for the variable y. 1 subgoal ============================ R n p

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 option:

Option Universal Lemma Under Conjunction

This option, which preserves compatibility with versions of Coq prior to 8.4 is also available for apply term in ident (see apply … in).

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 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 A <-> B statement, 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 of term in sequence in ident.

Variant apply term with (id := val)+++, in hyp+,

This does the same but uses the bindings in each (id := val) to instantiate the parameters of the corresponding type of term (see syntax of bindings in Section 8.1.3).

Variant eapply term with (id := val)+++, in hyp+,

This works as above but turns unresolved bindings into existential variables, if any, instead of failing.

Variant apply term with (id := val)++, in hyp+, as intropattern

This works as apply above, then applies the intropattern to the hypothesis ident.

Variant eapply term with (id := val)++, in hyp+, as intropattern

Same as above, but using eapply.

Variant simple apply terms in ident

This behaves like apply term in ident but it reasons modulo conversion only on subterms that contain no variables to instantiate. For instance, if id := fun x:nat => x and H : forall y, id y = y -> True and H0 : O = O then simple apply H in H0 does not succeed because it would require the conversion of id ?1234 and O where ?1234 is a variable to instantiate. Tactic simple apply term in ident does not either traverse tuples as apply term in ident does.

Variant simple? apply term with (id := val)+?+, in ident as intro_pattern?

This summarizes the different syntactic variants of apply term in ident and eapply term in ident.

fresh component+
fun ident+ => expr
solve [expr+|]
apply term with term+
apply term with (ref := term)+
apply term+,
apply term+, in ident
apply term with (id := val)++, in ident
eapply term with (id := val)++, in ident
apply term with (id := val)++, in ident as intro_pattern
eapply term with (id := val)++, in ident as intro_pattern
simple? apply term with (id := val)+?+, in ident as intro_pattern?
exists (id := val)++,
intros ident+
clear ident+
clear - ident+
revert ident+
rename ident into ident+,
set (ident binder+ := term)
set (ident binder+ := term) in goal_occurrences
pose (ident binder+ := term)
decompose [qualid+] term
specialize (ident term+)
generalize term+,
generalize term at num+
generalize term at num+ as ident+,
destruct term+,
induction term+, using qualid
dependent induction ident generalizing ident+
functional induction (qualid term+)
functional induction (qualid term+) as disj_conj_intro_pattern using term with (id := val)+
ediscriminate term with (id := val)+?
einjection term with (id := val)+?
injection term with (id := val)+? as intro_pattern+
injection num as intro_pattern+
injection as intro_pattern+
einjection term with (id := val)+? as intro_pattern+
einjection num as intro_pattern+
einjection as intro_pattern+
inversion ident in ident+
inversion ident as intro_pattern in ident+
inversion_clear ident in ident+
inversion_clear ident as intro_pattern in ident+
inversion ident using ident' in ident+
fix ident num with (ident binder+ {struct ident'}? : type)+
cofix ident with (ident binder+ : type)+
rewrite term+,
subst ident+
change term at num+ with term
change term at num+ with term in ident
cbv flag+
lazy flag+
compute [qualid+]
cbv [qualid+]
compute -[qualid+]
cbv -[qualid+]
lazy [qualid+]
lazy -[qualid+]
cbn [qualid+]
cbn -[qualid+]
simpl pattern at num+
simpl qualid at num+
simpl string at num+
unfold qualid+,
unfold qualid at num+,+,
unfold id|string at num+,+,
pattern term at num+
pattern term at - num+
pattern term+,
pattern term at num++,
auto with ident+
auto using lemma+,
auto using lemma+, with ident+
trivial with ident+
autounfold with ident+
autounfold with ident+ in clause
autorewrite with ident+
autorewrite with ident+ using tactic
autorewrite with ident+ in qualid
autorewrite with ident+ in qualid using tactic
autorewrite with ident+ in clause
firstorder with ident+
firstorder using qualid+,
firstorder using qualid+, with ident+
congruence with term+
esimplify_eq term with (id := val)+?
quote ident [ident+]
ring_simplify term+
field_simplify term+
idtac message_token+
fail message_token+
fail n message_token+
gfail message_token+
gfail n message_token+
quote ident [ident+] in term using tactic
ring [term+]
ring_simplify [term+] t+ in ident
field [term+]
field_simplify [term+]
field_simplify [term+] term+
field_simplify [term+] in hyp
field_simplify [term+] term+ in hyp
field_simplify_eq [term+]
field_simplify_eq [term+] in hyp
setoid_symmetry in ident?
setoid_rewrite term in ident?
setoid_rewrite <- term in ident?
setoid_rewrite <- term at occs? in ident?
setoid_rewrite orientation? term at occs? in ident?
setoid_replace term with term in ident? using relation term? by tactic?
rewrite_strat s in ident?
Program Fixpoint ident params {order} : type := term.
Add Field name : field (mod+,).
Add Ring name : ring (mod+,).
Admit Obligations of ident?.
Arguments ident !arg+.
Arguments ident possibly_bracketed_ident+ / possibly_bracketed_ident+.
Arguments ident possibly_bracketed_ident+ : simpl never.
Arguments ident possibly_bracketed_ident+ : simpl nomatch.
Arguments qualid name+ : rename.
Arguments qualid name %scope+.
Arguments qualid possibly_bracketed_ident+.
Class ident binder+ : sort:= {field+;}.
Class ident binder+ : sort:= ident : type.
Collection ident:= ident+.
Context binder+.
Corollary ident binders? : type.
Create HintDb ident discriminated?.
Definition ident binder+.
Definition ident binders? : type.
Derive Dependent Inversion_clear ident with forall ident: type+, I arg+ Sort sort.
Derive Dependent Inversion ident with forall ident: type+, I arg+ Sort sort.
Derive Inversion_clear ident with forall ident: type+, I arg+ Sort sort.
Derive Inversion ident with forall ident: type+, I arg+ Sort sort.
Existing Instance ident priority?.
Existing Instances ident+ priority?.
Extract Constant qualid "string"+ => "string".
Extract Inductive qualid => "string" ["string"+] optstring.
Extraction Blacklist ident+.
Extraction "file" qualid+.
Extraction Implicit qualid [ident+].
Fact ident binders? : type.
Fixpoint ident params {struct ident} : type := term.
Function ident binder+ {decrease_annot} : type := term.
Generalizable Variables ident+.
Global Arguments qualid name %scope+.
Global Arguments qualid possibly_bracketed_ident+.
Global Opaque qualid+.
Hint hint_definition : ident+.
Hint Local hint_definition : ident+.
Hint Rewrite term+ : ident+.
Hint Rewrite -> term+ : ident+.
Hint Rewrite <- term+ : ident+.
Hint Rewrite term+ using tactic : ident+.
Implicit Types ident+ : type.
Include module+<+.
Inductive ident binder+ : term := ident: term+|.
Infix "symbol" := qualid (modifier+,).
Instance ident binder+ : Class term+ priority? := {field := b+;}.
Instance ident binder+ : forall binder+, Class term+ priority? := term.
Lemma ident binders? : type.
Let CoFixpoint ident with cofix_body+.
Let Fixpoint ident with fix_body+.
Let ident binders? : type.
Local Arguments qualid name %scope+.
Local Arguments qualid possibly_bracketed_ident+.
Local Declare ML Module "string"+.
Local? Hint Constructors ident: ident+?.
Local? Hint Constructors ident+: ident+?.
Local? Hint Cut regexp: ident+?.
Local? Hint Extern num pattern? => tactic: ident+?.
Local Hint hint_definition : ident+.
Local? Hint Immediate term: ident+?.
Local? Hint Immediate term+: ident+?.
Local? Hint Resolve term: ident+?.
Local? Hint Resolve term+: ident+?.
Local? Hint Unfold ident+: ident+?.
Local? Hint Unfold qualid: ident+?.
Local? Notation ident ident ident+? := term (only parsing)?.
Module ident module_bindings := module_expression+<+.
Module ident module_bindings <: module_type+<:.
Module ident module_bindings <: module_type+<::= module_expression.
Module ident <: module_type+<:.
Module Type ident module_bindings := module_type+<+.
Next Obligation of ident?.
Obligation num of ident?.
Obligations of ident?.
Opaque qualid+.
Parameter ident+ : term.
Preterm of ident?.
Print Sorted? Universes.
Print Sorted? Universes "string".
Program Definition ident binder+ : term := term.
Proof using collection - (ident+).
Proof using ident+.
Proof using -(ident+).
Proof using ident+ with tactic.
Proof with tactic using ident+.
Proposition ident binders? : type.
Qed exporting ident+,.
Record ident params : sort := ident {ident binders : term+;}.
Recursive Extraction qualid+.
Remark ident binders? : type.
Remove Hints term+ : ident+.
SearchHead term inside module+.
SearchHead term outside module+.
SearchPattern term inside module+.
SearchPattern term outside module+.
SearchRewrite term inside module+.
SearchRewrite term outside module+.
Search -?search_term+.
Search search_term+ inside module+.
Search search_term+ outside module+.
selector: Search -?search_term+.
Separate Extraction qualid+.
Solve All Obligations with expr?.
Solve Obligations of ident? with expr?.
Strategy level [qualid+].
Tactic Notation tactic_level prod_item+? := tactic.
Theorem ident binders? : type.
Transparent qualid+.
Typeclasses Opaque ident+.
Typeclasses Transparent ident+.
Variable ident+ : term.
Variant ident binder+ : term := constructors+.