Chapter 8  Tactics

• 8.1  Invocation of tactics
• 8.2  Explicit proof as a term
• 8.3  Basics
• 8.4  Negation and contradiction
• 8.5  Conversion tactics
• 8.6  Introductions
• 8.7  Induction and Case Analysis
• 8.8  Equality
• 8.9  Equality and inductive sets
• 8.10  Inversion
• 8.11  Classical tactics
• 8.12  Automatizing
• 8.13  Controlling automation
• 8.14  Generation of induction principles with Scheme
• 8.15  Generation of induction principles with Functional Scheme
• 8.16  Simple tactic macros

A deduction rule is a link between some (unique) formula, that we call the conclusion and (several) formulas that we call the premises. Indeed, a deduction rule can be read in two ways. The first one has the shape: “if I know this and this then I can deduce this”. For instance, if I have a proof of A and a proof of B then I have a proof of A ∧ B. This is forward reasoning from premises to conclusion. The other way says: “to prove this I have to prove this and this”. For instance, to prove A ∧ B, I have to prove A and I have to prove B. This is backward reasoning which proceeds from conclusion to premises. We say that the conclusion is the goal to prove and premises are the subgoals. The tactics implement backward reasoning. When applied to a goal, a tactic replaces this goal with the subgoals it generates. We say that a tactic reduces a goal to its subgoal(s).

Each (sub)goal is denoted with a number. The current goal is numbered 1. By default, a tactic is applied to the current goal, but one can address a particular goal in the list by writing n:tactic which means “apply tactic tactic to goal number n”. We can show the list of subgoals by typing Show (see Section 7.3.1).

Since not every rule applies to a given statement, every tactic cannot be used to reduce any goal. In other words, before applying a tactic to a given goal, the system checks that some preconditions are satisfied. If it is not the case, the tactic raises an error message.

Tactics are build from atomic tactics and tactic expressions (which extends the folklore notion of tactical) to combine those atomic tactics. This chapter is devoted to atomic tactics. The tactic language will be described in Chapter 9.

There are, at least, three levels of atomic tactics. The simplest one implements basic rules of the logical framework. The second level is the one of derived rules which are built by combination of other tactics. The third one implements heuristics or decision procedures to build a complete proof of a goal.

8.1  Invocation of tactics

A tactic is applied as an ordinary command. If the tactic does not address the first subgoal, the command may be preceded by the wished subgoal number as shown below:

8.2  Explicit proof as a term

8.2.1  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 Section 4.3).

Error messages:

1. Not an exact proof

Variants:

1. eexact term

   This tactic behaves like exact but is able to handle terms with meta-variables.

8.2.2  refine term

This tactic allows to give an exact proof but still with some holes. The holes are noted “_”.

Error messages:

1. invalid argument: the tactic refine doesn’t know what to do with the term you gave.
2. 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, which call refine internally.
3. Cannot infer a term for this placeholder there is a hole in the term you gave which type cannot be inferred. Put a cast around it.

An example of use is given in Section 10.1.

8.3  Basics

Tactics presented in this section implement the basic typing rules of pCic given in Chapter 4.

8.3.1  assumption

This tactic applies to any goal. It implements the “Var” rule given in Section 4.2. It looks in the local context for an hypothesis which type is equal to the goal. If it is the case, the subgoal is proved. Otherwise, it fails.

Error messages:

1. No such assumption

Variants:

1. eassumption

   This tactic behaves like assumption but is able to handle goals with meta-variables.

8.3.2  clear ident

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

Variants:

1. clear ident₁ … ident_n

   This is equivalent to clear ident₁. … clear ident_n.

2. clearbody ident

   This tactic expects ident to be a local definition then clears its body. Otherwise said, this tactic turns a definition into an assumption.

3. clear - ident₁ … ident_n

   This tactic clears all hypotheses except the ones depending in the hypotheses named ident₁ … ident_n and in the goal.

4. clear

   This tactic clears all hypotheses except the ones depending in goal.

5. clear dependent ident

   This clears the hypothesis ident and all hypotheses which depend on it.

Error messages:

1. ident not found
2. ident is used in the conclusion
3. ident is used in the hypothesis ident’

8.3.3  move ident₁ after ident₂

This moves the hypothesis named ident₁ in the local context after the hypothesis named ident₂.

If ident₁ comes before ident₂ in the order of dependences, then all hypotheses between ident₁ and ident₂ which (possibly indirectly) depend on ident₁ are moved also.

If ident₁ comes after ident₂ in the order of dependences, then all hypotheses between ident₁ and ident₂ which (possibly indirectly) occur in ident₁ are moved also.

Variants:

1. move ident₁ before ident₂

   This moves ident₁ towards and just before the hypothesis named ident₂.

2. move ident at top

   This moves ident at the top of the local context (at the beginning of the context).

3. move ident at bottom

   This moves ident at the bottom of the local context (at the end of the context).

Error messages:

1. ident_i not found
2. Cannot move ident₁ after ident₂: it occurs in ident₂
3. Cannot move ident₁ after ident₂: it depends on ident₂

8.3.4  rename ident₁ into ident₂

This renames hypothesis ident₁ into ident₂ in the current context¹

Variants:

1. rename ident₁ into ident₂, …, ident_2k-1 into ident_2k

   Is equivalent to the sequence of the corresponding atomic rename.

Error messages:

1. ident₁ not found
2. ident₂ is already used

8.3.5  intro

This tactic applies to a goal which is either a product or starts with a let binder. If the goal is a product, the tactic implements the “Lam” rule given in Section 4.2². 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 -> 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 neither a product nor starting with a let definition, the tactic intro applies the tactic red until the tactic intro can be applied or the goal is not reducible.

Error messages:

1. No product even after head-reduction
2. ident is already used

Variants:

1. intros

   Repeats intro until it meets the head-constant. It never reduces head-constants and it never fails.

2. intro ident

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

   
   Error message: name ident is already used

   
   Remark: 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 2.6.2).

3. intros ident₁ … ident_n

   Is equivalent to the composed tactic intro ident₁; … ; intro ident_n.

   More generally, the intros tactic takes a pattern as argument in order to introduce names for components of an inductive definition or to clear introduced hypotheses; This is explained in 8.7.3.

4. intros until ident

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

   
   Error message: No such hypothesis in current goal

5. intros until num

   Repeats intro until the num-th non-dependent product. For instance, 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. And 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 message: No such hypothesis in current goal

   Happens when num is 0 or is greater than the number of non-dependent products of the goal.

