Sublists

Posted on 2018-01-20 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 Sublists
  ( sublists, _test_sublists, main_sublists
  ) where

import Testing
import Booleans
import Unary
import NaturalNumbers
import Exponentiation
import Lists
import Cat
import Length
import Map
import AllAndAny
import Elt
import Sublist
import Select

We’ve already defined a predicate that detects when one list is a sublist of another. Today we’ll define a function that constructs a list of all sublists of a given list.

Let \(A\) be a set. Define \(\varphi : A \times \lists{\lists{A}} \rightarrow \lists{\lists{A}}\) by \[\varphi(a,z) = \cat(\map(\cons(a)(z)),z).\] Now define \(\sublists : \lists{A} \rightarrow \lists{\lists{A}}\) by \[\sublists = \foldr(\cons(\nil,\nil))(\varphi).\]

In Haskell:

sublists :: (List t) => t a -> t (t a)
sublists = foldr (cons nil nil) phi
  where
    phi a z = cat (map (cons a) z) z

Since \(\sublists\) 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. \(\sublists\) is the unique map \(f : \lists{A} \rightarrow \lists{\lists{A}}\) satisfying the following equations for all \(a \in A\) and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(\nil) = \cons(\nil,\nil) \\ f(\cons(a,x)) = \cat(\map(\cons(a))(f(x)),f(x)) \end{array}\right.\]

_test_sublists_nil :: (List t, Equal (t (t a)))
  => t a -> Test Bool
_test_sublists_nil t =
  testName "sublists(nil) == cons(nil,nil)" $
  eq
    (sublists (nil `withTypeOf` t))
    (cons nil nil)


_test_sublists_cons :: (List t, Equal (t (t a)))
  => t a -> Test (a -> t a -> Bool)
_test_sublists_cons _ =
  testName "sublists(cons(a,x)) == cat(map(cons(a,-))(x),sublists(x))" $
  \a x -> eq
    (sublists (cons a x))
    (cat (map (cons a) (sublists x)) (sublists x))

Every item in \(\sublists(x)\) is a sublist.

