The processing and analysis of the Mizar library has been performed using the infrastructure of the University of Bialystok High Performance Computing Center. In the current Mizar language, direct linking to statements formulated as compound conditions is prohibited. This particular language feature has often been considered by the users as an unnecessary disruption of the natural course of proof steps. In this paper, we present an analysis of the linking structure in the current contents of the Mizar Mathematical Library which provides statistical data needed to implement a usability-based solution to this problem and propose corresponding changes in the library.
Using a Weakly-Strict Mizar (WSM) [Nau16, Byl12] parser 3, we have collected some statistical data which shows the usage of these constructs in the MML version (5.33.1254) distributed together with the current ocial Mizar version (8.1.04) 4. The table below shows the number of occurences of these language constructs.
As we can see, some of the constructs are signicantly less frequent than others. Notably, case and suppose are used only in special kinds of proofs (reasoning per cases) and the use of compound statements in this context is usually connected with applying denitional expansion [Kor15]. Let us also note that loci declarations and generalizations both use the same let keyword and so syntactically they are similar (what makes them dierent is the context, since loci declarations are only available within denitions). In most contexts the case and suppose constructs can be used interchangeably and most users tend to prefer the more common suppose. The syntax of choice statements ( consider) and existential assumptions ( given) requires a that phrase, so they never occur without the conditions part, even if they are followed by a single proposition. In all other cases, a user might decide to use only the simple forms of the constructs, e.g. a sequence of single assumptions, and never use compound conditions. And so there are articles in the Mizar library whose authors avoided using compound conditions completely. However, the compound conditions are in general used quite often in the MML. The number of conditions used in an article ranges from 0 to 412 (total 94392). If we assume (very roughly) that each condition is represented by one line of formal text and we compare it to the total number of 2473054 lines of the WSM representation of all the articles, this gives about 4% of all the text content.
It is also worth mentioning that the existential assumption is actually a syntactic sugar construct which replaces an assumption followed by a choice statement - this language feature is rarely used by less experienced Mizar users who are interested primarily in the correctness of their proofs and not in their brevity or good style.
Now let us look at the simplest example which demonstrates the underlying linking problem. Here we have a common choice statement with one chosen constant and two labelled compound conditions potentially related to this constant, and we want to immediately refer to this statement in the next proof step: consider x such that A1: then by references2 ; and A2:
by references1 ; In the original Mizar parser the linking (here using the then keyword) is not allowed, because it is ambiguous what it should link to. In consequence, the parser marks the second line with the 164: Nothing to link error message. In fact, the comment might as well say Too many options to link , because in this case there are four possible interpretations of the linked statement, namely: 1. ex x st
& 2. 3. 4.
&
Although there are cases when option 1. would be useful, usually reasoning in Mizar requires an existentially quantied statements to be eliminated in order to advance the proof. As for option 2., it would be quite useful for a small number of compounds. The average number of compounds in the current MML is 1.92, which makes this option potentially useful for accumulating available facts rather than being very selective in inference statements. However, there are cases of compound statements in the library composed of as many as 33 propositions 5 and in this case linking to a conjunction of all these propositions would produce too complicated inferences to be practically justied. Option 3. seems least useful and would be most misleading for the users, especially if there were more than two compound propositions involved. This leaves us with option 4., and apparently this 3The parser can be downloaded from a dedicated Git repository: https://github.com/MizarProject/wsm-tools . 4http://mizar.org/ 5E.g. the GATE_3 article developing the theory of digital circuits. is the semantics adopted by two Mizar-inspired systems: Mizar Light for HOL Light developed by F. Wiedijk [Wie01] as well as Makarius Wenzel’s implementation of the Isabelle/Isar language [Wen02]. Therefore, we have implemented the fourth option in an experimental Mizar version. Mizar veriers pre-compiled for main supported software platforms are available for download and further experimentation at the author’s website 6. There you can also nd an example of a simple set-theoretical Mizar article adapted to this new linking method (le xboole_0.miz) to demonstrate its usefulness. 3
First of all, the proposed enhancement of the Mizar parsing module might be benecial for some Mizar users. But apparently, the inability of linking to compound statements is also one of the main obstacles that complicate automatic improving the legibility of natural deduction proofs in Mizar [Pak14] and make lemma selection based on the close reference principle equivalent to an NP-hard graph problem [Pak15]. So the enhancement might help advance the research on proof legibility. And nally, Mizar has been widely known for its inuence on other proof assistant systems and their proof languages - this work is an example that the inuence might as well work in the other direction. 3.0.1
The processing and analysis of the Mizar library has been performed using the infrastructure of the University of Bialystok High Performance Computing Center.
6http://mizar.uwb.edu.pl/~softadm/linking