Caves Travel Diving Graphics Mizar Texts Cuisine Lemkov Contact Map RSS Polski
Trybiks' Dive Mizar Eddie Eddie::MSE vs. Mizar-MSE YAC Software
  Back

Mizar

Eddie

Eddie::MSE vs. Mizar-MSE

Version History

Articles

Mizar-MSE Syntax

Eddie::MSE vs. Mizar-MSE
Mizar-MSE as used in Eddie::MSE differs in some points from the classic Mizar-MSE language. These differences, as well as motivations leading to their introduction, are here described.

Namely: Details:

sort instruction

In classic Mizar-MSE there is not instruction for the explicit introduction of sorts. Sorts are "collected", that is, when the parser sees a new sort (in the reserve instruction, for instance) it adds this sort to the list of defined sorts (without reporting any errors).

This can lead to a situation where a misspelling of a type name (such as POINT and PONT) introduces a new type. And this, in turn, may lead to strange errors, when we try to use a theorem or prove one that is actually defined with another sort. Experienced Mizarers will find such errors quickly, but novice users may have lots of problems with cases such as the one described.

So, a new environment instruction was introduced - sort - that allows the introduction of sorts (types).

In a single sort instruction, a single sort or many sorts can be defined:
  environ
  
  sort set;
  sort POINT, LINE, PLANE;
  
  begin
Now, if the user tries to reserve a variable for a given type, and misspells the type's name, for instance, an error will be reported.

Top

pred instruction

Just as there's no instruction for the introduction of sorts in classic Mizar-MSE, there's also no instruction for the introduction of predicates. When the parser sees a new predicate (in an axiom or a constant definition) it adds this predicate to the list of defined predicates (without reporting any errors).

Both the misspelling of the predicate's identifier and the change of the order of sorts under a predicate introduce a new predicate in the article. This again may lead to unexpected errors.

So, a new environment instruction was introduced - pred - that allows the introduction of predicates.

In a single pred instruction, a single predicate can be defined. A definition consists of the predicate's identifier, optionally followed by a list of sorts. Only variables and constants of the appropriate sorts, and in the correct order, may later by used with this predicate.

Examples:
  environ
  
  sort set;
  sort LINE, POINT;
  
  pred p[];
  pred in[set, set];
  pred ON[LINE, POINT];
  
  begin
If the user tries to introduce a new predicate that is not defined in the pred instruction, for instance by unknowingly changing the order of the arguments in the ON predicate, an error will be reported.

Top

Infix notation for predicates

In classic Mizar-MSE, only prefix notation is allowed for predicates:
  for A, B being POINT, K, L being LINE st
    ON[A, K] & ON[A, L] & ON[B, K] & ON[B, L] holds
      A = B or K = L;
  
  for X, Y, Z being set holds
    SUM[Z, X, Y] iff
      for x being set holds
        IN[Z, x] iff IN[X, x] or IN[Y, x];
Without seeing the definition of belonging of a point to a line, or of the sum of sets, you can easily forget when writing the article, whether the line or the point comes first in the ON predicate. Or, whether in the SUM predicate, the arguments of the sum operator go first, or the result.

It should be obvious that in cases such as these, infix notation is much more readable. Thus, Eddie::MSE allows now for such notation in predicates:
  environ
  
  sort LINE, POINT;
  sort set;
  
  pred POINT on LINE;
  pred set in set;
  pred set is_sum_of set, set;
and then:
  Ax1:
  for A, B being POINT, K, L being LINE st
    A on K & A on L & B on K & B on L holds
      A = B or K = L;
  
  Ax2:
  for X, Y, Z being set holds
    Z is_sum_of X, Y iff
      for x being set holds
        x in Z iff x in X or x in Y;
  
  begin
It seems that the second version of these formulae are much more helpful in understanding the text, for readers as well as for the author. :-) However, for backward compatibility and to keep the "spirit" of classic Mizar-MSE, prefix notation is still allowed.

Top