[Haskell-cafe] Proof in Haskell

[Felipe Almeida Lessa]

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.

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20101221/d7bb93d2/attachment.htm>