Next: Relaxed Patterns and Inductive Types Up: New features in LEGO Version 1.3 Previous: Inversion and Invert

Lego Version 1.3: qnify, Qnify and Configure Qnify

First-order unification problems involving only constructors and variables are decidable and have most general unifiers. We have provided a tactic which automates (most of) this procedure. Since it uses Qrepl to perform substitutions, it has acquired the name qnify.

qnify works on unification problems represented as equational premises in the goal. It can be called in three ways:

  • qnify n;
where the problem is to be the leftmost n equational premises
  • qnify;
where the problem is to be all the equational premises
  • qnify H;
which is equivalent to Refine cut H; qnify 1;

qnify essentially sequences calls to other tactics which implement transitions in the unification process. These transitions are (in order of priority):

  • conflict
(Eq (coni blah) (conj blah))->P
  • injectivity
(Eq xi1 yi1)->..->(Eq xiji yiji)->P
(Eq (coni xi1 .. xiji) (coni yi1 .. yiji))->P
  • coalescence
(Eq x y)->P
x,y distinct variables
  • elimination
(Eq x M)->P
x not free in M
  • deletion

So, for example, given a binary tree type with constructors leaf and node, generated with the Theorems switch set, consider the goal:

  ?0: {x:tree}(Eq (node x leaf) (node (node leaf leaf) x))->absurd

Now let's prove it at one stroke:

  Lego> qnify;
  (* deletion *)
  ?1: (Eq (node x leaf) (node (node leaf leaf) x))->absurd
  (* injectivity *)
  ?2: (Eq x (node leaf leaf))->(Eq leaf x)->absurd
  (* elimination *)
  ?3: (Eq leaf (node leaf leaf))->absurd
  (* conflict *)
  *** QED ***

Conflict and injectivity are implemented using the gadgets generated by the Theorems switch, hence the goal-orientated shape of the injectivity theorems. Coalescence and elimination (and the symmetric cases) are implemented using Qrepl. Deletion is just intros.

The coalescence rule compares the depth in context of the two variables and substitutes the more global for the more local. This seems to be the more useful way round in most cases.

The Qnify tactic has similar syntax and behaviour to qnify, except that it performs head normalisation in order to reveal more equations in constructor form. (The relationship is similar to that of Intros to intros.) Hence

  ?: (Eq zero (plus (suc x) y))->absurd

will be proven directly by Qnify but not by qnify.

Note that Qnify will not work correctly with an equality symbol which has a definitional expansion (eg Leibnitz equality) unless that definition is frozen, as head normalisation will otherwise remove the occurrence of the equality symbol rather than revealing it.

Both tactics can be equipped with an occurs-check rule for disproving cyclic equations:
  • checking
(Eq x (coni1 .. (conin x) .. ))->P
This is done with the command

All first-order cyclic equations in inductive datatypes can be mapped onto the equation of a natural number with its successor. Configure Qnify registers the names of the appropriate datatype and disproof. The library definition of the natural numbers contains an appropriate configuration. However, should no such configuration be supplied, the elimination transition nonetheless performs an occurs-check. Equations (Eq x M) with x free in M but not equal to M are merely deleted, but the user is informed.

Note that a single qnify or Qnify command can be undone with Undo 1, even though it may call Refine, intros and Qrepl many times.

Finally, both Theorems and these unification tactics need to be able to recognise the equality predicate and apply properties of reflexivity, substitutivity and symmetry. Further, qnify must use the same equality as Qrepl. For this reason, Configure Qrepl has been subsumed by the stronger Configure Equality.