Sublist

Posted on 2017-05-23 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 Sublist
  ( sublist, _test_sublist, main_sublist
  ) where

import Testing
import Booleans
import And
import Tuples
import NaturalNumbers
import LessThanOrEqualTo
import Lists
import HeadAndTail
import DoubleFold
import Snoc
import Reverse
import Cat
import Length
import AllAndAny
import Filter
import Elt

Today we’ll nail down what it means for one list to be a sublist of another. Intuitively, a sublist is “part of” some larger list; but there is some ambiguity here: does the sublist have to be contiguous in the larger list? For example, it seems clear that \[\langle b, c \rangle\] should be considered a sublist of \[\langle a, b, c, d, e \rangle\] while \[\langle e, g \rangle\] should not. But what about \[\langle a, c \rangle,\] or even \[\langle c, a \rangle\] for that matter? First, lists are inherently ordered, so the “sublist” idea should reflect this – sublists have to respect the order of their superlists. On the other hand, it is less crucial that sublists be contiguous in their superlists. Contiguous sublists are still interesting though (for reasons we’ll see later), so we will single them out as infixes (analogous to prefixes and suffixes).

So we have two related but distinct concepts, sublists and infixes, that will need to be dealt with separately. We’ll define two boolean functions, \(\sublist\) and \(\infix\), which detect when one list is a sublist or infix (respectively) of another. We’ll start with \(\sublist\). This function should have a signature like \[\lists{A} \times \lists{A} \rightarrow \bool.\] Double fold was made for situations like this, so we could try to define \(\sublist\) as a double fold like \[\sublist(x,y) = \dfoldr(\delta)(\psi)(\chi)(x,y)\] But if we do this, assuming some reasonable behavior for \(\sublist\), we get stuck! (Try it!) What happens is that the fold eats \(x\), but when \(x\) and \(y\) are not nil but have different first items we need the recursion to un-eat the \(x\) parameter. The fix is to instead fold on \(y\) like \[\sublist(x,y) = \dfoldr(\delta)(\psi)(\chi)(y,x).\]

Blah blah, define \(\sublist\) like this.

Let \(A\) be a set. Define \(\psi : A \times \bool \rightarrow \bool\) by \[\psi(a,p) = \btrue,\] and \(\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}{q}.\] We now define \(\sublist : \lists{A} \times \lists{A} \rightarrow \bool\) by \[\sublist(x,y) = \dfoldr(\isnil)(\psi)(\chi)(y,x).\]

In Haskell:

Since \(\sublist\) is defined as a \(\dfoldr\), it can be characterized as the unique solution to a system of functional equations.

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

\(\sublist\) is reflexive.

Let \(A\) be a set. For all \(x \in \lists{A}\) we have \(\sublist(x,x)\).

We proceed by list induction on \(x\). For the base case \(x = \nil\), certainly \[\sublist(\nil,\nil) = \btrue.\] For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Now \[\begin{eqnarray*} & & \sublist(\cons(a,x),\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \bif{\beq(a,a)}{\sublist(x,x)}{\sublist(\cons(a,x),x)} \\ & = & \sublist(x,x) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-reflexive} = & \btrue \end{eqnarray*}\] as needed.

