%unique

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 be transformed into first-class uniqueness lemmas. Unfortunately, there is no automatic way of doing this transformation!

Example

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

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%term pz plus z N N %.
%term ps %pi (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.

If we had created a non-unique definition of plus, for instance by adding an additional, broken version of ps2, STELF 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.

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.

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort div2 {_ nat} {_ nat} %.
%sort div2' {_ nat} {_ nat} %.
%term d2s %pi (div2 (s N) (s M)) %<- (div2' N M) %.
%term d2z div2 z z %.
%term d2's %pi (div2' (s N) M) %<- (div2 N M) %.
%worlds () (div2 _ _) (div2' _ _) %.
%unique div2 %in %out %.
%unique div2' %in %out %.

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 STELF checked) %unique a +X1 … +Xk -1Y. Then, STELF’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.

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%term pz plus z N N %.
%term ps %pi (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.

%sort id {_ nat} {_ nat} %.
%term refl id N N %.

Then we can say that for any $N_1$ and $N_2$, if both $N_1 + N_2 = M$ and $N_1 + N_2 = M'$, then in fact $M = M'$.

%sort plus-unique {_ plus N1 N2 M} {_ plus N1 N2 M'} {_ id M M'} %.
%mode plus-unique %in %in %out %.

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

%term _ 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 _ _ _).

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 %in %in %out %.

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

See also

• Verifying Uniqueness in a Logical Framework, by Penny Anderson and Frank Pfenning