Fair enough :) that'll teach me to hypothesize something without thinking about it! I guess I could amend my coinductive proof:<div><br></div><div><a href="http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517">http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517</a></div>
<div><br></div><div>does that cover bottom-ness adequately? I can't say I've thought through it terribly carefully.<br><br><div class="gmail_quote">On Thu, Dec 23, 2010 at 12:30 PM, Ryan Ingram <span dir="ltr"><<a href="mailto:ryani.spam@gmail.com">ryani.spam@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="im">On Thu, Dec 23, 2010 at 8:19 AM, Daniel Peebles <<a href="mailto:pumpkingod@gmail.com">pumpkingod@gmail.com</a>> wrote:<br>
> Simulating bottoms wouldn't be too hard, but I don't think the statement is<br>
> even true in the presence of bottoms, is it?<br>
<br>
</div>Isn't it?<br>
<div class="im"><br>
data Tree a = Tip | Node (Tree a) a (Tree a)<br>
<br>
mirror :: Tree a -> Tree a<br>
</div>mirror Tip = Tip<br>
<div class="im">mirror (Node x y z) = Node (mirror z) y (mirror x)<br>
<br>
</div>--<br>
<br>
-- base cases<br>
mirror (mirror _|_)<br>
= mirror _|_<br>
= _|_<br>
<br>
mirror (mirror Tip)<br>
= mirror Tip<br>
= Tip<br>
<br>
-- inductive case<br>
mirror (mirror (Node x y z))<br>
= mirror (Node (mirror z) y (mirror x))<br>
= Node (mirror (mirror x)) y (mirror (mirror z))<br>
-- induction<br>
= Node x y z<br>
<font color="#888888"><br>
-- ryan<br>
</font></blockquote></div><br></div>