Comments: 
(Deleted comment)
Because Chris showedandtelled, 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)
appendcong2 : ∀{A} {a : A} {as bs : List A}
→ as ≡ bs
→ (a :: as) ≡ (a :: bs)
appendcong2 Refl = Refl
appendnil : ∀{A} {as : List A} → as ++ [] ≡ as
appendnil {as = []} = Refl
appendnil {as = a :: as} = appendcong2 (appendnil {as = as})
assocappend : ∀{A} {as bs cs : List A}
→ (as ++ (bs ++ cs)) ≡ ((as ++ bs) ++ cs)
assocappend {as = []} = Refl
assocappend {as = a :: as} = appendcong2 (assocappend {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 }
spliteqlem : ∀{A B} (lx : List A) (ly : List B) (lxy : List (A × B))
→ (lx ++ map fst lxy , ly ++ map snd lxy) ≡ split' lxy lx ly
spliteqlem lx ly [] = Product.paircong appendnil appendnil
spliteqlem lx ly ((x , y) :: lxy) =
Product.paircong (assocappend {as = lx}) (assocappend {as = ly})
≡≡ spliteqlem (lx ++ [ x ]) (ly ++ [ y ]) lxy
spliteq : ∀{A B} (lxy : List (A × B)) → split lxy ≡ split' lxy [] []
spliteq lxy = spliteqlem [] [] 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 letbindings 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.
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. conglem : ∀{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)
conglem Refl = refl
spliteqA : ∀{A B} → (lxy : List (A × B)) → split lxy ≡ splitA lxy
spliteqA [] = refl
spliteqA ((x , y) :: lxy) = conglem (spliteqA lxy)
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 (Deleted comment)
Do you actually get to prove that two coq functions are equivalent? How do you take apart the construction of split and split' to reason about them? I didn't think you could deal with meta level functions like that, but I've never really used Coq.
Yeah, you do. How you "take apart" the definitions depends, but it's a matter of showing that given the same arguments they produce the same results. Look at how Neel did it up above. His split' (the one that uses map ) is basically my split , while his split is sort of like my split' but prettier. Mine might be harder to prove stuff about  I'm not really sure yet.
 From: pmb 20101022 06:04 pm (UTC)
 (Link)

The real problem is that zip() is of arity 2, and not arity n. An narity zip() is its own inverse! :) (Deleted comment) (Deleted comment)
Eh, I posted the ACL2 version, and given the lack of higherorder functions, it's even less interesting (especially if you had to define your own mapcar and mapcdr ).
From: markluffel 20101026 06:52 pm (UTC)
Proof language for nonPLresearchers?  (Link)

Hey Lindsey et al!
If I wanted to learn one of these wild proof languages, say for doing geometric/computergraphics proofs, what language would you recommend? I started working through a tutorial for that Omega language, which I understand is rather different from what the folks in this thread are using... but the documentation made it seem to be a better choice for a beginner.
If I'm concerned mostly with ease of use (and libraries for dealing with real numbers, I guess) what should I use?
 From: lindseykuper 20101026 08:04 pm (UTC)
Re: Proof language for nonPLresearchers?  (Link)

Hm. Have you looked at GeoProof? Apparently it talks to Coq. In any case, I'd recommend whichever one has the best library for geometric proofs, since if it doesn't already exist you'll be spending a lot of time building up scaffolding before you can even get started. To my knowledge, Omega's less a proof assistant than it is a generalpurpose language with dependent types. Having said that, the line between the two is blurry, and I think a lot of people like Agda precisely because it straddles that line pretty well.  