Reasoning with inductive types¶
Applying constructors¶
The tactics presented here specialize apply
(and
eapply
) to the case of constructors of inductive types.

Tactic
constructor natural
¶ This tactic applies to a goal such that its conclusion is an inductive type (say
I
). The argumentnatural
must be less or equal to the numbers of constructor(s) ofI
. Letc_{i}
be the ith constructor ofI
, thenconstructor i
is equivalent tointros; apply c_{i}
.
Error
Not an inductive product.
¶

Error
Not enough constructors.
¶

Variant
constructor
This tries
constructor 1
thenconstructor 2
, ..., thenconstructor n
wheren
is the number of constructors of the head of the goal.

Variant
constructor natural with bindings
Let
c
be the ith constructor ofI
, thenconstructor i with bindings
is equivalent tointros; apply c with bindings
.

Variant
split with bindings?
¶ This applies only if
I
has a single constructor. It is then equivalent toconstructor 1 with bindings?
. It is typically used in the case of a conjunction \(A \wedge B\).
Variant
exists bindings
¶ This applies only if
I
has a single constructor. It is then equivalent tointros; constructor 1 with bindings.
It is typically used in the case of an existential quantification \(\exists x, P(x).\)

Error
Not an inductive goal with 1 constructor.
¶

Variant

Variant
left with bindings?
¶ 
Variant
right with bindings?
¶ These tactics apply only if
I
has two constructors, for instance in the case of a disjunction \(A \vee B\). Then, they are respectively equivalent toconstructor 1 with bindings?
andconstructor 2 with bindings?
.
Error
Not an inductive goal with 2 constructors.
¶

Error

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

Error
Case analysis and induction¶
The tactics presented in this section implement induction or case analysis on inductive or coinductive objects (see Theory of inductive definitions).

Tactic
destruct term
¶ This tactic applies to any goal. The argument
term
must be of inductive or coinductive type and the tactic generates subgoals, one for each possible form ofterm
, i.e. one for each constructor of the inductive or coinductive type. Unlikeinduction
, no induction hypothesis is generated bydestruct
.
Variant
destruct ident
If
ident
denotes a quantified variable of the conclusion of the goal, thendestruct ident
behaves asintros until ident; destruct ident
. Ifident
is not anymore dependent in the goal after application ofdestruct
, it is erased (to avoid erasure, use parentheses, as indestruct (ident)
).If
ident
is a hypothesis of the context, andident
is not anymore dependent in the goal after application ofdestruct
, it is erased (to avoid erasure, use parentheses, as indestruct (ident)
).

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

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

Variant
destruct term as or_and_intropattern_loc
This behaves as
destruct term
but uses the names inor_and_intropattern_loc
to name the variables introduced in the context. Theor_and_intropattern_loc
must have the form[p11 ... p1n  ...  pm1 ... pmn ]
withm
being the number of constructors of the type ofterm
. Each variable introduced bydestruct
in the context of thei
th goal gets its name from the listpi1 ... pin
in order. If there are not enough names,destruct
invents names for the remaining variables to introduce. More generally, thepij
can be any introduction pattern (seeintros
). This provides a concise notation for chaining destruction of a hypothesis.

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

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

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

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

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

Variant
destruct term with bindings? as or_and_intropattern_loc? eqn:naming_intropattern? using term with bindings?? in goal_occurrences?

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

Variant

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

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

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

Variant
simple destruct natural
This tactic behaves as
intros until natural; case ident
whereident
is the name given byintros until natural
to thenatural
th nondependent premise of the goal.

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

Tactic
induction term
¶ This tactic applies to any goal. The argument
term
must be of inductive type and the tacticinduction
generates subgoals, one for each possible form ofterm
, i.e. one for each constructor of the inductive type.If the argument is dependent in either the conclusion or some hypotheses of the goal, the argument is replaced by the appropriate constructor form in each of the resulting subgoals and induction hypotheses are added to the local context using names whose prefix is IH.
There are particular cases:
If term is an identifier
ident
denoting a quantified variable of the conclusion of the goal, then inductionident behaves asintros until ident; induction ident
. Ifident
is not anymore dependent in the goal after application ofinduction
, it is erased (to avoid erasure, use parentheses, as ininduction (ident)
).If
term
is anatural
, theninduction natural
behaves asintros until natural
followed byinduction
applied to the last introduced hypothesis.Note
For simple induction on a number, use syntax induction (number) (not very interesting anyway).
In case term is a hypothesis
ident
of the context, andident
is not anymore dependent in the goal after application ofinduction
, it is erased (to avoid erasure, use parentheses, as ininduction (ident)
).The argument
term
can also be a pattern of which holes are denoted by “_”. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are compatible and performs induction using this subterm.
Example
 Lemma induction_test : forall n:nat, n = n > n <= n.
 1 goal ============================ forall n : nat, n = n > n <= n
 intros n H.
 1 goal n : nat H : n = n ============================ n <= n
 induction n.
 2 goals H : 0 = 0 ============================ 0 <= 0 goal 2 is: S n <= S n
 exact (le_n 0).
 1 goal n : nat H : S n = S n IHn : n = n > n <= n ============================ S n <= S n

Error
Not an inductive product.
¶

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

Variant
induction term as or_and_intropattern_loc
This behaves as
induction
but uses the names inor_and_intropattern_loc
to name the variables introduced in the context. Theor_and_intropattern_loc
must typically be of the form[ p
_{11}... p
_{1n} ...  p
_{m1}... p
_{mn}]
withm
being the number of constructors of the type ofterm
. Each variable introduced by induction in the context of the ith goal gets its name from the listp
_{i1}... p
_{in} in order. If there are not enough names, induction invents names for the remaining variables to introduce. More generally, thep
_{ij} can be any disjunctive/conjunctive introduction pattern (seeintros …
). For instance, for an inductive type with one constructor, the pattern notation(p
_{1}, ... , p
_{n})
can be used instead of[ p
_{1}... p
_{n}]
.

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

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

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

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

Variant
induction term+, using qualid
This syntax is used for the case
qualid
denotes an induction principle with complex predicates as the induction principles generated byFunction
orFunctional Scheme
may be.

