Hi Bill, | John, I'm pretty sure I downloaded it from this link | http://www.cl.cam.ac.uk/~jrh13/hol-light/ | a snapshot from 10th January 2010 is available as | a GZIPPED TAR FILE or as a zip file. | That's the right version, as hol.ml reads hol_version = "2.20++";;
OK, that's fine then. In general I would recommend that you just pick up the latest version from the Google Code site via subversion svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light rather than use those images. It gives you an easier way of keeping in sync with changes. However, if what you have works fine, then it doesn't matter for now. | It's perfectly possible to set things up this way, effectively | giving each theorem the additional hypothesis. I think that then | the proofs would look even more like your Mizar originals with the | "TarskiModel" hypothesis and the corresponding first step of each | proof. | | That would be excellent, John! OK, see the example appended below. It's slightly worse than I claimed because miz3 doesn't like theorems with free variables, so you also need to quantify over the geometric predicates and introduce them at the beginning of each proof. Other than that, the core of the proof is the same except with the additional hypothesis, which I label [0], which has to be called out when using other consequences. The extra cruft could certainly be removed with a bit of programming effort, since the whole miz3 platform is completely programmable. | I can give you more detailed guidance on how to set this up if you | like, but it might be fine to stick to the simpler version for a | bit. | | I would really like that advice. I want to submit my Hilbert geometry | paper soon, and I want to cite some readable geometry code. | | By the simpler version, I assume you mean | | | I had one theorem [whose proof was a mile long] | | | | AXIOM_1 and ... AXIOM_1 implies lemma1, lemma2, ... lemma17 | | I can start out that way! Can you explain? I'm so ignorant I don't | even know how to do that, but I bet it's easy, just new_definition... No, by the simpler version I just meant along the lines I was first suggesting where you work in a concrete model. If all you want to know is that your axiomatic reasoning is correct, then this is fine. The additional cruft of doing things more generically would only be useful if you really want to apply it in different models. Like Ulysses having himself lashed to the mast, you can even overwrite all the OCaml identifiers before the axioms so that you can't respond to their siren song and you are forced to work just from the axioms. | With either of these two solution, we're not using your original code | showing that R^2 is a model of Tarski's axioms, and that's a priority. Well, it's OK, it would just become part of a separate proof that R^2 is indeed a model of the axioms. I was thinking a bit about how to prove your other axioms in real^2, and I just added a useful lemma in the latest svn revision (135) that there exists a rigid transformation between two congruent sets (SSS congruent triangles in the plane being the case N = 2, M = 3) RIGID_TRANSFORMATION_BETWEEN_CONGRUENT_SETS = |- !x y. (!i j. 1 <= i /\ i <= dimindex(:M) /\ 1 <= j /\ j <= dimindex(:M) ==> dist(x$i,x$j) = dist(y$i,y$j)) ==> ?a f. orthogonal_transformation f /\ (!i. 1 <= i /\ i <= dimindex(:M) ==> y$i = a + f(x$i)) | | BTW Hilbert and Birkhoff both prove that with enough axioms | | including the parallel postulate, there's a unique model R^2, so | | there's nothing unrigorous about working in coordinates, at least | | if you understand this result, which Hartshorne does a pretty | | good job explaining. | | Yes, it would be very interesting to prove that. | | Would you really like to know how to prove that? I don't do it in my | paper, but I've often thought I should. Hartshorne's whole book more | of an extremely cool overview than a source of rigorous proofs, and | this part is especially sketchy. Birkhoff's proof barely exists, and | MacLane who cleaned up Birkhoff didn't fix that part? It would certainly be a very nice addition to any geometry formalization. | Yes, I think miz3 is definitely the best of the bunch. I've been | quite pleasantly surprised how usable it is, and how like Mizar the | experience of writing proofs in it becomes. | | I'll be happy to write miz3/HOL-Light code, if we can just fix some | problems that annoyed me with Mizar (see below). But I'm not happy | with Freek posting here about how he used dirty Ocaml hacks! What can | we do to clean up the code? BTW you told me to write HOL-Light, and | I'm be really happy to, and I must do this eventually, but right now | I'm really confused by all the non-Mizar proof assistants, because: Well, the whole point of LCF-style theorem provers like HOL Light is that you can afford pretty much arbitrary hacks without compromising logical soundness, because of the encapsulated kernel. This freedom is not quite absolute, as is being discussed in a parallel thread, but takes in what I would consider "normal ML programming". | I say the first requirement for a good proof assistant is for humans | to be able to code up nice readable axiomatic proofs. Right now this | does not seem to be true for HOL-Light, Coq or Isabelle. But proof | assistants can't do anything (I think) besides generate and check | axiomatic proofs. And if we can't code up nice readable axiomatic | proofs, then aren't the machines getting escaping our control? I think the main focus has been on raising the level of automation to the point where one can handle proofs that are not already presented in a nice axiomatic way. As a thought-experiment, imagine writing an explicit axiomatic proof of the following identity over the reals: |- ((x1 pow 2) + (x2 pow 2) + (x3 pow 2) + (x4 pow 2)) * ((y1 pow 2) + (y2 pow 2) + (y3 pow 2) + (y4 pow 2)) = (((((x1*y1) - (x2*y2)) - (x3*y3)) - (x4*y4)) pow 2) + (((((x1*y2) + (x2*y1)) + (x3*y4)) - (x4*y3)) pow 2) + (((((x1*y3) - (x2*y4)) + (x3*y1)) + (x4*y2)) pow 2) + (((((x1*y4) + (x2*y3)) - (x3*y2)) + (x4*y1)) pow 2) HOL Light's REAL_RING will construct such a proof for you automatically. The thought of being forced to do it by hand is pretty dismal, at least to me. I think I heard about someone spending months doing it in a more rudimentary proof assistant. | I assume everyone agrees with me, so maybe the problem was that no one | had any nice readable axiomatic proofs they wanted to code up. The | action seems to be in using powerful proof assistants to verify | e.g. FoG or Tom's Hales's Kepler conjecture proof. These are worthy | aims, and much more ambitious projects than mine. But mine is worth | doing too, I claim, and probably not very hard. I'd write the | readable axiomatic proofs code myself if I had a clue about how | HOL-Light worked. But I'm stymied by the examples being so much more | complicated than my Hilbert/Tarski geometry axioms examples. I think that's about it. Checking proofs that are already presented in a precise and explicit axiomatic style is not so difficult. But there aren't that many domains where we find such proofs. Besides synthetic geometry, Landau's real number construction was another particularly favorable example and it's no accident that it was formalized early, by Jutting in AUTOMATH. But indeed, the mechanics of basic proof checking is not that hard. You can of course read all about this and more in my textbook, so you can code it all yourself and don't need to rely on any fancy prover :-) http://www.cambridge.org/gb/knowledge/isbn/item2327697/ | To take our copyright discussion public, I'm absolutely thrilled that | HOL Light has a BSD license, as we see from | http://code.google.com/p/hol-light/. | I'm not sure why you think GPL is viral, but BSD is fine with me. | What confused me was the copyright on your ml files, e.g. | (* (c) Copyright, University of Cambridge 1998 *) | (* (c) Copyright, John Harrison 1998-2007 *) Although the code for HOL Light was largely written from scratch, a lot of the basic design follows earlier versions of HOL, and indeed there used to be some traces of code from older HOLs. So besides the fact that I worked in Cambridge myself for a lot of this period, the influence of other HOL work at Cambridge was significant. Since I left Cambridge HOL Light has been more a personal project, to which quite a few others besides myself have contributed. (You'll find other names in some of the other copyright headers in the distribution.) John. (* ------------------------------------------------------------------------- *) (* Infix status for a couple of the geometric predicates. *) (* ------------------------------------------------------------------------- *) parse_as_infix("===",(12, "right"));; parse_as_infix("cong",(12, "right"));; (* ------------------------------------------------------------------------- *) (* Constant saying that three predicates satisfy the Tarski axioms. *) (* ------------------------------------------------------------------------- *) let TarskiModel = new_definition `TarskiModel((===),(Between:point#point#point->bool),(cong)) <=> (!a b. a,b === b,a) /\ (!a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s) /\ (!a b c. a,b === c,c ==> a = b) /\ (!a q b c. ?x. Between(q,a,x) /\ a,x === b,c) /\ (!a b c x a' b' c' x'. ~(a = b) /\ a,b,c cong a',b',c' /\ Between(a,b,x) /\ Between(a',b',x') /\ b,x === b',x' ==> c,x === c',x') /\ (!a b. Between(a,b,a) ==> a = b) /\ (!a b p q z. Between(a,p,z) /\ Between(b,q,z) ==> ?x. Between(p,x,b) /\ Between(q,x,a)) /\ (!a b c x y z. a,b,c cong x,y,z <=> a,b === x,y /\ a,c === x,z /\ b,c === y,z)`;; let [A1;A2;A3;A4;A5;A6;A7;cong] = map DISCH_ALL (CONJUNCTS(UNDISCH(fst(EQ_IMP_RULE(SPEC_ALL TarskiModel)))));; (* ------------------------------------------------------------------------- *) (* Now Mizarlight versions of the actual proofs. *) (* ------------------------------------------------------------------------- *) loadt "miz3/make.ml";; let EquivReflexive = thm `; !(===) (Between:point#point#point->bool) (cong). TarskiModel((===),(Between:point#point#point->bool),(cong)) ==> !a b. a,b === a,b proof let (===) be point#point->point#point->bool; let (Between) be point#point#point->bool; let (cong) be point#point#point->point#point#point->bool; assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0]; let a b be point; b,a === a,b by 0,A1; thus a,b === a,b by 0,A2; end`;; let EquivSymmetric = thm `; !(===) (Between:point#point#point->bool) (cong). TarskiModel((===),(Between:point#point#point->bool),(cong)) ==> !a b c d. a,b === c,d ==> c,d === a,b proof let (===) be point#point->point#point->bool; let (Between) be point#point#point->bool; let (cong) be point#point#point->point#point#point->bool; assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0]; let a b c d be point; assume a,b === c,d [1]; a,b === a,b by 0,EquivReflexive; thus c,d === a,b by 0, 1, A2; end`;; let EquivTransitive = thm `; !(===) (Between:point#point#point->bool) (cong). TarskiModel((===),(Between:point#point#point->bool),(cong)) ==> !a b p q r s : point. a,b === p,q /\ p,q === r,s ==> a,b === r,s proof let (===) be point#point->point#point->bool; let (Between) be point#point#point->bool; let (cong) be point#point#point->point#point#point->bool; assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0]; let a b p q r s be point; assume a,b === p,q [1]; assume p,q === r,s [2]; p,q === a,b by 0, 1, EquivSymmetric; thus a,b === r,s by 0, 2, A2; end`;; let Baaa_THM = thm `; !(===) (Between:point#point#point->bool) (cong). TarskiModel((===),(Between:point#point#point->bool),(cong)) ==> !a b. Between (a,a,a) /\ a,a === b,b proof let (===) be point#point->point#point->bool; let (Between) be point#point#point->bool; let (cong) be point#point#point->point#point#point->bool; assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0]; let a b be point; ?x. Between (a,a,x) /\ a,x === b,b by 0,A4; consider x such that Between (a,a,x) /\ a,x === b,b [1]; a = x by 0,1, A3; thus Between (a,a,a) /\ a,a === b,b by 0,1; end`;; ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
