8.1 Improvement of an Article
8.1.1 Improvement of the Main Section
First, we need to improve an article. To do this, we need the following commands.
RELPREM Checks unnecessary citations.
CHKLAB Checks unnecessary labels.
INACC Checks unnecessary lines.
TRIVDEMO Checks trivial demonstrations.
RELINFER Checks unnecessary lines.
Such commands are provided. All these commands are used in
the following way.
RELPREM TEXT\EXAMPLE1.MIZ
If we execute the following after carrying out each command,
the error number will be written into an article.
ERRFLAG TEXT\EXAMPLE1.MIZ
RELPREM checks to see if irrelevant matters in reasoning
are cited after "by". It also checks for the same thing for "then".
If certain things are not needed for reasoning, an error will appear.
CHKLAB later on checks for the labels that are not used after
labeling.
INACC later checks for the lines that are not used. If an
error occurs from this checker and lines are erased, there may be excess
citations and labels due to this; therefore, it needs to be checked again
from the beginning.
TRIVDEMO checks to see if there are trivial proofs. Trivial
matters need to be removed. When being as follows,
A=B
proof
To:A=C by T1;
C=D by T2;
hence thosis by To;
end;
it meens that we can simplify them like the following. T1 and T2 are the labels used between the above-mentioned proof and end (external label of proof --- end).
A=B by T1,T2;
Explanation of RELINFER;
RELINFER checks to see if two lines are summarize to one. For example, When an error (*605) is displayed as follows,
A=B + C by T1;then
D=E + (B + C) by T2;
*605
it meens that we can manage with the following one line.
D=E + (B + C) by T1,T2;
When the error of the number *604 is as follows,
S1: A=B + C by T1;
----------
----------
D=E+ (B + C) by S1,T2
*604
it meens that we can write the following.
S1: A=B + C by T1;
----------
----------
D=E+(B + C) by T1.T2;
If the line of a label S1 is not used for others, we can
delete it, but if used, we cannot delete and cannot reduce a line. We can
find out whether it is used or not, using CHKLAB once again, but when it
is used, *604 may be disregarded because of troublesome to restore it.
Anyway, it is necessary to use a series of check programs repeatedly. As
a result, the number of lines may be decreased no less than several 10
percent. Because derivation of a line to a line is powerful, it is natural
for Mizar checker, but it may become an oversimplification which cannot
be understood when man reads. Therefore, it is not need to necessarily
turn the number of lines even into the minimum, and we may stop moderately.