6. intro after ident
   intro before ident
   intro at top
   intro at bottom

   Applies intro and moves 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. Note that intro at bottom is a synonym for intro with no argument.

   
   Error messages:

   1. No product even after head-reduction
   2. No such hypothesis : ident
7. intro ident₁ after ident₂
   intro ident₁ before ident₂
   intro ident₁ at top
   intro ident₁ at bottom

   Behaves as previously but naming the introduced hypothesis ident₁. It is equivalent to intro ident₁ followed by the appropriate call to move (see Section 8.3.3).

   
   Error messages:

   1. No product even after head-reduction
   2. No such hypothesis : ident

8.3.6  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 unifies, then P is taken to be (fun x => Q). Otherwise, apply tries to define P by abstracting over t₁ … t_n in the goal. See pattern in Section 8.5.7 to transform the goal so that it gets the form (fun x => Q) u₁ … u_n.

Error messages:

1. 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.5.7, 8.3.12).

2. Unable to find an instance for the variables ident …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:

Variants:

1. apply term with term₁ … term_n

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

   
   Error message: Not the right number of missing arguments

2. apply term with (ref₁ := term₁) … (ref_n := term_n)

   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.3.22).

3. apply term₁ , …, term_n

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

4. eapply term

   The tactic eapply behaves as apply but does not fail when no instantiation are deducible for some variables in the premises. Rather, it turns these variables into so-called existential variables which are variables still to instantiate. An existential variable is identified by a name of the form ?n where n is a number. The instantiation is intended to be found later in the proof.

   An example of use of eapply is given in Section 10.2.

5. simple apply term

   This behaves like apply 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 then simple apply H on goal O = O does not succeed because it would require the conversion of f ?y and O where ?y is a variable to instantiate. Tactic simple apply does not either traverse tuples as apply does.

   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.

6. [simple] apply term₁ [with bindings_list₁] , …, term_n [with bindings_list_n]
   [simple] eapply term₁ [with bindings_list₁] , …, term_n [with bindings_list_n]

   This summarizes the different syntaxes for apply and eapply.

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

8.3.7  set ( ident := term )

This replaces term by ident in the conclusion or in the hypotheses of the current goal and adds the new definition ident:= term to the local context. The default is to make this replacement only in the conclusion.

Variants:

1. set ( ident := term ) in goal_occurrences

   This notation allows to specify which occurrences of term have to be substituted in the context. The in goal_occurrences clause is an occurrence clause whose syntax and behavior is described in Section 8.3.23.

2. set ( ident binder  …  binder := term )

   This is equivalent to set ( ident := fun binder  …  binder => term ).

3. set term

   This behaves as set ( ident := term ) but ident is generated by Coq. This variant also supports an occurrence clause.

4. set ( ident₀ binder  …  binder := term ) in goal_occurrences
   set term in goal_occurrences

   These are the general forms which combine the previous possibilities.

5. remember term as ident

   This behaves as set ( ident := term ) in * and using a logical (Leibniz’s) equality instead of a local definition.

6. remember term as ident in goal_occurrences

   This is a more general form of remember that remembers the occurrences of term specified by an occurrences set.

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

8. pose ( ident binder  …  binder := term )

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

9. pose term

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

8.3.8  assert ( ident : form )

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³. The subgoal U comes first in the list of subgoals remaining to prove.

Error messages:

1. Not a proposition or a type

   Arises when the argument form is neither of type Prop, Set nor Type.

Variants:

1. assert form

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

2. assert ( ident := term )

   This behaves as assert (ident : type);[exact term|idtac] where type is the type of term.

3. cut form

   This tactic applies to any goal. It implements the non dependent case of the “App” rule given in Section 4.2. (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.

4. assert form by tactic

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

5. assert form as intro_pattern

   If intro_pattern is a naming introduction pattern (see Section 8.7.3), the hypothesis is named after this introduction pattern (in particular, if intro_pattern is ident, the tactic behaves like assert (ident : form)).

   If intro_pattern is a disjunctive/conjunctive introduction pattern, the tactic behaves like assert form then destructing the resulting hypothesis using the given introduction pattern.

6. assert form as intro_pattern by tactic

   This combines the two previous variants of assert.

7. pose proof term as intro_pattern

   This tactic behaves like assert T as intro_pattern by exact term where T is the type of term.

   In particular, pose proof term as ident behaves as assert (ident:T) by exact term (where T is the type of term) and pose proof term as disj_conj_intro_pattern behaves like destruct term as disj_conj_intro_pattern.

8. specialize (ident term₁ … term_n)
   specialize ident with bindings_list

   The tactic specialize 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₁ … term_n or from a bindings list (see Section 8.3.22 for more about bindings lists). In the second form, all instantiation elements must be given, whereas in the first form the application to term₁ … term_n can be partial. The first form is equivalent to assert (ident’:=identterm₁ … term_n); clear ident; rename ident’ into ident.

   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.

8.3.9  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 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 messages:

1. Statement without assumptions

   This happens if the type of term has no non dependent premise.

2. Unable to apply

   This happens if the conclusion of ident does not match any of the non dependent premises of the type of term.

Variants:

1. apply term , … , term in ident

   This applies each of term in sequence in ident.

2. apply term with bindings_list , … , term with bindings_list in ident

   This does the same but uses the bindings in each bindings_list to instantiate the parameters of the corresponding type of term (see syntax of bindings in Section 8.3.22).

3. eapply term with bindings_list , … , term with bindings_list in ident

   This works as apply term with bindings_list , … , term with bindings_list in ident but turns unresolved bindings into existential variables, if any, instead of failing.

4. apply term, with bindings_list , … , term, with bindings_list in ident as disj_conj_intro_pattern

   This works as apply term, with bindings_list , … , term, with bindings_list in ident then destructs the hypothesis ident along disj_conj_intro_pattern as destruct ident as disj_conj_intro_pattern would.

5. eapply term, with bindings_list , … , term, with bindings_list in ident as disj_conj_intro_pattern

   This works as apply term, with bindings_list , … , term, with bindings_list in ident as disj_conj_intro_pattern but using eapply.

6. simple apply term 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 f ?y and O where ?y is a variable to instantiate. Tactic simple apply term in ident does not either traverse tuples as apply term in ident does.

7. [simple] apply term [with bindings_list] , … , term [with bindings_list] in ident [as disj_conj_intro_pattern]
   [simple] eapply term [with bindings_list] , … , term [with bindings_list] in ident [as disj_conj_intro_pattern]

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

8.3.10  generalize term

This tactic applies to any goal. It generalizes the conclusion w.r.t. one subterm of it. For example:

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.

Variants:

1. generalize term₁ , … , term_n

   Is equivalent to generalize term_n; … ; generalize term₁. Note that the sequence of term_i’s are processed from n to 1.

2. generalize term at num₁ … num_i

   Is equivalent to generalize term but generalizing only over the specified occurrences of term (counting from left to right on the expression printed using option Set Printing All).

3. generalize term as ident

   Is equivalent to generalize term but use ident to name the generalized hypothesis.

4. generalize term₁ at num₁₁ … num_1i1 as ident₁ , … , term_n at num_n1 … num_nin as ident₂

   This is the most general form of generalize that combines the previous behaviors.

5. generalize dependent term

   This generalizes term but also all hypotheses which depend on term. It clears the generalized hypotheses.

8.3.11  revert ident₁ … ident_n

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

Error messages:

1. ident is used in the hypothesis ident’

Variants:

1. revert dependent ident

   This moves to the goal the hypothesis ident and all hypotheses which depend on it.

8.3.12  change term

This tactic applies to any goal. It implements the rule “Conv” given in Section 4.3. change U replaces the current goal T with U providing that U is well-formed and that T and U are convertible.

Error messages:

1. Not convertible

Variants:

1. change term₁ with term₂

   This replaces the occurrences of term₁ by term₂ in the current goal. The terms term₁ and term₂ must be convertible.

2. change term₁ at num₁ … num_i with term₂

   This replaces the occurrences numbered num₁ … num_i of term₁ by term₂ in the current goal. The terms term₁ and term₂ must be convertible.

   
   Error message: Too few occurrences

3. change term in ident
4. change term₁ with term₂ in ident
5. change term₁ at num₁ … num_i with term₂ in ident

   This applies the change tactic not to the goal but to the hypothesis ident.

See also: 8.5

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

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

Variants:

1. fix ident₁ num with ( ident₂ binder₂  …  binder₂ [{ struct ident′₂ }] : type₂ ) … ( ident₁ binder_n  …  binder_n [{ struct ident′_n }] : type_n )

   This starts a proof by mutual induction. The statements to be simultaneously proved are respectively forall binder₂  …  binder₂, type₂, …, forall binder_n  …  binder_n, type_n. The identifiers ident₁ … ident_n are the names of the induction hypotheses. The identifiers ident′₂ … ident′_n 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).

