title: inductive step of proof by structural induction
body: <p>I am given the following 2 versions of a tree-flattening program and i am asked to prove identical behaviour.</p>
  
  <pre><code>flatten::Tree-&gt;[Int]
  flatten (Leaf z)        =[z]                             F.1
  flatten (Node x y)      =concat (flatten x)(flatten y)   F.2
  
  flatten'::Tree-&gt;Int-&gt;[Int]
  flatten' (Leaf z) a     =concat [z] a                    P.1
  flatten' (Node x y) a   =flatten' x (flatten' y a)       P.2
  
  concat-&gt;[a]-&gt;a-&gt;[a]
  concat [] a             =a                               C.1
  concat (h:t) a          =h:concat t a                    C.2
  </code></pre>
  
  <p>Prove that:</p>
  
  <pre><code>flatten' z a = concat (flatten z) a
  </code></pre>
  
  <p>Base Case:</p>
  
  <pre><code>LHS:
      flatten' (Leaf z) a = concat [z] a                   By P.1
  RHS:
      concat (flatten z) a = concat (flatten (Leaf z)) a
                           = concat [z] a                  By F.1 and C.1
  
  LHS=RHS, hence base case holds
  </code></pre>
  
  <p>Inductive Case: </p>
  
  <blockquote>
    <p>(Only possible thanks to the guy below who explained how induction on
    binary trees works!)</p>
  </blockquote>
  
  <pre><code>Assume that:
     flatten' x a = concat (flatten x) a                   Ind. Hyp1
     flatten' y a = concat (flatten y) a                   Ind. Hyp2
  
  Show that:
     flatten'(Node x y) a = concat (flatten (Node x y)) a
  
  LHS:
     flatten' (Node x y) a = 
     flatten' x (flatten' y a)                             By P.2
     flatten' x (concat (flatten y) a)                     By Ind. Hyp2
     concat (flatten x) (concat (flatten y) a)             By Ind. Hyp1
  
  RHS:
     concat (flatten (Node x y)) a =
     concat (concat (flatten x) (flatten y)) a             By F.2
     concat (flatten x) (concat (flatten y) a)             By C.2
  
     LHS = RHS, hence inductive step holds. End of proof.
  </code></pre>