Infix

Posted on 2017-05-24 by nbloomf

Tags: arithmetic-made-difficult, literate-haskell

$\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}$ $\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}$ $\newcommand{\a}{a}$ $\newcommand{\b}{b}$ $\newcommand{\c}{c}$ $\newcommand{\p}{p}$ $\newcommand{\q}{q}$ $\newcommand{\r}{r}$ $\newcommand{\s}{s}$ $\newcommand{\x}{x}$ $\newcommand{\y}{y}$ $\newcommand{\z}{z}$ $\newcommand{\bool}{\mathbb{B}}$ $\newcommand{\btrue}{\mathsf{true}}$ $\newcommand{\bfalse}{\mathsf{false}}$ $\newcommand{\bnot}{\mathsf{not}}$ $\newcommand{\band}{\mathbin{\mathsf{and}}}$ $\newcommand{\bor}{\mathbin{\mathsf{or}}}$ $\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}$ $\newcommand{\beq}{\mathsf{eq}}$ $\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}$ $\newcommand{\id}{\mathsf{id}}$ $\newcommand{\compose}{\mathsf{compose}}$ $\newcommand{\const}{\mathsf{const}}$ $\newcommand{\apply}{\mathsf{apply}}$ $\newcommand{\flip}{\mathsf{flip}}$ $\newcommand{\flipB}{\mathsf{flip2}}$ $\newcommand{\flipC}{\mathsf{flip3}}$ $\newcommand{\flipD}{\mathsf{flip4}}$ $\newcommand{\flipE}{\mathsf{flip5}}$ $\newcommand{\clone}{\mathsf{clone}}$ $\newcommand{\cloneC}{\mathsf{clone3}}$ $\newcommand{\composeAonB}{\mathsf{compose1on2}}$ $\newcommand{\composeAonC}{\mathsf{compose1on3}}$ $\newcommand{\composeAonD}{\mathsf{compose1on4}}$ $\newcommand{\composeBonA}{\mathsf{compose2on1}}$ $\newcommand{\composeBonB}{\mathsf{compose2on2}}$ $\newcommand{\composeConA}{\mathsf{compose3on1}}$ $\newcommand{\ptrue}{\mathsf{ptrue}}$ $\newcommand{\pfalse}{\mathsf{pfalse}}$ $\newcommand{\pnot}{\mathsf{pnot}}$ $\newcommand{\pand}{\mathbin{\mathsf{pand}}}$ $\newcommand{\por}{\mathbin{\mathsf{por}}}$ $\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}$ $\newcommand{\fst}{\mathsf{first}}$ $\newcommand{\snd}{\mathsf{second}}$ $\newcommand{\dup}{\mathsf{dup}}$ $\newcommand{\tup}{\mathsf{tup}}$ $\newcommand{\tSwap}{\mathsf{swap}_{\times}}$ $\newcommand{\tPair}{\mathsf{pair}_{\times}}$ $\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}$ $\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}$ $\newcommand{\tupL}{\mathsf{tupL}}$ $\newcommand{\tupR}{\mathsf{tupR}}$ $\newcommand{\uncurry}{\mathsf{uncurry}}$ $\newcommand{\curry}{\mathsf{curry}}$ $\newcommand{\lft}{\mathsf{left}}$ $\newcommand{\rgt}{\mathsf{right}}$ $\newcommand{\either}{\mathsf{either}}$ $\newcommand{\uSwap}{\mathsf{swap}_{+}}$ $\newcommand{\uPair}{\mathsf{pair}_{+}}$ $\newcommand{\uAssocL}{\mathsf{assocL}_{+}}$ $\newcommand{\uAssocR}{\mathsf{assocR}_{+}}$ $\newcommand{\isLft}{\mathsf{isLeft}}$ $\newcommand{\isRgt}{\mathsf{isRight}}$ $\newcommand{\nats}{\mathbb{N}}$ $\newcommand{\zero}{\mathsf{0}}$ $\newcommand{\next}{\mathsf{next}}$ $\newcommand{\unnext}{\mathsf{unnext}}$ $\newcommand{\iszero}{\mathsf{isZero}}$ $\newcommand{\prev}{\mathsf{prev}}$ $\newcommand{\natrec}{\mathsf{natrec}}$ $\newcommand{\simprec}{\mathsf{simprec}}$ $\newcommand{\bailrec}{\mathsf{bailrec}}$ $\newcommand{\mutrec}{\mathsf{mutrec}}$ $\newcommand{\dnatrec}{\mathsf{dnatrec}}$ $\newcommand{\normrec}{\mathsf{normrec}}$ $\newcommand{\findsmallest}{\mathsf{findsmallest}}$ $\newcommand{\mnormrec}{\mathsf{mnormrec}}$ $\newcommand{\nequal}{\mathsf{eq}}$ $\newcommand{\nplus}{\mathsf{plus}}$ $\newcommand{\ntimes}{\mathsf{times}}$ $\newcommand{\nleq}{\mathsf{leq}}$ $\newcommand{\ngeq}{\mathsf{geq}}$ $\newcommand{\nminus}{\mathsf{minus}}$ $\newcommand{\nmax}{\mathsf{max}}$ $\newcommand{\nmin}{\mathsf{min}}$ $\newcommand{\ndivalg}{\mathsf{divalg}}$ $\newcommand{\nquo}{\mathsf{quo}}$ $\newcommand{\nrem}{\mathsf{rem}}$ $\newcommand{\ndiv}{\mathsf{div}}$ $\newcommand{\ngcd}{\mathsf{gcd}}$ $\newcommand{\ncoprime}{\mathsf{coprime}}$ $\newcommand{\nlcm}{\mathsf{lcm}}$ $\newcommand{\nmindiv}{\mathsf{mindiv}}$ $\newcommand{\nisprime}{\mathsf{isPrime}}$ $\newcommand{\npower}{\mathsf{power}}$ $\newcommand{\nchoose}{\mathsf{choose}}$ $\newcommand{\dom}{\mathsf{dom}}$ $\newcommand{\cod}{\mathsf{cod}}$ $\newcommand{\lists}[1]{\mathsf{List}(#1)}$ $\newcommand{\nil}{\mathsf{nil}}$ $\newcommand{\cons}{\mathsf{cons}}$ $\newcommand{\uncons}{\mathsf{uncons}}$ $\newcommand{\isnil}{\mathsf{isNil}}$ $\newcommand{\tail}{\mathsf{tail}}$ $\newcommand{\head}{\mathsf{head}}$ $\newcommand{\foldr}{\mathsf{foldr}}$ $\newcommand{\foldl}{\mathsf{foldl}}$ $\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}$ $\newcommand{\unfoldN}{\mathsf{unfoldN}}$ $\newcommand{\dfoldr}{\mathsf{dfoldr}}$ $\newcommand{\cfoldr}{\mathsf{cfoldr}}$ $\newcommand{\bfoldr}{\mathsf{bfoldr}}$ $\newcommand{\dbfoldr}{\mathsf{dbfoldr}}$ $\newcommand{\lfoldr}{\mathsf{lfoldr}}$ $\newcommand{\snoc}{\mathsf{snoc}}$ $\newcommand{\revcat}{\mathsf{revcat}}$ $\newcommand{\rev}{\mathsf{rev}}$ $\newcommand{\last}{\mathsf{last}}$ $\newcommand{\cat}{\mathsf{cat}}$ $\newcommand{\addlength}{\mathsf{addlength}}$ $\newcommand{\length}{\mathsf{length}}$ $\newcommand{\head}{\mathsf{head}}$ $\newcommand{\at}{\mathsf{at}}$ $\newcommand{\map}{\mathsf{map}}$ $\newcommand{\range}{\mathsf{range}}$ $\newcommand{\zip}{\mathsf{zip}}$ $\newcommand{\zipPad}{\mathsf{zipPad}}$ $\newcommand{\unzip}{\mathsf{unzip}}$ $\newcommand{\prefix}{\mathsf{prefix}}$ $\newcommand{\suffix}{\mathsf{suffix}}$ $\newcommand{\lcp}{\mathsf{lcp}}$ $\newcommand{\lcs}{\mathsf{lcs}}$ $\newcommand{\all}{\mathsf{all}}$ $\newcommand{\any}{\mathsf{any}}$ $\newcommand{\tails}{\mathsf{tails}}$ $\newcommand{\inits}{\mathsf{inits}}$ $\newcommand{\filter}{\mathsf{filter}}$ $\newcommand{\elt}{\mathsf{elt}}$ $\newcommand{\addcount}{\mathsf{addcount}}$ $\newcommand{\count}{\mathsf{count}}$ $\newcommand{\repeat}{\mathsf{repeat}}$ $\newcommand{\sublist}{\mathsf{sublist}}$ $\newcommand{\infix}{\mathsf{infix}}$ $\newcommand{\select}{\mathsf{select}}$ $\newcommand{\unique}{\mathsf{unique}}$ $\newcommand{\delete}{\mathsf{delete}}$ $\newcommand{\dedupeL}{\mathsf{dedupeL}}$ $\newcommand{\dedupeR}{\mathsf{dedupeR}}$ $\newcommand{\common}{\mathsf{common}}$ $\newcommand{\disjoint}{\mathsf{disjoint}}$ $\newcommand{\sublists}{\mathsf{sublists}}$ $\newcommand{\take}{\mathsf{take}}$ $\newcommand{\drop}{\mathsf{drop}}$ $\newcommand{\takeBut}{\mathsf{takeBut}}$ $\newcommand{\dropBut}{\mathsf{dropBut}}$ $\newcommand{\takeWhile}{\mathsf{takeWhile}}$ $\newcommand{\dropWhile}{\mathsf{dropWhile}}$

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 Infix
  ( isInfix, _test_isInfix, main_isInfix
  ) where

import Testing
import Booleans
import And
import Or
import NaturalNumbers
import Lists
import HeadAndTail
import BailoutFold
import Snoc
import Reverse
import Cat
import PrefixAndSuffix
import AllAndAny
import TailsAndInits
import Sublist

Today we’ll nail down $\infix$, a variant on $\sublist$.

Let $A$ be a set. Define $\beta : A \times \lists{A} \times \lists{A} \rightarrow \bool$ by \[\beta(a,x,y) = \prefix(y,\cons(a,x)),\] $\psi : A \times \lists{A} \times \lists{A} \rightarrow \bool$ by \[\beta(a,x,y) = \btrue,\] and $\omega : A \times \lists{A} \times \lists{A} \rightarrow \lists{A}$ by \[\omega(a,x,y) = y.\] Then define $\infix : \lists{A} \times \lists{A} \rightarrow \bool$ by \[\infix(x,y) = \bfoldr(\isnil)(\beta)(\psi)(\omega)(y,x).\]

In Haskell:

isInfix :: (List t, Equal a) => t a -> t a -> Bool
isInfix x y = bfoldr isNil beta psi omega y x
  where
    beta a z w = prefix w (cons a z)
    psi _ _ _ = true
    omega _ _ w = w

(infix is a reserved word in Haskell, so we’ll call this function isInfix.)

Since $\infix$ is defined in terms of bailout fold, it can be characterized as the unique solution to a system of functional equations.

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

_test_infix_list_nil :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> Bool)
_test_infix_list_nil _ =
  testName "infix(x,nil) == isNil(x)" $
  \x -> eq (isInfix x nil) (isNil x)


_test_infix_list_cons :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> a -> t a -> Bool)
_test_infix_list_cons _ =
  testName "infix(x,cons(b,y)) == if(prefix(x,cons(b,y)),true,infix(x,y))" $
  \x b y -> eq
    (isInfix x (cons b y))
    (if prefix x (cons b y) then true else isInfix x y)

$\infix$ is an $\bor$.

Let $A$ be a set. For all $x,y \in \lists{A}$, we have \[\infix(x,y) = \bor(\prefix(x,y),\infix(x,\tail(y))).\]

We consider two possibilities for $y$. If $y = \nil$, we have \[\begin{eqnarray*} & & \infix(x,\nil) \\ & = & \isnil(x) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-idempotent} = & \bor(\isnil(x),\isnil(x)) \\ & = & \bor(\prefix(x,\nil),\infix(x,\nil)) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-tail-nil} = & \bor(\prefix(x,\nil),\infix(x,\tail(\nil))) \end{eqnarray*}\] as needed. If $y = \cons(b,u)$, we have \[\begin{eqnarray*} & & \infix(x,\cons(b,u)) \\ & = & \bif{\prefix(x,\cons(b,u))}{\btrue}{\infix(x,u)} \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-is-if} = & \bor(\prefix(x,\cons(b,u)),\infix(x,u)) \\ & = & \bor(\prefix(x,y),\infix(x,\tail(y))) \end{eqnarray*}\] as needed.

_test_infix_prefix_or :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_infix_prefix_or _ =
  testName "infix(x,y) == or(prefix(x,y),infix(x,tail(y)))" $
  \x y -> eq (isInfix x y) (or (prefix x y) (isInfix x (tail y)))

