# Common

Posted on 2018-01-21 by nbloomf

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

{-# LANGUAGE NoImplicitPrelude #-}
module Common (
common, _test_common, main_common
) where

import Testing
import And
import Unary
import Lists
import Snoc
import Reverse
import Cat
import Filter
import Elt
import Sublist
import Dedupe

Today we’ll define a map, $$\common(x,y)$$, that deletes from $$x$$ any items that don’t also appear in $$y$$. This doesn’t require explicit recursion.

Let $$A$$ be a set. We define $$\common : \lists{A} \times \lists{A}$$ by $\common(x,y) = \filter(\elt(-,y))(x).$

common :: (List t, Equal a) => t a -> t a -> t a
common x y = filter (\a -> elt a y) x

Because $$\filter$$ is the unique solution to a system of equations, so is $$\common$$.

Let $$A$$ be a set. Then $$\common$$ is the unique map $$f : \lists{A} \times \lists{A} \rightarrow \lists{A}$$ satisfying the following equations for all $$a \in A$$ and $$x,y \in \lists{A}$$. $\left\{\begin{array}{l} f(\nil,y) = \nil \\ f(\cons(a,x),y) = \bif{\elt(a,y)}{\cons(a,f(x,y))}{f(x,y)} \end{array}\right.$

_test_common_nil :: (List t, Equal a, Equal (t a))
=> t a -> Test (t a -> Bool)
_test_common_nil _ =
testName "common(nil,y) == nil" $\y -> eq (common nil y) nil _test_common_cons :: (List t, Equal a, Equal (t a)) => t a -> Test (a -> t a -> t a -> Bool) _test_common_cons _ = testName "common(cons(a,x),y) == if(elt(a,y),cons(a,common(x,y)),common(x,y))"$
\a x y -> eq
(common (cons a x) y)
(if elt a y then cons a (common x y) else common x y)

$$\common$$ interacts with $$\cat$$.

Let $$A$$ be a set. For all $$x,y,z \in \lists{A}$$ we have $\common(\cat(x,y),z) = \cat(\common(x,z),\common(y,z)).$

Note that $\begin{eqnarray*} & & \common(\cat(x,y),z) \\ & = & \filter(\elt(-,z))(\cat(x,y)) \\ & = & \cat(\filter(\elt(-,z))(x),\filter(\elt(-,z))(y)) \\ & = & \cat(\common(x,z),\common(y,z)) \end{eqnarray*}$ as claimed.

_test_common_cat_left :: (List t, Equal a, Equal (t a))
=> t a -> Test (t a -> t a -> t a -> Bool)
_test_common_cat_left _ =
testName "common(cat(x,y),z) == cat(common(x,z),common(y,z))" $\x y z -> eq (common (cat x y) z) (cat (common x z) (common y z)) $$\common$$ interacts with $$\rev$$ in the first argument. Let $$A$$ be a set. For all $$x,y \in \lists{A}$$ we have $\common(\rev(x),y) = \rev(\common(x,y)).$ We have $\begin{eqnarray*} & & \common(\rev(x),y) \\ & = & \filter(\elt(-,y))(\rev(x)) \\ & = & \rev(\filter(\elt(-,y))(x)) \\ & = & \rev(\common(x,y)) \end{eqnarray*}$ as claimed. _test_common_rev_left :: (List t, Equal a, Equal (t a)) => t a -> Test (t a -> t a -> Bool) _test_common_rev_left _ = testName "common(rev(x),y) == rev(common(x,y))"$
\x y -> eq
(common (rev x) y)
(rev (common x y))

$$\common$$ interacts with $$\rev$$ in the second argument.

Let $$A$$ be a set. For all $$x,y \in \lists{A}$$ we have $\common(x,\rev(y)) = \common(x,y).$

We have $\begin{eqnarray*} & & \common(x,\rev(y)) \\ & = & \filter(\elt(-,\rev(y)))(x) \\ & = & \filter(\elt(-,y))(x) \\ & = & \common(x,y) \end{eqnarray*}$ as claimed.

_test_common_rev_right :: (List t, Equal a, Equal (t a))
=> t a -> Test (t a -> t a -> Bool)
_test_common_rev_right _ =
testName "common(x,rev(y)) == common(x,y)" $\x y -> eq (common x (rev y)) (common x y) $$\common$$ interacts with $$\dedupeL$$ in the second argument. Let $$A$$ be a set. For all $$x,y \in \lists{A}$$, we have $\common(x,\dedupeL(y)) = \common(x,y).$ We have $\begin{eqnarray*} & & \common(x,\dedupeL(y)) \\ & = & \filter(\elt(-,\dedupeL(y)))(x) \\ & = & \filter(\elt(-,y))(x) \\ & = & \common(x,y) \end{eqnarray*}$ as claimed. _test_common_dedupeL_right :: (List t, Equal a, Equal (t a)) => t a -> Test (t a -> t a -> Bool) _test_common_dedupeL_right _ = testName "common(x,dedupeL(y)) == common(x,y)"$
\x y -> eq
(common x (dedupeL y))
(common x y)

$$\common$$ interacts with $$\dedupeL$$ in the left argument.

Let $$A$$ be a set. For all $$x,y \in \lists{A}$$, we have $\common(\dedupeL(x),y) = \dedupeL(\common(x,y)).$

Note that $\begin{eqnarray*} & & \common(\dedupeL(x),y) \\ & = & \filter(\elt(-,y))(\dedupeL(x)) \\ & = & \dedupeL(\filter(\elt(-,y))(x)) \\ & = & \dedupeL(\common(x,y)) \end{eqnarray*}$ as claimed.

_test_common_dedupeL_left :: (List t, Equal a, Equal (t a))
=> t a -> Test (t a -> t a -> Bool)
_test_common_dedupeL_left _ =
testName "common(dedupeL(x),y) == dedupeL(common(x,y))" $\x y -> eq (common (dedupeL x) y) (dedupeL (common x y)) $$\common$$ interacts with $$\snoc$$. Let $$A$$ be a set. For all $$a \in A$$ and $$x,y \in \lists{A}$$ we have $\common(\snoc(a,x),y) = \bif{\elt(a,y)}{\snoc(\common(x,y))}{\common(x,y)}.$ We have $\begin{eqnarray*} & & \common(\snoc(a,x),y) \\ & = & \filter(\elt(-,y))(\snoc(a,x)) \\ & = & \bif{\elt(a,y)}{\snoc(a,\filter(\elt(-,y))(x))}{\filter(\elt(-,y))(x)} \\ & = & \bif{\elt(a,y)}{\snoc(a,\common(x,y))}{\common(x,y)} \end{eqnarray*}$ as claimed. _test_common_snoc :: (List t, Equal a, Equal (t a)) => t a -> Test (a -> t a -> t a -> Bool) _test_common_snoc _ = testName "common(snoc(a,x),y) == if(elt(a,y),snoc(a,common(x,y)),common(x,y))"$
\a x y -> eq
(common (snoc a x) y)
(if elt a y then snoc a (common x y) else common x y)

We can simplify $$\common$$ if the second argument is a singleton.

Let $$A$$ be a set. For all $$a \in A$$ and $$x \in \lists{A}$$ we have $\common(x,\cons(a,\nil)) = \filter(\beq(a,-))(x).$

Note that $\begin{eqnarray*} & & \common(x,\cons(a,\nil)) \\ & = & \filter(\elt(-,\cons(a,\nil)))(x) \\ & = & \filter(\beq(-,a))(x) \\ & = & \filter(\beq(a,-))(x) \end{eqnarray*}$ as claimed.

_test_common_singleton_right :: (List t, Equal a, Equal (t a))
=> t a -> Test (a -> t a -> Bool)
_test_common_singleton_right _ =
testName "common(x,cons(a,nil)) == filter(eq(a,-))(x)" $\a x -> eq (common x (cons a nil)) (filter (eq a) x) $$\common$$ interacts with $$\elt$$. Let $$A$$ be a set. For all $$a \in A$$ and $$x,y \in \lists{A}$$, we have $\elt(a,\common(x,y)) = \band(\elt(a,x),\elt(a,y)).$ Note that $\begin{eqnarray*} & & \elt(a,\common(x,y)) \\ & = & \elt(a,\filter(\elt(-,y))(x)) \\ & = & \band(\elt(a,y),\elt(a,x)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-commutative} = & \band(\elt(a,x),\elt(a,y)) \end{eqnarray*}$ as claimed. _test_common_elt_distribute :: (List t, Equal a, Equal (t a)) => t a -> Test (a -> t a -> t a -> Bool) _test_common_elt_distribute _ = testName "elt(a,common(x,y)) == and(elt(a,x),elt(a,y))"$
\a x y -> eq
(elt a (common x y))
(and (elt a x) (elt a y))

As a consequence, $$\common$$ is almost commutative.

Let $$A$$ be a set. For all $$a \in A$$ and $$x,y \in \lists{A}$$, we have $\elt(a,\common(x,y)) = \elt(a,\common(y,x)).$

We have $\begin{eqnarray*} & & \elt(a,\common(x,y)) \\ & = & \band(\elt(a,x),\elt(a,y)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-commutative} = & \band(\elt(a,y),\elt(a,x)) \\ & = & \elt(a,\common(y,x)) \end{eqnarray*}$ as claimed.

_test_common_elt_commutative :: (List t, Equal a, Equal (t a))
=> t a -> Test (a -> t a -> t a -> Bool)
_test_common_elt_commutative _ =
testName "elt(a,common(x,y)) == elt(a,common(y,x))" $\a x y -> eq (elt a (common x y)) (elt a (common y x)) $$\common$$ is associative. Let $$A$$ be a set. For all $$x,y,z \in \lists{A}$$, we have $\common(x,\common(y,z)) = \common(\common(x,y),z).$ We proceed by list induction on $$x$$. For the base case $$x = \nil$$ we have $\begin{eqnarray*} & & \common(\nil,\common(y,z)) \\ & = & \nil \\ & = & \common(\nil,z) \\ & = & \common(\common(\nil,y),z) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$y$$ and $$z$$ for some $$x$$ and let $$a \in A$$. Now $\begin{eqnarray*} & & \common(\cons(a,x),\common(y,z)) \\ & = & \filter(\elt(-,\common(y,z)))(\cons(a,x)) \\ & = & \bif{\elt(a,\common(y,z))}{\cons(a,\filter(\elt(-,\common(y,z)))(x))}{\filter(\elt(-,\common(y,z)))(x)} \\ & = & \bif{\elt(a,\common(y,z))}{\cons(a,\common(x,\common(y,z)))}{\common(x,\common(y,z))} \\ & = & \bif{\elt(a,\filter(\elt(-,z))(y))}{\cons(a,\common(x,\common(y,z)))}{\common(x,\common(y,z))} \\ & = & \bif{\band(\elt(a,z),\elt(a,y))}{\cons(a,\common(x,\common(y,z)))}{\common(x,\common(y,z))} \\ & = & \bif{\band(\elt(a,y),\elt(a,z))}{\cons(a,\common(\common(x,y),z))}{\common(\common(x,y),z)} \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-if-hyp} = & \bif{\elt(a,y)}{\bif{\elt(a,z)}{\cons(a,\common(\common(x,y),z))}{\common(\common(x,y),z)}}{\common(\common(x,y),z)} \\ & = & \bif{\elt(a,y)}{\bif{\elt(a,z)}{\cons(a,\filter(\elt(-,z))(\common(x,y)))}{\filter(\elt(-,z))(\common(x,y))}}{\common(\common(x,y),z)} \\ & = & \bif{\elt(a,y)}{\filter(\elt(-,z))(\cons(a,\common(x,y)))}{\common(\common(x,y),z)} \\ & = & \bif{\elt(a,y)}{\filter(\elt(-,z))(\cons(a,\common(x,y)))}{\filter(\elt(-,z))(\common(x,y))} \\ & = & \bif{\elt(a,y)}{\filter(\elt(-,z))(\cons(a,\filter(\elt(-,y))(x)))}{\filter(\elt(-,z))(\filter(\elt(-,y))(x))} \\ & = & \filter(\elt(-,z))(\bif{\elt(a,y)}{\cons(a,\filter(\elt(-,y))(x))}{\filter(\elt(-,y))(x)}) \\ & = & \filter(\elt(-,z))(\filter(\elt(-,y))(\cons(a,x))) \\ & = & \common(\filter(\elt(-,y))(\cons(a,x)),z) \\ & = & \common(\common(\cons(a,x),y),z) \end{eqnarray*}$ as needed. _test_common_associative :: (List t, Equal a, Equal (t a)) => t a -> Test (t a -> t a -> t a -> Bool) _test_common_associative _ = testName "common(x,common(y,z)) == common(common(x,y),z)"$
\x y z -> eq
(common x (common y z))
(common (common x y) z)

$$\common$$ is a sublist.

Let $$A$$ be a set. For all $$x,y \in \lists{A}$$, we have $\sublist(\common(x,y),x).$

Note that $\begin{eqnarray*} & & \sublist(\common(x,y),x) \\ & = & \sublist(\filter(\elt(-,y))(x),x) \\ & = & \btrue \end{eqnarray*}$ as claimed.

_test_common_sublist :: (List t, Equal a, Equal (t a))
=> t a -> Test (t a -> t a -> Bool)
_test_common_sublist _ =
testName "sublist(common(x,y),x)" $\x y -> sublist (common x y) x $$\common$$ interacts with $$\cat$$ in the second argument. Let $$A$$ be a set. For all $$x,y \in \lists{A}$$, we have $\common(x,\cat(y,x)) = x.$ We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \common(\nil,\cat(y,\nil)) \\ & = & \nil \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$y$$ for some $$x$$, and let $$a \in A$$. Now $\begin{eqnarray*} & & \common(\cons(a,x),\cat(y,\cons(a,x))) \\ & = & \bif{\elt(a)(\cat(y,\cons(a,x)))}{\cons(a,\common(x,\cat(y,\cons(a,x))))}{\common(x,\cat(y,\cons(a,x)))} \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \bif{\elt(a)(\cat(y,\cons(a,x)))}{\cons(a,\common(x,\cat(\snoc(a,y),x)))}{\common(x,\cat(y,\cons(a,x)))} \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \bif{\elt(a)(\cat(y,\cons(a,x)))}{\cons(a,\common(x,\cat(\snoc(a,y),x)))}{\common(x,\cat(\snoc(a,y),x))} \\ & = & \bif{\elt(a)(\cat(y,\cons(a,x)))}{\cons(a,x)}{\common(x,\cat(\snoc(a,y),x))} \\ & = & \bif{\elt(a)(\cat(y,\cons(a,x)))}{\cons(a,x)}{x} \\ & = & \bif{\btrue}{\cons(a,x)}{x} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \cons(a,x) \end{eqnarray*}$ as needed. _test_common_cat_right :: (List t, Equal a, Equal (t a)) => t a -> Test (t a -> t a -> Bool) _test_common_cat_right _ = testName "common(x,cat(y,x)) == x"$
\x y -> eq (common x (cat y x)) x

## Testing

Suite:

_test_common ::
( 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_common size cases t = do
testLabel1 "common" t

let args = testArgs size cases

runTest args (_test_common_nil t)
runTest args (_test_common_cons t)
runTest args (_test_common_cat_left t)
runTest args (_test_common_rev_left t)
runTest args (_test_common_rev_right t)
runTest args (_test_common_dedupeL_right t)
runTest args (_test_common_dedupeL_left t)
runTest args (_test_common_snoc t)
runTest args (_test_common_singleton_right t)
runTest args (_test_common_elt_distribute t)
runTest args (_test_common_elt_commutative t)
runTest args (_test_common_associative t)
runTest args (_test_common_sublist t)
runTest args (_test_common_cat_right t)

Main:

main_common :: IO ()
main_common = do
_test_common 20 100 (nil :: ConsList Bool)
_test_common 20 100 (nil :: ConsList Unary)