In an effort to become more familiar with Coq, I've been working my way through the Software Foundations book. So far, it's been more about *proving* things with Coq than it's been about *programming* with it (although the distinction is blurry). Yesterday, though, I got to this problem. As the text explains, `combine`

, better known as `zip`

, is a function that takes two lists and combines them into a list of pairs. (For instance, given `[0, 1, 3, 18]`

and `[true, false, false, true]`

, it takes those two lists and "zips" them together, producing `[(0, true), (1, false), (3, false), (18, true)]`

.)

The problem asks you to do the inverse: given the list of pairs, *unzip* it to produce the pair of lists. At first, the only way I could think of to do it was with `map`

:

Fixpoint map {X Y: Type} (fn : X -> Y) (lx : list X) : list Y := match lx with | [] => [] | x::tx => fn x :: map fn tx end. Fixpoint split {X Y : Type} (lxy : list (X*Y)) : (list X * list Y) := (map fst lxy, map snd lxy).

Later, I realized that I could do it in one pass provided I have a couple of accumulator arguments:

Fixpoint split' {X Y : Type} (lxy : list (X*Y)) : (list X * list Y) := let fix f (res1 : list X) (res2 : list Y) (lxy : list (X*Y)) := match lxy with | [] => (res1, res2) | xy::txy => f (res1 ++ [(fst xy)]) (res2 ++ [(snd xy)]) txy end in f [] [] lxy.

So, that was fun. But the larger point is that since I'm doing it in Coq, pretty soon I'll be able to do a machine-assisted proof that `split`

and `split'`

are equivalent, not to mention a proof that `split`

(or `split'`

) actually *is* the inverse of `combine`

. That will be even better.