Common

Posted on 2018-01-21 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 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).\]

In Haskell:

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)