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

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

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


From: simrob
2010-10-22 09:25 pm (UTC)
Dan pointed out that if I want to prove equivalence of split and splitA the proof is actually very, very nice. I needed an annoying lemma whose proof is Refl = refl in this setup, but the proof is dead simple if that is factored out.

  cong-lem : ∀{A B} {x : A} {y : B} {xs1 xs2 : List A} {ys1 ys2 : List B}
     → (xs1 , ys1) ≡ (xs2 , ys2) 
     → IdT {A = List A × List B} (x :: xs1 , y :: ys1) (x :: xs2 , y :: ys2)
  cong-lem Refl = refl

  split-eqA : ∀{A B} → (lxy : List (A × B)) → split lxy ≡ splitA lxy
  split-eqA [] = refl
  split-eqA ((x , y) :: lxy) = cong-lem (split-eqA lxy)
(Reply) (Parent) (Thread)
From: simrob
2010-10-22 09:58 pm (UTC)
It's cheating when you control the standard library, but I can get rid of cong-lem with a standard subst-equals-for-equals function resp:
  split-eqA : ∀{A B} → (lxy : List (A × B)) → split lxy ≡ splitA lxy
  split-eqA [] = refl
  split-eqA ((x , y) :: lxy) = 
     resp (λ p → x :: fst p , y :: snd p)  (split-eqA lxy)

This whole thread increasingly feels wonderfully like the opposite of a flamewar. Water gun fight?
(Reply) (Parent) (Thread)
[User Picture]From: jcreed
2010-10-22 10:53 pm (UTC)
I think it is even more like politely offering a glass of water to a visiting guest.

Oh, but we also have milk! Or would you like a beer? Soda? Diet? Tea? Coffee? Tactical theorem-prover juice?
(Reply) (Parent) (Thread)