8.3.14  cofix ident

This tactic starts a proof by coinduction. The identifier ident is the name given to the coinduction hypothesis. Like in a cofix expression, the use of induction hypotheses have to guarded by a constructor. The verification that the use of coinductive hypotheses is correct is done only at the time of registering the lemma in the environment. To know if the use of coinduction hypotheses is correct at some time of the interactive development of a proof, use the command Guarded (see Section 7.3.2).

Variants:

1. cofix ident₁ with ( ident₂ binder₂  …  binder₂ : type₂ ) … ( ident₁ binder₁  …  binder₁ : type_n )

   This starts a proof by mutual coinduction. The statements to be simultaneously proved are respectively forall binder₂  …  binder₂, type₂, …, forall binder_n  …  binder_n, type_n. The identifiers ident₁ … ident_n are the names of the coinduction hypotheses.

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

8.3.16  instantiate (num:= term)

The instantiate tactic allows to solve an existential variable with the term term. The num argument is the position of the existential variable from right to left in the conclusion. This cannot be the number of the existential variable since this number is different in every session.

Variants:

1. instantiate (num:=term) in ident
2. instantiate (num:=term) in (Value of ident)
3. instantiate (num:=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.

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

8.3.17  admit

The admit tactic “solves” the current subgoal by an axiom. This typically allows to temporarily skip a subgoal so as to progress further in the rest of the proof. To know if some proof still relies on unproved subgoals, one can use the command Print Assumptions (see Section 6.3.5). Admitted subgoals have names of the form ident_admitted possibly followed by a number.

8.3.18  constr_eq term₁ term₂

This tactic applies to any goal. It checks whether its arguments are equal modulo alpha conversion and casts.

Error message: Not equal

8.3.19  is_evar term

This tactic applies to any goal. It checks whether its argument is an existential variable. Existential variables are uninstantiated variables generated by e.g. eapply (see Section 8.3.6).

Error message: Not an evar

8.3.20  has_evar term

This tactic applies to any goal. It 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 message: No evars

8.3.21  is_var term

This tactic applies to any goal. It checks whether its argument is a variable or hypothesis in the current goal context or in the opened sections.

Error message: Not a variable or hypothesis

8.3.22  Bindings list

Tactics that take a term as argument may also support a bindings list, so as to instantiate some parameters of the term by name or position. The general form of a term equipped with a bindings list is term with bindings_list where bindings_list may be of two different forms:

• In a bindings list of the form (ref₁ := term₁) … (ref_n := term_n), ref is either an ident or a num. The references are determined according to the type of term. If ref_i is an identifier, this identifier has to be bound in the type of term and the binding provides the tactic with an instance for the parameter of this name. If ref_i is some number n, this number denotes the n-th non dependent premise of the term, as determined by the type of term.

  
  Error message: No such binder

• A bindings list can also be a simple list of terms term₁ …term_n. In that case the references to which these terms correspond are determined by the tactic. In case of induction, destruct, elim and case (see Section 11) the terms have to provide instances for all the dependent products in the type of term while in the case of apply, or of constructor and its variants, only instances for the dependent products which are not bound in the conclusion of the type are required.

  
  Error message: Not the right number of missing arguments

8.3.23  Occurrences sets and occurrences clauses

An occurrences clause is a modifier to some tactics that obeys the following syntax:

The role of an occurrence clause is to select a set of occurrences of a term in a goal. In the first case, the ident_i [at num₁ⁱ … num_niⁱ] parts indicate that occurrences have to be selected in the hypotheses named ident_i. If no numbers are given for hypothesis ident_i, then all occurrences of term in the hypothesis are selected. If numbers are given, they refer to occurrences of term when the term is printed using option Set Printing All (see Section 2.9), counting from left to right. In particular, occurrences of term in implicit arguments (see Section 2.7) or coercions (see Section 2.8) are counted.

If a minus sign is given between at and the list of occurrences, it negates the condition so that the clause denotes all the occurrences except the ones explicitly mentioned after the minus sign.

As an exception to the left-to-right order, the occurrences in the return subexpression of a match are considered before the occurrences in the matched term.

In the second case, the * on the left of |- means that all occurrences of term are selected in every hypothesis.

In the first and second case, if * is mentioned on the right of |-, the occurrences of the conclusion of the goal have to be selected. If some numbers are given, then only the occurrences denoted by these numbers are selected. In no numbers are given, all occurrences of term in the goal are selected.

Finally, the last notation is an abbreviation for * |- *. Note also that |- is optional in the first case when no * is given.

Here are some tactics that understand occurrences clauses: set, remember, induction, destruct.

See also:  Sections 8.3.7, 8.7, 2.9.

8.4  Negation and contradiction

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

8.4.2  contradiction

This tactic applies to any goal. The contradiction tactic attempts to find in the current context (after all intros) one hypothesis which is equivalent to False. It permits to prune irrelevant cases. This tactic is a macro for the tactics sequence intros; elimtype False; assumption.

Error messages:

1. No such assumption

Variants:

1. contradiction ident

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

8.4.3  contradict ident

This tactic allows to manipulate 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

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

8.5  Conversion tactics

This set of tactics implements different specialized usages of the tactic change.

All conversion tactics (including change) can be parameterized by the parts of the goal where the conversion can occur. This is done using goal clauses which consists in a list of hypotheses and, optionally, of a reference to the conclusion of the goal. For defined hypothesis it is possible to specify if the conversion should occur on the type part, the body part or both (default).

Goal clauses are written after a conversion tactic (tactics set 8.3.7, rewrite 8.8.1, replace 8.8.3 and autorewrite 8.12.13 also use goal clauses) and are introduced by the keyword in. If no goal clause is provided, the default is to perform the conversion only in the conclusion.

The syntax and description of the various goal clauses is the following:

in ident₁ … ident_n |- only in hypotheses ident₁ …ident_n

in ident₁ … ident_n |- * in hypotheses ident₁ …ident_n and in the conclusion

in * |- in every hypothesis

in * (equivalent to in * |- *) everywhere

in (type of ident₁) (value of ident₂) … |- in type part of ident₁, in the value part of ident₂, etc.

For backward compatibility, the notation in ident₁…ident_n performs the conversion in hypotheses ident₁…ident_n.

8.5.1  cbv flag₁ … flag_n, lazy flag₁ … flag_n and compute

These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. In correspondence with the kinds of reduction considered in Coq  namely β (reduction of functional application), δ (unfolding of transparent constants, see 6.10.2), ι (reduction of pattern-matching over a constructed term, and unfolding of fix and cofix expressions) and ζ (contraction of local definitions), the flag are either beta, delta, iota or zeta. The delta flag itself can be refined into delta [qualid₁…qualid_k] or delta -[qualid₁…qualid_k], restricting in the first case the constants to unfold to the constants listed, and restricting in the second case the constant to unfold to all but the ones explicitly mentioned. Notice that the delta flag does not apply to variables bound by a let-in construction inside the term itself (use here the zeta flag). In any cases, opaque constants are not unfolded (see Section 6.10.1).

The goal may be normalized with two strategies: lazy (lazy tactic), or call-by-value (cbv tactic). The lazy strategy is a call-by-need strategy, with sharing of reductions: the arguments of a function call are partially evaluated only when necessary, and if an argument is used several times then it is computed only once. This reduction is efficient for reducing expressions with dead code. For instance, the proofs of a proposition exists x. P(x) reduce to a pair of a witness t, and a proof that t satisfies the predicate P. Most of the time, t may be computed without computing the proof of P(t), thanks to the lazy strategy.

The call-by-value strategy is the one used in ML languages: the arguments of a function call are evaluated first, using a weak reduction (no reduction under the λ-abstractions). Despite the lazy strategy always performs fewer reductions than the call-by-value strategy, the latter is generally more efficient for evaluating purely computational expressions (i.e. with few dead code).

Variants:

1. compute
   cbv

   These are synonyms for cbv beta delta iota zeta.

2. lazy

   This is a synonym for lazy beta delta iota zeta.

3. compute [qualid₁…qualid_k]
   cbv [qualid₁…qualid_k]

   These are synonyms of cbv beta delta [qualid₁…qualid_k] iota zeta.

4. compute -[qualid₁…qualid_k]
   cbv -[qualid₁…qualid_k]

   These are synonyms of cbv beta delta -[qualid₁…qualid_k] iota zeta.

5. lazy [qualid₁…qualid_k]
   lazy -[qualid₁…qualid_k]

   These are respectively synonyms of cbv beta delta [qualid₁…qualid_k] iota zeta and cbv beta delta -[qualid₁…qualid_k] iota zeta.

6. vm_compute

   This tactic evaluates the goal using the optimized call-by-value evaluation bytecode-based virtual machine. This algorithm is dramatically more efficient than the algorithm used for the cbv tactic, but it cannot be fine-tuned. It is specially interesting for full evaluation of algebraic objects. This includes the case of reflexion-based tactics.

8.5.2  red

This tactic applies to a goal which has the form forall (x:T1)…(xk:Tk), c t1 … tn where c is a constant. If c is transparent then it replaces c with its definition (say t) and then reduces (t t1 … tn) according to βιζ-reduction rules.

Error messages:

1. Not reducible

8.5.3  hnf

This tactic applies to any goal. It replaces the current goal with its head normal form according to the βδιζ-reduction rules, i.e. it reduces the head of the goal until it becomes a product or an irreducible term.

Example: The term forall n:nat, (plus (S n) (S n)) is not reduced by hnf.

Remark: The δ rule only applies to transparent constants (see Section 6.10.1 on transparency and opacity).

8.5.4  simpl

This tactic applies to any goal. The tactic simpl first applies βι-reduction rule. Then it expands transparent constants and tries to reduce T’ according, once more, to βι rules. But when the ι rule is not applicable then possible δ-reductions are not applied. For instance trying to use simpl on (plus n O)=n changes nothing. Notice that only transparent constants whose name can be reused as such in the recursive calls are possibly unfolded. For instance a constant defined by plus’ := plus is possibly unfolded and reused in the recursive calls, but a constant such as succ := plus (S O) is never unfolded.

Variants:

1. simpl term

   This applies simpl only to the occurrences of term in the current goal.

2. simpl term at num₁ … num_i

   This applies simpl only to the num₁, …, num_i occurrences of term in the current goal.

   
   Error message: Too few occurrences

3. simpl ident

   This applies simpl only to the applicative subterms whose head occurrence is ident.

4. simpl ident at num₁ … num_i

   This applies simpl only to the num₁, …, num_i applicative subterms whose head occurrence is ident.

8.5.5  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 messages:

1. qualid does not denote an evaluable constant

Variants:

1. unfold qualid₁, …, qualid_n

   Replaces simultaneously qualid₁, …, qualid_n with their definitions and replaces the current goal with its βι normal form.

2. unfold qualid₁ at num₁¹, …, num_i¹, …, qualid_n at num₁ⁿ … num_jⁿ

   The lists num₁¹, …, num_i¹ and num₁ⁿ, …, num_jⁿ specify the occurrences of qualid₁, …, qualid_n to be unfolded. Occurrences are located from left to right.

   
   Error message: bad occurrence number of qualid_i

   
   Error message: qualid_i does not occur

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

4. 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).

