ZipPad

Posted on 2018-01-06 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 ZipPad
  ( zipPad, _test_zipPad, main_zipPad
  ) where

import Testing
import Flip
import Tuples
import NaturalNumbers
import MaxAndMin
import Lists
import DoubleFold
import Length
import Map

Now to define $\zipPad$, an alternate interpretation of $\zip$.

Let $A$ and $B$ be sets, with $u \in A$ and $v \in B$. Define $\delta : \lists{B} \rightarrow \lists{A \times B}$ by \[\delta(y) = \map(\tup(u))(y),\] $\psi : A \times \lists{A \times B} \rightarrow \lists{A \times B}$ by \[\psi(a,z) = \cons((a,v),z),\] and $\chi : A \times B \times \lists{B} \times \lists{A \times B} \times \lists{A \times B} \rightarrow \lists{A \times B}$ by \[\chi(a,b,y,z,w) = \cons((a,b),z).\] We then define $\zipPad(u,v) : \lists{A} \times \lists{B} \rightarrow \lists{A \times B}$ by \[\zipPad(u,v) = \dfoldr(\delta)(\psi)(\chi).\]

In Haskell:

zipPad :: (List t) => a -> b -> t a -> t b -> t (Pair a b)
zipPad u v = dfoldr delta psi chi
  where
    delta y = map (tup u) y
    psi a z = cons (tup a v) z
    chi a b _ z _ = cons (tup a b) z

Since $\zipPad(u,v)$ is defined as a $\dfoldr$, it is the unique solution to a system of functional equations.