Variant
induction term in goal_occurrences
This syntax is used for selecting which occurrences of
term
the induction has to be carried on. Thein goal_occurrences
clause is an occurrence clause whose syntax and behavior is described in occurrences sets. If variables or hypotheses not mentioningterm
in their type are listed ingoal_occurrences
, those are generalized as well in the statement to prove.Example
 Lemma comm x y : x + y = y + x.
 1 goal x, y : nat ============================ x + y = y + x
 induction y in x  *.
 2 goals x : nat ============================ x + 0 = 0 + x goal 2 is: x + S y = S y + x
 Show 2.
 goal 2 is: x, y : nat IHy : forall x : nat, x + y = y + x ============================ x + S y = S y + x

Variant
induction term with bindings as or_and_intropattern_loc using term with bindings in goal_occurrences

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

Variant
elim term
¶ This is a more basic induction tactic. Again, the type of the argument
term
must be an inductive type. Then, according to the type of the goal, the tacticelim
chooses the appropriate destructor and applies it as the tacticapply
would do. For instance, if the local context containsn:nat
and the current goal isT
of typeProp
, thenelim n
is equivalent toapply nat_ind with (n:=n)
. The tacticelim
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 ofterm
is a statement with premises and whose conclusion is inductive. In that case the tactic performs induction on the conclusion of the type ofterm
and leaves the nondependent premises of the type as subgoals. In the case of dependent products, the tactic tries to find an instance for which the elimination lemma applies and fails otherwise.

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

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

Variant
elim term using term

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

Variant
elim term with bindings using term with bindings

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

Variant
elimtype type
¶ The argument
type
must be inductively defined.elimtype I
is equivalent tocut I. intro Hn; elim Hn; clear Hn.
Therefore the hypothesisHn
will not appear in the context(s) of the subgoal(s). Conversely, ift
is aterm
of (inductive) typeI
that does not occur in the goal, thenelim t
is equivalent toelimtype I; 2:exact t.

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

Variant
simple induction natural
This tactic behaves as
intros until natural; elim ident
whereident
is the name given byintros until natural
to thenatural
th nondependent premise of the goal.

Tactic
dependent induction ident
¶ The experimental tactic dependent induction performs induction inversion on an instantiated inductive predicate. One needs to first require the Coq.Program.Equality module to use this tactic. The tactic is based on the BasicElim tactic by Conor McBride [McB00] and the work of Cristina Cornes around inversion [CT95]. From an instantiated inductive predicate and a goal, it generates an equivalent goal where the hypothesis has been generalized over its indexes which are then constrained by equalities to be the right instances. This permits to state lemmas without resorting to manually adding these equalities and still get enough information in the proofs.
Example
 Lemma lt_1_r : forall n:nat, n < 1 > n = 0.
 1 goal ============================ forall n : nat, n < 1 > n = 0
 intros n H ; induction H.
 2 goals n : nat ============================ n = 0 goal 2 is: n = 0
Here we did not get any information on the indexes to help fulfill
this proof. The problem is that, when we use the induction
tactic, we
lose information on the hypothesis instance, notably that the second
argument is 1 here. Dependent induction solves this problem by adding
the corresponding equality to the context.
 Require Import Coq.Program.Equality.
 Lemma lt_1_r : forall n:nat, n < 1 > n = 0.
 1 goal ============================ forall n : nat, n < 1 > n = 0
 intros n H ; dependent induction H.
 2 goals ============================ 0 = 0 goal 2 is: n = 0
The subgoal is cleaned up as the tactic tries to automatically simplify the subgoals with respect to the generated equalities. In this enriched context, it becomes possible to solve this subgoal.
 reflexivity.
 1 goal n : nat H : S n <= 0 IHle : 0 = 1 > n = 0 ============================ n = 0
Now we are in a contradictory context and the proof can be solved.
 inversion H.
 No more goals.
This technique works with any inductive predicate. In fact, the
dependent induction
tactic is just a wrapper around the induction
tactic. One can make its own variant by just writing a new tactic
based on the definition found in Coq.Program.Equality
.

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

Variant
dependent destruction ident
¶ This performs the generalization of the instance
ident
but usesdestruct
instead of induction on the generalized hypothesis. This gives results equivalent toinversion
ordependent inversion
if the hypothesis is dependent.
See also the larger example of dependent induction
and an explanation of the underlying technique.
See also

Tactic
discriminate term
¶ This tactic proves any goal from an assumption stating that two structurally different
term
s 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 conclusionterm = term
with the two terms being elements of an inductive set. To build the proof, the tactic traverses the normal forms 1 of the terms looking for a couple of subtermsu
andw
(u
subterm of the normal form ofterm
andw
subterm of the normal form ofterm
), 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.
Note
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
No primitive equality found.
¶

Error
Not a discriminable equality.
¶

Variant
discriminate natural
This does the same thing as
intros until natural
followed bydiscriminate ident
whereident
is the identifier for the last introduced hypothesis.

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

Variant
ediscriminate natural
¶ 
Variant
ediscriminate term with bindings?
¶ This works the same as
discriminate
but if the type ofterm
, or the type of the hypothesis referred to bynatural
, has uninstantiated parameters, these parameters are left as existential variables.

Variant
discriminate
This behaves like
discriminate ident
if ident is the name of an hypothesis to whichdiscriminate
is applicable; if the current goal is of the formterm <> term
, this behaves asintro ident; discriminate ident
.
Error
No discriminable equalities.
¶

Error

Tactic
injection term
¶ The injection tactic exploits the property that constructors of inductive types are injective, i.e. that if
c
is a constructor of an inductive type andc t
_{1} andc t
_{2} are equal thent
_{1} andt
_{2} are equal too.If
term
is a proof of a statement of conclusionterm = term
, theninjection
applies the injectivity of constructors as deep as possible to derive the equality of all the subterms ofterm
andterm
at positions where the terms start to differ. For example, from(S p, S n) = (q, S (S m))
we may deriveS p = q
andn = S m
. For this tactic to work, the terms should be typed with an inductive type and they should be neither convertible, nor having a different head constructor. If these conditions are satisfied, the tactic derives the equality of all the subterms at positions where they differ and adds them as antecedents to the conclusion of the current goal.Example
Consider the following goal:
 Inductive list : Set :=  nil : list  cons : nat > list > list.
 list is defined list_rect is defined list_ind is defined list_rec is defined list_sind is defined
 Parameter P : list > Prop.
 P is declared
 Goal forall l n, P nil > cons n l = cons 0 nil > P l.
 1 goal ============================ forall (l : list) (n : nat), P nil > cons n l = cons 0 nil > P l
 intros.
 1 goal l : list n : nat H : P nil H0 : cons n l = cons 0 nil ============================ P l
 injection H0.
 1 goal l : list n : nat H : P nil H0 : cons n l = cons 0 nil ============================ l = nil > n = 0 > P l