\(\snoc\) is cancellative inside \(\sublist\).

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

  1. \(\sublist(\nil,\snoc(b,y)) = \btrue\).
  2. \(\sublist(\snoc(a,x),\snoc(a,y)) = \sublist(x,y)\).
  1. There are two possibilities for \(y\). If \(y = \nil\), we have \[\begin{eqnarray*} & & \sublist(\nil,\snoc(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \sublist(\nil,\cons(b,\nil)) \\ & = & \btrue, \end{eqnarray*}\] and if \(y = \cons(c,u)\) we have \[\begin{eqnarray*} & & \sublist(\nil,\snoc(b,\cons(c,u))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \sublist(\nil,\cons(c,\snoc(b,u))) \\ & = & \btrue \end{eqnarray*}\] as claimed.
  2. We proceed by list induction on \(x\). For the base case \(x = \nil\), note that \(\sublist(x,y) = \btrue\). We show that \(\sublist(\snoc(a,\nil),\snoc(a,y)) = \btrue\) by list induction on \(y\). For the base case \(y = \nil\), we have \[\sublist(\snoc(a,\nil),\snoc(a,\nil)) = \btrue\] by reflexivity. For the inductive step (on \(y\)), suppose the equality holds for some \(y\) and let \(b \in A\). Now \[\begin{eqnarray*} & & \sublist(\snoc(a,\nil),\snoc(a,\cons(b,y))) \\ & = & \sublist(\cons(a,\nil),\cons(b,\snoc(a,y))) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \bif{\beq(a,b)}{\sublist(\nil,\snoc(a,y))}{\sublist(\cons(a,\nil),\snoc(a,y))} \\ & = & \bif{\beq(a,b)}{\btrue}{\sublist(\snoc(a,\nil),\snoc(a,y))} \\ & = & \bif{\beq(a,b)}{\btrue}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \btrue \end{eqnarray*}\] as needed. For the inductive step (on \(x\)), suppose the equality holds for some \(x\) and let \(c \in A\). We need to show that \[\sublist(\cons(c,x),y) = \sublist(\snoc(a,\cons(c,x)),\snoc(a,y))\] for all \(y\); we again proceed by list induction on \(y\). For the base case \(y = \nil\), note that \[\begin{eqnarray*} & & \sublist(\cons(c,x),y) \\ & = & \sublist(\cons(c,x),\nil) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil} = & \isnil(\cons(c,x)) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \bfalse \end{eqnarray*}\] and likewise \[\begin{eqnarray*} & & \sublist(\snoc(a,\cons(c,x)),\snoc(a,y)) \\ & = & \sublist(\snoc(a,\cons(c,x)),\snoc(a,\nil)) \\ & = & \sublist(\cons(c,\snoc(a,x)),\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \bif{\beq(c,a)}{\sublist(\snoc(a,x),\nil)}{\sublist(\cons(c,\snoc(a,x)),\nil)} \\ & = & \bif{\beq(c,a)}{\bfalse}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \bfalse \end{eqnarray*}\] as needed. For the inductive step (on \(y\)), suppose we have \[\sublist(\cons(c,x),y) = \sublist(\snoc(a,\cons(c,x)),\snoc(a,y))\] for some \(y\), and let \(b \in A\). Using both the outer and nested inductive hypotheses we have \[\begin{eqnarray*} & & \sublist(\snoc(a,\cons(c,x)),\snoc(a,\cons(b,y))) \\ & = & \sublist(\cons(c,\snoc(a,x)),\cons(b,\snoc(a,y))) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \bif{\beq(c,b)}{\sublist(\snoc(a,x),\snoc(a,y))}{\sublist(\cons(c,\snoc(a,x)),\snoc(a,y))} \\ & = & \bif{\beq(c,b)}{\sublist(x,y)}{\sublist(\snoc(a,\cons(c,x)),\snoc(a,y))} \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-snoc-cancel} = & \bif{\beq(c,b)}{\sublist(x,y)}{\sublist(\cons(c,x),y)} \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \sublist(\cons(c,x),\cons(b,y)) \end{eqnarray*}\] as needed.

\(\cat\) is cancellative inside \(\sublist\).

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

  1. \(\sublist(\cat(z,x),\cat(z,y)) = \sublist(x,y)\).
  2. \(\sublist(\cat(x,z),\cat(y,z)) = \sublist(x,y)\).
  1. We proceed by list induction on \(z\). For the base case \(z = \nil\), of course \[\begin{eqnarray*} & & \sublist(\cat(\nil,x),\cat(\nil,y)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-cat-left-cancel} = & \sublist(x,y) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(x\) and \(y\) for some \(z\), and let \(a \in A\). Now \[\begin{eqnarray*} & & \sublist(\cat(\cons(a,z),x),\cat(\cons(a,z),y)) \\ & = & \sublist(\cons(a,\cat(z,x)),\cons(a,\cat(z,y))) \\ & = & \bif{\beq(a,a)}{\sublist(x,y)}{\sublist(\cons(a,x),y)} \\ & = & \sublist(x,y) \end{eqnarray*}\] as needed.
  2. We proceed by snoc induction on \(z\). For the base case \(z = \nil\), of course \[\begin{eqnarray*} & & \sublist(\cat(x,\nil),\cat(y,\nil)) \\ & = & \sublist(\cat(x,\nil),y,) \\ & = & \sublist(x,y) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(x\) and \(y\) for some \(z\), and let \(a \in A\). Now \[\begin{eqnarray*} & & \sublist(\cat(x,\snoc(a,z)),\cat(y,\snoc(a,z))) \\ & = & \sublist(\snoc(a,\cat(x,z)),\snoc(a,\cat(y,z))) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-snoc-cancel} = & \sublist(\cat(x,z),\cat(y,z)) \\ & \hyp{\sublist(\cat(x,z),\cat(y,z)) = \sublist(x,y)} = & \sublist(x,y) \end{eqnarray*}\] as needed.

Sublist conditionally interacts with \(\cons\). This one seems like it should be obvious, but the only proof I could find was kind of complicated – nested induction of two statements at once.

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

  1. If \(\sublist(x,y) = \btrue\), then \(\sublist(x,\cons(b,y)) = \btrue\).
  2. If \(\sublist(\cons(a,x),y) = \btrue\), then \(\sublist(x,y) = \btrue\).

This proof is a little different: we will prove both (1) and (2) simultaneously by list induction on \(x\). For the base case \(x = \nil\), to see (1), note that for all \(b \in A\) and \(y \in \lists{A}\) we have \[\sublist(\nil,y) = \btrue = \sublist(\nil,\cons(b,y))\] as needed. To see (2), note that \(\sublist(\nil,y)\), so the implication holds regardless of the values of \(a\) and \(y\).

For the inductive step, suppose both (1) and (2) hold for all \(a,b \in A\) and \(y \in \lists{A}\) for some \(x \in \lists{A}\), and let \(c \in A\).

Now we claim that (1) holds with \(x\) replaced by \(\cons(c,x)\); that is, for all \(b \in A\) and \(y \in \lists{A}\), if \(\sublist(\cons(c,x),y) = \btrue\) then \(\sublist(\cons(c,x),\cons(b,y)) = \btrue\). To this end, suppose we have \(\sublist(\cons(c,x),y) = \btrue\). Using part (2) of the induction hypothesis, we have \(\sublist(x,y) = \btrue\). Now \[\begin{eqnarray*} & & \sublist(\cons(c,x),\cons(b,y)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \bif{\beq(c,b)}{\sublist(x,y)}{\sublist(\cons(c,x),y)} \\ & = & \bif{\beq(c,b)}{\btrue}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \btrue \end{eqnarray*}\] as needed.

Next we claim that (2) holds with \(x\) replaced by \(\cons(c,x)\). That is, for all \(a \in A\) and \(y \in \lists{A}\), if \(\sublist(\cons(a,\cons(c,x)),y) = \btrue\) then \(\sublist(\cons(c,x),y) = \btrue\). We proceed by list induction on \(y\). For the base case \(y = \nil\), note that \[\begin{eqnarray*} & & \sublist(\cons(a,\cons(c,x)),y) \\ & = & \sublist(\cons(a,\cons(c,x)),\nil) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil} = & \isnil(\cons(a,\cons(c,x))) \\ & = & \bfalse; \end{eqnarray*}\] thus the implication (2) holds vacuously.

For the inductive step, suppose we have \(y \in \lists{A}\) such that, for all \(a \in A\), if \(\sublist(\cons(a,\cons(c,x)),y) = \btrue\) then \(\sublist(\cons(c,x),y) = \btrue\). Let \(d \in A\), and suppose \[\sublist(\cons(a,\cons(c,x)),\cons(d,y)) = \btrue.\]

We consider two possibilities. If \(a \neq d\), we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cons(a,\cons(c,x)),\cons(d,y)) \\ & = & \sublist(\cons(a,\cons(c,x)),y). \end{eqnarray*}\] By the (nested) induction hypothesis, we have \[\sublist(\cons(c,x),y) = \btrue.\] We established above that this implies \[\sublist(\cons(c,x),\cons(d,y)) = \btrue\] as needed. Now suppose instead that \(a = d\). Then \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cons(a,\cons(c,x)),\cons(d,y)) \\ & = & \sublist(\cons(c,x),y). \end{eqnarray*}\] By part (2) of the (outer) induction hypothesis, we have \[\sublist(x,y) = \btrue.\] Now \[\begin{eqnarray*} & & \sublist(\cons(c,x),\cons(d,y)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \bif{\beq(c,d)}{\sublist(x,y)}{\sublist(\cons(c,x),y)} \\ & = & \bif{\beq(c,d)}{\btrue}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \btrue \end{eqnarray*}\] as needed.

\(\sublist\) interacts with \(\length\).

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

We proceed by list induction on \(y\). For the base case \(y = \nil\), note that \(\length(y) = \zero\). Now if \[\begin{eqnarray*} & & \btrue \\ & \hyp{\sublist(x,y) = \btrue} = & \sublist(x,y) \\ & \hyp{y = \nil} = & \sublist(x,\nil) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil} = & \isnil(x) \end{eqnarray*}\] we have \(x = \nil\), so that \(\length(x) = \zero\). Thus \[\begin{eqnarray*} & & \nleq(\length(x),\length(y)) \\ & = & \nleq(\zero,\zero) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-reflexive} = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for all \(x\) for some \(y\), and let \(b \in A\). We consider two cases for \(x\). If \(x = \nil\), we have \[\begin{eqnarray*} & & \sublist(x,\cons(b,y)) \\ & \hyp{x = \nil} = & \sublist(\nil,\cons(b,y)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil-cons} = & \btrue \end{eqnarray*}\] and furthermore \[\begin{eqnarray*} & & \nleq(\length(x),\length(\cons(b,y))) \\ & \hyp{x = \nil} = & \nleq(\length(\nil),\length(\cons(b,y))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \nleq(\zero,\length(\cons(b,y))) \end{eqnarray*}\] as needed. Suppose then that \(x = \cons(a,u)\), and suppose further that \(\sublist(x,\cons(b,y)) = \btrue\). We have two possibilities. If \(a = b\), we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(x,\cons(b,y)) \\ & \let{x = \cons(a,u)} = & \sublist(\cons(a,u),\cons(b,y)) \\ & \hyp{a = b} = & \sublist(\cons(a,u),\cons(a,y)) \\ & = & \sublist(u,y). \end{eqnarray*}\] By the induction hypothesis, we have \[\begin{eqnarray*} & & \btrue \\ & = & \nleq(\length(u),\length(y)) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-next-cancel} = & \nleq(\next(\length(u)),\next(\length(y))) \\ & = & \nleq(\length(\cons(a,u)),\length(\cons(b,y))) \\ & = & \nleq(\length(x),\length(\cons(b,y))) \end{eqnarray*}\] as needed. If \(a \neq b\), we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(x,\cons(b,y)) \\ & = & \sublist(\cons(a,u),\cons(b,y)) \\ & = & \sublist(\cons(a,u),y). \end{eqnarray*}\] By the induction hypothesis, we have \[\begin{eqnarray*} & & \btrue \\ & = & \nleq(\length(\cons(a,u)),\length(y)) \\ & = & \nleq(\length(x),\length(y)) \\ & = & \nleq(\length(x),\next(\length(y))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \nleq(\length(x),\length(\cons(b,y))) \end{eqnarray*}\] as needed.

\(\sublist\) is antisymmetric.

Let \(A\) be a set, and \(x,y \in \lists{A}\). We have \(\sublist(x,y)\) and \(\sublist(y,x)\) if and only if \(x = y\).

The “if” direction is trivial. To see the “only if” direction we proceed by list induction on \(x\). For the base case \(x = \nil\), note that \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(y,x) \\ & = & \sublist(y,\nil) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil} = & \isnil(y) \end{eqnarray*}\] so that \(y = \nil = x\) as claimed. For the inductive step, suppose the implication holds for some \(x\) and let \(a \in A\). We now consider two possibilities for \(y\). If \(y = \nil\), note that \[\begin{eqnarray*} & & \sublist(\cons(a,x),y) \\ & = & \sublist(\cons(a,x),\nil) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil} = & \isnil(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \bfalse \end{eqnarray*}\] Thus the implication holds vacuously. Suppose instead that \(y = \cons(b,v)\), and suppose further that \(\sublist(\cons(a,x),\cons(b,v))\) and \(\sublist(\cons(b,v),\cons(a,x))\) are both \(\btrue\). If \(a \neq b\), we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cons(b,v),\cons(a,x)) \\ & = & \sublist(\cons(b,v),x) \\ & = & \sublist(y,x). \end{eqnarray*}\] But now we have \[\begin{eqnarray*} & & \btrue \\ & = & \nleq(\length(\cons(a,x)),\length(y)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \nleq(\next(\length(x)),\length(y)) \end{eqnarray*}\] and \[\begin{eqnarray*} & & \btrue \\ & = & \nleq(\length(y),\length(x)); \end{eqnarray*}\] by transitivity, we thus also have \[\nleq(\next(\length(x)),\length(x)),\] a contradiction. So in fact \(a = b\). Thus we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cons(b,v),\cons(a,x)) \\ & = & \sublist(v,x) \end{eqnarray*}\] and \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cons(a,x),\cons(b,v)) \\ & = & \sublist(x,v), \end{eqnarray*}\] so that (by the induction hypothesis) we have \(x = v\), and so \[\begin{eqnarray*} & & \cons(a,x) \\ & = & \cons(b,v) \\ & = & y \end{eqnarray*}\] as needed.

