Introduction

We often find ourselves in the situation of wanting to prove something of the form:

That is, we want to prove that all elements of some set S have the property P. If all of the elements of S are defined by some regular structural rules, induction is frequently the proof technique of choice.

Examples of sets that can be defined by structural rules include:

• natural numbers: starting with the element 0, each element is the successor of some other element in the set.
• sequences: starting with the empty sequence, <>, each element is built up by appending an element to an existing list.
• parse trees: starting with the ``terminal'' nodes of a grammar, each parse true is a structure defined by one of a ``non-terminal'' productions of the grammar.

In the first of these examples, the proof technique is typically referred to as ``natural induction''. In the others, it is typically referred to as ``structural induction''.

In these notes we will illustrate the use of structural induction over binary trees. Other forms of structural induction work similarly. Here is how we will proceed. First, we provide a ``structural'' definition of trees: this determines the rules that allow us to define all trees of interest. Next, we define what we mean by ``size'' of a tree. Then we will propose a small theorem about calculating the size; this is what we will then prove.