Beware that injection yields an equality in a sigma type whenever the injected object has a dependent type
P
with its two instances in different types(P t
_{1}... t
_{n})
and(P u
_{1}... u
_{n} _{)}. Ift
_{1} andu
_{1} are the same and have for type an inductive type for which a decidable equality has been declared usingScheme
Equality ...
(see Generation of induction principles with Scheme), the use of a sigma type is avoided.Note
If some quantified hypothesis of the goal is named
ident
, theninjection ident
first introduces the hypothesis in the local context usingintros until ident
.
Error
Nothing to do, it is an equality between convertible terms.
¶

Error
Not a primitive equality.
¶

Error
Nothing to inject.
¶ This error is given when one side of the equality is not a constructor.

Variant
injection natural
This does the same thing as
intros until natural
followed byinjection ident
whereident
is the identifier for the last introduced hypothesis.

Variant
injection term with bindings
This does the same as
injection term
but using the given bindings to instantiate parameters or hypotheses ofterm
.

Variant
einjection natural
¶ 
Variant
einjection term with bindings?
¶ This works the same as
injection
but if the type ofterm
, or the type of the hypothesis referred to bynatural
, has uninstantiated parameters, these parameters are left as existential variables.

Variant
injection
If the current goal is of the form
term <> term
, this behaves asintro ident; injection ident
.
Error
goal does not satisfy the expected preconditions.
¶

Error

Variant
injection term with bindings? as simple_intropattern+

Variant
injection natural as simple_intropattern+

Variant
injection as simple_intropattern+

Variant
einjection term with bindings? as simple_intropattern+

Variant
einjection natural as simple_intropattern+

Variant
einjection as simple_intropattern+
These variants apply
intros simple_intropattern+
after the call toinjection
oreinjection
so that all equalities generated are moved in the context of hypotheses. The number ofsimple_intropattern
must not exceed the number of equalities newly generated. If it is smaller, fresh names are automatically generated to adjust the list ofsimple_intropattern
to the number of new equalities. The original equality is erased if it corresponds to a hypothesis.

Variant
injection term with bindings? as injection_intropattern

Variant
injection natural as injection_intropattern

Variant
injection as injection_intropattern

Variant
einjection term with bindings? as injection_intropattern

Variant
einjection natural as injection_intropattern

Variant
einjection as injection_intropattern
These are equivalent to the previous variants but using instead the syntax
injection_intropattern
whichintros
uses. In particularas [= simple_intropattern+]
behaves the same asas simple_intropattern+
.

Tactic
inversion ident
¶ Let the type of
ident
in the local context be(I t)
, whereI
is a (co)inductive predicate. Then,inversion
applied toident
derives for each possible constructorc i
of(I t)
, all the necessary conditions that should hold for the instance(I t)
to be proved byc i
.
Note
If ident
does not denote a hypothesis in the local context but
refers to a hypothesis quantified in the goal, then the latter is
first introduced in the local context using intros until ident
.
Note
As inversion
proofs may be large in size, we recommend the
user to stock the lemmas whenever the same instance needs to be
inverted several times. See Generation of inversion principles with Derive Inversion.
Note
Part of the behavior of the inversion
tactic is to generate
equalities between expressions that appeared in the hypothesis that is
being processed. By default, no equalities are generated if they
relate two proofs (i.e. equalities between term
s whose type is in sort
Prop
). This behavior can be turned off by using the
Keep Proof Equalities
setting.

Variant
inversion natural
This does the same thing as
intros until natural
theninversion ident
whereident
is the identifier for the last introduced hypothesis.

