#### Log in

No account? Create an account
 Equivalent unzippers - Lindsey Kuper [entries|archive|friends|userinfo]
Lindsey Kuper

 [ website | composition.al ] [ userinfo | livejournal userinfo ] [ archive | journal archive ]

Equivalent unzippers [Oct. 21st, 2010|11:50 pm]
Lindsey Kuper
 [ Tags | programming ]

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.

LinkReply

Comments:
 From: 2010-10-22 06:02 am (UTC) (Link)
Do you actually get to prove that two coq functions are equivalent? How do you take apart the construction of split and split' to reason about them? I didn't think you could deal with meta level functions like that, but I've never really used Coq.
(Reply) (Thread)
 From: 2010-10-22 03:12 pm (UTC) (Link)
Yeah, you do. How you "take apart" the definitions depends, but it's a matter of showing that given the same arguments they produce the same results. Look at how Neel did it up above. His `split'` (the one that uses `map`) is basically my `split`, while his `split` is sort of like my `split'` but prettier. Mine might be harder to prove stuff about -- I'm not really sure yet.
(Reply) (Parent) (Thread)
 From: 2010-10-22 04:55 pm (UTC) (Link)
Oh that is crazy, though neel's proof is obviously in crazy moon language.
(Reply) (Parent) (Thread)
 From: 2010-10-22 06:51 pm (UTC) (Link)
Oh, yeah, well, basically this whole post and all the comments and arguably my entire academic field is a my-approach-is-more-crazy-than-yours arms race.
(Reply) (Parent) (Thread)
 From: 2010-10-23 04:55 am (UTC) (Link)
the key word is "extensionality"
(Reply) (Parent) (Thread)