$\infix$ is reflexive.

Let $A$ be a set. If $x \in \lists{A}$, then $\infix(x,x) = \btrue$.

We consider two cases for $x$. If $x = \nil$, we have \[\infix(x,x) = \infix(\nil,\nil) = \btrue\] as claimed. If $x = \cons(a,u)$, we have \[\begin{eqnarray*} & & \infix(x,x) \\ & = & \infix(x,\cons(a,u)) \\ & = & \bif{\prefix(x,\cons(a,u))}{\btrue}{\infix(x,u)} \\ & = & \bif{\prefix(x,x)}{\btrue}{\infix(x,u)} \\ & = & \btrue \end{eqnarray*}\] as claimed.

_test_infix_reflexive :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> Bool)
_test_infix_reflexive _ =
  testName "infix(x,x) == true" $
  \x -> eq (isInfix x x) true

$\infix$ interacts with $\cat$:

Let $A$ be a set and $x,y \in \lists{A}$.

$\infix(x,\cat(y,x)) = \btrue$.
$\infix(x,\cat(x,y)) = \btrue$.

We proceed by list induction on $y$. For the base case, note that \[\begin{eqnarray*} & & \infix(x,\cat(y,x)) \\ & = & \infix(x,\cat(\nil,x)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \infix(x,x) \\ & = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some $y$ and let $b \in A$. Now \[\begin{eqnarray*} & & \infix(x,\cat(\cons(b,y),x)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \infix(x,\cons(b,\cat(y,x))) \\ & = & \bor(\prefix(x,\cons(b,\cat(y,x))),\infix(x,\cat(y,x))) \\ & = & \bor(\prefix(x,\cons(b,\cat(y,x))),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}\] as needed.
We consider two possibilities for $x$. If $x = \nil$, we have \[\infix(x,\cat(x,y)) = \infix(\nil,\cat(x,y)) = \btrue\] as claimed. Suppose then that $x = \cons(a,u)$. Then we have \[\begin{eqnarray*} & & \infix(x,\cat(x,y)) \\ & = & \infix(x,\cat(\cons(a,u),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \infix(x,\cons(a,\cat(u,y))) \\ & = & \bor(\prefix(x,\cons(a,\cat(u,y))),\infix(x,\cat(u,y))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \bor(\prefix(x,\cat(\cons(a,u),y)),\infix(x,\cat(u,y))) \\ & = & \bor(\prefix(x,\cat(x,y)),\infix(x,\cat(u,y))) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#thm-prefix-cat-self} = & \bor(\btrue,\infix(x,\cat(u,y))) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \btrue \end{eqnarray*}\] as needed.

_test_infix_cat_right :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_infix_cat_right _ =
  testName "infix(x,cat(x,y)) == true" $
  \x y -> isInfix x (cat x y)


_test_infix_cat_left :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_infix_cat_left _ =
  testName "infix(x,cat(y,x)) == true" $
  \x y -> isInfix x (cat y x)

Prefixes and suffixes are also infixes.

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

If $\prefix(x,y) = \btrue$, then $\infix(x,y) = \btrue$.
If $\suffix(x,y) = \btrue$, then $\infix(x,y) = \btrue$.

Recall that $\prefix(x,y) = \btrue$ if and only if $y = \cat(x,z)$ for some $z$. Then \[\infix(x,y) = \infix(x,\cat(x,z)) = \btrue\] as claimed.
Recall that $\suffix(x,y) = \btrue$ if and only if $y = \cat(z,x)$ for some $z$. Then \[\infix(x,y) = \infix(x,\cat(z,x)) = \btrue\] as claimed.

_test_infix_prefix :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_infix_prefix _ =
  testName "if prefix(x,y) then infix(x,y)" $
  \x y -> if prefix x y then isInfix x y else true


_test_infix_suffix :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_infix_suffix _ =
  testName "if suffix(x,y) then infix(x,y)" $
  \x y -> if suffix x y then isInfix x y else true

$\infix$ interacts conditionally with $\cons$.

Let $A$ be a set with $a \in A$ and $x,y \in \lists{A}$. If $\infix(x,y) = \btrue$, then $\infix(x,\cons(a,y)) = \btrue$.

Note that \[\begin{eqnarray*} & & \infix(x,\cons(a,y)) \\ & = & \bor(\prefix(x,\cons(a,y)),\infix(x,y)) \\ & = & \bor(\prefix(x,\cons(a,y)),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}\] as claimed.

_test_infix_cond_cons :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> a -> Bool)
_test_infix_cond_cons _ =
  testName "if infix(x,y) then infix(x,cons(a,y))" $
  \x y a -> if isInfix x y then isInfix x (cons a y) else true

$\infix$ interacts conditionally with $\snoc$.

Let $A$ be a set with $a \in A$ and $x,y \in \lists{A}$. If $\infix(x,y) = \btrue$, then $\infix(x,\snoc(a,y)) = \btrue$.

We proceed by list induction on $y$. For the base case $y = \nil$, note that we must have $x = \nil$. Now \[\infix(x,\snoc(a,y)) = \infix(\nil,\snoc(a,y)) = \btrue\] as needed. For the inductive step, suppose the implication holds for some $y$ and let $b \in A$. Suppose further that $\infix(x,\cons(b,y)) = \btrue$. Now \[\begin{eqnarray*} & & \btrue \\ & = & \infix(x,\cons(a,y)) \\ & = & \bor(\prefix(x,\cons(b,y)),\infix(x,y)). \end{eqnarray*}\] We have two possibilities. First suppose $\prefix(x,\cons(b,y)) = \btrue$. Then $\prefix(x,\snoc(a,\cons(a,y))) = \btrue$, and so $\infix(x,\snoc(a,\cons(b,y)))$ as needed. Suppose instead that $\infix(x,y) = \btrue$. By the inductive hypothesis we have \[\infix(x,\snoc(a,y)) = \btrue,\] and by the previous result we have \[\begin{eqnarray*} & & \btrue \\ & = & \infix(x,\cons(b,\snoc(a,y))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \infix(x,\snoc(a,\cons(b,y))) \end{eqnarray*}\] as needed.

_test_infix_cond_snoc :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> a -> Bool)
_test_infix_cond_snoc _ =
  testName "if infix(x,y) then infix(x,snoc(a,y))" $
  \x y a -> if isInfix x y then isInfix x (snoc a y) else true

$\infix$ is right-compatible with $\cat$ (from both sides).

Let $A$ be a set and $x,y \in \lists{A}$.

If $\infix(x,y) = \btrue$, then $\infix(x,\cat(y,z)) = \btrue$.
If $\infix(x,y) = \btrue$, then $\infix(x,\cat(z,y)) = \btrue$.

We proceed by list induction on $z$. For the base case $z = \nil$, we have \[\infix(x,\cat(y,z)) = \infix(x,\cat(y,\nil)) = \infix(x,y) = \btrue.\] For the inductive step, suppose the implication holds for some $z$ and let $a \in A$. Now \[\begin{eqnarray*} & & \btrue \\ & = & \infix(x,y) \\ & = & \infix(x,\snoc(a,y)) \\ & = & \infix(x,\cat(\snoc(a,y),z)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \infix(x,\cat(y,\cons(a,z))) \end{eqnarray*}\] as needed.
We proceed by list induction on $z$. For the base case $z = \nil$ we have \[\infix(x,\cat(z,y)) = \infix(x,\cat(\nil,y)) = \infix(x,y) = \btrue\] as needed. For the inductive step, suppose the implication holds for some $z$ and let $a \in A$. Now \[\begin{eqnarray*} & & \btrue \\ & = & \infix(x,y) \\ & = & \infix(x,\cat(z,y)) \\ & = & \infix(x,\cons(a,\cat(z,y))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \infix(x,\cat(\cons(a,z),y)) \end{eqnarray*}\] as needed.

_test_infix_cat_right_compatible_right :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> t a -> Bool)
_test_infix_cat_right_compatible_right _ =
  testName "if infix(x,y) then infix(x,cat(y,z))" $
  \x y z -> if isInfix x y then isInfix x (cat y z) else true


_test_infix_cat_right_compatible_left :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> t a -> Bool)
_test_infix_cat_right_compatible_left _ =
  testName "if infix(x,y) then infix(x,cat(z,y))" $
  \x y z -> if isInfix x y then isInfix x (cat z y) else true

$\infix$ perfectly detects two-sided $\cat$-factorizations.

Let $A$ be a set. Then the following hold for all $x,y \in \lists{A}$.

$\infix(x,\cat(u,\cat(x,v))) = \btrue$ for all $u,v \in \lists{A}$.
If $\infix(x,y) = \btrue$, then $y = \cat(u,\cat(x,v))$ for some $u,v \in \lists{A}$.

We have \[\begin{eqnarray*} & & \btrue \\ & = & \infix(x,x) \\ & = & \infix(x,\cat(x,v)) \\ & = & \infix(x,\cat(u,\cat(x,v))) \end{eqnarray*}\] as claimed.
We proceed by list induction on $y$. For the base case $y = \nil$, if $\infix(x,y) = \btrue$, we have $x = \nil$. Now $x = y$, so that $y = \cat(\nil,\cat(x,\nil))$ as needed. For the inductive step, suppose the implication holds for some $y$ and let $a \in A$. Suppose further that $\infix(x,\cons(a,y)) = \btrue$. Now \[\begin{eqnarray*} & & \btrue \\ & = & \infix(x,\cons(a,y)) \\ & = & \bor(\prefix(x,\cons(a,y)),\infix(x,y)). \end{eqnarray*}\] We have two possibilities. If $\prefix(x,\cons(a,y)) = \btrue$, then $\cons(a,y) = \cat(x,z)$ for some $z$; now \[\cons(a,y) = \cat(\nil,\cat(x,z))\] as needed. Suppose instead that $\infix(x,y) = \btrue$. By the inductive hypothesis we have $y = \cat(u,\cat(x,v))$ for some $u$ and $v$, so that \[\begin{eqnarray*} & & \cons(a,y) \\ & = & \cons(a,\cat(u,\cat(x,v))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \cat(\cons(a,u),\cat(x,v)) \end{eqnarray*}\] as needed.

_test_infix_cat_factor :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> t a -> Bool)
_test_infix_cat_factor _ =
  testName "infix(x,cat(u,cat(x,v)))" $
  \x u v -> isInfix x (cat u (cat x v))

$\infix$ interacts with $\rev$.

Let $A$ be a set. If $x \in \lists{A}$, we have $\infix(\rev(x),\rev(y)) = \infix(x,y)$.

Note that, for all $x,u,v \in \lists{A}$, we have \[\begin{eqnarray*} & & \rev(\cat(u,\cat(x,v))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-rev-cat-antidistribute} = & \cat(\rev(\cat(x,v)),\rev(u)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-rev-cat-antidistribute} = & \cat(\cat(\rev(v),\rev(x)),\rev(u)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-associative} = & \cat(\rev(v),\cat(\rev(x),\rev(u))) \end{eqnarray*}\] In particular, \[y = \cat(u,\cat(x,v))\] for some $u$ and $v$ if and only if \[\rev(y) = \cat(h,\cat(\rev(x),k))\] for some $h$ and $k$. So $\infix(x,y) = \btrue$ if and only if $\infix(\rev(x),\rev(y)) = \btrue$.

_test_infix_rev :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_infix_rev _ =
  testName "infix(rev(x),rev(y)) == infix(x,y)" $
  \x y -> eq (isInfix (rev x) (rev y)) (isInfix x y)

$\snoc(a,x)$ is not an infix of $\nil$.

Let $A$ be a set. For all $a \in A$ and $x \in \lists{A}$, we have \[\infix(\snoc(a,x),\nil) = \bfalse.\]

\[\begin{eqnarray*} & & \infix(\snoc(a,x),\nil) \\ & = & \isnil(\snoc(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#thm-isnil-snoc} = & \bfalse \end{eqnarray*}\] as claimed.

_test_infix_snoc_nil :: (List t, Equal a, Equal (t a))
  => t a -> Test (a -> t a -> Bool)
_test_infix_snoc_nil _ =
  testName "infix(snoc(a,x),nil) == false" $
  \a x -> eq (isInfix (snoc a x) nil) false

$\infix$ interacts with $\snoc$.

Let $A$ be a set. For all $x,y \in \lists{A}$ and $b \in A$, we have \[\infix(x,\snoc(b,y)) = \bor(\suffix(x,\snoc(b,y)),\infix(x,y)).\]

Note that \[\begin{eqnarray*} & & \infix(x,\snoc(b,y)) \\ & = & \infix(\rev(x),\rev(\snoc(b,y))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-snoc} = & \infix(\rev(x),\cons(b,\rev(y))) \\ & = & \bor(\prefix(\rev(x),\cons(b,\rev(y))),\infix(\rev(x),\rev(y))) \\ & = & \bor(\prefix(\rev(x),\rev(\snoc(b,y))),\infix(x,y)) \\ & = & \bor(\suffix(x,\snoc(b,y)),\infix(x,y)) \end{eqnarray*}\] as claimed.

_test_infix_snoc :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> a -> t a -> Bool)
_test_infix_snoc _ =
  testName "infix(x,snoc(b,y)) == or(suffix(x,snoc(b,y)),infix(x,y))" $
  \x b y -> eq
    (isInfix x (snoc b y))
    (or (suffix x (snoc b y)) (isInfix x y))

$\infix$ is antisymmetric.

Let $A$ be a set with $x,y \in \lists{A}$. If $\infix(x,y) = \btrue$ and $\infix(y,x) = \btrue$, then $x = y$.

Suppose $\infix(x,y) = \btrue$; then we have $u$ and $v$ such that \[y = \cat(u,\cat(x,v)).\] Similarly, if $\infix(y,x) = \btrue$ we have $h$ and $k$ such that \[x = \cat(h,\cat(y,k)).\] Now \[\begin{eqnarray*} & & x \\ & = & \cat(h,\cat(y,k)) \\ & = & \cat(h,\cat(\cat(u,\cat(x,v)),k)) \\ & = & \cat(\cat(h,u),\cat(\cat(x,v),k)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-associative} = & \cat(\cat(h,u),\cat(x,\cat(v,k))) \end{eqnarray*}\] so that $\cat(h,u) = \nil$ and $\cat(v,k) = \nil$. Thus $h = k = \nil$, and we have \[\begin{eqnarray*} & & x \\ & = & \cat(h,\cat(y,k)) \\ & = & \cat(\nil,\cat(y,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-nil-right} = & \cat(\nil,y) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & y \end{eqnarray*}\] as claimed.

_test_infix_antisymmetric :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_infix_antisymmetric _ =
  testName "infix(x,y) & infix(y,x) ==> eq(x,y)" $
  \x y -> if and (isInfix x y) (isInfix y x)
    then eq x y
    else true

$\infix$ is transitive.

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

If $\infix(x,y) = \btrue$, we have \[y = \cat(u,\cat(x,v))$ for some $u$ and $v$, and if $\infix(y,z) = \btrue$ we have \]z = (h,cat(y,k))$ for some $h$ and $k$. Now \[\begin{eqnarray*} & & z \\ & = & \cat(h,\cat(y,k)) \\ & = & \cat(h,\cat(\cat(u,\cat(x,v)),k)) \\ & = & \cat(\cat(h,u),\cat(\cat(x,v),k)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-associative} = & \cat(\cat(h,u),\cat(x,\cat(v,k))) \end{eqnarray*}\] so that $\infix(x,z) = \btrue$ as claimed.

_test_infix_transitive :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> t a -> Bool)
_test_infix_transitive _ =
  testName "infix(x,y) & infix(y,z) ==> sublist(x,z)" $
  \x y z -> if and (isInfix x y) (isInfix y z)
    then isInfix x z
    else true

Infixes are also sublists:

Let $A$ be a set and $x,y \in \lists{A}$.

If $\infix(x,y) = \btrue$, then $\sublist(x,y) = \btrue$.
If $\prefix(x,y) = \btrue$, then $\sublist(x,y) = \btrue$.
If $\suffix(x,y) = \btrue$, then $\sublist(x,y) = \btrue$.

We proceed by list induction on $y$. For the base case $y = \nil$, note that if \[\btrue = \infix(x,y) = \infix(x,\nil),\] we have $x = \nil$. Then \[\sublist(x,y) = \sublist(\nil,y) = \btrue\] as needed. For the inductive step, suppose the implication holds for all $x$ for some $y$, and let $a \in A$. Suppose further that $\infix(x,\cons(a,y)) = \btrue$. Now \[\begin{eqnarray*} & & \btrue \\ & = & \infix(x,\cons(a,y)) \\ & = & \bor(\prefix(x,\cons(a,y)),\infix(x,y)). \end{eqnarray*}\] We consider two possibilities. If $\prefix(x,\cons(a,y)) = \btrue$, we consider two possibilities for $x$. If $x = \nil$, we have \[\sublist(x,\cons(a,y)) = \sublist(\nil,\cons(a,y)) = \btrue\] as needed. Suppose then that $x = \cons(b,u)$; since $\prefix(x,\cons(a,y)) = \btrue$, we have $b = a$ and $\prefix(u,y) = \btrue$. Now $\infix(u,y)$, and by the induction hypothesis $\sublist(u,y) = \btrue$, so that \[\begin{eqnarray*} & & \btrue \\ & = & \sublist(u,y) \\ & = & \sublist(\cons(a,u),\cons(a,y)) \\ & = & \sublist(\cons(b,u),\cons(a,y)) \\ & = & \sublist(x,\cons(a,y)) \end{eqnarray*}\] as needed. Now suppose $\infix(x,y) = \btrue$. By the induction hypothesis, we have $\sublist(x,y) = \btrue$, so that $\sublist(x,\cons(b,y)) = \btrue$ as needed.
If $\prefix(x,y) = \btrue$, then $\infix(x,y) = \btrue$.
If $\suffix(x,y) = \btrue$, then $\infix(x,y) = \btrue$.

_test_infix_sublist :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_infix_sublist _ =
  testName "if infix(x,y) then sublist(x,y)" $
  \x y -> if isInfix x y then sublist x y else true


_test_prefix_sublist :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_prefix_sublist _ =
  testName "if prefix(x,y) then sublist(x,y)" $
  \x y -> if prefix x y then sublist x y else true


_test_suffix_sublist :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_suffix_sublist _ =
  testName "if suffix(x,y) then sublist(x,y)" $
  \x y -> if suffix x y then sublist x y else true

$\infix$ is an $\any$.

Let $A$ be a set. For all $x \in \lists{A}$, we have \[\infix(x,y) = \any(\prefix(x,-))(\tails(y)).\]

We proceed by list induction on $y$. For the base case $y = \nil$, we have \[\begin{eqnarray*} & & \any(\prefix(x,-))(\tails(\nil)) \\ & = & \any(\prefix(x,-))(\cons(\nil,\nil)) \\ & = & \bor(\prefix(x,\nil),\any(\prefix(x,-))(\nil)) \\ & = & \bor(\prefix(x,\nil),\btrue) \\ & = & \prefix(x,\nil) \\ & = & \isnil(x) \\ & = & \infix(x,y) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all $x$ for some $y$, and let $a \in A$. Now \[\begin{eqnarray*} & & \infix(x,\cons(a,y)) \\ & = & \bor(\prefix(x,\cons(a,y)),\infix(x,y)) \\ & = & \bor(\prefix(x,\cons(a,y)),\any(\prefix(x,))(\tails(y))) \\ & = & \any(\prefix(x,-))(\cons(\cons(a,y),\tails(y))) \\ & = & \any(\prefix(x,-))(\tails(\cons(a,y))) \end{eqnarray*}\] as needed.

_test_infix_any :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> t a -> Bool)
_test_infix_any _ =
  testName "infix(x,y) == any(prefix(x,-))(tails(y))" $
  \x y -> eq (isInfix x y) (any (prefix x) (tails y))

Testing

Suite:

_test_isInfix ::
  ( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
  , TypeName (t a), List t
  , Equal (t a), Show (t a), Arbitrary (t a)
  ) => Int -> Int -> t a -> IO ()
_test_isInfix size cases t = do
  testLabel1 "infix" t

  let args = testArgs size cases

  runTest args (_test_infix_list_nil t)
  runTest args (_test_infix_list_cons t)
  runTest args (_test_infix_prefix_or t)
  runTest args (_test_infix_reflexive t)
  runTest args (_test_infix_cat_right t)
  runTest args (_test_infix_cat_left t)
  runTest args (_test_infix_prefix t)
  runTest args (_test_infix_suffix t)
  runTest args (_test_infix_cond_cons t)
  runTest args (_test_infix_cond_snoc t)
  runTest args (_test_infix_cat_right_compatible_right t)
  runTest args (_test_infix_cat_right_compatible_left t)
  runTest args (_test_infix_cat_factor t)
  runTest args (_test_infix_rev t)
  runTest args (_test_infix_snoc_nil t)
  runTest args (_test_infix_snoc t)
  runTest args (_test_infix_antisymmetric t)
  runTest args (_test_infix_transitive t)
  runTest args (_test_infix_sublist t)
  runTest args (_test_prefix_sublist t)
  runTest args (_test_suffix_sublist t)
  runTest args (_test_infix_any t)

Main:

main_isInfix :: IO ()
main_isInfix = do
  _test_isInfix 30 1000 (nil :: ConsList Bool)
  _test_isInfix 30 1000 (nil :: ConsList Unary)