# TakeBut and DropBut

Posted on 2017-12-15 by nbloomf

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

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.

1. $$\takeBut(\zero)(x) = x$$.
2. $$\takeBut(\next(k))(\nil) = \nil$$.
3. $$\takeBut(\next(k))(\snoc(a,x)) = \takeBut(k)(x)$$.
1. 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.
2. 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.
3. 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. 1. $$\dropBut(\zero,x) = \nil$$. 2. $$\dropBut(\next(k),\nil) = \nil$$. 3. $$\dropBut(\next(k),\snoc(a,x)) = \snoc(a,\dropBut(k,x))$$. 1. 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. 2. 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. 3. 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)