Hi Bill,
| Thanks for thinking about my Tarski geometry code problems, John!
| That would be great to use less than full Mizar mode. Let me stress
| that Mizar does more automation than is allowed in 2-column proofs.
One of the nice things about miz3 (and indeed Isabelle/Isar) is that
the question of what automation to use for the steps is pretty much
orthogonal to the structuring and syntactic support. You can replace
the default miz3 prover just by changing this line:
let default_prover = ref ("HOL_BY", CONV_TAC o HOL_BY);;
That default uses the prover HOL_BY in "Examples/holby.ml", which
Freek and I once designed as a reverse-engineering or rational
reconstruction of Mizar's own prover. My own thoughts have always
been on how to make it stronger in useful ways, but you could
deliberately choose to weaken it.
If you don't already know it, Piotr Rudnicki's paper "Obvious
Inferences" is an interesting discussion of what should be considered
"obvious" and relates closely to the design of the Mizar prover.
| BTW can we use fancy characters like
| =E2=88=A7=E2=87=92=E2=88=80=E2=88=83 in HOL Light?
The logical core allows any OCaml string, i.e. any finite sequence
of bytes, as the name of a variable or constant, without restrictions.
For example, the following variable has a sound but looks invisible.
Almost like a koan: what is the sound of an invisible variable?
# mk_var("\007",`:num`);;
val it : term = ``
However, the parsing and printing layer does not currently support the
use of characters beyond the following categories of conventional
ASCII printables (see "preterm.ml" for the code):
spaces = " \t\n\r"
separators = ",;"
brackets = "()[]{}"
symbs = "\\!@#$%^&*-+|\\<=>/?~.:"
alphas = "'abcdefghijklmnopqrstuvwxyz_ABCDEFGHIJKLMNOPQRSTUVWXYZ"
nums = "0123456789"
So it would be severely inconvient to use other characters without
modifying the front end. Of course, you can do that if you want, but
I would discourage it and advise you to set up some additional
interface layer. HOL Zero has a much better story here where
special characters are consistently escaped and the parser and
printer have a reasonable inverse relationship.
| It sure makes the code more readable. I wrote Emacs code so I could
| do it in Mizar.
That's a matter of opinion. Personally, I dislike top-bit-set
characters in code and proofs, finding that the improvement in
readability is minor and the other inconveniences significant. The
first thing I did with your Mizar code was to remove them.
| I suppose that most geometric problems are purely universally
| quantified so the extra structuring steps are not as important.
|
| I don't know. Is this theorem and definition universally quantified?
No, clearly there are exceptions, but still I think my statement (note
the "most") holds for what I think of as the classical corpus of
geometry theorems. However, I can't pretend to have done any sort of
rigorous survey.
| Thanks for the encouragement to modify code! I suppose I'd have to
| learn the HOL Light mechanics pretty well first. I think I'm a pretty
| good Scheme programmer, and ML can't be that different. But, uh, I
| was really hoping you guys would write it :) Right now we're not
| having an interface problem, but a design problem: how do you stack
| definitions and axioms into something like an Isabelle locale, and
| then cite that locale portably?
Instead of making "===" and "Between" constants, you can just define
a constant "TarskiModel" to indicate that two arbitrary predicates
"===" and "Between" satisfy the axioms, something like this
TarskiModel((===),Between) <=>
(!a b. a,b === b,a) /\
....
(!a b p q z.
Between(a,p,z) /\ Between(b,q,z)
==> ?x. Between(p,x,b) /\ Between(q,x,a))
Then every theorem would become |- TarskiModel((===),Between) ==> P
instead of just |- P. If I understand your Mizar code correctly, this
pretty much matches what you are doing there.
| Julien Narboux, who used Coq to prove Tarksi theorems, said something
| like that, and I just don't understand. It took me 300 lines to
| (porting Julien) prove Gupta's amazing theorem that 2 points determine
| a line. I found it exhilarating, not painful. My problem is math: I
| don't know how to prove the rest of Hilbert's axioms. I don't know
| how to prove the full Pasch axiom (Tarski's axiom is 1/3 of that).
This reminds me of something Andrzej Trybulec said about automated
theorem provers: why should we let the machine deprive us of the
pleasure of proving things?
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