Variant
inversion ident as or_and_intropattern_loc
This generally behaves as inversion but using names in
or_and_intropattern_loc
for naming hypotheses. Theor_and_intropattern_loc
must have the form[p
_{11}... p
_{1n} ...  p
_{m1}... p
_{mn}]
withm
being the number of constructors of the type ofident
. Be careful that the list must be of lengthm
even ifinversion
discards some cases (which is precisely one of its roles): for the discarded cases, just use an empty list (i.e.n = 0
).The arguments of the ith constructor and the equalities thatinversion
introduces in the context of the goal corresponding to the ith constructor, if it exists, get their names from the listp
_{i1}... p
_{in} in order. If there are not enough names,inversion
invents names for the remaining variables to introduce. In case an equation splits into several equations (becauseinversion
appliesinjection
on the equalities it generates), the corresponding namep
_{ij} in the list must be replaced by a sublist of the form[p
_{ij1}... p
_{ijq}]
(or, equivalently,(p
_{ij1}, ..., p
_{ijq})
) whereq
is the number of subequalities obtained from splitting the original equation. Here is an example. Theinversion ... as
variant ofinversion
generally behaves in a slightly more expectable way thaninversion
(no artificial duplication of some hypotheses referring to other hypotheses). To take benefit of these improvements, it is enough to useinversion ... as []
, letting the names being finally chosen by Coq.Example
 Inductive contains0 : list nat > Prop :=  in_hd : forall l, contains0 (0 :: l)  in_tl : forall l b, contains0 l > contains0 (b :: l).
 contains0 is defined contains0_ind is defined contains0_sind is defined
 Goal forall l:list nat, contains0 (1 :: l) > contains0 l.
 1 goal ============================ forall l : list nat, contains0 (1 :: l) > contains0 l
 intros l H; inversion H as [  l' p Hl' [Heqp Heql'] ].
 1 goal l : list nat H : contains0 (1 :: l) l' : list nat p : nat Hl' : contains0 l Heqp : p = 1 Heql' : l' = l ============================ contains0 l

Variant
inversion natural as or_and_intropattern_loc
This allows naming the hypotheses introduced by
inversion natural
in the context.

Variant
inversion_clear ident as or_and_intropattern_loc
This allows naming the hypotheses introduced by
inversion_clear
in the context. Notice that hypothesis names can be provided as ifinversion
were called, even though theinversion_clear
will eventually erase the hypotheses.

Variant
inversion ident in ident+
Let
ident+
be identifiers in the local context. This tactic behaves as generalizingident+
, and then performinginversion
.

Variant
inversion ident as or_and_intropattern_loc in ident+
This allows naming the hypotheses introduced in the context by
inversion ident in ident+
.

Variant
inversion_clear ident in ident+
Let
ident+
be identifiers in the local context. This tactic behaves as generalizingident+
, and then performinginversion_clear
.

Variant
inversion_clear ident as or_and_intropattern_loc in ident+
This allows naming the hypotheses introduced in the context by
inversion_clear ident in ident+
.

Variant
dependent inversion ident
¶ That must be used when
ident
appears in the current goal. It acts likeinversion
and then substitutesident
for the corresponding@term
in the goal.

Variant
dependent inversion ident as or_and_intropattern_loc
This allows naming the hypotheses introduced in the context by
dependent inversion ident
.

Variant
dependent inversion_clear ident
Like
dependent inversion
, except thatident
is cleared from the local context.

Variant
dependent inversion_clear ident as or_and_intropattern_loc
This allows naming the hypotheses introduced in the context by
dependent inversion_clear ident
.

Variant
dependent inversion ident with term
¶ This variant allows you to specify the generalization of the goal. It is useful when the system fails to generalize the goal automatically. If
ident
has type(I t)
andI
has typeforall (x:T), s
, thenterm
must be of typeI:forall (x:T), I x > s'
wheres'
is the type of the goal.

Variant
dependent inversion ident as or_and_intropattern_loc with term
This allows naming the hypotheses introduced in the context by
dependent inversion ident with term
.

Variant
dependent inversion_clear ident with term
Like
dependent inversion … with …
with but clearsident
from the local context.

Variant
dependent inversion_clear ident as or_and_intropattern_loc with term
This allows naming the hypotheses introduced in the context by
dependent inversion_clear ident with term
.

Variant
simple inversion ident
¶ It is a very primitive inversion tactic that derives all the necessary equalities but it does not simplify the constraints as
inversion
does.

Variant
simple inversion ident as or_and_intropattern_loc
This allows naming the hypotheses introduced in the context by
simple inversion
.

Tactic
inversion ident using ident
¶ Let
ident
have type(I t)
(I
an inductive predicate) in the local context, andident
be a (dependent) inversion lemma. Then, this tactic refines the current goal with the specified lemma.

Variant
inversion ident using ident in ident+
This tactic behaves as generalizing
ident+
, then doinginversion ident using ident
.

Variant
inversion_sigma ident as simple_intropattern??
¶ This tactic turns equalities of dependent pairs (e.g.,
existT P x p = existT P y q
, frequently left over by inversion on a dependent type family) into pairs of equalities (e.g., a hypothesisH : x = y
and a hypothesis of typerew H in p = q
); these hypotheses can subsequently be simplified usingsubst
, without ever invoking any kind of axiom asserting uniqueness of identity proofs. If you want to explicitly specify the hypothesis to be inverted, you can pass it as an argument toinversion_sigma
. This tactic also works forsig
,sigT2
,sig2
,ex
, andex2
and there are similareq_sig
***_rect
induction lemmas.
Error
Type of ident is not an equality of recognized Σ types: expected one of sig sig2 sigT sigT2 sigT2 ex or ex2 but got term
¶ When applied to a hypothesis,
inversion_sigma
can only handle equalities of the listed sigma types.

Error
ident is not an equality of Σ types
¶ When applied to a hypothesis,
inversion_sigma
can only be called on hypotheses that are equalities usingCoq.Logic.Init.eq
.

Error
Example
Nondependent inversion.
Let us consider the relation Le
over natural numbers:
 Inductive Le : nat > nat > Set :=  LeO : forall n:nat, Le 0 n  LeS : forall n m:nat, Le n m > Le (S n) (S m).
 Le is defined Le_rect is defined Le_ind is defined Le_rec is defined Le_sind is defined
Let us consider the following goal:
 Section Section.
 Variable P : nat > nat > Prop.
 P is declared
 Variable Q : forall n m:nat, Le n m > Prop.
 Q is declared
 Goal forall n m, Le (S n) m > P n m.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop ============================ forall n m : nat, Le (S n) m > P n m
 intros.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m : nat H : Le (S n) m ============================ P n m
To prove the goal, we may need to reason by cases on H
and to derive
that m
is necessarily of the form (S m0)
for certain m0
and that
(Le n m0)
. Deriving these conditions corresponds to proving that the only
possible constructor of (Le (S n) m)
is LeS
and that we can invert
the arrow in the type of LeS
. This inversion is possible because Le
is the smallest set closed by the constructors LeO
and LeS
.
 inversion_clear H.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m, m0 : nat H0 : Le n m0 ============================ P n (S m0)
Note that m
has been substituted in the goal for (S m0)
and that the
hypothesis (Le n m0)
has been added to the context.
Sometimes it is interesting to have the equality m = (S m0)
in the
context to use it after. In that case we can use inversion
that does
not clear the equalities:
 intros.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m : nat H : Le (S n) m ============================ P n m
 inversion H.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m : nat H : Le (S n) m n0, m0 : nat H1 : Le n m0 H0 : n0 = n H2 : S m0 = m ============================ P n (S m0)
Example
Dependent inversion.
Let us consider the following goal:
 Abort.
 Goal forall n m (H:Le (S n) m), Q (S n) m H.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop ============================ forall (n m : nat) (H : Le (S n) m), Q (S n) m H
 intros.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m : nat H : Le (S n) m ============================ Q (S n) m H
As H
occurs in the goal, we may want to reason by cases on its
structure and so, we would like inversion tactics to substitute H
by
the corresponding @term in constructor form. Neither inversion
nor
inversion_clear
do such a substitution. To have such a behavior we
use the dependent inversion tactics:
 dependent inversion_clear H.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m, m0 : nat l : Le n m0 ============================ Q (S n) (S m0) (LeS n m0 l)
Note that H
has been substituted by (LeS n m0 l)
and m
by (S m0)
.
Example
Using inversion_sigma.
Let us consider the following inductive type of lengthindexed lists, and a lemma about inverting equality of cons:
 Require Import Coq.Logic.Eqdep_dec.
 Inductive vec A : nat > Type :=  nil : vec A O  cons {n} (x : A) (xs : vec A n) : vec A (S n).
 vec is defined vec_rect is defined vec_ind is defined vec_rec is defined vec_sind is defined
 Lemma invert_cons : forall A n x xs y ys, @cons A n x xs = @cons A n y ys > xs = ys.
 1 goal ============================ forall (A : Type) (n : nat) (x : A) (xs : vec A n) (y : A) (ys : vec A n), cons A x xs = cons A y ys > xs = ys
 Proof.
 intros A n x xs y ys H.
 1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys ============================ xs = ys
After performing inversion, we are left with an equality of existTs:
 inversion H.
 1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H2 : existT (fun n : nat => vec A n) n xs = existT (fun n : nat => vec A n) n ys ============================ xs = ys
We can turn this equality into a usable form with inversion_sigma:
 inversion_sigma.
 1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H2_ : n = n H2_0 : eq_rect n (fun n : nat => vec A n) xs n H2_ = ys ============================ xs = ys
To finish cleaning up the proof, we will need to use the fact that that all proofs of n = n for n a nat are eq_refl:
 let H := match goal with H : n = n  _ => H end in pose proof (Eqdep_dec.UIP_refl_nat _ H); subst H.
 1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H2_0 : eq_rect n (fun n : nat => vec A n) xs n eq_refl = ys ============================ xs = ys
 simpl in *.
 1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H2_0 : xs = ys ============================ xs = ys
Finally, we can finish the proof:
 assumption.
 No more goals.
 Qed.
See also

Tactic
fix ident natural
¶ This tactic is a primitive tactic to start a proof by induction. In general, it is easier to rely on higherlevel induction tactics such as the ones described in
induction
.In the syntax of the tactic, the identifier
ident
is the name given to the induction hypothesis. The natural numbernatural
tells on which premise of the current goal the induction acts, starting from 1, counting both dependent and non dependent products, but skipping local definitions. Especially, the current lemma must be composed of at leastnatural
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 global 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 Requesting information).

Variant
fix ident natural with (ident binder+ [{struct ident}] : type)+
This starts a proof by mutual induction. The statements to be simultaneously proved are respectively
forall binder ... binder, type
. The identifiersident
are the names of the induction hypotheses. The identifiersident
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).

