%unique

From The Twelf Project
Jump to: navigation, search
This article or section describes an undocumented feature of Twelf.
The information may be incomplete and subject to change.

A %unique declaration attempts to automatically check whether some positions of a relation (its outputs) are uniquely determined by some other positions (its inputs). Its syntax is similar to that of %mode, except that in addition to being able to specify an argument to be an input (+), an output (-), or unmoded (*), you may also specify an argument to be a unique output (-1).

Successful %unique declarations are used to simplify coverage checking, and they can easily be transformed into first-class uniqueness lemmas.


Example

We define the oft-used example of addition of natural numbers:

nat : type.
z : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.
pz : plus z N N.
ps : plus (s N1) N2 (s N3)
      <- plus N1 N2 N3.


We can then check for uniqueness using %unique (a %worlds declaration is also required).

%worlds () (plus _ _ _).
%unique plus +N1 +N2 -1N3.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%worlds () (plus _ _ _). %unique +{N1:nat} +{N2:nat} -1{N3:nat} (plus N1 N2 N3).

%% OK %%


If we had created a non-unique definition of plus, for instance by adding an additional, broken version of ps2, Twelf would have indicated an error upon checking for uniqueness:

ps2 : plus (s N1) N2 N3 
      <- plus N1 N2 N3.
%worlds () (plus _ _ _).
%unique plus +N1 +N2 -1N3.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%worlds () (plus _ _ _). Error: Uniqueness checking plus: Constants ps and ps2 overlap

%% ABORT %%


Mutual recursion

Checking the uniqueness of mutually recursive predicates creates a problem, because uniqueness (unlike %mode) cannot be checked incrementally. We therefore introduce a simultaneous form of uniqueness declarations, in analogy with other simultaneous declarations.

nat : type.
z : nat.
s : nat -> nat.

div2 : nat -> nat -> type.
div2' : nat -> nat -> type.
d2s : div2 (s N) (s M)
      <- div2' N M.
d2z : div2 z z.
d2's : div2' (s N) M
       <- div2 N M.

%worlds () (div2 _ _) (div2' _ _).

%unique (div2 +N -1M) (div2' +N' -1M').

Coverage checking

Successful %unique declarations are taken into account to simplify certain kinds of coverage goals in coverage checking. Suppose you have a goal with two hypotheses of the form

... {x : a N1 ... Nk M } ... {y : a N1 ... Nk M' } ...

where the inputs N1 ... Nk are all equal, and suppose further that you have declared (and Twelf checked)

%unique a +X1 ... +Xk -1Y.

Then, Twelf's coverage checker will unify the unique outputs M and M' in the coverage goal, which may cause some otherwise non-exhaustive pattern match to be recognized as exhaustive. (If M and M' do not unify, the coverage goal is impossible, and no case will be needed to cover it.)

As a simple example, consider proving a first-class uniqueness lemma for the original plus relation defined above.

nat : type.
z : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.
pz : plus z N N.
ps : plus (s N1) N2 (s N3)
      <- plus N1 N2 N3.

To state such a lemma , we first define identity on natural numbers with just one constructor, reflexivity.

id : nat -> nat -> type.
refl : id N N.

Then we can say that for any and , if both and , then in fact .

plus-unique : plus N1 N2 M -> plus N1 N2 M' -> id M M' -> type.
%mode plus-unique +D +D' -Did.

We might naively hope to be able to prove this theorem with a single case:

- : plus-unique D D' refl.

However, before taking any uniqueness information into account, this pattern match isn't sufficiently general to cover all cases, since matching the third argument as refl requires the types of D and D' to be equal.

%worlds () (plus-unique _ _ _).
%total {} (plus-unique _ _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%worlds () (plus-unique _ _ _). Error: Coverage error --- missing cases: {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:plus X1 X2 X3} {X6:plus X1 X2 X4} {X7:id X3 X4} |- plus-unique X5 X6 X7.

%% ABORT %%

If we can show that plus's output is unique, though, the coverage checker can determine that the coverage goal need not be so generic: the types of D and D' can be considered equal, since the uniqueness declaration says that they will be.

%worlds () (plus _ _ _).
%unique plus +X1 +X2 -1Y.
%worlds () (plus-unique _ _ _).
%total {} (plus-unique _ _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%worlds () (plus-unique _ _ _). %total {} (plus-unique _ _ _).

%% OK %%

See also

Penny Anderson, Frank Pfenning - Verifying uniqueness in a logical framework
Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'04) pp. 18-33, Park City, Utah, September 2004
Bibtex
Author : Penny Anderson, Frank Pfenning
Title : Verifying uniqueness in a logical framework
In : Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'04) -
Address : Park City, Utah
Date : September 2004