From lusk Thu Jun 23 09:58:04 1994 Received: from swan.cl.cam.ac.uk (swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id JAA19248 for ; Thu, 23 Jun 1994 09:55:13 -0500 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 23 Jun 1994 15:54:25 +0100 To: qed@mcs.anl.gov Subject: Re: Examples In-reply-to: Your message of "Fri, 17 Jun 94 13:34:20 MDT." <94Jun17.133431-0600.18491-2@scapa.cs.ualberta.ca> Date: Thu, 23 Jun 94 15:54:14 +0100 From: John Harrison Message-ID: <"swan.cl.cam.:054850:940623145432"@cl.cam.ac.uk> Andrzej Trybulec writes: | 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.