TakeBut and DropBut

Posted on 2017-12-15 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 TakeButAndDropBut
  ( takeBut, dropBut, _test_takebut_dropbut, main_takebut_dropbut
  ) where

import Testing
import Booleans
import NaturalNumbers
import Lists
import Snoc
import Reverse
import Cat
import PrefixAndSuffix
import Sublist
import TakeAndDrop

Today we’ll define two functions, \(\takeBut\) and \(\dropBut\), analogous to \(\take\) and \(\drop\), but acting from the end of the list rather than from the beginning. We’d like \(\takeBut\) to have a signature like \[\takeBut : \nats \rightarrow {\lists{A}}^{\lists{A}}\] such that \(\takeBut(k)(x)\) is obtained by lopping off the last \(k\) items in \(x\), and similarly \(\dropBut(k)(x)\) lops off all but the last \(k\) items. The simplest way to do this is with \(\take\), \(\drop\), and \(\rev\); explicit recursion is not required.

Let \(A\) be a set. We define \(\takeBut : \nats \rightarrow {\lists{A}}^{\lists{A}}\) by \[\takeBut(k)(x) = \rev(\drop(k)(\rev(x)))\] and define \(\dropBut : \nats \rightarrow {\lists{A}}^{\lists{A}}\) by \[\dropBut(k)(x) = \rev(\take(k)(\rev(x))).\]

In Haskell:

takeBut :: (Natural n, List t) => n -> t a -> t a
takeBut k x = rev (drop k (rev x))

dropBut :: (Natural n, List t) => n -> t a -> t a
dropBut k x = rev (take k (rev x))

The defining equations for \(\drop\) have \(\takeBut\) equivalents.

Let \(A\) be a set, with \(x \in \lists{A}\), \(a \in A\), and \(k \in \nats\). Then we have the following.

\(\takeBut(\zero)(x) = x\).
\(\takeBut(\next(k))(\nil) = \nil\).
\(\takeBut(\next(k))(\snoc(a,x)) = \takeBut(k)(x)\).

