Thanks, John! Please take my code whenever you like. I'm done coding, and I'll regard my tar.gz file to be final after I fold my miz3 improvement back into my paper and finish my Miz3Tips file, which only requires me to understand Freek's syntax, and he just made a contribution to that, explaining that miz3 definitely allow ending a proof with the final semicolon end; `;; These two matters won't take more than 2 weeks. Understanding HOL might take longer, but that's not needed for you to distribute my code. Thanks again for offering to include my code in your distribution. The stronger my ties are to the HOL community, the better the chances of my math paper is. The math folks and K-12 math ed folks would like to know that the HOL community thinks that e.g. teaching real axiomatic geometry with a proof assistant is possible.
Generally speaking, I'd say that "the automation is too powerful" is a problem we'd love [miz3] to have! Great! Right now it's not powerful enough for me. Among other things, this makes MESON relatively inefficient at using a logical equivalence |- !x. P[x] <=> Q[x] to "rewrite" P to Q inside another formula; the length of the required proof grows with the size of that formula, and replacement inside quantifiers may expand the search space further because you need to examine different instantiations. I think that accounts for your time-consuming B4' derivation, for example. Excellent, and for B4', we can say P = open (A,B) and Q = \X. Between A X B: let IN_Interval = thm `; ! A B X. X IN open (A,B) <=> Between A X B by Interval_DEF, IN_ELIM_THM, REWRITE_TAC`;; Is there any easy fix for this? Freek noticed that REWRITE_TAC often improved speed. I think you're saying that I'm not really having a set theory problem, but that set theory often involves |- !x. P[x] <=> Q[x]. The description of HOL in the Logic manual is based on a formal semantics inside set theory, developed by Andy Pitts. I see Andy wrote a paper with your advisor The HOL Logic and System but I can't find a pdf for it. Should I read that? While this might be considered the ultimate reference, I'm not sure that it's necessarily the easiest place to start, even for a mathematician, if you want a satisfying intuitive understanding of the logic. That's been my experience, but I think my problem is that the stuff I don't know is assumed to be already understood. Math papers of course always have this problem. My own (perhaps unhelpful) point of view is that if you think of types as nonempty sets, you can pretty much read statements at face value with the ordinary mathematical sense of "->" as function space etc. That's helpful and how I think of it, and I learned it from your tutorial. But I'd like to really understand. I want to explain this to my math audience, who all understand ZFC. Greenberg e.g. posted very literate math logic in his recent Amer Math Monthly survey http://www.jstor.org/stable/10.4169/000298910X480063 What confuses me is that I understand how a computer can verify FOL proofs, or even construct them, so if we use ZFC, we can do modern math on computers. I want to understand the analogous picture with HOL. And I can't even imagine how a computer can do HOL if it's not using axioms with something very much like FOL! It isn't that I like ZFC, and as Rob pointed out, I'd never understood the F part, the replacement axiom. It's just something I was taught in math classes. I admit that polymorphic type variables slightly spoil this naive picture. And I'm using that from sets.ml, and even wrote some of my own: let union = new_definition `! s t:A->bool. s union t = \ x. x IN s \/ x IN t`;; let union_SUBSET = thm `; let s t u be A->bool; thus s union t SUBSET u <=> s SUBSET u /\ t SUBSET u by union, SUBSET, IN, BETA_THM`;; I'm certainly happy with polymorphic Scheme code (map etc)! And I don't see the problem with your naive picture: A is any set. I don't think the correspondence between everyday informal mathematics and HOL is any more complicated than that between informal mathematics and ZF set theory. Great, and as Paul Halmos's book Naive Set Theory explains, hardly any mathematicians understand how to use ZFC to construct the real numbers and prove its basic properties. So I don't insist on understand HOL any better than I already understand ZFC :) Yes, that's correct. This proof doesn't look very much like a normal axiomatic one: first it proves that cos(angle_sum) = -1 Thanks, and I haven't figured out your proof of this yet. I do think this is obvious for right triangles, because the sine & cosine of the two non-right angles are transposed, and that must prove, by your calculus definition of angles, that they're complementary. I just understood something related to this that's been bugging me for a while: Trig is based on the arc-length integral definition of angle measures, but we don't actually know that the arc-length integral measures the arc length! We don't have any other definition of arc length besides the integral. For integrals calculating the area under the curve, there's no such problem, because the upper and lower sums coincide if the function is integrable, so the integral must be the area. With arc-length integrals, there's no upper and lower sum. So Trig is based on a Calculus formula that we think, but don't know, measures arc length. But this isn't really a problem, because Greenberg, Moise & Venema's axioms for angle measures just requires there be some function mu that satisfies some properties, most importantly mu(AOB) = mu(AOG) + mu(GOB) if G is in the interior of angle AOB. Well, the arc-length integral gives you that! It doesn't matter if mu(AOB) is "really" the length of the arc swept out by angle AOB in a unit circle centered at O. We get the mu additivity from integral manipulations. I'm still a long way from understanding your proof, but it's a start :) -- 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
