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

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Andrzej,

>Recently we intend to be rather close to the language, so we
>rather use
>   'real number'
>than
>   'Real', i.e. 'Element of REAL'
>what actually  means "an element of the set of all real
>numbers", that is rather complicated, the shortcut 'Real' is
>misleading.

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?

>You propose to go just the opposite direction: to treat real
>numbers as elements of a structure S,
>that is actually
>      'Element of the carrier of S'
>I have not strong arguments against it. However the problem
>is what S should be. Why the monoid?

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.

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).

>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?

Freek