Let \(A\) be a set. For all \(x \in \lists{A}\), we have \[\all(\sublist(-,x))(\sublists(x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \all(\sublist(-,\nil))(\sublists(\nil)) \\ & = & \all(\sublist(-,\nil))(\cons(\nil,\nil)) \\ & = & \band(\sublist(\nil,\nil),\all(\sublist(-,\nil))(\nil)) \\ & = & \band(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-true} = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the result holds for some \(x\) and let \(a \in A\). Note that \[\pimpl(\sublist(-,x),\sublist(-,\cons(a,x))),\] so that \[\bimpl(\all(\sublist(-,x))(z),\all(\sublist(-,\cons(a,x)))(z))\] for all \(z \in \lists{\lists{A}}\). Since \(\all(\sublist(-,x))(\sublists(x))\) by the inductive hypothesis, we have \(\all(\sublist(-,\cons(a,x)))(\sublists(x)) = \btrue\). Now \[\begin{eqnarray*} & & \all(\sublist(-,\cons(a,x)))(\sublists(\cons(a,x))) \\ & = & \all(\sublist(-,\cons(a,x)))(\cat(\map(\cons(a))(\sublists(x)),\sublists(x))) \\ & = & \band(\all(\sublist(-,\cons(a,x)))(\map(\cons(a))(\sublists(x))),\all(\sublist(-,\cons(a,x)))(\sublists(x))) \\ & = & \band(\all(\sublist(\cons(a),\cons(a,x)))(\sublists(x)),\all(\sublist(-,\cons(a,x)))(\sublists(x))) \\ & = & \band(\all(\sublist(-,x))(\sublists(x)),\all(\sublist(-,\cons(a,x)))(\sublists(x))) \\ & = & \band(\btrue,\all(\sublist(-,\cons(a,x)))(\sublists(x))) \\ & = & \all(\sublist(-,\cons(a,x)))(\sublists(x)) \\ & = & \btrue \end{eqnarray*}\] As needed.

_test_sublists_sublist :: (List t, Equal a, Equal (t (t a)))
  => t a -> t (t a) -> Test (t a -> Bool)
_test_sublists_sublist _ u =
  testName "all(sublist(-,x))(sublists(x))" $
  \x -> all (\y -> sublist y x) ((sublists x) `withTypeOf` u)

\(\sublists(x)\) is not \(\nil\).

Let \(A\) be a set. For all \(x \in \lists{A}\), we have \[\elt(\nil,\sublists(x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \elt(\nil,\sublists(\nil)) \\ & = & \elt(\nil,\cons(\nil,\nil)) \\ & = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the result holds for some \(x\) and let \(a \in A\). Now \[\begin{eqnarray*} & & \elt(\nil,\sublists(\cons(a,x))) \\ & = & \elt(\nil,\cat(\map(\cons(a))(\sublists(x)),\sublists(x))) \\ & \href{/posts/arithmetic-made-difficult/Elt.html#thm-elt-cat} = & \bor(\elt(\nil,\map(\cons(a))(\sublists(x))),\elt(\nil,\sublists(x))) \\ & = & \bor(\elt(\nil,\map(\cons(a))(\sublists(x))),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}\] as needed.

_test_sublists_nil_elt :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> Bool)
_test_sublists_nil_elt _ =
  testName "elt(nil,sublists(x))" $
  \x -> elt nil (sublists x)

Every sublist is an item in \(\sublists(x)\).

Let \(A\) be a set. For all \(x,y \in \lists{A}\) we have \[\elt(y,\sublists(x)) = \sublist(y,x).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \elt(y,\sublists(\nil)) \\ & = & \elt(y,\cons(\nil,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Elt.html#thm-elt-one} = & \beq(y,\nil) \\ & = & \isnil(y) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil} = & \sublist(y,\nil) \end{eqnarray*}\] as needed. For the inductive step, suppose the equation holds for all \(y\) for some \(x\), and let \(a \in A\). We have two possiblities for \(y\). If \(y = \nil\), we have \[\begin{eqnarray*} & & \elt(y,\sublists(\cons(a,x))) \\ & = & \elt(\nil,\sublists(\cons(a,x))) \\ & = & \btrue \\ & = & \sublist(\nil,x) \\ & = & \sublist(y,x) \end{eqnarray*}\] as claimed. If \(y = \cons(b,w)\), note that \(\bimpl(\sublist(\cons(b,w),x),\sublist(w,x))\). Then we have \[\begin{eqnarray*} & & \elt(y,\sublists(\cons(a,x))) \\ & = & \elt(y,\cat(\map(\cons(a))(\sublists(x)),\sublists(x))) \\ & \href{/posts/arithmetic-made-difficult/Elt.html#thm-elt-cat} = & \bor(\elt(y,\map(\cons(a))(\sublists(x))),\elt(y,\sublists(x))) \\ & = & \bor(\elt(y,\map(\cons(a))(\sublists(x))),\sublist(y,x)) \\ & = & \bor(\elt(\cons(b,w),\map(\cons(a))(\sublists(x))),\sublist(y,x)) \\ & = & \bor(\band(\beq(b,a),\elt(w,\sublists(x))),\sublist(y,x)) \\ & = & \bor(\band(\beq(b,a),\sublist(w,x)),\sublist(y,x)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-is-if} = & \bif{\band(\beq(b,a),\sublist(w,x))}{\btrue}{\sublist(y,x)} \\ & = & \bif{\beq(b,a)}{\sublist(w,x)}{\sublist(y,x)} \\ & = & \bif{\beq(b,a)}{\sublist(w,x)}{\sublist(\cons(b,w),x)} \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \sublist(\cons(b,w),\cons(a,x)) \\ & = & \sublist(y,\cons(a,x)) \end{eqnarray*}\]

_test_sublists_elt_sublist :: (List t, Equal a, Equal (t a))
  => t a -> t (t a) -> Test (t a -> t a -> Bool)
_test_sublists_elt_sublist _ u =
  testName "elt(y,sublists(x)) == sublist(y,x)" $
  \x y -> eq (elt y (sublists x)) (sublist y x)

\(\sublists\) interacts with \(\map\).

Let \(A\) and \(B\) be sets, with \(f : A \rightarrow B\). For all \(x \in \lists{A}\), we have \[\sublists(\map(f)(x)) = \map(\map(f))(\sublists(x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \sublists(\map(f)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \sublists(\nil) \\ & = & \cons(\nil,\nil) \\ & = & \cons(\map(f)(\nil),\map(\map(f))(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \map(\map(f))(\cons(\nil,\nil)) \\ & = & \map(\map(f))(\sublists(\nil)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\), and let \(a \in A\). Now \[\begin{eqnarray*} & & \sublists(\map(f)(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \sublists(\cons(f(a),\map(f)(x))) \\ & = & \cat(\map(\cons(f(a),-))(\sublists(\map(f)(x))),\sublists(\map(f)(x))) \\ & = & \cat(\map(\cons(f(a),-))(\map(\map(f))(\sublists(x))),\map(\map(f))(\sublists(x))) \\ & = & \cat(\map(\cons(f(a),-) \circ \map(f))(\sublists(x)),\map(\map(f))(\sublists(x))) \\ & = & \cat(\map(\map(f) \circ \cons(a))(\sublists(x)),\map(\map(f))(\sublists(x))) \\ & = & \cat(\map(\map(f))(\map(\cons(a))(\sublists(x))),\map(\map(f))(\sublists(x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-map-cat} = & \map(\map(f))(\cat(\map(\cons(a))(\sublists(x)),\sublists(x))) \\ & = & \map(\map(f))(\sublists(\cons(a,x))) \end{eqnarray*}\] as needed.

_test_sublists_map :: (List t, Equal a, Equal (t a), Equal (t (t a)))
  => t a -> t (t a) -> Test ((a -> a) -> t a -> Bool)
_test_sublists_map _ u =
  testName "sublists(map(f)(x)) == map(map(f))(sublists(x))" $
  \f x -> eq (sublists (map f x)) (map (map f) (sublists x))

\(\sublists\) interacts with \(\length\).

Let \(A\) be a set. For all \(x \in \lists{A}\) we have \[\length(\sublists(x)) = \npower(\next(\next(\zero)),\length(x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \length(\sublists(\nil)) \\ & = & \length(\cons(\nil,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-length-singleton} = & \next(\zero) \\ & = & \npower(\next(\next(\zero)),\zero) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \npower(\next(\next(\zero)),\length(\nil)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Now \[\begin{eqnarray*} & & \length(\sublists(\cons(a,x))) \\ & = & \length(\cat(\map(\cons(a))(\sublists(x)),\sublists(x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-length-cat} = & \nplus(\length(\map(\cons(a))(\sublists(x))),\length(\sublists(x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-length-map} = & \nplus(\length(\sublists(x)),\length(\sublists(x))) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-two} = & \ntimes(\next(\next(\zero)),\length(\sublists(x))) \\ & = & \ntimes(\next(\next(\zero)),\npower(\next(\next(\zero)),\length(x))) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-commutative} = & \ntimes(\npower(\next(\next(\zero)),\length(x)),\next(\next(\zero))) \\ & = & \npower(\next(\next(\zero)),\next(\length(x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \npower(\next(\next(\zero)),\length(\cons(a,x))) \end{eqnarray*}\] as needed.

_test_sublists_length :: (List t, Natural n, Equal n)
  => t a -> n -> Test (t n -> Bool)
_test_sublists_length _ k =
  testName "length(sublists(x)) == power(next(next(zero)),length(x))" $
  \x -> eq
    ((length (sublists (x))) `withTypeOf` k)
    (power (next (next zero)) (length x))

\(\select(k)\) is a sublist of \(\sublists\).

Let \(A\) be a set and \(k \in \nats\). For all \(x \in \lists{A}\) we have \[\sublist(\select(k)(x),\sublists(x)).\]

we proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \sublist(\select(k)(\nil),\sublists(\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 equality holds for all \(k\) for some \(x\), and let \(a \in A\). We have two possibilities for \(k\). If \(k = \zero\), we have \[\begin{eqnarray*} & & \sublist(\select(\zero)(\cons(a,x)),\sublists(\cons(a,x))) \\ & = & \sublist(\cons(\nil,\nil),\sublists(a,x)) \\ & = & \elt(\nil,\sublists(a,x)) \\ & = & \btrue \end{eqnarray*}\] as needed. Suppose instead that \(k = \next(m)\). Now we have \[\begin{eqnarray*} & & \sublist(\select(\next(m))(\cons(a,x)),\sublists(\cons(a,x))) \\ & = & \sublist(\cat(\map(\cons(a))(\select(m)(x)),\select(\next(m))(x)),\cat(\map(\cons(a))(\sublists(x)),\sublists(x))) \\ & = & Q. \end{eqnarray*}\] By the inductive hypothesis, note that \(\cons(a)\) is injective, so we have \[\begin{eqnarray*} & & \sublist(\map(\cons(a))(\select(m)(x)),\map(\cons(a))(\sublists(x))) \\ & = & \sublist(\select(m)(x),\sublists(x)) \\ & = & \btrue, \end{eqnarray*}\] and also \[\begin{eqnarray*} & & \sublist(\select(\next(m))(x),\sublists(x)) \\ & = & \btrue. \end{eqnarray*}\] Since \(\sublist\) is compatible with \(\cat\), we have \[\begin{eqnarray*} & & Q \\ & = & \btrue \end{eqnarray*}\] as needed.

_test_sublists_select :: (List t, Natural n, Equal (t a))
  => t a -> n -> Test (n -> t a -> Bool)
_test_sublists_select _ _ =
  testName "sublist(select(k)(x),sublists(x))" $
  \k x -> sublist (select k x) (sublists x)

Testing

Suite:

_test_sublists ::
  ( Equal a, Show a, Arbitrary a, CoArbitrary a, TypeName a
  , Equal b, Show b, Arbitrary b, CoArbitrary b, TypeName b, Boolean b
  , Equal n, Show n, Arbitrary n, CoArbitrary n, TypeName n, Natural n
  , Equal (t a), Show (t a), Arbitrary (t a), CoArbitrary (t a), TypeName (t a), List t
  , Equal (t n), Show (t n), Arbitrary (t n), CoArbitrary (t n), TypeName (t n)
  , Equal (t (t a))
  ) => Int -> Int -> t a -> t (t a) -> n -> b -> IO ()
_test_sublists size cases t u k p = do
  testLabel1 "sublists" t
  let args = testArgs size cases

  runTest args (_test_sublists_nil t)
  runTest args (_test_sublists_cons t)
  runTest args (_test_sublists_sublist t u)
  runTest args (_test_sublists_nil_elt t)
  runTest args (_test_sublists_elt_sublist t u)
  runTest args (_test_sublists_map t u)
  runTest args (_test_sublists_length t k)
  runTest args (_test_sublists_select t k)

Main:

main_sublists :: IO ()
main_sublists = do
  _test_sublists 10 100 (nil :: ConsList Bool)  nil (zero :: Unary) (true :: Bool)
  _test_sublists 10 100 (nil :: ConsList Unary) nil (zero :: Unary) (true :: Bool)