I am trying to figure out...

[Ozyavas, Adem]

Hello All,

I would like to thank for your very helpful comments and time..
 I have tried and still trying to figrue out the answers to 2 questions formulated below.

There are two user-defined sets A and B. The first theorem to be proved is:

    for a,A being set st a being Element of A holds a in A;      ::Q1

and the second:

   for f being Function of A,B holds dom f = A;                ::Q2

For Q2 I tried to use

definition
  let X,Y;
  let R be Relation of X,Y;
  attr R is quasi_total means
:: FUNCT_2:def 1

  X = dom R if Y = {} implies X = {}
  otherwise R = {};
end;

and looked into the theorems in FUNCT_2 article. The hypothesis "Y = {} implies X = {}" seems a lot of work and I was wondering if there is another way.

Thank you again very much and have a nice weekend.

Adem Ozyavas

[Adam Naumowicz]

Hi Adem,

On Sat, 24 Oct 2009, Ozyavas, Adem wrote:

> There are two user-defined sets A and B. The first theorem to be proved is:
>
>    for a,A being set st a being Element of A holds a in A;      ::Q1

It holds if (and only if) A is non-empty.

> and the second:
>
>   for f being Function of A,B holds dom f = A;                ::Q2
>
> For Q2 I tried to use
>
> definition
>  let X,Y;
>  let R be Relation of X,Y;
>  attr R is quasi_total means
> :: FUNCT_2:def 1
>
>  X = dom R if Y = {} implies X = {}
>  otherwise R = {};
> end;
>
> and looked into the theorems in FUNCT_2 article. The hypothesis "Y = {}
> implies X = {}" seems a lot of work and I was wondering if there is
> another way.

As in the former case, the statement is clearly accepted if Y is
non-empty. The condition is formulated in this form just to allow
defining functions from X to Y even in a slightly more general situation.

Best,

Adam Naumowicz

=======================================================================
Dept. of Programming and Formal Methods  Fax: [phone]
Institute of Informatics                 Tel: [phone] (office)
University of Bialystok                  E-mail: adamn@...
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================

[Freek Wiedijk]

Adam:

>> There are two user-defined sets A and B. The first theorem to be proved is:
>>
>>    for a,A being set st a being Element of A holds a in A;      ::Q1
>
> It holds if (and only if) A is non-empty.

If Mizar's type system wasn't broken (in the sense that
it doesn't allow types to be empty; well, maybe "broken"
is too strong a word, but the Mizar type system _is_
severly limited because of this) then one could define
"Element of" in the natural way.  And then this would be
a provable theorem (and then in fact it would be automatic
when one has requirement SUBSET, I guess.)

Freek

[trybulec]

Hi:

Cytowanie freek <freek@...>:

>
> If Mizar's type system wasn't broken (in the sense that
> it doesn't allow types to be empty; well, maybe "broken"
> is too strong a word, but the Mizar type system _is_
> severly limited because of this) then one could define
> "Element of" in the natural way.  And then this would be
> a provable theorem (and then in fact it would be automatic
> when one has requirement SUBSET, I guess.)
>

Mizar does not allow for meaningless types like

     an empty non empty set
     an element of the empty set
     a function from a non empty set into the empty set

Does it means that it is "broken"? I may agree that it is more limited;
I would rather say that it is more demanding. Then suspending the
requirement might be exciting: the life becomes easier (and the quality
of work done becomes lower: some questions are left unanswered).

If a meaningless type \theta is allowed that           for x being
\theta holds ...

is understood as

     for x st x is \theta holds ...

so actulally the type is eliminated by a predicate and the whole type
system becomes syntactic sugar. And why we need two predicates

        x is element of A

and     x in A?

I do not argue that the solution adopted by Mizar is the only good solution
or the best one. However we need arguments to change it, not to keep it
as it is. I do not claim that it is not possible that we eventually
find such arguments. The problem is that it is difficult to anticipate
the consequences of changing the approach.

Regards,
Andrzej

[Freek Wiedijk]

Hi Andrzej,

>Mizar does not allow for meaningless types like
>
>    an empty non empty set
>    an element of the empty set
>    a function from a non empty set into the empty set

I disagree that they're meaningless!  They're just empty.
Is the empty _set_ a meaningless _set?_  No, of course it
isn't.  And likewise an empty type is not a meaningless type.

In Coq I can do

     Coq < Check unit->Empty_set.
     unit -> Empty_set
          : Set

     Coq <

and there is no problem there at all.  ("Empty_set" is an
empty type, and "unit" is a type with exactly one inhabitant,
called "tt":

     Coq < Check tt.
     tt
          : unit
     
     Coq <

.)

>If a meaningless type \theta is allowed that
>
>    for x being \theta holds ...
>
>is understood as
>
>    for x st x is \theta holds ...
>
>so actulally the type is eliminated by a predicate and the
>whole type system becomes syntactic sugar. And why we need
>two predicates
>
>       x is element of A
>
>and    x in A?

For the same reasons that one now has types in Mizar:

     1. to have the system automatically infer that certain
        predicates hold (using the types in definitions
        and registrations)

     2. to disambiguate overloaded syntax

>However we need arguments to change it, not to keep it
>as it is. I do not claim that it is not possible that we
>eventually find such arguments.

For me the argument is that the types can have much more
natural defintions.  Now, often when I want to define a
type, Mizar won't allow me to write what should be there,
and then I just give up.

