Next: qnify, Qnify and Configure Qnify Up: New features in LEGO Version 1.3: Previous: Infix Notation

LEGO Version 1.3: Inversion and Invert

Consider a typical inductively defined relation:

  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.