Induction on Trees
Lists and binary trees are similar when viewed as data types. Here are the definitions of both, side-by-side for comparison:
type 'a bintree = type 'a list =
| Leaf | []
| Node of 'a bintree * 'a * 'a bintree | ( :: ) of 'a * 'a list
Both have a constructor that represents "empty", and both have a constructor
that combines a value of type 'a
together with another instance of the
data type. The only real difference is that ( :: )
takes just one list,
whereas Node
takes two trees.
The induction principle for binary trees is therefore very similar to the induction principle for lists, except that with binary trees we get two inductive hypotheses, one for each subtree:
forall properties P,
if P(Leaf),
and if forall l v r, (P(l) and P(r)) implies P(Node (l, v, r)),
then forall t, P(t)
An inductive proof for binary trees therefore has the following structure:
Proof: by induction on t.
P(t) = ...
Base case: t = Leaf
Show: P(Leaf)
Inductive case: t = Node (l, v, r)
IH1: P(l)
IH2: P(r)
Show: P(Node (l, v, r))
Let's try an example of this kind of proof. Here is a function that creates the mirror image of a tree, swapping its left and right subtrees at all levels:
let rec reflect = function
| Leaf -> Leaf
| Node (l, v, r) -> Node (reflect r, v, reflect l)
For example, these two trees are reflections of each other:
1 1
/ \ / \
2 3 3 2
/ \ / \ / \ / \
4 5 6 7 7 6 5 4
If you take the mirror image of a mirror image, you should get the original
back. That means reflection is an involution, which is any function f
such that f (f x) = x
. Another example of an involution is multiplication
by negative one on the integers.
Let's prove that reflect
is an involution.
Claim: forall t, reflect (reflect t) = t
Proof: by induction on t.
P(t) = reflect (reflect t) = t
Base case: t = Leaf
Show: reflect (reflect Leaf) = Leaf
reflect (reflect Leaf)
= { evaluation }
reflect Leaf
= { evaluation }
Leaf
Inductive case: t = Node (l, v, r)
IH1: reflect (reflect l) = l
IH2: reflect (reflect r) = r
Show: reflect (reflect (Node (l, v, r))) = Node (l, v, r)
reflect (reflect (Node (l, v, r)))
= { evaluation }
reflect (Node (reflect r, v, reflect l))
= { evaluation }
Node (reflect (reflect l), v, reflect (reflect r))
= { IH1 }
Node (l, v, reflect (reflect r))
= { IH2 }
Node (l, v, r)
QED
Induction on trees is really no more difficult than induction on lists or natural numbers. Just keep track of the inductive hypotheses, using our stylized proof notation, and it isn't hard at all.