The paper contains some remarks on building automated counterpart of the research presented during one of the previous CS&P workshops by A. Gomolinska. My main objective was the formal (and machine-checked) proof of Theorem 4.1 from her paper \A Comparative Study of Some Generalized Rough Approximations", hence the title of the present paper is by no means accidental.
During Concurrency Speci cation & Programming International Workshop in
2001 Anna Gomolinska presented a draft of her paper on the generalization of
rough approximation operators. Essentially, the idea behind the research was to
collect some standard properties of rough approximations and to cut o some
ordinary properties of binary relations to get { a little bit in the spirit of reverse
mathematics { a catalogue of equivalences between relations' properties and
corresponding formulas for rough sets. The nal { revised and updated { version
of the research appeared eventually in Fundamenta Informaticae under the
title A Comparative Study of Some Generalized Rough Approximations [
During that time, I was also interested in computer-supported formalization of rough sets and I claimed that the paper could be a quite interesting testbed for my studies on the use of proof-assistants to support mathematicians in their work. Just to be a little more explicit, the system which was considered by me was Mizar, equipped with rst order logic language and Tarski-Grothendieck set theory as a underlying set theory.
After a deeper study at that time, I decided to abandon the formalization
work as it looked too much di erent from the one I followed as described in
[
Gomolinska started with { quite general { uncertainty map I from non-empty universe U into its powerset. Potentially, no additional assumptions at the beginning are made, with the exception of a kind of re exivity { that any object u from the universe is an element of I(u):
Theorem 4.1 is the core of the rst part. We aimed at the full formalization
of this item, so we quote it here using original notation from [
U , objects u; w 2 U , and i = 0; 1, it Theorem 4.1 For any sets x; y holds that: a) f0d id f0: b) f1d id f1: c) f0(x) is de nable. d) 8u 2 f1(x): (I(u); x) > 0: e) 8u 2 f1d(x): (I(u); x) = 1: f) If (u) = (w), then u 2 f0(x) i w 2 f0(x); and similarly for f0d. g) If I(u) = I(w), then u 2 f1(x) i w 2 f1(x); and similarly for f1d. h) fi(;) = ; and fi(U ) = U ; and similarly for fid. i) fi and fid are monotone. j) fi(x [ y) = fi(x) [ fi(y): k) fid(x [ y) fid(x) [ fid(y): l) fi(x \ y) fi(x) \ fi(y): m) fid(x \ y) = fid(x) \ fid(y):
The approach is signi cantly di erent than those of W. Zhu [
In our formal approach to rough approximations, our choice was to have indiscernibility relation de ned as a binary relation on a non-empty universe U . Essentially then, this corresponds to an abstract relational structure
R = hU; i with all properties credited to the internal relation of R.
At the very beginning, we do not assume any of standard properties of
approximations (or tolerances) added to the type of , although we introduce two
basic Mizar types, called Approximation_Space and Tolerance_Space, to have
them available in the Mizar Mathematical Library. More thorough discussion on
this development is given in [
Faithfully following Gomolinska, we should be aware of the fact that we have
A = hU; I; i as a formal approximation space. I had some doubts if I should mention at all { rough inclusion function as in the classical approach the membership function was considered. Also as indiscernibility relation was rather preferred over the uncertainty mapping. My convincement was stronger after the formalization of Zhu's paper on correspondence between properties of binary relations and of rough sets.
In the literature [
Even if in considered paper standard lower approximation operator is de ned as (10)
LOW (x) = fu 2 U : (I(u); x) = 1g; happily its immediate consequence is available as (12):
LOW (x) = fu 2 U : I(u) xg: Then we could be sure the function will not be needed at the moment. 4
Gomolinska claimed the following name space for approximations operators (18): f0(x) = fu 2 U : (u) \ x 6= ;g f1(x) = fu 2 U : I(u) \ x 6= ;g with corresponding f0d and f1d:
Then we can think on the following de nition for definition let R be non empty RelStr; let tau be Function of the carrier of R, bool the carrier of R; func f_0 R -> map of R means for x being Subset of R holds
it.x = { u where u is Element of R : tau.u meets x }; end; and similar, for uncertainty mapping I. Hence, it is quite straightforward to see that the common variable in both de nitions is just arbitrary function (with proper domain and codomain), let us call it f , and then it is quite natural to use instead of the above formulation something like definition let R be non empty RelStr; let f be Function of the carrier of R, bool the carrier of R; func ff_0 f -> map of R means for x being Subset of R holds
it.x = { u where u is Element of R : f.u meets x }; and then to use definition let R be non empty RelStr; func f_0 R -> map of R equals ff_0 tau R; func f_1 R -> map of R equals ff_0 UncertaintyMap R; end;
For a reader not very much acquainted with the Mizar system it is not very cryptic, but the use of a keyword equals turns automatic treatment of equalities on and then more reasonings can be justi ed automatically.
Furthermore, we have just a single { more general { theorem expressing (f) and (g) at the same time, instead of two: theorem :: ROUGHS_5:31 :: 4.1 f) Flip for u,w being Element of R,
x being Subset of R st f.u = f.w holds
u in (Flip ff_0 f).x iff w in (Flip ff_0 f).x;
It can be noted at the rst sight, that there is nothing on approximation operators there { we can think on quite general property of mappings as R is only non-empty relational structure.
The Mizar functor Flip f, which is the formal counterpart of f d is de ned accordingly as definition let X be set;
let f be Function of bool X, bool X; func Flip f -> Function of bool X, bool X means for x being Subset of X holds
it.x = (f.x`)`;
Obviously, no approximations are needed here, either.
In our Mizar approach, U P P and LOW operators from [
In our study of fuzzy implications, we developed some techniques (Mizar schemes) which could decrease the number of technical steps in de ning functions.
It should be pointed out that if we start with the uncertainty mapping rather than with indiscernibility relation, the core property is
8u2U u 2 f (u);
which is essentially the formula (1) in [
To have faithful formal representation is the above, we introduced the new Mizar attribute definition :: property (1) p. 105 let R be non empty set; let I be Function of R, bool R; attr I is map-reflexive means :: ROUGHS_5:def 1
for u being Element of R holds u in I.u; end;
As we already mentioned before, our core idea was to start with an approximation space hU; i, where U is non-empty universe and is an indiscernibility relation de ned on U . All rough operators, membership and uncertainty functions, and also rough inclusions, could be de ned based within this framework. The proper choice of the formal background is especially important, because in the Mizar Mathematical Library, all statements should be proven based on classical logic and/or already proven lemmas.
In this paper, as a rule we do not quote correctness conditions (as they are needed also for de nitions), although de nitions should also obey the rule of the necessary justi cation. Even if sometimes of quite technical character, the proof is needed and the example of that is given below. We formulate a bunch of handy Mizar schemes which make this activity a little bit less painful for the user. definition let R be non empty set; func singleton R -> Function of R, bool R means :: ROUGHS_5:def 2 for x being Element of R holds it.x = {x}; existence proof
deffunc U(object) = {$1}; A1: now let x be Element of R; {x} c= R; hence U(x) in bool R; end; thus ex f being Function of R, bool R st for x being Element of R holds f.x = U(x)
from FUNCT_2:sch 8(A1); end; uniqueness; ::: here the proof is not quoted end;
Why this de nition was really needed? Essentially, to use the Mizar type (and adjectives are important constructors for types) one should prove its nonemptiness, i.e., to construct at least one example of an object possessing this property, to show the usefulness of the attribute. registration let R be non empty set; cluster singleton R -> map-reflexive; end;
Another handy use of adjectives is given below: registration let R, f; cluster ff_0 f -> c=-monotone; end;
This allows to obtain automatically the proof of Theorem 4.1(i) as follows: registration let R be non empty RelStr; :: i) cluster f_0 R -> c=-monotone; cluster f_1 R -> c=-monotone; end; 6
Obviously, building proper formal framework for further work is crucial. Having
said that, we can build the rest of functions de ned in [
Even is this extended abstract is only a draft of the formal work done, the complete formalization (just accepted for inclusion into the Mizar Mathematical Library) is available at
Using 1386 lines of Mizar code (44 kilobytes) and formulating 7 de nitions
and proving 53 theorems we completed the rst part of formalization work of
Gomolinska's paper [