# Equivalent unzippers

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.

Tags:
• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic