Filter
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 Filter
( filter, _test_filter, main_filter
) where
import Testing
import Booleans
import Tuples
import NaturalNumbers
import Lists
import Snoc
import Reverse
import Cat
import AllAndAnyToday we’ll nail down \(\filter\), which takes a list and a predicate on the items and “filters out” the items which satisfy the predicate. \(\filter\) should have a signature like \[\bool^A \times \lists{A} \rightarrow \lists{A}.\] As usual, we want to define \(\filter\) as a fold; say \[\filter(p)(x) = \foldr(\varepsilon)(\varphi)(x).\] Where on the right hand side of that equation should the \(p\) parameter go? Lets think out loud for a moment. On the one hand, we want \[\begin{eqnarray*} & & \nil \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \filter(p)(\nil) \\ & = & \foldr(\varepsilon)(\varphi)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \varepsilon \end{eqnarray*}\] On the other hand, we want \[\begin{eqnarray*} & & \filter(p)(\cons(a,x)) \\ & = & \foldr(\varepsilon)(\varphi)(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \varphi(a,\foldr(\varepsilon)(\varphi)(x)) \\ & = & \varphi(a,\filter(p)(x)). \end{eqnarray*}\] Intuitively, if \(p(a)\) is \(\btrue\) we want \[\filter(p)(\cons(a,x)) = \cons(a,\filter(p)(x)),\] while if \(p(a)\) is \(\bfalse\) we want \[\filter(p)(\cons(a,x)) = \filter(p)(x).\] With this in mind we define \(\filter\) like so.
Let \(A\) be a set. Define \(\varphi : A \times \lists{A} \rightarrow \lists{A}\) by \[\varphi(a,w) = \left\{ \begin{array}{ll} \cons(a,w) & \mathrm{if}\ p(a) = \btrue \\ w & \mathrm{if}\ p(a) = \bfalse. \end{array}\right.\] Now define \[\filter : \bool^A \rightarrow {\lists{A}}^{\lists{A}}\] by \[\filter(p)(x) = \foldr(\nil)(\varphi)(x).\]
In Haskell:
Since \(\filter(p)\) is defined as a \(\foldr(\ast)(\ast)\), it can be characterized as the unique solution to a system of functional equations.
Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate. \(\filter(p)\) is the unique map \(f : \lists{A} \rightarrow \lists{A}\) satisfying the following for all \(a \in A\) and \(x \in \lists{A}\). \[\left\{\begin{array}{ll} f(\nil) = \nil \\ f(\cons(a,x)) = \bif{p(a)}{\cons(a,f(x))}{f(x)} \end{array}\right.\]
_test_filter_nil :: (List t, Equal a, Equal (t a))
=> t a -> Test ((a -> Bool) -> Bool)
_test_filter_nil t =
testName "filter(p)(nil) == nil" $
\p -> eq (filter p (nil `withTypeOf` t)) nil
_test_filter_cons :: (List t, Equal a, Equal (t a))
=> t a -> Test ((a -> Bool) -> a -> t a -> Bool)
_test_filter_cons _ =
testName "filter(p)(cons(a,x)) == if(p(a),cons(a,filter(p)(x)),filter(p)(x))" $
\p a x -> eq
(filter p (cons a x))
(if p a then cons a (filter p x) else filter p x)As we might expect, the items in \(\filter(p)(x)\) all satisfy \(p\).
Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate. For all \(x \in \lists{A}\) we have \[\all(p,\filter(p)(x)) = \btrue.\]
We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \all(p,\filter(p)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \all(p,\nil) \\ & = & \nil \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). If \(p(a) = \btrue\), we have \[\begin{eqnarray*} & & \all(p,\filter(p)(\cons(a,x))) \\ & = & \all(p,\cons(a,\filter(p)(x))) \\ & = & \band(p(a),\all(p,\filter(p)(x))) \\ & = & \band(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-true} = & \btrue \end{eqnarray*}\] as claimed, while if \(p(a) = \bfalse\), we have \[\begin{eqnarray*} & & \all(p,\filter(p)(\cons(a,x))) \\ & = & \all(p,\filter(p)(x)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#thm-filter-all} = & \btrue \end{eqnarray*}\] as claimed.
\(\filter\) interacts with \(\snoc\).
Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate. For all \(a \in A\) and \(x \in \lists{A}\), we have \[\filter(p)(\snoc(a,x)) = \bif{p(a)}{\snoc(a,\filter(p)(x))}{\filter(p)(x)}.\]
We proceed by list induction on \(x\). For the base case \(x = \nil\), if \(p(a) = \btrue\) we have \[\begin{eqnarray*} & & \filter(p)(\snoc(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \filter(p)(\cons(a,\nil)) \\ & = & \cons(a,\filter(p)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \cons(a,\nil) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \snoc(a,\nil) \end{eqnarray*}\] as claimed, while if \(p(a) = \bfalse\) we have \[\begin{eqnarray*} & & \filter(p)(\snoc(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \filter(p)(\cons(a,\nil)) \\ & = & \filter(p)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \nil \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some \(x\) and let \(b \in A\). If \(p(a) = p(b) = \btrue\), we have \[\begin{eqnarray*} & & \filter(p)(\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \filter(p)(\cons(b,\snoc(a,x))) \\ & = & \cons(b,\filter(p)(\snoc(a,x))) \\ & = & \cons(b,\snoc(a,\filter(p)(x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \snoc(a,\cons(b,\filter(p)(x))) \\ & = & \snoc(a,\filter(p)(\cons(b,x))) \end{eqnarray*}\] as needed. If \(p(a) = \btrue\) and \(p(b) = \bfalse\), we have \[\begin{eqnarray*} & & \filter(p)(\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \filter(p)(\cons(b,\snoc(a,x))) \\ & = & \filter(p)(\snoc(a,x)) \\ & = & \snoc(a,\filter(p)(x)) \\ & = & \snoc(a,\filter(p)(\cons(b,x))) \end{eqnarray*}\] as needed. If \(p(a) = \bfalse\) and \(p(b) = \btrue\), we have \[\begin{eqnarray*} & & \filter(p)(\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \filter(p)(\cons(b,\snoc(a,x))) \\ & = & \cons(b,\filter(p)(\snoc(a,x))) \\ & = & \cons(b,\filter(p)(x)) \\ & = & \filter(p)(\cons(b,x)) \end{eqnarray*}\] as needed. Finally, if \(p(a) = p(b) = \bfalse\), we have \[\begin{eqnarray*} & & \filter(p)(\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \filter(p)(\cons(b,\snoc(a,x))) \\ & = & \filter(p)(\snoc(a,x)) \\ & = & \filter(p)(x) \\ & = & \filter(p)(\cons(b,x)) \end{eqnarray*}\] as needed.
\(\filter\) interacts with \(\rev\).
Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate. For all \(x \in \lists{A}\), we have \[\filter(p)(\rev(x)) = \rev(\filter(p)(x)).\]
We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \filter(p)(\rev(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \filter(p)(\nil) \\ & = & \nil \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \rev(\nil) \\ & = & \rev(\filter(p)(\nil)) \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). If \(p(a) = \btrue\), we have \[\begin{eqnarray*} & & \rev(\filter(p)(\cons(a,x))) \\ & = & \rev(\cons(a,\filter(p)(x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \snoc(a,\rev(\filter(p)(x))) \\ & = & \snoc(a,\filter(p)(\rev(x))) \\ & = & \filter(p)(\snoc(a,\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \filter(p)(\rev(\cons(a,x))) \end{eqnarray*}\] as claimed. If \(p(a) = \bfalse\), we have \[\begin{eqnarray*} & & \rev(\filter(p)(\cons(a,x))) \\ & = & \rev(\filter(p)(x)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#thm-filter-rev} = & \filter(p)(\rev(x)) \\ & = & \filter(p)(\snoc(a,\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \filter(p)(\rev(\cons(a,x))) \end{eqnarray*}\] as claimed.
\(\filter(p)\) distributes over \(\cat\).
Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate. For all \(x,y \in \lists{A}\) we have \[\filter(p)(\cat(x,y)) = \cat(\filter(p)(x),\filter(p)(y)).\]
We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \filter(p)(\cat(x,y)) \\ & = & \filter(p)(\cat(\nil,y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \filter(p)(y) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \cat(\nil,\filter(p)(y)) \\ & = & \cat(\filter(p)(\nil),\filter(p)(y)) \\ & = & \cat(\filter(p)(x),\filter(p)(y)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). If \(p(a) = \btrue\), we have \[\begin{eqnarray*} & & \filter(p)(\cat(\cons(a,x),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \filter(p)(\cons(a,\cat(x,y))) \\ & = & \cons(a,\filter(p)(\cat(x,y))) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#thm-filter-cat} = & \cons(a,\cat(\filter(p)(x),\filter(p)(y))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \cat(\cons(a,\filter(p)(x)),\filter(p)(y)) \\ & = & \cat(\filter(p)(\cons(a,x)),\filter(p)(y)) \end{eqnarray*}\] as needed. If \(p(a) = \bfalse\), we have \[\begin{eqnarray*} & & \filter(p)(\cat(\cons(a,x),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \filter(p)(\cons(a,\cat(x,y))) \\ & = & \filter(p)(\cat(x,y)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#thm-filter-cat} = & \cat(\filter(p)(x),\filter(p)(y)) \\ & = & \cat(\filter(p)(\cons(a,x)),\filter(p)(y)) \end{eqnarray*}\] as needed.
\(\filter(p)\) is idempotent.
Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate. For all \(x \in \lists{A}\) we have \[\filter(p)(\filter(p)(x)) = \filter(p)(x).\]
We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \filter(p)(\filter(p)(x)) \\ & = & \filter(p)(\filter(p)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \filter(p)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \nil \\ & = & x \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Now we have \[\begin{eqnarray*} & & \filter(p)(\filter(p)(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-cons} = & \filter(p)(\bif{p(a)}{\cons(a,\filter(p)(x))}{\filter(p)(x)}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \bif{p(a)}{\filter(p)(\cons(a,\filter(p)(x)))}{\filter(p)(\filter(p)(x))} \\ & = & \bif{p(a)}{\bif{p(a)}{\cons(a,\filter(p)(x))}{\filter(p)(x)}}{\filter(p)(x)} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-prune-true} = & \bif{p(a)}{\cons(a,\filter(p)(x))}{\filter(p)(x)} \\ & = & \filter(p)(\cons(a,x)) \end{eqnarray*}\] as needed
A list \(x\) is invariant under \(\filter(p)\) if and only if \(\all(p)(x)\).
Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate with \(x \in \lists{A}\). We have \[\beq(x,\filter(p)(x)) = \all(p,x).\]
We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \beq(x,\filter(p)(x)) \\ & = & \beq(\nil,\filter(p)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \beq(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \btrue \\ & = & \all(p,\nil) \\ & \hyp{x = \nil} = & \all(p,x) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). We consider two possibilities. If \(p(a) = \btrue\), we have \[\begin{eqnarray*} & & \beq(\cons(a,x),\filter(p)(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-cons} = & \beq(\cons(a,x),\bif{p(a)}{\cons(a,\filter(p)(x))}{\filter(p)(x)}) \\ & = & \beq(\cons(a,x),\bif{\btrue}{\cons(a,\filter(p)(x))}{\filter(p)(x)}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \beq(\cons(a,x),\cons(a,\filter(p)(x))) \\ & = & \band(\beq(a,a),\beq(x,\filter(p)(x))) \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \band(\btrue,\beq(x,\filter(p)(x))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \beq(x,\filter(p)(x)) \\ & = & \all(p,x) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \band(\btrue,\all(p,x)) \\ & = & \band(p(a),\all(p,x)) \\ & = & \all(p,\cons(a,x)) \end{eqnarray*}\] as needed. Suppose instead that \(p(a) = \bfalse\). Now \(\sublist(\filter(p)(x),x) = \btrue\), and using the inductive hypothesis we have \[\begin{eqnarray*} & & \beq(\cons(a,x),\filter(p)(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-cons} = & \beq(\cons(a,x),\bif{p(a)}{\cons(a,\filter(p)(x))}{\filter(p)(x)}) \\ & = & \beq(\cons(a,x),\bif{\bfalse}{\cons(a,\filter(p)(x))}{\filter(p)(x)}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \beq(\cons(a,x),\filter(p)(x)) \\ & = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \band(\bfalse,\all(p,x)) \\ & = & \band(p(a),\all(p,x)) \\ & = & \all(p,\cons(a,x)) \end{eqnarray*}\] as needed.
\(\filter(p)\) and \(\filter(q)\) commute.
Let \(A\) be a set and \(p,q : A \rightarrow \bool\) predicates. For all \(x \in \lists{A}\) we have \[\filter(p)(\filter(q)(x)) = \filter(q)(\filter(p)(x)).\]
We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \filter(p)(\filter(q)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \filter(p)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \nil \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \filter(q)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \filter(q)(\filter(p)(\nil)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Now \[\begin{eqnarray*} & & \filter(p)(\filter(q)(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-cons} = & \filter(p)(\bif{q(a)}{\cons(a,\filter(q)(x))}{\filter(q)(x)}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \bif{q(a)}{\filter(p)(\cons(a,\filter(q)(x)))}{\filter(p)(\filter(q)(x))} \\ & = & \bif{q(a)}{\bif{p(a)}{\cons(a),\filter(p)(\filter(q)(x))}{\filter(p)(\filter(q)(x))}}{\filter(p)(\filter(q)(x))} \\ & = & \bif{p(a)}{\bif{q(a)}{\cons(a),\filter(p)(\filter(q)(x))}{\filter(p)(\filter(q)(x))}}{\filter(p)(\filter(q)(x))} \\ & = & \bif{p(a)}{\filter(q)(\cons(a,\filter(p)(x)))}{\filter(q)(\filter(p)(x))} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \filter(q)(\bif{p(a)}{\cons(a,\filter(p)(x))}{\filter(p)(x)}) \\ & = & \filter(q)(\filter(p)(\cons(a,x))) \end{eqnarray*}\] as needed.
Testing
Suite:
_test_filter ::
( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
, TypeName (t a), List t
, Show (t a), Equal (t a), Arbitrary (t a), Equal (t (Pair a a))
) => Int -> Int -> t a -> IO ()
_test_filter size cases t = do
testLabel1 "filter" t
let args = testArgs size cases
runTest args (_test_filter_nil t)
runTest args (_test_filter_cons t)
runTest args (_test_filter_all t)
runTest args (_test_filter_snoc t)
runTest args (_test_filter_rev t)
runTest args (_test_filter_cat t)
runTest args (_test_filter_idempotent t)
runTest args (_test_filter_eq_all t)
runTest args (_test_filter_commute t)Main: