Select
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 Select
( select, _test_select, main_select
) where
import Testing
import Booleans
import NaturalNumbers
import Choose
import Lists
import DoubleBailoutFold
import Cat
import Length
import Map
import AllAndAny
import SublistToday we’ll define a function, \(\select\), which takes a natural number \(n\) and a list \(x\) and constructs the list of all length \(n\) sublists of \(x\). The signature of \(\select\) should be \[\nats \times \lists{A} \rightarrow \lists{\lists{A}},\] which matches several of our recursion operators. After trying a few, we’ll use double bailout fold.
Let \(A\) be a set. Define \(\delta : \nats \rightarrow \lists{\lists{A}}\) by \[\delta(n) = \bif{\iszero(n)}{\cons(\nil,\nil)}{\nil},\] \(\beta : A \times \lists{A} \times \nats \rightarrow \bool\) by \[\beta(a,x,n) = \iszero(n),\] \(\psi : A \times \lists{A} \times \nats \rightarrow \lists{\lists{A}}\) by \[\psi(a,x,n) = \cons(\nil,\nil),\] and \(\chi : A \times \lists{A} \times \nats \times \lists{\lists{A}} \times \lists{\lists{A}} \rightarrow \lists{\lists{A}}\) by \[\chi(a,x,n,u,v) = \cat(\map(\cons(a))(v),u).\] Now define \(\select : \nats \times \lists{A} \rightarrow \lists{\lists{A}}\) by \[\select(n,x) = \dbfoldr(\delta)(\beta)(\prev)(\psi)(\chi)(x,n).\]
In Haskell:
Since \(\select\) is defined as a double bailout fold, it can be characterized as the unique solution to a system of functional equations.
Let \(A\) be a set. \(\select\) is the unique map \(f : \nats \times \lists{A} \rightarrow \lists{\lists{A}}\) satisfying the following equations for all \(n \in \nats\), \(a \in A\), and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(n,\nil) = \bif{\iszero(n)}{\cons(\nil,\nil)}{\nil} \\ f(n,\cons(a,x)) = \bif{\iszero(n)}{\cons(\nil,\nil)}{\cat(\map(\cons(a))(f(\prev(n),x)),f(n,x))} \end{array}\right.\]
In particular, we have \[\select(\zero,\cons(a,x)) = \cons(\nil,\nil)\] and \[\select(\next(n),\cons(a,x)) = \cat(\map(\cons(a))(\select(n,x)),\select(\next(n),x)).\]
_test_select_nil :: (List t, Equal a, Natural n, Equal n, Equal (t (t a)))
=> t a -> n -> Test (n -> Bool)
_test_select_nil t _ =
testName "select(n,nil) == if(eq(n,zero),cons(nil,nil),nil)" $
\n -> eq
(select n (nil `withTypeOf` t))
(if isZero n then cons nil nil else nil)
_test_select_cons :: (List t, Equal a, Natural n, Equal n, Equal (t (t a)))
=> t a -> n -> Test (n -> a -> t a -> Bool)
_test_select_cons _ _ =
testName "select(n,cons(a,x)) == if(eq(n,zero),cons(nil,nil),cat(map(cons(a,-))(select(prev(n),x)),select(n,x)))" $
\n a x -> eq
(select n (cons a x))
(if isZero n then cons nil nil else cat (map (cons a) (select (prev n) x)) (select n x))We can directly compute \(\select(\zero,-)\).
Let \(A\) be a set. For all \(x \in \lists{A}\), we have \[\select(\zero,x) = \cons(\nil,\nil).\]
If \(x = \nil\), then \[\begin{eqnarray*} & & \select(\zero,\nil) \\ & \href{/posts/arithmetic-made-difficult/Select.html#cor-select-nil} = & \bif{\iszero(\zero)}{\cons(\nil,\nil)}{\nil} \\ & = & \cons(\nil,\nil), \end{eqnarray*}\] and if \(x = \cons(a,u)\), then \[\begin{eqnarray*} & & \select(\zero,\cons(a,u)) \\ & \href{/posts/arithmetic-made-difficult/Select.html#cor-select-cons} = & \bif{\iszero(\zero)}{\cons(\nil,\nil)}{\cat(\map(\cons(a))(\select(\prev(\zero),u)),\select(\zero,u))} \\ & = & \cons(\nil,\nil) \end{eqnarray*}\] as claimed.
We can directly compute \(\select(\next(\zero),-)\).
Let \(A\) be a set. For all \(x \in \lists{A}\), we have \[\select(\next(\zero),x) = \map(\cons(-,\nil))(x).\]
We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \select(\next(\zero),x) \\ & = & \select(\next(\zero),\nil) \\ & = & \bif{\isnil(\next(\zero))}{\cons(\nil,\nil)}{\nil} \\ & = & \nil \\ & = & \map(\cons(-,\nil))(\nil) \\ & = & \map(\cons(-,\nil))(x) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Using the inductive hypothesis, we have \[\begin{eqnarray*} & & \select(\next(\zero),\cons(a,x)) \\ & = & \cat(\map(\cons(a))(\select(\zero,x)),\select(\next(\zero),x)) \\ & = & \cat(\map(\cons(a))(\cons(\nil,\nil)),\map(\cons(-,\nil))(x)) \\ & = & \cat(\cons(\cons(a,\nil),\map(\cons(a))(\nil)),\map(\cons(-,\nil))(x)) \\ & = & \cat(\cons(\cons(a,\nil),\nil),\map(\cons(-,\nil))(x)) \\ & = & \cat(\snoc(\cons(a,\nil),\nil),\map(\cons(-,\nil))(x)) \\ & = & \cat(\nil,\cons(\cons(a,\nil),\map(\cons(-,\nil))(x))) \\ & = & \cons(\cons(a,\nil),\map(\cons(-,\nil))(x)) \\ & = & \cons(\cons(-,\nil)(a),\map(\cons(-,\nil))(x)) \\ & = & \map(\cons(-,\nil))(\cons(a,x)) \end{eqnarray*}\] as needed.
\(\select\) interacts with \(\length\).
Let \(A\) be a set with \(x \in \lists{A}\). For all \(k \in \nats\), we have \[\length(\select(k,x)) = \nchoose(\length(x),k).\]
We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \length(\select(k,x)) \\ & = & \length(\select(k,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Select.html#cor-select-nil} = & \length(\bif{\iszero(k)}{\cons(\nil,\nil)}{\nil}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \bif{\iszero(k)}{\length(\cons(\nil,\nil))}{\length(\nil)} \\ & = & \bif{\iszero(k)}{\next(\zero)}{\zero} \\ & = & \nchoose(\zero,k) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \nchoose(\length(\nil),k) \\ & = & \nchoose(\length(x),k) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). We consider two possibilities for \(k\). If \(k = \zero\), we have \[\begin{eqnarray*} & & \length(\select(k,\cons(a,x))) \\ & = & \length(\select(\zero,\cons(a,x))) \\ & = & \length(\cons(\nil,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-length-singleton} = & \next(\zero) \\ & = & \nchoose(\next(\length(x)),\zero) \\ & = & \nchoose(\length(\cons(a,x)),k) \end{eqnarray*}\] as needed. If \(k = \next(m)\), then using the inductive hypothesis we have \[\begin{eqnarray*} & & \length(\select(k,\cons(a,x))) \\ & = & \length(\select(\next(m),\cons(a,x))) \\ & = & \length(\cat(\map(\cons(a))(\select(m,x)),\select(\next(m),x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-length-cat} = & \nplus(\length(\map(\cons(a))(\select(m,x))),\length(\select(\next(m),x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-length-map} = & \nplus(\length(\select(m,x)),\length(\select(\next(m),x))) \\ & = & \nplus(\nchoose(\length(x),m),\nchoose(\length(x),\next(m))) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-commutative} = & \nplus(\nchoose(\length(x),\next(m)),\nchoose(\length(x),m)) \\ & = & \nchoose(\next(\length(x)),\next(m)) \\ & = & \nchoose(\length(\cons(a,x)),k) \end{eqnarray*}\] as needed.
\(\select\) is compatible with \(\sublist\).
Let \(A\) be a set and let \(x,y \in \lists{A}\). If \(\sublist(x,y) = \btrue\), then \(\sublist(\select(k,x),\select(k,y)) = \btrue\) for all \(k \in \nats\).
We proceed by induction on \(k\). For the base case \(k = \zero\), suppose \(\sublist(x,y) = \btrue\). Now \[\begin{eqnarray*} & & \sublist(\select(k,x),\select(k,y)) \\ & = & \sublist(\select(\zero,x),\select(\zero,y)) \\ & = & \sublist(\cons(\nil,\nil),\cons(\nil,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-reflexive} = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for some \(k\). We now proceed by list induction on \(y\). For the base case \(y = \nil\), suppose \[\btrue = \sublist(x,y) = \sublist(x,\nil);\] then we must have \(x = \nil\). In this case we have \[\begin{eqnarray*} & & \sublist(\select(\next(k),x),\select(\next(k),y)) \\ & = & \sublist(\select(\next(k),\nil),\select(\next(k),\nil)) \\ & = & \sublist(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-reflexive} = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for \(\next(k)\) and all \(x\) for some \(y\), and let \(b \in A\). Suppose further that \(\sublist(x,\cons(b,y)) = \btrue\). We consider two possibilities for \(x\). If \(x = \nil\), we have \[\begin{eqnarray*} & & \sublist(\select(\next(k),x),\select(\next(k),\cons(b,y))) \\ & = & \sublist(\select(\next(k),\nil),\select(\next(k),\cons(b,y))) \\ & = & \sublist(\nil,\select(\next(k),\cons(b,y))) \\ & = & \btrue \end{eqnarray*}\] as needed. Suppose instead that \(x = \cons(a,u)\). We have two possibilities. If \(a \neq b\), then since \[\btrue = \sublist(x,\cons(b,y)) = \sublist(\cons(a,u),\cons(b,y))\] we have \(\btrue = \sublist(\cons(a,u),y) = \sublist(x,y)\). By the inductive hypothesis on \(y\) we have \[\sublist(\select(\next(k),x),\select(\next(k),y)) = \btrue.\] Moreover, note that \[\begin{eqnarray*} & & \select(\next(k),\cons(b,y)) \\ & = & \cat(\map(\cons(b,-))(\select(k,y)),\select(\next(k),y)) \end{eqnarray*}\] so that, in particular, \[\sublist(\select(\next(k),y),\select(\next(k),\cons(b,y))) = \btrue.\] Since \(\sublist\) is transitive, we have \[\sublist(\select(\next(k),x),\select(\next(k),\cons(b,y))) = \btrue\] as needed.
Suppose instead that \(a = b\). Then since \[\btrue = \sublist(x,\cons(b,y)) = \sublist(\cons(a,u),\cons(b,y)),\] in fact we have \(\sublist(u,y) = \btrue\). Using the inductive hypothesis on \(k\), we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(u,y) \\ & = & \sublist(\select(k,u),\select(k,y)) \\ & = & \sublist(\map(\cons(a))(\select(k,u)),\map(\cons(a))(\select(k,y))) \\ & = & \sublist(H,K) \end{eqnarray*}\] and similarly using the inductive hypothesis on \(y\) we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(u,y) \\ & = & \sublist(\select(\next(k),u),\select(\next(k),y)) \\ & = & \sublist(P,Q). \end{eqnarray*}\] Now we have \[\begin{eqnarray*} & & \sublist(\select(\next(k),x),\select(\next(k),\cons(b,y))) \\ & = & \sublist(\select(\next(k),\cons(a,u)),\select(\next(k),\cons(b,y))) \\ & = & \sublist(\select(\next(k),\cons(a,u)),\select(\next(k),\cons(a,y))) \\ & = & \sublist(\cat(\map(\cons(a))(\select(k,u)),\select(\next(k),u)),\cat(\map(\cons(a))(\select(k,y)),\select(\next(k),y))) \\ & = & \sublist(\cat(H,P),\cat(K,Q)) \\ & = & \btrue \end{eqnarray*}\] as needed.
Selections are sublists.
Let \(A\) be a set with \(x \in \lists{A}\) and \(k \in \nats\). Then \[\all(\sublist(-,x),\select(k,x)) = \btrue.\]
We consider two possibilities for \(k\). If \(k = \zero\), we have \[\begin{eqnarray*} & & \all(\sublist(-,x),\select(k,x)) \\ & = & \all(\sublist(-,x),\select(\zero,x)) \\ & = & \all(\sublist(-,x),\cons(\nil,\nil)) \\ & = & \band(\sublist(\nil,x),\all(\sublist(-,x),\nil)) \\ & = & \band(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-true} = & \btrue \end{eqnarray*}\] as claimed. Suppose instead that \(k = \next(m)\); we proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \all(\sublist(-,x),\select(k,x)) \\ & = & \all(\sublist(-,\nil),\select(\next(m),\nil)) \\ & = & \all(\sublist(-,\nil),\nil) \\ & = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(k\) for some \(x\) and let \(a \in A\). Using the inductive hypothesis we have \[\begin{eqnarray*} & & \all(\sublist(-,\cons(a,x)),\map(\cons(a))(\select(m,x))) \\ & = & \all(\sublist(-,\cons(a,x)) \circ \cons(a),\select(m,x)) \\ & = & \all(\sublist(\cons(a),\cons(a,x)),\select(m,x)) \\ & = & \all(\sublist(-,x),\select(m,x)) \\ & = & \btrue. \end{eqnarray*}\] Also using the inductive hypothesis, we have \[\begin{eqnarray*} & & \all(\sublist(-,x),\select(\next(m),x)) \\ & = & \btrue, \end{eqnarray*}\] and for all \(u \in \lists{A}\), if \(\sublist(u,x) = \btrue\) then \(\sublist(u,\cons(a,x)) = \btrue\). Thus we have \[\begin{eqnarray*} & & \all(\sublist(-,\cons(a,x)),\select(\next(m),x)) \\ & = & \btrue. \end{eqnarray*}\] Now \[\begin{eqnarray*} & & \all(\sublist(-,\cons(a,x)),\select(k,\cons(a,x))) \\ & = & \all(\sublist(-,\cons(a,x)),\select(\next(m),\cons(a,x))) \\ & = & \all(\sublist(-,\cons(a,x)),\cat(\map(\cons(a))(\select(m,x)),\select(\next(m),x))) \\ & = & \band(\all(\sublist(-,\cons(a,x)),\map(\cons(a))(\select(m,x))),\all(\sublist(-,\cons(a,x)),\select(\next(m),x))) \\ & = & \band(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-true} = & \btrue \end{eqnarray*}\] as needed.
Selections have fixed length.
Let \(A\) be a set with \(x \in \lists{A}\) and \(k \in \nats\). Then \[\all(\beq(k,\length(-)),\select(k,x)) = \btrue.\]
We consider two possibilities for \(k\). If \(k = \zero\), we have \[\begin{eqnarray*} & & \all(\beq(k,\length(-)),\select(k,x)) \\ & = & \all(\beq(\zero,\length(-)),\select(\zero,x)) \\ & = & \all(\beq(\zero,\length(-)),\cons(\nil,\nil)) \\ & = & \band(\beq(\zero,\length(\nil)),\all(\beq(\zero,\length(-)),\nil)) \\ & = & \band(\beq(\zero,\zero),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \band(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-true} = & \btrue \end{eqnarray*}\] as claimed. Suppose instead that \(k = \next(m)\). We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \all(\beq(k,\length(-)),\select(k,x)) \\ & = & \all(\beq(k,\length(-)),\select(\next(m),\nil)) \\ & = & \all(\beq(k,\length(-)),\nil) \\ & = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(k\) for some \(x\) and let \(a \in A\). Using the inductive hypothesis (twice!) we have \[\begin{eqnarray*} & & \all(\beq(k,\length(-)),\select(k,\cons(a,x))) \\ & = & \all(\beq(k,\length(-)),\select(\next(m),\cons(a,x))) \\ & = & \all(\beq(k,\length(-)),\cat(\map(\cons(a))(\select(m,x)),\select(\next(m),x))) \\ & = & \band(\all(\beq(k,\length(-)),\map(\cons(a))(\select(m,x))),\all(\beq(k,\length(-)),\select(\next(m),x))) \\ & = & \band(\all(\beq(k,\length(-)),\map(\cons(a))(\select(m,x))),\all(\beq(k,\length(-)),\select(k,x))) \\ & = & \band(\all(\beq(k,\length(-)),\map(\cons(a))(\select(m,x))),\btrue) \\ & = & \band(\all(\beq(k,\length(-) \circ \cons(a)),\select(m,x)),\btrue) \\ & = & \band(\all(\beq(k,\length(\cons(a))),\select(m,x)),\btrue) \\ & = & \band(\all(\beq(\next(m),\next(\length(-))),\select(m,x)),\btrue) \\ & = & \band(\all(\beq(m,\length(-)),\select(m,x)),\btrue) \\ & = & \band(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-true} = & \btrue \end{eqnarray*}\] as needed.
Testing
Suite:
_test_select ::
( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
, TypeName n, Natural n, Show n, Arbitrary n, Equal n
, TypeName (t a), List t
, Equal (t a), Show (t a), Arbitrary (t a), Equal (t (t a))
) => Int -> Int -> t a -> n -> IO ()
_test_select size cases t n = do
testLabel1 "select" t
let args = testArgs size cases
runTest args (_test_select_nil t n)
runTest args (_test_select_cons t n)
runTest args (_test_select_zero t n)
runTest args (_test_select_one t n)
runTest args (_test_select_length t n)
runTest args (_test_select_sublist t n)
runTest args (_test_select_all_sublist t n)
runTest args (_test_select_all_length t n)Main: