[Haskell-cafe] Haskell.org GSoC
Wouter Swierstra
wss at cs.nott.ac.uk
Thu Feb 19 09:36:27 EST 2009
> 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.
More information about the Haskell-Cafe
mailing list