We have \[\begin{eqnarray*} & & \takeBut(\zero)(x) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-takebut} = & \rev(\drop(\zero)(\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-drop-zero} = & \rev(\rev(x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-involution} = & x \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \takeBut(\next(k))(\nil) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-takebut} = & \rev(\drop(\next(k))(\rev(\nil))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \rev(\drop(\next(k))(\nil)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-drop-next-nil} = & \rev(\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \nil \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \takeBut(\next(k))(\snoc(a,x)) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-takebut} = & \rev(\drop(\next(k))(\rev(\snoc(a,x)))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-snoc} = & \rev(\drop(\next(k))(\cons(a,\rev(x)))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-drop-next-cons} = & \rev(\drop(k)(\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-takebut} = & \takeBut(k,x) \end{eqnarray*}\] as claimed.

_test_takeBut_zero :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (t a -> Bool)
_test_takeBut_zero _ n =
  testName "takeBut(zero)(x) == x" $
  \x -> eq (takeBut (zero `withTypeOf` n) x) x


_test_takeBut_next_nil :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (n -> Bool)
_test_takeBut_next_nil t _ =
  testName "takeBut(next(n))(nil) == nil" $
  \n -> eq (takeBut (next n) nil) (nil `withTypeOf` t)


_test_takeBut_next_snoc :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (n -> a -> t a -> Bool)
_test_takeBut_next_snoc _ _ =
  testName "takeBut(next(n))(snoc(a,x)) == takeBut(k)(x)" $
  \n a x -> eq
    (takeBut (next n) (snoc a x))
    (takeBut n x)

\(\takeBut\) is a prefix.

Let \(A\) be a set. For all \(x \in \lists{A}\) and \(k \in \nats\), we have \[\prefix(\takeBut(k,x),x) = \btrue.\]

We have \[\begin{eqnarray*} & & \prefix(\takeBut(k,x),x) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-takebut} = & \prefix(\rev(\drop(k,\rev(x))),x) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-involution} = & \prefix(\rev(\drop(k,\rev(x))),\rev(\rev(x))) \\ & = & \suffix(\drop(k,\rev(x)),\rev(x)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#thm-drop-suffix} = & \btrue \end{eqnarray*}\] as needed.

_test_takeBut_prefix :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (n -> t a -> Bool)
_test_takeBut_prefix _ _ =
  testName "prefix(takeBut(k,x),x) == true" $
  \k x -> eq (prefix (takeBut k x) x) true

So \(\takeBut\) is a sublist:

Let \(A\) be a set, with \(x \in \lists{A}\) and \(k \in \nats\). Then we have \[\sublist(\takeBut(k,x),x) = \btrue.\]

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

_test_takeBut_sublist :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (n -> t a -> Bool)
_test_takeBut_sublist _ _ =
  testName "sublist(takeBut(k,x),x) == true" $
  \k x -> eq (sublist (takeBut k x) x) true

Now for \(\dropBut\).

Let \(A\) be a set. For all \(a \in A\), \(x \in \lists{A}\), and \(k \in \nats\), we have the following.

\(\dropBut(\zero,x) = \nil\).
\(\dropBut(\next(k),\nil) = \nil\).
\(\dropBut(\next(k),\snoc(a,x)) = \snoc(a,\dropBut(k,x))\).

We have \[\begin{eqnarray*} & & \dropBut(\zero,x) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-dropbut} = & \rev(\take(\zero,\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-zero} = & \rev(\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \nil \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \dropBut(k,\nil) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-dropbut} = & \rev(\take(k,\rev(\nil))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \rev(\take(k,\nil)) \\ & = & \rev(\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \nil \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \dropBut(\next(k),\snoc(a,x)) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-dropbut} = & \rev(\take(\next(k),\rev(\snoc(a,x)))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-snoc} = & \rev(\take(\next(k),\cons(a,\rev(x)))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-cons} = & \rev(\cons(a,\take(k,\rev(x)))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \snoc(a,\rev(\take(k,\rev(x)))) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-dropbut} = & \snoc(a,\dropBut(k,x)) \end{eqnarray*}\] as claimed.

_test_dropBut_zero :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (t a -> Bool)
_test_dropBut_zero _ n =
  testName "dropBut(zero)(x) == nil" $
  \x -> eq (dropBut (zero `withTypeOf` n) x) nil


_test_dropBut_next_nil :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (n -> Bool)
_test_dropBut_next_nil t _ =
  testName "dropBut(next(n))(nil) == nil" $
  \n -> eq (dropBut (next n) nil) (nil `withTypeOf` t)


_test_dropBut_next_snoc :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (n -> a -> t a -> Bool)
_test_dropBut_next_snoc _ _ =
  testName "dropBut(next(n))(snoc(a,x)) == snoc(a,dropBut(k)(x))" $
  \n a x -> eq
    (dropBut (next n) (snoc a x))
    (snoc a (dropBut n x))

\(\dropBut\) is a \(\suffix\).

Let \(A\) be a set. For all \(x \in \lists{A}\) and \(k \in \nats\), we have \[\suffix(\dropBut(k,x),x) = \btrue.\]

We have \[\begin{eqnarray*} & & \suffix(\dropBut(k,x),x) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-dropbut} = & \suffix(\rev(\take(k,\rev(x))),x) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-involution} = & \suffix(\rev(\take(k,\rev(x))),\rev(\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#thm-prefix-rev} = & \prefix(\take(k,\rev(x)),\rev(x)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#thm-take-prefix} = & \btrue \end{eqnarray*}\] as claimed.

_test_dropBut_suffix :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (n -> t a -> Bool)
_test_dropBut_suffix _ _ =
  testName "suffix(dropBut(k,x),x) == true" $
  \k x -> eq (suffix (dropBut k x) x) true

\(\dropBut\) is idempotent.

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

Note that \[\begin{eqnarray*} & & \dropBut(k,\dropBut(k,x)) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-dropbut} = & \dropBut(k,\rev(\take(k,\rev(x)))) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-dropbut} = & \rev(\take(k,\rev(\rev(\take(k,\rev(x)))))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-involution} = & \rev(\take(k,\take(k,\rev(x)))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#thm-take-idempotent} = & \rev(\take(k,\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-dropbut} = & \dropBut(k,x) \end{eqnarray*}\] as claimed.

_test_dropBut_idempotent :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (n -> t a -> Bool)
_test_dropBut_idempotent _ _ =
  testName "dropBut(k,dropBut(k,x)) == dropBut(k,x)" $
  \k x -> eq (dropBut k (dropBut k x)) (dropBut k x)

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

Let \(A\) be a set. For all \(x \in \lists{A}\) and \(k \in \nats\), we have \[x = \cat(\takeBut(k,x),\dropBut(k,x)).\]

We have \[\begin{eqnarray*} & & \cat(\takeBut(k,x),\dropBut(k,x)) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-takebut} = & \cat(\rev(\drop(k,\rev(x))),\dropBut(k,x)) \\ & \href{/posts/arithmetic-made-difficult/TakeButAndDropBut.html#def-dropbut} = & \cat(\rev(\drop(k,\rev(x))),\rev(\take(k,\rev(x)))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-rev-cat-antidistribute} = & \rev(\cat(\take(k,\rev(x)),\drop(k,\rev(x)))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#thm-take-drop-cat} = & \rev(\rev(x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-involution} = & x \end{eqnarray*}\] as claimed.

_test_takeBut_dropBut_cat :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (n -> t a -> Bool)
_test_takeBut_dropBut_cat _ _ =
  testName "cat(takeBut(k,x),dropBut(k,x)) == x" $
  \k x -> eq (cat (takeBut k x) (dropBut k x)) x

Testing

Suite:

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

  let args = testArgs size cases

  runTest args (_test_takeBut_zero t k)
  runTest args (_test_takeBut_next_nil t k)
  runTest args (_test_takeBut_next_snoc t k)
  runTest args (_test_takeBut_prefix t k)
  runTest args (_test_takeBut_sublist t k)

  runTest args (_test_dropBut_zero t k)
  runTest args (_test_dropBut_next_nil t k)
  runTest args (_test_dropBut_next_snoc t k)
  runTest args (_test_dropBut_suffix t k)
  runTest args (_test_dropBut_idempotent t k)

  runTest args (_test_takeBut_dropBut_cat t k)

Main:

main_takebut_dropbut :: IO ()
main_takebut_dropbut = do
  _test_takebut_dropbut 20 100 (nil :: ConsList Bool)  (zero :: Unary)
  _test_takebut_dropbut 20 100 (nil :: ConsList Unary) (zero :: Unary)