Let $A$ and $B$ be sets. Then $\zip$ is the unique solution $f : \lists{A} \times \lists{B} \rightarrow \lists{A \times B}$ to the following equations for all $a \in A$, $b \in B$, $x \in \lists{A}$, and $y \in \lists{B}$. \[\left\{\begin{array}{l} f(\nil,y) = \map(\tup(u))(y) \\ f(\cons(a,x),\nil) = \cons(\tup(a)(v),f(x,nil)) \\ f(\cons(a,x),\cons(b,y)) = \cons(\tup(a)(b),f(x,y)) \end{array}\right.\]

_test_zipPad_nil_list :: (List t, Equal (t (Pair a b)))
  => t a -> t b -> Test (a -> b -> t b -> Bool)
_test_zipPad_nil_list ta _ =
  testName "zipPad(u,v)(nil,y) == map(tupL(u))(y)" $
  \u v y -> eq (zipPad u v (nil `withTypeOf` ta) y) (map (tup u) y)


_test_zipPad_cons_nil :: (List t, Equal (t (Pair a b)))
  => t a -> t b -> Test (a -> b -> a -> t a -> Bool)
_test_zipPad_cons_nil _ tb =
  testName "zipPad(u,v)(cons(a,x),nil) == nil" $
  \u v a x -> eq
    (zipPad u v (cons a x) (nil `withTypeOf` tb))
    (cons (tup a v) (zipPad u v x nil))


_test_zipPad_cons_cons :: (List t, Equal (t (Pair a b)))
  => t a -> t b -> Test (a -> b -> a -> t a -> b -> t b -> Bool)
_test_zipPad_cons_cons _ _ =
  testName "zipPad(u,v)(cons(a,x),cons(b,y)) == cons((a,b),zipPad(u,v)(x,y))" $
  \u v a x b y -> eq (zipPad u v (cons a x) (cons b y)) (cons (tup a b) (zipPad u v x y))

$\zipPad$ with a nil right argument is a $\map$.

Let $A$ and $B$ be sets, with $u \in A$ and $v \in B$. For all $x \in \lists{A}$, we have $$\zipPad(u,v)(x,\nil) = \map(\flip(\tup)(v))(x)$.

We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \zipPad(u,v)(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#cor-zippad-nil-left} = & \map(\tup(u))(\nil) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \nil \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \map(\flip(\tup)(v))(\nil) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some $x$ and let $a \in A$. Now \[\begin{eqnarray*} & & \zipPad(u,v)(\cons(a,x),\nil) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#cor-zippad-cons-nil} = & \cons(\tup(a)(v),\zipPad(u,v)(x,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip} = & \cons(\flip(\tup)(v)(a),\zipPad(u,v)(x,\nil)) \\ & \hyp{\zipPad(u,v)(x,\nil) = \map(\flip(\tup)(v))(x)} = & \cons(\flip(\tup)(v)(a),\map(\flip(\tup)(v))(x)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \map(\flip(\tup)(v))(\cons(a,x)) \end{eqnarray*}\] as needed.

_test_zipPad_nil_right :: (List t, Equal (t (Pair a b)))
  => t a -> t b -> Test (a -> b -> t a -> Bool)
_test_zipPad_nil_right _ _ =
  testName "zipPad(u,v)(x,nil) == map(tupR(v))(x)" $
  \u v x -> eq (zipPad u v x nil) (map ((flip tup) v) x)

$\zipPad$ interacts with $\tSwap$.

Let $A$ and $B$ be sets. Then for all $u \in A$, $v \in B$, $x \in \lists{A}$, and $y \in \lists{B}$ we have \[\map(\tSwap)(\zipPad(u,v)(x,y)) = \zipPad(v,u)(y,x).\]

We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \map(\tSwap)(\zipPad(u,v)(\nil,y)) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#cor-zippad-nil-left} = & \map(\tSwap)(\map(\tup(u))(y)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(\map(\tSwap))(\map(\tup(u)))(y) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-map-compose} = & \map(\compose(\tSwap)(\tup(u)))(y) \\ & = & \map(\flip(\tup)(u))(y) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#thm-zippad-nil-right} = & \zipPad(v,u)(y,\nil) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some $x$ and let $a \in A$. Now we consider two cases for $y$; either $y = \nil$ or $y = \cons(b,w)$. If $y = \nil$, we have \[\begin{eqnarray*} & & \map(\tSwap)(\zipPad(u,v)(\cons(a,x),y)) \\ & = & \map(\tSwap)(\zipPad(u,v)(\cons(a,x),\nil)) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#thm-zippad-nil-right} = & \map(\tSwap)(\map(\flip(\tup)(v))(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(\map(\tSwap))(\map(\flip(\tup)(v)))(\cons(a,x)) \\ & = & \map(\compose(\tSwap)(\flip(\tup)(v)))(\cons(a,x)) \\ & = & \map(\tup(v))(\cons(a,x)) \\ & = & \zipPad(u,v)(\nil,\cons(a,x)) \end{eqnarray*}\] as needed. Finally, suppose $y = \cons(b,w)$. Then we have \[\begin{eqnarray*} & & \map(\tSwap)(\zipPad(u,v)(\cons(a,x),y)) \\ & \let{y = \cons(b,w)} = & \map(\tSwap)(\zipPad(u,v)(\cons(a,x),\cons(b,w))) \\ & = & \map(\tSwap)(\cons(\tup(a)(b),\zipPad(u,v)(x,w))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \cons(\tSwap(\tup(a)(b)),\map(\tSwap)(\zipPad(u,v)(x,w))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-tSwap-swap} = & \cons(\tup(b)(a),\map(\tSwap)(\zipPad(u,v)(x,w))) \\ & = & \cons(\tup(b)(a),\zipPad(v,u)(w,x)) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#cor-zippad-cons-cons} = & \zipPad(v,u)(\cons(b,w),\cons(a,x)) \\ & \let{y = \cons(b,w)} = & \zipPad(v,u)(y,\cons(a,x)) \end{eqnarray*}\] as needed.

_test_zipPad_tswap :: (List t, Equal (t (Pair b a)))
  => t a -> t b -> Test (a -> b -> t a -> t b -> Bool)
_test_zipPad_tswap _ _ =
  testName "map(tswap)(zipPad(u,v)(x,y)) == zipPad(v,u)(y,x)" $
  \u v x y -> eq (map tswap (zipPad u v x y)) (zipPad v u y x)

$\zipPad$ interacts with $\tPair$.

Let $A$, $B$, $U$, and $V$ be sets, with functions $f : A \rightarrow U$ and $g : B \rightarrow V$. Then for all $u \in A$, $v \in B$, $x \in \lists{A}$, and $y \in \lists{B}$, we have \[\map(\tPair(f,g))(\zipPad(u,v)(x,y)) = \zipPad(f(u),g(v))(\map(f)(x),\map(g)(y)).\]

We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \map(\tPair(f,g))(\zipPad(u,v)(x,y)) \\ & \let{x = \nil} = & \map(\tPair(f,g))(\zipPad(u,v)(\nil,y)) \\ & = & \map(\tPair(f,g))(\map(\tup(u))(y)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(\map(\tPair(f,g)))(\map(\tup(u)))(y) \\ & = & \map(\compose(\tPair(f,g))(\tup(u)))(y) \\ & = & \map(\compose(\tup(f(u)))(g))(y) \\ & = & \map(\tup(f(u)))(\map(g)(y)) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#cor-zippad-nil-left} = & \zipPad(f(u),g(v))(\nil,\map(g)(y)) \\ & = & \zipPad(f(u),g(v))(x,\map(g)(y)) \end{eqnarray*}\] as needed. Now suppose the equality holds for some $x$ and let $a \in A$. We consider two cases for $y$; either $y = \nil$ or $y = \cons(b,w)$. If $y = \nil$, we have \[\begin{eqnarray*} & & \map(\tPair(f,g))(\zipPad(u,v)(\cons(a,x),y)) \\ & = & \map(\tPair(f,g))(\zipPad(u,v)(\cons(a,x),\nil)) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#thm-zippad-nil-right} = & \map(\tPair(f,g))(\map(\flip(\tup)(v))(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(\map(\tPair(f,g)))(\map(\flip(\tup)(v)))(\cons(a,x)) \\ & = & \map(\compose(\tPair(f,g))(\flip(\tup)(v)))(\cons(a,x)) \\ & = & \map(\compose(\flip(\tup)(g(v)))(f))(\cons(a,x)) \\ & = & \map(\flip(\tup)(g(v)))(\map(f)(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#thm-zippad-nil-right} = & \zipPad(f(u),g(v))(\map(f)(\cons(a,x)),\nil) \\ & = & \zipPad(f(u),g(v))(\map(f)(\cons(a,x)),y) \end{eqnarray*}\] as needed. If $y = \cons(b,w)$, we have \[\begin{eqnarray*} & & \map(\tPair(f,g))(\zipPad(u,v)(\cons(a,x),\cons(b,w))) \\ & = & \map(\tPair(f,g))(\cons((a,b),\zipPad(u,v)(x,w))) \\ & = & \cons(\tPair(f,g)(a,b),\map(\tPair(f,g))(\zipPad(u,v)(x,w))) \\ & = & \cons((f(a),g(b)),\zipPad(f(u),g(v))(\map(f)(x),\map(g)(w))) \\ & = & \zipPad(f(u),g(v))(\cons(f(a),\map(f)(x)),\cons(g(b),\map(g)(w))) \\ & = & \zipPad(f(u),g(v))(\map(f)(\cons(a,x)),\map(g)(\cons(b,w))) \\ & = & \zipPad(f(u),g(v))(\map(f)(\cons(a,x)),\map(g)(y)) \end{eqnarray*}\] as needed.

_test_zipPad_tpair :: (List t, Equal (t (Pair a b)))
  => t a -> t b -> Test ((a -> a) -> (b -> b) -> a -> b -> t a -> t b -> Bool)
_test_zipPad_tpair _ _ =
  testName "map(tpair(f,g))(zipPad(u,v)(x,y)) == zipPad(f(u),g(v))(map(f)(x),map(g)(y))" $
  \f g u v x y -> eq
    (map (tpair f g) (zipPad u v x y))
    (zipPad (f u) (g v) (map f x) (map g y))

$\zipPad$ interacts with $\length$.

Let $A$ and $B$ be sets, with $u \in A$, $v \in B$, $x \in \lists{A}$, and $y \in \lists{B}$. Then \[\length(\zipPad(u,v)(x,y)) = \nmax(\length(x),\length(y)).\]

We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \length(\zipPad(u,v)(x,y)) \\ & = & \length(\zipPad(u,v)(\nil,y)) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#cor-zippad-nil-left} = & \length(\map(\tup(u))(y)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-length-map} = & \length(y) \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#thm-max-zero-left} = & \nmax(\zero,\length(y)) \\ & = & \nmax(\length(\nil),\length(y)) \\ & = & \nmax(\length(x),\length(y)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some $x$ and let $a \in A$. We consider two possibilities for $y$: either $y = \nil$ or $y = \cons(b,w)$. If $y = \nil$, we have \[\begin{eqnarray*} & & \length(\zipPad(u,v)(\cons(a,x),y)) \\ & = & \length(\zipPad(u,v)(\cons(a,x),\nil)) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#thm-zippad-nil-right} = & \length(\map(\flip(\tup)(v))(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-length-map} = & \length(\cons(a,x)) \\ & = & \nmax(\length(\cons(a,x)),\zero) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \nmax(\length(\cons(a,x)),\length(\nil)) \\ & = & \nmax(\length(\cons(a,x)),\length(y)) \end{eqnarray*}\] as claimed. Suppose then that $y = \cons(b,w)$. Now \[\begin{eqnarray*} & & \length(\zipPad(u,v)(\cons(a,x),y)) \\ & = & \length(\zipPad(u,v)(\cons(a,x),\cons(b,w))) \\ & = & \length(\cons((a,b),\zipPad(u,v)(x,w))) \\ & = & \next(\length(\zipPad(u,v)(x,w))) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#thm-zippad-length} = & \next(\nmax(\length(x),\length(w))) \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#thm-next-max-distribute} = & \nmax(\next(\length(x)),\next(\length(w))) \\ & = & \nmax(\length(\cons(a,x)),\length(\cons(b,w))) \\ & = & \nmax(\length(\cons(a,x)),\length(y)) \end{eqnarray*}\] as claimed.

_test_zipPad_length :: (List t, Natural n, Equal n)
  => t a -> t b -> n -> Test (a -> b -> t a -> t b -> Bool)
_test_zipPad_length _ _ n =
  testName "length(zipPad(u,v)(x,y)) == max(length(x),length(y))" $
  \u v x y -> eq
    ((length (zipPad u v x y)) `withTypeOf` n)
    (max (length x) (length y))

$\zipPad$ is also kind of associative:

Let $A$, $B$, and $C$ be sets, with $u \in A$, $v \in B$, $w \in C$, $x \in \lists{A}$, $y \in \lists{B}$, and $z \in \lists{C}$. Then the following hold.

We have \[\begin{eqnarray*} & & \zipPad((u,v),w)(\zipPad(u,v)(x,y),z) \\ & = & \map(\tAssocL)(\zipPad(u,(v,w))(x,\zipPad(v,w)(y,z))). \end{eqnarray*}\]
We have \[\begin{eqnarray*} & & \zipPad(u,(v,w))(x,\zipPad(v,w)(y,z)) \\ & = & \map(\tAssocR)(\zipPad((u,v),w)(\zipPad(u,v)(x,y),z)). \end{eqnarray*}\]

We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \zipPad((u,v),w)(\zipPad(u,v)(x,y),z) \\ & = & \zipPad((u,v),w)(\zipPad(u,v)(\nil,y),z) \\ & = & \zipPad((u,v),w)(\nil,z) \\ & = & \nil \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \map(\tAssocL)(\nil) \\ & = & \map(\tAssocL)(\zipPad(u,(v,w))(\nil,\zipPad(v,w)(y,z))) \\ & = & \map(\tAssocL)(\zipPad(u,(v,w))(x,\zipPad(v,w)(y,z))) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some $x$ and let $a \in A$. If $y = \nil$, we have \[\begin{eqnarray*} & & \zipPad((u,v),w)(\zipPad(u,v)(\cons(a,x),y),z) \\ & = & \zipPad((u,v),w)(\zipPad(u,v)(\cons(a,x),\nil),z) \\ & = & \zipPad((u,v),w)(\nil,z) \\ & = & \nil \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \map(\tAssocL)(\nil) \\ & = & \map(\tAssocL)(\zipPad(u,(v,w))(\cons(a,x),\nil)) \\ & = & \map(\tAssocL)(\zipPad(u,(v,w))(\cons(a,x),\zipPad(v,w)(\nil,z))) \\ & = & \map(\tAssocL)(\zipPad(u,(v,w))(\cons(a,x),\zipPad(v,w)(y,z))) \end{eqnarray*}\] as claimed. Similarly, if $z = \nil$, we have \[\begin{eqnarray*} & & \zipPad(\tup(u)(v),w)(\zipPad(u,v)(\cons(a,x),y),z) \\ & \let{z = \nil} = & \zipPad(\tup(u)(v),w)(\zipPad(u,v)(\cons(a,x),y),\nil) \\ & \href{/posts/arithmetic-made-difficult/ZipPad.html#thm-zippad-nil-right} = & \map(\flip(\tup)(w))(\zipPad(u,v)(\cons(a,x),y)) \\ & = & (@@@) \end{eqnarray*}\] as claimed. Suppose then that $y = \cons(b,u)$ and $z = \cons(c,v)$. Using the inductive hypothesis, we have \[\begin{eqnarray*} & & \zipPad((u,v),w)(\zipPad(u,v)(\cons(a,x),y),z) \\ & = & \zipPad((u,v),w)(\zipPad(u,v)(\cons(a,x),\cons(b,u)),\cons(c,v)) \\ & = & \zipPad((u,v),w)(\cons((a,b),\zipPad(u,v)(x,u)),\cons(c,v)) \\ & = & \cons(((a,b),c),\zipPad((u,v),w)(\zipPad(u,v)(x,u),v)) \\ & = & \cons(\tAssocL(a,(b,c)),\map(\tAssocL)(\zipPad(u,(v,w))(x,\zipPad(v,w)(u,v)))) \\ & = & \map(\tAssocL)(\cons((a,(b,c)),\zipPad(u,(v,w))(x,\zipPad(v,w)(u,v)))) \\ & = & \map(\tAssocL)(\zipPad(u,(v,w))(\cons(a,x),\cons((b,c),\zipPad(v,w)(u,v)))) \\ & = & \map(\tAssocL)(\zipPad(u,(v,w))(\cons(a,x),\zipPad(v,w)(\cons(b,u),\cons(c,v)))) \\ & = & \map(\tAssocL)(\zipPad(u,(v,w))(\cons(a,x),\zip(y,z))) \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \zipPad(u,(v,w))(x,\zipPad(v,w)(y,z)) \\ & = & \id(\zipPad(u,(v,w))(x,\zipPad(v,w)(y,z))) \\ & = & \map(\id)(\zipPad(u,(v,w))(x,\zipPad(v,w)(y,z))) \\ & = & \map(\compose(\tAssocR)(\tAssocL))(\zipPad(u,(v,w))(x,\zipPad(v,w)(y,z))) \\ & = & \map(\tAssocR)(\map(\tAssocL)(\zipPad(u,(v,w))(x,\zipPad(v,w)(y,z)))) \\ & = & \map(\tAssocR)(\zipPad((u,v),w)(\zipPad(u,v)(x,y),z)) \end{eqnarray*}\] as claimed.

_test_zipPad_zipPad_left :: (List t, Equal a, Equal (t (Pair (Pair a a) a)))
  => t a -> Test (a -> a -> a -> t a -> t a -> t a -> Bool)
_test_zipPad_zipPad_left _ =
  testName "zipPad((a,b),c)(zipPad(a,b)(x,y),z) == map(tassocL)zipPad(a,(b,c))(x,zipPad(b,c)(y,z))" $
  \a b c x y z -> eq
    (zipPad (tup a b) c (zipPad a b x y) z)
    (map tassocL (zipPad a (tup b c) x (zipPad b c y z)))


_test_zipPad_zipPad_right :: (List t, Equal a, Equal (t (Pair a (Pair a a))))
  => t a -> Test (a -> a -> a -> t a -> t a -> t a -> Bool)
_test_zipPad_zipPad_right _ =
  testName "zipPad((a,b),c)(zipPad(a,b)(x,y),z) == map(tassocR)zipPad(a,(b,c))(x,zipPad(b,c)(y,z))" $
  \a b c x y z -> eq
    (zipPad a (tup b c) x (zipPad b c y z))
    (map tassocR (zipPad (tup a b) c (zipPad a b x y) z))

Testing

Suite:

_test_zipPad ::
  ( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
  , TypeName b, Equal b, Show b, Arbitrary b, CoArbitrary b
  , TypeName n, Natural n, Equal n, Show n, Arbitrary n
  , TypeName (t a), TypeName (t b), List t, Equal (t a), Show (t a), Arbitrary (t a)
  , Equal (t b), Show (t b), Arbitrary (t b), Equal (t (Pair a b)), Equal (t (Pair b a))
  , Equal (t (Pair a (Pair a a))), Equal (t (Pair (Pair a a) a))
  ) => Int -> Int -> t a -> t b -> n -> IO ()
_test_zipPad size cases t u n = do
  testLabel3 "zipPad" t u n

  let args = testArgs size cases

  runTest args (_test_zipPad_nil_list t u)
  runTest args (_test_zipPad_cons_nil t u)
  runTest args (_test_zipPad_cons_cons t u)
  runTest args (_test_zipPad_nil_right t u)
  runTest args (_test_zipPad_tswap t u)
  runTest args (_test_zipPad_tpair t u)
  runTest args (_test_zipPad_length t u n)
  runTest args (_test_zipPad_zipPad_left t)
  runTest args (_test_zipPad_zipPad_right t)

Main:

main_zipPad :: IO ()
main_zipPad = do
  _test_zipPad 20 100 (nil :: ConsList Bool)  (nil :: ConsList Bool)  (zero :: Unary)
  _test_zipPad 20 100 (nil :: ConsList Unary) (nil :: ConsList Unary) (zero :: Unary)