# Structural induction on binary trees

I have some problems understanding structural induction, maybe because it is such a rigorous way of thinking, so I don't really know where to start here..

This is taken from our Algorithms course and I was wondering if anyone could help me understand how to solve this and how to generally think this way..

Let us define the data structure binary tree (BinTree) using these constructors and operands:

Constructors:

empty : -> BinTree (new void tree)

node : BinTree * Elem * BinTree -> BinTree (left subtree, root, right subtree)

Operands:

height : BinTree -> ℕ // number of levels of the tree ($0$ for void, $1$ for root only, etc.)

member : Elem * BinTree -> Bool (predicate indicating if an element is in the tree or not)

distance : Elem * BinTree -> ℕ (minimum number of edges from the root until the apparition of the element ; $0$ for root, $\infty$ if not in the tree)

How can one prove with structural induction that $$member(x,t) => distance(x,t) < height(t)$$

We proceed by structural induction on $t$. If $t$ is empty, then the implication is vacuously true, since an empty tree contains no elements.
Otherwise, assume that $t$ is nonempty so that $t = \textsf{node}(\ell, y, r)$ for some $\ell, r \in \textsf{BinTree}$ and $y \in \textsf{Elem}$. Then since $\textsf{member}(x, t)$, we know that $x = y$, $\textsf{member}(x, \ell)$, or $\textsf{member}(x, r)$. If $x = y$, then since $t$ is not empty, we know that: $$\textsf{distance}(x, t) = \textsf{distance}(y, \textsf{node}(\ell, y, r)) = 0 < 1 \leq \textsf{height}(\textsf{node}(\ell, y, r)) = \textsf{height}(t)$$
Now suppose that $x \neq y$ and $\textsf{member}(x, \ell)$. Then observe that: \begin{align*} \textsf{distance}(x, t) &= \textsf{distance}(x, \textsf{node}(\ell, y, r)) \\ &= 1 + \min(\textsf{distance}(x, \ell), \textsf{distance}(x, r)) \\ &\leq 1 + \textsf{distance}(x, \ell) \\ &< 1 + \textsf{height}(\ell) & \text{by the induction hypothesis} \\ &\leq 1 + \max(\textsf{height}(\ell), \textsf{height}(r)) \\ &= \textsf{height}(t) \end{align*} as desired. An analogous argument holds if $\textsf{member}(x, r)$. $~\blacksquare$