Cat

Posted on 2017-04-25 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 Cat
  ( cat, _test_cat, main_cat
  ) where

import Testing
import Booleans
import And
import NaturalNumbers
import Lists
import HeadAndTail
import Snoc
import Reverse

In this post we’ll consider the function that takes two lists and appends one to the “end” of the other. This function is known as $\cat$, which is short for catenate – a jargony word that means to connect in a series.

We define a map $\cat : \lists{A} \times \lists{A} \rightarrow \lists{A}$ by \[\cat(x,y) = \foldr(y)(\cons)(x).\]

In Haskell:

cat :: (List t) => t a -> t a -> t a
cat x y = foldr y cons x

Because $\cat$ is defined in terms of fold, it is the unique solution to a system of functional equations.

Let $A$ be a set. Then $\cat$ is the unique mapping $f : \lists{A} \times \lists{A} \rightarrow \lists{A}$ with the property that for all $a \in A$ and $x,y \in \lists{A}$ we have \[\left\{\begin{array}{l} f(\nil,y) = y \\ f(\cons(a,x),y) = \cons(a,f(x,y)). \end{array}\right.\]

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


_test_cat_cons_left :: (List t, Equal (t a))
  => t a -> Test (a -> t a -> t a -> Bool)
_test_cat_cons_left _ =
  testName "cat(cons(a,x),y) == cons(a,cat(x,y))" $
  \a x y -> eq (cat (cons a x) y) (cons a (cat x y))

Note that $\cat$ works a lot like $\snoc$; it marches down the list $x$ until it reaches the end, and then sticks $y$ there. In some ways, $\cat$ is like $\nplus$ for lists, and $\nil$ is the $\zero$.

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

Note that \[\begin{eqnarray*} & & \cat(x,\nil) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#def-cat} = & \foldr(\nil)(\cons)(x) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-foldr-nil-cons} = & \id(x) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & x \end{eqnarray*}\] as claimed.

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

$\cat$ interacts with $\snoc$:

Let $A$ be a set. The following hold for all $a \in A$ and $x,y \in \lists{A}$.

$\cat(\snoc(a,x),y) = \cat(x,\cons(a,y))$.
$\cat(x,\snoc(a,y)) = \snoc(a,\cat(x,y))$.

We have \[\begin{eqnarray*} & & \cat(x,\cons(a,y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#def-cat} = & \foldr(\cons(a,y))(\cons)(x) \\ & = & \foldr(y)(\cons)(\snoc(a,y)) \\ & = & \cat(x,\snoc(a,y)) \end{eqnarray*}\] as claimed.
We proceed by list induction on $y$. For the base case $y = \nil$ we have \[\begin{eqnarray*} & & \snoc(a,\cat(x,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-nil-right} = & \snoc(a,x) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#def-snoc} = & \foldr(\cons(a,\nil))(\cons)(x) \\ & = & \cat(x,\cons(a,\nil)) \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some $y \in \lists{A}$, and let $b \in A$. Now \[\begin{eqnarray*} & & \snoc(a,\cat(x,\cons(b,y))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \snoc(a,\cat(\snoc(b,x),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-right} = & \cat(\snoc(b,x),\snoc(a,y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \cat(x,\cons(b,\snoc(a,y))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \cat(x,\snoc(a,\cons(b,y))) \end{eqnarray*}\] as needed.

_test_cat_snoc_left :: (List t, Equal (t a))
  => t a -> Test (a -> t a -> t a -> Bool)
_test_cat_snoc_left _ =
  testName "cat(x,cons(a,y)) == cat(snoc(a,x),y)" $
  \a x y -> eq (cat x (cons a y)) (cat (snoc a x) y)


_test_cat_snoc_right :: (List t, Equal (t a))
  => t a -> Test (a -> t a -> t a -> Bool)
_test_cat_snoc_right _ =
  testName "snoc(a,cat(x,y)) == cat(x,snoc(a,y))" $
  \a x y -> eq (snoc a (cat x y)) (cat x (snoc a y))

We can “solve” a simple list equation.

We have $\nil = \cat(x,y)$ if and only if $x = y = \nil$.

The “only if” direction is clear. To see the “if” direction, suppose we have $x,y \in \lists{A}$ such that $\cat(x,y) = \nil$. If $x = \cons(a,u)$, then \[\begin{eqnarray*} & & \btrue \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-nil} = & \isnil(\nil) \\ & = & \isnil(\cat(x,y)) \\ & = & \isnil(\cat(\cons(a,u),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \isnil(\cons(a,\cat(u,y))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \bfalse \end{eqnarray*}\] which is absurd. Thus $x = \nil$, and we have \[\begin{eqnarray*} & & \btrue \\ & = & \isnil(\cat(\nil,y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \isnil(y) \end{eqnarray*}\] as claimed.

_test_cat_nil_nil :: (List t, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_cat_nil_nil _ =
  testName "isNil(cat(x,y)) == and(isNil(x),isNil(y))" $
  \x y -> eq (isNil (cat x y)) (and (isNil x) (isNil y))

And $\cat$ is associative.

Let $A$ be a set and $x,y,z \in \lists{A}$. Then \[\cat(\cat(x,y),z) = \cat(x,\cat(y,z)).\]

We proceed by list induction on $z$. For the base case $z = \nil$, we have \[\begin{eqnarray*} & & \cat(\cat(x,y),\nil) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-nil-right} = & \cat(x,y) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-nil-right} = & \cat(x,\cat(y,\nil)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some $z \in \lists{A}$, and let $a \in A$. Then we have \[\begin{eqnarray*} & & \cat(\cat(x,y),\cons(a,z)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \cat(\snoc(a,\cat(x,y)),z) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-right} = & \cat(\cat(x,\snoc(a,y)),z) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-associative} = & \cat(x,\cat(\snoc(a,y),z)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \cat(x,\cat(y,\cons(a,z))) \end{eqnarray*}\] as needed.

_test_cat_associative :: (List t, Equal (t a))
  => t a -> Test (t a -> t a -> t a -> Bool)
_test_cat_associative _ =
  testName "cat(cat(x,y),z) == cat(x,cat(y,z))" $
  \x y z -> eq (cat (cat x y) z) (cat x (cat y z))

And $\rev$ is antidistributive over $\cat$.

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

We proceed by list induction on $y$. For the base case $y = \nil$, we have \[\begin{eqnarray*} & & \rev(\cat(x,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-nil-right} = & \rev(x) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \cat(\nil,\rev(x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \cat(\rev(\nil),\rev(x)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some $y \in \lists{A}$ and let $a \in A$. Then we have \[\begin{eqnarray*} & & \rev(\cat(x,\cons(a,y))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \rev(\cat(\snoc(a,x),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-rev-cat-antidistribute} = & \cat(\rev(y),\rev(\snoc(a,x))) \\ & = & \cat(\rev(y),\cons(a,\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \cat(\snoc(a,\rev(y)),\rev(x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \cat(\rev(\cons(a,y)),\rev(x)) \end{eqnarray*}\] as needed.

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

Finally, $\cat$ is cancellative.

Let $A$ be a set. For all $x,y,z \in \lists{A}$ we have the following.

$\cat(z,x) = \cat(z,y)$ if and only if $x = y$.
$\cat(x,z) = \cat(y,z)$ if and only if $x = y$.

The “only if” direction is clear. For the “if” direction we proceed by list induction on $z$. For the base case $z = \nil$, suppose $\cat(z,x) = \cat(z,y)$. Then we have \[\begin{eqnarray*} & & x \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \cat(\nil,x) \\ & = & \cat(z,x) \\ & = & \cat(z,y) \\ & = & \cat(\nil,y) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & y \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for some $z$, and let $a \in A$. Now suppose we have \[\cat(\cons(a,z),x) = \cat(\cons(a,z),y).\] Then we have $\cons(a,\cat(z,x)) = \cons(a,\cat(z,y)),$$ so that \[\cat(z,x) = \cat(z,y).\] By the inductive hypothesis, $x = y$ as claimed.
The “only if” direction is clear. For the “if” direction, note that \[\begin{eqnarray*} & & \cat(\rev(z),\rev(x)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-rev-cat-antidistribute} = & \rev(\cat(x,z)) \\ & = & \rev(\cat(y,z)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-rev-cat-antidistribute} = & \cat(\rev(z),\rev(y)) \end{eqnarray*}\] By (1), we have $\rev(x) = \rev(y)$, and thus $x = y$ as claimed.

_test_cat_left_cancellative :: (List t, Equal (t a))
  => t a -> Test (t a -> t a -> t a -> Bool)
_test_cat_left_cancellative _ =
  testName "eq(cat(z,x),cat(z,y)) == eq(x,y)" $
  \x y z -> eq
    (eq (cat z x) (cat z y))
    (eq x y)


_test_cat_right_cancellative :: (List t, Equal (t a))
  => t a -> Test (t a -> t a -> t a -> Bool)
_test_cat_right_cancellative _ =
  testName "eq(cat(x,z),cat(y,z)) == eq(x,y)" $
  \x y z -> eq
    (eq (cat x z) (cat y z))
    (eq x y)

One more.

Let $A$ be a set. The following hold for all $x,u,v \in \lists{A}$.

If $x = \cat(x,v)$ then $v = \nil$.
If $x = \cat(u,x)$ then $u = \nil$.
If $x = \cat(u,\cat(x,v))$ then $u = v = \nil$.

Note that \[\begin{eqnarray*} & & \cat(x,\nil) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-nil-right} = & x \\ & = & \cat(x,v), \end{eqnarray*}\] so that $v = \nil$ by cancellation.
Note that \[\begin{eqnarray*} & & \cat(\nil,x) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & x \\ & = & \cat(u,x), \end{eqnarray*}\] so that $u = \nil$ by cancellation.
We proceed by list induction on $x$. For the base case $x = \nil$, if $x = \cat(u,\cat(x,v))$ we have \[\begin{eqnarray*} & & \nil \\ & = & x \\ & = & \cat(u,\cat(x,v)) \\ & = & \cat(u,\cat(\nil,v)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \cat(u,v) \end{eqnarray*}\] so that $v = u = \nil$ as needed. For the inductive step, suppose the implication holds for all $u$ and $v$ for some $x$, and let $a \in A$. Suppose further that $\cons(a,x) = \cat(u,\cat(\cons(a,x),v))$ for some $u$ and $v$. We consider two possibilities for $u$. If $u = \cons(b,w)$, we have \[\begin{eqnarray*} & & \cons(a,x) \\ & = & \cat(u,\cat(\cons(a,x),v)) \\ & = & \cat(\cons(b,w),\cat(\cons(a,x),v)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \cons(b,\cat(w,\cat(\cons(a,x),v))) \end{eqnarray*}\] So in fact we have $a = b$, and \[\begin{eqnarray*} & & x \\ & = & \cat(w,\cat(\cons(a,x),v)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-associative} = & \cat(\cat(w,\cons(a,x)),v) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \cat(\cat(\snoc(a,w),x),v) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-associative} = & \cat(\snoc(a,w),\cat(x,v)) \end{eqnarray*}\] By the inductive hypothesis, we have $\snoc(a,w) = \nil$, a contradiction. So we must have $u = \nil$. Now \[\begin{eqnarray*} & & \cons(a,x) \\ & = & \cat(u,\cat(\cons(a,x),v)) \\ & = & \cat(\nil,\cat(\cons(a,x),v)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \cat(\cons(a,x),v) \end{eqnarray*}\] so that $v = u = \nil$ as claimed.

_test_cat_right_identity_unique :: (List t, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_cat_right_identity_unique _ =
  testName "if eq(cat(x,v),x) then eq(v,nil)" $
  \x v -> if eq (cat x v) x then eq v nil else true


_test_cat_left_identity_unique :: (List t, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_cat_left_identity_unique _ =
  testName "if eq(cat(u,x),x) then eq(u,nil)" $
  \x u -> if eq (cat u x) x then eq u nil else true


_test_cat_nil_list_nil :: (List t, Equal (t a))
  => t a -> Test (t a -> t a -> t a -> Bool)
_test_cat_nil_list_nil _ =
  testName "if eq(cat(u,cat(x,v)),x) then and(eq(u,nil),eq(v,nil))" $
  \x u v -> if eq (cat u (cat x v)) x
    then and (eq u nil) (eq v nil)
    else true

Testing

Suite:

_test_cat ::
  ( TypeName a, Show a, Equal a, Arbitrary a
  , TypeName (t a), List t, Equal (t a), Show (t a), Arbitrary (t a)
  ) => Int -> Int -> t a -> IO ()
_test_cat size cases t = do
  testLabel1 "cat" t

  let args = testArgs size cases

  runTest args (_test_cat_nil_left t)
  runTest args (_test_cat_cons_left t)
  runTest args (_test_cat_nil_right t)
  runTest args (_test_cat_snoc_left t)
  runTest args (_test_cat_snoc_right t)
  runTest args (_test_cat_nil_nil t)
  runTest args (_test_cat_associative t)
  runTest args (_test_cat_rev t)
  runTest args (_test_cat_left_cancellative t)
  runTest args (_test_cat_right_cancellative t)
  runTest args (_test_cat_right_identity_unique t)
  runTest args (_test_cat_left_identity_unique t)
  runTest args (_test_cat_nil_list_nil t)

Main:

main_cat :: IO ()
main_cat = do
  _test_cat 20 100 (nil :: ConsList Bool)
  _test_cat 20 100 (nil :: ConsList Unary)