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.s...@gmail.com> wrote: > On Thu, Dec 23, 2010 at 8:19 AM, Daniel Peebles <pumpkin...@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 >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
