Snoc

Posted on 2018-01-05 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 Snoc (
  snoc, _test_snoc, main_snoc
) where

import Testing
import Booleans
import And
import Unary
import Lists
import HeadAndTail
import LeftFold

We’ve defined a set \(\lists{A}\) with a special element \(\nil\), a map \(\cons : A \times \lists{A} \rightarrow \lists{A}\), and a universal map \(\foldr(\ast)(\ast)\). As you might guess we’ll be thinking of the elements of \(\lists{A}\) as finite lists, and they will form a simple kind of data structure.

The \(\cons\) function attaches a new item to the “beginning” of a list; we want an analogous function that attaches items to the “end”.

First let’s tackle adding items to the end of a list; traditionally this operator is called \(\snoc\) as a bad pun on “reverse \(\cons\)”. Now the signature of \(\snoc\) should be something like \[\snoc : A \times \lists{A} \rightarrow \lists{A},\] and \(\foldr(e)(\varphi)\) can be used to build a map \(\lists{A} \rightarrow \lists{A}\), provided \(e\) is in \(\lists{A}\) and \(\varphi : A \times \lists{A} \rightarrow \lists{A}\). Considering the behavior we want \(\snoc\) to have, we define the following.

Let \(A\) be a set. We now define a map \(\snoc : A \times \lists{A} \rightarrow \lists{A}\) by \[\snoc(a,x) = \foldr(\cons(a,\nil))(\cons)(x).\]

In Haskell:

snoc :: (List t) => a -> t a -> t a
snoc a = foldr (cons a nil) cons

Because \(\snoc\) is defined directly as a fold, it is the unique solution to a system of functional equations.

