---
title: Longest Common Prefix
author: nbloomf
date: 2017-05-09
tags: arithmetic-made-difficult, literate-haskell
slug: lcp-lcs
---

> {-# LANGUAGE NoImplicitPrelude #-}
> module LongestCommonPrefix
>   ( lcp, lcs, _test_lcp, main_lcp
>   ) where
> 
> import Testing
> import Booleans
> import Not
> import And
> import Tuples
> import NaturalNumbers
> import Lists
> import DoubleFold
> import Snoc
> import Reverse
> import Cat
> import Map
> import Zip
> import PrefixAndSuffix

Today we'll compute the *longest common prefix* of two lists (and while we're at it, the *longest common suffix*). Given two lists $x$ and $y$, their longest common prefix is the longest list which is a prefix of both, just like it says on the tin. We'll denote this function $\lcp$, and we want it to have a signature like $$\lists{A} \times \lists{A} \rightarrow \lists{A}.$$ Double fold was made for situations like this.

:::::: definition ::
Let $A$ be a set. Define $\delta : \lists{A} \rightarrow \lists{A}$ by $\delta(y) = \nil$, $\psi : A \times \lists{A} \rightarrow \lists{A}$ by $$\psi(a,x) = \nil,$$ and $\chi : A \times A \times \lists{A} \times \lists{A} \times \lists{A} \rightarrow \lists{A}$ by $$\chi(a,b,y,z,w) = \bif{\beq(a,b)}{cons(a,z)}{\nil}.$$ Now define $\lcp : \lists{A} \times \lists{A} \rightarrow \lists{A}$ by $$\lcp = \dfoldr(\delta)(\psi)(\chi).$$

In Haskell:

> lcp :: (List t, Equal a) => t a -> t a -> t a
> lcp = dfoldr delta psi chi
>   where
>     delta _ = nil
>     psi _ _ = nil
>     chi a b _ z _ = if eq a b then cons a z else nil

::::::::::::::::::::

Since $\lcp$ is defined as a double fold, it is the unique solution to a system of functional equations.

:::::: corollary :::
[]{#cor-lcp-nil}[]{#cor-lcp-cons-nil}[]{#cor-lcp-cons-cons}
Let $A$ be a set. Then $\lcp$ is the unique map $f : \lists{A} \times \lists{A} \rightarrow \lists{A}$ satisfying the following equations for all $a,b \in A$ and $x,y \in \lists{A}$.
$$\left\{\begin{array}{l}
 f(\nil,y) = \nil \\
 f(\cons(a,x),\nil) = \nil \\
 f(\cons(a,x),\cons(b,y)) = \bif{\beq(a,b)}{\cons(a,f(x,y))}{\nil}
\end{array}\right.$$

::: test :::::::::::

> _test_lcp_nil_list :: (List t, Equal a, Equal (t a))
>   => t a -> Test (t a -> Bool)
> _test_lcp_nil_list _ =
>   testName "lcp(nil,y) == nil" $
>   \y -> eq (lcp nil y) nil
> 
> 
> _test_lcp_cons_nil :: (List t, Equal a, Equal (t a))
>   => t a -> Test (a -> t a -> Bool)
> _test_lcp_cons_nil _ =
>   testName "lcp(cons(a,x),nil) == nil" $
>   \a x -> eq (lcp (cons a x) nil) nil
> 
> 
> _test_lcp_cons_cons :: (List t, Equal a, Equal (t a))
>   => t a -> Test (a -> t a -> a -> t a -> Bool)
> _test_lcp_cons_cons _ =
>   testName "lcp(cons(a,x),cons(b,y)) == if(eq(a,b),cons(a,lcp(x,y),nil))" $
>   \a x b y -> eq
>     (lcp (cons a x) (cons b y))
>     (if eq a b then cons a (lcp x y) else nil)

::::::::::::::::::::
::::::::::::::::::::

Now $\lcp$ lives up to the name (the *universal property* of $\lcp$):

:::::: theorem :::::
[]{#thm-lcp-prefix-left}[]{#thm-lcp-prefix-right}
Let $A$ be a set. The following hold for all $x,y,z \in \lists{A}$.

1. $\prefix(\lcp(x,y),x)$ and $\prefix(\lcp(x,y),y)$.
2. If $\prefix(z,x)$ and $\prefix(z,y)$, then $\prefix(z,\lcp(x,y))$.

::: proof ::::::::::
1. We proceed by list induction on $x$. For the base case $x = \nil$, we have
$$\begin{eqnarray*}
 &   & \prefix(\lcp(x,y),x) \\
 &     \let{x = \nil}
   = & \prefix(\lcp(\nil,y),\nil) \\
 & = & \prefix(\nil,\nil) \\
 &     \href{@prefix-suffix@#cor-prefix-nil-left}
   = & \btrue
\end{eqnarray*}$$
and
$$\begin{eqnarray*}
 &   & \prefix(\lcp(x,y),y) \\
 &     \hyp{x = \nil}
   = & \prefix(\lcp(\nil,y),y) \\
 & = & \prefix(\nil,y) \\
 &     \href{@prefix-suffix@#cor-prefix-nil-left}
   = & \btrue
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equalities hold for all $y$ for some $x$, and let $a \in A$. We consider two cases for $y$. If $y = \nil$, we have
$$\begin{eqnarray*}
 &   & \prefix(\lcp(\cons(a,x),y),\cons(a,x)) \\
 &     \hyp{y = \nil}
   = & \prefix(\lcp(\cons(a,x),\nil),\cons(a,x)) \\
 & = & \prefix(\nil,\cons(a,x)) \\
 &     \href{@prefix-suffix@#cor-prefix-nil-left}
   = & \btrue
\end{eqnarray*}$$
and
$$\begin{eqnarray*}
 &   & \prefix(\lcp(\cons(a,x),y),y) \\
 &     \let{y = \nil}
   = & \prefix(\lcp(\cons(a,x),\nil),\nil) \\
 & = & \prefix(\nil,\nil) \\
 &     \href{@prefix-suffix@#cor-prefix-nil-left}
   = & \btrue
\end{eqnarray*}$$
as needed. Suppose now that $y = \cons(b,w)$. If $b = a$, we have
$$\begin{eqnarray*}
 &   & \prefix(\lcp(\cons(a,x),y),\cons(a,x)) \\
 &     \let{y = \cons(b,w)}
   = & \prefix(\lcp(\cons(a,x),\cons(b,w)),\cons(a,x)) \\
 & = & \prefix(\lcp(\cons(a,x),\cons(a,w)),\cons(a,x)) \\
 & = & \prefix(\cons(a,\lcp(x,w)),\cons(a,x)) \\
 & = & \prefix(\lcp(x,w),x) \\
 &     \href{@lcp-lcs@#thm-lcp-prefix-left}
   = & \btrue
\end{eqnarray*}$$
and
$$\begin{eqnarray*}
 &   & \prefix(\lcp(\cons(a,x),y),y) \\
 &     \let{y = \cons(b,w)}
   = & \prefix(\lcp(\cons(a,x),\cons(b,w)),\cons(b,w)) \\
 & = & \prefix(\lcp(\cons(a,x),\cons(a,w)),\cons(a,w)) \\
 & = & \prefix(\cons(a,\lcp(x,w)),\cons(a,w)) \\
 & = & \prefix(\lcp(x,w),w) \\
 & = & \btrue,
\end{eqnarray*}$$
while if $b \neq a$, we have
$$\begin{eqnarray*}
 &   & \prefix(\lcp(\cons(a,x),y),\cons(a,x)) \\
 & = & \prefix(\lcp(\cons(a,x),\cons(b,w)),\cons(a,x)) \\
 & = & \prefix(\nil,\cons(a,x)) \\
 &     \href{@prefix-suffix@#cor-prefix-nil-left}
   = & \btrue
\end{eqnarray*}$$
and
$$\begin{eqnarray*}
 &   & \prefix(\lcp(\cons(a,x),y),y) \\
 & = & \prefix(\lcp(\cons(a,x),\cons(b,w)),\cons(b,w)) \\
 & = & \prefix(\nil,\cons(b,w)) \\
 &     \href{@prefix-suffix@#cor-prefix-nil-left}
   = & \btrue
\end{eqnarray*}$$
as needed.
2. We proceed by list induction on $z$. For the base case $z = \nil$, note that $\prefix(\nil,x)$, $\prefix(\nil,y)$, and $\prefix(\nil,\lcp(x,y))$ are all $\btrue$. For the inductive step, suppose the result holds for all $x$ and $y$ for some $z$ and let $a \in A$. Suppose further that $\prefix(\cons(a,z),x)$ and $\prefix(\cons(a,z),y)$. Then we must have $x = \cons(a,u)$ and $y = \cons(a,v)$, and thus $\prefix(z,u)$ and $\prefix(z,v)$ are both $\btrue$. Using the inductive hypothesis, we have
$$\begin{eqnarray*}
 &   & \prefix(\cons(a,z),\lcp(x,y)) \\
 & = & \prefix(\cons(a,z),\lcp(\cons(a,u),\cons(a,v))) \\
 & = & \prefix(\cons(a,z),\cons(a,\lcp(u,v))) \\
 & = & \prefix(z,\lcp(u,v)) \\
 & = & \btrue
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_lcp_is_common :: (List t, Equal a, Equal (t a))
>   => t a -> Test (t a -> t a -> Bool)
> _test_lcp_is_common _ =
>   testName "and(prefix(lcp(x,y),x),prefix(lcp(x,y),y))" $
>   \x y -> and (prefix (lcp x y) x) (prefix (lcp x y) y)
> 
> 
> _test_lcp_is_longest :: (List t, Equal a, Equal (t a))
>   => t a -> Test (t a -> t a -> t a -> Bool)
> _test_lcp_is_longest _ =
>   testName "if and(prefix(z,x),prefix(z,y)) then prefix(z,lcp(x,y))" $
>   \x y z -> if and (prefix z x) (prefix z y)
>     then prefix z (lcp x y)
>     else true

::::::::::::::::::::
::::::::::::::::::::

$\lcp$ is idempotent.

:::::: theorem :::::
[]{#thm-lcp-idempotent}
Let $A$ be a set. For all $x \in \lists{A}$ we have $\lcp(x,x) = x$.

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, we have
$$\begin{eqnarray*}
 &   & \lcp(x,x) \\
 & = & \lcp(\nil,\nil) \\
 &     \href{@lcp-lcs@#cor-lcp-nil}
   = & \nil \\
 & = & x
\end{eqnarray*}$$
as claimed. For the inductive step, suppose the equality holds for some $x$ and let $a \in A$. Now
$$\begin{eqnarray*}
 &   & \lcp(\cons(a,x),\cons(a,x)) \\
 & = & \cons(a,\lcp(x,x)) \\
 &     \href{@lcp-lcs@#thm-lcp-idempotent}
   = & \cons(a,x)
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

$\lcp$ is commutative.

:::::: theorem :::::
[]{#thm-lcp-commutative}
Let $A$ be a set. For all $x,y \in \lists{A}$ we have $\lcp(x,y) = \lcp(y,x)$.

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, we have
$$\begin{eqnarray*}
 &   & \lcp(x,y) \\
 & = & \lcp(\nil,y) \\
 &     \href{@lcp-lcs@#cor-lcp-nil}
   = & \nil \\
 & = & \lcp(y,\nil) \\
 & = & \lcp(y,x)
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equality holds for all $y$ for some $x$, and let $a \in A$. Now we consider two possibilities for $y$. If $y = \nil$, we have
$$\begin{eqnarray*}
 &   & \lcp(\cons(a,x),y) \\
 & = & \lcp(\cons(a,x),\nil) \\
 &     \href{@lcp-lcs@#cor-lcp-cons-nil}
   = & \nil \\
 &     \href{@lcp-lcs@#cor-lcp-nil}
   = & \lcp(\nil,\cons(a,x)) \\
 & = & \lcp(y,\cons(a,x))
\end{eqnarray*}$$
as needed. Now suppose $y = \cons(b,w)$. Then we have
$$\begin{eqnarray*}
 &   & \lcp(\cons(a,x),y) \\
 & = & \lcp(\cons(a,x),\cons(b,w)) \\
 & = & \bif{\beq(a,b)}{\lcp(x,w)}{\nil} \\
 & = & \bif{\beq(b,a)}{\lcp(w,x)}{\nil} \\
 & = & \lcp(\cons(b,w),\cons(a,x)) \\
 & = & \lcp(y,\cons(a,x))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

$\lcp$ is associative.

:::::: theorem :::::
[]{#thm-lcp-associative}
Let $A$ be a set. For all $x,y,z \in \lists{A}$ we have $\lcp(\lcp(x,y),z) = \lcp(x,\lcp(y,z))$.

::: proof ::::::::::
Let $h = \lcp(\lcp(x,y),z)$, $k = \lcp(x,\lcp(y,z))$, $u = \lcp(x,y)$, and $v = \lcp(y,z)$. First we show that $\prefix(h,k)$. Note that $\prefix(h,u)$, so that $\prefix(h,x)$ and $\prefix(h,y)$. Now $\prefix(h,z)$, so that $\prefix(h,v)$. Thus $\prefix(h,k)$. The proof that $\prefix(k,h)$ is similar; thus $h = k$ as claimed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

$\cat$ distributes over $\lcp$ from the left.

:::::: theorem :::::
[]{#thm-lcp-cat-dist}
Let $A$ be a set. For all $x,y,z \in \lists{A}$ we have $\cat(x,\lcp(y,z)) = \lcp(\cat(x,y),\cat(x,z))$.

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, we have
$$\begin{eqnarray*}
 &   & \cat(x,\lcp(y,z)) \\
 &     \hyp{x = \nil}
   = & \cat(\nil,\lcp(y,z)) \\
 &     \href{@cat@#cor-cat-nil}
   = & \lcp(y,z) \\
 & = & \lcp(\cat(\nil,y),\cat(\nil,z)) \\
 &     \let{x = \nil}
   = & \lcp(\cat(x,y),\cat(x,z))
\end{eqnarray*}$$
as needed. Suppose now that the equality holds for all $y$ and $z$ for some $x$, and let $a \in A$. Then we have
$$\begin{eqnarray*}
 &   & \cat(\cons(a,x),\lcp(y,z)) \\
 &     \href{@cat@#cor-cat-cons}
   = & \cons(a,\cat(x,\lcp(y,z))) \\
 & = & \cons(a,\lcp(\cat(x,y),\cat(x,z))) \\
 & = & \lcp(\cons(a,\cat(x,y)),\cons(a,\cat(x,z))) \\
 & = & \lcp(\cat(\cons(a,x),y),\cat(\cons(a,x),z))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

$\lcp$ detects prefixes.

:::::: theorem :::::
Let $A$ be a set with $x,y \in \lists{A}$. Then $\lcp(x,y) = x$ if and only if $\prefix(x,y) = \btrue$.

::: proof ::::::::::
To see the "if" part, suppose $\prefix(x,y)$. Then we have $y = \cat(x,z)$ for some $z$. Now
$$\begin{eqnarray*}
 &   & \lcp(x,y) \\
 & = & \lcp(\cat(x,\nil),\cat(x,z)) \\
 &     \href{@lcp-lcs@#thm-lcp-cat-dist}
   = & \cat(x,\lcp(\nil,z)) \\
 &     \href{@lcp-lcs@#cor-lcp-nil}
   = & \cat(x,\nil) \\
 &     \href{@cat@#thm-cat-nil-right}
   = & x
\end{eqnarray*}$$
as claimed. To see the "only if" part, suppose we have $\lcp(x,y) = x$; using the universal property of $\lcp$, we have
$$\begin{eqnarray*}
 &   & \prefix(x,y) \\
 & = & \prefix(\lcp(x,y),y) \\
 & = & \btrue
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

And $\lcp$ interacts with $\zip$.

:::::: theorem :::::
[]{#thm-lcp-zip-abide}
Let $A$ and $B$ be sets with $x,y \in \lists{A}$ and $u,v \in \lists{B}$. Then $$\lcp(\zip(x,u),\zip(y,v)) = \zip(\lcp(x,y),\lcp(u,v)).$$

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$, we have
$$\begin{eqnarray*}
 &   & \lcp(\zip(x,u),\zip(y,v)) \\
 &     \hyp{x = \nil}
   = & \lcp(\zip(\nil,u),\zip(y,v)) \\
 &     \href{@zip@#cor-zip-nil-left}
   = & \lcp(\nil,\zip(y,v)) \\
 & = & \nil \\
 &     \href{@zip@#cor-zip-nil-left}
   = & \zip(\nil,\lcp(u,v)) \\
 & = & \zip(\lcp(\nil,y),\lcp(u,v)) \\
 &     \hyp{x = \nil}
   = & \zip(\lcp(x,y),\lcp(u,v))
\end{eqnarray*}$$
as needed. For the inductive step, suppose the equality holds for some $x$ and let $a \in A$. If $y = \nil$, we have
$$\begin{eqnarray*}
 &   & \lcp(\zip(\cons(a,x),u),\zip(y,v)) \\
 &     \hyp{y = \nil}
   = & \lcp(\zip(\cons(a,x),u),\zip(\nil,v)) \\
 &     \href{@zip@#cor-zip-nil-left}
   = & \lcp(\zip(\cons(a,x),u),\nil) \\
 & = & \nil \\
 &     \href{@zip@#cor-zip-nil-left}
   = & \zip(\nil,\lcp(u,v)) \\
 & = & \zip(\lcp(\cons(a,x),\nil),\lcp(u,v)) \\
 &     \hyp{y = \nil}
   = & \zip(\lcp(\cons(a,x),y),\lcp(u,v))
\end{eqnarray*}$$
as claimed. If $u = \nil$, we have
$$\begin{eqnarray*}
 &   & \lcp(\zip(\cons(a,x),u),\zip(y,v)) \\
 &     \let{u = \nil}
   = & \lcp(\zip(\cons(a,x),\nil),\zip(y,v)) \\
 &     \href{@zip@#cor-zip-cons-nil}
   = & \lcp(\nil,\zip(y,v)) \\
 & = & \nil \\
 &     \href{@zip@#thm-zip-nil-right}
   = & \zip(\lcp(\cons(a,x),y),\nil) \\
 & = & \zip(\lcp(\cons(a,x),y),\lcp(\nil,v)) \\
 &     \let{u = \nil}
   = & \zip(\lcp(\cons(a,x),y),\lcp(u,v))
\end{eqnarray*}$$
as claimed. If $v = \nil$, we have
$$\begin{eqnarray*}
 &   & \lcp(\zip(\cons(a,x),u),\zip(y,v)) \\
 &     \let{v = \nil}
   = & \lcp(\zip(\cons(a,x),u),\zip(y,\nil)) \\
 &     \href{@zip@#thm-zip-nil-right}
   = & \lcp(\zip(\cons(a,x),u),\nil) \\
 & = & \nil \\
 &     \href{@zip@#thm-zip-nil-right}
   = & \zip(\lcp(\cons(a,x),y),\nil) \\
 & = & \zip(\lcp(\cons(a,x),y),\lcp(u,\nil)) \\
 &     \let{v = \nil}
   = & \zip(\lcp(\cons(a,x),y),\lcp(u,v))
\end{eqnarray*}$$
as claimed. Thus we can say $y = \cons(c,w)$, $u = \cons(b,h)$, and $v = \cons(d,k)$. If $a \neq c$, we have
$$\begin{eqnarray*}
 &   & \zip(\lcp(\cons(a,x),y),\lcp(u,v)) \\
 & = & \zip(\lcp(\cons(a,x),\cons(c,w)),\lcp(u,v)) \\
 & = & \zip(\nil,\lcp(u,v)) \\
 &     \href{@zip@#cor-zip-nil-left}
   = & \nil \\
 & = & \lcp(\cons((a,b),\zip(x,h)),\cons((c,d),\zip(w,k))) \\
 & = & \lcp(\zip(\cons(a,x),\cons(b,h)),\zip(\cons(c,w),\cons(d,k))) \\
 & = & \lcp(\zip(\cons(a,x),u),\zip(y,v))
\end{eqnarray*}$$
as claimed. If $b \neq d$, we have
$$\begin{eqnarray*}
 &   & \zip(\lcp(\cons(a,x),y),\lcp(u,v)) \\
 & = & \zip(\lcp(\cons(a,x),y),\lcp(\cons(c,h),\cons(d,k))) \\
 & = & \zip(\lcp(\cons(a,x),y),\nil) \\
 &     \href{@zip@#thm-zip-nil-right}
   = & \nil \\
 & = & \lcp(\cons((a,b),\zip(x,h)),\cons((c,d),\zip(w,k))) \\
 & = & \lcp(\zip(\cons(a,x),\cons(b,h)),\zip(\cons(c,w),\cons(d,k))) \\
 & = & \lcp(\zip(\cons(a,x),u),\zip(y,v))
\end{eqnarray*}$$
as claimed. Finally, suppose $a = c$ and $b = d$. Using the inductive hypothesis, we have
$$\begin{eqnarray*}
 &   & \lcp(\zip(\cons(a,x),y),\zip(u,v)) \\
 & = & \lcp(\zip(\cons(a,x),\cons(b,w)),\zip(\cons(c,w),\cons(d,k))) \\
 & = & \lcp(\cons((a,b),\zip(x,h)),\cons((c,d),\zip(w,k))) \\
 & = & \lcp(\cons((a,b),\zip(x,h)),\cons((a,b),\zip(w,k))) \\
 & = & \cons((a,b),\lcp(\zip(x,h),\zip(w,k))) \\
 & = & \cons((a,b),\zip(\lcp(x,w),\lcp(h,k))) \\
 & = & \zip(\cons(a,\lcp(x,w)),\cons(b,\lcp(h,k))) \\
 & = & \zip(\lcp(\cons(a,x),\cons(a,w)),\lcp(\cons(b,h),\cons(b,k))) \\
 & = & \zip(\lcp(\cons(a,x),\cons(c,w)),\lcp(\cons(b,h),\cons(d,k))) \\
 & = & \zip(\lcp(\cons(a,x),y),\lcp(u,v))
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _test_lcp_zip :: (List t, Equal a, Equal (t (Pair a a)))
>   => t a -> Test (t a -> t a -> t a -> t a -> Bool)
> _test_lcp_zip _ =
>   testName "zip(lcp(x,y),lcp(u,v)) == lcp(zip(x,u),zip(y,v))" $
>   \x y u v -> eq (zip (lcp x y) (lcp u v)) (lcp (zip x u) (zip y v))

::::::::::::::::::::
::::::::::::::::::::

$\lcp$ interacts with $\map(f)$ if $f$ is injective.

:::::: theorem :::::
Let $A$ and $B$ be sets with $f : A \rightarrow B$ an injective map. For all $x,y \in \lists{A}$ we have $$\map(f)(\lcp(x,y)) = \lcp(\map(f)(x),\map(f)(y)).$$

::: proof ::::::::::
We proceed by list induction on $x$. For the base case $x = \nil$ we have
$$\begin{eqnarray*}
 &   & \map(f)(\lcp(x,y)) \\
 & = & \map(f)(\lcp(\nil,y)) \\
 &     \href{@lcp-lcs@#cor-lcp-nil}
   = & \map(f)(\nil) \\
 &     \href{@map@#cor-map-nil}
   = & \nil \\
 & = & \lcp(\nil,\map(f)(y)) \\
 &     \href{@map@#cor-map-nil}
   = & \lcp(\map(f)(\nil),\map(f)(y)) \\
 & = & \lcp(\map(f)(x),\map(f)(y))
\end{eqnarray*}$$
as needed. Suppose now the equality holds for some $x$ and let $a \in A$. We consider two possitiblities for $y$. If $y = \nil$, we have
$$\begin{eqnarray*}
 &   & \map(f)(\lcp(\cons(a,x),y)) \\
 & = & \map(f)(\lcp(\cons(a,x),\nil)) \\
 &     \href{@lcp-lcs@#cor-lcp-cons-nil}
   = & \map(f)(\nil) \\
 &     \href{@map@#cor-map-nil}
   = & \nil \\
 & = & \lcp(\map(f)(\cons(a,x)),\nil) \\
 &     \href{@map@#cor-map-nil}
   = & \lcp(\map(f)(\cons(a,x)),\map(f)(\nil)) \\
 & = & \lcp(\map(f)(\cons(a,x)),\map(f)(y))
\end{eqnarray*}$$
as needed. Suppose then that $y = \cons(b,u)$. If $a = b$, we have $f(a) = f(b)$. Now
$$\begin{eqnarray*}
 &   & \map(f)(\lcp(\cons(a,x),y)) \\
 & = & \map(f)(\lcp(\cons(a,x),\cons(b,u))) \\
 & = & \map(f)(\lcp(\cons(a,x),\cons(a,u))) \\
 & = & \map(f)(\cons(a,\lcp(x,u))) \\
 &     \href{@map@#cor-map-cons}
   = & \cons(f(a),\map(f)(\lcp(x,u))) \\
 & = & \cons(f(a),\lcp(\map(f)(x),\map(f)(u))) \\
 & = & \lcp(\cons(f(a),\map(f)(x)),\cons(f(a),\map(f)(u))) \\
 & = & \lcp(\map(f)(\cons(a,x)),\map(f)(\cons(a,u))) \\
 & = & \lcp(\map(f)(\cons(a,x)),\map(f)(\cons(b,u))) \\
 & = & \lcp(\map(f)(\cons(a,x)),\map(f)(y))
\end{eqnarray*}$$
as needed. On the other hand, if $a \neq b$, then (since $f$ is injective) $f(a) \neq f(b)$. Then we have
$$\begin{eqnarray*}
 &   & \map(f)(\lcp(\cons(a,x),y)) \\
 & = & \map(f)(\lcp(\cons(a,x),\cons(b,u))) \\
 & = & \map(f)(\lcp(x,u)) \\
 & = & \lcp(\map(f)(x),\map(f)(u)) \\
 & = & \lcp(\cons(f(a),\map(f)(x)),\cons(f(b),\map(f)(u))) \\
 & = & \lcp(\map(f)(\cons(a,x)),\map(f)(\cons(b,u))) \\
 & = & \lcp(\map(f)(\cons(a,x)),\map(f)(y))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::
::::::::::::::::::::

And $\lcp$ interacts with $\map(f)$ and $\map(g)$ if $f$ and $g$ have no images in common.

:::::: theorem :::::
Let $A$ and $B$ be sets

1. Suppose $f,g : A \rightarrow B$ are functions with the property that $f(a) \neq g(b)$ for all $a,b \in A$. Then $\lcp(\map(f)(x),\map(g)(y)) = \nil$ for all $x,y \in \lists{A}$.
2. In particular, $f(x) = \cons(a,x)$ and $g(x) = \cons(b,x)$ have this property if $a \neq b$.

::: proof ::::::::::
1. We proceed by list induction on $x$. For the base case $x = \nil$, note that
$$\begin{eqnarray*}
 &   & \lcp(\map(f)(\nil),\map(g)(y)) \\
 &     \href{@map@#cor-map-nil}
   = & \lcp(\nil,\map(g)(y)) \\
 & = & \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*}
 &   & \lcp(\map(f)(\cons(a,x)),\map(g)(\nil)) \\
 &     \href{@map@#cor-map-nil}
   = & \lcp(\map(f)(\cons(a,x)),\nil) \\
 & = & \nil
\end{eqnarray*}$$
as needed, and if $y = \cons(b,u)$, since $f(a) \neq g(b)$, we have
$$\begin{eqnarray*}
 &   & \lcp(\map(f)(\cons(a,x)),\map(g)(\cons(b,u))) \\
 & = & \lcp(\cons(f(a),\map(f)(x)),\cons(g(b))(\map(g)(u))) \\
 & = & \nil
\end{eqnarray*}$$
as needed.
2. Note that if $\cons(a,x) = \cons(b,y)$, we must have $a = b$.
::::::::::::::::::::

::: test :::::::::::

> _test_lcp_map_cons :: (List t, Equal a, Equal (t a), Equal (t (t a)))
>   => t a -> Test (a -> a -> t (t a) -> t (t a) -> Bool)
> _test_lcp_map_cons _ =
>   testName "if a /= b then lcp(map(cons(a,-))(x),map(cons(b,-))(y)) == nil" $
>   \a b x y -> if not (eq a b)
>     then eq (lcp (map (cons a) x) (map (cons b) y)) nil
>     else true

::::::::::::::::::::
::::::::::::::::::::

We can define the dual operation, longest common suffix, in terms of $\lcp$ like so.

:::::: definition ::
[]{#def-lcs}
Let $A$ be a set. We define $\lcs : \lists{A} \times \lists{A} \rightarrow \lists{A}$ by $$\lcs(x,y) = \rev(\lcp(\rev(x),\rev(y))).$$

In Haskell:

> lcs :: (List t, Equal a) => t a -> t a -> t a
> lcs x y = rev (lcp (rev x) (rev y))

::::::::::::::::::::

Many properties of $\lcp$ have analogues for $\lcs$.

:::::: corollary :::
[]{#cor-lcs-nil}[]{#cor-lcs-snoc-nil}[]{#cor-lcs-snoc-snoc}
Let $A$ be a set. For all $a,b \in A$ and $x,y \in \lists{A}$, we have the following.

1. $\lcs(\nil,y) = \nil$.
2. $\lcs(\snoc(a,x),\nil) = \nil$.
3. $\lcs(\snoc(a,x),\snoc(b,y)) = \bif{\beq(a,b)}{\snoc(a,\lcs(x,y))}{\nil}$.

::: test :::::::::::

> _test_lcs_nil_list :: (List t, Equal a, Equal (t a))
>   => t a -> Test (t a -> Bool)
> _test_lcs_nil_list _ =
>   testName "lcs(nil,y) == nil" $
>   \y -> eq (lcs nil y) nil
> 
> 
> _test_lcs_snoc_nil :: (List t, Equal a, Equal (t a))
>   => t a -> Test (a -> t a -> Bool)
> _test_lcs_snoc_nil _ =
>   testName "lcs(snoc(a,x),nil) == nil" $
>   \a x -> eq (lcs (snoc a x) nil) nil
> 
> 
> _test_lcs_snoc_snoc :: (List t, Equal a, Equal (t a))
>   => t a -> Test (a -> t a -> a -> t a -> Bool)
> _test_lcs_snoc_snoc _ =
>   testName "lcs(snoc(a,x),snoc(b,y)) == if(eq(a,b),snoc(a,lcs(x,y)),nil)" $
>   \a x b y -> eq
>     (lcs (snoc a x) (snoc b y))
>     (if eq a b then snoc a (lcs x y) else nil)

::::::::::::::::::::
::::::::::::::::::::

$\lcs$ lives up to the name.

:::::: theorem :::::
Let $A$ be a set with $x,y,z \in \lists{A}$. Then we have the following.

1. $\suffix(\lcs(x,y),x)$ and $\suffix(\lcs(x,y),y)$.
2. If $\suffix(z,x)$ and $\suffix(z,y)$, then $\suffix(z,\lcs(x,y))$.

::: proof ::::::::::
1. Note that
$$\begin{eqnarray*}
 &   & \suffix(\lcs(x,y),x) \\
 & = & \prefix(\rev(\lcs(x,y)),\rev(x)) \\
 &     \href{@lcp-lcs@#def-lcs}
   = & \prefix(\rev(\rev(\lcp(\rev(x),\rev(y)))),\rev(x)) \\
 &     \href{@rev@#thm-rev-involution}
   = & \prefix(\lcp(\rev(x),\rev(y)),\rev(x)) \\
 & = & \btrue,
\end{eqnarray*}$$
and likewise
$$\begin{eqnarray*}
 &   & \suffix(\lcs(x,y),y) \\
 & = & \prefix(\rev(\lcs(x,y)),\rev(y)) \\
 &     \href{@lcp-lcs@#def-lcs}
   = & \prefix(\rev(\rev(\lcp(\rev(x),\rev(y)))),\rev(y)) \\
 &     \href{@rev@#thm-rev-involution}
   = & \prefix(\lcp(\rev(x),\rev(y)),\rev(y)) \\
 & = & \btrue,
\end{eqnarray*}$$
2. Suppose $\suffix(z,x)$ and $\suffix(z,y)$. Then we have
$$\begin{eqnarray*}
 &   & \btrue \\
 & = & \suffix(z,x) \\
 & = & \prefix(\rev(z),\rev(x))
\end{eqnarray*}$$
and likewise
$$\begin{eqnarray*}
 &   & \btrue \\
 & = & \suffix(z,y) \\
 & = & \prefix(\rev(z),\rev(y)).
\end{eqnarray*}$$
So we have
$$\begin{eqnarray*}
 &   & \btrue \\
 & = & \prefix(\rev(z),\lcp(\rev(x),\rev(y))) \\
 &     \href{@rev@#thm-rev-involution}
   = & \prefix(\rev(z),\rev(\rev(\lcp(\rev(x),\rev(y))))) \\
 & = & \prefix(\rev(z),\rev(\lcs(x,y))) \\
 & = & \suffix(z,\lcs(x,y))
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _test_lcs_is_common :: (List t, Equal a, Equal (t a))
>   => t a -> Test (t a -> t a -> Bool)
> _test_lcs_is_common _ =
>   testName "and(suffix(lcs(x,y),x),suffix(lcs(x,y),y))" $
>   \x y -> and (suffix (lcs x y) x) (suffix (lcs x y) y)
> 
> 
> _test_lcs_is_longest :: (List t, Equal a, Equal (t a))
>   => t a -> Test (t a -> t a -> t a -> Bool)
> _test_lcs_is_longest _ =
>   testName "if and(suffix(z,x),suffix(z,y)) then suffix(z,lcs(x,y))" $
>   \x y z -> if and (suffix z x) (suffix z y)
>     then suffix z (lcs x y)
>     else true

::::::::::::::::::::
::::::::::::::::::::

$\lcs$ is idempotent.

:::::: theorem :::::
[]{#thm-lcs-idempotent}
Let $A$ be a set. For all $x \in \lists{A}$ we have $\lcs(x,x) = x$.

::: proof ::::::::::
Note that
$$\begin{eqnarray*}
 &   & \lcs(x,x) \\
 &     \href{@lcp-lcs@#def-lcs}
   = & \rev(\lcp(\rev(x),\rev(x))) \\
 &     \href{@lcp-lcs@#thm-lcp-idempotent}
   = & \rev(\rev(x)) \\
 &     \href{@rev@#thm-rev-involution}
   = & x
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

$\lcs$ is commutative.

:::::: theorem :::::
[]{#thm-lcs-commutative}
Let $A$ be a set. For all $x,y \in \lists{A}$ we have $\lcs(x,y) = \lcs(y,x)$.

::: proof ::::::::::
We have
$$\begin{eqnarray*}
 &   & \lcs(x,y) \\
 &     \href{@lcp-lcs@#def-lcs}
   = & \rev(\lcp(\rev(x),\rev(y))) \\
 &     \href{@lcp-lcs@#thm-lcp-commutative}
   = & \rev(\lcp(\rev(y),\rev(x))) \\
 &     \href{@lcp-lcs@#def-lcs}
   = & \lcs(y,x)
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

$\lcs$ is associative.

:::::: theorem :::::
[]{#thm-lcs-associative}
Let $A$ be a set. For all $x,y,z \in \lists{A}$ we have $\lcs(\lcs(x,y),z) = \lcs(x,\lcs(y,z))$.

::: proof ::::::::::
We have
$$\begin{eqnarray*}
 &   & \lcs(\lcs(x,y),z) \\
 &     \href{@lcp-lcs@#def-lcs}
   = & \lcs(\rev(\lcp(\rev(x),\rev(y))),z) \\
 &     \href{@lcp-lcs@#def-lcs}
   = & \rev(\lcp(\rev(\rev(\lcp(\rev(x),\rev(y)))),\rev(z))) \\
 &     \href{@rev@#thm-rev-involution}
   = & \rev(\lcp(\lcp(\rev(x),\rev(y)),\rev(z))) \\
 & = & \rev(\lcp(\rev(x),\lcp(\rev(y),\rev(z)))) \\
 &     \href{@rev@#thm-rev-involution}
   = & \rev(\lcp(\rev(x),\rev(\rev(\lcp(\rev(y),\rev(z)))))) \\
 & = & \rev(\lcp(\rev(x),\rev(\lcs(y,z)))) \\
 &     \href{@lcp-lcs@#def-lcs}
   = & \lcs(x,\lcs(y,z))
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

$\cat$ distributes over $\lcs$ from the right.

:::::: theorem :::::
[]{#thm-lcs-cat-dist}
Let $A$ be a set. For all $x,y,z \in \lists{A}$ we have $\cat(\lcs(x,y),z) = \lcs(\cat(x,z),\cat(y,z))$.

::: proof ::::::::::
Note that
$$\begin{eqnarray*}
 &   & \lcs(\cat(x,z),\cat(y,z)) \\
 &     \href{@lcp-lcs@#def-lcs}
   = & \rev(\lcp(\rev(\cat(x,z)),\rev(\cat(y,z)))) \\
 & = & \rev(\lcp(\cat(\rev(z),\rev(x)),\cat(\rev(z),\rev(y)))) \\
 &     \href{@lcp-lcs@#thm-lcp-cat-dist}
   = & \rev(\cat(\rev(z),\lcp(\rev(x),\rev(y)))) \\
 &     \href{@cat@#thm-rev-cat-antidistribute}
   = & \cat(\rev(\lcp(\rev(x),\rev(y))),\rev(\rev(z))) \\
 & = & \cat(\lcs(x,y),z)
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

$\lcs$ detects suffixes.

:::::: theorem :::::
Let $A$ be a set with $x,y \in \lists{A}$. Then $\lcs(x,y) = x$ if and only if $\suffix(x,y)$.

::: proof ::::::::::
Note that $$\lcs(x,y) = x$$ if and only if $$\rev(\lcp(\rev(x),\rev(y))) = x$$ if and only if $$\rev(\rev(\lcp(\rev(x),\rev(y)))) = \rev(x)$$ if and only if $$\lcp(\rev(x),\rev(y)) = \rev(x)$$ if and only if $$\prefix(\rev(x),\rev(y)) = \btrue$$ if and only if $$\suffix(x,y) = \btrue$$ as claimed.
::::::::::::::::::::

::: test :::::::::::

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

::::::::::::::::::::
::::::::::::::::::::

And $\lcs$ also interacts with $\map(f)$ if $f$ is injective.

:::::: theorem :::::
Let $A$ and $B$ be sets with $f : A \rightarrow B$ an injective map. For all $x,y \in \lists{A}$ we have $$\map(f)(\lcs(x,y)) = \lcs(\map(f)(x),\map(f)(y)).$$

::: proof ::::::::::
Note that
$$\begin{eqnarray*}
 &   & \map(f)(\lcs(x,y)) \\
 &     \href{@lcp-lcs@#def-lcs}
   = & \map(f)(\rev(\lcp(\rev(x),\rev(y)))) \\
 &     \href{@map@#thm-map-rev}
   = & \rev(\map(f)(\lcp(\rev(x),\rev(y)))) \\
 & = & \rev(\lcp(\map(f)(\rev(x)),\map(f)(\rev(y)))) \\
 & = & \rev(\lcp(\rev(\map(f)(x)),\rev(\map(f)(y)))) \\
 &     \href{@lcp-lcs@#def-lcs}
   = & \lcs(\map(f)(x),\map(f)(y))
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::
::::::::::::::::::::


Testing
-------

Suite:

> _test_lcp ::
>   ( TypeName a, Equal a, Show a, Arbitrary a
>   , TypeName (t a), List t
>   , Show (t a), Equal (t a), Arbitrary (t a), Equal (t (Pair a a))
>   , Arbitrary (t (t a)), Show (t (t a)), Equal (t (t a))
>   ) => Int -> Int -> t a -> IO ()
> _test_lcp size cases t = do
>   testLabel1 "lcp & lcs" t
>   let args = testArgs size cases
> 
>   runTest args (_test_lcp_nil_list t)
>   runTest args (_test_lcp_cons_nil t)
>   runTest args (_test_lcp_cons_cons t)
>   runTest args (_test_lcp_is_common t)
>   runTest args (_test_lcp_is_longest t)
>   runTest args (_test_lcp_idempotent t)
>   runTest args (_test_lcp_commutative t)
>   runTest args (_test_lcp_associative t)
>   runTest args (_test_lcp_cat_left t)
>   runTest args (_test_lcp_prefix t)
>   runTest args (_test_lcp_zip t)
>   runTest args (_test_lcp_map_cons t)
> 
>   runTest args (_test_lcs_nil_list t)
>   runTest args (_test_lcs_snoc_nil t)
>   runTest args (_test_lcs_snoc_snoc t)
>   runTest args (_test_lcs_is_common t)
>   runTest args (_test_lcs_is_longest t)
>   runTest args (_test_lcs_idempotent t)
>   runTest args (_test_lcs_commutative t)
>   runTest args (_test_lcs_associative t)
>   runTest args (_test_lcs_cat_right t)
>   runTest args (_test_lcs_suffix t)

Main:

> main_lcp :: IO ()
> main_lcp = do
>   _test_lcp 20 100 (nil :: ConsList Bool)
>   _test_lcp 20 100 (nil :: ConsList Unary)