qnify works on unification problems represented as equational premises in the goal. It can be called in three ways:
|
where the problem is to be the leftmost n equational premises |
|
where the problem is to be all the equational premises |
|
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):
|
----------------------------------- (Eq (coni blah) (conj blah))->P | |
|
(Eq xi1 yi1)->..->(Eq xiji yiji)->P ------------------------------------------------- (Eq (coni xi1 .. xiji) (coni yi1 .. yiji))->P | |
|
P[x:=y] --------------- (Eq x y)->P |
x,y distinct variables |
|
P[x:=M] --------------- (Eq x M)->P |
x not free in M |
|
P -------- A->P |
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:
|
-------------------------------------- (Eq x (coni1 .. (conin x) .. ))->P |
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.