John & Freek, I have miz3 comments, based on John's miz3 axiom port of
my Tarksi geometry code, below. It would be great to write good miz3
dox, because there are no good Mizar dox. Maybe I can help.
********************************
A misfeature of my Mizar code was duplicating the thm assumptions at
the top of the proof. 1201.3601v2.pdf had a way to avoid that:
let CongruenceDoubleSymmetry_THM = thm `;
let a b c d be point;
assume a,b === c,d [H1];
thus b,a === d,c
proof
b,a === a,b /\ c,d === d,c [X1] by H1, A1;
a,b === d,c by H1, X1, EquivTransitive;
qed by -, X1, EquivTransitive`;;
I also used Freek's qed feature to get rid of a useless line.
Improvements like this are really important to pull kids in.
********************************
I'd like a Mizar feature which reduces duplication. In miz3 we write
? x . Between (b,x,b) /\ Between (a,x,a) by -, H1, A7;
consider x such that
Between (b,x,b) /\ Between (a,x,a) [X1];
But in Mizar we can also write more simply
consider x such that
Between (b,x,b) /\ Between (a,x,a) by -, H1, A7 [X1];
********************************
If a statement has a label, the label must precede `by ...' I don't
know where this is explained, and it seems to be contradicted on p 17:
The labels are behind the statements in brackets, instead of in front
with a colon.
This caused me a lot of trouble, but I would have known if I'd read
Freek's examples, as the correct behavior is showne.g. on p 13:
consider x such that ~P x [3] by 2;
take x;
assume P x [4];
F [5] by 3,4;
thus !y. P y [6] by 5;
********************************
I'd prefer statement labels at the beginning of a line, as in Mizar.
That seems more readable, and in the tradition of 2-column proofs.
********************************
On p 17 of 1201.3601v2.pdf, Freek writes
The label `-' refers to the previous statement. Also, the last
‘horizon’ statements are visible without reference, where horizon is
a variable of the miz3 server that is usually set to 1.
That seems to mean that the previous statement is always visible, and
that we never need `-'. I want to need a `-' to refer to the previous
statement, so (this works fine so far) I set
horizon := 0;;
but it makes the there-exists/consider even more cluttered:
? x . Between (a,c,x) /\ c,x === c,d by A4;
consider x such that
Between (a,c,x) /\ c,x === c,d [X1] by -;
********************************
I think the miz3 error message are not nearly as good as the Mizar
error message, which are often baffling, but obey one principle: on
the first offending line, there is an error message, and it's indented
to mark the offending expression. I don't have a good example yet.
I have a serious problem the miz3 error message aren't helping me fix,
but that requires the Tarski code, so I'll write a separate message.
********************************
Freek's `cases' discussion does not point out that in sufficiently trivial
cases, no `by' is needed, as in
let B124and234Ordered_THM = thm `;
! a b c d .
Between (a,b,d) /\ Between (b,c,d) ==> is_ordered (a,b,c,d)
proof
let a b c d be point;
assume Between (a,b,d) [H1];
assume Between (b,c,d) [H2];
cases;
suppose b = c [P1];
Between (a,b,c) [P2] by -, Bqaa_THM;
Between (a,c,d) by P1, H1;
thus is_ordered (a,b,c,d) by P2, H1, -, H2, is_ordered_DEF;
end;
suppose ~(b = c) [Q1];
Between (a,b,c) by H1, H2, B124and234then123_THM;
thus is_ordered (a,b,c,d) by -, Q1, H2, BTransitivityOrdered_THM;
end;
end`;;
--
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
