@@ -107,6 +107,38 @@ length (x::xs) = 1 + length xs
107107(++) [] right = right
108108(++) (x::xs) right = x :: (xs ++ right)
109109
110+--------------------------------------------------------------------------------
111+-- Zips and unzips
112+--------------------------------------------------------------------------------
113+
114+zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
115+ (length l = length r) -> List c
116+zipWith f [] [] p = []
117+zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
118+
119+zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
120+ (z : List c) -> (length x = length y) -> (length y = length z) -> List d
121+zipWith3 f [] [] [] p q = []
122+zipWith3 f (x::xs) (y::ys) (z::zs) p q =
123+ f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
124+
125+zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
126+zip = zipWith (\x => \y => (x, y))
127+
128+zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
129+ (length y = length z) -> List (a, b, c)
130+zip3 = zipWith3 (\x => \y => \z => (x, y, z))
131+
132+unzip : List (a, b) -> (List a, List b)
133+unzip [] = ([], [])
134+unzip ((l, r)::xs) with (unzip xs)
135+ | (lefts, rights) = (l::lefts, r::rights)
136+
137+unzip3 : List (a, b, c) -> (List a, List b, List c)
138+unzip3 [] = ([], [], [])
139+unzip3 ((l, c, r)::xs) with (unzip3 xs)
140+ | (lefts, centres, rights) = (l::lefts, c::centres, r::rights)
141+
110142--------------------------------------------------------------------------------
111143-- Maps
112144--------------------------------------------------------------------------------
@@ -542,3 +574,24 @@ mapPreservesLengthStepCase = proof {
542574 trivial;
543575}
544576
577+prelude.list.zipWithTailProof = proof {
578+ intros;
579+ rewrite (succInjective (length xs) (length ys) p);
580+ trivial;
581+}
582+
583+
584+---------- Proofs ----------
585+
586+prelude.list.zipWith3TailProof = proof {
587+ intros;
588+ rewrite (succInjective (length xs) (length ys) p);
589+ trivial;
590+}
591+
592+prelude.list.zipWith3TailProof' = proof {
593+ intros;
594+ rewrite (succInjective (length ys) (length zs) q);
595+ trivial;
596+}
597+