Hi Bill,
First a reply to your other mail:
>I can't understand what's wrong with this proof below. This is the
>only thm I wrote where the conclusion is there-exists statement, and
>I'm guessing that's the problem.
Nah, there's nothing special about that.
>The to-me incomprehensible Mizar_error:
>
> (`;
> ! a o b . (~(o = a) ==>
(? x y . (Between (b,o,x) /\ Between (a,o,y) /\ (x,y,o cong a,b,o))))
> :: #8
> :: 8: syntax or type error hol
It says "syntax or type error hol", so it's a HOL syntax
or type error :-) If you copy-paste the statement into
the HOL session, you indeed get:
# `! a o b . (~(o = a) ==>
(? x y . (Between (b,o,x) /\ Between (a,o,y) /\ (x,y,o cong a,b,o))))`;;
Exception: Noparse.
This error has nothing to do with miz3, but with the fact
that in HOL Light you aren't allowed to use the variable
name "o". The constant "o" already is an infix operator.
You write "f o g" for the composition of functions:
# `o`;;
Warning: inventing type variables
val it : term = `(o)`
# type_of it;;
val it : hol_type = `:(?88022->?88024)->(?88023->?88022)->?88023->?88024`
Therefore, already "o = a" is a HOL syntax error:
# `o = a`;;
Exception: Noparse.
And then this mail:
>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];
And in miz3 you should write it just like that! Why do you
think you have to use the more convoluted route? The "by"
justification for the ?... statement and the one for the
consider have to justify exactly the same statements.
I don't understand this point.
>********************************
>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.
The statement _to me_ is the HOL formula, not the whole
"proof step". I don't see why this quote from me is wrong.
The label _is_ right behind the "statement"!
>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.
The reason I replaced the "then" with the "by -",
and put the labels behind the statements (ahem), is
because I wanted to have the part of the proof step
that belongs to the "Formal Proof Sketch" of the thing
(see <http://www.cs.ru.nl/~freek/pubs/sketches2.pdf>),
to be all in front of the part that doesn't belong there.
Labels and references (which "then" implicitly is) don't
belong in a Formal Proof Sketch, so should be at the end.
(By the way, please don't refer to Formal Proof Sketches
as "proof sketches". I feel strongly that they should
be called _formal_ proof sketches. They have a notion of
correctness that's _formal,_ even if it's undecidable.)
Also, I thought at some point that it was a bit easier to
shallowly parse proof steps with the bracketed label syntax.
However, that's probably not true. miz3 is quite close
to John's original Mizar mode - apart from the "tactics in
justifications" and "automatically growing the proof parts -
and John _did_ have the thens and the labels in Mizar style.
Still, I certainly won't change the syntax. And I even
less would like to allow both label styles simultaneously.
Furthermore, I don't know what "2-column proofs" are, sorry.
Is there a separate column for the labels?
>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 -;
Again, _if_ you write it like this the "by -" seems to
belong in it? But, again, there is no reason at all to
write it like this.
>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 try to obey the same principle. However, error recovery
probably is less developed than in the real Mizar system.
Also, with HOL syntax errors, I don't get good information
for positioning the error message. (I think that the miz3
error messages should be seen as firmly in the HOL Light
error message tradition :-))
>Freek's `cases' discussion does not point out that in
>sufficiently trivial cases, no `by' is needed.
A "by" without labels is always implicit. So if the
automated prover can prove something without references, then
yes, indeed no "by" is needed. But this is not specific to
"cases".
If you do the same thing with the "cases" as you did with
the "consider", your proof would look like:
b = c \/ ~(b = c); :: this is provable without references,
:: hence no "by" is needed
cases by -;
suppose b = c [P1];
...
suppose ~(b = c) [Q1];
...
But, just like with the "consider", miz3 synthesizes the
proof obligation for you, and having a separate statement
in front of it is not needed at all.
Freek
------------------------------------------------------------------------------
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
