%unique

From The Twelf Project

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.

[edit] 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 (built 03/19/11 at 09:41:05 on gs6177)
%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 (built 03/19/11 at 09:41:05 on gs6177)
%worlds () (plus _ _ _).
Error: 
Uniqueness checking plus:
Constants ps and ps2 overlap


%% ABORT %%

[edit] 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').

[edit] 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 N₁ and N₂, if both N₁ + N₂ = M and N₁ + N₂ = M', then in fact M = M'.

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 (built 03/19/11 at 09:41:05 on gs6177)
%worlds () (plus-unique _ _ _).
Error: 
Coverage error --- missing cases:
{N1:nat} {N2:nat} {M:nat} {M':nat} {X4:plus N1 N2 M} {X5:plus N1 N2 M'}
   {X6:id M M'}
   |- plus-unique X4 X5 X6.


%% 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 (built 03/19/11 at 09:41:05 on gs6177)
%worlds () (plus-unique _ _ _).
%total {} (plus-unique _ _ _).

%% OK %%

[edit] See also

Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'04) pp. 18-33, Park City, Utah, September, 2004

Bibtex

Auteur : Penny Anderson, Frank Pfenning
Titre : Verifying uniqueness in a logical framework
Dans : Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'04) -
Adresse : Park City, Utah
Date : September 2004