5. unfold qualid_or_string₁ at num₁¹, …, num_i¹, …, qualid_or_string_n at num₁ⁿ … num_jⁿ

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

8.5.6  fold term

This tactic applies to any goal. The term term is reduced using the red tactic. Every occurrence of the resulting term in the goal is then replaced by term.

Variants:

1. fold term₁ … term_n

   Equivalent to fold term₁;…; fold term_n.

8.5.7  pattern term

This command applies to any goal. The argument term must be a free subterm of the current goal. The command pattern performs β-expansion (the inverse of β-reduction) of the current goal (say T) by

1. replacing all occurrences of term in T with a fresh variable
2. abstracting this variable
3. applying the abstracted goal to term

For instance, if the current goal T is expressible has φ(t) where the notation captures all the instances of t in φ(t), then pattern t transforms it into (fun x:A => φ(x)) t. This command can be used, for instance, when the tactic apply fails on matching.

Variants:

1. pattern term at num₁ … num_n

   Only the occurrences num₁ … num_n of term are considered for β-expansion. Occurrences are located from left to right.

2. pattern term at - num₁ … num_n

   All occurrences except the occurrences of indexes num₁ … num_n of term are considered for β-expansion. Occurrences are located from left to right.

3. pattern term₁, …, term_m

   Starting from a goal φ(t₁ … t_m), the tactic pattern t₁, …, t_m generates the equivalent goal (fun (x₁:A₁) … (x_m:A_m) => φ(x₁… x_m)) t₁ … t_m.
   If t_i occurs in one of the generated types A_j these occurrences will also be considered and possibly abstracted.

