?

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: lindseykuper
2010-10-22 02:56 pm (UTC)

Ooh, me next, me next!

Here it is in miniKanren:

(import (minikanren vanilla))
(load "matche.scm")

(define zipo
  (lambda (pairoflists listofpairs)
    (matche `(,pairoflists ,listofpairs)
      [( (() ()) () )]
      [( ((,X . ,Xs) (,Y . ,Ys)) ((,X ,Y) . ,XYs) )
       (zipo `(,Xs ,Ys) XYs)])))

> (run* (q) (zipo '((1 3 5) (2 4 6)) q))
(((1 2) (3 4) (5 6)))
> (run* (q) (zipo q '((1 2) (3 4) (5 6))))
(((1 3 5) (2 4 6)))

(Reply) (Parent) (Thread)
[User Picture]From: sstrickl
2010-10-22 06:48 pm (UTC)

Meanwhile I've taken a try at it in Isabelle/HOL using Isar. I make no claim on how "native" this is, given my relative lack of experience in the system.

theory Kuper
imports Main

begin

fun ksplit :: "('a * 'b) list ⇒ 'a list * 'b list"
where "ksplit ABs = (map fst ABs, map snd ABs)"

fun ksplit' :: "('a * 'b) list ⇒ 'a list * 'b list"
where
  "ksplit' [] = ([], [])" |
  "ksplit' ((a, b) # ABs) =
    (case ksplit' ABs of
      (As, Bs) ⇒ (a # As, b # Bs))"

theorem ksplit_ksplit' : "ksplit l = ksplit' l"
proof (induct l rule: ksplit'.induct)
  case 1 thus ?case by simp
next
  case (2 a b ABs)
  assume H : "ksplit ABs = ksplit' ABs"
  then have "ksplit' ABs = (map fst ABs, map snd ABs)" by simp
  then have "ksplit' ((a, b) # ABs) = (a # map fst ABs, b # map snd ABs)" by simp
  thus ?case by simp
qed
  
end
(Reply) (Parent) (Thread)
[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)
[User Picture]From: sstrickl
2010-10-22 07:20 pm (UTC)

Once more, in ACL2!

(defun mymapcar (l)
  (if (endp l) nil
    (cons (car (car l)) (mymapcar (cdr l)))))

(defun mymapcdr (l)
  (if (endp l) nil
    (cons (cdr (car l)) (mymapcdr (cdr l)))))

(defun split1 (l)
  (cons (mymapcar l) (mymapcdr l)))

(defun split2 (l)
  (if (endp l) (cons nil nil)
    (let ((ls (split2 (cdr l))))
      (cons (cons (car (car l)) (car ls))
            (cons (cdr (car l)) (cdr ls))))))

(defthm split1-split2
  (equal (split1 l) (split2 l)))

Notes:

  • ACL2 is first-order, so no ability to use map.
  • Though mapcar/mapcdr exist in Lisp, they're not defined in ACL2, which means I can't even define them by the usual names because it conflicts with the underlying Lisp. (They really should be defined in ACL2 though, boo.)

And with that, I'll stop spamming this post.

Edit: Except for what I got after talking to my local ACL2 expert:

(defun split1 (l)
  (cons (strip-cars l) (strip-cdrs l)))

(defun split2 (l)
  (if (endp l) (cons nil nil)
    (let ((ls (split2 (cdr l))))
      (cons (cons (car (car l)) (car ls))
            (cons (cdr (car l)) (cdr ls))))))

(defthm split1-split2
  (equal (split1 l) (split2 l)))

So "mapcar" is "strip-cars" and "mapcdr" "strip-cdrs"? I am so sending a look of disapproval in the direction of the ACL2 people.



Edited at 2010-10-22 07:24 pm (UTC)
(Reply) (Parent) (Thread)
[User Picture]From: lindseykuper
2010-10-22 07:43 pm (UTC)
In split1-split2, is the l globally quantified? As someone who knows nothing about ACL2, how would you go about proving that theorem in ACL2? Would it be more difficult than using Coq, etc.?
(Reply) (Parent) (Thread)
[User Picture]From: sstrickl
2010-10-22 07:47 pm (UTC)
You don't prove it; you let ACL2 prove it, or fail trying. In the latter case, you try and find the lemma that'll lead ACL2 to the right place and have it attempt that, or realize there's a mistake in your theorem. ACL2 is an automated theorem prover, not a proof assistant.

As for the l in the theorem, ACL2 assumes that unbound variables in theorems are universally quantified (i.e. that's equivalent to "for all l, ...").
(Reply) (Parent) (Thread)
[User Picture]From: lindseykuper
2010-10-22 07:57 pm (UTC)
Oh, okay! So presumably it was able to prove it? Being from Coq-land I'm sort of proof-term-or-it-didn't-happen. (On the other hand, just because I write Qed. at the end of some Coq code and post it on the Internet doesn't mean that Coq actually accepted the proof.)
(Reply) (Parent) (Thread)
[User Picture]From: sstrickl
2010-10-22 08:02 pm (UTC)
Yeah, I wouldn't have posted it here if it'd failed :)

It didn't need any extra lemmas to push the proof through, as this was a pretty simple proof for it. I already included the proof transcript in the previous comment I left.
(Reply) (Parent) (Thread)
(Deleted comment)
[User Picture]From: lindseykuper
2010-10-23 09:16 pm (UTC)
Maybe I'll design a shirt.
(Reply) (Parent) (Thread)
[User Picture]From: sstrickl
2010-10-22 07:55 pm (UTC)

Here's the interactions I had with ACL2 at the REPL, which will give you an idea of what that looks like (well, just the theorem proving part), since the rest puts it over the comment limit):

ACL2 !>
(defthm split1-split2
  (equal (split1 l) (split2 l)))

ACL2 Warning [Non-rec] in ( DEFTHM SPLIT1-SPLIT2 ...):  A :REWRITE
rule generated from SPLIT1-SPLIT2 will be triggered only by terms containing
the non-recursive function symbol SPLIT1.  Unless this function is
disabled, this rule is unlikely ever to be used.


This simplifies, using the :definition SPLIT1, to

Goal'
(EQUAL (CONS (STRIP-CARS L) (STRIP-CDRS L))
       (SPLIT2 L)).

Name the formula above *1.

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  Subsumption reduces that number to one.

We will induct according to a scheme suggested by (SPLIT2 L).  This
suggestion was produced using the :induction rules SPLIT2, STRIP-CARS
and STRIP-CDRS.  If we let (:P L) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP L)) (:P (CDR L)))
              (:P L))
     (IMPLIES (ENDP L) (:P L))).
This induction is justified by the same argument used to admit SPLIT2.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP L))
              (EQUAL (CONS (STRIP-CARS (CDR L))
                           (STRIP-CDRS (CDR L)))
                     (SPLIT2 (CDR L))))
         (EQUAL (CONS (STRIP-CARS L) (STRIP-CDRS L))
                (SPLIT2 L))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP L)
              (EQUAL (CONS (STRIP-CARS (CDR L))
                           (STRIP-CDRS (CDR L)))
                     (SPLIT2 (CDR L))))
         (EQUAL (CONS (STRIP-CARS L) (STRIP-CDRS L))
                (SPLIT2 L))).

This simplifies, using the :definitions SPLIT2, STRIP-CARS and STRIP-CDRS,
primitive type reasoning and the :rewrite rule CONS-EQUAL, to the following
two conjectures.

Subgoal *1/2.2
(IMPLIES (AND (CONSP L)
              (EQUAL (CONS (STRIP-CARS (CDR L))
                           (STRIP-CDRS (CDR L)))
                     (SPLIT2 (CDR L))))
         (EQUAL (STRIP-CARS (CDR L))
                (CAR (SPLIT2 (CDR L))))).

But simplification reduces this to T, using primitive type reasoning,
the :rewrite rule CAR-CONS and the :type-prescription rules SPLIT2
and STRIP-CDRS.

Subgoal *1/2.1
(IMPLIES (AND (CONSP L)
              (EQUAL (CONS (STRIP-CARS (CDR L))
                           (STRIP-CDRS (CDR L)))
                     (SPLIT2 (CDR L))))
         (EQUAL (STRIP-CDRS (CDR L))
                (CDR (SPLIT2 (CDR L))))).

But simplification reduces this to T, using primitive type reasoning
and the :rewrite rule CDR-CONS.

Subgoal *1/1
(IMPLIES (ENDP L)
         (EQUAL (CONS (STRIP-CARS L) (STRIP-CDRS L))
                (SPLIT2 L))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP L))
         (EQUAL (CONS (STRIP-CARS L) (STRIP-CDRS L))
                (SPLIT2 L))).

But simplification reduces this to T, using the :definitions SPLIT2,
STRIP-CARS and STRIP-CDRS and the :executable-counterparts of CONS
and EQUAL.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM SPLIT1-SPLIT2 ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION SPLIT1)
        (:DEFINITION SPLIT2)
        (:DEFINITION STRIP-CARS)
        (:DEFINITION STRIP-CDRS)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SPLIT2)
        (:INDUCTION STRIP-CARS)
        (:INDUCTION STRIP-CDRS)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-EQUAL)
        (:TYPE-PRESCRIPTION SPLIT2)
        (:TYPE-PRESCRIPTION STRIP-CDRS))
Warnings:  Non-rec
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 SPLIT1-SPLIT2
ACL2 !>
(Reply) (Parent) (Thread)