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

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

Dear Josef,

Josef Urban wrote:

> This seems to me rather a trouble with structures and identification
> mechanisms generally. I would most probably want a real number to be
> Element of all the structures you show (if present in environment).
> A hack in this direction could be st. like:
>
> definition let S be set;
>   redefine mode Element of S -> Element of 1-sorted(# S #);
>   coherence by STRUCT_0:def 2;
> end;
>

I believe the problem is not with the concept of 'Element of ...' but with
the other concepts. E.g. how should I know that the addition in the monoid
of real numbers is the same as the additional of real numbers (that is
defined separately).
An that it is not the multiplication of real numbers. Actually we have three
natural semigroups for real numbers:
with '+', '*', 'max' and 'min'. The adopted solution is just 4 different
selectors, so maybe more important is to have sort of a generic monoid (or
rather semigroup) and specialize it as 'LoopStr', 'multLoopStr',
'/\-SemiLattStr' and
'\/-SemiLattStr'. On the other hand it is enough to register clusters like

                  cluster -> real  Element of RealSpace

and so on. And then we can make each 'Element of (#REAL, ...#)' to be 'real
number'. What we need it is a mechanism that allows for identifying 'open
Subset of REAL' and 'open Subset of RealSpace'

>
> But it is not enough for current Mizar. I really think we could save
> ourselves a lot of problems like this, if we re-thought the structure
> mechanisms and had as much automatization as e.g. in the cluster
> mechanisms, which work comparatively well.

I agree. We need to work on finding better mechanisms for dealing with
structures.

Reagrds,
Andrzej