Reverse

Posted on 2017-04-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 Reverse
  ( revcat, rev, last, _test_rev, main_rev
  ) where

import Testing
import Flip
import DisjointUnions
import Unary
import Lists
import HeadAndTail
import LeftFold
import Snoc

Today we’ll define a function that takes a list and reverses the order of its elements; say, to turn \((a,b,c)\) into \((c,b,a)\) and vice versa.

First we define a utility as follows.

Let \(A\) be a set. We define a map \(\revcat : \lists{A} \times \lists{A} \rightarrow \lists{A}\) by \[\revcat = \foldl(\flip(\cons)).\]

In Haskell:

revcat :: (List t) => t a -> t a -> t a
revcat = foldl (flip cons)

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

Let \(A\) be a set. Then \(\revcat\) is the unique solution \(f : \lists{A} \times \lists{A} \rightarrow \lists{A}\) to the following system of equations for all \(a \in A\) and \(x,y \in \lists{A}\). \[\left\{\begin{array}{l} f(x,\nil) = x \\ f(x,\cons(a,y)) = f(\cons(a,x),y) \end{array}\right.\]

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


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

Now \(\revcat\) interacts with \(\snoc\).

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

\(\revcat(\snoc(a,x),y) = \snoc(a,\revcat(x,y))\).
\(\revcat(x,\snoc(a,y)) = \cons(a,\revcat(x,y))\).

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

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


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

And we define list reversal in terms of \(\revcat\).

Let \(A\) be a set. We define \(\rev : \lists{A} \rightarrow \lists{A}\) by \[\rev(x) = \revcat(\nil,x).\]

In Haskell:

rev :: (List t) => t a -> t a
rev = revcat nil

Now \(\rev\) is essentially defined here as a left fold, but it can also be characterized as a right fold.

We have \[\rev(x) = \foldr(\nil)(\snoc)(x).\]

Let \(\varphi\) be as defined in the definition of \(\rev\). We proceed by list induction on \(x\). For the base case \(x = \nil\), note that \[\begin{eqnarray*} & & \foldr(\nil)(\snoc)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \nil \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-revcat-nil} = & \revcat(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#def-rev} = & \rev(\nil) \end{eqnarray*}\] For the inductive step, suppose the equality holds for some \(x \in \lists{A}\), and let \(a \in A\). Now \[\begin{eqnarray*} & & \foldr(\nil)(\snoc)(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \snoc(a,\foldr(\nil)(\snoc)(x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-foldr} = & \snoc(a,\rev(x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#def-rev} = & \snoc(a,\revcat(\nil,x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-revcat-snoc-left} = & \revcat(\snoc(a,\nil),x) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \revcat(\cons(a,\nil),x) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-revcat-cons} = & \revcat(\nil,\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#def-rev} = & \rev(\cons(a,x)) \end{eqnarray*}\] as needed.

_test_rev_foldr :: (List t, Equal (t a))
  => t a -> Test (t a -> Bool)
_test_rev_foldr _ =
  testName "rev(x) == foldr(nil,snoc)(x)" $
  \x -> eq (rev x) (foldr nil snoc x)

Because \(\rev\) is equivalent to a \(\foldr(\ast)(\ast)\), it can be characterized as the unique solution to a system of functional equations.

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

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


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

Special cases:

Let \(A\) be a set. For all \(a,b \in A\) we have the following.

\(\rev(\cons(a,\nil)) = \cons(a,\nil)\).
\(\rev(\cons(a,\cons(b,\nil))) = \cons(b,\cons(a,\nil))\).

Note that \[\begin{eqnarray*} & & \rev(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#def-rev} = & \revcat(\nil,\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-revcat-cons} = & \revcat(\cons(a,\nil),\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-revcat-nil} = & \cons(a,\nil) \end{eqnarray*}\] as claimed.
Note that \[\begin{eqnarray*} & & \rev(\cons(a,\cons(b,\nil))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#def-rev} = & \revcat(\nil,\cons(a,\cons(b,\nil))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-revcat-cons} = & \revcat(\cons(a,\nil),\cons(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-revcat-cons} = & \revcat(\cons(b,\cons(a,\nil)),\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-revcat-nil} = & \cons(b,\cons(a,\nil)) \end{eqnarray*}\] as claimed.

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


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

Now \(\rev\) and \(\snoc\) interact:

Let \(A\) be a set. Then for all \(a \in A\) and \(x \in \lists{A}\), we have \[\rev(\snoc(a,x)) = \cons(a,\rev(x)).\]

We have \[\begin{eqnarray*} & & \rev(\snoc(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#def-rev} = & \revcat(\nil,\snoc(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-revcat-snoc-right} = & \cons(a,\revcat(\nil,x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#def-rev} = & \cons(a,\rev(x)) \end{eqnarray*}\] as claimed.

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

And \(\rev\) is an involution.

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

We proceed by list induction. For the base case \(x = \nil\), note that \[\begin{eqnarray*} & & \rev(\rev(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \rev(\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \nil \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some \(x \in \lists{A}\), and let \(a \in A\). Now \[\begin{eqnarray*} & & \rev(\rev(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \rev(\snoc(a,\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-snoc} = & \cons(a,\rev(\rev(x))) \\ & \hyp{\rev(\rev(x)) = x} = & \cons(a,x) \end{eqnarray*}\] as needed.

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

\(\rev\) preserves \(\isnil\) and \(\beq\).

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

\(\isnil(x) = \isnil(\rev(x))\).
\(\beq(x,y) = \beq(\rev(x),\rev(y))\).

We consider two possibilities. If \(x = \nil\), we have \[x = \nil = \rev(\nil) = \rev(x),\] so that \(\isnil(x) = \isnil(\rev(x))\) as claimed. Suppose instead that \(x = \cons(a,u)\) for some \(u\); then \(x = \snoc(b,v)\) for some \(v\). Now we have \[\begin{eqnarray*} & & \isnil(x) \\ & \let{x = \cons(a,u)} = & \isnil(\cons(a,u)) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \isnil(\cons(b,\rev(v))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-rev-snoc} = & \isnil(\rev(\snoc(b,v))) \\ & \let{x = \snoc(b,v)} = & \isnil(\rev(x)) \end{eqnarray*}\] as claimed.
We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \beq(x,y) \\ & \let{x = \nil} = & \beq(\nil,y) \\ & = & \isnil(y) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-isnil-rev} = & \isnil(\rev(y)) \\ & = & \beq(\nil,\rev(y)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \beq(\rev(\nil),\rev(y)) \\ & = & \beq(\rev(x),\rev(y)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(y\) for some \(x\) and let \(a \in A\). We consider two possibilities for \(y\). If \(y = \nil\), we have \[\begin{eqnarray*} & & \beq(\cons(a,x),y) \\ & \hyp{y = \nil} = & \beq(\cons(a,x),\nil) \\ & = & \isnil(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-isnil-rev} = & \isnil(\rev(\cons(a,x))) \\ & = & \beq(\rev(\cons(a,x)),\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \beq(\rev(\cons(a,x)),\rev(\nil)) \\ & \hyp{y = \nil} = & \beq(\rev(\cons(a,x)),\rev(y)) \end{eqnarray*}\] as needed. Suppose instead that \(y = \cons(b,u)\). Using the inductive hypothsis, we have \[\begin{eqnarray*} & & \beq(\cons(a,x),y) \\ & \hyp{y = \cons(b,u)} = & \beq(\cons(a,x),\cons(b,u)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(a,b),\beq(x,u)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#thm-beq-rev} = & \band(\beq(a,b),\beq(\rev(x),\rev(u))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#thm-snoc-eq} = & \beq(\snoc(a,\rev(x)),\snoc(b,\rev(u))) \\ & = & \beq(\rev(\cons(a,x)),\snoc(b,\rev(u))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \beq(\rev(\cons(a,x)),\rev(\cons(b,u))) \\ & \hyp{y = \cons(b,u)} = & \beq(\rev(\cons(a,x)),\rev(y)) \end{eqnarray*}\] as needed.

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


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

And left fold is a reversed right fold.

Let \(f : B \times A \rightarrow B\). Now \[\foldl(f)(e,x) = \foldr(e)(\flip(f))(\rev(x)).\]

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

_test_rev_foldl :: (List t, Equal (t a), Equal a)
  => t a -> Test ((a -> a -> a) -> a -> t a -> Bool)
_test_rev_foldl _ =
  testName "foldl(phi)(e,x) == foldr(e,flip(phi))(rev(x))" $
  \phi e x ->
    let psi a b = phi b a in
    eq (foldl phi e x) (foldr e psi (rev x))

Note that \(\rev\) is a nontrivial involution on \(\lists{A}\) – in particular, that means it is a bijection on \(\lists{A}\) other than the identity. When this happens on a type with an induction principle, if we can show that our nontrivial bijection is actually an isomorphism, we get an alternative induction principle (almost) for free. And indeed, \(\rev\) is an isomorphism taking \(\cons\) to \(\snoc\).

(Snoc Induction.) Let \(A\) be a set, and let \(f : \lists{A} \rightarrow B\) be a map. Suppose \(C \subseteq B\) is a subset with the property that

\(f(\nil) \in C\)
If \(f(x) \in C\) and \(a \in A\), then \(f(\snoc(a,x)) \in C\).

Then we have \(f(x) \in C\) for all \(x \in \lists{A}\).

This proof is analogous to that of the ordinary list induction principle. Define \(T \subseteq \lists{A}\) by \[T = \{ x \in \lists{A} \mid f(x) \in C \}.\] Note that \(\nil \in T\) and if \(x \in T\) and \(a \in A\) then \(\snoc(a,x) \in T\); that is, \((T,\nil,\snoc)\) is an \(A\)-iterative set. We define \(\Theta : \lists{A} \rightarrow T\) to be the fold \[\Theta = \foldr(\nil)(\snoc).\] Now \(\rev : T \rightarrow \lists{A}\) is an \(A\)-iterative homomorphism since \[\rev(\cons(a,x)) = \snoc(a,\rev(x)).\] Thus \(\rev \circ \Theta\) is an \(A\)-inductive homomorphism, which by uniqueness must be the identity on \(\lists{A}\). If \(x \in \lists{A}\), we have \[x = \rev(\rev(x)) = \rev(\id(\rev(x))) = \rev(\rev(\Theta(\rev(x)))) = \Theta(\rev(x)) \in T,\] so that \(T = \lists{A}\) as claimed.

We can define an analog to \(\head\) in terms of \(\rev\):

Let \(A\) be a set. We define \(\last : \lists{A} \rightarrow 1 + A\) by \[\last(x) = \head(\rev(x)).\]

In Haskell:

last :: (List t) => t a -> Union () a
last = head . rev

And \(\last\) has some nice properties.

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

\(\last(\nil) = \lft(\ast)\).
\(\last(\cons(a,\nil)) = \rgt(a)\).
\(\last(\cons(a,\cons(b,x))) = \last(\cons(b,x))\).

We have \[\begin{eqnarray*} & & \last(\nil) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#def-last} = & \head(\rev(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \head(\nil) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-nil} = & \lft(\ast) \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \last(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#def-last} = & \head(\rev(\cons(a,\nil))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \head(\snoc(a,\rev(\nil))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \head(\snoc(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \head(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-cons} = & \rgt(a) \end{eqnarray*}\] as claimed.
Note that \[\begin{eqnarray*} & & \last(\cons(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#def-last} = & \head(\rev(\cons(a,\cons(b,x)))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \head(\snoc(a,\rev(\cons(b,x)))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \head(\snoc(a,\snoc(b,\rev(x)))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#thm-snoc-head} = & \head(\snoc(b,\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \head(\rev(\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#def-last} = & \last(\cons(b,x)) \end{eqnarray*}\] as claimed.

_test_last_nil :: (List t, Equal (t a), Equal a)
  => t a -> Test Bool
_test_last_nil l =
  testName "eq(last(nil),lft(*))" $
  eq (last (nil `withTypeOf` l)) (lft ())


_test_last_one :: (List t, Equal (t a), Equal a)
  => t a -> Test (a -> Bool)
_test_last_one l =
  testName "eq(last(cons(a,xs)),rgt(a))" $
  \a -> eq (last (cons a (nil `withTypeOf` l))) (rgt a)


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

Testing

Suite:

_test_rev ::
  ( 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_rev size cases t = do
  testLabel1 "rev" t
  let args = testArgs size cases

  runTest args (_test_revcat_nil t)
  runTest args (_test_revcat_cons t)
  runTest args (_test_revcat_snoc_left t)
  runTest args (_test_revcat_snoc_right t)
  runTest args (_test_rev_foldr t)
  runTest args (_test_rev_nil t)
  runTest args (_test_rev_cons t)
  runTest args (_test_rev_single t)
  runTest args (_test_rev_double t)
  runTest args (_test_rev_snoc t)
  runTest args (_test_rev_involution t)
  runTest args (_test_rev_isnil t)
  runTest args (_test_rev_eq t)
  runTest args (_test_rev_foldl t)
  runTest args (_test_last_nil t)
  runTest args (_test_last_one t)
  runTest args (_test_cons_last t)

Main:

main_rev :: IO ()
main_rev = do
  _test_rev 20 100 (nil :: ConsList Bool)
  _test_rev 20 100 (nil :: ConsList Unary)