4. pattern term₁ at num₁¹ … num_n1¹, …, term_m at num₁^m … num_nm^m

   This behaves as above but processing only the occurrences num₁¹, …, num_i¹ of term₁, …, num₁^m, …, num_j^m of term_m starting from term_m.

5. pattern term₁ [at [-] num₁¹ … num_n1¹] , …, term_m [at [-] num₁^m … num_nm^m]

   This is the most general syntax that combines the different variants.

8.5.8  Conversion tactics applied to hypotheses

conv_tactic in ident₁ … ident_n

Applies the conversion tactic conv_tactic to the hypotheses ident₁, …, ident_n. The tactic conv_tactic is any of the conversion tactics listed in this section.

If ident_i is a local definition, then ident_i can be replaced by (Type of ident_i) to address not the body but the type of the local definition. Example: unfold not in (Type of H1) (Type of H3).

Error messages:

1. No such hypothesis : ident.

8.6  Introductions

Introduction tactics address goals which are inductive constants. They are used when one guesses that the goal can be obtained with one of its constructors’ type.

8.6.1  constructor num

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

Error messages:

1. Not an inductive product
2. Not enough constructors

Variants:

1. constructor

   This tries constructor 1 then constructor 2, … , then constructor n where n if the number of constructors of the head of the goal.

2. constructor num with bindings_list

   Let ci be the i-th constructor of I, then constructor i with bindings_list is equivalent to intros; apply ci with bindings_list.

   
   Warning: the terms in the bindings_list 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).

3. split

   Applies if I has only one constructor, typically in the case of conjunction A∧ B. Then, it is equivalent to constructor 1.

4. exists bindings_list

   Applies if I has only one constructor, for instance in the case of existential quantification ∃ x· P(x). Then, it is equivalent to intros; constructor 1 with bindings_list.

5. exists bindings_list , … , bindings_list

   This iteratively applies exists bindings_list.

6. left
   right

   Apply if I has two constructors, for instance in the case of disjunction A∨ B. Then, they are respectively equivalent to constructor 1 and constructor 2.

7. left with bindings_list
   right with bindings_list
   split with bindings_list

   As soon as the inductive type has the right number of constructors, these expressions are equivalent to calling constructor i with bindings_list for the appropriate i.

8. econstructor
   eexists
   esplit
   eleft
   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 Section 10.2).

8.7  Induction and Case Analysis

The tactics presented in this section implement induction or case analysis on inductive or coinductive objects (see Section 4.5).

8.7.1  induction term

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

The tactic induction automatically replaces every occurrences of term in the conclusion and the hypotheses of the goal. It automatically adds induction hypotheses (using names of the form IHn1) to the local context. If some hypothesis must not be taken into account in the induction hypothesis, then it needs to be removed first (you can also use the tactics elim or simple induction, see below).

There are particular cases:

• If term is an identifier ident denoting a quantified variable of the conclusion of the goal, then induction ident behaves as intros until ident; induction ident.
• If term is a num, then induction num behaves as intros until num followed by induction applied to the last introduced hypothesis.

  
  Remark: For simple induction on a numeral, use syntax induction (num) (not very interesting anyway).

Example:

Error messages:

1. Not an inductive product
2. Unable to find an instance for the variables ident …ident

   Use in this case the variant elim … with … below.

Variants:

1. induction term as disj_conj_intro_pattern

   This behaves as induction term but uses the names in disj_conj_intro_pattern to name the variables introduced in the context. The disj_conj_intro_pattern must typically be of the form [ p₁₁ …p_1n1 | … | p_m1 …p_mnm ] 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_ini 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 Section 8.7.3). For instance, for an inductive type with one constructor, the pattern notation (p₁,…,p_n) can be used instead of [ p₁ …p_n ].

2. induction term as naming_intro_pattern

   This behaves as induction term but adds an equation between term and the value that term takes in each of the induction case. The name of the equation is built according to naming_intro_pattern which can be an identifier, a “?”, etc, as indicated in Section 8.7.3.

3. induction term as naming_intro_pattern disj_conj_intro_pattern

   This combines the two previous forms.

4. induction term with bindings_list

   This behaves like induction term providing explicit instances for the premises of the type of term (see the syntax of bindings in Section 8.3.22).

5. einduction term

   This tactic behaves like induction term excepts 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 (see Section 10.2).

6. induction term₁ using term₂

   This behaves as induction term₁ but using term₂ as induction scheme. It does not expect the conclusion of the type of term₁ to be inductive.

7. induction term₁ using term₂ with bindings_list

   This behaves as induction term₁ using term₂ but also providing instances for the premises of the type of term₂.