\(\sublist\) is transitive.

Let \(A\) be a set, with \(x,y,z \in \lists{A}\). If \(\sublist(x,y)\) and \(\sublist(y,z)\), then \(\sublist(x,z)\).

We proceed by list induction on \(z\). For the base case \(z = \nil\), note that if \(\sublist(y,z) = \btrue\) we have \(y = \nil\), and then if \(\sublist(x,y) = \btrue\) we also have \(x = \nil\). In particular, \(\sublist(x,z) = \btrue\) as needed. For the inductive step, suppose the implication holds for all \(x\) and \(y\) for some \(z\), and let \(c \in A\). Suppose further that \(\sublist(x,y)\) and \(\sublist(y,\cons(c,z))\). We consider two cases for \(y\). If \(y = \nil\), note that \(x = \nil\), so we have \(\sublist(x,\cons(c,z))\) as claimed. Suppose instead that \(y = \cons(b,v)\). If \(b \neq c\), we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cons(b,v),\cons(c,z)) \\ & = & \sublist(\cons(b,v),z); \end{eqnarray*}\] by the inductive hypothesis, we have \(\sublist(x,z)\), so that \(\sublist(x,\cons(c,z))\) as claimed. Suppose instead that \(b = c\); then we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cons(b,v),\cons(c,z)) \\ & = & \sublist(v,z). \end{eqnarray*}\] We consider two cases for \(x\); if \(x = \nil\), then \(\sublist(x,\cons(c,z))\) as claimed. Suppose instead that \(x = \cons(a,u)\). If \(a \neq b\), we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cons(a,u),\cons(b,v)) \\ & = & \sublist(\cons(a,u),v), \end{eqnarray*}\] and by the inductive hypothesis, \(\sublist(x,z)\), so that \(\sublist(x,\cons(c,z))\) as claimed. If \(a = b\), we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cons(a,u),\cons(b,v)) \\ & = & \sublist(u,v). \end{eqnarray*}\] By the inductive hypothesis, \(\sublist(u,z)\), so that \(\sublist(x,\cons(c,z))\) as claimed.

