Re: [mizar] be and being

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Wed, 17 Dec 2003, Piotr Rudnicki wrote:

> Pity that Freek did not include in his comparison some other proof
> helpers.  These days my favourite proof helper is "Algebra' by
> MacLane and Birkhoff where the claims are written in this way (just a
> few samples of theorems but they are consistent throughout)
> 
>    - For n x n matrices B and A over K, |BA| = |B| |A|
> 
>    - ... for each scalar k there is exactly one n-linear 
>      form d_: (K^n)^n -> Kwith d_k(I) = k
> 
>    - Let L be any complete lattice, and let S be any subset of L
>      such that (i) I in S, and (ii) T c< S implies inf T in S.  Then
>      S is a complete lattice.
> 
>    - For each ideal A in a ring R there are unique binary operations of
>      addition and multiplication on the quotient set R/A which ...
> 
> There is a lot of "let ... be ..." in this book but I have not seen
> a single "being".


It is off-topic but interesting that after "for" (or rather "for each") 
they first write the type (quite consequently). So in Mizar, that would 
mean allowing something like:

for real number x,y holds ...     ; or even if the plural is allowed:

for real numbers x,y holds ...   ; 

I quite like it, the problem is  with dependant types, where e.g.

"for Function of X Z  holds ... " is bad and poorly distinguishable from
"for Function of X,Y Z holds ... "

They solve it by using prefix notation for arguments of types:

"for n-Matrix A holds ..." instead of "for Matrix of n A holds ...".

So Mizar would have to allow such "-" type synonyms in additiion to normal 
"of" syntax for dependant types.

Other possibility would be to allow the following syntax:

"for Matrix A of n holds .... ", which also feels quite natural.
 
> All what I propose is a one character alias for 'be' and 'being'.
> Colon ':' should not cause much of a confusion because the context 
> allows for good error recovery.

Also a bit off-topic: there is an abbreviation "bei" for "being" in my 
abbreviation table for Mizar 
(http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/mizarmode/.abbrev_defs?rev=HEAD&content-type=text/vnd.viewcvs-markup 
), so if three characters are too much, something like "bi" or "bg" should 
be also quite nonconflicting.

Best,
Josef