Re: Syntax change to scheme proposal

Hello,

Quoting "Alex Nelson  thmprover _AT_ gmail.com"  
<[email protected]>:

> 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: [email protected]
Ciolkowskiego 1M, 15-245 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
===========================================================================