Hi Bill, | Thanks, John! I'm up to Euclid's Prop I.28, so I have formalized | Hartshorne's result | http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertA | xiomGeometry.tar.gz Thm 10.4: All of Euclid's propositions (I.1) to | (I.28) except (I.1) and (I.22), can be proved in an arbitrary Hilbert | plane, as explained above.
Congratulations --- it's a really impressive piece of work! I've just tried it out and it all runs for me too without a hitch. If you are agreeable, I think it would make sense to include it (after any final improvements or polishing you want to make) in the HOL Light distribution, either on its own or in the "miz3" directory. It's a very nice extended example of how the miz3 style of proof can be used. Some of the additional material like your "Miz3Tips" might be very useful to miz3 users too, as also might the material on Felix Breuer's blog (http://blog.felixbreuer.net/2012/06/11/hol.html). In general, it might be a good idea to make the HOL Light tutorial pages more open and wiki-like, which is something Colin Rowat has already suggested to me. | So thanks for all your help, and for writing such a great program HOL | Light! Prop I.29 is the first time Euclid uses the parallel postulate, | and I think that's why Hartshorne quit there. I'll go a little | farther, as no US high school geometry text does a reasonable job | proving the triangle sum theorem (angle sum = 180 deg), but I'll | finish soon. You're welcome! Indeed I think Freek deserves at least as much of the credit as I do, since he did most of the hard work of writing miz3, without which you would have been stuck with one of HOL Light's more cryptic proof styles. (The HOL expert style of proof was once parodied, I think by by Conor McBride, as "EAR_OF_BAT_TAC[]".) I'll be interested to see how the angle sum proof looks in axiomatic style. I remember being a bit surprised and disappointed at how messy the "vectorial" proof is that I once formalized. (See TRIANGLE_ANGLE_SUM in "Multivariate/geom.ml"). It might be fun to contact Hartshorne himself to see if he is interested in your detailed formal proofs. | If you can tell me how to use use permutative rewrites in my miz3 | code, so that ~Collinear {A, B, C} = ~Collinear {B, C, A} = | ~Collinear {C, B, A} etc, I'll code it up, and it will make my | code a little cleaner. I bet you're especially busy with the new | ocaml release, and if we don't fix this, that's fine. I'll take a look at your code and see if it would be easy-ish to make such a cleanup. | I didn't have any serious comment about the different versions of | HOL. All of you are using HOL for real world projects where you | really have to believe the code works, and I bet everyone sensibly | says, "I'm going to use my code, which I trust." Yes, and even though I trust other code, one gets very attached to one's own baby, as you can imagine. | I really want to know how strong or weak you want miz3 to be. My | belief (not based on a lot of info) is that Mizar is intentionally | weak, partly to encourage very readable proofs and to make Mizar | usable for student homework, but that you have no such interest in | miz3 weakness. You are certainly right about Mizar's prover being intentionally weak. I think efficiency of proof processing may have been a (or even the) major factor behind this decision. With the batch processing model you really want the individual steps to be quick. And the timeout in miz3 is presumably motivated similarly, though as I recall you found that a higher timeout was still productive as you became more experienced. Yes, I don't have any similar motivation for wanting the prover to be weak, though requiring very low-level proofs has its place, such as the pedagogical application you mentioned. I do like to keep proofs somewhat explicit in the sense of not using many lemmas implicitly (which is why, for example, I don't have a larger set of rewrites and simplifications as the default), but I don't want to have to spend time manually proving things that could easily be blown away with decision procedures. So I suppose I want to be somewhat explicit about lemmas but not so much about proof methods. | MESON is pretty powerful! If you had a more powerful FOL prover than | MESON, or a compatible set-theory prover, I think you use such provers | in holby.ml as well. Your purple book seemed to stress that we should | be combining the procedural and declarative approaches, and that | doesn't indicate a desire to weaken the declarative approach. Yes, there is lots of scope for improving such provers, and I think it could raise the level of interaction in miz3 to have a more powerful prover. Ideally one would want a smooth integration of pure logic, set theory, algebra and arithmetical theories, but that's still a research challenge. Still, we know enough to make it much more powerful than the current placeholder, and modern FOL provers do sometimes manage to do more than you might expect. For example, I once mentioned a nice little metric space exercise from Kaplansky's "Set theory and metric spaces") to Tobias Nipkow: (!x. d(x,x) = &0) /\ (!x y. d(x,y) = d(y,x)) /\ (!x y. ~(x = y) ==> &1 <= d(x,y) /\ d(x,y) <= &2) ==> !a b c. d(a,c) <= d(a,b) + d(b,c) and he even surprised himself when the E prover (via the Sledgehammer linkup) got it automatically just from lemmas lying round in the Isabelle/HOL library, even though it needs a bit of arithmetic as well as pure FOL. John. ------------------------------------------------------------------------------ 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
