Here's a bug report on a miz3 inference error I wish miz3 had avoided (code included below). I think it's a serious set theory problem.
I define a predicate angle A O B P and use it as set theoretically as P IN angle A O B. 4 times in my miz3 Hilbert axiomatic geometry code http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar I have to insert an extra line reminding miz3 that A O B P means the same thing as P IN angle A O B, as in AngleKludgeWorks_THM below, rather than just putting IN in the by list as in AngleShorterWorks_THM below, where I only use part of the angle def. If I don't insert the extra line, I get an inference error as in AngleInferenceError_THM. I use the set theoretic idiom P IN angle A O B 66 times in my 1900- lines of miz3 Hilbert code,So I don't think I'm making a dumb mistake. A similar set theoretic stunt with ray (P IN ray O Q: 47 times) works without any trouble. I'm guessing the problem is simply that InteriorAngle_DEF is longer than Ray_DEF. -- Best, Bill (* Paste in these 5 commands, in two pastes, with a RET in between. cd ~/hol_light ocaml #use "hol.ml";; #load "unix.cma";; loadt "miz3/miz3.ml";; AngleKludgeWorks_THM works fine, but AngleInferenceError_THM gets an #1 inference error after the InteriorAngle_DEF line. A shortened version of AngleInferenceError_THM, AngleShorterWorks_THM, works fine. *) horizon := 0;; new_type("point",0);; new_type_abbrev("point_set",`:point->bool`);; new_constant("Between",`:point#point#point->bool`);; new_constant("===",`:point#point->point#point->bool`);; new_constant("Line",`:point_set->bool`);; parse_as_infix("===",(12, "right"));; parse_as_infix("cong",(12, "right"));; parse_as_infix("same_side",(12, "right"));; let Interval_DEF = new_definition `! A B X. open (A,B) X <=> Between (A,X,B)`;; let Collinear_DEF = new_definition `Collinear A B C <=> ? l. Line l /\ A IN l /\ B IN l /\ C IN l`;; let SameSide_DEF = new_definition `A,B same_side l <=> Line l /\ ~(? X. (X IN l) /\ X IN open (A,B))`;; let InteriorAngle_DEF = new_definition `! A O B P. angle A O B P <=> ~Collinear A O B /\ ? a b. Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\ ~(P IN a) /\ ~(P IN b) /\ P,B same_side a /\ P,A same_side b`;; let AngleKludgeWorks_THM = thm `; let A O B P be point; assume P IN angle A O B [ P_AOB]; thus P = P proof angle A O B P by P_AOB, IN; consider alpha beta such that ~Collinear A O B /\ Line alpha /\ O IN alpha /\ A IN alpha /\ Line beta /\ O IN beta /\B IN beta /\ ~(P IN alpha) /\ ~(P IN beta) /\ P,B same_side alpha /\ P,A same_side beta [exists] by -, InteriorAngle_DEF; qed by -`;; let AngleInferenceError_THM = thm `; let A O B P be point; assume P IN angle A O B [ P_AOB]; thus P = P proof consider alpha beta such that ~Collinear A O B /\ Line alpha /\ O IN alpha /\ A IN alpha /\ Line beta /\ O IN beta /\B IN beta /\ ~(P IN alpha) /\ ~(P IN beta) /\ P,B same_side alpha /\ P,A same_side beta [exists] by P_AOB, IN, InteriorAngle_DEF; qed by -`;; let AngleShorterWorks_THM = thm `; let A O B P be point; assume P IN angle A O B [ P_AOB]; thus P = P proof consider alpha beta such that ~Collinear A O B /\ Line alpha /\ O IN alpha /\ A IN alpha /\ Line beta /\ O IN beta /\B IN beta /\ ~(P IN alpha) /\ ~(P IN beta) by P_AOB, IN, InteriorAngle_DEF; qed by -`;; ------------------------------------------------------------------------------ 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
