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.
HOL output has a lot of math symbols, which are encoded in Unicode. Displaying these math symbols in DOS when running HOL in Windows is not satisfying. To solve this problem, I developed a simple Java server that talks to HOL in the background, and I can use the web-browser to talk to the server. With such a system I can easily get the math symbols in the browser, and also enhance the display of HOL input/output with colors.
The code for my little work is in https://bitbucket.org/jhlchan/shell.
This is also my first experience with Bitbucket, a free source code hosting based on Mercurial, a distributed version control system. There is a nice short tutorial by Joel Spolsky, which explains clearly and simply how to use Mercurial.
The HOL System Tutorial is a fairly gentle introduction to using the system HOL. It provides screenshots from the interactive sessions, so you can follow what’s happening even if you don’t have the system installed. Better still, download and install HOL, then follow the tutorial to verify the sessions and get a hands-on experience with the system.
The first substantial example is a proof of this theorem: that there are infinitely many primes. The classic proof by Euclid is considered as a proof from “The Book” — in which God keeps the most elegant proof of each mathematical theorem, according to the mathematician Paul Erdös. During a lecture in 1985, Erdös said, “You don’t have to believe in God, but you should believe in The Book.”
However, to rephrase this proof in HOL, many basic concepts needs to be established first: what is a prime? how to define divisibility? All these boil down to logical statements about natural numbers.
The actual proof process in HOL is assisted by the Proof Manager. There are actions to put a goal to the manager, expand the goal by tactics, which are strategies to pick either known facts or lemma from a HOL theory. The expansion of a goal usually gives subgoals, which can be further expanded until everything is known, upon which the initial goal is proved. Of course, picking the correct strategies take some understanding and experience. The Proof Manager allows you to advance a step, backup a step, or redo from the start. All these techniques are demonstrated in this example of the Tutorial.
In the end, Euclid’s proof of the infinity of primes is done in about 10 lines of HOL code, after much polishing. This is finale of a whole chapter with more than 30 pages!