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

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Wed, Mar 05, 2003 at 12:19:14PM +0100, 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
> 
> 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?
> 
> Freek

Grzegorz has fixed some parameters of the query engine at:

	http://megrez.mizar.org/mmlquery/three.html

and we can do the query that Freek asked for.  Let me repeat:

The fact that Freek is looking for involves the following constructors

        HIDDEN:mode 1           set
        XREAL_0:attr 1          real
        XREAL_0:func 5          -  (binary)
        XREAL_0:pred 1          <=

and in addition number 0.  We query for the items in which these resources
occur exactly (i.e. no other resources occur) in this way:

exactly * ({hidden:mode 1, xreal_0:attr 1, xreal_0:pred 1, xreal_0:func 5 })
and number 0 occur

and we get

HEINE:th 4
PROB_1:th 2
SQUARE_1:th 11
SQUARE_1:th 12
SQUARE_1:th 29

I do not know how to make this query more precise as the fact that
Freek is looking for can be expressed in many ways.

Cheers,

PR

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr