Editing Structural induction (section)

==Examples==

[[File:Waldburg Ahnentafel.jpg|thumb|Ancient ancestor tree, showing 31 persons in 5 generations]]
An [[family tree|ancestor tree]] is a commonly known data structure, showing the parents, grandparents, etc. of a person as far as known (see picture for an example). It is recursively defined:
* in the simplest case, an ancestor tree shows just one person (if nothing is known about their parents);
* alternatively, an ancestor tree shows one person and, connected by branches, the two ancestor subtrees of their parents (using for brevity of proof the simplifying assumption that if one of them is known, both are).

As an example, the property "An ancestor tree extending over {{mvar|g}} generations shows at most {{math|2<sup>''g''</sup> − 1}} persons" can be proven by structural induction as follows:
* In the simplest case, the tree shows just one person and hence one generation; the property is true for such a tree, since {{math|1 ≤ 2<sup>1</sup> − 1}}.
* Alternatively, the tree shows one person and their parents' trees. Since each of the latter is a substructure of the whole tree, it can be assumed to satisfy the property to be proven (a.k.a. the ''induction hypothesis''). That is, {{math|''p'' ≤ 2<sup>''g''</sup> − 1}} and {{math|''q'' ≤ 2<sup>''h''</sup> − 1}} can be assumed, where {{mvar|g}} and {{mvar|h}} denotes the number of generations the father's and the mother's subtree extends over, respectively, and {{mvar|p}} and {{mvar|q}} denote the numbers of persons they show.
** In case {{math|''g'' ≤ ''h''}}, the whole tree extends over {{math|1 + ''h''}} generations and shows {{math|1=''p'' + ''q'' + 1}} persons, and<math display=block>p+q+1 \leq (2^g-1) + (2^h-1) + 1 \leq 2^h+2^h-1 = 2^{1+h}-1,</math>i.e. the whole tree satisfies the property.
** In case {{math|1=''h'' ≤ ''g''}}, the whole tree extends over {{math|1=1 + ''g''}} generations and shows {{math|''p'' + ''q'' + 1 ≤ 2{{sup|''g'' + 1}} − 1}} persons by similar reasoning, i.e. the whole tree satisfies the property in this case also.
Hence, by structural induction, each ancestor tree satisfies the property.

As another, more formal example, consider the following property of lists :

:<math>\text{EQ:} \quad \operatorname{len}(L +\!+\ M) = \operatorname{len}(L) + \operatorname{len}(M)</math>

Here {{math|++}} denotes the list concatenation operation, {{math|len()}} the list length, and {{mvar|L}} and {{mvar|M}} are lists.

In order to prove this, we need definitions for length and for the concatenation operation. Let {{math|(''h'':''t'')}} denote a list whose head (first element) is {{mvar|h}} and whose tail (list of remaining elements) is {{mvar|t}}, and let {{math|[]}} denote the empty list. The definitions for length and the concatenation operation are:

:<math>\begin{array}{ll}
\text{LEN1:} & \operatorname{len}([\ ]) = 0 \\
\text{LEN2:} & \operatorname{len}(h:t) = 1 + \operatorname{len}(t) \\
& \\
\text{APP1:} &  [\ ] +\!+\ list = list \\
\text{APP2:} & (h:t) +\!+\ list = h : (t +\!+\ list)
\end{array}</math>

Our proposition {{math|''P''(''l'')}} is that {{math|EQ}} is true for all lists {{mvar|M}} when {{mvar|L}} is {{mvar|l}}.  We want to show that {{math|1=''P''(''l'')}} is true for all lists {{mvar|l}}. We will prove this by structural induction on lists.

First we will prove that {{math|''P''([])}} is true; that is, {{math|EQ}} is true for all lists {{mvar|M}} when {{mvar|L}} happens to be the empty list {{math|[]}}. Consider {{math|EQ}}:

:<math>\begin{array}{rll}
\operatorname{len}(L +\!+\ M) 
&= \operatorname{len}([\ ] +\!+\ M)                 \\
&= \operatorname{len}(M)                            & (\text{by APP1})\\
&= 0 + \operatorname{len}(M)                        \\
&= \operatorname{len}([\ ]) + \operatorname{len}(M) & (\text{by LEN1})\\
&= \operatorname{len}(L) + \operatorname{len}(M)    \\
\end{array}</math>

So this part of the theorem is proved; {{math|EQ}} is true for all {{mvar|M}}, when {{mvar|L}} is {{math|[]}}, because the left-hand side and the right-hand side  are equal.

Next, consider any nonempty list {{mvar|I}}. Since {{mvar|I}} is nonempty, it has a head item, {{mvar|x}}, and a tail list, {{mvar|xs}}, so we can express it as {{math|(''x'':''xs'')}}.  The induction hypothesis is that {{math|EQ}} is true for all values of {{mvar|M}} when {{mvar|L}} is {{mvar|xs}}:

:<math>\text{HYP:} \quad \operatorname{len}(xs +\!+\ M) = \operatorname{len}(xs) + \operatorname{len}(M)</math>

We would like to show that if this is the case, then {{math|EQ}} is also true for all values of {{mvar|M}} when {{math|1=''L'' = ''I'' = (''x'':''xs'')}}. We proceed as before:

:<math>\begin{array}{rll}
\operatorname{len}(L) + \operatorname{len}(M) 
&= \operatorname{len}(x:xs) + \operatorname{len}(M)       \\
&= 1 + \operatorname{len}(xs) + \operatorname{len}(M)     & (\text{by LEN2}) \\
&= 1 + \operatorname{len}(xs +\!+\ M)                     & (\text{by HYP}) \\
&= \operatorname{len}(x: (xs +\!+\ M))                    & (\text{by LEN2}) \\
&= \operatorname{len}((x:xs) +\!+\ M)                     & (\text{by APP2}) \\
&= \operatorname{len}(L +\!+\ M)
\end{array}</math>

Thus, from structural induction, we obtain that {{math|''P''(''L'')}} is true for all lists {{mvar|L}}.