8. induction term₁ … term_n 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.

9. induction term in goal_occurrences

   This syntax is used for selecting which occurrences of term the induction has to be carried on. The in at_occurrences clause is an occurrence clause whose syntax and behavior is described in Section 8.3.23.

   When an occurrence clause is given, an equation between term and the value it gets in each case of the induction is added to the context of the subgoals corresponding to the induction cases (even if no clause as naming_intro_pattern is given).

10. induction term₁ with bindings_list₁ as naming_intro_pattern disj_conj_intro_pattern using term₂ with bindings_list₂ in goal_occurrences
    einduction term₁ with bindings_list₁ as naming_intro_pattern disj_conj_intro_pattern using term₂ with bindings_list₂ 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.

11. 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 proof 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.

12. elim term with bindings_list

    Allows to give explicit instances to the premises of the type of term (see Section 8.3.22).

13. eelim term

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

14. elim term₁ using term₂
    elim term₁ using term₂ with bindings_list

    Allows the user to give explicitly an elimination predicate term₂ which is not the standard one for the underlying inductive type of term₁. The bindings_list clause allows to instantiate premises of the type of term₂.

15. elim term₁ with bindings_list₁ using term₂ with bindings_list₂
    eelim term₁ with bindings_list₁ using term₂ with bindings_list₂

    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.

16. elimtype form

    The argument form 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 and which does not occur in the goal then elim t is equivalent to elimtype I; 2: exact t.

17. simple induction ident

    This tactic behaves as intros until ident; elim ident when ident is a quantified variable of the goal.

18. simple induction num

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

8.7.2  destruct term

The tactic destruct is used to perform case analysis without recursion. Its behavior is similar to induction except that no induction hypothesis is generated. It applies to any goal and the type of term must be inductively defined. There are particular cases:

• If term is an identifier ident denoting a quantified variable of the conclusion of the goal, then destruct ident behaves as intros until ident; destruct ident.
• If term is a num, then destruct num behaves as intros until num followed by destruct applied to the last introduced hypothesis.

  
  Remark: For destruction of a numeral, use syntax destruct (num) (not very interesting anyway).

Variants:

1. destruct term as disj_conj_intro_pattern

   This behaves as destruct term but uses the names in intro_pattern to name the variables introduced in the context. The intro_pattern must have the form [ p₁₁ …p_1n1 | … | p_m1 …p_mnm ] 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 p_i1 …p_ini in order. If there are not enough names, destruct invents names for the remaining variables to introduce. More generally, the p_ij can be any disjunctive/conjunctive introduction pattern (see Section 8.7.3). This provides a concise notation for nested destruction.

2. destruct term as disj_conj_intro_pattern _eqn

   This behaves as destruct term but adds an equation between term and the value that term takes in each of the possible cases. The name of the equation is chosen by Coq. If disj_conj_intro_pattern is simply [], it is automatically considered as a disjunctive pattern of the appropriate size.

3. destruct term as disj_conj_intro_pattern _eqn: naming_intro_pattern

   This behaves as destruct term as disj_conj_intro_pattern _eqn but use naming_intro_pattern to name the equation (see Section 8.7.3). Note that spaces can generally be removed around _eqn.

4. destruct term with bindings_list

   This behaves like destruct term providing explicit instances for the dependent premises of the type of term (see syntax of bindings in Section 8.3.22).

5. edestruct term

   This tactic behaves like destruct term excepts 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 (see Section 10.2).

6. destruct term₁ using term₂
   destruct term₁ using term₂ with bindings_list

   These are synonyms of induction term₁ using term₂ and induction term₁ using term₂ with bindings_list.

7. 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 Section 8.3.23.

   When an occurrence clause is given, an equation between term and the value it gets in each case of the analysis is added to the context of the subgoals corresponding to the cases (even if no clause as naming_intro_pattern is given).

8. destruct term₁ with bindings_list₁ as disj_conj_intro_pattern _eqn: naming_intro_pattern using term₂ with bindings_list₂ in goal_occurrences
   edestruct term₁ with bindings_list₁ as disj_conj_intro_pattern _eqn: naming_intro_pattern using term₂ with bindings_list₂ in goal_occurrences

   These are the general forms of destruct and edestruct. They combine the effects of the with, as, using, and in clauses.

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

10. case_eq term

    The tactic case_eq is a variant of the case tactic that allow 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. The effect of this tactic is similar to the effect of destruct term in |- * with the exception that no new hypotheses are introduced in the context.

11. case term with bindings_list

    Analogous to elim term with bindings_list above.

12. ecase term
    ecase term with bindings_list

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

13. simple destruct ident

    This tactic behaves as intros until ident; case ident when ident is a quantified variable of the goal.

14. simple destruct num

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

8.7.3  intros intro_pattern … intro_pattern

This extension of the tactic intros combines introduction of variables or hypotheses and case analysis. An introduction pattern is either:

• A naming introduction pattern, i.e. either one of:
  • the pattern ?
  • the pattern ?ident
  • an identifier
• A disjunctive/conjunctive introduction pattern, i.e. either one of:
  • a disjunction of lists of patterns: [p₁₁ … p_1m1 | … | p₁₁ … p_nmn]
  • a conjunction of patterns: ( p₁ , … , p_n )
  • a list of patterns ( p₁ & … & p_n ) for sequence of right-associative binary constructs
• the wildcard: _
• the rewriting orientations: -> or <-

Assuming a goal of type Q -> P (non dependent product), or of type forall x:T, P (dependent product), the behavior of intros p is defined inductively over the structure of the introduction pattern p:

