Paul Johnson paul at cogito.org.uk
Fri Sep 25 12:42:53 EDT 2009

```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
>