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.