Re: [mizar] How to search for a lemma?

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Dear Freek,

Freek Wiedijk wrote:

> I always use "Real" for variables.  I don't know why.
> Probably because it is less typing, but maybe also because
> that the variables have _both_ the types "Real" and "real
> number".
>
> Maybe there could be a requirement that gives all expressions
> of type "real number" also the type "Real" (and the same for
> "natural number" versus "Nat", etc.), and then it doesn't
> matter anymore what you choose?
>

Too much adhocness for me. If we want it, we definitely need the concept
of
      the set of all \theta
with a mechanism of the registration of the fact that this set exists (I
mean that it is not a proper class). Then the fact that
    x in the set of all \theta implies x is \theta
may be obvious. Or even
    x in the set of all \theta iff x is \theta
because the types in Mizar are non empty. So what you propose is to have
a requirement for special cases:
 \theta = 'real number', 'natural number',
what about other cases 'complex', 'rational', 'integer', hereditary
finite? (The last example is maybe unfair, we have only 'Element of
FinSETS', no attribute for it.)
I see only one argument for using 'Element of REAL' instead of 'real
number'. When we use some schemes, e.g.
'LambdaD' (FUNCT_2) we have to use 'Element of REAL' anyway (or to
define special schemes for real numbers).
Is it a sufficiently strong argument?

>
> Okay, so the operation "+" should be defined on the level of
> the LoopStr (I said "monoid" because a mathematician doesn't
> say "LoopStr"), and I think it is.

I meant only that the semigroup structure is enough, we can define the
zero, can't we? And we may be interested
in e.g. the semigroup of positive natural numbers.

>
> But the "S" that you talk about should be as rich as
> possible.  In the Coq library that we have here it would be a
> metric ordered field that is Archimedean ("every element is
> bounded by a natural number") and complete in the metric (or
> something like that, I don't know what the current state of
> these structures here is).

OK In the case of real numbers maybe one can determine what it means 'as
rich as possible'. And maybe it is what you use. Only I do not
understand 'Archimedean' in the meaning given by you - is the set of
natural numbers fixed?
Then the structure must be enriched by the subset of natural numbers. It
is not criticism, I am just interested, how you do it in Coq.
I doubt if the same can be done in general case.

>
> >So the problem is, if we really can choose the most
> >important structure S with
> >       the carrier of S = REAL
>
> I'm surprised all these "strict" structures are there
> separately!  Why aren't they all "projections" ("the ... of
> ...") of one common superstructure that's defined only once?

Still the problem what the common superstructure is? Why the metric and
not the norm? Why ordering and not the
lattice with min and max? What about the topology?

Again in the case of real numbers it probably could be done. Could we
always determine which topology is natural?

Regards,
Andrzej