Comments: |
**(Deleted comment)**
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
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.
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.
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.
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.)
*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.
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)
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?
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?
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)))
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
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)*
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)*
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.? **(Deleted comment)**
| |