7.10 Inversion
7.10.1 Inversion ident
Let the type of ident in the local context be (I t),
where I is a (co)inductive predicate. Then,
Inversion applied to ident derives for each possible
constructor ci of (I t), all the necessary
conditions that should hold for the instance (I t) to be
proved by ci.
Variants:
-
Inversion_clear ident
That does Inversion and then erases ident from the
context.
- Inversion ident in ident1 ... identn
Let ident1 ... identn, be identifiers in the local context. This
tactic behaves as generalizing ident1 ... identn, and
then performing Inversion.
- Inversion_clear ident in ident1 ...identn
Let ident1 ... identn, be identifiers in the local context. This
tactic behaves as generalizing ident1 ... identn, and
then performing Inversion_clear.
- Dependent Inversion ident
That must be used when ident appears in the current goal.
It acts like Inversion and then substitutes ident for the
corresponding term in the goal.
- Dependent Inversion_clear ident
Like Dependant Inversion, except that ident is cleared
from the local context.
- Dependent Inversion ident with term
This variant allow to give the good generalization of the goal. It
is useful when the system fails to generalize the goal automatically. If
ident has type (I t) and I has type
(x:T)s, then term must be of type
I:(x:T)(I x)® s' where s' is the
type of the goal.
- Dependent Inversion_clear ident with term
Like Dependant Inversion ... with but clears identfrom
the local context.
- Inversion ident using ident'
Let ident have type (I t) (I an inductive
predicate) in the local context, and ident' be a (dependent) inversion
lemma. Then, this tactic refines the current goal with the specified
lemma.
- Inversion ident using ident'
in ident1... identn
This tactic behaves as generalizing ident1... identn,
then doing Inversionident using ident'.
- 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 do.
See also: 8.4 for detailed examples
7.10.2 Derive Inversion ident with
(x:T)(I t) Sort sort
This command generates an inversion principle for the
Inversion ... using tactic.
Let I be an inductive predicate and x the variables
occurring in t. This command generates and stocks the
inversion lemma for the sort sort corresponding to the instance
(x:T)(I t) with the name ident in the global environment. When applied it is equivalent to have inverted
the instance with the tactic Inversion.
Variants:
-
Derive Inversion_clear ident with
(x:T)(I t) Sort sort
When applied it is equivalent to having
inverted the instance with the tactic Inversion
replaced by the tactic Inversion_clear.
- Derive Dependent Inversion ident with
(x:T)(I t) Sort sort
When applied it is equivalent to having
inverted the instance with the tactic Dependent Inversion.
- Derive Dependent Inversion_clear ident with
(x:T)(I t) Sort sort
When applied it is equivalent to having
inverted the instance with the tactic Dependent Inversion_clear.
See also: 8.4 for examples
7.10.3 Quote ident
-level approach
This kind of inversion has nothing to do with the tactic
Inversion above. This tactic does Change (ident
t), where t is a term build in order to ensure the
convertibility. In other words, it does inversion of the function
ident. This function must be a fixpoint on a simple recursive
datatype: see 8.6 for the full details.
Error messages:
-
Quote: not a simple fixpoint
Happens when Quote is not able to perform inversion properly.
Variants:
-
Quote ident [ ident1 ...identn ]
All terms that are build only with ident1 ...identn will be
considered by Quote as constants rather than variables.
See also: file theories/DEMOS/DemoQuote.v in the distribution