Let \(A\) be a set. Then \(\snoc\) is the unique function \(f : A \times \lists{A} \rightarrow \lists{A}\) with the property that for all \(a,b \in A\) and \(x \in \lists{A}\) we have \[\left\{ \begin{array}{ll} f(a,\nil) = \cons(a,\nil) \\ f(a,\cons(b,x)) = \cons(b,f(a,x)). \end{array} \right.\]

_test_snoc_nil :: (List t, Equal (t a))
  => t a -> Test (a -> Bool)
_test_snoc_nil z =
  testName "snoc(a,nil) == cons(a,nil)" $
  \a ->
    let nil' = nil `withTypeOf` z in
    eq (snoc a nil') (cons a nil')


_test_snoc_cons :: (List t, Equal (t a))
  => t a -> Test (a -> a -> t a -> Bool)
_test_snoc_cons _ =
  testName "snoc(a,cons(b,x)) == cons(b,snoc(a,x))" $
  \a b x -> eq (snoc a (cons b x)) (cons b (snoc a x))

Now \(\snoc\) interacts with \(\foldr(\ast)(\ast)\).

Let \(A\) and \(B\) be sets with \(e \in B\) and \(\varphi : A \times B \rightarrow B\). Then for all \(a \in A\) and \(x \in \lists{A}\) we have \[\foldr(e)(\varphi)(\snoc(a,x)) = \foldr(\varphi(a,e))(\varphi)(x).\]

We proceed by list induction. For the base case \(x = \nil\), note that \[\begin{eqnarray*} & & \foldr(e)(\varphi)(\snoc(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \foldr(e)(\varphi)(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \varphi(a,\foldr(e)(\varphi)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \varphi(a,e) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \foldr(\varphi(a,e))(\varphi)(\nil) \end{eqnarray*}\] as claimed. Suppose now that the equality holds for some \(x \in \lists{A}\). Now \[\begin{eqnarray*} & & \foldr(e)(\varphi)(\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \foldr(e)(\varphi)(\cons(b,\snoc(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \varphi(b,\foldr(e)(\varphi)(\snoc(a,x))) \\ & \hyp{\foldr(e)(\varphi)(\snoc(a,x)) = \foldr(\varphi(a,e))(\varphi)(x)} = & \varphi(b,\foldr(\varphi(a,e))(\varphi)(x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \foldr(\varphi(a,e))(\varphi)(\cons(b,x)) \end{eqnarray*}\] as needed.

We can perform case analysis on lists with \(\snoc\).

Let \(A\) be a set and let \(x \in \lists{A}\). Then either \(x = \nil\) or \(x = \snoc(a,w)\) for some \(w \in \lists{A}\) and \(a \in A\).

We proceed by list induction on \(x\). For the base case \(x = \nil\), the conclusion holds trivially. For the inductive step, suppose the conclusion holds for some \(x\) and let \(a \in A\). Now \(\cons(a,x) \neq \nil\). We have two cases for \(x\); if \(x = \nil\), then \[\cons(a,x) = \cons(a,\nil) = \snoc(a,\nil)\] as needed. Suppose instead that \(x \neq \nil\); by the inductive hypothesis we have \(x = \snoc(b,w)\) for some \(b \in A\) and \(w \in \lists{A}\). Then we have \[\begin{eqnarray*} & & \cons(a,x) \\ & \hyp{x = \snoc(b,w)} = & \cons(a,\snoc(b,w)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \snoc(b,\cons(a,w)) \end{eqnarray*}\] as claimed.

Also, \(\snoc\) interacts with \(\beq\).

Let \(A\) be a set with \(a,b \in A\) and \(x,y \in \lists{A}\). Then \[\beq(\snoc(a,x),\snoc(b,y)) = \band(\beq(a,b),\beq(x,y)).\]

We proceed by list induction on \(x\). For the base case, set \(x = \nil\). We consider two possibilities for \(y\). If \(y = \nil\), we have \[\begin{eqnarray*} & & \beq(\snoc(a,\nil),\snoc(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \beq(\cons(a,\nil),\snoc(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \beq(\cons(a,\nil),\cons(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(a,b),\beq(\nil,\nil)) \end{eqnarray*}\] as needed. If \(y = \cons(c,u)\), we have \[\begin{eqnarray*} & & \beq(\snoc(a,\nil),\snoc(b,y)) \\ & \let{y = \cons(c,u)} = & \beq(\snoc(a,\nil),\snoc(b,\cons(c,u))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \beq(\snoc(a,\nil),\cons(c,\snoc(b,u))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \beq(\cons(a,\nil),\cons(c,\snoc(b,u))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(a,c),\beq(\nil,\snoc(b,u))) \\ & = & \band(\beq(a,c),\bfalse) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-right} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-right} = & \band(\beq(a,b),\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-nil} = & \band(\beq(a,b),\beq(\nil,\cons(c,u))) \\ & \let{y = \cons(c,u)} = & \band(\beq(a,b),\beq(\nil,y)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(a\), \(b\), and \(y\) for some \(x\) and let \(d \in A\). We again consider two possibilities for \(y\). If \(y = \nil\), we have \[\begin{eqnarray*} & & \beq(\snoc(a,\cons(d,x)),\snoc(b,y)) \\ & = & \beq(\snoc(a,\cons(d,x)),\snoc(b,\nil)) \\ & = & \beq(\cons(d,\snoc(a,x)),\cons(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(d,b),\beq(\snoc(a,x),\nil)) \\ & = & \band(\beq(d,b),\bfalse) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-right} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-right} = & \band(\beq(a,b),\bfalse) \\ & = & \band(\beq(a,b),\beq(\cons(d,x),\nil)) \\ & = & \band(\beq(a,b),\beq(\cons(d,x),y)) \end{eqnarray*}\] as needed. Suppose instead that \(y = \cons(c,u)\). Using the inductive hypothesis, we have \[\begin{eqnarray*} & & \beq(\snoc(a,\cons(d,x)),\snoc(b,y)) \\ & \hyp{y = \cons(c,u)} = & \beq(\snoc(a,\cons(d,x)),\snoc(b,\cons(c,u))) \\ & = & \beq(\cons(d,\snoc(a,x)),\snoc(b,\cons(c,u))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \beq(\cons(d,\snoc(a,x)),\cons(c,\snoc(b,u))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(d,c),\beq(\snoc(a,x),\snoc(b,u))) \\ & \hyp{\beq(\snoc(a,x),\snoc(b,u)) = \band(\beq(a,b),\beq(x,u))} = & \band(\beq(d,c),\band(\beq(a,b),\beq(x,u))) \\ & = & \band(\band(\beq(d,c),\beq(a,b)),\beq(x,u)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-commutative} = & \band(\band(\beq(a,b),\beq(d,c)),\beq(x,u)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-associative} = & \band(\beq(a,b),\band(\beq(d,c),\beq(x,u))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(a,b),\beq(\cons(d,x),\cons(c,u))) \\ & \let{y = \cons(c,u)} = & \band(\beq(a,b),\beq(\cons(d,x),y)) \end{eqnarray*}\] as needed.

_test_snoc_eq :: (List t, Equal (t a), Equal a)
  => t a -> Test (a -> a -> t a -> t a -> Bool)
_test_snoc_eq _ =
  testName "eq(snoc(a,x),snoc(b,y)) iff and(eq(a,b),eq(x,y))" $
  \a b x y -> eq
    (eq (snoc a x) (snoc b y))
    (and (eq a b) (eq x y))

Now \(\foldl(\ast)\) interacts with \(\snoc\).

We have \[\foldl(\varphi)(e,\snoc(a,x)) = \varphi(\foldl(\varphi)(e,x),a).\]

We proceed by list induction on \(x\). For the base case we have \[\begin{eqnarray*} & & \foldl(\varphi)(e,\snoc(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \foldl(\varphi)(e,\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\varphi)(\varphi(e,a),\nil) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-nil} = & \varphi(e,a) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-nil} = & \varphi(\foldl(\varphi)(e,\nil),a) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(e\) and \(a\) for some \(x\), and let \(b \in A\). Then we have \[\begin{eqnarray*} & & \foldl(\varphi)(e,\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \foldl(\varphi)(e,\cons(b,\snoc(a,x))) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\varphi)(\varphi(e,b),\snoc(a,x)) \\ & \hyp{\foldl(\varphi)(c,\snoc(a,x)) = \varphi(\foldl(\varphi)(c,x),a)} = & \varphi(\foldl(\varphi)(\varphi(e,b),x),a) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \varphi(\foldl(\varphi)(e,\cons(b,x)),a) \end{eqnarray*}\] as needed.

_test_snoc_foldl :: (List t, Equal (t a), Equal a)
  => t a -> Test ((a -> a -> a) -> a -> a -> t a -> Bool)
_test_snoc_foldl _ =
  testName "foldl(phi)(e,snoc(a,x)) == phi(foldl(phi)(e,x),a)" $
  \phi e a x -> eq
    (foldl phi e (snoc a x))
    (phi (foldl phi e x) a)

And \(\snoc\) is not \(\nil\).

We have \[\isnil(\snoc(a,x)) = \bfalse.\]

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

_test_snoc_isnil :: (List t, Equal (t a), Equal a)
  => t a -> Test (a -> t a -> Bool)
_test_snoc_isnil _ =
  testName "eq(isnil(snoc(a,x)),false)" $
  \a x -> eq (isNil (snoc a x)) false

Many interesting list functions can be implemented in terms of either \(\foldr(\ast)(\ast)\) or \(\foldl(\ast)\), and depending on the function, one may be preferable over the other. A useful question to ask is this: under what circumstances is a given right fold equivalent to a left fold? The next result provides a sufficient condition.

Let \(A\) and \(B\) be sets, and suppose \(\varphi : A \times B \rightarrow B\) has the property that \[\varphi(a,\varphi(b,e)) = \varphi(b,\varphi(a,e))\] for all \(a,b \in A\) and \(e \in B\). Letting \(\psi : B \times A \rightarrow B\) be given by \(\psi(b,a) = \varphi(a,b)\), we have the following.

\(\foldl(\psi)(e,\snoc(a,x)) = \foldl(\psi)(e,\cons(a,x))\).
\(\foldr(e)(\varphi)(x) = \foldl(\psi)(e,x)\).

We proceed by list induction on \(x\). For the base case \(x = \nil\) we have \[\begin{eqnarray*} & & \foldl(\psi)(e)(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \foldl(\psi)(e)(\snoc(a,\nil)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(e\) and \(a\) for some \(x\) and let \(b \in A\). Now \[\begin{eqnarray*} & & \foldl(\psi)(e,\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \foldl(\psi)(e,\cons(b,\snoc(a,x))) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\psi)(\psi(e,b),\snoc(a,x)) \\ & \hyp{\foldl(\psi)(w)(\cons(a,x)) = \foldl(\psi)(w)(\snoc(a,x))} = & \foldl(\psi)(\psi(e,b),\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\psi)(\psi(\psi(e,b),a),x) \\ & = & \foldl(\psi)(\varphi(a,\varphi(b,e)),x) \\ & = & \foldl(\psi)(\varphi(b,\varphi(a,e)),x) \\ & = & \foldl(\psi)(\psi(\psi(e,a),b),x) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\psi)(\psi(e,a),\cons(b,x)) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\psi)(e,\cons(a,\cons(b,x))) \end{eqnarray*}\] as needed.
We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \foldr(e)(\varphi)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & e \\ & = & \foldl(\psi)(e,\nil) \end{eqnarray*}\] as needed. If \(x = \cons(a,\nil)\), we have \[\begin{eqnarray*} & & \foldr(e)(\varphi)(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \varphi(a,\foldr(e)(\varphi)(x)) \\ & = & \varphi(a,\foldl(\psi)(e,x)) \\ & = & \psi(\foldl(\psi)(e,x),a) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#thm-snoc-foldl} = & \foldl(\psi)(e,\snoc(a,x)) \\ & = & \foldl(\psi)(e,\cons(a,x)) \end{eqnarray*}\] as needed.

\(\snoc\) interacts with \(\head\).

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

We consider two possibilities for \(x\). If \(x = \nil\), we have \[\begin{eqnarray*} & & \head(\snoc(a,\snoc(b,\nil))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \head(\snoc(a,\cons(b,\nil))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \head(\cons(b,\snoc(a,\nil))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-cons} = & \rgt(b) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-cons} = & \head(\cons(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \head(\snoc(b,\nil)) \end{eqnarray*}\] and if \(x = \cons(c,y)\) we have \[\begin{eqnarray*} & & \head(\snoc(a,\snoc(b,x))) \\ & \let{x = \cons(c,y)} = & \head(\snoc(a,\snoc(b,\cons(c,y)))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \head(\snoc(a,\cons(c,\snoc(b,y)))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \head(\cons(c,\snoc(a,\snoc(b,y)))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-cons} = & \rgt(c) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-cons} = & \head(\cons(c,\snoc(b,y))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \head(\snoc(b,\cons(c,y))) \\ & \let{x = \cons(c,y)} = & \head(\snoc(b,x)) \end{eqnarray*}\] as needed.

_test_snoc_head :: (List t, Equal (t a), Equal a)
  => t a -> Test (a -> a -> t a -> Bool)
_test_snoc_head _ =
  testName "eq(head(snoc(a,snoc(b,xs))),head(snoc(b,xs)))" $
  \a b x -> eq (head (snoc a (snoc b x))) (head (snoc b x))

Testing

Suite:

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

  let args = testArgs size cases

  runTest args (_test_snoc_nil t)
  runTest args (_test_snoc_cons t)
  runTest args (_test_snoc_eq t)
  runTest args (_test_snoc_foldl t)
  runTest args (_test_snoc_isnil t)
  runTest args (_test_snoc_head t)

Main:

main_snoc :: IO ()
main_snoc = do
  _test_snoc 20 100 (nil :: ConsList Bool)
  _test_snoc 20 100 (nil :: ConsList Unary)