TakeWhile and DropWhile

Posted on 2017-12-16 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 TakeWhileAndDropWhile
  ( takeWhile, dropWhile
  , _test_takewhile_dropwhile, main_takewhile_dropwhile
  ) where

import Testing
import Booleans
import NaturalNumbers
import Lists
import ConsumingFold
import Cat
import PrefixAndSuffix
import Sublist

Today we’ll define two functions, \(\takeWhile\) and \(\dropWhile\), similar to \(\take\) and \(\drop\), but instead of taking or dropping a prefix of some length, we will take or drop the longest prefix satisfying some predicate. We’d like \(\takeBut\) to have a signature like \[\takeWhile : \bool^A \rightarrow {\lists{A}}^{\lists{A}}.\]

As usual, suppose \(\takeWhile\) can be defined in terms of fold; say \[\takeWhile(p)(x) = \foldr(e)(\varphi)(x)\] for some \(e\) and \(\varphi\). To make the types work out we need \(e \in \lists{A}\) and \(\varphi : A \times \lists{A} \rightarrow \lists{A}\). Thinking about the desired behavior for \(\takeWhile\), we need

\[\begin{eqnarray*} & & \nil \\ & = & \takeWhile(p)(\nil) \\ & = & \foldr(e)(\varphi)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & e \end{eqnarray*}\]

and

\[\begin{eqnarray*} & & \bif{p(a)}{\cons(a,\takeWhile(p,x))}{\nil} \\ & = & \takeWhile(p)(\cons(a,x)) \\ & = & \foldr(e)(\varphi)(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \varphi(a,\foldr(e)(\varphi)(x)) \\ & = & \varphi(a,\takeWhile(p,x)) \end{eqnarray*}\]

With this in mind, we define \(\takeWhile\) like so.

Let \(A\) be a set, with \(p : A \rightarrow \bool\). Define \(\varphi(p) : A \times \lists{A} \rightarrow \lists{A}\) by \[\varphi(p)(a,x) = \left\{ \begin{array}{ll} \cons(a,x) & \mathrm{if}\ p(a) = \btrue \\ \nil & \mathrm{otherwise}. \end{array} \right.\]

We define \(\takeWhile : \bool^A \times \lists{A} \rightarrow \lists{A}\) by \[\takeWhile(p,x) = \foldr(\nil)(\varphi(p))(x).\]

In Haskell:

takeWhile :: (List t) => (a -> Bool) -> t a -> t a
takeWhile p = foldr nil phi
  where
    phi a x = if eq (p a) true
      then cons a x
      else nil

As usual, since \(\takeWhile\) is defined directly in terms of foldr it is the unique solution to a system of functional equations.

Let \(A\) be a set. Then \(\takeWhile\) is the unique function \[f : \bool^A \times \lists{A} \rightarrow \lists{A}\] satisfying the following system of equations for all \(p : A \rightarrow \bool\), \(a \in A\), and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(p,\nil) = \nil \\ f(p,\cons(a,x)) = \bif{p(a)}{\cons(a,f(p,x))}{\nil}. \end{array}\right.\]

_test_takeWhile_nil :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> Bool)
_test_takeWhile_nil t =
  testName "takeWhile(p)(nil) == nil" $
  \p -> eq (takeWhile p nil) (nil `withTypeOf` t)


_test_takeWhile_cons :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> a -> t a -> Bool)
_test_takeWhile_cons t =
  testName "takeWhile(p)(cons(a,x)) == if(p(a),cons(a,takeWhile(p)(x),nil))" $
  \p a x -> eq
    (takeWhile p (cons a x))
    (if p a then cons a (takeWhile p x) else nil)

\(\takeWhile\) gives prefixes.

