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.
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
