[Haskell-cafe] Proof in Haskell
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.
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>
More information about the Haskell-Cafe
mailing list