The HOL theorem-prover includes tactics on induction, a standard technique for proofs involving a recursive data structure.
For example, the whole numbers can be constructed recursively as follows: starting from 0, successive numbers can be obtained by adding 1 to the predecessor: n to n+1. So if a property P can be shown such that:
- P is valid for 0, and
- If P is valid for n, it is also valid for n+1.
Then we can claim that the property P is valid for all whole number n.
Similarly, the list data structure can be constructed recursively as: starting from the empty list , elements are inserted into the list (h::t), with head h and tail t. If tail t = , the list has one element [h]. If tail = [k], the list has two elements [h; k], and so on.
Corresponding to the induction for proofs involving whole number properties, there is Structural Induction for proofs involving lists:
- Property P is valid for , and
- If P is valid for list t, it is also valid for list (h::t).
The we can claim that the property P is valid for all lists.
Usually the base case (1) is trivial, easily proved by some fundamental results from definition.
The trick to prove the step case (2) is to match the pattern of the induction hypothesis: P is valid for t, to the pattern in the goal: P is valid for (h::t).
Sometimes the definition provides decomposition of the pattern (h::t) to t, then the step case is easy to match.
Otherwise, the best strategy is:
- figure out what’s the stumbling block,
- formulate a lemma that can solve the stumbling block,
- prove the lemma.
It is the solving of stumbling blocks that make theorem-proving endeavours interesting.