Reasoning with inductive types¶
Applying constructors¶
The tactics presented here specialize apply
and
eapply
to constructors of inductive types.
- Tactic constructor nat_or_var? with bindings?¶
First does
repeat intro; hnf
on the goal. If the result is an inductive typeI
, then apply the appropriate constructor(s), and otherwise fail. Ifnat_or_var
is specified and has the valuei
, it usesapply c_{i}
, wherec_{i}
is the i-th constructor ofI
. If not specified, the tactic tries all the constructors, which can result in more than one success (e.g. for\/
) when using backtracking tactics such asconstructor; ...
. Seeltac-seq
.- Error Not an inductive product.¶
- Error Not enough constructors.¶
- Error The type has no constructors.¶
- Tactic split with bindings?¶
Equivalent to
constructor 1 with bindings?
when the conclusion is an inductive type with a single constructor. Thebindings
specify any parameters required for the constructor. It is typically used to split conjunctions in the conclusion such asA /\ B
into two new goalsA
andB
.
- Tactic exists bindings*,¶
Equivalent to
constructor 1 with bindings_{i}
for each set of bindings (or justconstructor 1
if there are nobindings
) when the conclusion is an inductive type with a single constructor. It is typically used on existential quantifications in the formexists x, P x.
- Error Not an inductive goal with 1 constructor.¶
- Tactic left with bindings?¶
- Tactic right with bindings?¶
These tactics apply only if
I
has two constructors, for instance in the case of a disjunctionA \/ B
. Then they are respectively equivalent toconstructor 1 with bindings?
andconstructor 2 with bindings?
.- Error Not an inductive goal with 2 constructors.¶
- Tactic econstructor nat_or_var with bindings??¶
- Tactic eexists bindings*,¶
- Tactic esplit with bindings?¶
- Tactic eleft with bindings?¶
- Tactic eright with bindings?¶
These tactics behave like
constructor
,exists
,split
,left
andright
, but they introduce existential variables instead of failing when a variable can't be instantiated (cf.eapply
andapply
).
Example: constructor
, left
and right
- Print or. (* or, represented by \/, has two constructors, or_introl and or_intror *)
- Inductive or (A B : Prop) : Prop := or_introl : A -> A \/ B | or_intror : B -> A \/ B. Arguments or (A B)%type_scope Arguments or_introl [A B]%type_scope _, [_] _ _ Arguments or_intror [A B]%type_scope _, _ [_] _
- Goal forall P1 P2 : Prop, P1 -> P1 \/ P2.
- 1 goal ============================ forall P1 P2 : Prop, P1 -> P1 \/ P2
- constructor 1. (* equivalent to "left" *)
- 1 goal P1, P2 : Prop H : P1 ============================ P1
- apply H. (* success *)
- No more goals.
In contrast, we won't be able to complete the proof if we select constructor 2:
- Goal forall P1 P2 : Prop, P1 -> P1 \/ P2.
- 1 goal ============================ forall P1 P2 : Prop, P1 -> P1 \/ P2
- constructor 2. (* equivalent to "right" *)
- 1 goal P1, P2 : Prop H : P1 ============================ P2
You can also apply a constructor by name:
- Goal forall P1 P2 : Prop, P1 -> P1 \/ P2.
- 1 goal ============================ forall P1 P2 : Prop, P1 -> P1 \/ P2
- intros; apply or_introl. (* equivalent to "left" *)
- 1 goal P1, P2 : Prop H : P1 ============================ P1
Case analysis¶
The tactics in this section implement case analysis on inductive or coinductive objects (see Variants and the match construct).
- Tactic destruct induction_clause+, induction_principle?¶
- induction_clause
::=
induction_arg as or_and_intropattern? eqn : naming_intropattern? occurrences?induction_arg
::=
one_term_with_bindings|
naturalPerforms case analysis by generating a subgoal for each constructor of the inductive or coinductive type selected by
induction_arg
. The selected subterm, after possibly doing anintros
, must have an inductive or coinductive type. Unlikeinduction
,destruct
generates no induction hypothesis.In each new subgoal, the tactic replaces the selected subterm with the associated constructor applied to its arguments, if any.
induction_clause+,
Giving multiple
induction_clause
s is equivalent to applyingdestruct
serially on eachinduction_clause
.induction_arg
If
one_term
(inone_term_with_bindings
) is an identifierident
:one_term
may contain holes that are denoted by “_”. In this case, the tactic selects the first subterm that matches the pattern and performs case analysis using that subterm.If
induction_arg
is anatural
, thendestruct natural
behaves likeintros until natural
followed bydestruct
applied to the last introduced hypothesis.
as or_and_intropattern
Provides names for (or applies further transformations to) the variables and hypotheses introduced in each new subgoal. The
or_and_intropattern
must have oneintropattern*
for each constructor, given in the order in which the constructors are defined. If there are not enough names, Rocq picks fresh names. Innerintropattern
s can also split introduced hypotheses into multiple hypotheses or subgoals.eqn : naming_intropattern
Generates a new hypothesis in each new subgoal that is an equality between the term being case-analyzed and the associated constructor (applied to its arguments). The name of the new item may be specified in the
naming_intropattern
.with bindings
(inone_term_with_bindings
)Provides explicit instances for the dependent premises of the type of
one_term
.occurrences
Selects specific subterms of the goal and/or hypotheses to apply the tactic to. See Occurrence clauses. If it occurs in the
induction_principle
, then there can only be oneinduction_clause
, which can't have its ownoccurrences
clause.induction_principle
Makes the tactic equivalent to
induction
induction_clause+, induction_principle
.
Example: Using
destruct
on an argument with premises- Parameter A B C D : Prop.
- A is declared B is declared C is declared D is declared
- Goal (A -> B \/ C) -> D.
- 1 goal ============================ (A -> B \/ C) -> D
- intros until 1.
- 1 goal H : A -> B \/ C ============================ D
- destruct H.
- 3 goals ============================ A goal 2 is: D goal 3 is: D
- Show 2.
- goal 2 is: H : B ============================ D
- Show 3.
- goal 3 is: H : C ============================ D
The single tactic
destruct 1
is equivalent to theintros
anddestruct
used here.- Tactic edestruct induction_clause+, induction_principle?¶
If the type of
one_term
(ininduction_arg
) has dependent premises whose values can't be inferred from thewith bindings
clause,edestruct
turns them into existential variables to be resolved later on.
- Tactic case induction_clause+, induction_principle?¶
An older, more basic tactic to perform case analysis without recursion. We recommend using
destruct
instead where possible.case
only modifies the goal; it does not modify the local context.- Tactic ecase induction_clause+, induction_principle?¶
If the type of
one_term
(ininduction_arg
) has dependent premises whose values can't be inferred from thewith bindings
clause,ecase
turns them into existential variables to be resolved later on.
- Tactic case_eq one_term¶
A variant of the
case
tactic that allows performing 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. We recommend using thedestruct
tactic with aneqn:
clause instead.
- Tactic simple destruct identnatural¶
Equivalent to
intros
until identnatural; case ident
whereident
is aforall
variable in the goal and otherwise fails.
- Tactic dependent destruction ident generalizing ident+? using one_term?¶
There is a long example of
dependent destruction
and an explanation of the underlying technique here.
- Tactic decompose [ one_term+ ] one_term¶
Recursively decomposes a complex proposition in order to obtain atomic ones.
Example
- Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.
- 1 goal ============================ forall A B C : Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C
- intros A B C H; decompose [and or] H.
- 3 goals A, B, C : Prop H : A /\ B /\ C \/ B /\ C \/ C /\ A H1 : A H0 : B H3 : C ============================ C goal 2 is: C goal 3 is: C
- all: assumption.
- No more goals.
- Qed.
Note
decompose
does not work on right-hand sides of implications or products.
Induction¶
- Tactic induction induction_clause+, induction_principle?¶
- induction_principle
::=
using one_term_with_bindings occurrences?Applies an induction principle to generate a subgoal for each constructor of an inductive type.
If the argument is dependent in the conclusion or some hypotheses of the goal, the argument is replaced by the appropriate constructor in each of the resulting subgoals and induction hypotheses are added to the local context using names whose prefix is IH. The tactic is similar to
destruct
, except thatdestruct
doesn't generate induction hypotheses.induction
anddestruct
are very similar. Aside from the following differences, please refer to the description ofdestruct
while mentally substitutinginduction
fordestruct
.induction_clause+,
If no
induction_principle
clause is provided, this is equivalent to doinginduction
on the firstinduction_clause
followed bydestruct
on any subsequent clauses.induction_principle
one_term
specifies which induction principle to use. The optionalwith bindings
gives any values that must be substituted into the induction principle. The number ofbindings
must be the same as the number of parameters of the induction principle.If unspecified, the tactic applies the appropriate induction principle that was automatically generated when the inductive type was declared based on the sort of the goal.
- Error Cannot recognize a statement based on reference.¶
The type of the
induction_arg
(in aninduction_clause
) must reduce to thereference
which was inferred as the type the induction principle operates on. Note that it is not enough to be convertible, but you can work around that withchange
:- Definition N := nat.
- N is defined
- Axiom strong : forall P, (forall n:N, (forall m:N, m < n -> P m) -> P n) -> forall n, P n.
- strong is declared
- Axiom P : N -> Prop.
- P is declared
- Goal forall n:nat, P n.
- 1 goal ============================ forall n : nat, P n
- intros.
- 1 goal n : nat ============================ P n
- Fail induction n using strong.
- The command has indeed failed with message: Cannot recognize a statement based on N.
- change N in n.
- 1 goal n : N ============================ P n
- (* n is now of type N, matching the inferred type that strong operates on *)
- induction n using strong.
- 1 goal n : N H : forall m : N, m < n -> P m ============================ P n
- Error Unable to find an instance for the variables ident … ident.¶
Use the
with bindings
clause or theeinduction
tactic instead.
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
Example:
induction
withoccurrences
- Lemma induction_test2 : forall n:nat, n = n -> n <= n.
- 1 goal ============================ forall n : nat, n = n -> n <= n
- intros.
- 1 goal n : nat H : n = n ============================ n <= n
- induction n in H |-.
- 2 goals n : nat H : 0 = 0 ============================ n <= n goal 2 is: n <= n
- Show 2.
- goal 2 is: n, n0 : nat H : S n0 = S n0 IHn0 : n0 = n0 -> n <= n ============================ n <= n
- Tactic einduction induction_clause+, induction_principle?¶
Behaves like
induction
except that it does not fail if some dependent premise of the type ofone_term
can't be inferred. Instead, the unresolved premises are posed as existential variables to be inferred later, in the same way aseapply
does.
- Tactic elim one_term_with_bindings using one_term_with_bindings?¶
An older, more basic induction tactic. Unlike
induction
,elim
only modifies the goal; it does not modify the local context. We recommend usinginduction
instead where possible.with bindings
(inone_term_with_bindings
)Explicitly gives instances to the premises of the type of
one_term
(see Bindings).using one_term_with_bindings?
Allows explicitly giving an induction principle
one_term
that is not the standard one for the underlying inductive type ofone_term
. Thebindings
clause allows instantiating premises of the type ofone_term
.
- Tactic eelim one_term_with_bindings using one_term_with_bindings?¶
If the type of
one_term
has dependent premises, this turns them into existential variables to be resolved later on.
- Tactic simple induction identnatural¶
Behaves like
intros until identnatural; elim ident
whenident
is aforall
variable in the goal.
- Tactic dependent induction ident generalizingin ident+? using one_term?¶
The experimental tactic
dependent induction
performs induction-inversion on an instantiated inductive predicate. One needs to firstRequire
theStdlib.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.generalizingin ident+
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 variables that are inside constructors in the induction hypothesis. The other ones need not be further generalized.
There is a long example of
dependent induction
and an explanation of the underlying technique here.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 Stdlib.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 theinduction
tactic. One can make its own variant by just writing a new tactic based on the definition found inStdlib.Program.Equality
.See also
- Tactic fix ident natural with ( ident simple_binder* { struct name }? : type )+?¶
A primitive tactic that starts a proof by induction. Generally, higher-level tactics such as
induction
orelim
are easier to use.The
ident
s (including the first one before thewith
clause) are the names of the induction hypotheses.natural
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. The current lemma must be composed of at leastnatural
products.As in a fix expression, induction hypotheses must be used on structurally smaller arguments. The verification that inductive proof arguments are correct is done only when registering the lemma in the global environment. To know if the use of induction hypotheses is correct during the interactive development of a proof, use the command
Guarded
.with ( ident simple_binder* { struct name }? : type )+
Starts a proof by mutual induction. The statements to be proven are
forall simple_binder_{i}, type_{i}
. The identifiersident
(including the first one before thewith
clause) are the names of the induction hypotheses. The identifiersname
(in the{ struct ... }
clauses) are the respective names of the premises on which the induction is performed in the statements to be proved (if not given, Rocq guesses what they are).
- Tactic cofix ident with ( ident simple_binder* : type )+?¶
Starts a proof by coinduction. The
ident
s (including the first one before thewith
clause) are the names of the coinduction hypotheses. As in a cofix expression, the use of induction hypotheses must be 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
.with ( ident simple_binder* : type )+
Starts a proof by mutual coinduction. The statements to be proven are
forall simple_binder_{i}, type_{i}
. The identifiersident
(including the first one before thewith
clause) are the names of the coinduction hypotheses.
Equality of inductive types¶
This section describes some special purpose tactics to work with Leibniz equality of inductive sets or types.
- Tactic discriminate induction_arg?¶
Proves goals for which a hypothesis or a premise in the goal that is convertible to the form
term_{1} = term_{2}
has inconsistent constructors between the two sides of the equality (i.e., a contradiction). The tactic also works for goals in the formterm_{1} <> term_{2}
that are inconsistent (example).If
induction_arg
is provided, only the provided proof term or hypothesis is checked for inconsistency. Ifinduction_arg
is not given, the tactic does anintro
for each premise in the goal, then it checks all the resulting hypotheses for impossible equalities.The tactic relies on the fact that constructors of inductive types are injective and disjoint, i.e. if
C1
andC2
are distinct constructors of an inductive type thenC1 term_{1} = C1 term_{2}
implies thatterm_{1} = term_{2}
(injectivity) andC1 term_{1} = C2 term_{2}
is a contradiction (disjointedness). For example,S (S O) = S O
is a contradiction: while the outermost constructors are bothS
, the next ones differ (S
versusO
).The tactic traverses the normal forms of
term_{1}
andterm_{2}
, looking for subterms placed in the same positions whose head symbols are different constructors. If such subterms are present, the equality is impossible and the current goal is completed. Otherwise the tactic fails. Note that opaque constants are not expanded by δ reductions while computing the head normal form.Note that
discriminate
doesn't handle contradictory equalities such asn = S n
. In this case you must useinduction
(see example).ident
(asinduction_arg
)Checks the hypothesis
ident
for impossible equalities. Ifident
is not already in the context, this is equivalent tointros until ident; discriminate ident
.natural
(asinduction_arg
)Equivalent to
intros
until natural; discriminate ident
, whereident
is the identifier for the last introduced hypothesis.one_term with bindings
(ininduction_arg
)Equivalent to
discriminate one_term
but uses the given bindings to instantiate parameters or hypotheses ofone_term
.one_term
must be a proof ofterm_{1} = term_{2}
.
- Error No primitive equality found.¶
- Error Not a discriminable equality.¶
- Tactic ediscriminate induction_arg?¶
Works the same as
discriminate
but if the type ofone_term
, or the type of the hypothesis referred to bynatural
, has uninstantiated parameters, these parameters are left as existential variables.
Example: Proving
1 <> 2
- Goal 1 <> 2.
- 1 goal ============================ 1 <> 2
- discriminate.
- No more goals.
- Qed.
This works because
1 <> 2
is represented internally asnot (1 = 2)
, which is just(1 = 2) -> False
from the definition ofnot
:
- Print not.
- not = fun A : Prop => A -> False : Prop -> Prop Arguments not A%type_scope
You can see this better by doing the
intro
explicitly:
- Goal 1 <> 2.
- 1 goal ============================ 1 <> 2
- intro. (* if omitted, "discriminate" does an intro *)
- 1 goal H : 1 = 2 ============================ False
- discriminate.
- No more goals.
- Qed.
Example:
discriminate
limitation: provingn <> S n
- Goal forall n:nat, n <> S n.
- 1 goal ============================ forall n : nat, n <> S n
- intro n.
- 1 goal n : nat ============================ n <> S n
- induction n.
- 2 goals ============================ 0 <> 1 goal 2 is: S n <> S (S n)
- - discriminate. (* works: O and (S O) start with different constructors *)
- 1 goal ============================ 0 <> 1 This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. 1 goal goal 1 is: S n <> S (S n)
- - Fail discriminate. (* fails: discriminate doesn't handle this case *)
- 1 goal n : nat IHn : n <> S n ============================ S n <> S (S n) The command has indeed failed with message: No primitive equality found.
- injection.
- 1 goal n : nat IHn : n <> S n H : S n = S (S n) ============================ n = S n -> False
- assumption.
- No more goals.
- Qed.
- Tactic injection induction_arg? as simple_intropattern*?¶
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} = c t_{2}
thent_{1} = t_{2}
are equal too.If there is a hypothesis
H
in the formterm_{1} = term_{2}
, theninjection H
applies the injectivity of constructors as deep as possible to derive the equality of subterms ofterm_{1}
andterm_{2}
wherever the subterms start to differ. For example, from(S p, S n) = (q, S (S m))
we may deriveS p = q
andn = S m
. The terms must have inductive types and the same head constructor, but must not be convertible. If so, the tactic derives the equalities and adds them to the current goal as premises (except if theas
clause is used).If no
induction_arg
is provided and the current goal is of the formterm <> term
,injection
is equivalent tointro ident; injection ident
.ident
(ininduction_arg
)Derives equalities based on constructor injectivity for the hypothesis
ident
. Ifident
is not already in the context, this is equivalent tointros until ident; injection ident
.natural
(ininduction_arg
)Equivalent to
intros
until natural
followed byinjection ident
whereident
is the identifier for the last introduced hypothesis.one_term with bindings
(ininduction_arg
)Like
injection one_term
but uses the given bindings to instantiate parameters or hypotheses ofone_term
.as [= intropattern* ]
Specifies names to apply after the injection so that all generated equalities become hypotheses, which (unlike
intros
) may replace existing hypotheses with same name. The number of provided names must not exceed the number of newly generated equalities. If it is smaller, fresh names are generated for the unspecified items. The original equality is erased if it corresponds to a provided name or if the list of provided names is incomplete.Note that, as a convenience for users, specifying
simple_intropattern+
is treated as if[= simple_intropattern+ ]
was specified.
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
Note
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
, the use of a sigma type is avoided.- Error No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop. You can try to use option Set Keep Proof Equalities.¶
- Error Not a negated primitive equality¶
When
induction_arg
is not provided, the goal must be in the formterm <> term
.
- Error Nothing to inject.¶
Generated when one side of the equality is not a constructor.
- Tactic einjection induction_arg? as simple_intropattern*?¶
Works the same as
injection
but if the type ofone_term
, or the type of the hypothesis referred to bynatural
has uninstantiated parameters, these parameters are left as existential variables.
- Tactic simple injection induction_arg?¶
Similar to
injection
, but always adds the derived equalities as new premises in the current goal (instead of as new hypotheses) even if theStructural Injection
flag is set.
- Flag Structural Injection¶
When this flag is set,
injection term
erases the original hypothesis and adds the generated equalities as new hypotheses rather than adding them to the current goal as premises, as if givinginjection term as
(with an empty list of names). This flag is off by default.
- Tactic simplify_eq induction_arg?¶
Examines a hypothesis that has the form
term_{1} = term_{2}
. If the terms are structurally different, the tactic does adiscriminate
. Otherwise, it does aninjection
to simplify the equality, if possible. Ifinduction_arg
is not provided, the tactic examines the goal, which must be in the formterm_{1} <> term_{2}
.See the description of
induction_arg
ininjection
for an explanation of the parameters.- Tactic esimplify_eq induction_arg?¶
Works the same as
simplify_eq
but if the type ofone_term
or the type of the hypothesis referred to bynatural
has uninstantiated parameters, these parameters are left as existential variables.
- Tactic inversion identnatural as or_and_intropattern? in ident+?¶
- Tactic inversion identnatural using one_term in ident+?¶
For a hypothesis whose type is a (co)inductively defined proposition, the tactic introduces a goal for each constructor of the proposition that isn't self-contradictory. Each such goal includes the hypotheses needed to deduce the proposition. (Co)inductively defined propositions are those defined with the
Inductive
orCoInductive
commands whose contructors yield aProp
, as in this example.ident
The name of the hypothesis to invert. 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 usingintros until ident
.natural
Equivalent to
intros until natural; inversion ident
whereident
is the identifier for the last introduced hypothesis.in ident+?
When
ident+
are identifiers in the local context, this does ageneralize
ident+
as the initial step ofinversion
.as or_and_intropattern
Provides names for the variables introduced in each new subgoal. The
or_and_intropattern
must have oneintropattern*
for each constructor of the (co)inductive predicate, given in the order in which the constructors are defined. If there are not enough names, Rocq picks fresh names.If an equation splits into several equations (because
inversion
appliesinjection
on the equalities it generates), the correspondingintropattern
should be in the form[ intropattern* ]
(or the equivalent( simple_intropattern )*,
), with the number of entries equal to the number of subequalities obtained from splitting the original equation. Example here.
Note
The
inversion … as
variant ofinversion
generally behaves in a slightly more expected way thaninversion
(no artificial duplication of some hypotheses referring to other hypotheses). To take advantage of these improvements, it is enough to useinversion … as []
, letting Rocq choose fresh names.Note
As
inversion
proofs may be large, we recommend creating and using 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 betweenterm
s whose type is in sortProp
). This behavior can be turned off by using theKeep Proof Equalities
setting.
Example:
inversion
withas or_and_intropattern
- 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.
- 1 goal l : list nat H : contains0 (1 :: l) ============================ contains0 l
- 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
- Tactic inversion_clear identnatural as or_and_intropattern? in ident+?¶
Does an
inversion
and then erases the hypothesis that was used for the inversion.
- Tactic simple inversion identnatural as or_and_intropattern? in ident+?¶
A very simple inversion tactic that derives all the necessary equalities but does not simplify the constraints as
inversion
does.
- Tactic dependent inversion identnatural as or_and_intropattern? with one_term?¶
For use when the inverted hypothesis appears in the current goal. Does an
inversion
and then substitutes the name of the hypothesis where the corresponding term appears in the goal.
- Tactic dependent inversion_clear identnatural as or_and_intropattern? with one_term?¶
Does a
dependent inversion
and then erases the hypothesis that was used for the dependent inversion.
- Tactic dependent simple inversion identnatural as or_and_intropattern? with one_term?¶
- Tactic inversion_sigma ident as simple_intropattern??¶
Turns equalities of dependent pairs (e.g.,
existT P x p = existT P y q
, frequently left over byinversion
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 usingStdlib.Logic.Init.eq
.
Example: Non-dependent 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 length-indexed lists, and a lemma about inverting equality of cons:
- Require Import Stdlib.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
Helper tactics¶
- Tactic decide one_term_{1} with one_term_{2}¶
Replaces occurrences of
one_term_{1}
in the form{P}+{~P}
in the goal with(left _)
or(right _)
, depending onone_term_{2}
.one_term_{2}
must be of type eitherP
or~P
, andP
must be of typeProp
.Example: Using
decide
to rewrite the goal- Goal forall (P Q : Prop) (Hp : {P} + {~P}) (Hq : {Q} + {~Q}), P -> ~Q -> (if Hp then true else false) = (if Hq then false else true).
- 1 goal ============================ forall (P Q : Prop) (Hp : {P} + {~ P}) (Hq : {Q} + {~ Q}), P -> ~ Q -> (if Hp then true else false) = (if Hq then false else true)
- intros P Q Hp Hq p nq.
- 1 goal P, Q : Prop Hp : {P} + {~ P} Hq : {Q} + {~ Q} p : P nq : ~ Q ============================ (if Hp then true else false) = (if Hq then false else true)
- decide Hp with p.
- 1 goal P, Q : Prop Hp : {P} + {~ P} Hq : {Q} + {~ Q} nq : ~ Q p : P ============================ true = (if Hq then false else true)
- decide Hq with nq.
- 1 goal P, Q : Prop Hp : {P} + {~ P} Hq : {Q} + {~ Q} p : P nq : ~ Q ============================ true = true
- reflexivity.
- No more goals.
- Qed.
- Tactic decide equality¶
Solves a goal of the form
forall x y : R,? {x = y} + {~ x = y}
orforall x y : R,? (x = y) \/ (~ x = y)
, whereR
is an inductive type whose constructors do not take proofs or functions as arguments, nor objects in dependent types.
- Tactic compare one_term_{1} one_term_{2}¶
Compares two
one_term
s of an inductive datatype. IfG
is the current goal, it leaves the sub-goalsone_term_{1} = one_term_{2} -> G
and~ one_term_{1} = one_term_{2} -> G
. The type of theone_term
s must satisfy the same restrictions as in the tacticdecide equality
.
- Tactic dependent rewrite -><-? one_term in ident?¶
If
ident
has type(existT B a b)=(existT B a' b')
in the local context (i.e. each term of the equality has a sigma type{ a:A & (B a)}
) this tactic 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.-><-?
By default, the equality is applied from left to right. Specify
<-
to apply the equality from right to left.
Generation of induction principles with Scheme
¶
- Command Scheme ident :=? scheme_kind with ident :=? scheme_kind*¶
- scheme_kind
::=
scheme_type for reference Sort sort_familyscheme_type
::=
Induction|
Minimality|
Elimination|
Casesort_family
::=
Prop|
SProp|
Set|
TypeGenerates induction principles with given
scheme_type
s andscheme_sort
s for an inductive type. In the case where the inductive definition is a mutual inductive definition, thewith
clause is used to generate a mutually recursive inductive scheme for each clause of the mutual inductive type.ident
The name of the scheme. If not provided, the name will be determined automatically from the
scheme_type
andsort_family
.
The following
scheme_type
s generate induction principles with given properties:Recursive
Dependent
Induction
Yes
Yes
Minimality
Yes
No
Elimination
No
Yes
Case
No
No
See examples of the
scheme_type
s here.
- Command Scheme Boolean? Equality for reference¶
Tries to generate a Boolean equality for
reference
. IfBoolean
is not specified, the command also tries to generate a proof of the decidability of propositional equality overreference
. Ifreference
involves independent constants or other inductive types, we recommend defining their equality first.
Example: Induction scheme for tree and forest
Currently the automatically-generated induction principles such as
odd_ind
are not useful for mutually-inductive types such asodd
andeven
. You can define a mutual induction principle for tree and forest in sortSet
with theScheme
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.
- tree_forest_rec is defined forest_tree_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 f : forest, P0 f -> P0 (cons t f)) -> forall t : tree, P t
This principle involves two different predicates for trees and forests; 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.
- odd_even is defined even_odd 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
forall n : nat, even n -> P0 n
.
Example:
Scheme
commands with variousscheme_type
sLet us demonstrate the difference between the Scheme commands.
- Unset Elimination Schemes.
- Inductive Nat := | z : Nat | s : Nat -> Nat.
- Nat is defined
- (* dependent, recursive *)
- Scheme Induction for Nat Sort Set.
- Nat_rec is defined Nat_rec is recursively defined
- About Nat_rec.
- Nat_rec : forall P : Nat -> Set, P z -> (forall n : Nat, P n -> P (s n)) -> forall n : Nat, P n Nat_rec is not universe polymorphic Arguments Nat_rec P%function_scope f f0%function_scope n Nat_rec is transparent Expands to: Constant Top.Nat_rec
- (* non-dependent, recursive *)
- Scheme Minimality for Nat Sort Set.
- Nat_rec_nodep is defined Nat_rec_nodep is recursively defined
- About Nat_rec_nodep.
- Nat_rec_nodep : forall P : Set, P -> (Nat -> P -> P) -> Nat -> P Nat_rec_nodep is not universe polymorphic Arguments Nat_rec_nodep P%type_scope f f0%function_scope n Nat_rec_nodep is transparent Expands to: Constant Top.Nat_rec_nodep
- (* dependent, non-recursive *)
- Scheme Elimination for Nat Sort Set.
- Nat_case is defined Nat_case is recursively defined
- About Nat_case.
- Nat_case : forall P : Nat -> Set, P z -> (forall n : Nat, P (s n)) -> forall n : Nat, P n Nat_case is not universe polymorphic Arguments Nat_case P%function_scope f f0%function_scope n Nat_case is transparent Expands to: Constant Top.Nat_case
- (* non-dependent, non-recursive *)
- Scheme Case for Nat Sort Set.
- Nat_case_nodep is defined Nat_case_nodep is recursively defined
- About Nat_case_nodep.
- Nat_case_nodep : forall P : Set, P -> (Nat -> P) -> Nat -> P Nat_case_nodep is not universe polymorphic Arguments Nat_case_nodep P%type_scope f f0%function_scope n Nat_case_nodep is transparent Expands to: Constant Top.Nat_case_nodep
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 Rocq may now reject well-defined inductive types because it cannot compute a Boolean equality for them.
Combined Scheme¶
- Command Combined Scheme ident_{def} from ident+,¶
Combines 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.
- tree_forest_ind is defined forest_tree_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 f : forest, P0 f -> P0 (cons t f)) -> (forall t : tree, P t) /\ (forall f : forest, P0 f)
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.
- tree_forest_rect is defined forest_tree_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 f : forest, P0 f -> P0 (cons t f)) -> (forall t : tree, P t) * (forall f : forest, P0 f)
Generation of inversion principles with Derive
Inversion
¶
- Command Derive Inversion ident with one_term Sort sort_family?¶
Generates an inversion lemma for the
inversion
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
- 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 Stdlib.Logic.JMeq, hence we need to require it before. For example, revisiting the first example of the inversion documentation:
- Require Import Stdlib.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 Stdlib.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 Stdlib.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 higher-order tactic do_depind
defined in Stdlib.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 simply-typed lambda-calculus formalized in a dependently-typed 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 snoc-lists 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 well-typed 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 inducted-on
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 Stdlib.Program.Tactics.
- Require Import Stdlib.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'