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
