Thanks, John, and thanks again for your help porting to miz3!
there is probably a gap in the market for a tutorial and/or
reference for miz3 from the user perspective.
Great! This is my main task now. But I don't know enough to write
this miz3 tutorial and user reference manual (more below).
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,
Yes, and Freek's idea (which violates the grammar) of beginning a thm
with let ... assume ... thus ... proof (example below), with the
assume statements taking 1 line instead of 2. But I'll count:
The part you wrote saved 150 lines. Ignoring that, my new code is 3/4
the size of the original. As these little syntactic improvements
count more in short proofs, let's go to the first Mizar proof that's
over 30 lines (SegmentAddition), and then the miz3 code is 7/9 the
size of the Mizar code, which isn't 2/3, but every little bit helps.
Since I gather you were trying to keep the automation at a
Mizar-like level,
Absolutely, and I'm convinced that this is mild enough Mizar-like
automation that good high school students could use it.
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.
I am really grateful to you, John, and I couldn't have done without
you, but, uh, I was hoping you'd do even more The reference manual
says not to use new_axiom. Better error messages would be great.
I'll write some dox but I don't know enough right now to write them.
Here's something simple about `cases' I don't know, in a short proof:
let B124and234Ordered_THM = thm `;
let a b c d be point;
assume Between (a,b,d) [H1];
assume Between (b,c,d) [H2];
thus is_ordered (a,b,c,d)
proof
cases;
suppose b = c [P1];
Between (a,b,c) [P2] by -, Bqaa_THM;
Between (a,c,d) by P1, H1;
qed by P2, H1, -, H2, is_ordered_DEF;
suppose ~(b = c) [Q1];
Between (a,b,c) by H1, H2, B124and234then123_THM;
qed by -, Q1, H2, BTransitivityOrdered_THM;
end`;;
Note the new more compact Freek style of stating the thm, which
violates Freek's grammar on p 16, which say a lemma must start
let ident = thm `; formula proof; `;;
When the cases construction ends, I immediately write end`;;. Why is
that OK? Why didn't I need to write qed by -`;;, or thus thesis; end?
Of my 37 miz3 lemmas, the only ones that end in end`;; are the ones
that end on a cases construction. I can't write the new dox until I
understand this. Maybe I can figure it out by reading miz3.ml.
Or another dumb question: How do you run miz3 code? I'm just
selecting in an Emacs window and then pasting into a terminal running
hol_light> ocaml
#use "hol.ml";;
Why can't I paste in a use command like
#use "John5-8ModelTarski.ml";;
I know Freek describes a vi-based system but I haven't learned it yet.
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.
Great, I'm email them to you again privately. Basically I'd say that
the miz3 error messages are good enough for reasonably short proofs,
but for proofs 70+ lines long, the error messages can be useless.
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.
The Mizar type system caused me a lot of trouble, because I couldn't
define the class of Tarski models without showing that R^2 was a
Tarski model, and that ran something 450+ lines in Trybulec's simpler
version of incidence axioms that I ported. But more seriously:
I don't think Mizar is a flourishing community anymore. HOL Light is
a flourishing community, while Mizar made great contribution before.
I know folks teach courses using Mizar,but I'm sure code improvements
would really help, like TABs and no 80 character line limit.
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 hope so too. I had kind of a falling out with Richard Stallman
about his free books crusade, which I felt violated the spirit of his
free software crusade (we need to read and modify each other's code).
But I really learned a lot from Richard, and found it a great pleasure
to work with him. My combinatorics paper
http://www.math.northwestern.edu/~richter/RichterPAMS-Lambda.pdf took
6 years to submit because I couldn't get anyone to admit that they
didn't know the supposedly trivial combinatorial proofs. While
Richard loved to get bug report! I used to have this on my web page:
Emacs Pretester
>From '92 to '02, reported to head of GNU project
Richard Stallman, 100s of bug reports. Wrote some C code for mouse/X
interaction. Ran Emacs under source-level C debugger GDB. Wrote 100
lines GDB/Emacs documentation. Learned enough C, X, & configure to
take active part in investigations, and RCS to keep up with patches.
One bug: found pointer which was garbage-collected prematurely.
Wrote/maintained code for international character display long enough
that Emacs needed legal papers for the copyright.
--
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