\(\sublist\) is compatible with \(\cat\).

Let \(A\) be a set. The following hold for all \(x,y,u,v \in \lists{A}\). If \(\sublist(x,u)\) and \(\sublist(y,v)\), then \(\sublist(\cat(x,y),\cat(u,v))\).

If \(\sublist(x,u) = \btrue\), then \(\sublist(\cat(x,y),\cat(u,y)) = \btrue\). Similarly, if \(\sublist(y,v) = \btrue\), then \(\sublist(\cat(u,y),\cat(u,v)) = \btrue\). By transitivity, we have \[\sublist(\cat(x,y),cat(u,v)) = \btrue\] as claimed.

\(\sublist\) interacts with \(\snoc\).

Let \(A\) be a set. For all \(a,b \in A\) and \(x,y \in \lists{A}\) we have \[\sublist(\snoc(a,x),\snoc(b,y)) = \bif{\beq(a,b)}{\sublist(x,y)}{\sublist(\snoc(a,x),y)}.\]

We’ve already seen that \[\sublist(\snoc(a,x),\snoc(a,y)) = \sublist(x,y).\] So it suffices to show that if \(a \neq b\) we have \[\sublist(\snoc(a,x),\snoc(b,y)) = \sublist(\snoc(a,x),y).\] We proceed by list induction on \(y\). For the base case \(y = \nil\), note that \[\begin{eqnarray*} & & \sublist(\snoc(a,x),y) \\ & = & \sublist(\snoc(a,x),\nil) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil} = & \isnil(\snoc(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#thm-isnil-snoc} = & \bfalse \end{eqnarray*}\] We will now show that \(\sublist(\snoc(a,x),\snoc(b,\nil)) = \bfalse\) by considering two cases for \(x\). If \(x = nil\), we have \[\begin{eqnarray*} & & \sublist(\snoc(a,x),\snoc(b,\nil)) \\ & = & \sublist(\snoc(a,\nil),\snoc(b,\nil)) \\ & = & \sublist(\cons(a,\nil),\cons(b,\nil)) \\ & = & \sublist(\cons(a,\nil),\nil) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil} = & \isnil(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \bfalse \end{eqnarray*}\] as needed. If \(x = \cons(c,u)\) and \(\sublist(\snoc(a,x),\snoc(b,\nil)) = \btrue\), we have \[\begin{eqnarray*} & & \btrue \\ & = & \nleq(\length(\snoc(a,x)),\length(\snoc(b,\nil))) \\ & = & \nleq(\next(\length(x)),\next(\length(\nil))) \\ & = & \nleq(\next(\length(\cons(c,u))),\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \nleq(\next(\next(\length(u))),\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-next-next-one} = & \bfalse \end{eqnarray*}\] a contradiction.

Now for the inductive step, suppose the equality holds for some \(y\). That is, for all \(a \neq b\) and all \(x\) we have \[\sublist(\snoc(a,x),\snoc(b,y)) = \sublist(\snoc(a,x),y).\] Let \(d \in A\). We consider two possibilities for \(x\). If \(x = \nil\), we have \[\begin{eqnarray*} & & \sublist(\snoc(a,x),\snoc(b,\cons(d,y))) \\ & = & \sublist(\snoc(a,\nil),\snoc(b,\cons(d,y))) \\ & = & \sublist(\cons(a,\nil),\cons(d,\snoc(b,y))) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \bif{\beq(a,d)}{\sublist(\nil,\snoc(b,y))}{\sublist(\cons(a,\nil),\snoc(b,y))} \\ & = & \bif{\beq(a,d)}{\btrue}{\sublist(\snoc(a,\nil),\snoc(b,y))} \\ & = & \bif{\beq(a,d)}{\btrue}{\sublist(\snoc(a,\nil),y)} \\ & = & \bif{\beq(a,d)}{\sublist(\nil,y)}{\sublist(\cons(a,\nil),y)} \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \sublist(\cons(a,\nil),\cons(d,y)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \sublist(\snoc(a,\nil),\cons(d,y)) \end{eqnarray*}\] as needed. Suppose instead that \(x = \cons(c,u)\). Now we have \[\begin{eqnarray*} & & \sublist(\snoc(a,x),\snoc(b,\cons(d,y))) \\ & = & \sublist(\snoc(a,\cons(c,u)),\snoc(b,\cons(d,y))) \\ & = & \sublist(\cons(c,\snoc(a,u)),\cons(d,\snoc(b,y))) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \bif{\beq(c,d)}{\sublist(\snoc(a,u),\snoc(b,y))}{\sublist(\cons(c,\snoc(a,u)),\snoc(b,y))} \\ & = & \bif{\beq(c,d)}{\sublist(\snoc(a,u),y)}{\sublist(\snoc(a,\cons(c,u)),\snoc(b,y))} \\ & = & \bif{\beq(c,d)}{\sublist(\snoc(a,u),y)}{\sublist(\snoc(a,\cons(c,u)),y)} \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \bif{\beq(c,d)}{\sublist(\snoc(a,u),y)}{\sublist(\cons(c,\snoc(a,u)),y)} \\ & = & \sublist(\cons(c,\snoc(a,u)),\cons(d,y)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \sublist(\snoc(a,\cons(c,u)),\cons(d,y)) \\ & = & \sublist(\snoc(a,x),\cons(d,y)) \end{eqnarray*}\] as needed.

\(\sublist\) interacts with \(\rev\):

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

We proceed by list induction on \(y\). For the base case \(y = \nil\), we have \[\begin{eqnarray*} & & \sublist(x,y) \\ & = & \sublist(x,\nil) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil} = & \isnil(x) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-isnil-rev} = & \isnil(\rev(x)) \\ & = & \sublist(\rev(x),\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \sublist(\rev(x),\rev(\nil)) \\ & = & \sublist(\rev(x),\rev(y)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(x\) for some \(y\) and let \(b \in A\). We consider two possibilities for \(x\). If \(x = \nil\), we have \[\begin{eqnarray*} & & \sublist(x,\cons(b,y)) \\ & = & \sublist(\nil,\cons(b,y)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil-cons} = & \btrue \\ & = & \sublist(\nil,\rev(\cons(b,y))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \sublist(\rev(\nil),\rev(\cons(b,y))) \\ & = & \sublist(\rev(x),\rev(\cons(b,y))) \end{eqnarray*}\] as needed. Suppose instead that \(x = \cons(a,w)\). Then we have \[\begin{eqnarray*} & = & \sublist(\rev(x),\rev(\cons(b,y))) \\ & = & \sublist(\rev(\cons(a,w)),\rev(\cons(b,y))) \\ & = & \sublist(\snoc(a,\rev(w)),\snoc(b,\rev(y))) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-snoc-snoc} = & \bif{\beq(a,b)}{\sublist(\rev(w),\rev(y))}{\sublist(\snoc(a,\rev(w)),\rev(y))} \\ & = & \bif{\beq(a,b)}{\sublist(w,y)}{\sublist(\rev(\cons(a,w)),\rev(y))} \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-rev} = & \bif{\beq(a,b)}{\sublist(w,y)}{\sublist(\cons(a,w),y)} \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \sublist(\cons(a,w),\cons(b,y)) \\ & = & \sublist(x,\cons(b,y)) \end{eqnarray*}\] as needed.

\(\sublist\) interacts conditionally with \(\snoc\) in one argument.

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

  1. If \(\sublist(x,y) = \btrue\), then \(\sublist(x,\snoc(a,y)) = \btrue\).
  2. If \(\sublist(\snoc(a,x),y) = \btrue\), then \(\sublist(x,y) = \btrue\).
  1. Suppose \(\sublist(x,y) = \btrue\). Then we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(x,y) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-rev} = & \sublist(\rev(x),\rev(y)) \\ & = & \sublist(\rev(x),\cons(a,\rev(y))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-snoc} = & \sublist(\rev(x),\rev(\snoc(a,y))) \\ & = & \sublist(x,\snoc(a,y)) \end{eqnarray*}\] as claimed.
  2. Suppose \(\sublist(\snoc(a,x),y) = \btrue\). Then we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\snoc(a,x),y) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-rev} = & \sublist(\rev(\snoc(a,x)),\rev(y)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-snoc} = & \sublist(\cons(a,\rev(x)),\rev(y)) \\ & = & \sublist(\rev(x),\rev(y)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-rev} = & \sublist(x,y) \end{eqnarray*}\] as claimed.