Tactic
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 global environment. To know if the use of coinduction hypotheses is correct at some time of the interactive development of a proof, use the commandGuarded
(see Section Requesting information).
Equality and inductive sets¶
We describe in this section some special purpose tactics dealing with
equality and inductive sets or types. These tactics use the
equality eq:forall (A:Type), A>A>Prop
, simply written with the infix
symbol =
.

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

Tactic
compare term term
¶ This tactic compares two given objects
term
andterm
of an inductive datatype. IfG
is the current goal, it leaves the sub goalsterm =term > G
and~ term = term > G
. The type ofterm
andterm
must satisfy the same restrictions as in the tacticdecide equality
.

Tactic
simplify_eq term
¶ Let
term
be the proof of a statement of conclusionterm = term
. Ifterm
andterm
are structurally different (in the sense described for the tacticdiscriminate
), then the tacticsimplify_eq
behaves asdiscriminate term
, otherwise it behaves asinjection term
.
Note
If some quantified hypothesis of the goal is named ident
,
then simplify_eq ident
first introduces the hypothesis in the local
context using intros until ident
.

Variant
simplify_eq natural
This does the same thing as
intros until natural
thensimplify_eq ident
whereident
is the identifier for the last introduced hypothesis.

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

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

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

Tactic
dependent rewrite > ident
¶ This tactic applies to any goal. If
ident
has type(existT B a b)=(existT B a' b')
in the local context (i.e. eachterm
of the equality has a sigma type{ a:A & (B a)}
) this tactic rewritesa
intoa'
andb
intob'
in the current goal. This tactic works even ifB
is also a sigma type. This kind of equalities between dependent pairs may be derived by theinjection
andinversion
tactics.

Variant
dependent rewrite < ident
¶ Analogous to
dependent rewrite >
but uses the equality from right to left.
Generation of induction principles with Scheme
¶

Command
Scheme ident :=? scheme_kind with ident :=? scheme_kind*
¶  scheme_kind
::=
Equality for reference
InductionMinimalityEliminationCase for reference Sort sort_familysort_family
::=
Set
Prop
SProp
TypeA highlevel tool for automatically generating (possibly mutual) induction principles for given types and sorts. Each
reference
is a different inductive type identifier belonging to the same package of mutual inductive definitions. The command generates theident
s as mutually recursive definitions. Each termident
proves a general principle of mutual induction for objects in typereference
.ident
The name of the scheme. If not provided, the scheme name will be determined automatically from the sorts involved.
Minimality for reference Sort sort_family
Defines a nondependent elimination principle more natural for inductively defined relations.
Equality for reference
Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If
reference
involves other inductive types, their equality has to be defined first.
Example
Induction scheme for tree and forest.
A mutual induction principle for tree and forest in sort
Set
can be defined using the command
 Axiom A : Set.
 A is declared
 Axiom B : Set.
 B is declared
 Inductive tree : Set := node : A > forest > tree with forest : Set := leaf : B > forest  cons : tree > forest > forest.
 tree, forest are defined tree_rect is defined tree_ind is defined tree_rec is defined tree_sind is defined forest_rect is defined forest_ind is defined forest_rec is defined forest_sind is defined
 Scheme tree_forest_rec := Induction for tree Sort Set with forest_tree_rec := Induction for forest Sort Set.
 forest_tree_rec is defined tree_forest_rec is defined tree_forest_rec, forest_tree_rec are recursively defined
You may now look at the type of tree_forest_rec:
 Check tree_forest_rec.
 tree_forest_rec : forall (P : tree > Set) (P0 : forest > Set), (forall (a : A) (f : forest), P0 f > P (node a f)) > (forall b : B, P0 (leaf b)) > (forall t : tree, P t > forall f1 : forest, P0 f1 > P0 (cons t f1)) > forall t : tree, P t
This principle involves two different predicates for trees andforests; it also has three premises each one corresponding to a constructor of one of the inductive definitions.
The principle forest_tree_rec
shares exactly the same premises, only
the conclusion now refers to the property of forests.
Example
Predicates odd and even on naturals.
Let odd and even be inductively defined as:
 Inductive odd : nat > Prop := oddS : forall n:nat, even n > odd (S n) with even : nat > Prop :=  evenO : even 0  evenS : forall n:nat, odd n > even (S n).
 odd, even are defined odd_ind is defined odd_sind is defined even_ind is defined even_sind is defined
The following command generates a powerful elimination principle:
 Scheme odd_even := Minimality for odd Sort Prop with even_odd := Minimality for even Sort Prop.
 even_odd is defined odd_even is defined odd_even, even_odd are recursively defined
