---
title: Unique
author: nbloomf
date: 2017-05-26
tags: arithmetic-made-difficult, literate-haskell
slug: unique
---

> {-# LANGUAGE NoImplicitPrelude #-}
> module Unique
>   ( unique, _test_unique, main_unique
>   ) where
> 
> import Testing
> import Booleans
> import Not
> import And
> import NaturalNumbers
> import Lists
> import ConsumingFold
> import Snoc
> import Reverse
> import Map
> import Range
> import AllAndAny
> import Filter
> import Elt
> import Sublist
> import Select

Today we'll introduce a boolean function $\unique$ to detect whether or not a list has any duplicate items. As usual, we'd like to define $\unique$ as a fold. The signature needs to be $$\lists{A} \rightarrow \bool.$$ How can we do this? Intuitively, we might say

1. $\nil$ is unique, and
2. $\cons(a,x)$ is unique if $x$ is unique and $a$ does not appear in $x$.

Note that $\unique$ will need to "have it's cake and eat it too"; that is, when testing $\cons(a,x)$ for uniqueness we have to check that $x$ is unique (eat the cake) *and* check that $a$ does not appear in $x$ (have the cake). We had a similar problem when we defined $\tails$; the solution there was to use consuming fold, so that's what we'll do here.

:::::: definition ::
Let $A$ be a set. Define $\sigma : A \times \lists{A} \times \bool \rightarrow \bool$ by $$\sigma(a,x,p) = \band(\bnot(\elt(a,x)),p).$$ We then define $\unique : \lists{A} \rightarrow \bool$ by $$\unique = \cfoldr(\btrue)(\sigma).$$

In Haskell:

> unique :: (List t, Equal a) => t a -> Bool
> unique = cfoldr true sigma
>   where
>     sigma a x p = and (not (elt a x)) p

::::::::::::::::::::

Since $\unique$ is defined as a $\cfoldr(\ast)(\ast)$, it can be characterized as the unique solution to a system of functional equations.

:::::: corollary :::
[]{#cor-unique-nil}[]{#cor-unique-cons}
Let $A$ be a set. $\unique$ is the unique map $f : \lists{A} \rightarrow \bool$ satisfying the following system of equations for all $a \in A$ and $x \in \lists{A}$.
$$\left\{\begin{array}{l}
 f(\nil) = \btrue \\
 f(\cons(a,x)) = \band(\bnot(\elt(a,x)),f(x))
\end{array}\right.$$

::: test :::::::::::

> _test_unique_nil :: (List t, Equal a)
>   => t a -> Test Bool
> _test_unique_nil t =
>   testName "unique(nil) == true" $
>    eq (unique (nil `withTypeOf` t)) true
> 
> 
> _test_unique_cons :: (List t, Equal a)
>   => t a -> Test (a -> t a -> Bool)
> _test_unique_cons _ =
>   testName "unique(cons(a,x)) == and(not(elt(a,x)),unique(x))" $
>    \a x -> eq (unique (cons a x)) (and (not (elt a x)) (unique x))

::::::::::::::::::::
::::::::::::::::::::

Special cases.

:::::: theorem :::::
[]{#thm-unique-one}[]{#thm-unique-two}
Let $A$ be a set with $a,b \in A$. Then we have the following.

1. $\unique(\cons(a,\nil)) = \btrue$.
2. $\unique(\cons(a,\cons(b,\nil))) = \bnot(\beq(a,b))$.

::: proof ::::::::::
1. Note that
$$\begin{eqnarray*}
 &   & \unique(\cons(a,\nil)) \\
 & = & \band(\bnot(\elt(a,\nil)),\unique(\nil)) \\
 & = & \band(\bnot(\bfalse),\btrue) \\
 &     \href{@not@#thm-not-false}
   = & \band(\btrue,\btrue) \\
 & = & \btrue
\end{eqnarray*}$$
as claimed.
2. Note that
$$\begin{eqnarray*}
 &   & \unique(\cons(a,\cons(b,\nil))) \\
 & = & \band(\bnot(\elt(a,\cons(b,\nil))),\unique(\cons(b,\nil))) \\
 & = & \band(\bnot(\beq(a,b)),\btrue) \\
 &     \href{@and@#thm-and-true-right}
   = & \bnot(\beq(a,b))
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _test_unique_single :: (List t, Equal a)
>   => t a -> Test (a -> Bool)
> _test_unique_single t =
>   testName "unique(cons(a,nil)) == true" $
>     \a -> unique (cons a (nil `withTypeOf` t))
> 
> 
> _test_unique_double :: (List t, Equal a)
>   => t a -> Test (a -> a -> Bool)
> _test_unique_double t =
>   testName "unique(cons(a,cons(b,nil))) == not(eq(a,b))" $
>     \a b -> eq 
>       (unique (cons a (cons b (nil `withTypeOf` t))))
>       (not (eq a b))

::::::::::::::::::::
::::::::::::::::::::

$\unique$ is "down closed" with respect to $\sublist$.

:::::: theorem :::::
Let $A$ be a set with $x,y \in \lists{A}$. If $\sublist(x,y) = \btrue$ and $\unique(y) = \btrue$, then $\unique(x) = \btrue$.

::: proof ::::::::::
We proceed by list induction on $y$. For the base case $y = \nil$, suppose $\sublist(x,y) = \btrue$. Then we have $x = \nil$, and thus $\unique(x) = \btrue$. For the inductive step, suppose the implication holds for all $x$ for some $y$ and let $b \in A$. Suppose further that $\unique(\cons(b,y)) = \btrue$ and $\sublist(x,\cons(b,y)) = \btrue$. We consider two possibilities for $x$. If $x = \nil$, then $\unique(x) = \btrue$ as needed. Suppose instead that $x = \cons(a,u)$ for some $a \in A$ and $u \in \lists{A}$. Note first that since $\unique(\cons(b,y)) = \btrue$, we have $$\band(\bnot(\elt(a,x)),\unique(y)) = \btrue;$$ in particular, $\unique(y) = \btrue$.  We now consider two possibilities. If $a \neq b$, we have
$$\begin{eqnarray*}
 &   & \btrue \\
 & = & \sublist(x,\cons(b,y)) \\
 & = & \sublist(\cons(a,u),\cons(b,y)) \\
 & = & \sublist(\cons(a,u),y) \\
 & = & \sublist(x,y).
\end{eqnarray*}$$
By the inductive hypothesis we have $\unique(x) = \btrue$ as needed. Suppose instead that $a = b$. Note that $\bnot(\elt(a,y))$, so $\bnot(\elt(a,u))$. Now we have
$$\begin{eqnarray*}
 &   & \btrue \\
 & = & \sublist(x,\cons(b,y)) \\
 & = & \sublist(\cons(a,u),\cons(b,y)) \\
 & = & \sublist(u,y).
\end{eqnarray*}$$
Again by the inductive hypothesis we have $\unique(u) = \btrue$. So
$$\begin{eqnarray*}
 &   & \unique(x) \\
 & = & \unique(\cons(a,u)) \\
 & = & \band(\bnot(\elt(a,u)),\unique(u)) \\
 & = & \band(\btrue,\btrue) \\
 &     \href{@and@#thm-and-eval-true-true}
   = & \btrue
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_unique_sublist :: (List t, Equal a)
>   => t a -> Test (t a -> t a -> Bool)
> _test_unique_sublist _ =
>   testName "if and(unique(x),sublist(y,x)) then unique(y)" $
>    \x y -> if and (unique x) (sublist y x)
>      then unique y
>      else true

::::::::::::::::::::
::::::::::::::::::::

If $f$ is injective, $\map(f)$ preserves uniqueness.

:::::: theorem :::::
Let $A$ and $B$ be sets with $x \in \lists{A}$ and $f : A \rightarrow B$. If $f$ is injective then $\unique(x) = \unique(\map(f)(x))$.

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, note that
$$\begin{eqnarray*}
 &   & \unique(\map(f)(x)) \\
 & = & \unique(\map(f)(\nil)) \\
 &     \href{@map@#cor-map-nil}
   = & \unique(\nil) \\
 & = & \unique(x)
\end{eqnarray*}$$
as needed. For the inductive step, suppose the implication holds for all $f$ for some $x$ and let $a \in A$. Suppose further that $\unique(\cons(a,x)) = \btrue$. Now if $f$ is injective, we have $\elt(f(a),\map(f)(x)) = \elt(a,x)$. Using the inductive hypothesis, we have
$$\begin{eqnarray*}
 &   & \unique(\map(f)(\cons(a,x))) \\
 &     \href{@map@#cor-map-cons}
   = & \unique(\cons(f(a),\map(f)(x))) \\
 & = & \band(\bnot(\elt(f(a),\map(f)(x))),\unique(\map(f)(x))) \\
 & = & \band(\bnot(\elt(a,x)),\unique(x)) \\
 & = & \unique(\cons(a,x)) \\
 & = & \btrue
\end{eqnarray*}$$
as needed.
::::::::::::::::::::
::::::::::::::::::::

$\unique$ and $\filter$.

:::::: theorem :::::
Let $A$ be a set with $x \in \lists{A}$ and $p : A \rightarrow \bool$. If $\unique(x) = \btrue$, then $\unique(\filter(p,x)) = \btrue$.

::: proof ::::::::::
Note that $\sublist(\filter(p,x),x) = \btrue$; so we have $\unique(\filter(p,x)) = \btrue$ as claimed.
::::::::::::::::::::

::: test :::::::::::

> _test_unique_filter :: (List t, Equal a)
>   => t a -> Test ((a -> Bool) -> t a -> Bool)
> _test_unique_filter _ =
>   testName "if unique(x) then unique(filter(p)(x))" $
>    \p x -> if unique x
>      then unique (filter p x)
>      else true

::::::::::::::::::::
::::::::::::::::::::

$\unique$ interacts with $\snoc$.

:::::: theorem :::::
Let $A$ be a set with $a \in A$ and $x \in \lists{A}$. Then $$\unique(\snoc(a,x)) = \band(\bnot(\elt(a,x)),\unique(x)).$$

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, note that
$$\begin{eqnarray*}
 &   & \unique(\snoc(a,\nil)) \\
 &     \href{@snoc@#cor-snoc-nil}
   = & \unique(\cons(a,\nil)) \\
 & = & \band(\bnot(\elt(a,\nil)),\unique(\nil))
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equality holds for all $a$ for some $x$ and let $b \in A$. Using the inductive hypothesis, we have
$$\begin{eqnarray*}
 &   & \unique(\snoc(a,\cons(b,x))) \\
 &     \href{@snoc@#cor-snoc-cons}
   = & \unique(\cons(b,\snoc(a,x))) \\
 & = & \band(\bnot(\elt(b,\snoc(a,x))),\unique(\snoc(a,x))) \\
 &     \href{@elt@#thm-elt-snoc}
   = & \band(\bnot(\bif{\beq(b,a)}{\btrue}{\elt(b,x)}),\unique(\snoc(a,x))) \\
 & = & \band(\bnot(\elt(b,\cons(a,x))),\band(\bnot(\elt(a,x))),\unique(x)) \\
 & = & \band(\bnot(\bif{\beq(b,a)}{\btrue}{\elt(b,x)}),\band(\bnot(\elt(a,x)),\unique(x))) \\
 & = & \band(\bif{\beq(b,a)}{\bfalse}{\bnot(\elt(b,x))},\band(\bnot(\elt(a,x)),\unique(x))) \\
 & = & \bif{\beq(a,b)}{\band(\bfalse,\band(\bnot(\elt(a,x)),\unique(x)))}{\band(\bnot(\elt(b,x)),\band(\bnot(\elt(a,x)),\unique(x)))} \\
 & = & \bif{\beq(a,b)}{\bfalse}{\band(\band(\bnot(\elt(b,x)),\bnot(\elt(a,x))),\unique(x))} \\
 &     \href{@and@#thm-and-commutative}
   = & \bif{\beq(a,b)}{\bfalse}{\band(\band(\bnot(\elt(a,x)),\bnot(\elt(b,x))),\unique(x))} \\
 &     \href{@and@#thm-and-associative}
   = & \bif{\beq(a,b)}{\bfalse}{\band(\bnot(\elt(a,x)),\band(\bnot(\elt(b,x)),\unique(x)))} \\
 &     \href{@and@#thm-and-false-left}
   = & \bif{\beq(a,b)}{\band(\bfalse,\band(\bnot(\elt(b,x)),\unique(x)))}{\band(\bnot(\elt(a,x)),\band(\bnot(\elt(b,x)),\unique(x)))} \\
 & = & \band(\bif{\beq(a,b)}{\bfalse}{\bnot(\elt(a,x))},\band(\bnot(\elt(b,x)),\unique(x))) \\
 & = & \band(\bnot(\bif{\beq(a,b)}{\btrue}{\elt(a,x)}),\band(\bnot(\elt(b,x)),\unique(x))) \\
 &     \href{@elt@#cor-elt-cons}
   = & \band(\bnot(\elt(a,\cons(b,x))),\band(\bnot(\elt(b,x)),\unique(x))) \\
 & = & \band(\bnot(\elt(a,\cons(b,x))),\unique(\cons(b,x)))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_unique_snoc :: (List t, Equal a)
>   => t a -> Test (a -> t a -> Bool)
> _test_unique_snoc _ =
>   testName "unique(snoc(a,x)) == and(not(elt(a,x)),unique(x))" $
>    \a x -> eq (unique (snoc a x)) (and (not (elt a x)) (unique x))

::::::::::::::::::::
::::::::::::::::::::

$\unique$ interacts with $\rev$.

:::::: theorem :::::
[]{#thm-unique-rev}
Let $A$ be a set with $x \in \lists{A}$. Then $\unique(x) = \unique(\rev(x))$.

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, note that
$$\begin{eqnarray*}
 &   & \unique(\rev(x)) \\
 & = & \unique(\rev(\nil)) \\
 &     \href{@rev@#cor-rev-nil}
   = & \unique(\nil) \\
 & = & \unique(x)
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equality holds for some $x$ and let $a \in A$. Now
$$\begin{eqnarray*}
 &   & \unique(\rev(\cons(a,x))) \\
 &     \href{@rev@#cor-rev-cons}
   = & \unique(\snoc(a,\rev(x))) \\
 & = & \band(\bnot(\elt(a,\rev(x))),\unique(\rev(x))) \\
 & = & \band(\bnot(\elt(a,x)),\unique(x)) \\
 & = & \unique(\cons(a,x))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_unique_rev :: (List t, Equal a)
>   => t a -> Test (t a -> Bool)
> _test_unique_rev _ =
>   testName "unique(x) == unique(rev(x))" $
>   \x -> eq (unique x) (unique (rev x))

::::::::::::::::::::
::::::::::::::::::::

$\range$s are unique.

:::::: theorem :::::
[]{#thm-unique-range}
Let $a,b \in \nats$. We have $$\unique(\range(a,b)) = \btrue.$$

::: proof ::::::::::
We proceed by induction on $b$. For the base case $b = \zero$, we have
$$\begin{eqnarray*}
 &   & \unique(\range(a,\zero)) \\
 & = & \unique(\nil) \\
 &     \href{@unique@#cor-unique-nil}
   = & \btrue
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equality holds for all $a$ for some $b$. Now
$$\begin{eqnarray*}
 &   & \unique(a,\next(b)) \\
 & = & \unique(\cons(a,\range(\next(a),b))) \\
 & = & \band(\bnot(\elt(a,\range(\next(a),b))),\unique(\range(\next(a),b))) \\
 &     \href{@unique@#thm-unique-range}
   = & \band(\bnot(\elt(a,\range(\next(a),b))),\btrue) \\
 &     \href{@and@#thm-and-true-right}
   = & \bnot(\elt(a,\range(\next(a),b))) \\
 & = & \bnot(\bfalse) \\
 &     \href{@not@#thm-not-false}
   = & \btrue
\end{eqnarray*}$$
::::::::::::::::::::

::: test :::::::::::

> _test_unique_range :: (List t, Natural n, Equal n)
>   => t a -> n -> Test (t n -> n -> n -> Bool)
> _test_unique_range _ _ =
>   testName "unique(range(a,b)) == true" $
>   \t a b -> unique ((range a b) `withTypeOf` t)

::::::::::::::::::::
::::::::::::::::::::

$\unique$ can detect $\elt$.

:::::: theorem :::::
Let $A$ be a set. For all $a \in A$ and $x \in X$, we have $$\all(\unique)(\map(\cons(a,\cons(-,\nil)))(x)) = \bnot(\elt(a,x)).$$

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, we have
$$\begin{eqnarray*}
 &   & \all(\unique)(\map(\cons(a,\cons(-,x)))(\nil)) \\
 & = & \all(\unique)(\nil) \\
 & = & \btrue \\
 &     \href{@not@#thm-not-false}
   = & \bnot(\bfalse) \\
 & = & \bnot(\elt(a,\nil))
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equality holds for all $a$ for some $x$, and let $b \in A$. Now
$$\begin{eqnarray*}
 &   & \all(\unique)(\map(\cons(a,\cons(-,\nil)))(\cons(b,x))) \\
 & = & \all(\unique)(\cons(\cons(a,\cons(b,\nil)),\map(\cons(a,\cons(-,\nil)))(x))) \\
 & = & \band(\unique(\cons(a,\cons(b,\nil))),\all(\unique)(\map(\cons(a,\cons(-,\nil)))(x))) \\
 & = & \band(\unique(\cons(a,\cons(b,\nil))),\bnot(\elt(a,x))) \\
 &     \href{@unique@#thm-unique-two}
   = & \band(\bnot(\beq(a,b)),\bnot(\elt(a,x))) \\
 &     \href{@or@#thm-demorgan-not-or}
   = & \bnot(\bor(\beq(a,b),\elt(a,x))) \\
 & = & \bnot(\elt(a,\cons(b,x)))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_unique_elt :: (List t, Equal a)
>   => t a -> Test (a -> t a -> Bool)
> _test_unique_elt t =
>   testName "all(unique)(map(cons(a,cons(-,nil)))(x)) == not(elt(a,x))" $
>   \a x -> eq
>     (all unique (map (\b -> cons a (cons b (nil `withTypeOf` t))) x))
>     (not (elt a x))

::::::::::::::::::::
::::::::::::::::::::

$\unique$ and $\select$.

:::::: theorem :::::
Let $A$ be a set. For all $x \in \lists{A}$ we have $$\unique(x) = \all(\unique)(\select(\next(\next(\zero)),x)).$$

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, we have
$$\begin{eqnarray*}
 &   & \all(\unique)(\select(\next(\next(\zero)),x)) \\
 & = & \all(\unique)(\select(\next(\next(\zero)),\nil)) \\
 & = & \all(\unique)(\nil) \\
 & = & \btrue \\
 &     \href{@unique@#cor-unique-nil}
   = & \unique(\nil) \\
 & = & \unique(x)
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equality holds for some $x$ and let $a \in A$. Using the inductive hypothesis, we have
$$\begin{eqnarray*}
 &   & \all(\unique)(\select(\next(\next(\zero)),\cons(a,x))) \\
 & = & \all(\unique)(\cat(\map(\cons(a,-))(\select(\next(\zero),x)),\select(\next(\next(\zero)),x))) \\
 & = & \all(\unique)(\cat(\map(\cons(a,-))(\map(\cons(-,\nil))(x)),\select(\next(\next(\zero)),x))) \\
 & = & \all(\unique)(\cat(\map(\cons(a,\cons(-,\nil)))(x),\select(\next(\next(\zero)),x))) \\
 & = & \band(\all(\unique)(\map(\cons(a,\cons(-,\nil)))(x)),\all(\unique)(\select(\next(\next(\zero)),x))) \\
 & = & \band(\all(\unique)(\map(\cons(a,\cons(-,\nil)))(x)),\unique(x)) \\
 & = & \band(\bnot(\elt(a,x)),\unique(x)) \\
 & = & \unique(\cons(a,x))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_unique_select_two :: (List t, Equal a, Natural n)
>   => t a -> n -> Test (t a -> Bool)
> _test_unique_select_two _ n =
>   testName "unique(x) == unique(select(next(next(zero)),x))" $
>   \x -> eq
>     (unique x)
>     (all unique (select (next (next zero) `withTypeOf` n) x))

::::::::::::::::::::
::::::::::::::::::::


Testing
-------

Suite:

> _test_unique ::
>   ( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
>   , TypeName (t a), List t, Arbitrary (t n), Show (t n), Equal (t n)
>   , TypeName n, Natural n, Show n, Arbitrary n, Equal n
>   , Equal (t a), Show (t a), Arbitrary (t a), Equal (t (t a))
>   ) => Int -> Int -> t a -> n -> IO ()
> _test_unique size cases t n = do
>   testLabel1 "unique" t
> 
>   let args = testArgs size cases
> 
>   runTest args (_test_unique_nil t)
>   runTest args (_test_unique_cons t)
>   runTest args (_test_unique_single t)
>   runTest args (_test_unique_double t)
>   runTest args (_test_unique_sublist t)
>   runTest args (_test_unique_filter t)
>   runTest args (_test_unique_snoc t)
>   runTest args (_test_unique_rev t)
>   runTest args (_test_unique_range t n)
>   runTest args (_test_unique_elt t)
>   runTest args (_test_unique_select_two t n)

Main:

> main_unique :: IO ()
> main_unique = do
>   _test_unique 20 100 (nil :: ConsList Bool)  (zero :: Unary)
>   _test_unique 20 100 (nil :: ConsList Unary) (zero :: Unary)