Delete

Posted on 2017-05-27 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 Delete
  ( delete, _test_delete, main_delete
  ) where

import Testing
import Booleans
import Not
import NaturalNumbers
import Lists
import Snoc
import Reverse
import Cat
import PrefixAndSuffix
import AllAndAny
import Filter
import Elt
import Sublist
import Unique

Today we’ll establish a function $\delete$ that removes all copies of a given item from a list. $\delete$ is a special case of $\filter$.

Let $A$ be a set, with $a \in A$. Define $\varphi : A \times \lists{A} \rightarrow \lists{A}$ by \[\varphi(b,x) = \bif{\beq(a,b)}{x}{\cons(b,x)},\] and define $\delete : A \rightarrow \lists{A}^{\lists{A}}$ by \[\delete(a) = \foldr(\nil)(\varphi).\]

In Haskell:

delete :: (List t, Equal a) => a -> t a -> t a
delete a = foldr nil phi
  where
    phi b x = if eq a b then x else cons b x

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

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

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


_test_delete_cons :: (List t, Equal a, Equal (t a))
  => t a -> Test (a -> a -> t a -> Bool)
_test_delete_cons _ =
  testName "delete(a)(cons(b,x)) == if(eq(a,b),delete(a)(x),cons(b,delete(a)(x)))" $
  \a b x -> eq
    (delete a (cons b x))
    (if eq a b then delete a x else cons b (delete a x))

$\delete$ is a filter.

Let $A$ be a set. For all $a \in A$ and $x \in \lists{A}$, we have \[\delete(a)(x) = \filter(\bnot(\beq(a,-)))(x).\]

We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \filter(\bnot(\beq(a,-)))(\nil) \\ & = & \nil \\ & = & \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$. Now \[\begin{eqnarray*} & & \filter(\bnot(\beq(a,-)))(\cons(b,x)) \\ & = & \bif{\bnot(\beq(a,b))}{\cons(b,\filter(\bnot(\beq(a,-)))(x))}{\filter(\bnot(\beq(a,-)))(x)} \\ & = & \bif{\bnot(\beq(a,b))}{\cons(b,\delete(a)(x))}{\delete(a)(x)} \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-ifnot} = & \bif{\beq(a,b)}{\delete(a)(x)}{\cons(b,\delete(a)(x))} \\ & = & \delete(a)(\cons(b,x)) \end{eqnarray*}\] as needed.

_test_delete_filter :: (List t, Equal a, Equal (t a))
  => t a -> Test (a -> t a -> Bool)
_test_delete_filter _ =
  testName "delete(a)(x) == filter(not(eq(a,-)))(x)" $
  \a x -> eq (delete a x) (filter (\b -> not (eq a b)) x)

So $\delete$ commutes with $\filter$.

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

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

And if $p(a) = \bfalse$, then $\filter(p)$ absorbs $\delete$.

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

