Tails and Inits

Posted on 2017-05-12 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 TailsAndInits
  ( tails, inits, _test_tails_inits, main_tails_inits
  ) where

import Testing
import Tuples
import NaturalNumbers
import Lists
import ConsumingFold
import Snoc
import Reverse
import Length
import Map
import PrefixAndSuffix
import LongestCommonPrefix
import AllAndAny

Today we’ll construct the lists of all suffixes (\(\tails\)) and prefixes (\(\inits\)) of a list. Starting with \(\tails\): this function should have a signature like \[\lists{A} \rightarrow \lists{\lists{A}}.\]

Let \(A\) be a set. Let \(\gamma = \cons(\nil,\nil)\), and define \(\sigma : A \times \lists{A} \times \lists{\lists{A}} \rightarrow \lists{\lists{A}}\) by \[\sigma(a,x,z) = \cons(\cons(a,x),z).\] Now define \(\tails : \lists{A} \rightarrow \lists{\lists{A}}\) by \[\tails = \cfoldr(\gamma)(\sigma).\]

In Haskell:

tails :: (List t) => t a -> t (t a)
tails = cfoldr gamma sigma
  where
    gamma = cons nil nil
    sigma a x z = cons (cons a x) z

Since \(\tails\) is defined as a \(\cfoldr(\ast)(\ast)\), it is the unique solution to a system of functional equations.

Let \(A\) be a set. \(\tails\) is the unique map \(f : \lists{A} \rightarrow \lists{\lists{A}}\) which satisfies 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)) = \cons(\cons(a,x),f(x)) \end{array}\right.\]

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


_test_tails_cons :: (List t, Equal a, Equal (t (t a)))
  => t a -> Test (a -> t a -> Bool)
_test_tails_cons _ =
  testName "tails(cons(a,x)) == cons(cons(a,x),tails(x))" $
  \a x -> eq (tails (cons a x)) (cons (cons a x) (tails x))

Special cases.

Let \(A\) be a sets. For all \(a,b \in A\) we have the following.

\(\tails(\cons(a,\nil)) = \cons(\cons(a,\nil),\cons(\nil,\nil))\).
\(\tails(\cons(a,\cons(b,\nil))) = \cons(\cons(a,\cons(b,\nil)),\cons(\cons(b,\nil),\cons(\nil,\nil)))\).

