[mizar] Strong Mizar wish: linking to consider

[Freek Wiedijk <freek@cs.kun.nl>]

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