Felipe Almeida Lessa felipe.lessa at gmail.com
Tue Dec 21 19:34:11 CET 2010

```On Tue, Dec 21, 2010 at 3:57 PM, austin seipp <as at 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.

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.
-------------- next part --------------
An HTML attachment was scrubbed...