Hi Bill,
| John and Freek, I finished porting my Tarski geometry Mizar code to
| miz3, and it's about 2/3 the size!!! Thank you again for your help!
Congratulations! I'm really happy to see this work, which is both a
nice addition to HOL Light and a serious stress-test of miz3. I
suppose it is Freek's little syntactic improvements like "qed" that
account for the smaller code, is it? Since I gather you were trying to
keep the automation at a Mizar-like level, I assume that you didn't
try cutting out stages and relying on stronger justification, let
along going in for Urban-style Vampirism :-) By the way, I appreciate
the acknowledgement in the comments, but it's a bit much to say that
the port is "mostly due to John Harrison". All I did was point you in
the right direction and prove a few really simple lemmas as an
example.
| You did a good job of boiling down the essential core.
|
| Thanks, John! I spent years working for Richard Stallman, who taught
| me to write (Emacs) bug reports. It didn't help my math career, but
| it was great to find folks who WANTED to hear about their errors!
Oh, I didn't know you used to work for Richard! I was sorry to see he
fell ill the other day while giving a talk in Barcelona. I hope he's
doing all right now.
| I found a workaround for this problem that I feel is a better
| solution. I didn't know how to nest cases in Mizar, but Freek's
| grammar showed me how to do it.
Oh I see, yes, that probably is a better solution in several ways.
Using an explicit tactic would make your proofs only 99% declarative
instead of 100%, which would have been a bit unsatisfying.
| 1) I was able to write 1500 lines of Mizar code without any good Mizar
| dox because the error messages were informative enough. The miz3
| error messages are not nearly as good, and I'll accept Freek's word
| that HOL Light causes this. But we can make do with baffling error
| messages if the dox are good enough. I would sit down right now and
| write up the syntax & semantics of miz3 if I knew what they were.
It would certainly be possible to improve the HOL Light error
messages. Generally HOL Light uses only the simplest error reporting
to keep the code simple. (In fact, some parts of the original HOL
Light core were basically Konrad Slind's hol90 code ported from SML to
OCaml and with the error handling removed.) If there are some specific
situations that you found particularly irksome, let me know and I'll
think about a fix. You might already have done this before on this
thread but I didn't pay close enough attention to that side of
things.
If you do have time to work on some kind of miz3 documentation, it
would be great, of course! I think the combination of the existing
paper by Freek, documentation for Mizar itself and even a closer
examination of the code might be enough to give a more or less
definitive picture. There is a reasonable level of documentation of
the "native HOL" facilities; in fact every non-theorem identifier in
the HOL Light system is supposed to have an entry in the reference
manual, which you can also get from inside HOL Light itself by
help "CONJ_TAC";;
| 2) We don't need strict miz3 compliance with Mizar. Mizar was
| extremely successful in showing that lots of folks can write up lots
| of formal proofs, without being a HOL Light or Coq code wizard. But
| at this point Mizar is like an old pyramid, and we need spaceships.
It's certainly true that HOL Light has advantages of programmability,
more decision procedures and a generally more open architecture. But
I wouldn't dismiss Mizar too readily since it has a lot of other very
good features like its more flexible type system, and a much larger
library of abstract mathematics.
| 1) Freek's 1201.3601-1.pdf isn't actually about how to run Mizar
| programs in HOL Light. It's about how to mix declarative &
| procedural, and I I give Freek credit for for his bold effort.
Yes, although I can't really speak for Freek I think I can confidently
say that his main interest was in discussing the ideas more abstractly
rather than trying to write end-user documentation. So there is
probably a gap in the market for a tutorial and/or reference for miz3
from the user perspective.
| 2) Make HOL Light the right place to write Mizar-like code. I think
| the Mizar authors were great pioneers, but their program is an
| Egyptian pyramid with secret source code that they're not maintaining.
I am certainly very happy to see the wider use of declarative proof in
HOL Light. More generally, I'm all in favour of having people try out
alternative approaches to the default tactic language or build other
proof tools around HOL Light. For example, there is an interesting set
of Isabelle-style tactics by Petros Papapanagiotou and Jacques Fleuriot
that you can find in the "IsabelleLight" subdirectory.
John.
------------------------------------------------------------------------------
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
