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

[Josef Urban <urban@mail.kolej.mff.cuni.cz>]

I think it is a good idea, to require that the checker would accept
such inferences. There are some mechanisms in the checker that almost do
this, e.g. if you first defined

definition
 let f, t be set ;
 pred t contains f means
      t c= f;
end;

and then your definition for Subset of tm was only a redefinition, the
inference would be accepted, because in such case the checker knows that
the hidden arguments do not have to agree.
I think it would not be too difficult to implement this "forgetting of
hidden arguments" in general case, not just for redefinitions.

Josef Urban


On Wed, 20 Jun 2001, Chen, Jing Chao (Jing Chao) wrote:

> Recently, I found that the proof of a very simple proposition cannot be
> accpted by Mizar.
> For example
> definition
>  let f, tm be set, t be Subset of tm;
>  pred t contains f means
>       t c= f;
> end;
>
>  for f, tm1 be set, t1 be Subset of tm1,
>  tm2 be set, t2 be Subset of tm2 st
>     t1 contains f & t1=t2 holds t2 contains f;
> ::>                 *4
> This proposition can be simplified into
>    A=B & (A contains C)  => B contains C.
> Clearly, it is ture. However, Mizar presented error 4.
> What deduction mechanism doesn't allow such an inference ?
>
> Jingchao Chen
>
>