| To continue the discussion on the examples for QED I would like to suggest
| the Stone's theorem that every metrizable space is paracompact, 1948.
|
| [...]
|
| I would like to see a proof of this theorem in some other system.
Well, I am not really qualified to judge its suitability. But I proved this
theorem in HOL. It wasn't especially *difficult*, but was quite messy and
intricate; I think I spent almost 10 hours on it. Actually I didn't have to use
"little theories", since the HOL libraries already contain the essential
ingredients:
* A theory of real numbers
* A proof of the wellordering principle and transfinite recursion
* A theory of finite sets.
* A theory of topology and metric spaces.
The last of these is a rather limited and ad-hoc theory which I developed as
part of the reals library; on reflection it was probably pointless to do so.
However it was sufficient for the present task, with a bit of tweaking to use
a proper set theory library instead of its own ad-hoc set notation (when I
wrote the reals library I wanted it to be independent of other libraries).
I spent a while looking at textbooks, and eventually translated the proof from
the book "General Topology" by Ryszard Engelking (Sigma series in pure
mathematics, vol. 6, Heldermann Verlag 1989). The HOL proof is pretty close to
the one there, except that the textbook proof occupies 1 page, and the HOL
proof 700 lines (but this includes additional lemmas, some quite trivial things
about arithmetic and set theory).
I can post the whole proof if there is demand (HOL proofs generally don't mean
much even to the initiated, unless you step through them in a HOL session). But
here are the severely edited highlights.
Definitions:
let COVER = new_definition(`COVER`,
"COVER C = (UNIONS C = UNIV:*->bool)");;
let OPEN_COVER = new_definition(`OPEN_COVER`,
"OPEN_COVER(top :* topology) C =
COVER C /\ (!s. s IN C ==> open(top) s)");;
let REFINES = new_infix_definition(`REFINES`,
"$REFINES C' C = !s':*->bool. s' IN C' ==> ?s. s IN C /\ s' SUBSET s");;
let LOCALLY_FINITE = new_definition(`LOCALLY_FINITE`,
"LOCALLY_FINITE(top: * topology) C =
!x. ?N. neigh(top) (N,x) /\
FINITE { s | s IN C /\ ~(s INTER N = EMPTY) }");;
let PARACOMPACT = new_definition(`PARACOMPACT`,
"PARACOMPACT(top:* topology) =
!C. OPEN_COVER(top) C ==>
?C'. OPEN_COVER(top) C' /\
C' REFINES C /\
LOCALLY_FINITE(top) C'");;
Main proof:
let STONE = prove_thm(`STONE`,
"!m:(*)metric. PARACOMPACT(mtop m)",
REWRITE_TAC[PARACOMPACT; OPEN_COVER] THEN REPEAT STRIP_TAC THEN
IMP_RES_THEN(X_CHOOSE_THEN "$<<:(*->bool)->(*->bool)->bool"
STRIP_ASSUME_TAC) STONE_WO THEN
FIRST_ASSUM(X_CHOOSE_THEN "min:*->(*->bool)" MP_TAC o
CONV_RULE SKOLEM_CONV) THEN
CONV_TAC(TOP_DEPTH_CONV FORALL_AND_CONV) THEN STRIP_TAC THEN
[Several hundred lines elided]
BETA_TAC THEN ASM_REWRITE_TAC[] THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [] [INTER_COMM] THEN
CONV_TAC(REDEPTH_CONV LEFT_AND_EXISTS_CONV) THEN REWRITE_TAC[]]);;
Total number of primitive inferences: 18433
Notes:
"mtop" is the function that takes a metric to the corresponding
metric topology
"open(top) S" means "S is open in topology top"
"neigh(top)(N,x)" means "N is a neighbourhood of x in topology top"
"!x. ..." means "for all x, ..."
"?x. ..." means "there exists an x, ..."
"/\" is "and", "\/" is "or", "==>" is "implies"
"=" is polymorphic equality including "iff"
"UNIONS" is set union; "INTER" is pairwise intersection
"UNIV" is the set representing the whole type, i.e. the "universe"
Stars are polymorphic type annotations.
"$" before a name suppresses special parse status (infix etc.)
John.
P.S. Of course I still haven't done the "easy" group theory problem. However I
can point out that there is an implementation of Knuth-Bendix completion as a
derived inference rule in HOL, due to Konrad Slind, and I think the group
theory problem is one of the standard examples it can blow away automatically.