Freek, I successfully ported my 120 line Mizar proof of Gupta's
theorem to miz3! That's a tribute to miz3 and its error messages, as
I got a lot of them, and the errors showed me how to debug my code.
But the first error messages I got didn't help me at all, and the 2nd
one seems erroneous.
I pasted in the following 120 line proof, and got only one error
message:
Exception: Failure "term_of_now".
The problem was that on line 70, I had a
~(e = c) [U1];
which should have read
~(e = c) [U1]
as it is a statement I'm about to prove.
After a few fixes, I got the error
cases;
:: #1
:: 1: inference error
suppose ~(e = c);
qed by -;
:: #9
:: 9: syntax error mizar
suppose e = c [U2]
c' = e by U2, Z4, EquivSymmetric, A3;
:: #9
You can clearly see my error:
suppose e = c [U2]
needs a ;
but nothing else here is wrong, and #1 and #9 are on different lines.
After those two baffling error messages, the error messages got a lot
clearer, and I finished debugging it (correction in my earlier post).
let Gupta_THM = thm `;
let a b c d be point;
assume ~(a = b) [H1];
assume Between (a,b,c) [H2];
assume Between (a,b,d) [H3];
thus Between (b,d,c) \/ Between (b,c,d)
proof
cases;
suppose b = c \/ b = d \/ c = d;
Between (b,d,c) \/ Between (b,c,d) by -, Baaq_THM, Bqaa_THM;
end;
suppose ~(b = c) /\ ~(b = d) /\ ~(c = d) [H4];
assume ~ Between (b,d,c) [H5];
consider d' such that
Between (a,c,d') /\ c,d' === c,d [X1] by A4;
consider c' such that
Between (a,d,c') /\ d,c' === c,d [X2] by A4;
is_ordered (a,b,c,d') by H2, X1, B123and134Ordered_THM;
Between (a,b,d') /\ Between (b,c,d') [X3] by -, is_ordered_DEF;
is_ordered (a,b,d,c') by H3, X2, B123and134Ordered_THM;
Between (a,b,c') /\ Between (b,d,c') [X4] by -, is_ordered_DEF;
~(c = d') [X5] by X1, H4, A3, EquivSymmetric;
~(d = c') [X6] by X2, H4, A3, EquivSymmetric;
~(b = d') [X7] by X3, H4, A6;
~(b = c') [X8] by X4, H4, A6;
consider u such that
Between (c,d',u) /\ d',u === b,d [Y1] by A4;
is_ordered (b,c,d',u) by X5, X3, Y1 BTransitivityOrdered_THM;
Between (b,c,u) /\ Between (b,d',u) [Y2] by -, is_ordered_DEF;
consider b' such that
Between (d,c',b') /\ c',b' === b,c [Y3] by A4;
is_ordered (b,d,c',b') by X6 X4 Y3 BTransitivityOrdered_THM;
Between (b,d,b') /\ Between (b,c',b') [Y4] by -, is_ordered_DEF;
Between (c',d,b) [Y5] by X4, Bsymmetry_THM;
d,c' === c',d /\ b,d === d,b [Y6] by A1;
c,d === d,c' by X2, EquivSymmetric;
c,d' === d,c' by -, X1, EquivTransitive;
c,d' === c',d [Y7] by -, Y6 EquivTransitive;
d',u === d,b by Y1, Y6, EquivTransitive;
c,u === c',b [Y8] by -, Y1, Y5, Y7, SegmentAddition_THM;
c',b' === b',c' /\ b',b === b,b' [Y9] by A1;
b,c === c',b' by Y3 EquivSymmetric;
b,c === b',c' [Y10] by -, Y9 EquivTransitive;
Between (b',c',b) by Y4, Bsymmetry_THM;
b,u === b',b by -, Y2, Y10, Y8, SegmentAddition_THM;
b,u === b,b' [Y11] by -, Y9, EquivTransitive;
is_ordered (a,b,d',u) [Y12] by X7, X3, Y2, BTransitivityOrdered_THM;
is_ordered (a,b,c',b') by X8, X4, Y4, BTransitivityOrdered_THM;
Between (a,b,u) /\ Between (a,b,b') by -, Y12, is_ordered_DEF;
u = b' [Y13] by -, H1, Y11, C1_THM;
c',b === c,b' by Y13, Y8, EquivSymmetric;
b,c' === b',c [Z1] by -, CongruenceDoubleSymmetry_THM;
c,c' === c',c by A1;
b,c,c' cong b',c',c [Z2] by -, Y10, Z1, cong_DEF;
Between (b',c',d) by Y3, Bsymmetry_THM;
c',d' === c,d [Z3] by -, H4, Z2, X3, Y7, A5;
d',c' === c',d' by A1;
d',c' === c,d by -, Z3, EquivTransitive;
consider e such that
Between (c,e,c') /\ Between (d,e,d') /\ c,e === c',e /\ d,e === d',e
[Z4] by -, X3, X4, X1, X2, RhombusDiagBisect_THM;
~(e = c) [U1];
proof
cases;
suppose ~(e = c);
qed by -;
suppose e = c [U2]
c' = e by U2, Z4, EquivSymmetric, A3;
c' = c by -, U2;
Between (b,d,c) [U3] by -, X4;
F by -, U3, H5;
qed by -;
end;
e = d [V1];
proof
cases;
suppose e = d;
qed by -;
suppose ~(e = d) [V2];
consider p r q such that
Between (p,r,q) /\ Between (r,c,d') /\ Between (e,c,p) /\
r,c,p cong r,c,q /\ r,c === e,c /\ p,r === d,e [W1]
by X3, Z4, X1, H4, V2, FlatNormal;
r,p === r,q /\ c,p === c,q [W2] by W1, cong_DEF;
~(c = r) by W1 U1 EquivSymmetric, A3;
d',p === d',q [W3] by -, W1, W2, EqDist2PointsBetween_THM;
Between (c,d',b') by Y1, Y13;
b',p === b',q [W4] by -, X5, W2, W3, EqDist2PointsBetween_THM;
Between (d',c,b) by X3 Bsymmetry_THM;
b,p === b,q [W5] by -, X5, W3, W2, EqDist2PointsBetween_THM;
c',p === c',q [W7]by Y4 W4 W5 EqDist2PointsInnerBetween_THM;
Between (c',e,c) by Z4, Bsymmetry_THM;
is_ordered (c',e,c,p) by -, U1, W1, BTransitivityOrdered_THM;
Between (c',c,p) [W8] by -, is_ordered_DEF;
~(c' = c) by Z4 U1 A6;
p,p === p,q by -, W8, W7, W2, EqDist2PointsBetween;
q = p by EquivSymmetric, A3;
p = r by -, W1 A6;
e = d [W9] by -, W1 EquivSymmetric A3;
F by -, W9, V2;
qed by -;
end;
d' = e by V1, Z4, EquivSymmetric, A3;
d' = d by -, V1; thus
Between (b,c,d) by X3;
end;
end`;;
------------------------------------------------------------------------------
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
