---
title: Delete
author: nbloomf
date: 2017-05-27
tags: arithmetic-made-difficult, literate-haskell
slug: delete
---

> {-# 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$.

:::::: definition ::
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.

:::::: corollary :::
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 :::::::::::

> _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.

:::::: theorem :::::
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).$$

::: proof ::::::::::
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{@not@#thm-ifnot}
   = & \bif{\beq(a,b)}{\delete(a)(x)}{\cons(b,\delete(a)(x))} \\
 & = & \delete(a)(\cons(b,x))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _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$.

:::::: corollary :::
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 :::::::::::

> _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$.

:::::: theorem :::::
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).$$

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, we have
$$\begin{eqnarray*}
 &   & \delete(a)(\filter(p)(\nil)) \\
 &     \href{@filter@#cor-filter-nil}
   = & \delete(a)(\nil) \\
 & = & \nil \\
 &     \href{@filter@#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 $\bfalse. Now
$$\begin{eqnarray*}
 &   & \delete(a)(\filter(p)(\cons(b,x))) \\
 &     \href{@filter@#cor-filter-cons}
   = & \delete(a)(\bif{p(b)}{\cons(b,\filter(p)(x))}{\filter(p)(x)}) \\
 &     \href{@booleans@#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{@booleans@#cor-if-false}
   = & \bif{p(b)}{\cons(b,\filter(p)(x))}{\filter(p)(x)} \\
 & = & \filter(p)(\cons(b,x))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _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.

:::::: theorem :::::
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).$$

::: proof ::::::::::
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 :::::::::::

> _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$.

:::::: theorem :::::
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)).$$

::: proof ::::::::::
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 :::::::::::

> _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.

:::::: theorem :::::
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)).$$

::: proof ::::::::::
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 :::::::::::

> _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.

:::::: theorem :::::
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.$$

::: proof ::::::::::
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 :::::::::::

> _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.

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

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

::: test :::::::::::

> _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$.

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

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

::: test :::::::::::

> _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$.

:::::: theorem :::::
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)}$.

::: proof ::::::::::
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{@elt@#cor-elt-nil}
   = & \bfalse \\
 &     \href{@booleans@#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{@elt@#cor-elt-cons}
   = & \bif{\beq(a,c)}{\btrue}{\elt(a,\delete(b,x))} \\
 & = & \btrue \\
 & = & \bif{\beq(a,c)}{\btrue}{\elt(a,x)} \\
 &     \href{@elt@#cor-elt-cons}
   = & \elt(a,\cons(c,x)) \\
 &     \href{@booleans@#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 :::::::::::

> _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$.

:::::: theorem :::::
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$.

::: proof ::::::::::
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{@prefix-suffix@#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 :::::::::::

> _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$.

:::::: theorem :::::
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))}.$$

::: proof ::::::::::
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{@snoc@#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{@snoc@#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{@snoc@#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{@booleans@#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{@booleans@#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{@booleans@#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 :::::::::::

> _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$.

:::::: theorem :::::
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)).$$

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, note that
$$\begin{eqnarray*}
 &   & \delete(a,\rev(\nil)) \\
 &     \href{@rev@#cor-rev-nil}
   = & \delete(a,\nil) \\
 & = & \nil \\
 &     \href{@rev@#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{@rev@#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{@rev@#cor-rev-cons}
   = & \bif{\beq(a,b)}{\rev(\delete(a,x))}{\rev(\cons(b,\delete(a,x)))} \\
 &     \href{@booleans@#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 :::::::::::

> _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$.

:::::: theorem :::::
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)).$$

::: proof ::::::::::
We proceed by list induction on $y$. For the base case $y = \nil$, we have
$$\begin{eqnarray*}
 &   & \delete(a)(\cat(x,\nil)) \\
 &     \href{@cat@#thm-cat-nil-right}
   = & \delete(a)(x) \\
 &     \href{@cat@#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{@cat@#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{@cat@#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{@booleans@#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 :::::::::::

> _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)