The type of odd_even for instance will be:
 Check odd_even.
 odd_even : forall P P0 : nat > Prop, (forall n : nat, even n > P0 n > P (S n)) > P0 0 > (forall n : nat, odd n > P n > P0 (S n)) > forall n : nat, odd n > P n
The type of even_odd
shares the same premises but the conclusion is
(n:nat)(even n)>(P0 n)
.
Automatic declaration of schemes¶

Flag
Elimination Schemes
¶ This flag enables automatic declaration of induction principles when defining a new inductive type. Defaults to on.

Flag
Nonrecursive Elimination Schemes
¶ This flag enables automatic declaration of induction principles for types declared with the
Variant
andRecord
commands. Defaults to off.

Flag
Case Analysis Schemes
¶ This flag governs the generation of case analysis lemmas for inductive types, i.e. corresponding to the pattern matching term alone and without fixpoint.

Flag
Boolean Equality Schemes
¶ 
Flag
Decidable Equality Schemes
¶ These flags control the automatic declaration of those Boolean equalities (see the second variant of
Scheme
).
Warning
You have to be careful with these flags since Coq may now reject welldefined inductive types because it cannot compute a Boolean equality for them.
Combined Scheme¶

Command
Combined Scheme ident_{def} from ident+,
¶ This command is a tool for combining induction principles generated by the
Scheme
command. Eachident
is a different inductive principle that must belong to the same package of mutual inductive principle definitions. This command generatesident_{def}
as the conjunction of the principles: it is built from the common premises of the principles and concluded by the conjunction of their conclusions. In the case where all the inductive principles used are in sortProp
, the propositional conjunctionand
is used, otherwise the simple productprod
is used instead.
Example
We can define the induction principles for trees and forests using:
 Scheme tree_forest_ind := Induction for tree Sort Prop with forest_tree_ind := Induction for forest Sort Prop.
 forest_tree_ind is defined tree_forest_ind is defined tree_forest_ind, forest_tree_ind are recursively defined
Then we can build the combined induction principle which gives the conjunction of the conclusions of each individual principle:
 Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind.
 tree_forest_mutind is defined tree_forest_mutind is recursively defined
The type of tree_forest_mutind will be:
 Check tree_forest_mutind.
 tree_forest_mutind : forall (P : tree > Prop) (P0 : forest > Prop), (forall (a : A) (f : forest), P0 f > P (node a f)) > (forall b : B, P0 (leaf b)) > (forall t : tree, P t > forall f1 : forest, P0 f1 > P0 (cons t f1)) > (forall t : tree, P t) /\ (forall f2 : forest, P0 f2)
Example
We can also combine schemes at sort
Type
:
 Scheme tree_forest_rect := Induction for tree Sort Type with forest_tree_rect := Induction for forest Sort Type.
 forest_tree_rect is defined tree_forest_rect is defined tree_forest_rect, forest_tree_rect are recursively defined
 Combined Scheme tree_forest_mutrect from tree_forest_rect, forest_tree_rect.
 tree_forest_mutrect is defined tree_forest_mutrect is recursively defined
 Check tree_forest_mutrect.
 tree_forest_mutrect : forall (P : tree > Type) (P0 : forest > Type), (forall (a : A) (f : forest), P0 f > P (node a f)) > (forall b : B, P0 (leaf b)) > (forall t : tree, P t > forall f1 : forest, P0 f1 > P0 (cons t f1)) > (forall t : tree, P t) * (forall f2 : forest, P0 f2)
Generation of inversion principles with Derive
Inversion
¶

Command
Derive Inversion ident with one_term Sort sort_family?
¶ Generates an inversion lemma for the
inversion ... using ...
tactic.ident
is the name of the generated lemma.one_term
should be in the formqualid
or(forall binder+, qualid term)
wherequalid
is the name of an inductive predicate andbinder+
binds the variables occurring in the termterm
. The lemma is generated for the sortsort_family
corresponding toone_term
. Applying the lemma is equivalent to inverting the instance with theinversion
tactic.

Command
Derive Inversion_clear ident with one_term Sort sort_family?
¶ When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic
inversion_clear
.

Command
Derive Dependent Inversion ident with one_term Sort sort_family
¶ When applied, it is equivalent to having inverted the instance with the tactic
dependent inversion
.

Command
Derive Dependent Inversion_clear ident with one_term Sort sort_family
¶ When applied, it is equivalent to having inverted the instance with the tactic
dependent inversion_clear
.
Example
Consider the relation Le
over natural numbers and the following
parameter P
:
 Inductive Le : nat > nat > Set :=  LeO : forall n:nat, Le 0 n  LeS : forall n m:nat, Le n m > Le (S n) (S m).
 Le is defined Le_rect is defined Le_ind is defined Le_rec is defined Le_sind is defined
 Parameter P : nat > nat > Prop.
 P is declared
To generate the inversion lemma for the instance (Le (S n) m)
and the
sort Prop
, we do:
 Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop.
 leminv is defined
 Check leminv.
 leminv : forall (n m : nat) (P : nat > nat > Prop), (forall m0 : nat, Le n m0 > P n (S m0)) > Le (S n) m > P n m
Then we can use the proven inversion lemma:
 Goal forall (n m : nat) (H : Le (S n) m), P n m.
 1 goal ============================ forall n m : nat, Le (S n) m > P n m
 intros.
 1 goal n, m : nat H : Le (S n) m ============================ P n m
 Show.
 1 goal n, m : nat H : Le (S n) m ============================ P n m
 inversion H using leminv.
 1 goal n, m : nat H : Le (S n) m ============================ forall m0 : nat, Le n m0 > P n (S m0)
Examples of dependent destruction / dependent induction¶
The tactics dependent induction
and dependent destruction
are another
solution for inverting inductive predicate instances and potentially
doing induction at the same time. It is based on the BasicElim
tactic
of Conor McBride which works by abstracting each argument of an
inductive instance by a variable and constraining it by equalities
afterwards. This way, the usual induction and destruct tactics can be
applied to the abstracted instance and after simplification of the
equalities we get the expected goals.
The abstracting tactic is called generalize_eqs and it takes as argument a hypothesis to generalize. It uses the JMeq datatype defined in Coq.Logic.JMeq, hence we need to require it before. For example, revisiting the first example of the inversion documentation:
 Require Import Coq.Logic.JMeq.
 Inductive Le : nat > nat > Set :=  LeO : forall n:nat, Le 0 n  LeS : forall n m:nat, Le n m > Le (S n) (S m).
 Le is defined Le_rect is defined Le_ind is defined Le_rec is defined Le_sind is defined
 Parameter P : nat > nat > Prop.
 P is declared
 Goal forall n m:nat, Le (S n) m > P n m.
 1 goal ============================ forall n m : nat, Le (S n) m > P n m
 intros n m H.
 1 goal n, m : nat H : Le (S n) m ============================ P n m
 generalize_eqs H.
 1 goal n, m, gen_x : nat H : Le gen_x m ============================ gen_x = S n > P n m