In the HOL systems, one doesn't get empty types either,
but there one doesn't have dependent types, so there it
doesn't hurt.  But Mizar, rightly so, _has_ dependent types,
and there often one gets specific parameters for which the
type naturally becomes empty.

>The problem is that it is difficult to anticipate the
>consequences of changing the approach.

You are right that no one will prove "existence" correctness
conditions anymore, and that for that reason there might
be more mistakes in definitions.  But that is balanced for
me by the fact that finally types can be defined in the
natural way.  In the _right_ way.  Like "Element of", yes.

We've had this discussion before, I'm sure.  My excuses
for being triggered.

Freek

[trybulec]

Cytowanie freek <freek@...>:
>> Mizar does not allow for meaningless types like
>>
>>    an empty non empty set
>>    an element of the empty set
>>    a function from a non empty set into the empty set
>
> I disagree that they're meaningless!  They're just empty.
A rose by any other name ...
> Is the empty _set_ a meaningless _set?_  No, of course it
> isn't.  And likewise an empty type is not a meaningless type.

The empty set has quite precise meaning. And what is

   the empty non empty set?
>
> In Coq I can do

Why we should mimic Coq?

>>
>>       x is element of A
>>
>> and    x in A?
>
> For the same reasons that one now has types in Mizar:
>
>     1. to have the system automatically infer that certain
>        predicates hold (using the types in definitions
>        and registrations)
>
>     2. to disambiguate overloaded syntax
>

OK It is a valid argument.

>> However we need arguments to change it, not to keep it
>> as it is. I do not claim that it is not possible that we
>> eventually find such arguments.
>
> For me the argument is that the types can have much more
> natural defintions.  Now, often when I want to define a
> type, Mizar won't allow me to write what should be there,
> and then I just give up.
>

You can always use a permissive definition. Like we do with

   Element of ...
or
   Function of ..., ...

So, actually it is a technicality.

>
>> The problem is that it is difficult to anticipate the
>> consequences of changing the approach.
>

I ment something like this:

In checker to get the contradiction between a universal formula we
remove quatifiers and substitute for bound variables free variables.

Than we try to find a substitution for free variables that contradicts
the other premises.

If we allow for types with the empty denotation, then we should
additionally check if all free variables have non empty types. Quite
unnnatural, isn't it?

In general we cannot infer

       for x being theta holds alfa
       -------------------------------
             alfa

when x does not occur in alfa

I guess that in Coq such inferences are not allowed in general.

It means that we cannot remove fictitious quantifiers.


> We've had this discussion before, I'm sure.  My excuses
> for being triggered.


No problem, we get better understanding the different approaches. I
appreciate it.

Regards,
Andrzej

[Josef Urban-2]

Dear Andrzej, Freek,

2009/10/26 <trybulec@...>

> Cytowanie freek <freek@...>:
>  We've had this discussion before, I'm sure.  My excuses
>> for being triggered.
>>
>
>
> No problem, we get better understanding the different approaches. I
> appreciate it.

This discussion comes every two years and brings little new arguments.
If you want to progress, you should create a wiki page summarizing the
discussion of the
topic, and everyone should check first if his argument has already
been answered or not.
Best,
Josef

[Freek Wiedijk]

Dear Andrzej,

>The empty set has quite precise meaning. And what is
>
>  the empty non empty set?

Ah yes, this new "the" thing won't work with empty types.
And the same holds for permissive definitions (that's the
name right, when there's an assumption in a func definition?)
If you would define

  definition
    assume contradiction;
    func foo -> A means ...
  end;

then A has better be a non empty type, right?  So one should
have Mizar requiring something like a "cluster" for _those_
two cases.  But I really would like the non-emptiness of a
type to be a _registration_ then, instead of it being part
of the definition.

>>In Coq I can do
>
>Why we should mimic Coq?

I just was trying to argue that it's unproblematic.
Because it's unproblematic there.

>You can always use a permissive definition.

What does this exactly mean in this case?  To do

definition
  let X be non empty set;
  mode Element of X means ...
end;

or to do

definition
  let X be set;
  assume X <> {};
  mode Element of X means ...
end;

?

However in both cases you won't be able to prove that

for x,X being set holds (x in X iff x is Element of X)

right?  So then it still is _wrong._

>So, actually it is a technicality.

You can work around the problems with the non-emptiness of
types, sure.  But you can do arithmetic in Roman numerals
too.  My claim is that the non-emptiness of types in Mizar
is like Roman numerals for arithmetic.   III + IV = VII!
What's the problem?

>If we allow for types with the empty denotation, then
>we should additionally check if all free variables have
>non empty types. Quite unnnatural, isn't it?

So if you make CHECKER first replace

  for x being A holds ...

by

  for x st x is A holds ...

(and similar for ex) in the cases that it cannot establish
the non-emptiness of A by way of a cluster, before running
its usual algorithms, _that_ wouldn't be so big a change,
maybe?  So then you wouldn't need to change your algorithms.
And maybe it still might behave reasonably?

>In general we cannot infer
>
>      for x being theta holds alfa
>      -------------------------------
>            alfa
>
>when x does not occur in alfa
>
>I guess that in Coq such inferences are not allowed in general.

Exactly.  In Coq need to exhibit an element of theta
for that.  And "the theta" doesn't exist :-)

Freek