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-LightMiz3HilbertAxiomGeometry.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.
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. 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 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." 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. I have only two pieces of evidence about your intentions. Your file Examples/holby.ml starts (* ========================================================================= *) (* A HOL "by" tactic, doing Mizar-like things, trying something that is *) (* sufficient for HOL's basic rules, trying a few other things like *) (* arithmetic, and finally if all else fails using MESON_TAC[]. *) (* ========================================================================= *) 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. My opinion about weakness has changed drastically. Initially I was counting on miz3 to be weak to make sure I wasn't taking big leaps, and to police student homework. But a long discussion here convinced me (Michael mostly) that this weakness isn't a good idea. I now think taking big leaps is fine, and if I'm too dumb to spot big leaps in either my code in a students, uh, I'm in bad shape, and I shouldn't be counting on the program to bail me out. One of the things which changed my mind was a discussion with Cris and Rob about Los's Logic problem which you write about on p 36 of your tutorial, writing "The machine proves this a lot faster than I could." I couldn't prove it at all. But Rob wrote up a short mathematical proof of Los's Logic result, which I easily coded in miz3 (code for Rob's original proof below) and I decided that it's OK for MESON to perform such leaps in my code. -- Best, Bill #load "unix.cma";; loadt "miz3/miz3.ml";; horizon := 0;; let RobProof2LosLogic_THM = thm `; let P Q be A->A->bool; assume ! x y z. P x y /\ P y z ==> P x z [Ptrans]; assume ! x y z. Q x y /\ Q y z ==> Q x z [Qtrans]; assume !x y. P x y ==> P y x [Psym]; assume !x y. P x y \/ Q x y [PunionQ]; thus (!x y. P x y) \/ (!x y. Q x y) proof assume ~(!x y. P x y); consider a b such that ~P a b /\ ~P b a [notPab] by -, Psym; Q a b /\ Q b a [Qab] by -, Psym, PunionQ; !x y. Q x y proof let x y be A; cases; suppose P x a /\ P b y [PxyPby]; ~P x y proof assume P x y [Con]; P a x /\ P y b by PxyPby, Psym; P a b by -, Con, Ptrans; qed by -, notPab; Q x y by -, PunionQ; qed by -; suppose ~P x a /\ ~P b y; Q x a /\ Q b y by -, PunionQ; qed by -, Qab, Qtrans; suppose P x a /\ ~P b y [Pxy_notPby]; ~P x b proof assume P x b; P a b by -, Pxy_notPby, Psym, Ptrans; qed by -, notPab; Q x b /\ Q b y by -, Pxy_notPby, PunionQ; qed by -, Qtrans; suppose ~P x a /\ P b y; P y b /\ ~P a x [Pyb_notPax] by -, Psym; ~P y a proof assume P y a; P a b by -, Psym, Pyb_notPax, Ptrans; qed by -, notPab; Q x a /\ Q a y by Pyb_notPax, -, Psym, PunionQ; qed by -, Qtrans; end; qed by -`;; ------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info