Note that \[\begin{eqnarray*} & & \tails(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#cor-tails-cons} = & \cons(\cons(a,\nil),\tails(\nil)) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#cor-tails-nil} = & \cons(\cons(a,\nil),\cons(\nil,\nil)) \end{eqnarray*}\] as claimed.
Note that \[\begin{eqnarray*} & & \tails(\cons(a,\cons(b,\nil))) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#cor-tails-cons} = & \cons(\cons(a,\cons(b,\nil)),\tails(\cons(b,\nil))) \\ & = & \cons(\cons(a,\cons(b,\nil)),\cons(\cons(a,\nil),\cons(\nil,\nil))) \end{eqnarray*}\] as claimed.

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


_test_tails_double :: (List t, Equal a, Equal (t (t a)))
  => t a -> Test (a -> a -> Bool)
_test_tails_double t =
  testName "tails(cons(a,cons(b,nil))) == cons(cons(a,cons(b,nil)),cons(cons(b,nil),cons(nil,nil)))" $
  \a b -> eq
    (tails (cons a (cons b (nil `withTypeOf` t))))
    (cons (cons a (cons b nil)) (cons (cons b nil) (cons nil nil)))

\(\tails\) interacts with \(\map\).

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

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

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

\(\tails\) interacts with \(\length\).

Let \(A\) be a set. For all \(x \in \lists{A}\) we have \[\length(\tails(x)) = \next(\length(x)).\] In particular, \(\tails{x} \neq \nil\).

We proceed by list induction. For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \length(\tails(\nil)) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#cor-tails-nil} = & \length(\cons(\nil,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-length-singleton} = & \next(\zero) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \next(\length(\nil)) \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Then we have \[\begin{eqnarray*} & & \length(\tails(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#cor-tails-cons} = & \length(\cons(\cons(a,x),\tails(x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \next(\length(\tails(x))) \\ & = & \next(\next(\length(x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \next(\length(\cons(a,x))) \end{eqnarray*}\] as claimed.

_test_tails_length
  :: (List t, Equal a, Natural n, Equal n, Equal (t a))
  => t a -> n -> Test (t a -> Bool)
_test_tails_length _ n =
  testName "length(tails(x)) == next(length(x))" $
  \x -> eq (length (tails x)) (next (length x `withTypeOf` n))

\(\tails\) interacts with \(\snoc\).

Let \(A\) be a set. For all \(x \in \lists{A}\) and \(a \in A\) we have \[\tails(\snoc(a,x)) = \snoc(\nil,\map(\snoc(a))(\tails(x))).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \snoc(\nil,\map(\snoc(a))(\tails(x))) \\ & = & \snoc(\nil,\map(\snoc(a))(\tails(\nil))) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#cor-tails-nil} = & \snoc(\nil,\map(\snoc(a))(\cons(\nil,\nil))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \snoc(\nil,\cons(\snoc(a,\nil),\map(\snoc(a))(\nil))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \snoc(\nil,\cons(\snoc(a,\nil),\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \cons(\snoc(a,\nil),\snoc(\nil,\nil)) \\ & = & \cons(\cons(a,\nil),\cons(\nil,\nil)) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#thm-tails-one} = & \tails(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \tails(\snoc(a,\nil)) \\ & = & \tails(\snoc(a,x)) \end{eqnarray*}\] as claimed. Suppose now that the equality holds for some \(x\) and let \(b \in A\). Now \[\begin{eqnarray*} & & \tails(\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \tails(\cons(b,\snoc(a,x))) \\ & = & \cons(\cons(b,\snoc(a,x)),\tails(\snoc(a,x))) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#thm-tails-snoc} = & \cons(\cons(b,\snoc(a,x)),\snoc(\nil,\map(\snoc(a))(\tails(x)))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \snoc(\nil,\cons(\cons(b,\snoc(a,x)),\map(\snoc(a))(\tails(x)))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \snoc(\nil,\cons(\snoc(a,\cons(b,x)),\map(\snoc(a))(\tails(x)))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \snoc(\nil,\map(\snoc(a))(\cons(\cons(b,x),\tails(x)))) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#cor-tails-cons} = & \snoc(\nil,\map(\snoc(a))(\tails(\cons(b,x)))) \end{eqnarray*}\] as needed.

_test_tails_snoc :: (List t, Equal a, Equal (t (t a)))
  => t a -> Test (a -> t a -> Bool)
_test_tails_snoc _ =
  testName "tails(snoc(a,x)) == snoc(nil,map(snoc(a,-))(tails(x)))" $
  \a x -> eq (tails (snoc a x)) (snoc nil (map (snoc a) (tails x)))

And \(\tails(x)\) consists of suffixes.

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

We proceed by list induction on \(x\). For the base case \(x = \nil\), note that \[\begin{eqnarray*} & & \all(\suffix(-,x),\tails(x)) \\ & = & \all(\suffix(-,\nil),\cons(\nil,\nil)) \\ & = & \band(\suffix(\nil,\nil),\all(\suffix(-,\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 equality holds for some \(x\) and let \(a \in A\). Note that if \(\suffix(u,x) = \btrue\) then \(\suffix(u,\cons(a,x)) = \btrue\). Using the inductive hypothesis, we have \[\begin{eqnarray*} & & \btrue \\ & = & \all(\suffix(-,x),\tails(x)) \\ & = & \all(\suffix(-,\cons(a,x)),\tails(x)) \\ & = & \band(\btrue,\all(\suffix(-,\cons(a,x)),\tails(x))i) \\ & = & \band(\suffix(\cons(a,x),\cons(a,x)),\all(\suffix(-,\cons(a,x)),\tails(x))) \\ & = & \all(\suffix(-,\cons(a,x)),\cons(\cons(a,x),\tails(x))) \\ & = & \all(\suffix(-,\cons(a,x)),\tails(\cons(a,x))) \end{eqnarray*}\] as needed.

_test_tails_suffix :: (List t, Equal a, Equal (t (t a)))
  => t a -> Test (t a -> Bool)
_test_tails_suffix _ =
  testName "all(suffix(_,x))(tails(x))" $
  \x -> all (\y -> suffix y x) (tails x)

Next we’ll define \(\inits\) in terms of \(\tails\).

Let \(A\) be a sets. We define \(\inits : \lists{A} \rightarrow \lists{\lists{A}}\) by \[\inits(x) = \rev(\map(\rev)(\tails(\rev(x)))).\]

In Haskell:

inits :: (List t) => t a -> t (t a)
inits = rev . map rev . tails . rev

And likewise, \(\tails\) has an expression in terms of \(\inits\).

Let \(A\) be a set. For all \(x \in \lists{A}\) we have \[\tails(x) = \map(\rev)(\rev(\inits(\rev(x)))).\]

Note that \[\begin{eqnarray*} & & \map(\rev) \circ \rev \circ \inits \circ \rev \\ & = & \map(\rev) \circ \rev \circ \rev \circ \map(\rev) \circ \tails \circ \rev \circ \rev \\ & = & \map(\rev) \circ \map(\rev) \circ \tails \\ & = & \compose(\map(\compose(\rev)(\rev)))(\tails) \\ & = & \compose(\map(\id))(\tails) \\ & = & \tails \end{eqnarray*}\] as needed.

_test_inits_tails :: (List t, Equal a, Equal (t (t a)))
  => t a -> Test (t a -> Bool)
_test_inits_tails _ =
  testName "tails(x) == rev(map(rev)(inits(rev(x))))" $
  \x -> eq (tails x) (map rev (rev (inits (rev x))))

\(\inits\) interacts with \(\cons\).

Let \(A\) be a set. For all \(a \in A\) and \(x \in \lists{A}\), we have \[\inits(\cons(a,x)) = \cons(\nil,\map(\cons(a))(\inits(x))).\]

Note that \[\begin{eqnarray*} & & \inits(\cons(a,x)) \\ & = & \rev(\map(\rev)(\tails(\rev(\cons(a,x))))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \rev(\map(\rev)(\tails(\snoc(a,\rev(x))))) \\ & = & \rev(\map(\rev)(\snoc(\nil,\map(\snoc(a))(\tails(\rev(a)))))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-map-snoc} = & \rev(\snoc(\rev(\nil),\map(\rev)(\map(\snoc(a))(\tails(\rev(a)))))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \rev(\snoc(\nil,\map(\rev)(\map(\snoc(a))(\tails(\rev(a)))))) \\ & = & \rev(\snoc(\nil,\map(\compose(\rev)(\snoc(a)))(\tails(\rev(a))))) \\ & = & \rev(\snoc(\nil,\map(\cons(a) \circ \rev)(\tails(\rev(a))))) \\ & = & \rev(\snoc(\nil,\map(\cons(a))(\map(\rev)(\tails(\rev(a)))))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-snoc} = & \cons(\nil,\rev(\map(\cons(a))(\map(\rev)(\tails(\rev(a)))))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-map-rev} = & \cons(\nil,\map(\cons(a))(\rev(\map(\rev)(\tails(\rev(a)))))) \\ & = & \cons(\nil,\map(\cons(a))(\inits(x))) \end{eqnarray*}\] as claimed.

_test_inits_cons :: (List t, Equal a, Equal (t (t a)))
  => t a -> Test (a -> t a -> Bool)
_test_inits_cons _ =
  testName "inits(cons(a,x)) == cons(nil,map(cons(a,-))(inits(x)))" $
  \a x -> eq (inits (cons a x)) (cons nil (map (cons a) (inits x)))

\(\inits\) interacts with \(\map\).

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

Note that \[\begin{eqnarray*} & & \inits(\map(f)(x)) \\ & = & \rev(\map(\rev)(\tails(\rev(\map(f)(x))))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-map-rev} = & \rev(\map(\rev)(\tails(\map(f)(\rev(x))))) \\ & = & \rev(\map(\rev)(\map(\map(f))(\tails(\rev(x))))) \\ & = & \rev(\map(\compose(\rev)(\map(f)))(\tails(\rev(x)))) \\ & = & \rev(\map(\compose(\map(f))(\rev))(\tails(\rev(x)))) \\ & = & \rev(\map(\map(f))(\map(\rev)(\tails(\rev(x))))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-map-rev} = & \map(\map(f))(\rev(\map(\rev)(\tails(\rev(x))))) \\ & = & \map(\map(f))(\inits(x)) \end{eqnarray*}\] as claimed.

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

\(\inits\) interacts with \(\length\).

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

Note that \[\begin{eqnarray*} & & \length(\inits(x)) \\ & = & \length(\rev(\map(\rev)(\tails(\rev(x))))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-length-rev} = & \length(\map(\rev)(\tails(\rev(x)))) \\ & = & \length(\tails(\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#thm-length-tails} = & \next(\length(\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-length-rev} = & \next(\length(x)) \end{eqnarray*}\] as claimed.

_test_inits_length :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (t a -> Bool)
_test_inits_length _ n =
  testName "length(inits(x)) == next(length(x))" $
  \x -> eq (length (inits x)) (next (length x `withTypeOf` n))

\(\inits\) distributes over \(\lcp\).

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

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have two possibilities for \(y\). If \(y = \nil\) we have \[\begin{eqnarray*} & & \lcp(\inits(x),\inits(y)) \\ & = & \lcp(\inits(\nil),\inits(\nil)) \\ & = & \lcp(\cons(\nil,\nil),\cons(\nil,\nil)) \\ & \href{/posts/arithmetic-made-difficult/LongestCommonPrefix.html#thm-lcp-idempotent} = & \cons(\nil,\nil) \end{eqnarray*}\] and if \(y = \cons(a,u)\), we have \[\begin{eqnarray*} & & \lcp(\inits(x),\inits(y)) \\ & = & \lcp(\inits(\nil),\inits(\cons(a,u))) \\ & = & \lcp(\cons(\nil,\nil),\cons(\nil,\map(\cons(a,-))(\inits(x)))) \\ & = & \cons(\nil,\lcp(\nil,\map(\cons(a,-))(\inits(x)))) \\ & = & \cons(\nil,\nil) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(y\) for some \(x\), and let \(a \in A\). We have two possibilities for \(y\). If \(y = \nil\), we have \[\begin{eqnarray*} & & \inits(\lcp(\cons(a,x),\nil)) \\ & \href{/posts/arithmetic-made-difficult/LongestCommonPrefix.html#thm-lcp-commutative} = & \inits(\lcp(\nil,\cons(a,x))) \\ & = & \lcp(\tails(\nil),\tails(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/LongestCommonPrefix.html#thm-lcp-commutative} = & \lcp(\tails(\cons(a,x)),\tails(\nil)) \end{eqnarray*}\] as needed. Suppose then that \(y = \cons(b,u)\). If \(b = a\), note that \(\cons(a,-)\) is injective, so that \[\begin{eqnarray*} & & \lcp(\tails(\cons(a,x)),\tails(y)) \\ & = & \lcp(\tails(\cons(a,x)),\tails(\cons(b,u))) \\ & = & \lcp(\cons(\nil,\map(\cons(a,-))(\tails(x))),\cons(\nil,\map(\cons(b,-))(\tails(u)))) \\ & = & \lcp(\cons(\nil,\map(\cons(a,-))(\tails(x))),\cons(\nil,\map(\cons(a,-))(\tails(u)))) \\ & = & \cons(\nil,\lcp(\map(\cons(a,-))(\tails(x)),\map(\cons(a,-))(\tails(u)))) \\ & = & \cons(\nil,\map(\cons(a,-))(\lcp(\tails(x),\tails(u)))) \\ & = & \cons(\nil,\map(\cons(a,-))(\tails(\lcp(x,u)))) \\ & = & \tails(\cons(a,\lcp(x,u))) \\ & = & \tails(\lcp(\cons(a,x),\cons(a,u))) \\ & = & \tails(\lcp(\cons(a,x),\cons(b,u))) \\ & = & \tails(\lcp(\cons(a,x),y)) \end{eqnarray*}\] as needed. If \(b \neq a\), we instead, since \(\cons(a,x) \neq \cons(b,x)\) for all \(x\), we have \[\begin{eqnarray*} & & \lcp(\tails(\cons(a,x)),\tails(y)) \\ & = & \lcp(\tails(\cons(a,x)),\tails(\cons(b,u))) \\ & = & \lcp(\cons(\nil,\map(\cons(a,-))(\tails(x))),\cons(\nil,\map(\cons(b,-))(\tails(u)))) \\ & = & \cons(\nil,\lcp(\map(\cons(a,-))(\tails(x)),\map(\cons(b,-))(\tails(u)))) \\ & = & \cons(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#cor-tails-nil} = & \tails(\nil) \\ & = & \tails(\lcp(\cons(a,x),\cons(b,u))) \\ & = & \tails(\lcp(\cons(a,x),y)) \end{eqnarray*}\] as needed.

_test_inits_lcp :: (List t, Equal a, Equal (t a), Equal (t (t a)))
  => t a -> Test (t a -> t a -> Bool)
_test_inits_lcp _ =
  testName "inits(lcp(x,y)) == lcp(inits(x),inits(y))" $
  \x y -> eq (inits (lcp x y)) (lcp (inits x) (inits y))

And \(\tails\) distributes over \(\lcs\).

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

Note that \(\rev\) is injective, so that \[\begin{eqnarray*} & & \tails(\lcs(x,y)) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#thm-tails-rev} = & \map(\rev)(\rev(\inits(\rev(\lcs(x,y))))) \\ & = & \map(\rev)(\rev(\inits(\lcp(\rev(x),\rev(y))))) \\ & \href{/posts/arithmetic-made-difficult/TailsAndInits.html#thm-inits-lcp} = & \map(\rev)(\rev(\lcp(\inits(\rev(x)),\inits(\rev(y))))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-map-rev} = & \rev(\map(\rev)(\lcp(\inits(\rev(x)),\inits(\rev(y))))) \\ & = & \rev(\lcp(\map(\rev)(\inits(\rev(x))),\map(\rev)(\inits(\rev(y))))) \\ & = & \lcs(\rev(\map(\rev)(\inits(\rev(x)))),\rev(\map(\rev)(\inits(\rev(y))))) \\ & = & \lcs(\tails(x),\tails(y)) \end{eqnarray*}\] as claimed.

_test_tails_lcs :: (List t, Equal a, Equal (t a), Equal (t (t a)))
  => t a -> Test (t a -> t a -> Bool)
_test_tails_lcs _ =
  testName "tails(lcs(x,y)) == lcs(tails(x),tails(y))" $
  \x y -> eq (tails (lcs x y)) (lcs (tails x) (tails y))

Testing

Suite:

_test_tails_inits ::
  ( TypeName a, Show a, Equal a, Arbitrary a, CoArbitrary a
  , TypeName n, Natural n, Equal n
  , TypeName (t a), List t
  , Show (t a), Equal (t a), Arbitrary (t a), Equal (t (Pair a a)), Equal (t (t a))
  ) => Int -> Int -> t a -> n -> IO ()
_test_tails_inits size cases t n = do
  testLabel2 "tails & inits" t n

  let args = testArgs size cases

  runTest args (_test_tails_nil t)
  runTest args (_test_tails_cons t)
  runTest args (_test_tails_single t)
  runTest args (_test_tails_double t)
  runTest args (_test_tails_map t)
  runTest args (_test_tails_length t n)
  runTest args (_test_tails_snoc t)
  runTest args (_test_tails_suffix t)

  runTest args (_test_inits_tails t)
  runTest args (_test_inits_cons t)
  runTest args (_test_inits_map t)
  runTest args (_test_inits_length t n)

  runTest args (_test_inits_lcp t)
  runTest args (_test_tails_lcs t)

Main:

main_tails_inits :: IO ()
main_tails_inits = do
  _test_tails_inits 20 100 (nil :: ConsList Bool)  (zero :: Unary)
  _test_tails_inits 20 100 (nil :: ConsList Unary) (zero :: Unary)