Re: [mizar] Possible language extension?

[Andrzej Trybulec <trybulec@cs.shinshu-u.ac.jp>]

Dear Freek,

I rather like the idea. Actually, more flexible syntax for theorems had
been discussed, some years ago. Eventually we dropped the subject.

So, we thought about writing theorems in a similar way as you proposed:

theorem
  let x,y,z be point;
  assume ....
.....
  proof
   ...
 end;

the only difference is the place where you put the label, I definitely
want it after 'theorem'.
Observe that such a syntax is used in FM.

Why we have not implemented it? (besides the sloth)

1. In s serious proof the skeleton is a small part of it, e.g. ABIAN:8 -
the has more than 500 lines and maybe 10 lines of the skeleton. An
extreme case : GOBOARD3:1 - the proof is more then 3100 lines and the
skeleton - 1 line ('hence thesis'):-).

2. Some our colleagues complain that Mizar syntax is already too
complicated (I would say sufficiently rich). If I recall Markus Wenzel
calls it 'baroque syntax'.

On the other hand, once we allow Diffuse Statement for a Conclusion, why
not for Theorem,
you of course write that the procedures for Diffuse Statement could be
used.

Anyway, it seems that there are much more urgent changes that must be
done (with Mizar).

All the best
Andrzej

Freek Wiedijk wrote:

> For some time I've been thinking about the following.
> Consider the following theorem:
>
>   theorem Example: P & Q & R implies S & T
>   proof
>    assume
> A1: P;
>    assume
> A2: Q;
>    assume
> A3: R;
>    ...
>   end;
>
> It seems strange to have to write P, Q and R _again_ when you
> just wrote those assumptions in the statement of the theorem.
>
> Now wouldn't it be nice to be able to say:
>
>   theorem
>    assume
> A1: P;
>    assume
> A2: Q;
>    assume
> A3: R;
> Example: S & T
>   proof
>    ...
>   end;
>
> It would match the assumptions in definitions.  Also I think
> I've seen this idiom with "assume" in the statement of a
> theorem in actual mathematical texts.
>
> Would it be hard to implement this?  I guess the machinery
> for diffuse reasoning should help here?
>
> Or is this a silly idea?
>
> Freek