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

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

Hi,

I agree with Freek. I do not see any need to keep this restriction.
Linking to last seems to be quite natural and such convension
is applied in Mizar everywhere else.
It will fit also to other convention that "then" before
iterative equality concerns only the first of equalities.

Freek, "ex x st P x & Q x" should be on the list of
possibilities insead of 1. It is what must be justified
in "by" after consider.

Grzegorz

Freek Wiedijk wrote:
> 
> Hello,
> 
> I have a strong wish for a change in the Mizar language.
> I wonder what the people here think about it.
> 
> 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