<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Jan 17, 2016 at 10:17 AM, 鲍凯文 <span dir="ltr"><<a href="mailto:traqueofziche@gmail.com" target="_blank">traqueofziche@gmail.com</a>></span> wrote:<br><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>How would you prove it for the second case? Is some sort of inductive proof necessary? I found this: <a href="http://ssomayyajula.github.io/posts/2015-11-07-proofs-of-functor-laws-with-Haskell.html" target="_blank">http://ssomayyajula.github.io/posts/2015-11-07-proofs-of-functor-laws-with-Haskell.html</a>, which goes over an inductive (on the length of the list) proof for the list type, but I'm not sure how to do it for a Tree.</div></blockquote></div><br></div><div class="gmail_extra">You've got the right idea. The general outline of a simple inductive proof is this:<br><br></div><div class="gmail_extra">1. Prove for the smallest case (in this case, a tree with just one Leaf)<br><br></div><div class="gmail_extra">2. While assuming that the hypothesis holds for a small case, prove hypothesis for the next case one up in size<br></div><div class="gmail_extra"><br>3. Put 1 and 2 together to claim hypothesis for all cases<br><br></div><div class="gmail_extra">You've done 1.<br><br></div><div class="gmail_extra">You're stuck at 2 because you haven't yet found some measure of a "size" of a Tree.<br><br></div><div class="gmail_extra">What are some common Tree measures you've seen?<br><br></div><div class="gmail_extra"><div><div class="gmail_signature">-- Kim-Ee</div></div>
</div></div>