The index S n
gets abstracted by a variable here, but a corresponding
equality is added under the abstract instance so that no information
is actually lost. The goal is now almost amenable to do induction or
case analysis. One should indeed first move n
into the goal to
strengthen it before doing induction, or n
will be fixed in the
inductive hypotheses (this does not matter for case analysis). As a
rule of thumb, all the variables that appear inside constructors in
the indices of the hypothesis should be generalized. This is exactly
what the generalize_eqs_vars
variant does:
 generalize_eqs_vars H.
 induction H.
 2 goals n, n0 : nat ============================ 0 = S n > P n n0 goal 2 is: S n0 = S n > P n (S m)
As the hypothesis itself did not appear in the goal, we did not need to use an heterogeneous equality to relate the new hypothesis to the old one (which just disappeared here). However, the tactic works just as well in this case, e.g.:
 Require Import Coq.Program.Equality.
 Parameter Q : forall (n m : nat), Le n m > Prop.
 Q is declared
 Goal forall n m (p : Le (S n) m), Q (S n) m p.
 1 goal ============================ forall (n m : nat) (p : Le (S n) m), Q (S n) m p
 intros n m p.
 1 goal n, m : nat p : Le (S n) m ============================ Q (S n) m p
 generalize_eqs_vars p.
 1 goal m, gen_x : nat p : Le gen_x m ============================ forall (n : nat) (p0 : Le (S n) m), gen_x = S n > p ~= p0 > Q (S n) m p0
One drawback of this approach is that in the branches one will have to
substitute the equalities back into the instance to get the right
assumptions. Sometimes injection of constructors will also be needed
to recover the needed equalities. Also, some subgoals should be
directly solved because of inconsistent contexts arising from the
constraints on indexes. The nice thing is that we can make a tactic
based on discriminate, injection and variants of substitution to
automatically do such simplifications (which may involve the axiom K).
This is what the simplify_dep_elim
tactic from Coq.Program.Equality
does. For example, we might simplify the previous goals considerably:
 induction p ; simplify_dep_elim.
 1 goal n, m : nat p : Le n m IHp : forall (n0 : nat) (p0 : Le (S n0) m), n = S n0 > p ~= p0 > Q (S n0) m p0 ============================ Q (S n) (S m) (LeS n m p)
The higherorder tactic do_depind
defined in Coq.Program.Equality
takes a tactic and combines the building blocks we have seen with it:
generalizing by equalities calling the given tactic with the
generalized induction hypothesis as argument and cleaning the subgoals
with respect to equalities. Its most important instantiations
are dependent induction
and dependent destruction
that do induction or
simply case analysis on the generalized hypothesis. For example we can
redo what we’ve done manually with dependent destruction:
 Lemma ex : forall n m:nat, Le (S n) m > P n m.
 1 goal ============================ forall n m : nat, Le (S n) m > P n m
 intros n m H.
 1 goal n, m : nat H : Le (S n) m ============================ P n m
 dependent destruction H.
 1 goal n, m : nat H : Le n m ============================ P n (S m)
This gives essentially the same result as inversion. Now if the destructed hypothesis actually appeared in the goal, the tactic would still be able to invert it, contrary to dependent inversion. Consider the following example on vectors:
 Set Implicit Arguments.
 Parameter A : Set.
 A is declared
 Inductive vector : nat > Type :=  vnil : vector 0  vcons : A > forall n, vector n > vector (S n).
 vector is defined vector_rect is defined vector_ind is defined vector_rec is defined vector_sind is defined
 Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a v'.
 1 goal ============================ forall (n : nat) (v : vector (S n)), exists (v' : vector n) (a : A), v = vcons a v'
 intros n v.
 1 goal n : nat v : vector (S n) ============================ exists (v' : vector n) (a : A), v = vcons a v'
 dependent destruction v.
 1 goal n : nat a : A v : vector n ============================ exists (v' : vector n) (a0 : A), vcons a v = vcons a0 v'
In this case, the v
variable can be replaced in the goal by the
generalized hypothesis only when it has a type of the form vector (S n)
,
that is only in the second case of the destruct. The first one is
dismissed because S n <> 0
.
A larger example¶
Let’s see how the technique works with induction on inductive predicates on a real example. We will develop an example application to the theory of simplytyped lambdacalculus formalized in a dependentlytyped style:
 Inductive type : Type :=  base : type  arrow : type > type > type.
 type is defined type_rect is defined type_ind is defined type_rec is defined type_sind is defined
 Notation " t > t' " := (arrow t t') (at level 20, t' at next level).
 Inductive ctx : Type :=  empty : ctx  snoc : ctx > type > ctx.
 ctx is defined ctx_rect is defined ctx_ind is defined ctx_rec is defined ctx_sind is defined
 Notation " G , tau " := (snoc G tau) (at level 20, tau at next level).
 Fixpoint conc (G D : ctx) : ctx := match D with  empty => G  snoc D' x => snoc (conc G D') x end.
 conc is defined conc is recursively defined (guarded on 2nd argument)
 Notation " G ; D " := (conc G D) (at level 20).
 Inductive term : ctx > type > Type :=  ax : forall G tau, term (G, tau) tau  weak : forall G tau, term G tau > forall tau', term (G, tau') tau  abs : forall G tau tau', term (G , tau) tau' > term G (tau > tau')  app : forall G tau tau', term G (tau > tau') > term G tau > term G tau'.
 term is defined term_rect is defined term_ind is defined term_rec is defined term_sind is defined
We have defined types and contexts which are snoclists of types. We
also have a conc
operation that concatenates two contexts. The term
datatype represents in fact the possible typing derivations of the
calculus, which are isomorphic to the welltyped terms, hence the
name. A term is either an application of:
the axiom rule to type a reference to the first variable in a context
the weakening rule to type an object in a larger context
the abstraction or lambda rule to type a function
the application to type an application of a function to an argument
Once we have this datatype we want to do proofs on it, like weakening:
 Lemma weakening : forall G D tau, term (G ; D) tau > forall tau', term (G , tau' ; D) tau.
 1 goal ============================ forall (G D : ctx) (tau : type), term (G; D) tau > forall tau' : type, term ((G, tau'); D) tau