• introduction on ? performs the introduction, and lets Coq choose a fresh name for the variable;
• introduction on ?ident performs the introduction, and lets Coq choose a fresh name for the variable based on ident;
• introduction on ident behaves as described in Section 8.3.5;
• introduction over a disjunction of list of patterns [p₁₁ … p_1m1 | … | p₁₁ … p_nmn] expects the product to be over an inductive type whose number of constructors is n (or more generally over a type of conclusion an inductive type built from n constructors, e.g. C -> A\/B if n=2): it destructs the introduced hypothesis as destruct (see Section 8.7.2) would and applies on each generated subgoal the corresponding tactic; intros p_i1 … p_imi; if the disjunctive pattern is part of a sequence of patterns and is not the last pattern of the sequence, then Coq completes the pattern so as all the argument of the constructors of the inductive type are introduced (for instance, the list of patterns [ | ] H applied on goal forall x:nat, x=0 -> 0=x behaves the same as the list of patterns [ | ? ] H);
• introduction over a conjunction of patterns (p₁, …, p_n) expects the goal to be a product over an inductive type I with a single constructor that itself has at least n arguments: it performs a case analysis over the hypothesis, as destruct would, and applies the patterns p₁ … p_n to the arguments of the constructor of I (observe that (p₁, …, p_n) is an alternative notation for [p₁ … p_n]);
• introduction via ( p₁ & …& p_n ) is a shortcut for introduction via (p₁,(…,(…,p_n)…)); it expects the hypothesis to be a sequence of right-associative binary inductive constructors such as conj or ex_intro; for instance, an hypothesis with type A/\exists x, B/\C/\D can be introduced via pattern (a & x & b & c & d);
• introduction on the wildcard depends on whether the product is dependent or not: in the non dependent case, it erases the corresponding hypothesis (i.e. it behaves as an intro followed by a clear, cf Section 8.3.2) while in the dependent case, it succeeds and erases the variable only if the wildcard is part of a more complex list of introduction patterns that also erases the hypotheses depending on this variable;
• introduction over -> (respectively <-) expects the hypothesis to be an equality and the right-hand-side (respectively the left-hand-side) is replaced by the left-hand-side (respectively the right-hand-side) in both the conclusion and the context of the goal; if moreover the term to substitute is a variable, the hypothesis is removed.

Remark: intros p₁ … p_n is not equivalent to intros p₁;…; intros p_n for the following reasons:

• A wildcard pattern never succeeds when applied isolated on a dependent product, while it succeeds as part of a list of introduction patterns if the hypotheses that depends on it are erased too.
• A disjunctive or conjunctive pattern followed by an introduction pattern forces the introduction in the context of all arguments of the constructors before applying the next pattern while a terminal disjunctive or conjunctive pattern does not. Here is an example
  Coq < Goal forall n:nat, n = 0 -> n = 0.
  1 subgoal
    
    ============================
     forall n : nat, n = 0 -> n = 0
  
  Coq < intros [ | ] H.
  2 subgoals
    
    H : 0 = 0
    ============================
     0 = 0
  subgoal 2 is:
   S n = 0
  
  Coq < Show 2.
  subgoal 2 is:
    
    n : nat
    H : S n = 0
    ============================
     S n = 0
  
  Coq < Undo.
  1 subgoal
    
    ============================
     forall n : nat, n = 0 -> n = 0
  
  Coq < intros [ | ]; intros H.
  2 subgoals
    
    H : 0 = 0
    ============================
     0 = 0
  subgoal 2 is:
   S H = 0 -> S H = 0
  
  Coq < Show 2.
  subgoal 2 is:
    
    H : nat
    ============================
     S H = 0 -> S H = 0
  

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

1. double induction num₁ num₂

   This tactic is deprecated and should be replaced by induction num₁; induction num₃ where num₃ is the result of num₂-num₁.

8.7.5  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 [98] and the work of Cristina Cornes around inversion [35]. 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. A simple example is the following:

Here we didn’t 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.

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.

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

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. Common useful variants are the following, defined in the same file:

Variants:

1. dependent induction ident generalizing ident₁ …ident_n

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

2. dependent destruction ident

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

A larger example of dependent induction and an explanation of the underlying technique are developed in section 10.6.

8.7.6  decompose [ qualid₁ … qualid_n ] term

This tactic allows to recursively decompose a complex proposition in order to obtain atomic ones. Example:

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

Variants:

1. decompose sum term This decomposes sum types (like or).
2. decompose record term This decomposes record types (inductive types with one constructor, like and and exists and those defined with the Record macro, see Section 2.1).

8.7.7  functional induction (qualid term₁ … term_n).

The experimental tactic functional induction performs case analysis and induction following the definition of a function. It makes use of a principle generated by Function (see Section 2.3) or Functional Scheme (see Section 8.15).

Remark: (qualid term₁ … term_n) must be a correct full application of qualid. In particular, the rules for implicit arguments are the same as usual. For example use @qualid if you want to write implicit arguments explicitly.

Remark: Parenthesis over qualid…term_n are mandatory.

Remark: functional induction (f x1 x2 x3) is actually a wrapper for induction x1 x2 x3 (f x1 x2 x3) using qualid followed by a cleaning phase, where qualid is the induction principle registered for f (by the Function (see Section 2.3) or Functional Scheme (see Section 8.15) command) corresponding to the sort of the goal. Therefore functional induction may fail if the induction scheme (qualid) is not defined. See also Section 2.3 for the function terms accepted by Function.

Remark: There is a difference between obtaining an induction scheme for a function by using Function (see Section 2.3) and by using Functional Scheme after a normal definition using Fixpoint or Definition. See 2.3 for details.

See also: 2.3,8.15,10.4, 8.10.3

Error messages:

1. Cannot find induction information on qualid

    

2. Not the right number of induction arguments

Variants:

1. functional induction (qualid term₁ … term_n) using term_m+1 with term_n+1 …term_m

   Similar to Induction and elim (see Section 8.7), allows to give explicitly the induction principle and the values of dependent premises of the elimination scheme, including predicates for mutual induction when qualid is part of a mutually recursive definition.

2. functional induction (qualid term₁ … term_n) using term_m+1 with ref₁ := term_n+1 … ref_m := term_n

   Similar to induction and elim (see Section 8.7).

3. All previous variants can be extended by the usual as intro_pattern construction, similar for example to induction and elim (see Section 8.7).

8.8  Equality

These tactics use the equality eq:forall A:Type, A->A->Prop defined in file Logic.v (see Section 3.1.2). The notation for eq T t u is simply t=u dropping the implicit type of t and u.

8.8.1  rewrite term

This tactic applies to any goal. The type of term must have the form

forall (x₁:A₁) … (x_n:A_n)eq term₁ term₂.

where eq is the Leibniz equality or a registered setoid equality.

Then rewrite term finds the first subterm matching term₁ in the goal, resulting in instances term₁′ and term₂′ and then replaces every occurrence of term₁′ by term₂′. Hence, some of the variables x_i are solved by unification, and some of the types A₁, …, A_n become new subgoals.

Error messages:

1. The term provided does not end with an equation
2. Tactic generated a subgoal identical to the original goal
   This happens if term₁ does not occur in the goal.

Variants:

1. rewrite -> term
   Is equivalent to rewrite term
2. rewrite <- term
   Uses the equality term₁=term₂ from right to left
