When doing a math proof, it’s like walking along the math landscape: your proof is a path (a logical path) from the hypotheses (starting point) to the conclusion (finishing point).
The HOL theorem-prover provides an interactive proof manager. When it shows “all goals proved”, it is indeed a revelation: suddenly the logical path is complete.
Because the logical path is taken by the machine, you’re sure that there are no logical gaps — no missing steps. This is the advantage of using the theorem-prover: it won’t allow logical gaps.
However, you can be driven into logical blind alleys — the theorm-prover won’t tell you. This is because along the proof path, there are many decision points: which symbol to induct on? should cases of a symbol be taken?
Ideally all paths will lead to the same goal, but some paths are easier to walk, while other paths go through mountains or deserts. Some even lead to a door — you just can’t open it without a key. The key may be nearby, or far away; but you need to find the key to open the door if you want to continue on with that particular path. That’s the key idea to overcome the stumbling block.
All in all, a theorem prover is a good guide for the proof path, as you can see the effect of tactics, and where you’re going. Most goals will branch off into subgoals, and it’s tedious to keep track of subgoals by hand — better let the machine do the book-keeping.
To spell out all the logical details of a proof, as required by a theorem-prover, can be routine — not very illuminating, even boring. The HOL theorem-prover provides various rewrite tactics and simplification sets to ease the task, but picking out the appropriate tools to do the job still needs experience.
However, sometimes you’ll hit a stumbling block: something that looks simple and must be true, but you just can’t see any simple proof of it. That’s when the proof becomes interesting.
This is not related to a particular theorem prover. Ask any mathematician and he or she will tell you stories.
The solution of the “stumbling block” usually involves a key idea.
For example, given a number N, how to show that there is a prime greater than N? There is no known formula to generate primes. It was Euclid, around 300 BC, who recorded this key idea: use N to generate a number M such that M cannot be divided by any primes up to N. By case-analysis of this M, the infinitude of primes can be proved.
Of course, during case-analysis of M, you’ll need to show that any number must be a product of primes. If this is a stumbling block, you’ll need another key idea. And so on.
How to find the key idea? Using examples or pictures can help visualizing the stumbling block. After some deep thoughts, the key idea will dawn upon. Sometimes you need to look outside the box. And you’ll need pencil-and-paper to try out the key idea, as the theorem prover will not allow unproven stuff.
To find the key idea in a proof is almost an art — there is no algorithm for it.
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.
Recently I’ve been doing actual theorem proving using HOL. This is a real eye-opener. Here is a summary of my first experience:
- Simple theorems can be proved just by using definitions.
- It’s not good to prove everything from definition — this makes the proof tedious.
- Some fundamental results should first be established by definition — they become theorems for proving more complex results.
This corresponds to the working mode of mathematicians. To build a theory one starts from definitions, properties, lemma, then theorems. There are many proof techniques, called tactics in HOL, and choosing the most efficient one needs a lot of experience.
Meanwhile, HOL upon loading includes some basic theories, and there is mechanism to load in more specific theories if required. Users of HOL can write up the proofs in scripts, and the Holmake utility can compile the script and generate the theory file and binary files, ready for loading so that the theorems will be available in other HOL sessions.
HOL is a very useful too, and I’m learning the basics of the tool. The HOL documentations are a big help here. I alway learn a lot by following the theory scripts provided in the source and examples.