# Structural induction

https://en.wikipedia.org/wiki/Structural\_induction

Structural induction, a `proof method` used in mathematical logic, is a generalization of mathematical induction over natural numbers and can be further generalized to arbitrary _Noetherian induction_.

_Structural recursion_ is a recursion method bearing the same relationship to _structural induction_ as ordinary _recursion_ bears to ordinary _mathematical induction_.

Structural induction is used to prove that some proposition `P(x)` holds for all `x` of some sort of recursively defined structure (formulas, lists, trees).

_A well-founded partial order_ is defined on the structures ("subformula" for formulas, "sublist" for lists, and "subtree" for trees).

The structural induction proof is a proof that the proposition holds

* for all the minimal structures and that
* if it holds for the immediate substructures of a certain structure S, then it must hold for S also.

Formally speaking, this then satisfies the premises of an _axiom of well-founded induction_, which asserts that these two conditions are sufficient for the proposition to hold for all x.

A _structurally recursive function_ uses the same idea to define a recursive function:

* _base case_ handle each minimal structure and
* _recursive case_ is a rule for recursion

Structural recursion is usually proved correct by structural induction; in particularly easy cases, the inductive step is often left out.

The `length` and (`++`) functions in the example below are structurally recursive.

For example, if the structures are lists, one usually introduces the partial order `<`, in which `L < M` whenever list `L` is the tail of list `M`.

```hs
ls@(x:xs) -> xs < ls
```

Under this ordering, the empty list `Nil` is the unique minimal element.

A structural induction proof of proposition `P(L)` consists of 2 parts:

1. proof that `P(Nil)` is true and
2. proof that if `P(L)` is true for some list `L`, and if `L` is the tail of list `M`, (`M = _:L`) then `P(M)` must also be true.

A structural induction proof of proposition `P(xs)` consists of 2 parts:

1. proof that `P([])` is true and
2. proof that if `P(xs)` is true for some list `xs`, and if `xs` is the tail of list `(x:xs)`, then `P(x:xs)` must also be true.

Eventually, there may exist more than one base or inductive case, depending on how the function or structure was constructed. In those cases, a structural induction proof of some proposition `P(l)` consists of:

* a proof that `P(BC)` is true for each base case `BC`
* a proof that if `P(I)` is true for some instance `I`, and `M` can be obtained from `I` by applying any one recursive rule once, then `P(M)` must also be true.