We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \delete(a)(\filter(p)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \delete(a)(\nil) \\ & = & \nil \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \filter(p)(\nil) \end{eqnarray*}\] as needed. For the inductive step, suppose the equatily holds for some $x$, and let $b \in A$. Note that if $p(b) = \btrue$, then $\beq(a,b)$ must be $. Now \[\begin{eqnarray*} & & \delete(a)(\filter(p)(\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-cons} = & \delete(a)(\bif{p(b)}{\cons(b,\filter(p)(x))}{\filter(p)(x)}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \bif{p(b)}{\delete(a)(\cons(b,\filter(p)(x)))}{\delete(a)(\filter(p)(x))} \\ & = & \bif{p(b)}{\bif{\beq(a,b)}{\delete(a)(\filter(p)(x))}{\cons(b,\delete(a)(\filter(p)(x)))}}{\delete(a)(\filter(p)(x))} \\ & = & \bif{p(b)}{\bif{\beq(a,b)}{\filter(p)(x)}{\cons(b,\filter(p)(x))}}{\filter(p)(x)} \\ & = & \bif{p(b)}{\bif{\bfalse}{\filter(p)(x)}{\cons(b,\filter(p)(x))}}{\filter(p)(x)} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{p(b)}{\cons(b,\filter(p)(x))}{\filter(p)(x)} \\ & = & \filter(p)(\cons(b,x)) \end{eqnarray*}\] as needed.

_test_delete_filter_absorb :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> a -> t a -> Bool)
_test_delete_filter_absorb _ =
  testName "if p(a) == false then delete(a)(filter(p)(x)) == filter(p)(x)" $
  \p a x -> if isFalse (p a)
    then eq (delete a (filter p x)) (filter p x)
    else true

$\delete$ is idempotent.

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

Note that, since $\filter(p)$ is idempotent for any predicate $p$, we have \[\begin{eqnarray*} & & \delete(a,\delete(a,x)) \\ & = & \filter(\bnot(\beq(a,-)),\filter(\bnot(\beq(a,-)),x)) \\ & = & \filter(\bnot(\beq(a,-)),x) \\ & = & \delete(a,x) \end{eqnarray*}\] as claimed.

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

$\delete$ can detect $\elt$.

Let $A$ be a set with $a \in A$ and $x \in \lists{A}$. Then we have \[\beq(x,\delete(a,x)) = \bnot(\elt(a,x)).\]

Note that \[\begin{eqnarray*} & & \beq(x,\delete(a,x)) \\ & = & \beq(x,\filter(\bnot(\beq(a,-)),x)) \\ & = & \all(\bnot(\beq(a,-)),x) \\ & = & \bnot(\any(\beq(a,-),x)) \\ & = & \bnot(\elt(a,x)) \end{eqnarray*}\] as claimed.

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

$\delete$ commutes with itself.

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

We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \delete(a,\delete(b,\nil)) \\ & = & \delete(a,\nil) \\ & = & \nil \\ & = & \delete(b,\nil) \\ & = & \delete(b,\delete(a,\nil)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some $x$ and let $c \in A$. We consider four possibilities. If $c = a$ and $c = b$, using the inductive hypothesis we have \[\begin{eqnarray*} & & \delete(a,\delete(b,\cons(c,x))) \\ & = & \delete(a,\delete(b,x)) \\ & = & \delete(b,\delete(a,x)) \\ & = & \delete(b,\delete(a,\cons(c,x))) \end{eqnarray*}\] as needed. If $c = a$ and $c \neq b$, using the inductive hypothesis we have \[\begin{eqnarray*} & & \delete(a,\delete(b,\cons(c,x))) \\ & = & \delete(a,\cons(c,\delete(b,x))) \\ & = & \delete(a,\delete(b,x)) \\ & = & \delete(b,\delete(a,x)) \\ & = & \delete(b,\delete(a,\cons(c,x))) \end{eqnarray*}\] as needed. If $c \neq a$ and $c = b$, using the inductive hypothesis we have \[\begin{eqnarray*} & & \delete(a,\delete(b,\cons(c,x))) \\ & = & \delete(a,\delete(b,x)) \\ & = & \delete(b,\delete(a,x)) \\ & = & \delete(b,\cons(c,\delete(a,x))) \\ & = & \delete(b,\delete(a,\cons(c,x))) \end{eqnarray*}\] as needed. Finally, if $c \neq a$ and $c \neq b$, using the inductive hypothesis we have \[\begin{eqnarray*} & & \delete(a,\delete(b,\cons(c,x))) \\ & = & \delete(a,\cons(c,\delete(b,x))) \\ & = & \cons(c,\delete(a,\delete(b,x))) \\ & = & \cons(c,\delete(b,\delete(a,x))) \\ & = & \delete(b,\cons(c,\delete(a,x))) \\ & = & \delete(b,\delete(a,\cons(c,x))) \end{eqnarray*}\] as needed.

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

$\delete$ removes elements.

Let $A$ be a set. For all $x \in \lists{A}$ and $a \in A$, we have \[\all(\bnot(\beq(a,-)))(\delete(a,x)) = \btrue.\]

Note that \[\begin{eqnarray*} & & \btrue \\ & = & \all(\bnot(\beq(a,-)),\filter(\bnot(\beq(a,-)),x)) \\ & = & \all(\bnot(\beq(a,-)),\delete(a,x)) \end{eqnarray*}\] as claimed.

_test_delete_all_not_eq :: (List t, Equal a, Equal (t a))
  => t a -> Test (a -> t a -> Bool)
_test_delete_all_not_eq _ =
  testName "all(not(eq(a,-)))(delete(a)(x))" $
  \a x -> all (\b -> not (eq a b)) (delete a x)

$\delete$ yields a sublist.

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

Note that \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\filter(\bnot(\beq(a,-)),x),x) \\ & = & \sublist(\delete(a,x),x) \end{eqnarray*}\] as claimed.

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

$\delete$ and $\unique$.

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

Note that $\sublist(\delete(a)(x),x) = \btrue$, so that $\unique(\delete(a)(x)) = \btrue$ as claimed.

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

$\delete$ interacts with $\elt$.

Let $A$ be a set with $x \in \lists{A}$ and $a,b \in A$. Then $$\elt(a,\delete(b,x)) = \bif{\beq(a,b)}{\bfalse}{\elt(a,x)}$.

