Freek, I just caught myself making a big inference leap that I didn't intend.
The line below
F NOTIN l [notFl] by l_line, Distinct, I1, Collinear_DEF, Fexists,
NOTIN;
is a bug on my part. I meant to write
F NOTIN l [notFl] by l_line, Cl, Collinear_DEF, -, NOTIN;
Miz3 justified my first buggy line with a 547,963 MESON solved at number, and
it took me a while to see how MESON did it. Here's the miz3 proof of an easy
result, Euclid's Proposition I.11: you can push a perpendicular off a line:
let EuclidProp11_THM = thm `;
let A B be point;
assume ~(A = B) [notAB];
thus ? F. Right (angle A B F)
proof
consider l such that
Line l /\ A IN l /\ B IN l [l_line] by notAB, I1;
consider C such that
B IN open (A,C) /\ seg B C === seg B A [ABC] by notAB, SEGMENT,
C1OppositeRay_THM;
C IN l [Cl] by l_line, -, BetweenLinear_THM;
~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C [Distinct] by ABC,
B1';
seg B A === seg B C [BAeqBC] by -, SEGMENT, ABC, C2Symmetric;
consider F such that
~Collinear A F C /\ seg F A === seg F C [Fexists] by Distinct,
IsoscelesExists_THM;
F NOTIN l [notFl] by l_line, Distinct, I1, Collinear_DEF, Fexists,
NOTIN;
~Collinear B F A /\ ~Collinear B F C [BFAncol] by l_line, Cl, Distinct,
I1, Collinear_DEF, -, NOTIN;
~Collinear A B F /\ Angle (angle A B F) [angABF] by -,
CollinearSymmetry_THM, ANGLE;
angle A B F Suppl angle F B C [ABFsuppl] by -, ABC,
SupplementaryAngles_DEF;
~(B = F) by l_line, notFl, NOTIN;
seg B F === seg B F by -, SEGMENT, C2Reflexive;
B,F,A cong B,F,C by BFAncol, -, BAeqBC, Fexists, SSS_THM;
angle A B F === angle F B C by -, TriangleCong_DEF, AngleSymmetry_THM;
qed by angABF, ABFsuppl, -, RightAngle_DEF`;;
All I needed was to say that A, F & C are noncollinear (Fexists), so there
can't be any line containing the three (Collinear_DEF) A & C already belong to
l (l_line, Cl), so if F belongs to l as well, A, F & C would be collinear, and
that's a contradiction. MESON does such proofs by contradiction just fine.
That's the line I should have written:
F NOTIN l [notFl] by l_line, Cl, Collinear_DEF, -, NOTIN;
But I wrote buggily
F NOTIN l [notFl] by l_line, Distinct, I1, Collinear_DEF, Fexists,
NOTIN;
I think I see how miz3 get a proof out of this nonsense I wrote:
A & B are distinct points on l (l_line, Distinct), and so there is only one
line containing A & B (I1). Since
A, B & C are collinear (Distinct), C must belong to this line l as well
(Collinear_DEF), and now we can use the proof I meant above. Maybe this leap
isn't that huge. But I certainly didn't intend it, and it took me a while to
figure out how miz3 could have made sense of it.
--
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
