# Tails and Inits

Posted on 2017-05-12 by nbloomf

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

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.

1. $$\tails(\cons(a,\nil)) = \cons(\cons(a,\nil),\cons(\nil,\nil))$$.
2. $$\tails(\cons(a,\cons(b,\nil))) = \cons(\cons(a,\cons(b,\nil)),\cons(\cons(b,\nil),\cons(\nil,\nil)))$$.
1. 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.
2. 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)))).$

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)