--- title: Tails and Inits author: nbloomf date: 2017-05-12 tags: arithmetic-made-difficult, literate-haskell slug: tails-inits --- > {-# 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}}.$$ :::::: definition :: 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. :::::: corollary ::: []{#cor-tails-nil}[]{#cor-tails-cons} 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 ::::::::::: > _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. :::::: theorem ::::: []{#thm-tails-one}[]{#thm-tails-two} 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)))$. ::: proof :::::::::: 1. Note that $$\begin{eqnarray*} & & \tails(\cons(a,\nil)) \\ & \href{@tails-inits@#cor-tails-cons} = & \cons(\cons(a,\nil),\tails(\nil)) \\ & \href{@tails-inits@#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{@tails-inits@#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 ::::::::::: > _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$. :::::: theorem ::::: []{#thm-tails-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)).$$ ::: proof :::::::::: We proceed by list induction on $x$. For the base case $x = \nil$, we have $$\begin{eqnarray*} & & \tails(\map(f)(\nil)) \\ & \href{@map@#cor-map-nil} = & \tails(\nil) \\ & = & (@@@) \\ & = & \nil \\ & \href{@map@#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{@map@#cor-map-cons} = & \tails(\cons(f(a),\map(f)(x))) \\ & = & \cons(\cons(f(a),\map(f)(x)),\tails(\map(f)(x))) \\ & \href{@tails-inits@#thm-tails-map} = & \cons(\cons(f(a),\map(f)(x)),\map(\map(f))(\tails(x))) \\ & \href{@map@#cor-map-cons} = & \cons(\map(f)(\cons(a,x)),\map(\map(f))(\tails(x))) \\ & \href{@map@#cor-map-cons} = & \map(\map(f))(\cons(\cons(a,x),\tails(x))) \\ & = & \map(\map(f))(\tails(\cons(a,x))) \end{eqnarray*}$$ as claimed. :::::::::::::::::::: ::: test ::::::::::: > _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$. :::::: theorem ::::: []{#thm-length-tails} 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$. ::: proof :::::::::: We proceed by list induction. For the base case$x = \nil$, we have $$\begin{eqnarray*} & & \length(\tails(\nil)) \\ & \href{@tails-inits@#cor-tails-nil} = & \length(\cons(\nil,\nil)) \\ & \href{@length@#thm-length-singleton} = & \next(\zero) \\ & \href{@length@#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{@tails-inits@#cor-tails-cons} = & \length(\cons(\cons(a,x),\tails(x))) \\ & \href{@length@#cor-length-cons} = & \next(\length(\tails(x))) \\ & = & \next(\next(\length(x))) \\ & \href{@length@#cor-length-cons} = & \next(\length(\cons(a,x))) \end{eqnarray*}$$ as claimed. :::::::::::::::::::: ::: test ::::::::::: > _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$. :::::: theorem ::::: []{#thm-tails-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))).$$ ::: proof :::::::::: 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{@tails-inits@#cor-tails-nil} = & \snoc(\nil,\map(\snoc(a))(\cons(\nil,\nil))) \\ & \href{@map@#cor-map-cons} = & \snoc(\nil,\cons(\snoc(a,\nil),\map(\snoc(a))(\nil))) \\ & \href{@map@#cor-map-nil} = & \snoc(\nil,\cons(\snoc(a,\nil),\nil)) \\ & \href{@snoc@#cor-snoc-cons} = & \cons(\snoc(a,\nil),\snoc(\nil,\nil)) \\ & = & \cons(\cons(a,\nil),\cons(\nil,\nil)) \\ & \href{@tails-inits@#thm-tails-one} = & \tails(\cons(a,\nil)) \\ & \href{@snoc@#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{@snoc@#cor-snoc-cons} = & \tails(\cons(b,\snoc(a,x))) \\ & = & \cons(\cons(b,\snoc(a,x)),\tails(\snoc(a,x))) \\ & \href{@tails-inits@#thm-tails-snoc} = & \cons(\cons(b,\snoc(a,x)),\snoc(\nil,\map(\snoc(a))(\tails(x)))) \\ & \href{@snoc@#cor-snoc-cons} = & \snoc(\nil,\cons(\cons(b,\snoc(a,x)),\map(\snoc(a))(\tails(x)))) \\ & \href{@snoc@#cor-snoc-cons} = & \snoc(\nil,\cons(\snoc(a,\cons(b,x)),\map(\snoc(a))(\tails(x)))) \\ & \href{@map@#cor-map-cons} = & \snoc(\nil,\map(\snoc(a))(\cons(\cons(b,x),\tails(x)))) \\ & \href{@tails-inits@#cor-tails-cons} = & \snoc(\nil,\map(\snoc(a))(\tails(\cons(b,x)))) \end{eqnarray*}$$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _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. :::::: theorem ::::: []{#thm-tails-suffix} Let$A$be a set. For all$x \in \lists{A}$we have $$\all(\flip(\suffix)(x),\tails(x)) = \btrue.$$ ::: proof :::::::::: 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{@and@#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 ::::::::::: > _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$. :::::: definition :: 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$. :::::: theorem ::::: []{#thm-tails-rev} Let $A$ be a set. For all $x \in \lists{A}$ we have $$\tails(x) = \map(\rev)(\rev(\inits(\rev(x)))).$$ ::: proof :::::::::: 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 ::::::::::: > _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$. :::::: theorem ::::: []{#thm-inits-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))).$$ ::: proof :::::::::: Note that $$\begin{eqnarray*} & & \inits(\cons(a,x)) \\ & = & \rev(\map(\rev)(\tails(\rev(\cons(a,x))))) \\ & \href{@rev@#cor-rev-cons} = & \rev(\map(\rev)(\tails(\snoc(a,\rev(x))))) \\ & = & \rev(\map(\rev)(\snoc(\nil,\map(\snoc(a))(\tails(\rev(a)))))) \\ & \href{@map@#thm-map-snoc} = & \rev(\snoc(\rev(\nil),\map(\rev)(\map(\snoc(a))(\tails(\rev(a)))))) \\ & \href{@rev@#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{@rev@#thm-rev-snoc} = & \cons(\nil,\rev(\map(\cons(a))(\map(\rev)(\tails(\rev(a)))))) \\ & \href{@map@#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 ::::::::::: > _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$. :::::: theorem ::::: []{#thm-inits-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)).$$ ::: proof :::::::::: Note that $$\begin{eqnarray*} & & \inits(\map(f)(x)) \\ & = & \rev(\map(\rev)(\tails(\rev(\map(f)(x))))) \\ & \href{@map@#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{@map@#thm-map-rev} = & \map(\map(f))(\rev(\map(\rev)(\tails(\rev(x))))) \\ & = & \map(\map(f))(\inits(x)) \end{eqnarray*}$$ as claimed. :::::::::::::::::::: ::: test ::::::::::: > _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$. :::::: theorem ::::: []{#thm-length-inits} Let$A$be a set. For all$x \in \lists{A}$, we have $$\length(\inits(x)) = \next(\length(x)).$$ ::: proof :::::::::: Note that $$\begin{eqnarray*} & & \length(\inits(x)) \\ & = & \length(\rev(\map(\rev)(\tails(\rev(x))))) \\ & \href{@length@#thm-length-rev} = & \length(\map(\rev)(\tails(\rev(x)))) \\ & = & \length(\tails(\rev(x))) \\ & \href{@tails-inits@#thm-length-tails} = & \next(\length(\rev(x))) \\ & \href{@length@#thm-length-rev} = & \next(\length(x)) \end{eqnarray*}$$ as claimed. :::::::::::::::::::: ::: test ::::::::::: > _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$. :::::: theorem ::::: []{#thm-inits-lcp} Let $A$ be a set. For all $x,y \in \lists{A}$, we have $$\inits(\lcp(x,y)) = \lcp(\inits(x),\inits(y)).$$ ::: proof :::::::::: 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{@lcp-lcs@#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{@lcp-lcs@#thm-lcp-commutative} = & \inits(\lcp(\nil,\cons(a,x))) \\ & = & \lcp(\tails(\nil),\tails(\cons(a,x))) \\ & \href{@lcp-lcs@#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{@tails-inits@#cor-tails-nil} = & \tails(\nil) \\ & = & \tails(\lcp(\cons(a,x),\cons(b,u))) \\ & = & \tails(\lcp(\cons(a,x),y)) \end{eqnarray*}$$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _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$. :::::: theorem ::::: []{#thm-tails-lcs} Let$A$be a set. For all$x,y \in \lists{A}$, we have $$\tails(\lcs(x,y)) = \lcs(\tails(x),\tails(y)).$$ ::: proof :::::::::: Note that$\rev$is injective, so that $$\begin{eqnarray*} & & \tails(\lcs(x,y)) \\ & \href{@tails-inits@#thm-tails-rev} = & \map(\rev)(\rev(\inits(\rev(\lcs(x,y))))) \\ & = & \map(\rev)(\rev(\inits(\lcp(\rev(x),\rev(y))))) \\ & \href{@tails-inits@#thm-inits-lcp} = & \map(\rev)(\rev(\lcp(\inits(\rev(x)),\inits(\rev(y))))) \\ & \href{@map@#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 ::::::::::: > _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)