:: Formal Development of Rough Inclusion Functions
::
:: Copyright (c) 2019-2021 Association of Mizar Users

theorem Lemacik: :: ROUGHIF1:1
for a, b, c being Real st a <= b & b > 0 & c >= 0 holds
a / b <= (a + c) / (b + c)
proof end;

registration
existence
ex b1 being Approximation_Space st
( b1 is strict & b1 is finite )
proof end;
end;

registration
let R be finite 1-sorted ;
cluster -> finite for Element of bool the carrier of R;
coherence
for b1 being Subset of R holds b1 is finite
;
end;

theorem LemmaSet: :: ROUGHIF1:2
for R being 1-sorted
for X, Y being Subset of R holds
( X c= Y iff (X ) \/ Y = [#] R )
proof end;

theorem LemmaCard: :: ROUGHIF1:3
for R being finite 1-sorted
for X, Y being Subset of R holds
( card (X \/ Y) = card Y iff X c= Y )
proof end;

theorem LemmaCard2: :: ROUGHIF1:4
for R being finite 1-sorted
for X, Y being Subset of R st card ((X ) \/ Y) = card ([#] R) holds
(X ) \/ Y = [#] R by CARD_2:102;

registration
let R be non empty 1-sorted ;
let X be Subset of R;
reduce ([#] R) \/ X to [#] R;
reducibility
([#] R) \/ X = [#] R
by XBOOLE_1:12;
reduce ([#] R) /\ X to X;
reducibility
([#] R) /\ X = X
by XBOOLE_1:28;
end;

definition
let R be finite Approximation_Space;
let X, Y be Subset of R;
func kappa (X,Y) -> Element of [.0,1.] equals :KappaDef: :: ROUGHIF1:def 1
(card (X /\ Y)) / (card X) if X <> {}
otherwise 1;
coherence
( ( X <> {} implies (card (X /\ Y)) / (card X) is Element of [.0,1.] ) & ( not X <> {} implies 1 is Element of [.0,1.] ) )
proof end;
consistency
for b1 being Element of [.0,1.] holds verum
;
end;

:: deftheorem KappaDef defines kappa ROUGHIF1:def 1 :
for R being finite Approximation_Space
for X, Y being Subset of R holds
( ( X <> {} implies kappa (X,Y) = (card (X /\ Y)) / (card X) ) & ( not X <> {} implies kappa (X,Y) = 1 ) );

theorem :: ROUGHIF1:5
for R being finite Approximation_Space
for X being Subset of R holds kappa (({} R),X) = 1 by KappaDef;

theorem Prop1a: :: ROUGHIF1:6
for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa (X,Y) = 1 iff X c= Y )
proof end;

theorem Prop1b: :: ROUGHIF1:7
for R being finite Approximation_Space
for X, Y, Z being Subset of R st Y c= Z holds
kappa (X,Y) <= kappa (X,Z)
proof end;

theorem :: ROUGHIF1:8
for R being finite Approximation_Space
for X, Y, Z being Subset of R st Z c= Y & Y c= X holds
kappa (X,Z) <= kappa (Y,Z)
proof end;

theorem Prop1d: :: ROUGHIF1:9
for R being finite Approximation_Space
for X, Y, Z being Subset of R holds kappa (X,(Y \/ Z)) <= (kappa (X,Y)) + (kappa (X,Z))
proof end;

theorem Prop1e: :: ROUGHIF1:10
for R being finite Approximation_Space
for X, Y, Z being Subset of R st X <> {} & Y misses Z holds
kappa (X,(Y \/ Z)) = (kappa (X,Y)) + (kappa (X,Z))
proof end;

definition
let R be 1-sorted ;
mode preRoughInclusionFunction of R is Function of [:(bool the carrier of R),(bool the carrier of R):],[.0,1.];
end;

definition end;

scheme :: ROUGHIF1:sch 1
BinOpEq{ F1() -> non empty 1-sorted , F2( Subset of F1(), Subset of F1()) -> Element of [.0,1.] } :
for f1, f2 being preRIF of F1() st ( for x, y being Subset of F1() holds f1 . (x,y) = F2(x,y) ) & ( for x, y being Subset of F1() holds f2 . (x,y) = F2(x,y) ) holds
f1 = f2
proof end;

definition
let R be finite Approximation_Space;
func kappa R -> preRIF of R means :DefKappa: :: ROUGHIF1:def 2
for x, y being Subset of R holds it . (x,y) = kappa (x,y);
existence
ex b1 being preRIF of R st
for x, y being Subset of R holds b1 . (x,y) = kappa (x,y)
proof end;
uniqueness
for b1, b2 being preRIF of R st ( for x, y being Subset of R holds b1 . (x,y) = kappa (x,y) ) & ( for x, y being Subset of R holds b2 . (x,y) = kappa (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefKappa defines kappa ROUGHIF1:def 2 :
for R being finite Approximation_Space
for b2 being preRIF of R holds
( b2 = kappa R iff for x, y being Subset of R holds b2 . (x,y) = kappa (x,y) );

definition
let R be finite Approximation_Space;
let X, Y be Subset of R;
func kappa_1 (X,Y) -> Element of [.0,1.] equals :Kappa1: :: ROUGHIF1:def 3
(card Y) / (card (X \/ Y)) if X \/ Y <> {}
otherwise 1;
coherence
( ( X \/ Y <> {} implies (card Y) / (card (X \/ Y)) is Element of [.0,1.] ) & ( not X \/ Y <> {} implies 1 is Element of [.0,1.] ) )
proof end;
consistency
for b1 being Element of [.0,1.] holds verum
;
func kappa_2 (X,Y) -> Element of [.0,1.] equals :: ROUGHIF1:def 4
(card ((X ) \/ Y)) / (card ([#] R));
coherence
(card ((X ) \/ Y)) / (card ([#] R)) is Element of [.0,1.]
proof end;
end;

:: deftheorem Kappa1 defines kappa_1 ROUGHIF1:def 3 :
for R being finite Approximation_Space
for X, Y being Subset of R holds
( ( X \/ Y <> {} implies kappa_1 (X,Y) = (card Y) / (card (X \/ Y)) ) & ( not X \/ Y <> {} implies kappa_1 (X,Y) = 1 ) );

:: deftheorem defines kappa_2 ROUGHIF1:def 4 :
for R being finite Approximation_Space
for X, Y being Subset of R holds kappa_2 (X,Y) = (card ((X ) \/ Y)) / (card ([#] R));

definition
let R be finite Approximation_Space;
func kappa_1 R -> preRIF of R means :DefKappa1: :: ROUGHIF1:def 5
for x, y being Subset of R holds it . (x,y) = kappa_1 (x,y);
existence
ex b1 being preRIF of R st
for x, y being Subset of R holds b1 . (x,y) = kappa_1 (x,y)
proof end;
uniqueness
for b1, b2 being preRIF of R st ( for x, y being Subset of R holds b1 . (x,y) = kappa_1 (x,y) ) & ( for x, y being Subset of R holds b2 . (x,y) = kappa_1 (x,y) ) holds
b1 = b2
proof end;
func kappa_2 R -> preRIF of R means :DefKappa2: :: ROUGHIF1:def 6
for x, y being Subset of R holds it . (x,y) = kappa_2 (x,y);
existence
ex b1 being preRIF of R st
for x, y being Subset of R holds b1 . (x,y) = kappa_2 (x,y)
proof end;
uniqueness
for b1, b2 being preRIF of R st ( for x, y being Subset of R holds b1 . (x,y) = kappa_2 (x,y) ) & ( for x, y being Subset of R holds b2 . (x,y) = kappa_2 (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefKappa1 defines kappa_1 ROUGHIF1:def 5 :
for R being finite Approximation_Space
for b2 being preRIF of R holds
( b2 = kappa_1 R iff for x, y being Subset of R holds b2 . (x,y) = kappa_1 (x,y) );

:: deftheorem DefKappa2 defines kappa_2 ROUGHIF1:def 6 :
for R being finite Approximation_Space
for b2 being preRIF of R holds
( b2 = kappa_2 R iff for x, y being Subset of R holds b2 . (x,y) = kappa_2 (x,y) );

theorem Prop11a: :: ROUGHIF1:11
for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa_1 (X,Y) = 1 iff X c= Y )
proof end;

theorem Prop11b: :: ROUGHIF1:12
for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa_2 (X,Y) = 1 iff X c= Y )
proof end;

theorem LemmaProp4a: :: ROUGHIF1:13
for R being finite Approximation_Space
for X, Y being Subset of R st kappa_1 (X,Y) = 0 holds
Y = {}
proof end;

theorem Prop4a: :: ROUGHIF1:14
for R being finite Approximation_Space
for X, Y being Subset of R st X <> {} holds
( kappa_1 (X,Y) = 0 iff Y = {} )
proof end;

theorem Prop4b: :: ROUGHIF1:15
for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa_2 (X,Y) = 0 iff ( X = [#] R & Y = {} ) )
proof end;

theorem Prop2b: :: ROUGHIF1:16
for R being finite Approximation_Space
for X, Y, Z being Subset of R st Y c= Z holds
kappa_1 (X,Y) <= kappa_1 (X,Z)
proof end;

theorem Prop3b: :: ROUGHIF1:17
for R being finite Approximation_Space
for X, Y, Z being Subset of R st Y c= Z holds
kappa_2 (X,Y) <= kappa_2 (X,Z)
proof end;

theorem Lemma2: :: ROUGHIF1:18
for R being finite Approximation_Space
for X being Subset of R holds kappa_1 (({} R),X) = 1
proof end;

theorem Lemma3: :: ROUGHIF1:19
for R being finite Approximation_Space
for X being Subset of R holds kappa_2 (({} R),X) = 1
proof end;

definition
let R be non empty RelStr ;
let f be preRIF of R;
attr f is satisfying_RIF1 means :RIF1Def: :: ROUGHIF1:def 7
for X, Y being Subset of R holds
( f . (X,Y) = 1 iff X c= Y );
attr f is satisfying_RIF2 means :: ROUGHIF1:def 8
for X, Y, Z being Subset of R st Y c= Z holds
f . (X,Y) <= f . (X,Z);
attr f is satisfying_RIF3 means :: ROUGHIF1:def 9
for X being Subset of R st X <> {} holds
f . (X,({} R)) = 0 ;
attr f is satisfying_RIF4 means :: ROUGHIF1:def 10
for X, Y being Subset of R st f . (X,Y) = 0 holds
X misses Y;
end;

:: deftheorem RIF1Def defines satisfying_RIF1 ROUGHIF1:def 7 :
for R being non empty RelStr
for f being preRIF of R holds
( f is satisfying_RIF1 iff for X, Y being Subset of R holds
( f . (X,Y) = 1 iff X c= Y ) );

:: deftheorem defines satisfying_RIF2 ROUGHIF1:def 8 :
for R being non empty RelStr
for f being preRIF of R holds
( f is satisfying_RIF2 iff for X, Y, Z being Subset of R st Y c= Z holds
f . (X,Y) <= f . (X,Z) );

:: deftheorem defines satisfying_RIF3 ROUGHIF1:def 9 :
for R being non empty RelStr
for f being preRIF of R holds
( f is satisfying_RIF3 iff for X being Subset of R st X <> {} holds
f . (X,({} R)) = 0 );

:: deftheorem defines satisfying_RIF4 ROUGHIF1:def 10 :
for R being non empty RelStr
for f being preRIF of R holds
( f is satisfying_RIF4 iff for X, Y being Subset of R st f . (X,Y) = 0 holds
X misses Y );

:: Towards weak quasi-RIFs, will be developed later on
definition
let R be non empty RelStr ;
let f be preRIF of R;
attr f is satisfying_RIF0 means :: ROUGHIF1:def 11
for X, Y being Subset of R st X c= Y holds
f . (X,Y) = 1;
attr f is satisfying_RIF01 means :: ROUGHIF1:def 12
for X, Y being Subset of R st f . (X,Y) = 1 holds
X c= Y;
attr f is satisfying_RIF2* means :: ROUGHIF1:def 13
for X, Y, Z being Subset of R st f . (Y,Z) = 1 holds
f . (X,Y) <= f . (X,Z);
end;

:: deftheorem defines satisfying_RIF0 ROUGHIF1:def 11 :
for R being non empty RelStr
for f being preRIF of R holds
( f is satisfying_RIF0 iff for X, Y being Subset of R st X c= Y holds
f . (X,Y) = 1 );

:: deftheorem defines satisfying_RIF01 ROUGHIF1:def 12 :
for R being non empty RelStr
for f being preRIF of R holds
( f is satisfying_RIF01 iff for X, Y being Subset of R st f . (X,Y) = 1 holds
X c= Y );

:: deftheorem defines satisfying_RIF2* ROUGHIF1:def 13 :
for R being non empty RelStr
for f being preRIF of R holds
( f is satisfying_RIF2* iff for X, Y, Z being Subset of R st f . (Y,Z) = 1 holds
f . (X,Y) <= f . (X,Z) );

:: rif1 -> (rif2 iff rif2*)
:: qRifs are rif0 and rif2*
:: weak qRIFs are rif0 and rif2
registration
let R be non empty RelStr ;
cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF1 -> satisfying_RIF0 satisfying_RIF01 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];
coherence
for b1 being preRIF of R st b1 is satisfying_RIF1 holds
( b1 is satisfying_RIF0 & b1 is satisfying_RIF01 )
;
cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF0 satisfying_RIF01 -> satisfying_RIF1 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];
coherence
for b1 being preRIF of R st b1 is satisfying_RIF0 & b1 is satisfying_RIF01 holds
b1 is satisfying_RIF1
;
end;

registration
let R be finite Approximation_Space;
coherence
proof end;
coherence
proof end;
coherence
proof end;
coherence
proof end;
coherence
proof end;
coherence
proof end;
end;

registration
let R be finite Approximation_Space;
cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) finite satisfying_RIF1 satisfying_RIF2 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];
existence
ex b1 being preRIF of R st
( b1 is satisfying_RIF1 & b1 is satisfying_RIF2 )
proof end;
end;

theorem RIF2Iff: :: ROUGHIF1:20
for R being finite Approximation_Space
for f being satisfying_RIF1 preRIF of R holds
( f is satisfying_RIF2 iff f is satisfying_RIF2* )
proof end;

registration
let R be finite Approximation_Space;
cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF1 satisfying_RIF2 -> satisfying_RIF1 satisfying_RIF2* for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];
coherence
for b1 being satisfying_RIF1 preRIF of R st b1 is satisfying_RIF2 holds
b1 is satisfying_RIF2*
by RIF2Iff;
cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) satisfying_RIF1 satisfying_RIF2* -> satisfying_RIF1 satisfying_RIF2 for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];
coherence
for b1 being satisfying_RIF1 preRIF of R st b1 is satisfying_RIF2* holds
b1 is satisfying_RIF2
by RIF2Iff;
end;

registration
let R be finite Approximation_Space;
coherence ;
end;

registration
let R be finite Approximation_Space;
cluster V6() V18([:(bool the carrier of R),(bool the carrier of R):],[.0,1.]) finite satisfying_RIF1 satisfying_RIF2 satisfying_RIF0 satisfying_RIF2* for Element of bool [:[:(bool the carrier of R),(bool the carrier of R):],[.0,1.]:];
existence
ex b1 being preRoughInclusionFunction of R st
( b1 is satisfying_RIF0 & b1 is satisfying_RIF1 & b1 is satisfying_RIF2 & b1 is satisfying_RIF2* )
proof end;
end;

definition end;

definition end;

definition end;

:: The following three should be obvious (Proposition 3)
:: kappa R is RIF of R;
:: kappa_1 R is RIF of R;
:: kappa_2 R is RIF of R;
theorem :: ROUGHIF1:21
for R being finite Approximation_Space
for X, Z, W being Subset of R st X <> {} & Z \/ W = [#] R & Z misses W holds
(kappa (X,Z)) + (kappa (X,W)) = 1
proof end;

theorem LemmaProp2b: :: ROUGHIF1:22
for R being finite Approximation_Space
for X, Y being Subset of R st kappa (X,Y) = 0 holds
X misses Y
proof end;

theorem Prop2b: :: ROUGHIF1:23
for R being finite Approximation_Space
for X, Y being Subset of R st X <> {} holds
( kappa (X,Y) = 0 iff X misses Y )
proof end;

theorem Prop2c: :: ROUGHIF1:24
for R being finite Approximation_Space
for X being Subset of R st X <> {} holds
kappa (X,({} R)) = 0
proof end;

theorem :: ROUGHIF1:25
for R being finite Approximation_Space
for X, Y, Z being Subset of R st X <> {} & X misses Y holds
( kappa (X,(Z \ Y)) = kappa (X,(Z \/ Y)) & kappa (X,(Z \/ Y)) = kappa (X,Z) )
proof end;

Test1: for R being finite Approximation_Space
for Y, Z, W being Subset of R st Z misses W holds
kappa ((Y \/ Z),W) <= kappa (Y,W)

proof end;

Test2: for R being finite Approximation_Space
for Y, Z, W being Subset of R st Z misses W holds
kappa (Y,W) <= kappa ((Y \ Z),W)

proof end;

theorem :: ROUGHIF1:26
for R being finite Approximation_Space
for Y, Z, W being Subset of R st Z misses W holds
( kappa ((Y \/ Z),W) <= kappa (Y,W) & kappa (Y,W) <= kappa ((Y \ Z),W) ) by ;

Test1AAA: for R being finite Approximation_Space
for Y, Z, W being Subset of R st Y misses Z & Z c= W holds
kappa ((Y \/ Z),W) >= kappa (Y,W)

proof end;

Test2AAA: for R being finite Approximation_Space
for Y, Z, W being Subset of R st Y misses Z & Z c= W holds
kappa (Y,W) >= kappa ((Y \ Z),W)

proof end;

theorem :: ROUGHIF1:27
for R being finite Approximation_Space
for Y, Z, W being Subset of R st Z misses Y & Z c= W holds
( kappa ((Y \ Z),W) <= kappa (Y,W) & kappa (Y,W) <= kappa ((Y \/ Z),W) ) by ;

registration
let R be finite Approximation_Space;
let X be non empty Subset of R;
cluster kappa (X,({} R)) -> empty ;
coherence
kappa (X,({} R)) is empty
by Prop2c;
end;

theorem Kappa1RIF4: :: ROUGHIF1:28
for R being finite Approximation_Space
for X, Y being Subset of R st kappa_1 (X,Y) = 0 holds
X misses Y
proof end;

theorem Kappa2RIF4: :: ROUGHIF1:29
for R being finite Approximation_Space
for X, Y being Subset of R st kappa_2 (X,Y) = 0 holds
X misses Y
proof end;

registration
let R be finite Approximation_Space;
coherence
proof end;
coherence
proof end;
coherence
proof end;
end;

theorem :: ROUGHIF1:30
for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa (X,Y) <= kappa_1 (X,Y) & kappa_1 (X,Y) <= kappa_2 (X,Y) )
proof end;

theorem :: ROUGHIF1:31
for R being finite Approximation_Space
for X, Y being Subset of R holds kappa_1 (X,Y) = kappa ((X \/ Y),Y)
proof end;

LemmaKap1: for R being finite Approximation_Space
for X, Y being Subset of R holds kappa (X,Y) = kappa (X,(X /\ Y))

proof end;

LemmaKap2: for R being finite Approximation_Space
for X, Y being Subset of R holds kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y))

proof end;

LemmaKap3: for R being finite Approximation_Space
for X, Y being Subset of R holds kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y))

proof end;

Lemma4f1: for R being finite Approximation_Space
for X, Y being Subset of R holds kappa_2 (X,Y) = kappa (([#] R),((X ) \/ Y))

proof end;

Lemma4f2: for R being finite Approximation_Space
for X, Y being Subset of R holds kappa (([#] R),((X ) \/ Y)) = (kappa (([#] R),(X ))) + (kappa (([#] R),(X /\ Y)))

proof end;

theorem :: ROUGHIF1:32
for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa_2 (X,Y) = kappa (([#] R),((X ) \/ Y)) & kappa (([#] R),((X ) \/ Y)) = (kappa (([#] R),(X ))) + (kappa (([#] R),(X /\ Y))) ) by ;

theorem :: ROUGHIF1:33
for R being finite Approximation_Space
for X, Y being Subset of R holds
( kappa (X,Y) = kappa (X,(X /\ Y)) & kappa (X,(X /\ Y)) = kappa_1 (X,(X /\ Y)) & kappa_1 (X,(X /\ Y)) = kappa_1 ((X \ Y),(X /\ Y)) ) by ;

theorem :: ROUGHIF1:34
for R being finite Approximation_Space
for X, Y being Subset of R st X \/ Y = [#] R holds
kappa_1 (X,Y) = kappa_2 (X,Y)
proof end;

theorem :: ROUGHIF1:35
for R being finite Approximation_Space
for X, Y being Subset of R st X <> {} holds
1 - (kappa (X,Y)) = kappa (X,(Y `))
proof end;

:: are distinct -- Example 1 and 2 translated
:: calculations in Mizar seem to be too complex, my propositions are a bit
:: shorter than in the original
definition
let X be set ;
func DiscreteApproxSpace X -> strict RelStr equals :: ROUGHIF1:def 14
RelStr(# X,(id X) #);
coherence
RelStr(# X,(id X) #) is strict RelStr
;
end;

:: deftheorem defines DiscreteApproxSpace ROUGHIF1:def 14 :
for X being set holds DiscreteApproxSpace X = RelStr(# X,(id X) #);

registration
let X be set ;
coherence ;
end;

registration
let X be non empty set ;
coherence
not DiscreteApproxSpace X is empty
;
end;

registration
let X be finite set ;
coherence ;
end;

definition
correctness
coherence ;
;
end;

:: deftheorem defines ExampleRIFSpace ROUGHIF1:def 15 :
ExampleRIFSpace = DiscreteApproxSpace {1,2,3,4,5};

theorem :: ROUGHIF1:36
for X, Y being Subset of ExampleRIFSpace st X = {1,2} & Y = {2,3,4} holds
kappa (X,Y) <> kappa (Y,X)
proof end;

theorem :: ROUGHIF1:37
for X, Y, U being Subset of ExampleRIFSpace st X = {1,2} & Y = {1,2,3} & U = {2,4,5} holds
not kappa (X,U) <= kappa (Y,U)
proof end;

theorem :: ROUGHIF1:38
for X, Y being Subset of ExampleRIFSpace st X = {1,2} & Y = {2,3,4} holds
kappa (X,Y), kappa_1 (X,Y), kappa_2 (X,Y) are_mutually_distinct
proof end;

:: A Comparative Study of Some Generalized Rough Approximations"
:: Fundamenta Informaticae, 51(2002), pp. 103-119
theorem :: ROUGHIF1:39
for R being finite Approximation_Space
for u being Element of R
for x, y being Subset of R st u in (f_1 R) . x & () . u = y holds
kappa (y,x) > 0
proof end;

theorem :: ROUGHIF1:40
for R being finite Approximation_Space
for u being Element of R
for x, y being Subset of R st u in (Flip (f_1 R)) . x & () . u = y holds
kappa (y,x) = 1
proof end;