# %unique

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