Re: [mizar] Contradiction in Mizar 6.3.05

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi,

On Thu, 26 Jun 2003, Piotr Rudnicki wrote:

> One can prove a contradiction in Mizar 6.3.05 but I guess it is not
> a new feature.

It works in 6.3.04 too, but is probably older.
I did not do debugging, just looked at the constructors involved (by using
Constr. Explanations), and the funny thing is:

definition
  let G be finite Graph, n be Nat;
  cluster (DCSeq G).n -> booboo;
  correctness proof
   thus (DCSeq G).n is finite by DCS;
  end;
end;

If you change this to
 cluster (DCSeq G).n -> finite;
Mizar will announce error *115 - Unknown attribute. However, if you change
the redfinition of "." to normal definition - e.g. by 
"  func f.x -> Graph equals f.x;", the error *115 disappears.
So in the cluster pattern, Mizar is looking for nonredefined constructor, 
and only the first "booboo" (not the synonym) matched the typing.

The bad thing is, that despite this "booboo#1" in the pattern, the 
correctness thesis still uses the second - "booboo#2", synonymous to 
"finite". This may be just a simple bug in the analyzer, though parser may 
be involved too.

I think we should really start describing somewhere all the deep 
philosophy behind using redefined and nonredefined versions of 
constructors. This is almost impossible for normal user to understand.

Josef