Re: [mizar] Why *4?

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

Hi,

I guess that this is again caused by the pattern matching algorithm  
in the checker.  FUNCT_2:def 1 is used in the following
format (I think, having the top-secret sources as the only documentation):

for X,Y being set  for R being Relation of X,Y holds
 ((Y = {} implies X = {}) implies ( X = dom R iff R is quasi_total))
 &
 (not (Y = {} implies X = {}) implies ( R = {} iff R is quasi_total));

so we want to get the first conjunct matched. 
This is a universal formula, all parts of which need to be succesfully 
instantiated, and its antecedent is the problem here.
We can do it either by directly supplying the antecedent (as you did),
or only adding the fact "NAT <> {}", which does almost the same ( and 
which is actually why adding the clusters also works).

But the checker has now no means how to add the tautology by itself,
nor how to find out that the two cases are complementary during the
pattern matching.

I think there are some changes planned in the checker, but do not know if 
they will be enough to take care of this.

Best,
Josef


On Sat, 3 Jan 2004, Piotr Rudnicki wrote:

> Hi:
> 
> In the following
> 
> -----------------------------------------------------------------------------
> 
> environ
> 
>  vocabulary FUNCT_1, RELAT_1, BOOLE;
>  notation XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS;
>  constructors FUNCT_2, NUMBERS;
>  clusters FUNCT_2;
>  theorems FUNCT_2;
> 
> begin
> 
>  consider f being Function of NAT, NAT;
> 
>  dom f = NAT by FUNCT_2:def 1;
> ::>           *4
> 
>  NAT = {} implies NAT = {}; then
>  dom f = NAT by FUNCT_2:def 1;
> 
> ------------------------------------------------------------------------------
> 
> we get *4.  Why?  Why adding an obvious premise here solves the problem?
> 
> Adding clusters from XBOOLE_0 and ORDINAL2 solves the problem too but this
> is not the point.
> 
>