Thanks, John! I'd be thrilled if you included my code in the HOL Light
distribution (miz3 dir sounds good)! I think it would improve my paper's
chance of being accepted. I'll definitely write to both Hartshorne &
Greenberg, but I'll let HOL Light finish debugging my paper first. I think BTW
that Hartshorne wrote a great book, but since he taught the course to
undergraduate non-math majors, he never got real feedback about his proofs.
Greenberg's book (which doesn't really explain the Hilbert/Euclid connection)
is used as a math grad text so it's been torture-tested. I certainly give
Freek a lot of credit too, for writing a great program miz3, and for the very
long private miz3 tutorial he gave me. I'm really happy you ran my code, and
that it worked! Thanks for clarifying that you don't want miz3 to be weak:
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.
I don't understand the technicalities, but may I make a suggestion? No matter
how powerful you make miz3, users can still put extra details in their proofs.
The purpose of extra details is good pedagogy, so that another human can read
the code and learn the proof. I think my miz3 code is almost as readable as my
paper, especially with the fancy HOL4/Isabelle-style math fonts. If miz3 is
really powerful, then users are on the "honor system" as to whether they really
understand their own proofs, but math is already on the "honor system", so it's
fine.
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, and a really important fact is that Freek tells people to increase
timeout! Timeout is only set to 1 because new users will make lots of simple
mistakes, and a high timeout makes you wait for HOL Light to tell you about
your obvious error. Once you know what you're doing you can raise the
timeout. I'm using timeout := 50;; now. Freek uses timeout := -1;; quite
often (infinite timeout).
I wasn't clear about my time-table yesterday. I have 4 tasks left, in
increasing order of difficulty:
1) finish formalizing the plane geometry parts of my 26 page paper (close to
done)
2) port the new geometry rigor from my code to my paper (shouldn't take long,
and then I can write to Hartshorne)
3) finish my miz3 users guide MizTips (I must understand Freek's syntax &
semantics lectures)
4) understand HOL (I'm reading the HOL4 Logic manual)
The last task sounds hard to me, and possibly I won't do a good job. So if you
want to improve miz3 for my paper, you'll have time. What I would most like you
to look at my code and figure out why MESON is working so hard. I have 16
MESON solved at numbers over 200,000, but I don't think I ever ask miz3 to do
anything as hard as the Los Logic problem, which had a MESON solved at number
about 20,000. My hazy guess is that I'm having a bad interaction between MESON
(a FOL prover) and the set theory in my paper. The first place this comes up
is with my completely trivial rewrite of axiom B4:
let B4' = thm `;
! l A B C. Line l /\ ~Collinear A B C /\
A NOTIN l /\ B NOTIN l /\ C NOTIN l /\
(? X. X IN l /\ X IN open (A,C)) ==>
(? Y. Y IN l /\ Y IN open (A,B)) \/ (? Y. Y IN l /\ Y IN open (B,C))
by IN_Interval, B4`;;
(*
The proof above only works because timeout is set to at least 5.
Otherwise the proof gets the miz3 error #2 inference time-out. With
timeout set to the default value of 1, we use this proof:
let B4prime_THM = thm `;
let l be point_set;
let A B C be point;
assume Line l /\ ~Collinear A B C /\
A NOTIN l /\ B NOTIN l /\ C NOTIN l /\
(? X. X IN l /\ X IN open (A,C)) [H1];
thus (? Y. Y IN l /\ Y IN open (A,B)) \/ (? Y. Y IN l /\ Y IN open (B,C))
proof
Line l /\ ~Collinear A B C /\
A NOTIN l /\ B NOTIN l /\ C NOTIN l /\
(? X. X IN l /\ Between A X C) by H1, IN_Interval;
(? Y. Y IN l /\ Between A Y B) \/ (? Y. Y IN l /\ Between B Y C) by -,
B4;
qed by -, IN_Interval`;;
*)
Maybe I'm the problem, and not miz3. Maybe I need to use some HOL Light
tactics to tell miz3 what I want it to do. In this case, replace each Between
P Q R in axiom B4 with the equivalent Q IN open (P,R).
--
Best,
Bill
let B4 = new_axiom
`! l A B C. Line l /\ ~Collinear A B C /\
A NOTIN l /\ B NOTIN l /\ C NOTIN l /\
(? X. X IN l /\ Between A X C) ==>
(? Y. Y IN l /\ Between A Y B) \/ (? Y. Y IN l /\ Between B Y C)`;;
let IN_Interval = thm `;
! A B X. X IN open (A,B) <=> Between A X B
by Interval_DEF, IN_ELIM_THM, REWRITE_TAC`;;
------------------------------------------------------------------------------
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
