# Select

Posted on 2017-05-25 by nbloomf

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 Sublist

Today 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).$

select :: (List t, Natural n) => n -> t a -> t (t a)
select n x = dbfoldr delta beta prev psi chi x n
where
delta m = if isZero m then cons nil nil else nil
beta _ _ m = isZero m
psi _ _ _ = cons nil nil
chi a _ _ u v = cat (map (cons a) v) u

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.

_test_select_zero :: (List t, Equal a, Natural n, Equal n, Equal (t (t a)))
=> t a -> n -> Test (t a -> Bool)
_test_select_zero _ n =
testName "select(zero,x) == cons(nil,nil)" $\x -> eq (select (zero withTypeOf n) x) (cons nil nil) 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. _test_select_one :: (List t, Equal a, Natural n, Equal n, Equal (t (t a))) => t a -> n -> Test (t a -> Bool) _test_select_one _ n = testName "select(next(zero),x) == map(cons(-,nil))(x)"$
\x -> eq
(select ((next zero) withTypeOf n) x)
(map (\a -> cons a nil) x)

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

_test_select_length :: (List t, Equal a, Natural n, Equal n, Equal (t a))
=> t a -> n -> Test (n -> t a -> Bool)
_test_select_length _ _ =
testName "length(select(k,x)) == choose(length(x),k)" $\k x -> eq (length (select k x)) (choose (length x) k) $$\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. _test_select_sublist :: (List t, Equal a, Natural n, Equal n, Equal (t a)) => t a -> n -> Test (n -> t a -> t a -> Bool) _test_select_sublist _ _ = testName "sublist(x,y) == sublist(select(k,x),select(k,y))"$
\k x y -> if sublist x y
then sublist (select k x) (select k y)
else true

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.

_test_select_all_sublist :: (List t, Equal a, Natural n, Equal n, Equal (t a))
=> t a -> n -> Test (n -> t a -> Bool)
_test_select_all_sublist _ _ =
testName "all(sublist(-,x),select(k,x))" $\k x -> all (\u -> sublist u x) (select k x) 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. _test_select_all_length :: (List t, Equal a, Natural n, Equal n, Equal (t a)) => t a -> n -> Test (n -> t a -> Bool) _test_select_all_length _ _ = testName "all(eq(k,length(-)),select(k,x))"$
\k x -> all (\u -> eq k (length u)) (select k x)

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

main_select :: IO ()
main_select = do
_test_select 20 30 (nil :: ConsList Bool)  (zero :: Unary)
_test_select 20 30 (nil :: ConsList Unary) (zero :: Unary)