7.10 Inversion

7.10 Inversion

7.10.1 Inversion ident

Let the type of ident  in the local context be (I vec(t)), where I is a (co)inductive predicate. Then, Inversion applied to ident  derives for each possible constructor ci of (I vec(t)), all the necessary conditions that should hold for the instance (I vec(t)) to be proved by ci.


Variants:
  1. Inversion_clear ident
    That does Inversion and then erases ident  from the context.
  2. 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.
  3. 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.
  4. 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.
  5. Dependent Inversion_clear ident 
    Like Dependant Inversion, except that ident  is cleared from the local context.
  6. 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 vec(t)) and I has type (vec(x):vec(T))s, then term  must be of type I:(vec(x):vec(T))(I vec(x))® s' where s' is the type of the goal.
  7. Dependent Inversion_clear ident  with term
    Like Dependant Inversion ...with but clears identfrom the local context.
  8. Inversion identusing ident'
    Let ident  have type (I vec(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.
  9. Inversion ident  using ident' in ident1...identn
    This tactic behaves as generalizing ident1...identn, then doing Inversionident using ident'.
  10. 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 (vec(x):vec(T))(I vec(t)) Sort sort

This command generates an inversion principle for the Inversion ...using tactic. Let I be an inductive predicate and vec(x) the variables occurring in vec(t). This command generates and stocks the inversion lemma for the sort sort  corresponding to the instance (vec(x):vec(T))(I vec(t)) with the name ident  in the global environment. When applied it is equivalent to have inverted the instance with the tactic Inversion.


Variants:
  1. Derive Inversion_clear ident  with (vec(x):vec(T))(I vec(t)) Sort sort 
    When applied it is equivalent to having inverted the instance with the tactic Inversion replaced by the tactic Inversion_clear.
  2. Derive Dependent Inversion ident  with (vec(x):vec(T))(I vec(t)) Sort sort 
    When applied it is equivalent to having inverted the instance with the tactic Dependent Inversion.
  3. Derive Dependent Inversion_clear ident  with (vec(x):vec(T))(I vec(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

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.1.2.9.html at 8/10/98