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