?

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: simrob
2010-10-22 01:58 pm (UTC)

Because Chris showed-and-telled, I wrote it in Agda as well. Most of it is boilerplate because I 1) perversely insisted on using my own library and 2) I lazily haven't added lists to that library yet.



module Kuper where

  {- Bolierplate -}

  open import Prelude

  data List (A : Set) : Set where
    [] : List A
    _::_ : A → List A → List A

  [_] : ∀{A} → A → List A
  [ x ] = x :: []

  _++_ : ∀{A} → List A -> List A -> List A
  [] ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

  append-cong2 : ∀{A} {a : A} {as bs : List A} 
     → as ≡ bs 
     → (a :: as) ≡ (a :: bs)
  append-cong2 Refl = Refl

  append-nil : ∀{A} {as : List A} → as ++ [] ≡ as
  append-nil {as = []} = Refl
  append-nil {as = a :: as} = append-cong2 (append-nil {as = as})

  assoc-append : ∀{A} {as bs cs : List A}
     → (as ++ (bs ++ cs)) ≡ ((as ++ bs) ++ cs)
  assoc-append {as = []} = Refl
  assoc-append {as = a :: as} = append-cong2 (assoc-append {as = as})
  
  map : ∀{A B} → (A → B) → List A → List B
  map f [] = []
  map f (x :: xs) = f x :: map f xs

  {- Functions -}

  split : ∀{A B} → List (A × B) → List A × List B
  split lxy = (map fst lxy , map snd lxy)

  split' : ∀{A B} → List (A × B) → List A → List B → List A × List B
  split' [] xs ys = (xs , ys)
  split' ((x , y) :: lxy) xs ys = split' lxy (xs ++ [ x ]) (ys ++ [ y ])

  {- Equivalence -}

  split-eq-lem : ∀{A B} (lx : List A) (ly : List B) (lxy : List (A × B))
     → (lx ++ map fst lxy , ly ++ map snd lxy) ≡ split' lxy lx ly
  split-eq-lem lx ly [] = Product.pair-cong append-nil append-nil
  split-eq-lem lx ly ((x , y) :: lxy) =
     Product.pair-cong (assoc-append {as = lx}) (assoc-append {as = ly}) 
     ≡≡ split-eq-lem (lx ++ [ x ]) (ly ++ [ y ]) lxy

  split-eq : ∀{A B} (lxy : List (A × B)) → split lxy ≡ split' lxy [] [] 
  split-eq lxy = split-eq-lem [] [] lxy


Question: the most natural way to express this function, in Agda, was neither of your options. Is the following definition naturally expressible in Coq? This comparison example has taught me at least as much about Coq as I think I knew before, which is to say I know very little.



  splitA : ∀{A B} → List (A × B) → List A × List B
  splitA [] = ([] , [])
  splitA ((x , y) :: lxy) = (x :: fst lxly) , (y :: snd lxly)
     where lxly = splitA lxy
(Reply) (Parent) (Thread)
From: neelk
2010-10-22 02:24 pm (UTC)
Yikes. That program is a pretty strong argument for tactical theorem proving! (As an aside: your natural definition works, but makes you rewrite with the extensionality of pairs to deal with let-bindings showing up in mildly annoying fashion.)
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Require Import List.

Fixpoint split (X Y : Type) (xys : list (X * Y)) :=
  match xys with
    | nil => (nil, nil)
    | cons (x,y) xys' =>
      let (xs', ys') := split xys' in (cons x xs', cons y ys')
  end.

Fixpoint zip (X Y : Type) (xs : list X) (ys : list Y) {struct xs} :=
  match xs, ys with
    | nil, _ => nil
    | _, nil => nil
    | (cons x xs'), (cons y ys') => cons (x,y) (zip xs' ys')
  end.

Lemma pair_ext : forall (A B : Type) (a : A * B), a = (fst a, snd a). 
Proof.
 intros A B [u v]; simpl; auto. (* Why isn't this in the stdlib??? *)
Qed.

Lemma zipsplit : forall (X Y : Type) (xys : list (X * Y)), 
   let (xs, ys) := split xys in zip xs ys = xys.
Proof.
  intros X Y; simpl; induction xys; [simpl; auto | unfold split; fold split].
  rewrite (pair_ext a); rewrite (pair_ext (split xys)) in IHxys |- *.
  simpl; rewrite IHxys; reflexivity.
Qed.
(Reply) (Parent) (Thread)
From: neelk
2010-10-22 02:37 pm (UTC)
Oh, I proved the wrong lemma. Here's the equivalence of split and split', using the definition of split above:
Definition split' (X Y : Type) (xys : list (X * Y)) := (map (@fst _ _) xys, map (@snd _ _) xys).

Lemma split_split' : forall (X Y : Type) (xys : list (X * Y)), split xys = split' xys.
Proof.
  intros X Y; induction xys; auto; simpl.
  rewrite IHxys; rewrite (pair_ext a); rewrite (pair_ext (split' xys)); reflexivity.
Qed.
(Reply) (Parent) (Thread)
From: simrob
2010-10-22 05:29 pm (UTC)
The boilerplate or the proof-after-boilerplate is a strong argument for tactical theorem proving? While I realize Product.pair-cong (assoc-append {as = lx}) (assoc-append {as = ly}) ≡≡ split-eq-lem (lx ++ [ x ]) (ly ++ [ y ]) lxy and intros X Y; induction xys; auto; simpl. rewrite IHxys; rewrite (pair_ext a); rewrite (pair_ext (split' xys)); reflexivity. are probably equally meaningless to someone unfamiliar with the relevant tools, I didn't find it at all inconvenient to write the non-boilerplate part, and now the boilerplate part is in my standard library where it belongs.
(Reply) (Parent) (Thread)
From: neelk
2010-10-24 10:34 am (UTC)
It's not the way the proof looks, since all proof assistants require crazy moon language (except for Isar, apparently). It's the raw size of the proof! That's too big.

I don't think I really believe he stdlib argument. In a dependently-typed language, if you have two libraries with N and M methods, then in general you'll need O(M x N) lemmas describing their interaction. (This is why even my Coq proof feels a bit too complicated to me -- these proofs need to be simple enough that machines can reliably cook them up for us.)
(Reply) (Parent) (Thread)
From: simrob
2010-10-24 04:00 pm (UTC)
Well, I actually don't see that being true, at least not in this case. In Agda, I'm annoyed to have to write proofs about the properties of algebraic structures, but not their interactions.

Basically every nitpicky lemma in my nascent standard library, in Dan's standard library that it's based upon, and literally everything that I wrote in boilerplate that's not map expresses one of the two things
  • A constructor respects equivalence (append-cong2) and is injective.
  • Something is a monoid (assoc-append, append-unit).
Mature-ish libraries (such as the Agda Stdlib) both have something like a ring solver that lets you automate most of these operations.
(Reply) (Parent) (Thread)
[User Picture]From: lindseykuper
2010-10-22 03:24 pm (UTC)
Question: the most natural way to express this function, in Agda, was neither of your options. Is the following definition naturally expressible in Coq?

I would hesitate to say that either of my options were the most natural way to express it in Coq, either. Well, the first one isn't bad. But the "most natural way" probably involves, first of all, letting the type inferencer do more work, and second, relying on libraries more. So, more like Neel did it, probably.
(Reply) (Parent) (Thread)
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)