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

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

I am a bit late with the answer. I was ill for few days, and the answer
is not easy, anyway.

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

For real numbers the following structures already defined in Mizar may
be used candidates as well:

the additive semigroup:
 func <REAL,+> -> unital associative invertible commutative cancelable
strict
     (non empty HGrStr) equals
:: MONOID_0:def 26
   HGrStr(#REAL, addreal#);
the multiplicative semigroup:
func <REAL,*> -> unital commutative associative strict (non empty
HGrStr)
  equals
:: MONOID_0:def 30
   HGrStr(#REAL,multreal#);
the additive monoid (what you proposed)
 func G_Real -> strict LoopStr equals
:: VECTSP_1:def 6
   LoopStr (# REAL,addreal,0 #);
the multiplicative monoid with zero:
 func multEX_0 -> strict multLoopStr_0 equals
:: ALGSTR_1:def 21
  multLoopStr_0 (# REAL, multreal, 1, 0 #);
the field:
 func F_Real -> strict doubleLoopStr equals
:: VECTSP_1:def 15
  doubleLoopStr (# REAL,addreal,multreal,1,0 #);
for people interested in topology the metric space may be more
interesting:
  func RealSpace -> strict MetrStruct equals
:: METRIC_1:def 14
    MetrStruct (# REAL, real_dist #);
or the topological space of real numbers
 func R^1 -> strict TopSpace equals
:: TOPMETR:def 7
   TopSpaceMetr(RealSpace);
the lattice may be not so interesting:
 func Real_Lattice -> strict LattStr equals
:: REAL_LAT:def 4
  LattStr (# REAL, maxreal, minreal #);
and some special constructions even less:
  func TernaryFieldEx -> strict TernaryFieldStr equals
:: ALGSTR_3:def 5
   TernaryFieldStr (# REAL, 0, 1, ternaryreal #);
I do not claim that's all.

So the problem is, if we really can choose the most important structure
S with
       the carrier of S = REAL

Regards,
Andrzej

Freek Wiedijk wrote:

> Dear Andrzej,
>
> In our Coq library that we wrote for FTA (it's called "CCORN"
> now, I think, don't ask me what it means) the + on the
> complex numbers is just an instance of the + on arbitrary
> additive monoids (or "LoopStr"s, really, it's the one that in
> the MML is defined as "RLVECT_1:def 3").  Do you consider it
> a good idea to recast the whole theory of NAT until COMPLEX
> to use that operator?  It makes everything more uniform, of
> course:  when you talk about other groups, like polynomials
> or elements of a vector space or whatever, you don't need to
> start developing all the basic lemmas all over again.