Structural induction on binary trees

Question

Consider the following function definitions :

data Tree a = Leaf a | Node a (Tree a) (Tree a)

sumLeaves :: Tree a -> Integer
sumLeaves (Leaf x) = 1 
sumLeaves (Node _ lt rt) = sumLeaves lt + sumLeaves rt 

sumNodes :: Tree a -> Integer
sumNodes (Leaf x) = 0 
sumNodes (Node _ lt rt) = 1 + sumNodes lt + sumNodes rt 

Task: Prove by structural induction that for all finite trees t :: Tree a holds:

sumLeaves t = sumNodes t + 1

I now have:

sumLeaves t = sumNodes t + 1

I.A. t = (Tree 0) = (Leaf 0)

sumLeaves (Leaf 0) = 1 sumNodes (Leaf 0) + 1

0 + 1 = 1

1 = 1

I.V.: We assume that the statement holds for an arbitrary t.

I.S.:

Now what is the induction step, I really have problems with solving this last step.

Answer 1

Similar to the induction over natural numbers, where the induction step is assuming that some hypothesis holds for all numbers less than n, and then proving the hypothesis for n, structural induction step assumes that hypothesis holds for all structures that are substructures of a given structure.

In your case, correct assumption would be that the statement holds for trees lt and rt that are subtrees of the arbitrary t@(Node x lt rt), and then proving the statement for t.