7.2.1
The induction scheme is based on how the datatype is defined.
For Tree elem that definition looks like:

data Tree elem = Empty | Node (Tree elem) elem (Tree elem)

From this you can see that the base case would be for Empty and the inductive step for
"Node (Tree elem) elem (Tree elem)" since there is recursion.


7.2.2

> data Tree elem = Empty | Node (Tree elem) elem (Tree elem)
>   deriving (Show)

> inner :: Tree elem -> Integer
> inner Empty        = 0
> inner (Node l a r) = 1 + inner l + inner r

> outer :: Tree elem -> Integer
> outer Empty        = 1
> outer (Node l a r) = 0 + outer l + outer r

Now we proof by Induction that:
"inner t + 1 = outer t" for all tree t

First we have the base case where "case t = Empty":

  inner Empty + 1
= {def of inner}
  0 + 1
=
  1
= {def of outer}
  outer empty

Then the induction step where "case t = (Node l a r)":

  inner (Node l a r) + 1
= {def of inner}
  (1 + inner l + inner r) + 1
= {IH}
  outer l + inner r + 1
= {IH}
  outer l + outer r
=
  outer l + outer r
= {def of outer}
  outer (Node l a r)

7.2.3

Now we proof by Induction that:
"2^(minHeight t)-1 <= size t <= 2^(maxHeight t)-1"

First we have the base case where "case t = Empty":

  2^(minHeight Empty) - 1
= {def of minHeight}
  2^0-1
= {def of mathematics}
  0
=
  0
= {def of size}
  size Empty

  2^(maxHeight Empty) - 1
= {def of maxHeight}
  2^0-1
= {def of mathematics}
  0
=
  0
= {def of size}
  size Empty

Then the induction step where "case t = (Node l a r)":
(Include the expliced definitions in these exercises next time please)

  2^(minHeight (Node l a r)) - 1
= {def of minHeight}
  2^(1 + (minHeight l `min` minHeight r)) - 1
= {def of `min`}
  2^(1 + (minHeight l || minHeight r)) - 1
<=
  1 + 2^(minHeight l) - 1 +  2^(minHeight r) - 1
= {IH}
  1 + size l + size r
= {def of size}
  size (Node l a r)

  2^(maxHeight (Node l a r)) - 1
= {def of maxHeight}
  2^(1 + (maxHeight l `max` maxHeight r)) - 1
= {def of `max`}
  2^(1 + (maxHeight l || maxHeight r)) - 1
greater or equal to
  1 + 2^(maxHeight l) - 1 +  2^(maxHeight r) - 1
= {IH}
  1 + size l + size r
= {def of size}
  size (Node l a r)

7.3.1

inorderCat t xs = inorder t ++ xs

First we have the base case where "t = Empty":

  inorderCat Empty xs
= {specification of inorderCat}
  inorder Empty ++ xs
= {def of inorder}
  [] ++ xs
= {monoid}
  xs

Then the case where "t = (Node l a r)":

  inorderCat (Node l a r) xs
= {specification of inorderCat}
  inorder (Node l a r) ++ xs
= {def of inorder}
  (inorder l ++ [a] ++ inorder r) ++ xs
= {monoid}
  inorder l ++ ([a] ++ (inorder r ++ xs))
= {definition of ++}
  inorder l ++ (a:(inorder r ++ xs))
= {specification of inorderCat}
  inorder l ++ (a:(inorderCat r xs))
= {specification of inorderCat}
  inorderCat l (a:(inorderCat r xs))

> inorder :: Tree elem -> [elem]
> inorder Empty = []
> inorder (Node l a r) = inorder l ++ [a] ++ inorder r

> inorderCat :: Tree elem -> [elem] -> [elem]
> inorderCat Empty xs = xs
> inorderCat (Node l a r) xs = inorderCat l (a:(inorderCat r xs))

7.3.2

> skewed :: Integer -> Tree Integer
> skewed 0 = Empty
> skewed x = Node (skewed (x-1)) x (Empty)

Yes it is way faster:
inorder (skewed 10000) ++ [1,2,3,4,5] takes 2.45 seconds
inorderCat (skewed 10000) [1,2,3,4,5] takes 1.04 seconds

7.3.3
preorder:
preorderCat t xs = preorder t ++ xs

First we have the base case where "t = Empty":
  preorderCat Empty xs
= {specification of preorderCat}
  preorder Empty ++ xs
= {def of preorder}
  [] ++ xs
= {monoid}
  xs

Then the case where "t = (Node l a r)":
  preorderCat (Node l a r) xs
= {specification of preorderCat}
  preorder (Node l a r) ++ xs
= {def of preorder}
  ([a] ++ preorder l ++ preorder r) ++ xs
= {monoid}
  [a] ++ (preorder l ++ (preorder r ++ xs))
= {definition of ++}
  a:(preorder l ++ (preorder r ++ xs))
= {specification of preorderCat}
  a:(preorder l ++ (preorderCat r xs))
= {specification of inorderCat}
  a:(preorderCat l (preorderCat r xs))

> preorder :: Tree elem -> [elem]
> preorder Empty = []
> preorder (Node l a r) = [a] ++ preorder l ++ preorder r

> preorderCat :: Tree elem -> [elem] -> [elem]
> preorderCat Empty xs = xs
> preorderCat (Node l a r) xs = a:(preorderCat l (preorderCat r xs))

Yes it is way faster:
preorder (skewed 10000) ++ [1,2,3,4,5] takes 2.45 seconds
preorderCat (skewed 10000) [1,2,3,4,5] takes 1.07 seconds

postorder:
postorderCat t xs = postorder t ++ xs

First we have the base case where "t = Empty":
  postorderCat Empty xs
= {specification of postorderCat}
  postorder Empty ++ xs
= {def of postorder}
  [] ++ xs
= {monoid}
  xs

Then the case where "t = (Node l a r)":
  postorderCat (Node l a r) xs
= {specification of postorderCat}
  postorder (Node l a r) ++ xs
= {def of postorder}
  (postorder l ++ postorder r ++ [a]) ++ xs
= {monoid}
  postorder l ++ (postorder r ++ ([a] ++ xs))
= {definition of ++}
  postorder l ++ (postorder r ++ (a:xs))
= {specification of postorderCat}
  postorder l ++ (postorderCat r (a:xs))
= {specification of postorderCat}
  postorderCat l (postorderCat r (a:xs))

> postorder :: Tree elem -> [elem]
> postorder Empty = []
> postorder (Node l a r) =  postorder l ++ postorder r ++ [a]

> postorderCat :: Tree elem -> [elem] -> [elem]
> postorderCat Empty xs = xs
> postorderCat (Node l a r) xs = postorderCat l (postorderCat r (a:xs))

Yes it is way faster:
postorder (skewed 10000) ++ [1,2,3,4,5] takes 2.47 seconds
postorderCat (skewed 10000) [1,2,3,4,5] takes 1.12 seconds

7.3.4
The dereviation is already the inductive proof since you implemented the function in a way for the specification to hold.

7.3.5
It uses the same idea of making sure the lists are smartly placed in a way that they are used most efficient.