[Haskell-cafe] Proof in Haskell

[Paul Johnson]

One alternative approach is to use QuickCheck to test many trees and 
look for counter-examples.  You can also use SmallCheck to do an 
exhaustive check up to a chosen size of tree.

To do this with QuickCheck you would write a function such as

    prop_mirror :: Node a -> Bool
    prop_mirror x = (mirror (mirror x)) == x

You would also need to define an instance of "Arbitrary" for Node to 
create random values of the Node type.  Then you can call:

    quickCheck prop_mirror

and it will call the prop_mirror function with 100 random test cases.  
Not the formal proof you wanted, but still very effective at finding bugs.



On 25/09/09 12:14, pat browne wrote:
> Hi,
> Below is a function that returns a mirror of a tree, originally from:
>
> http://www.nijoruj.org/~as/2009/04/20/A-little-fun.html
>
> where it was used to demonstrate the use of Haskabelle(1) which converts
> Haskell programs to the Isabelle theorem prover. Isabelle was used to
> show that the Haskell implementation of mirror is a model for the axiom:
>
>   mirror (mirror x) = x
>
> My question is this:
> Is there any way to achieve such a proof in Haskell itself?
> GHC appears to reject equations such has
> mirror (mirror x) = x
> mirror (mirror(Node x y z)) = Node x y z
>
>
> Regards,
> Pat
>
>
> =================CODE=====================
> module BTree where
>
> data Tree a = Tip
>              | Node (Tree a) a (Tree a)
>
> mirror ::  Tree a ->  Tree a
> mirror (Node x y z) = Node (mirror z) y (mirror x)
> mirror Tip = Tip
>
> (1)Thanks to John Ramsdell for the link to Haskabelle:
> http://www.cl.cam.ac.uk/research/hvg/Isabelle/haskabelle.html).
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>