Posted on 2018-01-06 by nbloomf

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude #-}
) 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).$

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)
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)
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)
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)
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.

1. 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*}$
2. 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*}$
1. 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.
2. 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)
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
(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

let args = testArgs size cases

runTest args (_test_zipPad_zipPad_right t)
main_zipPad :: IO ()
_test_zipPad 20 100 (nil :: ConsList Unary) (nil :: ConsList Unary) (zero :: Unary)