Dedupe

Posted on 2017-05-28 by nbloomf

Tags: arithmetic-made-difficult, literate-haskell

\(\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}\) \(\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}\) \(\newcommand{\a}{a}\) \(\newcommand{\b}{b}\) \(\newcommand{\c}{c}\) \(\newcommand{\p}{p}\) \(\newcommand{\q}{q}\) \(\newcommand{\r}{r}\) \(\newcommand{\s}{s}\) \(\newcommand{\x}{x}\) \(\newcommand{\y}{y}\) \(\newcommand{\z}{z}\) \(\newcommand{\bool}{\mathbb{B}}\) \(\newcommand{\btrue}{\mathsf{true}}\) \(\newcommand{\bfalse}{\mathsf{false}}\) \(\newcommand{\bnot}{\mathsf{not}}\) \(\newcommand{\band}{\mathbin{\mathsf{and}}}\) \(\newcommand{\bor}{\mathbin{\mathsf{or}}}\) \(\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}\) \(\newcommand{\beq}{\mathsf{eq}}\) \(\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}\) \(\newcommand{\id}{\mathsf{id}}\) \(\newcommand{\compose}{\mathsf{compose}}\) \(\newcommand{\const}{\mathsf{const}}\) \(\newcommand{\apply}{\mathsf{apply}}\) \(\newcommand{\flip}{\mathsf{flip}}\) \(\newcommand{\flipB}{\mathsf{flip2}}\) \(\newcommand{\flipC}{\mathsf{flip3}}\) \(\newcommand{\flipD}{\mathsf{flip4}}\) \(\newcommand{\flipE}{\mathsf{flip5}}\) \(\newcommand{\clone}{\mathsf{clone}}\) \(\newcommand{\cloneC}{\mathsf{clone3}}\) \(\newcommand{\composeAonB}{\mathsf{compose1on2}}\) \(\newcommand{\composeAonC}{\mathsf{compose1on3}}\) \(\newcommand{\composeAonD}{\mathsf{compose1on4}}\) \(\newcommand{\composeBonA}{\mathsf{compose2on1}}\) \(\newcommand{\composeBonB}{\mathsf{compose2on2}}\) \(\newcommand{\composeConA}{\mathsf{compose3on1}}\) \(\newcommand{\ptrue}{\mathsf{ptrue}}\) \(\newcommand{\pfalse}{\mathsf{pfalse}}\) \(\newcommand{\pnot}{\mathsf{pnot}}\) \(\newcommand{\pand}{\mathbin{\mathsf{pand}}}\) \(\newcommand{\por}{\mathbin{\mathsf{por}}}\) \(\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}\) \(\newcommand{\fst}{\mathsf{first}}\) \(\newcommand{\snd}{\mathsf{second}}\) \(\newcommand{\dup}{\mathsf{dup}}\) \(\newcommand{\tup}{\mathsf{tup}}\) \(\newcommand{\tSwap}{\mathsf{swap}_{\times}}\) \(\newcommand{\tPair}{\mathsf{pair}_{\times}}\) \(\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}\) \(\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}\) \(\newcommand{\tupL}{\mathsf{tupL}}\) \(\newcommand{\tupR}{\mathsf{tupR}}\) \(\newcommand{\uncurry}{\mathsf{uncurry}}\) \(\newcommand{\curry}{\mathsf{curry}}\) \(\newcommand{\lft}{\mathsf{left}}\) \(\newcommand{\rgt}{\mathsf{right}}\) \(\newcommand{\either}{\mathsf{either}}\) \(\newcommand{\uSwap}{\mathsf{swap}_{+}}\) \(\newcommand{\uPair}{\mathsf{pair}_{+}}\) \(\newcommand{\uAssocL}{\mathsf{assocL}_{+}}\) \(\newcommand{\uAssocR}{\mathsf{assocR}_{+}}\) \(\newcommand{\isLft}{\mathsf{isLeft}}\) \(\newcommand{\isRgt}{\mathsf{isRight}}\) \(\newcommand{\nats}{\mathbb{N}}\) \(\newcommand{\zero}{\mathsf{0}}\) \(\newcommand{\next}{\mathsf{next}}\) \(\newcommand{\unnext}{\mathsf{unnext}}\) \(\newcommand{\iszero}{\mathsf{isZero}}\) \(\newcommand{\prev}{\mathsf{prev}}\) \(\newcommand{\natrec}{\mathsf{natrec}}\) \(\newcommand{\simprec}{\mathsf{simprec}}\) \(\newcommand{\bailrec}{\mathsf{bailrec}}\) \(\newcommand{\mutrec}{\mathsf{mutrec}}\) \(\newcommand{\dnatrec}{\mathsf{dnatrec}}\) \(\newcommand{\normrec}{\mathsf{normrec}}\) \(\newcommand{\findsmallest}{\mathsf{findsmallest}}\) \(\newcommand{\mnormrec}{\mathsf{mnormrec}}\) \(\newcommand{\nequal}{\mathsf{eq}}\) \(\newcommand{\nplus}{\mathsf{plus}}\) \(\newcommand{\ntimes}{\mathsf{times}}\) \(\newcommand{\nleq}{\mathsf{leq}}\) \(\newcommand{\ngeq}{\mathsf{geq}}\) \(\newcommand{\nminus}{\mathsf{minus}}\) \(\newcommand{\nmax}{\mathsf{max}}\) \(\newcommand{\nmin}{\mathsf{min}}\) \(\newcommand{\ndivalg}{\mathsf{divalg}}\) \(\newcommand{\nquo}{\mathsf{quo}}\) \(\newcommand{\nrem}{\mathsf{rem}}\) \(\newcommand{\ndiv}{\mathsf{div}}\) \(\newcommand{\ngcd}{\mathsf{gcd}}\) \(\newcommand{\ncoprime}{\mathsf{coprime}}\) \(\newcommand{\nlcm}{\mathsf{lcm}}\) \(\newcommand{\nmindiv}{\mathsf{mindiv}}\) \(\newcommand{\nisprime}{\mathsf{isPrime}}\) \(\newcommand{\npower}{\mathsf{power}}\) \(\newcommand{\nchoose}{\mathsf{choose}}\) \(\newcommand{\dom}{\mathsf{dom}}\) \(\newcommand{\cod}{\mathsf{cod}}\) \(\newcommand{\lists}[1]{\mathsf{List}(#1)}\) \(\newcommand{\nil}{\mathsf{nil}}\) \(\newcommand{\cons}{\mathsf{cons}}\) \(\newcommand{\uncons}{\mathsf{uncons}}\) \(\newcommand{\isnil}{\mathsf{isNil}}\) \(\newcommand{\tail}{\mathsf{tail}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\foldr}{\mathsf{foldr}}\) \(\newcommand{\foldl}{\mathsf{foldl}}\) \(\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}\) \(\newcommand{\unfoldN}{\mathsf{unfoldN}}\) \(\newcommand{\dfoldr}{\mathsf{dfoldr}}\) \(\newcommand{\cfoldr}{\mathsf{cfoldr}}\) \(\newcommand{\bfoldr}{\mathsf{bfoldr}}\) \(\newcommand{\dbfoldr}{\mathsf{dbfoldr}}\) \(\newcommand{\lfoldr}{\mathsf{lfoldr}}\) \(\newcommand{\snoc}{\mathsf{snoc}}\) \(\newcommand{\revcat}{\mathsf{revcat}}\) \(\newcommand{\rev}{\mathsf{rev}}\) \(\newcommand{\last}{\mathsf{last}}\) \(\newcommand{\cat}{\mathsf{cat}}\) \(\newcommand{\addlength}{\mathsf{addlength}}\) \(\newcommand{\length}{\mathsf{length}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\at}{\mathsf{at}}\) \(\newcommand{\map}{\mathsf{map}}\) \(\newcommand{\range}{\mathsf{range}}\) \(\newcommand{\zip}{\mathsf{zip}}\) \(\newcommand{\zipPad}{\mathsf{zipPad}}\) \(\newcommand{\unzip}{\mathsf{unzip}}\) \(\newcommand{\prefix}{\mathsf{prefix}}\) \(\newcommand{\suffix}{\mathsf{suffix}}\) \(\newcommand{\lcp}{\mathsf{lcp}}\) \(\newcommand{\lcs}{\mathsf{lcs}}\) \(\newcommand{\all}{\mathsf{all}}\) \(\newcommand{\any}{\mathsf{any}}\) \(\newcommand{\tails}{\mathsf{tails}}\) \(\newcommand{\inits}{\mathsf{inits}}\) \(\newcommand{\filter}{\mathsf{filter}}\) \(\newcommand{\elt}{\mathsf{elt}}\) \(\newcommand{\addcount}{\mathsf{addcount}}\) \(\newcommand{\count}{\mathsf{count}}\) \(\newcommand{\repeat}{\mathsf{repeat}}\) \(\newcommand{\sublist}{\mathsf{sublist}}\) \(\newcommand{\infix}{\mathsf{infix}}\) \(\newcommand{\select}{\mathsf{select}}\) \(\newcommand{\unique}{\mathsf{unique}}\) \(\newcommand{\delete}{\mathsf{delete}}\) \(\newcommand{\dedupeL}{\mathsf{dedupeL}}\) \(\newcommand{\dedupeR}{\mathsf{dedupeR}}\) \(\newcommand{\common}{\mathsf{common}}\) \(\newcommand{\disjoint}{\mathsf{disjoint}}\) \(\newcommand{\sublists}{\mathsf{sublists}}\) \(\newcommand{\take}{\mathsf{take}}\) \(\newcommand{\drop}{\mathsf{drop}}\) \(\newcommand{\takeBut}{\mathsf{takeBut}}\) \(\newcommand{\dropBut}{\mathsf{dropBut}}\) \(\newcommand{\takeWhile}{\mathsf{takeWhile}}\) \(\newcommand{\dropWhile}{\mathsf{dropWhile}}\)

This page is part of a series on Arithmetic Made Difficult.

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude #-}
module Dedupe
  ( dedupeL, dedupeR, _test_dedupe, main_dedupe
  ) where

import Testing
import Booleans
import NaturalNumbers
import Lists
import Snoc
import Reverse
import PrefixAndSuffix
import Filter
import Elt
import Unique
import Delete

Today we’ll define a function dedupe which removes any “duplicate” items in a list. Before jumping in, let’s think a little about what such a function should do. For example, say we run dedupe on the list \[\langle a, b, a, c, a \rangle.\] The item \(a\) appears three times, so after deduplicating it should only appear once. We’d prefer not to change the relative order of items in the list, so all we can do is remove two of the \(a\)s. There are three ways to do this, resulting in either \[\langle a, b, c \rangle,\] \[\langle b, a, c \rangle,\] or \[\langle b, c, a \rangle.\] That is, we can keep the first copy of \(a\), the last copy, or some middle copy. It seems to me that keeping some middle copy is not the most general solution. If an item appears only twice, there is no middle appearance, and if an item appears more than three times then there is no unique middle appearance to keep. So it appears the two most general options are to keep the first copy of an item or to keep the last copy. We will call these strategies \(\dedupeL\) (deduplicate from the Left) and \(\dedupeR\) (deduplicate from the Right), respectively. We’ll see that these two options are related. We’ll start with \(\dedupeL\).

We want to implement \(\dedupeL\) as either a right fold or a left fold. But which one? Say our input list is \[x = \langle a, b, c \rangle.\] Note that \(\foldr(\varepsilon)(\varphi)(x)\) will expand into \[\varphi(a, \varphi(b, \varphi(c, \varepsilon))),\] while \(\foldl(\varepsilon){\varphi}(x)\) will expand into \[\varphi(c, \varphi(b, \varphi(a, \varepsilon))).\] Note that \(\dedupeL\) has to process the entire input list, so both of these computations will evaluate completely from the inside out. So which one makes more sense, keeping in mind that \(\dedupeL\) needs to detect the first appearance of each item?

With this handwavy mess in mind, we define \(\dedupeL\) as follows.

Let \(A\) be a set. Define \(\varphi : A \times \lists{A} \rightarrow \lists{A}\) by \[\varphi(a,x) = \cons(a,\delete(a,x)).\] Now define \(\dedupeL : \lists{A} \rightarrow \lists{A}\) by \[\dedupeL(x) = \foldr(\nil)(\varphi)(x).\]

In Haskell:

dedupeL :: (List t, Equal a) => t a -> t a
dedupeL = foldr nil phi
  where
    phi a x = cons a (delete a x)

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

Let \(A\) be a set. \(\dedupeL\) is the unique map \(f : \lists{A} \rightarrow \lists{A}\) satisfying the following equations for all \(a \in A\) and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(\nil) = \nil \\ f(\cons(a,x)) = \cons(a,\delete(a)(f(x))) \end{array}\right.\]

_test_dedupeL_nil :: (List t, Equal a, Equal (t a))
  => t a -> Test Bool
_test_dedupeL_nil t =
  testName "dedupeL(nil) == nil" $
  eq (dedupeL nil) (nil `withTypeOf` t)


_test_dedupeL_cons :: (List t, Equal a, Equal (t a))
  => t a -> Test (a -> t a -> Bool)
_test_dedupeL_cons _ =
  testName "dedupeL(cons(a,x)) == cons(a,delete(a)(dedupeL(x)))" $
  \a x -> eq (dedupeL (cons a x)) (cons a (delete a (dedupeL x)))

Now \(\dedupeL\) and \(\delete\) commute.

Let \(A\) be a set, with \(a \in A\) and \(x \in \lists{A}\). Then \[\delete(a,\dedupeL(x)) = \dedupeL(\delete(a,x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \delete(a,\dedupeL(\nil)) \\ & = & \delete(a,\nil) \\ & = & \nil \\ & = & \dedupeL(\nil) \\ & = & \dedupeL(\delete(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\). We consider two possibilities. If \(b = a\), we have \[\begin{eqnarray*} & & \delete(a,\dedupeL(\cons(b,x))) \\ & = & \delete(a,\cons(b,\delete(b,\dedupeL(x)))) \\ & = & \delete(a,\delete(b,\dedupeL(x))) \\ & = & \delete(a,\delete(a,\dedupeL(x))) \\ & = & \delete(a,\dedupeL(x)) \\ & = & \dedupeL(\delete(a,x)) \\ & = & \dedupeL(\delete(a,\cons(a,x))) \\ & = & \dedupeL(\delete(a,\cons(b,x))) \end{eqnarray*}\] as needed. Suppose instead that \(b \neq a\). Now we have \[\begin{eqnarray*} & & \delete(a,\dedupeL(\cons(b,x))) \\ & = & \delete(a,\cons(b,\delete(b,\dedupeL(x)))) \\ & = & \cons(b,\delete(a,\delete(b,\dedupeL(x)))) \\ & = & \cons(b,\delete(b,\delete(a,\dedupeL(x)))) \\ & = & \cons(b,\delete(b,\dedupeL(\delete(a,x)))) \\ & = & \dedupeL(\cons(b,\delete(a,x))) \\ & = & \dedupeL(\delete(a,\cons(b,x))) \end{eqnarray*}\] as needed.

_test_dedupeL_delete :: (List t, Equal a, Equal (t a))
  => t a -> Test (a -> t a -> Bool)
_test_dedupeL_delete _ =
  testName "dedupeL(delete(a,x)) == delete(a,dedupeL(x))" $
  \a x -> eq (dedupeL (delete a x)) (delete a (dedupeL x))

\(\dedupeL\)s are \(\unique\).

Let \(A\) be a set with \(x \in \lists{A}\). Then \(\unique(\dedupeL(x)) = \btrue\).

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \unique(\dedupeL(\nil)) \\ & = & \unique(\nil) \\ & \href{/posts/arithmetic-made-difficult/Unique.html#cor-unique-nil} = & \btrue \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 \(\unique(\dedupeL(x)) = \btrue\), so that \(\unique(\delete(a,\dedupeL(x))) = \btrue\). Now \[\begin{eqnarray*} & & \unique(\dedupeL(\cons(a,x))) \\ & = & \unique(\cons(a,\delete(a,\dedupeL(x)))) \\ & = & \band(\bnot(\elt(a,\delete(a,\dedupeL(x)))),\unique(\delete(a,\dedupeL(x)))) \\ & = & \band(\btrue,\unique(\delete(a,\dedupeL(x)))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \unique(\delete(a,\dedupeL(x))) \\ & = & \btrue \end{eqnarray*}\] as needed.

_test_dedupeL_unique :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> Bool)
_test_dedupeL_unique _ =
  testName "unique(dedupeL(x)) == true" $
  \x -> unique (dedupeL x)

\(\dedupeL\) preserves \(\prefix\).

Let \(A\) be a set with \(x,y \in \lists{A}\). If \(\prefix(x,y) = \btrue\) then \(\prefix(\dedupeL(x),\dedupeL(y)) = \btrue\).

We proceed by list induction on \(x\). For the base case \(x = \nil\), note that \[\prefix(x,y) = \prefix(\nil,y) = \btrue\] and \[\begin{eqnarray*} & & \prefix(\dedupeL(x),\dedupeL(y)) \\ & = & \prefix(\dedupeL(\nil),\dedupeL(y)) \\ & = & \prefix(\nil,\dedupeL(y)) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for all \(y\) for some \(x\) and let \(a \in A\). Suppose further that \(\prefix(\cons(a,x),y) = \btrue\). Now we must have \(y = \cons(a,u)\) where \(\prefix(x,u) = \btrue\). Using the inductive hypothesis, we have \[\prefix(\dedupeL(x),\dedupeL(u)) = \btrue,\] so that \[\prefix(\delete(a,\dedupeL(x)),\delete(a,\dedupeL(u))) = \btrue.\] Now \[\begin{eqnarray*} & & \prefix(\dedupeL(\cons(a,x)),\dedupeL(y)) \\ & = & \prefix(\dedupeL(\cons(a,x)),\dedupeL(\cons(a,u))) \\ & = & \prefix(\cons(a,\delete(a,\dedupeL(x))),\cons(a,\delete(a,\dedupeL(u)))) \\ & = & \prefix(\delete(a,\dedupeL(x)),\delete(a,\dedupeL(u))) \\ & = & \btrue \end{eqnarray*}\] as needed.

_test_dedupeL_prefix :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_dedupeL_prefix _ =
  testName "prefix(x,y) ==> prefix(dedupeL(x),dedupeL(y))" $
  \x y -> if prefix x y
    then prefix (dedupeL x) (dedupeL y)
    else true

\(\dedupeL\) fixes \(\unique\)s.

Let \(A\) be a set and \(x \in \lists{A}\). Then \(\beq(x,\dedupeL(x)) = \unique(x)\).

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \beq(x,\dedupeL(x)) \\ & = & \beq(\nil,\dedupeL(\nil)) \\ & = & \beq(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \btrue \\ & = & \unique(\nil) \\ & = & \unique(x) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). \[\begin{eqnarray*} & & \beq(\cons(a,x),\dedupeL(\cons(a,x))) \\ & = & \beq(\cons(a,x),\cons(a,\delete(a,\dedupeL(x)))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(a,a),\beq(x,\delete(a,\dedupeL(x)))) \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \band(\btrue,\beq(x,\delete(a,\dedupeL(x)))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \beq(x,\delete(a,\dedupeL(x))) \\ & = & \beq(x,\dedupeL(\delete(a,x))) \\ & = & Q. \end{eqnarray*}\] We now consider two possibilities. If \(\elt(a,x) = \bfalse\), then \[\beq(x,\delete(a,x)) = \bnot(\elt(a,x)) = \btrue,\] and using the inductive hypothesis on \(x\) we have \[\begin{eqnarray*} & & Q \\ & = & \beq(x,\dedupeL(x)) \\ & = & \unique(x) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \band(\btrue,\unique(x)) \\ & = & \band(\bnot(\elt(a,x)),\unique(x)) \\ & = & \unique(\cons(a,x)) \end{eqnarray*}\] as needed. Suppose instead that \(\elt(a,x) = \btrue\). Note that \[\begin{eqnarray*} & & \elt(a,\dedupeL(\delete(a,x))) \\ & = & \elt(a,\delete(a,\dedupeL(x))) \\ & = & \bfalse, \end{eqnarray*}\] so that \(\beq(x,\dedupeL(\delete(a,x))) = \bfalse\). Now \[\begin{eqnarray*} & & Q \\ & = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \band(\bfalse,\unique(x)) \\ & = & \band(\bnot(\elt(a,x)),\unique(x)) \\ & = & \unique(\cons(a,x)) \end{eqnarray*}\] as needed.

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

\(\dedupeL\) is idempotent.

Let \(A\) be a set and \(x \in \lists{A}\). Then \(\dedupeL(\dedupeL(x)) = \dedupeL(x)\).

Note that \(\unique(\dedupeL(x)) = \btrue\), so that \(\dedupeL(\dedupeL(x)) = \dedupeL(x)\) as claimed.

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

\(\dedupeL\) interacts with \(\snoc\).

Let \(A\) be a set. For all \(a \in A\) and \(x \in \lists{A}\), we have \[\dedupeL(\snoc(a,x)) = \bif{\elt(a,x)}{\dedupeL(x)}{\snoc(a,\dedupeL(x))}.\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \dedupeL(\snoc(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \dedupeL(\cons(a,\nil)) \\ & = & \cons(a,\nil) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{\nil}{\cons(a,\nil)} \\ & = & \bif{\elt(a,\nil)}{\nil}{\cons(a,\nil)} \\ & = & \bif{\elt(a,\nil)}{\dedupeL(\nil)}{\snoc(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*} & & \dedupeL(\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \dedupeL(\cons(b,\snoc(a,x))) \\ & = & \cons(b,\delete(b)(\dedupeL(\snoc(a,x)))) \\ & = & \cons(b,\delete(b)(\bif{\elt(a,x)}{\dedupeL(x)}{\snoc(a,\dedupeL(x))})) \\ & = & \bif{\elt(a,x)}{\cons(b,\delete(b)(\dedupeL(x)))}{\cons(b,\delete(b)(\snoc(a,\dedupeL(x))))} \\ & = & \bif{\elt(a,x)}{\dedupeL(\cons(b,x))}{\cons(b,\delete(b)(\snoc(a,\dedupeL(x))))} \\ & = & \bif{\elt(a,x)}{\dedupeL(\cons(b,x))}{\cons(b,\bif{\beq(a,b)}{\delete(b)(\dedupeL(x))}{\snoc(a,\delete(b)(\dedupeL(x)))})} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \bif{\elt(a,x)}{\dedupeL(\cons(b,x))}{\bif{\beq(a,b)}{\cons(b,\delete(b)(\dedupeL(x)))}{\cons(b,\snoc(a,\delete(b)(\dedupeL(x))))}} \\ & = & \bif{\elt(a,x)}{\dedupeL(\cons(b,x))}{\bif{\beq(a,b)}{\dedupeL(\cons(b,x))}{\cons(b,\snoc(a,\delete(b)(\dedupeL(x))))}} \\ & = & \bif{\bor(\beq(a,b),\elt(a,x))}{\dedupeL(\cons(b,x))}{\cons(b,\snoc(a,\delete(b)(\dedupeL(x))))} \\ & = & \bif{\elt(a,\cons(b,x))}{\dedupeL(\cons(b,x))}{\cons(b,\snoc(a,\delete(b)(\dedupeL(x))))} \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \bif{\elt(a,\cons(b,x))}{\dedupeL(\cons(b,x))}{\snoc(a,\cons(b,\delete(b)(\dedupeL(x))))} \\ & = & \bif{\elt(a,\cons(b,x))}{\dedupeL(\cons(b,x))}{\snoc(a,\dedupeL(\cons(b,x)))} \end{eqnarray*}\] as needed.

_test_dedupeL_snoc :: (List t, Equal a, Equal (t a))
  => t a -> Test (a -> t a -> Bool)
_test_dedupeL_snoc _ =
  testName "dedupeL(snoc(a,x)) == if(elt(a,x),dedupeL(x),snoc(a,dedupeL(x)))" $
  \a x -> eq
    (dedupeL (snoc a x))
    (if elt a x then dedupeL x else snoc a (dedupeL x))

\(\dedupeL\) interacts with \(\elt\).

Let \(A\) be a set. For all \(a \in A\) and \(x \in \lists{A}\), we have \[\elt(a,\dedupeL(x)) = \elt(a,x).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \elt(a,\dedupeL(\nil)) \\ & = & \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*} & & \elt(a,\dedupeL(\cons(b,x))) \\ & = & \elt(a,\cons(b,\delete(b)(\dedupeL(x)))) \\ & \href{/posts/arithmetic-made-difficult/Elt.html#cor-elt-cons} = & \bif{\beq(a,b)}{\btrue}{\elt(a,\delete(b)(\dedupeL(x)))} \\ & = & \bif{\beq(a,b)}{\btrue}{\bif{\beq(a,b)}{\bfalse}{\elt(a,\dedupeL(x))}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-prune-false} = & \bif{\beq(a,b)}{\btrue}{\elt(a,\dedupeL(x))} \\ & = & \bif{\beq(a,b)}{\btrue}{\elt(a,x)} \\ & \href{/posts/arithmetic-made-difficult/Elt.html#cor-elt-cons} = & \elt(a,\cons(b,x)) \end{eqnarray*}\] as needed.

_test_dedupeL_elt :: (List t, Equal a, Equal (t a))
  => t a -> Test (a -> t a -> Bool)
_test_dedupeL_elt _ =
  testName "elt(a,dedupeL(x)) == elt(a,x)" $
  \a x -> eq (elt a (dedupeL x)) (elt a x)

\(\dedupeL\) commutes with \(\filter\).

Let \(A\) be a set with \(p : A \rightarrow \bool\) a predicate. For all \(x \in \lists{A}\), we have \[\dedupeL(\filter(p)(x)) = \filter(p)(\dedupeL(x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \dedupeL(\filter(p)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \dedupeL(\nil) \\ & = & \nil \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \filter(p)(\nil) \\ & = & \filter(p)(\dedupeL(\nil)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equation holds for some \(x\) and let \(a \in A\). We consider the two possibilities for \(p(a)\). If \(p(a) = \btrue\), we have \[\begin{eqnarray*} & & \filter(p)(\dedupeL(\cons(a,x))) \\ & = & \filter(p)(\cons(a,\delete(a)(\dedupeL(x)))) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-cons} = & \bif{p(a)}{\cons(a,\filter(p)(\delete(a)(\dedupeL(x))))}{\filter(p)(\delete(a)(\dedupeL(x)))} \\ & = & \bif{\btrue}{\cons(a,\filter(p)(\delete(a)(\dedupeL(x))))}{\filter(p)(\delete(a)(\dedupeL(x)))} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \cons(a,\filter(p)(\delete(a)(\dedupeL(x)))) \\ & = & \cons(a,\delete(a)(\filter(a)(\dedupeL(x)))) \\ & = & \cons(a,\delete(a)(\dedupeL(\filter(p)(x)))) \\ & = & \dedupeL(\cons(a,\filter(p)(x))) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \dedupeL(\bif{\btrue}{\cons(a,\filter(p)(x))}{\filter(p)(x)}) \\ & = & \dedupeL(\filter(p)(\cons(a,x))) \end{eqnarray*}\] as needed. If \(p(a) = \bfalse\), we have \[\begin{eqnarray*} & & \filter(p)(\dedupeL(\cons(a,x))) \\ & = & \filter(p)(\cons(a,\delete(a)(\dedupeL(x)))) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-cons} = & \bif{p(a)}{\cons(a,\filter(p)(\delete(a)(\dedupeL(x))))}{\filter(p)(\delete(a)(\dedupeL(x)))} \\ & = & \bif{\bfalse}{\cons(a,\filter(p)(\delete(a)(\dedupeL(x))))}{\filter(p)(\delete(a)(\dedupeL(x)))} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \filter(p)(\delete(a)(\dedupeL(x))) \\ & = & \delete(a)(\filter(p)(\dedupeL(x))) \\ & = & \filter(p)(\dedupeL(x)) \\ & = & \dedupeL(\filter(p)(x)) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \dedupeL(\bif{\bfalse}{\cons(a,\filter(p)(x))}{\filter(p)(x)}) \\ & = & \dedupeL(\bif{p(a)}{\cons(a,\filter(p)(x))}{\filter(p)(x)}) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-cons} = & \dedupeL(\filter(p)(\cons(a,x))) \end{eqnarray*}\] as needed.

_test_dedupeL_filter :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_dedupeL_filter _ =
  testName "dedupeL(filter(p)(x)) == filter(p)(dedupeL(x))" $
  \p x -> eq (dedupeL (filter p x)) (filter p (dedupeL x))

We define \(\dedupeR\) in terms of \(\dedupeL\).

Let \(A\) be a set. Define \(\dedupeL : \lists{A} \rightarrow \lists{A}\) by \[\dedupeL(x) = \rev(\dedupeR(\rev(x))).\]

In Haskell:

dedupeR :: (List t, Equal a) => t a -> t a
dedupeR = rev . dedupeL . rev

The defining equations for \(\dedupeL\) have equivalents for \(\dedupeR\).

Let \(A\) be a set. For all \(a \in A\) and \(x \in \lists{A}\) we have the following.

\(\dedupeR(\nil) = \nil\).
\(\dedupeR(\snoc(a,x)) = \snoc(a,\delete(a,\dedupeR(x)))\).

Note that \[\begin{eqnarray*} & & \dedupeR(\nil) \\ & = & \rev(\dedupeL(\rev(\nil))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \rev(\dedupeL(\nil)) \\ & = & \rev(\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \nil \end{eqnarray*}\] as needed.
Note that \[\begin{eqnarray*} & & \dedupeR(\snoc(a,x)) \\ & = & \rev(\dedupeL(\rev(\snoc(a,x)))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-snoc} = & \rev(\dedupeL(\cons(a,\rev(x)))) \\ & = & \rev(\cons(a,\delete(a,\dedupeL(\rev(x))))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \snoc(a,\rev(\delete(a,\dedupeL(\rev(x))))) \\ & = & \snoc(a,\delete(a,\rev(\dedupeL(\rev(x))))) \\ & = & \snoc(a,\delete(a,\dedupeR(x))) \end{eqnarray*}\] as claimed.

_test_dedupeR_nil :: (List t, Equal a, Equal (t a))
  => t a -> Test Bool
_test_dedupeR_nil t =
  testName "dedupeR(nil) == nil" $
  eq (dedupeR nil) (nil `withTypeOf` t)


_test_dedupeR_snoc :: (List t, Equal a, Equal (t a))
  => t a -> Test (a -> t a -> Bool)
_test_dedupeR_snoc _ =
  testName "dedupeR(snoc(a,x)) == snoc(a,delete(a)(dedupeR(x)))" $
  \a x -> eq (dedupeR (snoc a x)) (snoc a (delete a (dedupeR x)))

\(\dedupeR\)s are unique.

Let \(A\) be a set with \(x \in \lists{A}\). Then \(\unique(\dedupeR(x)) = \btrue\).

Note that \[\begin{eqnarray*} & & \unique(\dedupeR(x)) \\ & = & \unique(\rev(\dedupeL(\rev(x)))) \\ & \href{/posts/arithmetic-made-difficult/Unique.html#thm-unique-rev} = & \unique(\dedupeL(\rev(x))) \\ & = & \btrue \end{eqnarray*}\] as claimed.

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

\(\dedupeR\) is idempotent.

Let \(A\) be a set with \(x \in \lists{A}\). Then \(\dedupeR(\dedupeR(x)) = \dedupeR(x)\).

Note that \[\begin{eqnarray*} & & \dedupeR \circ \dedupeR \\ & = & \rev \circ \dedupeL \circ \rev \circ \rev \circ \dedupeL \circ \rev \\ & = & \rev \circ \dedupeL \circ \dedupeL \circ \rev \\ & = & \rev \circ \dedupeL \circ \rev \\ & = & \dedupeR \end{eqnarray*}\] as claimed.

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

Testing

Suite:

_test_dedupe ::
  ( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
  , TypeName (t a), List t
  , Equal (t a), Show (t a), Arbitrary (t a), Equal (t (t a))
  ) => Int -> Int -> t a -> IO ()
_test_dedupe size cases t = do
  testLabel1 "dedupeL & dedupeR" t

  let args = testArgs size cases

  runTest args (_test_dedupeL_nil t)
  runTest args (_test_dedupeL_cons t)
  runTest args (_test_dedupeL_delete t)
  runTest args (_test_dedupeL_unique t)
  runTest args (_test_dedupeL_prefix t)
  runTest args (_test_dedupeL_eq_unique t)
  runTest args (_test_dedupeL_idempotent t)
  runTest args (_test_dedupeL_snoc t)
  runTest args (_test_dedupeL_elt t)
  runTest args (_test_dedupeL_filter t)

  runTest args (_test_dedupeR_nil t)
  runTest args (_test_dedupeR_snoc t)
  runTest args (_test_dedupeR_unique t)
  runTest args (_test_dedupeR_idempotent t)

Main:

main_dedupe :: IO ()
main_dedupe = do
  _test_dedupe 50 500 (nil :: ConsList Bool)
  _test_dedupe 50 500 (nil :: ConsList Unary)