Re: [Haskell-cafe] Proof in Haskell

23 Dec 2010

      Fair enough :) that'll teach me to hypothesize something without thinking
about it! I guess I could amend my coinductive proof:

http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517

does that cover bottom-ness adequately? I can't say I've thought through it
terribly carefully.

On Thu, Dec 23, 2010 at 12:30 PM, Ryan Ingram  wrote:
...
On Thu, Dec 23, 2010 at 8:19 AM, Daniel Peebles 
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