\(\sublist\) interacts conditionally with \(\cat\) in one argument.

Let \(A\) be a set, with \(x,y,z \in \lists{A}\).

  1. If \(\sublist(x,y) = \btrue\), then \(\sublist(x,\cat(z,y)) = \btrue\).
  2. If \(\sublist(x,y) = \btrue\), then \(\sublist(x,\cat(y,z)) = \btrue\).
  3. If \(\sublist(\cat(z,x),y) = \btrue\), then \(\sublist(x,y) = \btrue\).
  4. If \(\sublist(\cat(x,z),y) = \btrue\), then \(\sublist(x,y) = \btrue\).
  1. We proceed by list induction on \(z\). For the base case \(z = \nil\), suppose \(\sublist(x,y) = \btrue\). Then \[\begin{eqnarray*} & & \sublist(x,\cat(z,y)) \\ & = & \sublist(x,\cat(\nil,y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \sublist(x,y) \\ & = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for some \(z\) and let \(a \in A\). Suppose further that \(\sublist(x,y) = \btrue\). Then we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(x,y) \\ & = & \sublist(x,\cat(z,y)) \\ & = & \sublist(x,\cons(a,\cat(z,y))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \sublist(x,\cat(\cons(a,z),y)) \end{eqnarray*}\] as needed.
  2. Suppose \(\sublist(x,y) = \btrue\). Now \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(x,y) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-rev} = & \sublist(\rev(x),\rev(y)) \\ & = & \sublist(\rev(x),\cat(\rev(z),\rev(y))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-rev-cat-antidistribute} = & \sublist(\rev(x),\rev(\cat(y,z))) \\ & = & \sublist(x,\cat(y,z)) \end{eqnarray*}\] as claimed.
  3. We proceed by list induction on \(z\). For the base case \(z = \nil\), suppose \(\sublist(\cat(z,x),y) = \btrue\). Then we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cat(z,x),y) \\ & = & \sublist(\cat(\nil,x),y) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \sublist(x,y) \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for all \(x\) and \(y\) for some \(z\) and let \(a \in A\). Suppose further that \(\sublist(\cat(\cons(a,z),x),y) = \btrue\). Then we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cat(\cons(a,z),x),y) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \sublist(\cons(a,\cat(z,x)),y) \\ & = & \sublist(\cat(z,x),y) \\ & = & \sublist(x,y) \end{eqnarray*}\] as needed.
  4. Suppose \(\sublist(\cat(x,z),y) = \btrue\). Then we have \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(\cat(x,z),y) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-rev} = & \sublist(\rev(\cat(x,z)),\rev(y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-rev-cat-antidistribute} = & \sublist(\cat(\rev(z),\rev(x)),\rev(y)) \\ & = & \sublist(\rev(x),\rev(y)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-rev} = & \sublist(x,y) \end{eqnarray*}\] as needed.

