Re: [mizar] Strong Mizar wish: linking to consider

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

It is not clear to me what are the big savings.  With Freek's proposal
we save one label after conditions provided that we link only
to the last proposition and we never refer to this proposition later.

I may be biased, I do not like "then" at all and am quite happy with
using labels.  The main reason for this is that I cannot decide whether
it is to be placed at the end of a line or at the beginning.

If any enhancements are planned to "then", then I am willing to bribe
someone to allow "then thus".

PR



On Fri, Mar 08, 2002 at 11:41:35AM +0100, Freek Wiedijk wrote:

> Currently it's not possible to say something like:
> 
>   consider x such that
>  A1: P x and
>  A2: Q x by ...;
>   then R x by ...;
> 
> because the "then" is not allowed.  I would very much
> like this to be allowed.  It would save me many labels.
> 
> It might not seem clear what the "then" should link to.
> There are four possibilities:
> 
>   1. "ex x st P x"
>   2. "P x & Q x"
>   3. "P x"
>   4. "Q x"
> 
> I claim that possibility 4 is the natural choice.  (This is
> also the way my "Mizar Light" experiment behaves -- see the
> TPHOLs 2001 proceedings -- without anything special in the
> implementation.)
> 
> Reasons not to want possibility 1 or 2: a "then" replaces
> linking to an explicit label.  There is no way to label these
> statements in the example.
> 
> Reasons not to want possibility 3: "then" links to the latest
> statement.  "P x" comes before "Q x".
> 
> Of course the same wish applies to "let ... such that",
> "assume that", "given" etc.  But with "consider" I _really_
> hate not having it.
> 
> So: who should I bribe to make this change to Mizar? :-)
> 
> Freek

-- 
Piotr Rudnicki               CompSci, Univerity of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr