Prefix and Suffix

Posted on 2017-05-08 by nbloomf
Tags: arithmetic-made-difficult, literate-haskell

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 PrefixAndSuffix
  ( prefix, suffix, _test_prefix_suffix, main_prefix_suffix
  ) where

import Testing
import Booleans
import And
import NaturalNumbers
import LessThanOrEqualTo
import Lists
import DoubleFold
import Snoc
import Reverse
import Cat
import Length
import Map
import Zip

The \(\cat\) function on \(\lists{A}\) is analogous to \(\nplus\) on \(\nats\). Carrying this analogy further, \(\zip\) and \(\zipPad\) are analogous to \(\nmin\) and \(\nmax\), respectively. When analogies like this occur in mathematics it can be fruitful to see how far they go. With that in mind, today we will explore the list-analogue of \(\nleq\). This role is played by two functions which we call \(\prefix\) and \(\suffix\).

Intuitively, \(\prefix\) will detect when one list is an initial segment of another, while \(\suffix\) detects when one list is a terminal segment of another. We’ll start with \(\prefix\), which we can define as a \(\dfoldr\) as follows.

Let \(A\) be a set. Define \(\delta : \lists{A} \rightarrow \bool\) by \(\delta(y) = \btrue\), define \(\psi : A \times \bool \rightarrow \bool\) by \(\psi(a,p) = \bfalse\), and define \(\chi : A \times A \times \lists{A} \times \bool \times \bool \rightarrow \lists{A}\) by \[\chi(a,b,y,p,q) = \bif{\beq(a,b)}{p}{\bfalse}.\] Now define \[\prefix : \lists{A} \times \lists{A} \rightarrow \bool\] by \[\prefix = \dfoldr(\delta)(\psi)(\chi).\]

In Haskell:

Since \(\prefix\) is defined as a double fold, it is the unique solution to a system of functional equations.

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

Now \(\prefix\) is analogous to \(\nleq\) in that it detects the existence of solutions \(z\) to the equation \(y = \cat(x,z)\).

Let \(A\) be a set. The following hold for all \(x,y \in \lists{A}\).

  1. \(\prefix(x,\cat(x,y)) = \btrue\).
  2. If \(\prefix(x,y) = \btrue\), then \(y = \cat(x,z)\) for some \(z \in \lists{A}\).
  1. We proceed by list induction on \(x\). For the base case \(x = \nil\), certainly we have \[\begin{eqnarray*} & & \prefix(x,\cat(x,y)) \\ & \let{x = \nil} = & \prefix(\nil,\cat(\nil,y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \prefix(\nil,y) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \btrue \end{eqnarray*}\] For the inductive step, suppose the equality holds for some \(x\), and let \(a \in A\). Now we have \[\begin{eqnarray*} & & \prefix(\cons(a,x),\cat(\cons(a,x),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \prefix(\cons(a,x),\cons(a,\cat(x,y))) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-cons-cons} = & \bif{\beq(a,a)}{\prefix(x,\cat(x,y))}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \bif{\btrue}{\prefix(x,\cat(x,y))}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \prefix(x,\cat(x,y)) \\ & \hyp{\prefix(x,\cat(x,y)) = \btrue} = & \btrue \end{eqnarray*}\] as needed.
  2. We proceed by list induction on \(x\). For the base case \(x = \nil\), note that \[\begin{eqnarray*} & & \prefix(\nil,y) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \btrue \end{eqnarray*}\] and \[y = \cat(\nil,y).\] For the inductive step, suppose the result holds for some \(x\), and let \(a \in A\). Now suppose \(\prefix(\cons(a,x),y) = \btrue\); in particular, we must have \(y = \cons(a,w)\) for some \(w\), and \(\prefix(x,w) = \btrue\). By the induction hypothesis we have \(w = \cat(x,z)\) for some \(z\), and thus \[\begin{eqnarray*} & & y \\ & \let{y = \cons(a,w)} = & \cons(a,w) \\ & \hyp{w = \cat(x,z)} = & \cons(a,\cat(x,z)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \cat(\cons(a,x),z) \end{eqnarray*}\] as needed.

And \(\prefix\) interacts with \(\snoc\).

Let \(A\) be a set. For all \(x,y \in \lists{A}\), if \(\prefix(x,y) = \btrue\), then \(\prefix(x,\snoc(a,y)) = \btrue\).

If \(\prefix(x,y) = \btrue\), then \(y = \cat(x,z)\) for some \(z\). Now \[\snoc(a,y) = \snoc(\cat(x,z)) = \cat(x,\snoc(a,z)),\] and so \(\prefix(x,\snoc(a,y)) = \btrue\) as claimed.

\(\prefix\) is a partial order.

Let \(A\) be a set. Then we have the following for all \(x,y,z \in \lists{A}\).

  1. \(\prefix(x,x) = \btrue\).
  2. If \(\prefix(x,y)\) and \(\prefix(y,x)\), then \(x = y\).
  3. If \(\prefix(x,y)\) and \(\prefix(y,z)\), then \(\prefix(x,z)\).
  1. We have \[\begin{eqnarray*} & & \btrue \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#thm-prefix-cat-self} = & \prefix(x,\cat(x,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-nil-right} = & \prefix(x,x) \end{eqnarray*}\] as claimed.
  2. If \(\prefix(x,y)\), we have \(y = \cat(x,u)\) for some \(u\). Similarly, if \(\prefix(y,x)\) then \(x = \cat(y,v)\) for some \(v\). Now \[\begin{eqnarray*} & & \cat(x,\nil) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-nil-right} = & x \\ & = & \cat(y,v) \\ & = & \cat(\cat(x,u),v) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-associative} = & \cat(x,\cat(u,v)) \end{eqnarray*}\] Since \(\cat\) is cancellative, we have \(\nil = \cat(u,v)\), so that \(u = \nil\), and thus \(x = y\) as claimed.
  3. If \(\prefix(x,y)\), we have \(y = \cat(x,u)\). Similarly, if \(\prefix(y,z)\), we have \(z = \cat(y,v)\). Now \[z = \cat(\cat(x,u),v) = \cat(x,\cat(u,v))\] so that \(\prefix(x,z)\) as claimed.

\(\map\) preserves \(\prefix\).

Let \(A\) and \(B\) be sets with \(f : A \rightarrow B\), and let \(x,y \in \lists{A}\). If \(\prefix(x,y) = \btrue\), then \[\prefix(\map(f)(x),\map(f)(y)) = \btrue.\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \prefix(x,y) \\ & \let{x = \nil} = & \prefix(\nil,y) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \prefix(\nil,\map(f)(y)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \prefix(\map(f)(\nil),\map(f)(y)) \\ & \let{x = \nil} = & \prefix(\map(f)(x),\map(f)(y)) \end{eqnarray*}\] as claimed. Suppose now the implication holds for some \(x\), and let \(a \in A\). Suppose further that \(\prefix(\cons(a,x),y) = \btrue\). Now \(y = \cons(a,w)\) for some \(w\), and we have \[\begin{eqnarray*} & & \btrue \\ & = & \prefix(\cons(a,x),y) \\ & = & \prefix(\cons(a,x),\cons(a,w)) \\ & = & \prefix(x,w). \end{eqnarray*}\] Using the induction hypothesis, we have \[\begin{eqnarray*} & & \prefix(\map(f)(\cons(a,x)),\map(f)(y)) \\ & = & \prefix(\map(f)(\cons(a,x)),\map(f)(\cons(a,w))) \\ & = & \prefix(\cons(f(a),\map(f)(x)),\cons(f(a),\map(f)(w))) \\ & = & \prefix(\map(f)(x),\map(f)(w)) \\ & = & \btrue \end{eqnarray*}\] as claimed.

And \(\zip\) preserves \(\prefix\).

Let \(A\) and \(B\) be sets with \(x,y \in \lists{A}\) and \(u,v \in \lists{B}\). If \(\prefix(x,y) = \btrue\) and \(\prefix(u,v) = \btrue\), then \[\prefix(\zip(x,u),\zip(y,v)) = \btrue.\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), note that \(\prefix(x,y) = \btrue\). Suppose further that \(\prefix(u,v) = \btrue\); now \[\begin{eqnarray*} & & \prefix(\zip(x,u),\zip(y,v)) \\ & \let{x = \nil} = & \prefix(\zip(\nil,u),\zip(y,v)) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-nil-left} = & \prefix(\nil,\zip(y,v)) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \btrue \end{eqnarray*}\] as claimed. For the inductive step, suppose the implication holds for some \(x\) and let \(a \in A\). Suppose further that \(\prefix(\cons(a,x),y)\) and \(\prefix(u,v)\); in particular we must have \(y = \cons(a,k)\) for some \(k \in \lists{A}\) with \(\prefix(x,k)\), as otherwise \(\prefix(\cons(a,x),y) = \bfalse\). Now we have two possibilities for \(u\). If \(u = \nil\), we have \[\begin{eqnarray*} & & \prefix(\zip(\cons(a,x),u),\zip(y,v)) \\ & \let{u = \nil} = & \prefix(\zip(\cons(a,x),\nil),\zip(y,v)) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-cons-nil} = & \prefix(\nil,\zip(y,v)) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \btrue \end{eqnarray*}\] as claimed. Suppose then that \(u = \cons(b,w)\). Again we must have \(v = \cons(b,h)\) with \(h \in \lists{B}\) and \(\prefix(w,h)\), since otherwise we have \(\prefix(u,v) = \bfalse\). Using the inductive hypothesis, we have \[\begin{eqnarray*} & & \prefix(\zip(\cons(a,x),u),\zip(y,v)) \\ & \let{u = \cons(b,w)} = & \prefix(\zip(\cons(a,x),\cons(b,w)),\zip(y,v)) \\ & \let{v = \cons(b,h)} = & \prefix(\zip(\cons(a,x),\cons(b,w)),\zip(y,\cons(b,h))) \\ & \let{y = \cons(a,k)} = & \prefix(\zip(\cons(a,x),\cons(b,w)),\zip(\cons(a,k),\cons(b,h))) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-cons-cons} = & \prefix(\zip(\cons(a,x),\cons(b,w)),\cons(\tup(a)(b),\zip(k,h))) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-cons-cons} = & \prefix(\cons(\tup(a)(b),\zip(x,w)),\cons(\tup(a)(b),\zip(k,h))) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-cons-cons} = & \bif{\beq(\tup(a)(b),\tup(a)(b))}{\prefix(\zip(x,w))(\zip(k,h))}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-tup-eq} = & \bif{\band(\beq(a,a),\beq(b,b))}{\prefix(\zip(x,w))(\zip(k,h))}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \bif{\band(\btrue,\beq(b,b))}{\prefix(\zip(x,w))(\zip(k,h))}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \bif{\band(\btrue,\btrue)}{\prefix(\zip(x,w))(\zip(k,h))}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-true} = & \bif{\btrue}{\prefix(\zip(x,w))(\zip(k,h))}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \prefix(\zip(x,w),\zip(k,h)) \\ & \hyp{\prefix(\zip(x,w),\zip(k,h)) = \btrue} = & \btrue \end{eqnarray*}\] as claimed.

\(\prefix\) interacts with \(\length\).

Let \(A\) be a set with \(x,y \in \lists{A}\). If \(\prefix(x,y)\), then \(\nleq(\length(x),\length(y))\).

Suppose \(\prefix(x,y)\). Then we have \(y = \cat(x,z)\) for some \(z\), and so \[\begin{eqnarray*} & & \nleq(\length(x),\length(y)) \\ & = & \nleq(\length(x),\length(\cat(x,z))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-length-cat} = & \nleq(\length(x),\nplus(\length(x),\length(z))) \\ & = & \nleq(\zero,\length(z)) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-zero} = & \btrue \end{eqnarray*}\] as claimed.

The simplest way to define \(\suffix\) is in terms of \(\prefix\).

Let \(A\) be a set. Define \(\suffix : \lists{A} \times \lists{A} \rightarrow \bool\) by \[\suffix(x,y) = \prefix(\rev(x),\rev(y)).\]

In Haskell:

Not surprisingly, we can characterize \(\prefix\) in terms of \(\suffix\).

Let \(A\) be a set with \(x,y \in \lists{A}\). Then \[\prefix(x,y) = \suffix(\rev(x),\rev(y)).\]

Note that \[\begin{eqnarray*} & & \suffix(\rev(x),\rev(y)) \\ & = & \prefix(\rev(\rev(x)),\rev(\rev(y))) \\ & = & \prefix(x,y) \end{eqnarray*}\] as claimed.

Many theorems about \(\prefix\) has an analogue for \(\suffix\).

Let \(A\) be a set. For all \(a,b \in A\) and \(x,y \in \lists{A}\), we have the following.

  1. \(\suffix(\nil,y) = \btrue\).
  2. \(\suffix(\snoc(a,x),\nil) = \bfalse\).
  3. \[\suffix(\snoc(a,x),\snoc(b,y)) = \left\{\begin{array}{ll} \bfalse & \mathrm{if}\ a \neq b \\ \suffix(x,y) & \mathrm{if}\ a = b. \end{array}\right.\]
  1. We have \[\begin{eqnarray*} & & \suffix(\nil,y) \\ & = & \prefix(\rev(\nil),\rev(y)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \prefix(\nil,\rev(y)) \\ & = & \btrue \end{eqnarray*}\] as claimed.
  2. We have \[\begin{eqnarray*} & & \suffix(\snoc(a,x),\nil) \\ & = & \prefix(\rev(\snoc(a,x)),\rev(\nil)) \\ & = & \prefix(\cons(a,\rev(x)),\nil) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-cons-nil} = & \bfalse \end{eqnarray*}\] as claimed.
  3. First suppose \(a = b\). Now \[\begin{eqnarray*} & & \suffix(\snoc(a,x),\snoc(b,y)) \\ & = & \prefix(\rev(\snoc(a,x)),\rev(\snoc(b,y))) \\ & = & \prefix(\cons(a,\rev(x)),\cons(b,\rev(y))) \\ & = & \prefix(\rev(x),\rev(y)) \\ & = & \suffix(x,y) \end{eqnarray*}\] as claimed. If \(a \neq b\), we have \[\begin{eqnarray*} & & \suffix(\snoc(a,x),\snoc(b,y)) \\ & = & \prefix(\rev(\snoc(a,x)),\rev(\snoc(b,y))) \\ & = & \prefix(\cons(a,\rev(x)),\cons(b,\rev(y))) \\ & = & \bfalse \end{eqnarray*}\] as claimed.

\(\suffix\) also detects the existence of solutions \(z\) to the equation \(y = \cat(z,x)\).

Let \(A\) be a set. The following hold for all \(x,y \in \lists{A}\).

  1. \(\suffix(x,\cat(y,x)) = \btrue\).
  2. If \(\suffix(x,y) = \btrue\), then \(y = \cat(z,x)\) for some \(z \in \lists{A}\).
  1. We have \[\begin{eqnarray*} & & \suffix(x,\cat(y,x)) \\ & = & \prefix(\rev(x),\rev(\cat(y,x))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-rev-cat-antidistribute} = & \prefix(\rev(x),\cat(\rev(x),\rev(y))) \\ & = & \btrue \end{eqnarray*}\] as claimed.
  2. Suppose \(\suffix(x,y) = \btrue\). Then \(\prefix(\rev(x),\rev(y)) = \btrue\), so we have \(\rev(y) = \cat(\rev(x),w)\) for some \(w\). Now \[\begin{eqnarray*} & & y \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-involution} = & \rev(\rev(y)) \\ & = & \rev(\cat(\rev(x),w)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-rev-cat-antidistribute} = & \cat(\rev(w),\rev(\rev(x))) \\ & = & \cat(\rev(w),x) \end{eqnarray*}\] as claimed.

\(\suffix\) interacts with \(\cons\).

Let \(A\) be a set. For all \(x,y \in \lists{A}\) and \(a \in A\), if \(\suffix(x,y)\), then \(\suffix(x,\cons(a,y))\).

Suppose \(\suffix(x,y)\). Then we have \[\begin{eqnarray*} & & \btrue \\ & = & \suffix(x,y) \\ & = & \prefix(\rev(x),\rev(y)) \\ & = & \prefix(\rev(x),\snoc(a,\rev(y))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \prefix(\rev(x),\rev(\cons(a,y))) \\ & = & \suffix(x,\cons(a,y)) \end{eqnarray*}\] as claimed.

\(\suffix\) is a partial order:

Let \(A\) be a set. Then we have the following for all \(x,y,z \in \lists{A}\).

  1. \(\suffix(x,x) = \btrue\).
  2. If \(\suffix(x,y)\) and \(\suffix(y,x)\), then \(x = y\).
  3. If \(\suffix(x,y)\) and \(\suffix(y,z)\), then \(\suffix(x,z)\).
  1. We have \[\begin{eqnarray*} & & \btrue \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#thm-prefix-reflexive} = & \prefix(\rev(x),\rev(x)) \\ & = & \suffix(x,x) \end{eqnarray*}\] as claimed.
  2. If \(\suffix(x,y)\), we have \(y = \cat(u,x)\) for some \(u\). Similarly, if \(\suffix(y,x)\) then \(x = \cat(v,y)\) for some \(v\). Now \[\begin{eqnarray*} & & \cat(\nil,x) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & x \\ & = & \cat(v,y) \\ & = & \cat(v,\cat(u,x)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-associative} = & \cat(\cat(v,u),x) \end{eqnarray*}\] Since \(\cat\) is cancellative, we have \(\nil = \cat(v,u)\), so that \(u = \nil\), and thus \(x = y\) as claimed.
  3. If \(\suffix(x,y)\) and \(\suffix(y,z)\), then \(\prefix(\rev(x),\rev(y))\) and \(\prefix(\rev(y),\rev(z))\). So \(\prefix(\rev(x),\rev(z))\), and thus \(\suffix(x,z)\).

\(\map\) preserves suffixes:

Let \(A\) and \(B\) be sets with \(f : A \rightarrow B\), and let \(x,y \in \lists{A}\). If \(\suffix(x,y) = \btrue\), then \[\suffix(\map(f)(x),\map(f)(y)) = \btrue.\]

Suppose \(\suffix(x,y)\); then \(\prefix(\rev(x),\rev(y))\). Then we have \[\begin{eqnarray*} & & \suffix(\map(f)(x),\map(f)(y)) \\ & = & \prefix(\rev(\map(f)(x)),\rev(\map(f)(y))) \\ & = & \prefix(\map(f)(\rev(x)),\map(f)(\rev(y))) \\ & = & \btrue \end{eqnarray*}\] as claimed.

\(\suffix\) interacts with \(\length\).

Let \(A\) be a set with \(x,y \in \lists{A}\). If \(\suffix(x,y)\), then \(\nleq(\length(x),\length(y))\).

Suppose \(\suffix(x,y)\). Then \(\prefix(\rev(x),\rev(y))\), so we have \[\begin{eqnarray*} & & \nleq(\length(x),\length(y)) \\ & = & \nleq(\length(\rev(x),\length(\rev(y)))) \\ & = & \btrue \end{eqnarray*}\] as claimed.

As a special case, the prefixes and suffixes of a one-element list coincide.

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

We consider three possibilities for \(x\). If \(x = \nil\), we have \[\begin{eqnarray*} & & \prefix(x,\cons(a,\nil)) \\ & = & \prefix(\nil,\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \btrue \\ & = & \suffix(\nil,\cons(a,\nil)) \\ & = & \suffix(x,\cons(a,\nil)) \end{eqnarray*}\] as needed. If \(x = \cons(b,\nil)\), we have \[\begin{eqnarray*} & & \prefix(x,\cons(a,\nil)) \\ & = & \prefix(\cons(b,\nil),\cons(a,\nil)) \\ & = & \bif{\beq(a,b)}{\prefix(\nil,\nil)}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \bif{\beq(a,b)}{\btrue}{\bfalse} \\ & = & \bif{\beq(a,b)}{\suffix(\nil,\nil)}{\bfalse} \\ & = & \suffix(\snoc(b,\nil),\snoc(a,\nil)) \\ & = & \suffix(\cons(b,\nil),\cons(a,\nil)) \\ & = & \suffix(x,\cons(a,\nil)) \end{eqnarray*}\] as needed. Finally, suppose \(x = \cons(b,\cons(c,u))\) for some \(u\). In this case we have \[\begin{eqnarray*} & & \nleq(\next(\length(\cons(a,\nil))),\length(x)) \\ & = & \nleq(\next(\next(\zero)),\length(\cons(b,\cons(c,u)))) \\ & = & \nleq(\next(\next(\zero)),\next(\next(\length(u)))) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-next-cancel} = & \nleq(\next(\zero),\next(\length(u))) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-next-cancel} = & \nleq(\zero,\length(u)) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-zero} = & \btrue \end{eqnarray*}\] so that \(\prefix(x,\cons(a,\nil)) = \bfalse\). Similarly, \[\nleq(\next(\length(\cons(a,\nil))),\length(x)) = \btrue\] so that \(\suffix(x,\cons(a,\nil)) = \bfalse\) as needed.