\(\sublist\) interacts with \(\map(f)\) when \(f\) is injective.

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

We proceed by list induction on \(y\). For the base case \(y = \nil\), note that \[\begin{eqnarray*} & & \sublist(\map(f)(x),\map(f)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \sublist(\map(f)(x),\nil) \\ & = & \isnil(\map(f)(x)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-isnil-map} = & \isnil(x) \\ & = & \sublist(x,\nil) \end{eqnarray*}\] as needed. For the inductive step, suppose the equation holds for all \(x\) for some \(y\), and let \(b \in A\). We have two possibilities for \(x\). If \(x = \nil\), we have \[\begin{eqnarray*} & & \sublist(\map(f)(\nil),\map(f)(\cons(b,y))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \sublist(\nil,\map(f)(\cons(b,y))) \\ & = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil-cons} = & \sublist(\nil,\cons(b,y)) \end{eqnarray*}\] as claimed. Suppose instead that \(x = \cons(a,u)\). Note that since \(f\) is injective we have \(\beq(f(a),f(b)) = \beq(a,b)\); then we have \[\begin{eqnarray*} & & \sublist(\map(f)(\cons(a,u)),\map(f)(\cons(b,y))) \\ & = & \sublist(\cons(f(a),\map(f)(u)),\cons(f(b))(\map(f)(y))) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \bif{\beq(f(a),f(b))}{\sublist(\map(f)(u),\map(f)(y))}{\sublist(\cons(f(a),\map(f)(u)),\map(f)(y))} \\ & = & \bif{\beq(f(a),f(b))}{\sublist(u,y)}{\sublist(\map(f)(\cons(a,u)),\map(f)(y))} \\ & = & \bif{\beq(f(a),f(b))}{\sublist(u,y)}{\sublist(\cons(a,u),y)} \\ & = & \bif{\beq(a,b)}{\sublist(u,y)}{\sublist(\cons(a,u),y)} \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \sublist(\cons(a,u),\cons(b,y)) \end{eqnarray*}\] as needed.

\(\sublist\) interacts with \(\filter\).

Let \(A\) be a set, let \(p : A \rightarrow \bool\), and let \(x \in \lists{A}\). Then we have \[\sublist(\filter(p,x),x) = \btrue.\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \sublist(\filter(p,x),x) \\ & = & \sublist(\filter(p,\nil),\nil) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-nil} = & \sublist(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#thm-sublist-reflexive} = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(p\) for some \(x\) and let \(a \in A\). We consider two possibilities. If \(p(a) = \btrue\), we have \[\begin{eqnarray*} & & \sublist(\filter(p,\cons(a,x)),\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-cons} = & \sublist(\bif{p(a)}{\cons(a,\filter(p,x))}{\filter(p,x)},\cons(a,x)) \\ & = & \sublist(\cons(a,\filter(p,x)),\cons(a,x)) \\ & = & \sublist(\filter(p,x),x) \\ & = & \btrue \end{eqnarray*}\] as needed. If \(p(a) = \bfalse\), note that \[\sublist(\filter(p,x),x) = \btrue,\] so that \[\begin{eqnarray*} & & \sublist(\filter(p,\cons(a,x)),\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Filter.html#cor-filter-cons} = & \sublist(\bif{p(a)}{\cons(a,\filter(p,x))}{\filter(p,x)},\cons(a,x)) \\ & = & \sublist(\filter(p,x),\cons(a,x)) \\ & = & \btrue \end{eqnarray*}\] as needed.

\(\sublist\) interacts conditionally with \(\any\) and \(\all\).

Let \(A\) be a set, let \(x,y \in \lists{A}\), and let \(p : A \rightarrow \bool\). If \(\sublist(x,y) = \btrue\), then we have the following.

  1. If \(\all(p,y) = \btrue\) then \(\all(p,x) = \btrue\).
  2. If \(\any(p,x) = \btrue\) then \(\any(p,y) = \btrue\).
  1. We proceed by list induction on \(y\). For the base case \(y = \nil\), since \(\sublist(x,y) = \btrue\) we have \(x = \nil\). Now \[\all(p,y) = \all(p,\nil) = \btrue\] and \[\all(p,x) = \all(p,\nil) = \btrue\] as needed. For the inductive step, suppose the result holds for all \(x\) for some \(y\), and let \(b \in A\). Suppose \(\sublist(x,\cons(b,y)) = \btrue\), and further suppose that \(\all(p,\cons(b,y)) = \btrue\). In particular, note that \(p(b) = \btrue\). We consider two possibilities for \(x\). If \(x = \nil\), note that \[\all(p,x) = \all(p,\nil) = \btrue,\] so the implication holds regardless of \(y\). Suppose instead that \(x = \cons(a,u)\). Now \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(x,\cons(b,y)) \\ & = & \sublist(\cons(a,u),\cons(b,y)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \bif{\beq(a,b)}{\sublist(u,y)}{\sublist(\cons(a,u),y)} \\ & = & \bif{\beq(a,b)}{\all(p,u)}{\all(p,\cons(a,u))} \\ & = & \bif{\beq(a,b)}{\all(p,\cons(a,u))}{\all(p,\cons(a,u))} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \all(p,\cons(a,u)) \\ & = & \all(p,x) \end{eqnarray*}\] as needed.
  2. We prove this implication by contraposition. Suppose \(\any(p,y) = \bfalse\); then we have \[\begin{eqnarray*} & & \btrue \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \bnot(\bfalse) \\ & = & \bnot(\any(p,y)) \\ & = & \all(\bnot \circ p, y). \end{eqnarray*}\] Using (1), we thus have \[\begin{eqnarray*} & & \bfalse \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bnot(\btrue) \\ & = & \bnot(\all(\bnot \circ p,x)) \\ & = & \bnot(\bnot(\any(p,x))) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-involution} = & \any(p,x) \end{eqnarray*}\] as needed.

\(\sublist\) is destroyed by \(\cons\).

Let \(A\) be a set with \(x,y \in \lists{A}\). If \(\sublist(x,y)\), then \(\sublist(\cons(a,y),x) = \bfalse\).

Suppose to the contrary that \(\sublist(\cons(a,y),x) = \btrue\). By transitivity we have \(\sublist(\cons(a,y),y)\), and we also have \(\sublist(y,\cons(a,y))\), so by antisymmetry we have \(y = \cons(a,y)\) – a contradiction.

\(\sublist\) on singleton lists is equivalent to \(\elt\).

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

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \sublist(\cons(a,\nil),\nil) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-nil} = & \isnil(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \bfalse \\ & = & \elt(a,\nil) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(a\) for some \(x\), and let \(b \in A\). Now \[\begin{eqnarray*} & & \sublist(\cons(a,\nil),\cons(b,x)) \\ & \href{/posts/arithmetic-made-difficult/Sublist.html#cor-sublist-cons-cons} = & \bif{\beq(a,b)}{\sublist(\nil,x)}{\sublist(\cons(a,\nil),x)} \\ & = & \bif{\beq(a,b)}{\btrue}{\elt(a,x)} \\ & \href{/posts/arithmetic-made-difficult/Elt.html#cor-elt-cons} = & \elt(a,\cons(b,x)) \end{eqnarray*}\] as needed.

Testing

Suite:

_test_sublist ::
  ( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
  , TypeName (t a), List t
  , Show (t a), Equal (t a), Arbitrary (t a), Equal (t (Pair a a))
  , Natural n
  ) => Int -> Int -> t a -> n -> IO ()
_test_sublist size cases t n = do
  testLabel1 "sublist" t

  let args = testArgs size cases

  runTest args (_test_sublist_list_nil t)
  runTest args (_test_sublist_nil_cons t)
  runTest args (_test_sublist_cons_cons t)
  runTest args (_test_sublist_reflexive t)
  runTest args (_test_sublist_nil_snoc t)
  runTest args (_test_sublist_snoc_cancel t)
  runTest args (_test_sublist_cat_left_cancel t)
  runTest args (_test_sublist_cat_right_cancel t)
  runTest args (_test_sublist_cons_right t)
  runTest args (_test_sublist_cons_left t)
  runTest args (_test_sublist_length t n)
  runTest args (_test_sublist_antisymmetric t)
  runTest args (_test_sublist_transitive t)
  runTest args (_test_sublist_cat_compatible t)
  runTest args (_test_sublist_snoc_snoc t)
  runTest args (_test_sublist_rev t)
  runTest args (_test_sublist_snoc_right t)
  runTest args (_test_sublist_snoc_left t)
  runTest args (_test_sublist_left_cat_right t)
  runTest args (_test_sublist_right_cat_right t)
  runTest args (_test_sublist_left_cat_left t)
  runTest args (_test_sublist_right_cat_left t)
  runTest args (_test_sublist_filter t)
  runTest args (_test_sublist_all t)
  runTest args (_test_sublist_any t)
  runTest args (_test_sublist_cons_not t)
  runTest args (_test_sublist_singleton_elt t)

Main:

main_sublist :: IO ()
main_sublist = do
  _test_sublist 50 200 (nil :: ConsList Bool)  (zero :: Unary)
  _test_sublist 50 200 (nil :: ConsList Unary) (zero :: Unary)