The problem here is that we can’t just use induction on the typing
derivation because it will forget about the G ; D
constraint appearing
in the instance. A solution would be to rewrite the goal as:
 Lemma weakening' : forall G' tau, term G' tau > forall G D, (G ; D) = G' > forall tau', term (G, tau' ; D) tau.
 1 goal ============================ forall (G' : ctx) (tau : type), term G' tau > forall G D : ctx, G; D = G' > forall tau' : type, term ((G, tau'); D) tau
With this proper separation of the index from the instance and the
right induction loading (putting G
and D
after the inductedon
hypothesis), the proof will go through, but it is a very tedious
process. One is also forced to make a wrapper lemma to get back the
more natural statement. The dependent induction
tactic alleviates this
trouble by doing all of this plumbing of generalizing and substituting
back automatically. Indeed we can simply write:
 Require Import Coq.Program.Tactics.
 Require Import Coq.Program.Equality.
 Lemma weakening : forall G D tau, term (G ; D) tau > forall tau', term (G , tau' ; D) tau.
 1 goal ============================ forall (G D : ctx) (tau : type), term (G; D) tau > forall tau' : type, term ((G, tau'); D) tau
 Proof with simpl in * ; simpl_depind ; auto.
 intros G D tau H. dependent induction H generalizing G D ; intros.
 1 goal G, D : ctx tau : type H : term (G; D) tau ============================ forall tau' : type, term ((G, tau'); D) tau 4 goals G0 : ctx tau : type G, D : ctx x : G0, tau = G; D tau' : type ============================ term ((G, tau'); D) tau goal 2 is: term ((G, tau'0); D) tau goal 3 is: term ((G, tau'0); D) (tau > tau') goal 4 is: term ((G, tau'0); D) tau'
This call to dependent induction has an additional arguments which is a list of variables appearing in the instance that should be generalized in the goal, so that they can vary in the induction hypotheses. By default, all variables appearing inside constructors (except in a parameter position) of the instantiated hypothesis will be generalized automatically but one can always give the list explicitly.
 Show.
 4 goals G0 : ctx tau : type G, D : ctx x : G0, tau = G; D tau' : type ============================ term ((G, tau'); D) tau goal 2 is: term ((G, tau'0); D) tau goal 3 is: term ((G, tau'0); D) (tau > tau') goal 4 is: term ((G, tau'0); D) tau'
The simpl_depind
tactic includes an automatic tactic that tries to
simplify equalities appearing at the beginning of induction
hypotheses, generally using trivial applications of reflexivity
. In
cases where the equality is not between constructor forms though, one
must help the automation by giving some arguments, using the
specialize
tactic for example.
 destruct D... apply weak; apply ax. apply ax.
 5 goals G0 : ctx tau, tau' : type ============================ term ((G0, tau), tau') tau goal 2 is: term (((G, tau'); D), t) t goal 3 is: term ((G, tau'0); D) tau goal 4 is: term ((G, tau'0); D) (tau > tau') goal 5 is: term ((G, tau'0); D) tau' 4 goals G, D : ctx t, tau' : type ============================ term (((G, tau'); D), t) t goal 2 is: term ((G, tau'0); D) tau goal 3 is: term ((G, tau'0); D) (tau > tau') goal 4 is: term ((G, tau'0); D) tau' 3 goals G0 : ctx tau : type H : term G0 tau tau' : type IHterm : forall G D : ctx, G0 = G; D > forall tau' : type, term ((G, tau'); D) tau G, D : ctx x : G0, tau' = G; D tau'0 : type ============================ term ((G, tau'0); D) tau goal 2 is: term ((G, tau'0); D) (tau > tau') goal 3 is: term ((G, tau'0); D) tau'
 destruct D...
 4 goals G0 : ctx tau : type H : term G0 tau tau' : type IHterm : forall G D : ctx, G0 = G; D > forall tau' : type, term ((G, tau'); D) tau tau'0 : type ============================ term ((G0, tau'), tau'0) tau goal 2 is: term (((G, tau'0); D), t) tau goal 3 is: term ((G, tau'0); D) (tau > tau') goal 4 is: term ((G, tau'0); D) tau'
 Show.
 4 goals G0 : ctx tau : type H : term G0 tau tau' : type IHterm : forall G D : ctx, G0 = G; D > forall tau' : type, term ((G, tau'); D) tau tau'0 : type ============================ term ((G0, tau'), tau'0) tau goal 2 is: term (((G, tau'0); D), t) tau goal 3 is: term ((G, tau'0); D) (tau > tau') goal 4 is: term ((G, tau'0); D) tau'
 specialize (IHterm G0 empty eq_refl).
 4 goals G0 : ctx tau : type H : term G0 tau tau' : type IHterm : forall tau' : type, term ((G0, tau'); empty) tau tau'0 : type ============================ term ((G0, tau'), tau'0) tau goal 2 is: term (((G, tau'0); D), t) tau goal 3 is: term ((G, tau'0); D) (tau > tau') goal 4 is: term ((G, tau'0); D) tau'
Once the induction hypothesis has been narrowed to the right equality, it can be used directly.
 apply weak, IHterm.
 3 goals tau : type G, D : ctx IHterm : forall G0 D0 : ctx, G; D = G0; D0 > forall tau' : type, term ((G0, tau'); D0) tau H : term (G; D) tau t, tau'0 : type ============================ term (((G, tau'0); D), t) tau goal 2 is: term ((G, tau'0); D) (tau > tau') goal 3 is: term ((G, tau'0); D) tau'
Now concluding this subgoal is easy.
 constructor; apply IHterm; reflexivity.
 2 goals G, D : ctx tau, tau' : type H : term ((G; D), tau) tau' IHterm : forall G0 D0 : ctx, (G; D), tau = G0; D0 > forall tau'0 : type, term ((G0, tau'0); D0) tau' tau'0 : type ============================ term ((G, tau'0); D) (tau > tau') goal 2 is: term ((G, tau'0); D) tau'
 1
Reminder: opaque constants will not be expanded by δ reductions.