?

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:
[User Picture]From: sstrickl
2010-10-22 06:57 pm (UTC)

Experimenting with the proof script, it turns out I can leave out the second "then have" clause; just leading it to the equivalence of ksplit' and the expanded ksplit is enough for simplification.

Edit: here's the simplest version I've found for that so far:

theorem ksplit_ksplit' : "ksplit l = ksplit' l"
proof (induct rule: ksplit'.induct)
  case (2 a b ABs) 
  assume "ksplit ABs = ksplit' ABs"
  hence "... = (map fst ABs, map snd ABs)" by simp
  thus ?case by simp
qed (simp)

The simp on the qed gets rid of the trivial case, and Sam helped clean up the other case a bit. (Can you tell we're bored waiting for our flight this evening out of Reno?)



Edited at 2010-10-22 07:05 pm (UTC)
(Reply) (Parent) (Thread)
[User Picture]From: lindseykuper
2010-10-22 07:45 pm (UTC)
Ooh, I like the looks of the Isabelle/HOL proof. Do you have to actually write next when you move on to the next goal, or is that just there for readability?
(Reply) (Parent) (Thread)
[User Picture]From: sstrickl
2010-10-22 07:50 pm (UTC)
Readability; the Isar syntax is geared towards writing human-readable forward proofs. If you drop the next, nothing changes (just tested to make sure).
(Reply) (Parent) (Thread)
[User Picture]From: sstrickl
2010-10-22 10:42 pm (UTC)
Sam said earlier that next has some semantic meaning, but he didn't clarify to me and didn't post a correction here as I requested, so keep that in mind.
(Reply) (Parent) (Thread)