Inductive [R:T1->..->Tn->UNIV] Relation Constructors [rule1 : {x1:t1}..{xk:tk} (* schematic variables *) (* inductive premises *) (R p1 .. pn)->..->(R p'1 .. p'n)-> (* side conditions *) (*--------------------------------------*) S1->..->Sn-> R c1 .. cn (* conclusion *) ] (* more rules *) [ruleN: (* same pattern *) ];

Suppose we have a hypothesis

H : R a1 .. an

To **invert** `H` is to observe that it must have been
derived by some constructor of `R`. That is, for some rule, it
must be the case that the schematic variables have values for which
the premises and side conditions hold and `R a1 .. an`
unifies with `R c1 .. cn`, ie `a1 = c1` .. `an = cn`.

Adding the **Inversion** switch to such an inductive family
`R` (whether defined with Relation set or not) causes LEGO to
prove and store a generic inversion theorem, `R_inversion` for
that family, after the fashion of Clark's **completion**. (Note
that type dependencies within the parameters of `R` will make
the equalities ill-typed. In such cases, the user is informed and no
inversion theorem is generated, but the rest of the definiiton goes
through.)

Having established this theorem, we may now use the **Invert**
tactic to apply it to hypothetical inhabitants of the relation. The
goal will then be split into a case for each constructor of the relation
conditional on the relevant premises, side conditions and equalities.

For example, if we have defined less-than-or-equals inductively with

Inductive [le:nat->nat->Prop] Relation Inversion Constructors [le0:{n:nat}le zero n] [leS:{m,n|nat}(le m n)->le (suc m) (suc n)];

and our current proof state is

H : le m zero ?1 : Eq m zero

then we can invert `H` as follows

Lego> Invert H; Refine by le_inversion H ?3 : (Eq zero m)->{a1:nat}(Eq a1 zero)->Eq m zero ?4 : {a3:nat}(Eq (suc a3) m)->{a2:nat}(Eq (suc a2) zero)->(le a3 a2)-> Eq m zero

Observe that the schematic variables, premises and side conditions
from each constructor have become the premises of the corresponding
subgoal, together with the equations which comprise the claim that
`le m zero` unifies with the conclusion of the constructor.

The new tactic **qnify** attacks
unification problems expressed as equational premises in the
goal. Note that the equations have been deliberately shifted as far
left as their dependencies permit in order to maximise the scope of
any substitutions qnify might apply.

The new **Then** tactical can be used to
instruct Lego to qnify each subgoal generated by Invert. Indeed the
goal `?1` can be proven in one stroke:

H : le m zero ?1 : Eq m zero Lego> Invert H Then qnify Then Refine Eq_refl; (* machine effort *) *** QED ***

Note that the **Inversion** package uses the equality registered by
**Configure Equality**. Also, mutually
inductive relations are not yet supported by this feature.