Re: If A=B & (A contains C), why mizar doesn't infer (B contains C)

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Josef Urban wrote:

> There is practically no sense in having fictitious variables in loci (I
> can think of a very hypothetical case, when e.g. the type "Element of X"
> is needed, but we don't care at all about X (it is fictitious)).
> But once we have them, why not handle them the same way as superfluous
> variables in redefinitions, or at least warn the user (or both)?

Actually the Result Type (the Mother Ttype in the case of a mode) IS a part of
the definition. When we implemented the "commutativity" condition Grzegorz
almost immediately found the inconsistency, because the Result Type was not
checked. His example:

definition let a,b be set;
  mode First of a,b means
:D: it = a;
   existence;
end;

definition let a,b be set;
 func a ? b -> First of a,b means
  not contradiction;
 correctness;
 commutativity;
end;

then form "obvious "
1 ? 0 = 0 ? 1
one could infer
0=1

Of course now it is checked.

What to do with fictitious loci? I believe we need a revision program that
removes them. But what to do when fictitious loci are visible. Look to the
example:

definition
let C be non empty set;
let h,g be Membership_Func of C;
let A be FuzzySet of C,h;
let B be FuzzySet of C,g;
pred A=B means
:: FUZZY_1:def 3
for c being Element of C holds h.c = g.c;
end;

What you propose to with this?

> I think the real problem is understanding hidden variables. It is a nice
> feature to have them, and not to have to mention all of the "implicit
> context" in the notation, but it may be confusing when one is learning
> Mizar. Maybe adding the possibility to view items in the inner cnstructors
> notation (e.g. as in Grzegorz's Encyclopedia) would help this.
>

I am so accustomed to them ... BTW Lego has them, too. Has not?


Greetings,
Andrzej