On Tue, Dec 21, 2010 at 3:57 PM, austin seipp <as@hacks.yi.org> wrote:
> However, at one point I wrote about proving exactly such a thing (your
> exact code, coincidentally) in Haskell, only using an 'extraction
> tool' that extracts Isabelle theories from Haskell source code,
> allowing you to prove such properties with an automated theorem
> prover.

You may also write your program, for example, using Coq and then extract correct Haskell code from it. I'm far from a Coq expert so there must be a better way, but the following works =):

Inductive Tree (A : Type) :=
  | Tip : Tree A
  | Node : Tree A -> A -> Tree A -> Tree A.

Fixpoint mirror {A : Type} (x : Tree A) : Tree A :=
  match x with
  | Tip => Tip A
  | Node l v r => Node A (mirror r) v (mirror l)
  end.

Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.
  induction x; simpl; auto.
  rewrite IHx1; rewrite IHx2; trivial.
Qed.

Extraction Language Haskell.
Recursive Extraction mirror.

Then Coq generates the following correct-proven code:

data Tree a = Tip

| Node (Tree a) a (Tree a)

mirror :: (Tree a1) -> Tree a1

mirror x =

case x of

Tip -> Tip

Node l v r -> Node (mirror r) v (mirror l)

Cheers! =)

--
Felipe.