Testing

Suite:

_test_prefix_suffix ::
  ( TypeName a, Show a, Equal a, Arbitrary a, CoArbitrary a
  , TypeName (t a), List t
  , TypeName n, Equal n, Natural n, Show n, Arbitrary n
  , Show (t a), Equal (t a), Arbitrary (t a)
  ) => Int -> Int -> t a -> n -> IO ()
_test_prefix_suffix size cases t n = do
  testLabel2 "prefix & suffix" t n

  let args = testArgs size cases

  runTest args (_test_prefix_nil_list t)
  runTest args (_test_prefix_cons_nil t)
  runTest args (_test_prefix_cons_cons t)
  runTest args (_test_prefix_cat t)
  runTest args (_test_prefix_snoc t)
  runTest args (_test_prefix_reflexive t)
  runTest args (_test_prefix_symmetric t)
  runTest args (_test_prefix_transitive t)
  runTest args (_test_prefix_map t)
  runTest args (_test_prefix_zip t)
  runTest args (_test_prefix_length t n)

  runTest args (_test_suffix_prefix t)
  runTest args (_test_suffix_nil_list t)
  runTest args (_test_suffix_snoc_nil t)
  runTest args (_test_suffix_snoc_snoc t)
  runTest args (_test_suffix_cat t)
  runTest args (_test_suffix_cons t)
  runTest args (_test_suffix_reflexive t)
  runTest args (_test_suffix_symmetric t)
  runTest args (_test_suffix_transitive t)
  runTest args (_test_suffix_map t)
  runTest args (_test_suffix_length t n)

  runTest args (_test_prefix_suffix_singleton t)

Main:

main_prefix_suffix :: IO ()
main_prefix_suffix = do
  _test_prefix_suffix 20 100 (nil :: ConsList Bool)  (zero :: Unary)
  _test_prefix_suffix 20 100 (nil :: ConsList Unary) (zero :: Unary)