[Haskell-cafe] Proof in Haskell

[Daniel Peebles]

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 <ryani.spam at gmail.com> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20101223/5334ae11/attachment.htm>