3. rewrite term in clause
   Analogous to rewrite term but rewriting is done following clause (similarly to 8.5). For instance:
   • rewrite H in H1 will rewrite H in the hypothesis H1 instead of the current goal.
   • rewrite H in H1 at 1, H2 at - 2 |- * means rewrite H; rewrite H in H1 at 1; rewrite H in H2 at - 2. In particular a failure will happen if any of these three simpler tactics fails.
   • rewrite H in * |- will do rewrite H in H_i for all hypothesis H_i <> H. A success will happen as soon as at least one of these simpler tactics succeeds.
   • rewrite H in * is a combination of rewrite H and rewrite H in * |- that succeeds if at least one of these two tactics succeeds.
   Orientation -> or <- can be inserted before the term to rewrite.
4. rewrite term at occurrences

   Rewrite only the given occurrences of term₁′. Occurrences are specified from left to right as for pattern (§8.5.7). The rewrite is always performed using setoid rewriting, even for Leibniz’s equality, so one has to Import Setoid to use this variant.

5. rewrite term by tactic

   Use tactic to completely solve the side-conditions arising from the rewrite.

6. rewrite term₁, …, term_n
   Is equivalent to the n successive tactics rewrite term₁ up to rewrite term_n, each one working on the first subgoal generated by the previous one. Orientation -> or <- can be inserted before each term to rewrite. One unique clause can be added at the end after the keyword in; it will then affect all rewrite operations.
7. In all forms of rewrite described above, a term to rewrite can be immediately prefixed by one of the following modifiers:
   • ? : the tactic rewrite ?term performs the rewrite of term as many times as possible (perhaps zero time). This form never fails.
   • n? : works similarly, except that it will do at most n rewrites.
   • ! : works as ?, except that at least one rewrite should succeed, otherwise the tactic fails.
   • n! (or simply n) : precisely n rewrites of term will be done, leading to failure if these n rewrites are not possible.
8. erewrite term

   This tactic works as rewrite term but turning unresolved bindings into existential variables, if any, instead of failing. It has the same variants as rewrite has.

8.8.2  cutrewrite -> term₁ = term₂

This tactic acts like replace term₁ with term₂ (see below).

8.8.3  replace term₁ with term₂

This tactic applies to any goal. It replaces all free occurrences of term₁ in the current goal with term₂ and generates the equality term₂=term₁ as a subgoal. This equality is automatically solved if it occurs amongst the assumption, or if its symmetric form occurs. It is equivalent to cut term₂=term₁; [intro Hn; rewrite <- Hn; clear Hn| assumption || symmetry; try assumption].

Error messages:

1. terms do not have convertible types

Variants:

1. replace term₁ with term₂ by tactic
   This acts as replace term₁ with term₂ but applies tactic to solve the generated subgoal term₂=term₁.
2. replace term
   Replace term with term’ using the first assumption whose type has the form term=term’ or term’=term
3. replace -> term
   Replace term with term’ using the first assumption whose type has the form term=term’
4. replace <- term
   Replace term with term’ using the first assumption whose type has the form term’=term
5. replace term₁ with term₂ clause
   replace term₁ with term₂ clause by tactic
   replace term clause
   replace -> term clause
   replace <- term clause
   Act as before but the replacements take place in clause (see Section 8.5) and not only in the conclusion of the goal.
   The clause argument must not contain any type of nor value of.

8.8.4  reflexivity

This tactic applies to a goal which 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 messages:

1. The conclusion is not a substitutive equation
2. Impossible to unify … with ….

8.8.5  symmetry

This tactic applies to a goal which 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.

8.8.6  transitivity term

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

8.8.7  subst ident

This tactic applies to a goal which has ident in its context and (at least) one hypothesis, say H, of type ident=t or t=ident. Then it replaces ident by t everywhere in the goal (in the hypotheses and in the conclusion) and clears ident and H from the context.

Remark: When several hypotheses have the form ident=t or t=ident, the first one is used.

Variants:

1. subst ident₁ …ident_n
   Is equivalent to subst ident₁; …; subst ident_n.
2. subst
   Applies subst repeatedly to all identifiers from the context for which an equality exists.

8.8.8  stepl term

This tactic is for chaining rewriting steps. It assumes a goal of the form “R term₁ term₂” where R is a binary relation and relies on a database of lemmas of the form forall x y z, R x y -> eq x z -> R z y where eq is typically a setoid equality. The application of stepl term then replaces the goal by “R term term₂” and adds a new goal stating “eq term term₁”.

Lemmas are added to the database using the command

Declare Left Step term.

The tactic is especially useful for parametric setoids which are not accepted as regular setoids for rewrite and setoid_replace (see Chapter 25).

Variants:

1. stepl term by tactic
   This applies stepl term then applies tactic to the second goal.
2. stepr term
   stepr term by tactic
   This behaves as stepl but on the right-hand-side of the binary relation. Lemmas are expected to be of the form “forall x y z, R x y -> eq y z -> R x z” and are registered using the command

   Declare Right Step term.

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

8.9  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 =.

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

Variants:

1. decide equality term₁ term₂ .
   Solves a goal of the form {term₁=term₂}+{~term₁=term₂}.

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

8.9.3  discriminate term

This tactic proves any goal from an assumption stating that two structurally different terms of an inductive set are equal. For example, from (S (S O))=(S O) we can derive by absurdity any proposition.

The argument term is assumed to be a proof of a statement of conclusion term₁ = term₂ with term₁ and term₂ being elements of an inductive set. To build the proof, the tactic traverses the normal forms⁴ of term₁ and term₂ looking for a couple of subterms u and w (u subterm of the normal form of term₁ and w subterm of the normal form of term₂), placed at the same positions and whose head symbols are two different constructors. If such a couple of subterms exists, then the proof of the current goal is completed, otherwise the tactic fails.

Remark: The syntax discriminate ident can be used to refer to a hypothesis quantified in the goal. In this case, the quantified hypothesis whose name is ident is first introduced in the local context using intros until ident.

Error messages:

1. No primitive equality found
2. Not a discriminable equality

Variants:

1. discriminate num

   This does the same thing as intros until num followed by discriminate ident where ident is the identifier for the last introduced hypothesis.

2. discriminate term with bindings_list

   This does the same thing as discriminate term but using the given bindings to instantiate parameters or hypotheses of term.

3. ediscriminate num
   ediscriminate term [with bindings_list]

   This works the same as discriminate but if the type of term, or the type of the hypothesis referred to by num, has uninstantiated parameters, these parameters are left as existential variables.

4. discriminate

   This behaves like discriminate ident if ident is the name of an hypothesis to which discriminate is applicable; if the current goal is of the form term₁ <> term₂, this behaves as intro ident; injection ident.

   
   Error messages:

   1. No discriminable equalities
      occurs when the goal does not verify the expected preconditions.