Hello,Quoting "Alex Nelson thmprover _AT_ gmail.com" <owner-mizar-forum@mizar.uwb.edu.pl>:
Right now, the syntax for a scheme looks like:
```
Scheme-Block = "scheme" Scheme-Identifier "{" Scheme-Parameters "}" ":"
Scheme-Conclusion [ "provided" Scheme-Premise { "and" Scheme-Premise } ]
* ( "proof" | ";" )*
Reasoning "end" .
```
I am proposing we change the `( "proof" | ";" )` to just `"proof"`, i.e.,
```
Scheme-Block = "scheme" Scheme-Identifier "{" Scheme-Parameters "}" ":"
Scheme-Conclusion [ "provided" Scheme-Premise { "and" Scheme-Premise } ]
* "proof"*
Reasoning "end" .
```
...or even better...
```
Scheme-Block = "scheme" Scheme-Identifier "{" Scheme-Parameters "}" ":"
Scheme-Conclusion [ "provided" Scheme-Premise { "and" Scheme-Premise } ]
* Proof* .
```
This change adheres to the principle of least surprise: theorems require
either a justification or a `Proof` as a justification, schemes should have
a similar structure (but only `Proof` makes sense, really).
Only two schemes currently do not adhere to this proposed syntax (one in
FIELD_16, another in PRE_CIRC).
And the change requires only minimal changes to the parser.
I wholeheartedly second Alex's proposal (using the 'Proof' non-terminal) as I agree that most users will then find this bit of the Mizar grammar more natural.
Interestingly, since the 1970s the scheme body's syntax ended with the "proof" Reasoning "end" part. But in 2010 Andrzej had the idea that the syntax should better reflect the block-like nature of schemes (like in the case of definitions or notations): the "end" should close the scheme block rather than the scheme's justification and he decided to discard the "proof". The other option, i.e. having two "end"s (one for "scheme" and the other for "proof") was then rejected as rather misleading. Then, some five years later, the syntax was changed to support the optional ( "proof" | ";" ) as some sort of syntactic compromise. And now we seem to be ready for a complete rollover :-)
Adam -- Adam Naumowicz =========================================================================== Division of Programming and Formal Methods Fax: +48(85)738-83-33 Faculty of Computer Science Tel: +48(85)738-83-06 (office) University of Bialystok E-mail: adamn@math.uwb.edu.pl Ciolkowskiego 1M, 15-245 Bialystok, Poland http://math.uwb.edu.pl/~adamn/ ===========================================================================