[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Formalization of the Lebesgue measure in Mizar

On Sun, 22 May 2016, Amir Livne Bar-on wrote:


3. Some of the inference chains make the Mizar engine seem "less smart"
than others. For instance, the end of the proof of EmptySetMeasureZero. Or
algebraic manipulations, such as
       A5: c > a;
       set b = (a + c) / 2;
       a + c > a + a by A5, XREAL_1:6;
       then (a + c) / 2 > (a + a) / 2 by XREAL_1:74;
       then A6: b > a;
which would be nicer if it had equalities instead of inequalities.
You're right, the proof checker is not particularly strong in this respect, so quite simple steps must still be spelled out. But in the case of this proof fragment: 

     suppose A6: c in REAL;
        assume A5: c > a;
        reconsider c as Real by A6, XREAL_0:def 1;
        set b = (a + c) / 2;
        a + c > a + a by A5, XREAL_1:6;
        then (a + c) / 2 > (a + a) / 2 by XREAL_1:74;
        then A6: b > a;
        a + c < c + c by A5, XREAL_1:6;
        then (a + c) / 2 < (c + c) / 2 by XREAL_1:74;
        then b < c;
        hence contradiction by A1, A6, XXREAL_2:def 2;
      end;

it can be written like this:

      suppose c in REAL;
        then reconsider d=c as Real;
        assume c > a; then
        a + a < a + d < d + d by XREAL_1:6; then
        (a + a) / 2 < (a + d) / 2 < (d + d) / 2 by XREAL_1:74;
        hence contradiction by A1, XXREAL_2:def 2;
      end;

and then it looks a little better.
For example, I don't understand the difference between Real and Element of REAL.
In most contexts one should use 'Real' (which is just a shorthand for 'real Number'). 'Element of REAL' is used mainly in situations where you need to explicitely refer to the domain of real numbers, e.g. when a term is expected to be an element of some given set. The system should know automatically (thanks to the registration in XREAL_0) that any term with the type 'Element of REAL' possesses the 'real' adjective, so is has the type 'Real'.
As another example, I don't know what the "correctness" stanza of a registration should justify. Are there any more sources to learn about Mizar?
'correctness' is a general "placeholder" for a series of specific correctness conditions which have to be proved for various kinds of definitions or registrations. In case of registrations these are 'existence' or 'coherence' (when you specify new type). The "Mizar in a nutshell" manual has an appendix (Skeletons) which shows the formulas associated with these correctness conditions. Just beware that the syntax of conditional and existential registration statements has been changed slightly (it now requires writing the 'for' keyword before the type), but it's the only difference. 

Adam

===========================================================================
Dept. of Programming and Formal Methods      Fax: +48(85)738-83-33
Institute of Informatics                     Tel: +48(85)738-83-06 (office)
University of Bialystok                      E-mail: adamn@mizar.org
Ciolkowskiego 1M, 15-245 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
===========================================================================