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

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

On Mon, Jun 25, 2001 at 07:53:14PM +0200, Andrzej Trybulec wrote:

> 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.

I tried to play with something like this and here is what I got:

environ

vocabulary TRY, BOOLE;
constructors BOOLE;
notation BOOLE;

begin

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

definition let a,b be set;
 func a ? b -> First of a,b means
  not contradiction;
 existence;
 uniqueness proof
  let it1,it2 be First of a,b such that
   not contradiction and not contradiction;
  thus it1 = a U b by D .= it2 by D;
 end;
 commutativity;
::>          *84
end;

definition let a, b be set;
 redefine func a ? b;
 commutativity proof let a, b be set;
::>          *84
  thus a ? b = a U b by D .= b ? a by D;
 end;
end;

consider a, b being set;

a ? b = b ? a;


How to get rid of that *84 error?

PR