[Haskell-cafe] Haskell.org GSoC

[Wouter Swierstra]

> Unfortunately the "proofs" in dependently typed languages are  
> extremely long and tedious to write. Some kind of compiler proofing  
> tool could ease the pain, but I do not think it has low enough  
> complexity for a GSoC project.

I wouldn't say that.

Here's the complete proof script in Coq proving the theorem that was  
originally proposed: length (map f (xs ++ ys)) = length xs + length ys.

It weighs in at about 30 lines, although I could probably get it down  
to less than 10.

The proofs maybe look a bit unfamiliar if you haven't seen Coq before,  
but they are hardly "extremely long and tedious to write". I can  
understand that raw proof *terms* in type theory can be long and  
painful to write. But that's like saying Haskell is bad, because its  
hard to understand ghc-core.

   Wouter

Require Import List.

Variables a b : Set.
Variable f : a -> b.

Lemma lengthMap : forall (xs : list a),
   length (map f xs) = length xs.
   Proof.
     intros.
     induction xs; trivial.
     simpl; rewrite IHxs.
     reflexivity.
   Qed.

Lemma appendLength : forall (xs ys : list a),
   length (xs ++ ys) = length xs + length ys.
   Proof.
     intros.
     induction xs; trivial.
     simpl; rewrite IHxs.
     reflexivity.
   Qed.

Lemma main : forall (xs ys : list a),
   length (map f (xs ++ ys)) = length xs + length ys.
   Proof.
     intros.
     rewrite lengthMap.
     rewrite appendLength.
     reflexivity.
   Qed.