Let \(A\) be a set and \(p : A \rightarrow \bool\). For all \(x \in \lists{A}\), we have \[\prefix(\takeWhile(p,x),x) = \btrue.\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \prefix(\takeWhile(p,\nil),\nil) \\ & = & \prefix(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x \in \lists{A}\), and let \(a \in A\). We have \[\begin{eqnarray*} & & \prefix(\takeWhile(p,\cons(a,x),\cons(a,x))) \\ & = & \prefix(\bif{p(a)}{\cons(a,\takeWhile(p,x))}{\nil},\cons(a,x)) \\ & = & \bif{p(a)}{\prefix(\cons(a,\takeWhile(p,x)),\cons(a,x))}{\prefix(\nil,\cons(a,x))} \\ & = & \bif{p(a)}{\prefix(\takeWhile(p,x),x)}{\btrue} \\ & = & \bif{p(a)}{\btrue}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \btrue \end{eqnarray*}\] as needed.

_test_takeWhile_prefix :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_takeWhile_prefix _ =
  testName "prefix(takeWhile(p,x),x) == true" $
  \p x -> eq (prefix (takeWhile p x) x) true

So \(\takeWhile\) also gives a sublists.

Let \(A\) be a set, with \(p : A \rightarrow \bool\) and \(x \in \lists{A}\). Then we have \[\sublist(\takeWhile(k,x),x) = \btrue.\]

We have \[\prefix(\takeWhile(k,x),x) = \btrue,\] so \[\infix(\takeWhile(k,x),x) = \btrue,\] so \[\sublist(\takeWhile(k,x),x) = \btrue\] as claimed.

_test_takeWhile_sublist :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_takeWhile_sublist _ =
  testName "sublist(takeWhile(p,x),x) == true" $
  \p x -> eq (sublist (takeWhile p x) x) true

\(\takeWhile\) is idempotent.

Let \(A\) be a set with \(p : A \rightarrow \bool\). Then for all \(x \in \lists{A}\) we have \[\takeWhile(p,\takeWhile(p,x)) = \takeWhile(p,x).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), note that \[\begin{eqnarray*} & & \takeWhile(p,\takeWhile(p,x)) \\ & = & \takeWhile(p,\takeWhile(p,\nil)) \\ & = & \takeWhile(p,\nil) \\ & = & \takeWhile(p,x) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x \in \lists{A}\), and let \(a \in A\). If \(p(a) = \btrue\), we have \[\begin{eqnarray*} & & \takeWhile(p,\takeWhile(p,\cons(a,x))) \\ & = & \takeWhile(p,\cons(a,\takeWhile(p,x))) \\ & = & \cons(a,\takeWhile(p,\takeWhile(p,x))) \\ & = & \cons(a,\takeWhile(p,x)) \\ & = & \takeWhile(p,\cons(a,x)) \end{eqnarray*}\] as needed. If \(p(a) = \bfalse\), we have \[\begin{eqnarray*} & & \takeWhile(p,\takeWhile(p,\cons(a,x))) \\ & = & \takeWhile(p,\nil) \\ & = & \nil \\ & = & \takeWhile(p,\cons(a,x)) \end{eqnarray*}\] as needed.

_test_takeWhile_idempotent :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_takeWhile_idempotent _ =
  testName "takeWhile(p,takeWhile(p,x)) == takeWhile(p,x)" $
  \p x -> eq (takeWhile p (takeWhile p x)) (takeWhile p x)

\(\takeWhile\) commutes with itself (kind of).

Let \(A\) be a set with \(p\) and \(q\) mappings \(A \rightarrow \bool\). Then for all \(x \in \lists{A}\) we have \[\takeWhile(p,\takeWhile(q,x)) = \takeWhile(q,\takeWhile(p,x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), note that \[\begin{eqnarray*} & & \takeWhile(p,\takeWhile(q,x)) \\ & = & \takeWhile(p,\takeWhile(q,\nil)) \\ & = & \takeWhile(p,\nil) \\ & = & \nil \\ & = & \takeWhile(q,\nil) \\ & = & \takeWhile(q,\takeWhile(p,\nil)) \\ & = & \takeWhile(q,\takeWhile(p,x)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x \in \lists{A}\), and let \(a \in A\). If \(p(a) = \btrue\), we have \[\begin{eqnarray*} & & \takeWhile(p,\takeWhile(q,\cons(a,x))) \\ & = & \takeWhile(p,\bif{q(a)}{\cons(a,\takeWhile(q,x))}{\nil}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \bif{q(a)}{\takeWhile(p,\cons(a,\takeWhile(q,x)))}{\takeWhile(p,\nil)} \\ & = & \bif{q(a)}{\bif{p(a)}{\cons(a,\takeWhile(p,\takeWhile(q,x)))}{\nil}}{\nil} \\ & = & \bif{q(a)}{\bif{p(a)}{\cons(a,\takeWhile(q,\takeWhile(p,x)))}{\nil}}{\bif{p(a)}{\nil}{\nil}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-ifnest} = & \bif{p(a)}{\bif{q(a)}{\cons(a,\takeWhile(q,\takeWhile(p,x)))}{\nil}}{\bif{q(a)}{\nil}{\nil}} \\ & = & \bif{p(a)}{\bif{q(a)}{\cons(a,\takeWhile(q,\takeWhile(p,x)))}{\nil}}{\nil} \\ & = & \bif{p(a)}{\takeWhile(q,\cons(a,\takeWhile(p,x)))}{\takeWhile(q,\nil)} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \takeWhile(q,\bif{p(a)}{\cons(a,\takeWhile(p,x))}{\nil}) \\ & = & \takeWhile(q,\takeWhile(p,\cons(a,x))) \end{eqnarray*}\] as needed.

_test_takeWhile_commutes :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> (a -> Bool) -> t a -> Bool)
_test_takeWhile_commutes _ =
  testName "takeWhile(p,takeWhile(q,x)) == takeWhile(q,takeWhile(p,x))" $
  \p q x ->
    eq (takeWhile p (takeWhile q x)) (takeWhile q (takeWhile p x))

Now for \(\dropWhile\). This function should drop the longest prefix satisfying some predicate, again with signature \(\bool^A \times \lists{A} \rightarrow \lists{A}\). If we try defining this using foldr in the “obvious” way, we run into trouble, where the \(\varphi\) parameter needs to have its argument and eat it too. (try it!) One way around this is the trick we used to define \(\zip\).

Suppose \[\dropWhile(p,x) = \foldr(e)(\varphi)(x)(x)\] for some \(e\) and \(\varphi\). To make the types work out, we need \[e \in \lists{A}^{\lists{A}}\] and \[\varphi : A \times \lists{A}^{\lists{A}} \rightarrow \lists{A}^{\lists{A}};\] now \[\begin{eqnarray*} & & \nil \\ & = & \dropWhile(p,\nil) \\ & = & \foldr(e)(\varphi)(\nil)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & e(\nil) \end{eqnarray*}\] and \[\begin{eqnarray*} & & \varphi(a,\foldr(e)(\varphi)(x))(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \foldr(e)(\varphi)(\cons(a,x))(\cons(a,x)) \\ & = & \dropWhile(p,\cons(a,x)) \\ & = & \bif{p(a)}{\dropWhile(p,x)}{\cons(a,x)} \end{eqnarray*}\]

(that last line is why using a plain fold doesn’t work.) In cases like this, the consuming fold is handy.

Let \(A\) be a set with \(p : A \rightarrow \bool\). Define \(\sigma : A \times \lists{A} \times \lists{A} \rightarrow \lists{A}\) by \[\sigma(a,x,y) = \bif{p(a)}{y}{\cons(a,x)}.\] Now define \(\dropWhile : \bool^A \rightarrow {\lists{A}}^{\lists{A}}\) by \[\dropWhile(p) = \cfoldr(\nil)(\sigma).\]

In Haskell:

dropWhile :: (List t) => (a -> Bool) -> t a -> t a
dropWhile p = cfoldr nil sigma
  where
    sigma a x y = if p a then y else cons a x

Because \(\dropWhile\) is defined as a consuming fold, it can be characterized as the unique solution to a system of functional equations.

Let \(A\) be a set, with \(p\) a predicate on \(A\). Then \(\dropWhile(p)\) is the unique map \(f : \lists{A} \rightarrow \lists{A}\) satisfying the following equations for all \(a \in A\) and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(\nil) = \nil \\ f(\cons(a,x)) = \bif{p(a)}{f(x)}{\cons(a,x)} \end{array}\right.\]

_test_dropWhile_nil :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> Bool)
_test_dropWhile_nil t =
  testName "dropWhile(p)(nil) == nil" $
  \p -> eq (dropWhile p nil) (nil `withTypeOf` t)


_test_dropWhile_cons :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> a -> t a -> Bool)
_test_dropWhile_cons t =
  testName "dropWhile(p)(cons(a,x)) == if(p(a),dropWhile(p)(x),cons(a,x))" $
  \p a x -> eq
    (dropWhile p (cons a x))
    (if p a then dropWhile p x else cons a x)

Now \(\dropBut\) is a \(\suffix\):

Let \(A\) be a set. For all \(x \in \lists{A}\) and \(p : A \rightarrow \bool\), we have \[\suffix(\dropWhile(p)(x),x) = \btrue.\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \suffix(\dropWhile(p)(\nil),\nil) \\ & = & \suffix(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#thm-suffix-nil-left} = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). By the inductive hypothesis we have \(\suffix(\dropWhile(p)(x),x)\), so that \(\suffix(\dropWhile(p)(x),\cons(a,x))\). Now \[\begin{eqnarray*} & & \suffix(\dropWhile(p)(\cons(a,x)),\cons(a,x)) \\ & = & \suffix(\bif{p(a)}{\dropWhile(p)(x)}{\cons(a,x)},\cons(a,x)) \\ & = & \bif{p(a)}{\suffix(\dropWhile(p)(x),\cons(a,x))}{\suffix(\cons(a,x),\cons(a,x))} \\ & = & \bif{p(a)}{\btrue}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \btrue \end{eqnarray*}\] as needed.

_test_dropWhile_suffix :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_dropWhile_suffix _ =
  testName "suffix(dropWhile(p)(x),x) == true" $
  \p x -> eq (suffix (dropWhile p x) x) true

Like \(\take\) and \(\drop\), \(\takeWhile\) and \(\dropWhile\) give a kind of \(\cat\)-factorization.

Let \(A\) be a set and \(p : A \rightarrow \bool\). For all \(x \in \lists{A}\) we have \[x = \cat(\takeWhile(p)(x),\dropWhile(p)(x)).\]

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

_test_takeWhile_dropWhile_cat :: (List t, Equal a, Equal (t a))
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_takeWhile_dropWhile_cat _ =
  testName "cat(takeWhile(p)(x),dropWhile(p)(x)) == x" $
  \p x -> eq (cat (takeWhile p x) (dropWhile p x)) x

Testing

Suite:

_test_takewhile_dropwhile ::
  ( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
  , TypeName (t a), List t
  , TypeName n, Natural n, Show n, Arbitrary n
  , Equal (t a), Show (t a), Arbitrary (t a)
  ) => Int -> Int -> t a -> n -> IO ()
_test_takewhile_dropwhile size cases t k = do
  testLabel1 "takeWhile & dropWhile" t

  let args = testArgs size cases

  runTest args (_test_takeWhile_nil t)
  runTest args (_test_takeWhile_cons t)
  runTest args (_test_takeWhile_prefix t)
  runTest args (_test_takeWhile_sublist t)
  runTest args (_test_takeWhile_idempotent t)
  runTest args (_test_takeWhile_commutes t)

  runTest args (_test_dropWhile_nil t)
  runTest args (_test_dropWhile_cons t)
  runTest args (_test_dropWhile_suffix t)

  runTest args (_test_takeWhile_dropWhile_cat t)

Main:

main_takewhile_dropwhile :: IO ()
main_takewhile_dropwhile = do
  _test_takewhile_dropwhile 20 100 (nil :: ConsList Bool)  (zero :: Unary)
  _test_takewhile_dropwhile 20 100 (nil :: ConsList Unary) (zero :: Unary)