Thanks for explaining GSPEC, SETSPEC & IN_ELIM_THM, Michael! I'm glad to know
that HOL4 can replicate my 1-line proof with SRW_TAC [][EXTENSION], similarly
"complicated underneath the hood." I'm confused by you paraphrasing Konrad as
saying that your exercise was "annoying to prove." It would seem to me now
that Konrad probably meant that there's a slick 1-line proof that would be, for
newbies like me, "hard to understand".
Thanks for also explaining IN_ELIM_THM, John! Your 2nd fork is all I'm I'm
worrying:
the encoding of sets and the IN_ELIM_THM theorem that's used to
unravel it seems complicated or unintuitive to explain to readers
not versed in HOL?
And it's not just me who's not versed in HOL. I'm hoping mathematicians and
high school teachers are going to read my paper and code, so the less I
befuddle them the better. It doesn't follow that my lambda rewrite is a good
idea, and I'd like your guidance here. I didn't understand your SET_RULE
rewrite, so I'll go read about SET_RULE. Let me back up a bit:
Originally I had problems with set in miz3, but I think now that it was just my
incompetence, and after I learned about IN_ELIM_THM, I could use {...} in my
definitions of rays, angles etc. I just posted a problem with miz3 and {...},
but that seems pretty minor to me. So I'm no longer thinking that "compiler
does a poor job on code."
I still have set theory problems, but they don't seem to involve miz3. Ramana
and Michael helped me to eliminate new_axiom and new_type from the beginning of
my simpler Tarski axiomatic geometry code. But it got messy when I came to my
defined infix predicate
parse_as_infix("cong",(12, "right"));;
let cong_DEF = new_definition
`a,b,c cong x,y,z <=>
a,b === x,y /\ a,c === x,z /\ b,c === y,z`;;
and I never finished the rewrite. I was amazed to get even that far.
Right now I'm worrying about a different problem, that I've never understood
sets.ml, especially its use of IN_ELIM_THM to prove the IN_<operation>
theorems. After Michael taught me that a {...} is equal, in a complicated way,
to a lambda, I thought, why not just define INTER, DELETE, UNION etc as
lambdas? Then the IN_<operation> theorems are easy to prove, and I wrote up
miz3 proofs myself that I could easily understand. It would be easy to rewrite
my 4000 lines of miz3 Hilbert code using lambda defs of INTER etc, and maybe
that makes my code look simpler or more self-contained. I'm still not
convinced it's a good idea. I think I'm missing a lot. What is the point of
the {...} definition of INTER, other than to see the nice {...} notation? I
love the {...} notation myself, but it's really equal to a lambda. So I
wonder if the visual plus of some {...} in my code and in sets.ml offsets the
fact that BETA_THM is so much simpler than IN_ELIM_THM. I can't judge. It !
was definitely a thrill for me to write readable understandable miz3 proofs of
all the sets.ml results that I use.
I can think of other miz3 problems that seem a lot more pressing that set
notations, like being able to use
#use "<miz3-file>.ml";;
I'm guessing I'll have 5000 lines of code by the time I'm done, and what if
somebody's machine can't store that much in the X-selection or whatever to
paste it from one window to another? And if we could #use miz3 code, couldn't
it be included in distributions with straight HOL Light code?
We had a vigorous discussion about about how powerful miz3 could be, or wants
to be. Here's what I learned, mostly from Michael. Mizar, as opposed to
miz3, seems to have intentionally weakened itself (i.e. you have to write out
very complete proofs), and that's a plus for using Mizar in classrooms to
police the students' homework. I used to desire such weakness, but Michael
convinced me that this is a bad idea (respect the students, don't shackle
them!), and something that, at least in miz3, is just a matter of fiddling with
the heuristics in a hit or miss way. Freek explained there was no evidence for
any shackling of miz3, which can indeed give 1-line proofs of my first 24
theorems or so. But it's odd that miz3 isn't even more powerful. Freek
pointed out that MESON has a built-in depth limit of 50 which GEN_MESON_TAC can
remove. But you seem to argue in the reference manual that raising the depth
limit isn't a good idea:
However, the inconvenience of doing this is seldom repaid by a
dramatic improvement in performance, since exploration is normally
at least exponential with the size bound.
Michael & I agreed we wanted miz3 to be more powerful, and you're the expert!
Freek explained that all the calculation of "by" justifications is actually
done in your code holby.ml. Here's a dumb question. I know MESON is an FOL
prover that can't handle true HOL, and I think I have some true HOL code, owing
to my sets.ml set theory. But I have no idea how much my sets slow MESON down.
--
Best,
Bill
------------------------------------------------------------------------------
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
