John & Freek, I found a real bug (the code below), an inference error that miz3 should report but does not. I think miz3 calculates some result ~(A = B), but the `by' mechanism malfunctions, as ~(A = B) is used even though it's not given by a `by' justification.
BTW I've formalized my Hilbert geometry axiom paper http://www.math.northwestern.edu/~richter/hilbert.pdf up through Lemma 4.8 (1200 lines of code) http://www.math.northwestern.edu/~richter/OpenIntervalHilbertAxiom.ml and I'm amazed at how well miz3 is working. This is the only serious bug I've found, as opposed to additional features I'd like. -- Best, Bill new_type("point",0);; new_type_abbrev("point_set",`:point->bool`);; new_constant("Line",`:point_set->bool`);; let Collinear_DEF = new_definition `Collinear (A,B,C) <=> ?l. Line l /\ A IN l /\ B IN l /\ C IN l`;; let I1 = new_axiom `!A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;; let I3 = new_axiom `?A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear (A,B,C)`;; let OnePointImpliesAnother_THM = thm `; let P be point; thus ?Q:point. ~(Q = P) proof consider A B C such that ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear (A,B,C) [X1] by I3; cases; suppose B = P; ~(A = B) by -, X1; qed by -; suppose ~(B = P); qed by -; end`;; let NonCollinearImpliesDistinct_THM = thm `; let A B C be point; assume ~Collinear (A,B,C) [H1]; thus ~(A = B) /\ ~(A = C) /\ ~(B = C) proof cases; suppose A = B /\ B = C [C1]; consider Q such that ~(Q = A) by OnePointImpliesAnother_THM; consider l such that Line l /\ A IN l /\ Q IN l by -, I1; Collinear (A,B,C) by -, C1, Collinear_DEF; qed by -, H1; suppose ~(A = B) /\ B = C [C2]; consider l such that Line l /\ A IN l /\ B IN l by -, I1; Collinear (A,B,C) by -, C2, Collinear_DEF; qed by -, H1; suppose ~(B = C) [C3]; consider l such that Line l /\ B IN l /\ C IN l [X1] by C3, I1; ~(A = B) [U] proof assume A = B; Collinear (A,B,C) by -, X1, Collinear_DEF; qed by -, H1; ~(A = C) [V] proof assume A = C; Collinear (A,B,C) by -, X1, Collinear_DEF; qed by -, H1; qed by U, V, C3; end`;; (* This next proof works fine, and this shows a bug in miz3. I should have gotten a #1 inference error on line 2 of the proof. Line p should not exist, as Distinct does not include ~(A = B), even though this was calculated to be true by NonCollinearImpliesDistinct_THM *) let I1bug_THM = thm `; let A B C be point; assume ~Collinear (A,B,C) [H1]; thus A = A proof ~(B = C) [Distinct] by H1, NonCollinearImpliesDistinct_THM; consider p such that Line p /\ B IN p /\ A IN p by Distinct, I1; qed by -`;; (* this of course doesn't work *) let I1not_bug_THM = thm `; let A B C be point; thus A = A proof consider p such that Line p /\ B IN p /\ A IN p by I1; 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
