[Haskell-cafe] Proof in Haskell

[Ryan Ingram]

On Thu, Dec 23, 2010 at 8:19 AM, Daniel Peebles <pumpkingod at gmail.com> wrote:
> Simulating bottoms wouldn't be too hard, but I don't think the statement is
> even true in the presence of bottoms, is it?

Isn't it?

data Tree a = Tip | Node (Tree a) a (Tree a)

mirror :: Tree a -> Tree a
mirror Tip = Tip
mirror (Node x y z) = Node (mirror z) y (mirror x)

--

-- base cases
mirror (mirror _|_)
 = mirror _|_
 = _|_

mirror (mirror Tip)
 = mirror Tip
 = Tip

-- inductive case
mirror (mirror (Node x y z))
  = mirror (Node (mirror z) y (mirror x))
  = Node (mirror (mirror x)) y (mirror (mirror z))
  -- induction
  = Node x y z

  -- ryan