That is a function of type term -> thm, so will enable you to
"test" terms' behaviours. The more definitions you put into the
list passed to REWRITE_CONV, the more you will get out.
Thanks, Michael! I see your REWRITE_CONV is heavily discussed in sec 7.4
Rewriting of the HOL Light tutorial. I should work every example in the
section. I would not have guessed what you said, so thanks again.
My claim [on whether miz3 is "intentionally weakened"] is based on
my believing that miz3 imposes a time limit,
Freek boldly tells folks to increase the time limit. I use
timeout := 30;;
and Freek posted here not long ago, I believe, that
timeout := -1;;
means there is no time limit. I complained to Freek about something and he
told me to try
timeout := 10;;
as if that would take forever. I've learned to find other things to do while
I'm waiting for miz3 to evaluate my code. I don't just sit there and watch the
screen anymore, and I'm grateful for Freek's caching, which means "the 2nd time
around" there's no MESON calculations.
Thus, I conclude that the purpose of the default timeout isn't to weaken miz3,
but to better instruct beginners who, if I'm a representative example, make
scores of obvious errors and need immediate feedback :)
and that there is a depth limit in MESON more generally
Yes, but that has nothing to do with miz3. As the HOL Light reference manual
says,
Normally MESON, MESON_TAC and ASM_MESON_TAC explore the search space
by successively increasing a size limit from 0, increasing it by 1 per
step and giving up when a depth of 50 is reached. The more general
tactic GEN_MESON_TAC allows the user to specify the starting,
finishing and stepping value, but is otherwise identical to
ASM_MESON_TAC. In fact, that is defined as:
# let ASM_MESON_TAC = GEN_MESON_TAC 0 50 1;;
Normally, the defaults built into MESON_TAC and ASM_MESON_TAC are
reasonably effective. However, very occasionally a goal exhibits a
small search space yet still requires a deep proof, so you may
find GEN_MESON_TAC with a larger ``maximum'' value than 50
useful. Another potential use is to start the search at a depth
that you know will succeed, to reduce the search time when a proof
is re-run. 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.
I think it's clear that John isn't trying to put shackles on miz3 with the
MESON timeout. I don't have a clue about this depth biz, or whether I'd be
better off with a larger depth limit than the default of 50.
Both of these things will stop miz3's "by" from proving things that
it might otherwise. Hence it is "intentionally weakened".
I respectfully submit that you have not made your case.
That weakening then helps to limit the size of the inference jumps
you can make. I do not think this is a bad thing.
The default timeout, which I can't live with, definitely limit the size of the
inference jumps. But you taught me that such limits are a bad thing, or more
precisely, it's playing an unwinnable game to monkey with the heuristics to
shackle the proof assistant. You're the one who got me out of the
Mizar-in-the-classroom game of counting on proof assistant weakness in order to
police the students' homework. I am very grateful to you, Michael, for curing
me of this, and you may recall it took you many emails. It's hard to give up
control, but respect for your students may require it, as in, "If you're more
interested in exploring the proof assistant than in writing up a `complete'
geometry proof, maybe you're on the right track!"
BTW I'm near 3600 lines of my miz3 Hilbert geometry code
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
and just proved Euclid's Prop I.12, which Euclid used advanced circle
techniques to prove, and Greenberg skipped some important steps of:
DropPerpendicularToLine_THM : thm =
|- !P l.
Line l
==> P NOTIN l
==> ?A D. A IN l /\ D IN l /\ Right (angle P D A)
It's really improving my understanding to code up these miz3 proofs. Greenberg
has a nice proof (Prop. 3.16) which I saw no problem with until I tried to
formalize it.
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
