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