?

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

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: markluffel
2010-10-26 06:52 pm (UTC)

Proof language for non-PL-researchers?

Hey Lindsey et al!
If I wanted to learn one of these wild proof languages, say for doing geometric/computer-graphics proofs, what language would you recommend? I started working through a tutorial for that Omega language, which I understand is rather different from what the folks in this thread are using... but the documentation made it seem to be a better choice for a beginner.

If I'm concerned mostly with ease of use (and libraries for dealing with real numbers, I guess) what should I use?
(Reply) (Thread)
[User Picture]From: lindseykuper
2010-10-26 08:04 pm (UTC)

Re: Proof language for non-PL-researchers?

Hm. Have you looked at GeoProof? Apparently it talks to Coq.

In any case, I'd recommend whichever one has the best library for geometric proofs, since if it doesn't already exist you'll be spending a lot of time building up scaffolding before you can even get started.

To my knowledge, Omega's less a proof assistant than it is a general-purpose language with dependent types. Having said that, the line between the two is blurry, and I think a lot of people like Agda precisely because it straddles that line pretty well.
(Reply) (Parent) (Thread)