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.

```