[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] Hindrances
What really hinders the work with MML, it is using different
formulations of the same fact in different theorems. The typical
example:
sometimes it is 'i < j' sometimes 'i+1 <= j'
and one has to use NAT_1:38 to move from one to the other.
The same goes for 'A meets B' and " A /\ B <> {}'. This had been revised
when we were working on XBOOLE_1.
Recently I looked to 'A in bool X', i.e. 'A c= X'. I have found 20
occurrences of it in MML. Mostly ZFMISC_1. An attempt to revise 'in
bool' was quite successful. With the exception of SUBSET_1 (that cannot
use the requirements SUBSET), the proofs became shorter, the authors
actually needed the 'c=' version of the theorem, not 'in bool'.
The resulting theorems (in ZFMISC_1) either are already in XBOOLE_1 or
should be moved to it.
The same was done in MBOOLEAN (following ZFMISC_1; for many sorted
sets).
Adam Grabowski promised to revise it soon.
Andrzej Trybulec