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

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

Freek Wiedijk wrote:

> Hello,
>
> I _hate_ REAL_1 and REAL_2, I can never find anything in it.
> I'm really looking forward to XREAL.
>
> I just spent an hour looking for a lemma that would give me
>
>   for x,y being real number st x < y holds y - x > 0
>

It is

theorem :: SQUARE_1:11
  x < y implies 0 < y - x;


>
> Finally I gave up and used REAL_1:54 and REAL_1:36 with an
> intermediate step (y - x > x - x).
>
> So my question is not so much what was the lemma that I
> needed, but how to find it myself.  Grzegorz (or someone else
> who knows), can you tell me how to do this with MML Query?
>

Sorry, I still do not know how to use MML Query. I should learn.

We are late with XREAL_1. There are reasons for that.  XREAL_0 is ready
(or rather was ready).

1. A lot of theorems is formulated with 'x+ -y' instead of 'x-y' or
'x*(y")' instead of 'x/y'. Particularly in REAL_2.I have proposed just
eliminate them (with perhaps one step more for switching between them).
However, Czeslaw convinced me that the equality should be obvious and he
is working on the implementation.

2. Because we want real number to be complex numbers (we talked about it
in Bologna, I believe), so I work on suitable revision of MML. 'COMPLEX'
(the set of all complex numbers) is defined in COMPLEX1 as the Gauss
plane (with points meant as Kuratowski pairs of reals). So, if we tried
to glue in the set of all real numbers, into the place of the real axis,
we would run into troubles: the positive rational numbers are defined as
Kuratowski pairs of finite ordinals that are real. So I have changed the
definition of 'COMPLEX' (to 'Funcs({0,one},REAL)') and Adam Grabowski
reorganized MML to move the definition to ARYTM_0. It was quite a job,
because e.g. FUNCT_4 must be cut into two parts: one part is needed in
ARYTM_0 and the second one uses natural numbers and must be put after
NAT_1. Some intermediate stages of the revision of MML are on the net,
we are close to complete the revision.

The plan is to write (or rather to collect) theorems using the field
operation about complex numbers (they will be also theorems about
reals), the next article - theorems specific about reals (ordering), and
the next article about mixed properties - real and imaginary part,
absolute value.

I hope the integrity of MML will be much higher.

Regards,
Andrzej