Freek, I have two new bug reports, but first:
And in miz3 you should write it just like that! Why do you think
you have to use the more convoluted route?
Thanks, and you're right, the simple Mizar consider syntax works fine
in miz3. That really helps my code. My guess is that I was making so
many miz3 errors that I didn't isolate which problem I was having.
BUG1) I always get miz3 error messages if I put a comment line in the
middle of a proof. I'll explain this below.
BUG2) In the following proof that had a ton of mistakes (correct code
below), miz3 only flagged non-errors:
let FlatNormal_THM = thm `;
let a b c d d' e be point;
assume Between (b,c,d') [H1];
assume Between (d,e,d') [H2];
assume c,d' === c,d [H3];
assume d,e === d',e [H4];
assume ~(c = d) [H5];
assume ~(e = d) [H6];
thus
? p,r,q . 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
proof
~(c = d') by H5, H3, EquivSymmetric A3;
? p r . Between (e,c,p) /\ Between (d',c,r) /\ p,r,c cong d',e,c by
EasyAngleTransport;
consider p r such that
Between (e,c,p) /\ Between (d',c,r) /\ p,r,c cong d',e,c [X1] by -;
p,r === d',e /\ p,c === d',c /\ r,c === e,c [X2] by -, X1 cong_DEF;
d',e === d,e by H4 EquivSymmetric;
p,r === d,e [X3] by -, X2, EquivTransitive;
~(p = r) [X4] by -, EquivSymmetric, H6, A3;
consider q such that
Between (p,r,q) /\ r,q === e,d [X5] by A4;
Between (d',e,d) [X6] by H2, Bsymmetry_THM;
c,p === c,d' by -, X2, CongruenceDoubleSymmetry_THM;
c,p === c,d [X7] by -, H3, EquivTransitive;
:: Apply SAS to p+crq ∧ d'+ced
c,q=== c,d by X4, X1, X5, X6, A5;
c,d=== c,q by -, EquivSymmetric;
c,p=== c,q [X8] by -, X7, EquivTransitive;
r,c=== r,c [X9] by EquivReflexive;
r,p=== e,d [X10] by X3, CongruenceDoubleSymmetry_THM;
e,d=== r,q by X5, EquivSymmetric;
r,p=== r,q by -, X10, EquivTransitive;
r,c,p cong r,c,q [X11] by -, X9, X8, cong_DEF;
Between (r,c,d') [X12] by -, X1, Bsymmetry_THM;
qed by -, X5, X11, X12, X2, X1, X3`;;
The useless-to-me error message was
Exception:
Mizar_error
(`;
let a b c d d' e be point;
assume Between (b,c,d') [H1];
assume Between (d,e,d') [H2];
:: #3
:: 3: skeleton error
assume c,d' === c,d [H3];
:: #3
assume d,e === d',e [H4];
:: #3
assume ~(c = d) [H5];
:: #3
assume ~(e = d) [H6];
:: #3
thus
? p,r,q . 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
:: #8
:: 8: syntax or type error hol
The #3 and #8 errors in the statement of the lemma look wrong, and I
never changed the statement. Here's the correction, except for the
offending comment line:
let FlatNormal_THM = thm `;
let a b c d d' e be point;
assume Between (b,c,d') [H1];
assume Between (d,e,d') [H2];
assume c,d' === c,d [H3];
assume d,e === d',e [H4];
assume ~(c = d) [H5];
assume ~(e = d) [H6];
thus ? p r q .
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
proof
~(c = d') by H5, H3, EquivSymmetric, A3;
consider p r such that
Between (e,c,p) /\ Between (d',c,r) /\ p,r,c cong d',e,c [X1] by
-, EasyAngleTransport_THM;
p,r === d',e /\ p,c === d',c /\ r,c === e,c [X2] by -, X1, cong_DEF;
d',e === d,e by H4, EquivSymmetric;
p,r === d,e [X3] by -, X2, EquivTransitive;
~(p = r) [X4] by -, EquivSymmetric, H6, A3;
consider q such that
Between (p,r,q) /\ r,q === e,d [X5] by A4;
Between (d',e,d) [X6] by H2, Bsymmetry_THM;
c,p === c,d' by -, X2, CongruenceDoubleSymmetry_THM;
c,p === c,d [X7] by -, H3, EquivTransitive;
(* In proof below, Apply SAS to p+crq /\ d'+ced *)
c,q=== c,d by X4, X1, X5, X6, A5;
c,d=== c,q by -, EquivSymmetric;
c,p=== c,q [X8] by -, X7, EquivTransitive;
r,c=== r,c [X9] by EquivReflexive;
r,p=== e,d [X10] by X3, CongruenceDoubleSymmetry_THM;
e,d=== r,q by X5, EquivSymmetric;
r,p=== r,q by -, X10, EquivTransitive;
r,c,p cong r,c,q [X11] by -, X9, X8, cong_DEF;
Between (r,c,d') [X12] by X1, Bsymmetry_THM;
qed by -, X5, X11, X12, X2, X1, X3`;;
Here's the miz3 error message:
(* In proof below, Apply SAS to p+crq /\ d'+ced *)
c,q=== c,d by X4, X1, X5, X6, A5;
:: #8 #8
:: 8: syntax or type error hol
c,d=== c,q by -, EquivSymmetric;
c,p=== c,q [X8] by -, X7, EquivTransitive;
r,c=== r,c [X9] by EquivReflexive;
r,p=== e,d [X10] by X3, CongruenceDoubleSymmetry_THM;
e,d=== r,q by X5, EquivSymmetric;
r,p=== r,q by -, X10, EquivTransitive;
r,c,p cong r,c,q [X11] by -, X9, X8, cong_DEF;
Between (r,c,d') [X12] by X1, Bsymmetry_THM;
qed by -, X5, X11, X12, X2, X1, X3
;
::#9#3
:: 9: syntax error mizar
:: 3: skeleton error
`,
(4, 0, 0)).
And I easily fix this by moving the comment line above the lemma:
(* In proof below, Apply SAS to p+crq /\ d'+ced *)
let FlatNormal_THM = thm `;
let a b c d d' e be point;
assume Between (b,c,d') [H1];
assume Between (d,e,d') [H2];
assume c,d' === c,d [H3];
assume d,e === d',e [H4];
assume ~(c = d) [H5];
assume ~(e = d) [H6];
thus ? p r q .
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
proof
~(c = d') by H5, H3, EquivSymmetric, A3;
consider p r such that
Between (e,c,p) /\ Between (d',c,r) /\ p,r,c cong d',e,c [X1] by
-, EasyAngleTransport_THM;
p,r === d',e /\ p,c === d',c /\ r,c === e,c [X2] by -, X1, cong_DEF;
d',e === d,e by H4, EquivSymmetric;
p,r === d,e [X3] by -, X2, EquivTransitive;
~(p = r) [X4] by -, EquivSymmetric, H6, A3;
consider q such that
Between (p,r,q) /\ r,q === e,d [X5] by A4;
Between (d',e,d) [X6] by H2, Bsymmetry_THM;
c,p === c,d' by -, X2, CongruenceDoubleSymmetry_THM;
c,p === c,d [X7] by -, H3, EquivTransitive;
c,q=== c,d by X4, X1, X5, X6, A5;
c,d=== c,q by -, EquivSymmetric;
c,p=== c,q [X8] by -, X7, EquivTransitive;
r,c=== r,c [X9] by EquivReflexive;
r,p=== e,d [X10] by X3, CongruenceDoubleSymmetry_THM;
e,d=== r,q by X5, EquivSymmetric;
r,p=== r,q by -, X10, EquivTransitive;
r,c,p cong r,c,q [X11] by -, X9, X8, cong_DEF;
Between (r,c,d') [X12] by X1, Bsymmetry_THM;
qed by -, X5, X11, X12, X2, X1, X3`;;
miz3 tells it's correct, returning
val ( FlatNormal_THM ) : thm =
|- !a b c d d' e.
Between (b,c,d')
==> Between (d,e,d')
==> c,d' === c,d
==> d,e === d',e
==> ~(c = d)
==> ~(e = d)
==> (?p r q.
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)
--
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