We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \elt(a,\delete(b,\nil)) \\ & = & \elt(a,\nil) \\ & \href{/posts/arithmetic-made-difficult/Elt.html#cor-elt-nil} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \bif{\beq(a,b)}{\bfalse}{\bfalse} \\ & = & \bif{\beq(a,b)}{\bfalse}{\elt(a,\nil)} \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all $a$ and $b$ for some $x$ and let $c \in A$. If $b = c$ and $a \neq c$, we have \[\begin{eqnarray*} & & \elt(a,\delete(b,\cons(c,x))) \\ & = & \elt(a,\delete(b,x)) \\ & = & \bif{\beq(a,b)}{\bfalse}{\elt(a,x)} \\ & = & \bif{\beq(a,b)}{\bfalse}{\elt(a,\cons(c,x))}. \end{eqnarray*}\] If $b = c$ and $a = c$, then \[\begin{eqnarray*} & & \elt(a,\delete(b,\cons(c,x))) \\ & = & \elt(a,\delete(b,x)) \\ & = & \bif{\beq(a,b)}{\bfalse}{\elt(a,x)} \\ & = & \bfalse \\ & = & \bif{\beq(a,b)}{\bfalse}{\elt(a,\cons(c,x))}. \end{eqnarray*}\] Suppose then that $b \neq c$. If $a = c$, then $a \neq b$, and we have \[\begin{eqnarray*} & & \elt(a,\delete(b,\cons(c,x))) \\ & = & \elt(a,\cons(c,\delete(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Elt.html#cor-elt-cons} = & \bif{\beq(a,c)}{\btrue}{\elt(a,\delete(b,x))} \\ & = & \btrue \\ & = & \bif{\beq(a,c)}{\btrue}{\elt(a,x)} \\ & \href{/posts/arithmetic-made-difficult/Elt.html#cor-elt-cons} = & \elt(a,\cons(c,x)) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{\bfalse}{\elt(a,\cons(c,x))} \\ & = & \bif{\beq(a,b)}{\bfalse}{\elt(a,\cons(c,x))}. \end{eqnarray*}\] If $b \neq c$ and $a \neq c$, we have \[\begin{eqnarray*} & & \elt(a,\delete(b,\cons(c,x))) \\ & = & \elt(a,\cons(c,\delete(b,x))) \\ & = & \elt(a,\delete(b,x)) \\ & = & \bif{\beq(a,b)}{\bfalse}{\elt(a,x)} \\ & = & \bif{\beq(a,b)}{\bfalse}{\elt(a,\cons(c,x))} \end{eqnarray*}\] as needed.

_test_delete_elt :: (List t, Equal a, Equal (t a))
  => t a -> Test (a -> a -> t a -> Bool)
_test_delete_elt _ =
  testName "elt(a,delete(b)(x)) == if(eq(a,b),false,elt(a,x))" $
  \a b x -> eq
    (elt a (delete b x))
    (if eq a b then false else elt a x)

$\delete$ preserves $\prefix$.

Let $A$ be a set with $x,y \in \lists{A}$ and $a \in A$. If $\prefix(x,y) = \btrue$, then $\prefix(\delete(a)(x),\delete(a)(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(\delete(a,x),\delete(a,y)) \\ & = & \prefix(\delete(a,\nil),\delete(a,y)) \\ & = & \prefix(\nil,\delete(a,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 $a$ and $y$ for some $x$ and let $b \in A$. Suppose further that $\prefix(\cons(b,x),y) = \btrue$. Now we must have $y = \cons(b,u)$ for some $u$ with $\prefix(x,u) = \btrue$. We consider two possibilities. If $a = b$, we have \[\begin{eqnarray*} & & \prefix(\delete(a,\cons(b,x)),\delete(a,y)) \\ & = & \prefix(\delete(a,\cons(b,x)),\delete(a,\cons(b,u))) \\ & = & \prefix(\delete(a,x),\delete(a,u)) \\ & = & \btrue \end{eqnarray*}\] as needed. Suppose instead that $a \neq b$; again by the inductive hypothesis we have \[\begin{eqnarray*} & & \prefix(\delete(a,\cons(b,x)),\delete(a,y)) \\ & = & \prefix(\delete(a,\cons(b,x)),\delete(a,\cons(b,u))) \\ & = & \prefix(\cons(b,\delete(a,x)),\cons(b,\delete(a,u))) \\ & = & \prefix(\delete(a,x),\delete(a,u)) \\ & = & \btrue \end{eqnarray*}\] as needed.

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

$\delete$ interacts with $\snoc$.

Let $A$ be a set with $a,b \in A$ and $x \in \lists{A}$. Then we have \[\delete(a,\snoc(b,x)) = \bif{\beq(a,b)}{\delete(a,x)}{\snoc(b,\delete(a,x))}.\]

We proceed by list induction on $x$. For the base case $x = \nil$, note that \[\begin{eqnarray*} & & \delete(a,\snoc(b,x)) \\ & = & \delete(a,\snoc(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \delete(a,\cons(b,\nil)) \\ & = & \bif{\beq(a,b)}{\delete(a,\nil)}{\cons(b,\delete(a,\nil))} \\ & = & \bif{\beq(a,b)}{\delete(a,\nil)}{\cons(b,\nil)} \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \bif{\beq(a,b)}{\delete(a,\nil)}{\snoc(b,\nil)} \\ & = & \bif{\beq(a,b)}{\delete(a,\nil)}{\snoc(b,\delete(a,\nil))} \\ & = & \bif{\beq(a,b)}{\delete(a,x)}{\snoc(b,\delete(a,x))} \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all $a$ and $b$ for some $x$ and let $c \in A$. Using the inductive hypothesis, we have \[\begin{eqnarray*} & & \delete(a,\snoc(b,\cons(c,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \delete(a,\cons(c,\snoc(b,x))) \\ & = & \bif{\beq(a,c)}{\delete(a,\snoc(b,x))}{\cons(c,\delete(a,\snoc(b,x)))} \\ & = & \bif{\beq(a,c)}{\bif{\beq(a,b)}{\delete(a,x)}{\snoc(b,\delete(a,x))}}{\cons(c,\bif{\beq(a,b)}{\delete(a,x)}{\snoc(b,\delete(a,x))})} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \bif{\beq(a,c)}{\bif{\beq(a,b)}{\delete(a,x)}{\snoc(b,\delete(a,x))}}{\bif{\beq(a,b)}{\cons(c,\delete(a,x))}{\cons(c,\snoc(b,\delete(a,x)))}} \\ & = & \bif{\beq(a,c)}{\bif{\beq(a,b)}{\delete(a,x)}{\snoc(b,\delete(a,x))}}{\bif{\beq(a,b)}{\cons(c,\delete(a,x))}{\snoc(b,\cons(c,\delete(a,x)))}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-ifnest} = & \bif{\beq(a,b)}{\bif{\beq(a,c)}{\delete(a,x)}{\cons(c,\delete(a,x))}}{\bif{\beq(a,c)}{\snoc(b,\delete(a,x))}{\snoc(b,\cons(c,\delete(a,x)))}} \\ & = & \bif{\beq(a,b)}{\delete(a,\cons(c,x))}{\bif{\beq(a,c)}{\snoc(b,\delete(a,x))}{\snoc(b,\cons(c,\delete(a,x)))}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \bif{\beq(a,b)}{\delete(a,\cons(c,x))}{\snoc(b,\bif{\beq(a,c)}{\delete(a,x)}{\cons(c,\delete(a,x))})} \\ & = & \bif{\beq(a,b)}{\delete(a,\cons(c,x))}{\snoc(b,\delete(a,\cons(c,x)))} \end{eqnarray*}\] as needed.

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

$\delete$ commutes with $\rev$.

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

We proceed by list induction on $x$. For the base case $x = \nil$, note that \[\begin{eqnarray*} & & \delete(a,\rev(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \delete(a,\nil) \\ & = & \nil \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \rev(\nil) \\ & = & \rev(\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$. Using the inductive hypothesis, we have \[\begin{eqnarray*} & & \delete(a,\rev(\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \delete(a,\snoc(b,\rev(x))) \\ & = & \bif{\beq(a,b)}{\delete(a,\rev(x))}{\snoc(b,\delete(a,\rev(x)))} \\ & = & \bif{\beq(a,b)}{\rev(\delete(a,x))}{\snoc(b,\rev(\delete(a,x)))} \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \bif{\beq(a,b)}{\rev(\delete(a,x))}{\rev(\cons(b,\delete(a,x)))} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \rev(\bif{\beq(a,b)}{\delete(a,x)}{\cons(b,\delete(a,x))}) \\ & = & \rev(\delete(a,\cons(b,x))) \end{eqnarray*}\] as needed.

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

$\delete$ distributes over $\cat$.

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

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

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

Testing

Suite:

_test_delete ::
  ( 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_delete size cases t = do
  testLabel1 "delete" t

  let args = testArgs size cases

  runTest args (_test_delete_nil t)
  runTest args (_test_delete_cons t)
  runTest args (_test_delete_filter t)
  runTest args (_test_delete_filter_commute t)
  runTest args (_test_delete_filter_absorb t)
  runTest args (_test_delete_idempotent t)
  runTest args (_test_delete_eq_not_elt t)
  runTest args (_test_delete_commutative t)
  runTest args (_test_delete_all_not_eq t)
  runTest args (_test_delete_sublist t)
  runTest args (_test_delete_unique t)
  runTest args (_test_delete_elt t)
  runTest args (_test_delete_prefix t)
  runTest args (_test_delete_snoc t)
  runTest args (_test_delete_rev t)
  runTest args (_test_delete_cat t)

Main:

main_delete :: IO ()
main_delete = do
  _test_delete 20 100 (nil :: ConsList Bool)
  _test_delete 20 100 (nil :: ConsList Unary)