:: Formal Development of Rough Inclusion Functions
:: by Adam Grabowski
::
:: Received August 29, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, ORDERS_2, RELAT_1, TARSKI, ZFMISC_1, XBOOLE_0,
SUBSET_1, FUNCT_1, ROUGHS_1, ROUGHS_2, ROUGHS_5, ROUGHIF1, FINSET_1,
CARD_1, REAL_1, NUMBERS, ARYTM_3, XXREAL_0, XXREAL_1, ARYTM_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, ENUMSET1, ORDINAL1,
XCMPLX_0, XXREAL_0, FINSET_1, CARD_1, XREAL_0, PARTFUN1, FUNCT_2,
RCOMP_1, STRUCT_0, ORDERS_2, ROUGHS_1, ROUGHS_2, ROUGHS_5;
constructors REALSET2, ROUGHS_1, ROUGHS_2, RCOMP_1, RVSUM_1, ROUGHS_5;
registrations XBOOLE_0, SUBSET_1, FINSET_1, NAT_1, STRUCT_0, ORDERS_2,
ROUGHS_1, CARD_1, ORDINAL1, XXREAL_0, XREAL_0, MEMBERED, FUZNORM1,
XCMPLX_0;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
begin :: Preliminaries
theorem :: ROUGHIF1:1
for a,b,c being Real st a <= b & b > 0 & c >= 0
holds a / b <= (a + c) / (b + c);
registration
cluster strict finite for Approximation_Space;
end;
registration let R be finite 1-sorted;
cluster -> finite for Subset of R;
end;
reserve R for 1-sorted;
reserve X,Y for Subset of R;
theorem :: ROUGHIF1:2
X c= Y iff X` \/ Y = [#]R;
reserve R for finite 1-sorted;
reserve X,Y for Subset of R;
theorem :: ROUGHIF1:3
card (X \/ Y) = card Y iff X c= Y;
theorem :: ROUGHIF1:4
card (X` \/ Y) = card [#]R implies X` \/ Y = [#]R;
registration let R be non empty 1-sorted;
let X be Subset of R;
reduce [#]R \/ X to [#]R;
reduce [#]R /\ X to X;
end;
begin :: Standard Rough Inclusion Function
reserve R for finite Approximation_Space;
reserve X,Y,Z,W for Subset of R;
definition let R be finite Approximation_Space;
let X,Y be Subset of R;
func kappa (X,Y) -> Element of [.0,1.] equals
:: ROUGHIF1:def 1
card (X /\ Y) / card X if X <> {}
otherwise 1;
end;
theorem :: ROUGHIF1:5
kappa ({}R,X) = 1;
theorem :: ROUGHIF1:6 :: Proposition 1 a)
kappa (X,Y) = 1 iff X c= Y;
theorem :: ROUGHIF1:7 :: Proposition 1 b)
Y c= Z implies kappa (X,Y) <= kappa (X,Z);
theorem :: ROUGHIF1:8 :: Proposition 1 c)
Z c= Y c= X implies kappa (X,Z) <= kappa (Y,Z);
theorem :: ROUGHIF1:9 :: binary variant of Proposition 1 d)
kappa (X, Y \/ Z) <= kappa (X,Y) + kappa (X,Z);
theorem :: ROUGHIF1:10 :: binary variant of Proposition 1 e)
X <> {} & Y misses Z implies
kappa (X,Y \/ Z) = kappa (X,Y) + kappa (X,Z);
begin :: Rough Inclusion Functions
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 let R be 1-sorted;
mode preRIF of R is preRoughInclusionFunction of R;
end;
scheme :: ROUGHIF1:sch 1
BinOpEq {R() -> non empty 1-sorted,
F(Subset of R(), Subset of R()) -> Element of [.0,1.]} :
for f1, f2 being preRIF of R() st
(for x,y being Subset of R() holds f1.(x,y) = F(x,y)) &
(for x,y being Subset of R() holds f2.(x,y) = F(x,y)) holds
f1 = f2;
definition let R be finite Approximation_Space;
func kappa R -> preRIF of R means
:: ROUGHIF1:def 2
for x,y being Subset of R holds it.(x,y) = kappa (x,y);
end;
begin :: Defining Two New RIFs
definition let R be finite Approximation_Space;
let X,Y be Subset of R;
func kappa_1 (X,Y) -> Element of [.0,1.] equals
:: ROUGHIF1:def 3
card Y / card (X \/ Y) if X \/ Y <> {}
otherwise 1;
func kappa_2 (X,Y) -> Element of [.0,1.] equals
:: ROUGHIF1:def 4
card (X` \/ Y) / card ([#]R);
end;
definition let R be finite Approximation_Space;
func kappa_1 R -> preRIF of R means
:: ROUGHIF1:def 5
for x,y being Subset of R holds it.(x,y) = kappa_1 (x,y);
func kappa_2 R -> preRIF of R means
:: ROUGHIF1:def 6
for x,y being Subset of R holds it.(x,y) = kappa_2 (x,y);
end;
theorem :: ROUGHIF1:11 :: rif_1 for kappa_1
kappa_1 (X,Y) = 1 iff X c= Y;
theorem :: ROUGHIF1:12 :: rif_1 for kappa_2
kappa_2 (X,Y) = 1 iff X c= Y;
theorem :: ROUGHIF1:13
kappa_1 (X,Y) = 0 implies Y = {};
theorem :: ROUGHIF1:14 :: Proposition 4 a)
X <> {} implies (kappa_1 (X,Y) = 0 iff Y = {});
theorem :: ROUGHIF1:15 :: Proposition 4 b)
kappa_2(X,Y) = 0 iff X = [#]R & Y = {};
theorem :: ROUGHIF1:16
Y c= Z implies kappa_1 (X,Y) <= kappa_1 (X,Z);
theorem :: ROUGHIF1:17
Y c= Z implies kappa_2 (X,Y) <= kappa_2 (X,Z);
theorem :: ROUGHIF1:18
kappa_1 ({}R,X) = 1;
theorem :: ROUGHIF1:19
kappa_2 ({}R,X) = 1;
definition let R be non empty RelStr;
let f be preRIF of R;
attr f is satisfying_RIF1 means
:: 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;
:: 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;
:: rif1 -> (rif2 iff rif2*)
:: qRifs are rif0 and rif2*
:: weak qRIFs are rif0 and rif2
registration let R be non empty RelStr;
cluster satisfying_RIF1 -> satisfying_RIF0 satisfying_RIF01
for preRIF of R;
cluster satisfying_RIF0 satisfying_RIF01 -> satisfying_RIF1
for preRIF of R;
end;
registration let R be finite Approximation_Space;
cluster kappa R -> satisfying_RIF1;
cluster kappa R -> satisfying_RIF2;
cluster kappa_1 R -> satisfying_RIF1;
cluster kappa_1 R -> satisfying_RIF2;
cluster kappa_2 R -> satisfying_RIF1;
cluster kappa_2 R -> satisfying_RIF2;
end;
registration let R;
cluster satisfying_RIF1 satisfying_RIF2 for preRIF of R;
end;
theorem :: ROUGHIF1:20
for f being satisfying_RIF1 preRIF of R holds
f is satisfying_RIF2 iff f is satisfying_RIF2*;
registration let R;
cluster satisfying_RIF2 -> satisfying_RIF2* for
satisfying_RIF1 preRIF of R;
cluster satisfying_RIF2* -> satisfying_RIF2 for
satisfying_RIF1 preRIF of R;
end;
registration let R;
cluster kappa R -> satisfying_RIF0 satisfying_RIF2*;
end;
registration let R;
cluster satisfying_RIF0 satisfying_RIF1 satisfying_RIF2 satisfying_RIF2* for
preRoughInclusionFunction of R;
end;
definition let R;
mode RoughInclusionFunction of R is
satisfying_RIF1 satisfying_RIF2 preRoughInclusionFunction of R;
end;
definition let R;
mode quasi-RoughInclusionFunction of R is
satisfying_RIF0 satisfying_RIF2* preRIF of R;
mode weak_quasi-RoughInclusionFunction of R is
satisfying_RIF0 satisfying_RIF2 preRIF of R;
end;
definition let R;
mode RIF of R is RoughInclusionFunction of R;
mode qRIF of R is quasi-RoughInclusionFunction of R;
mode wqRIF of R is weak_quasi-RoughInclusionFunction of R;
end;
begin :: Proposition 2
:: 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 :: Proposition 2 a), binary case
X <> {} & Z \/ W = [#]R & Z misses W implies
kappa (X,Z) + kappa (X,W) = 1;
theorem :: ROUGHIF1:22 :: Proposition 2 b) from left to right, without X <> {}
kappa (X,Y) = 0 implies X misses Y;
theorem :: ROUGHIF1:23 ::: Proposition 2 b)
X <> {} implies (kappa (X,Y) = 0 iff X misses Y);
theorem :: ROUGHIF1:24 :: Proposition 2 c)
X <> {} implies kappa (X,{}R) = 0;
theorem :: ROUGHIF1:25 :: Proposition 2 d)
X <> {} & X misses Y implies
kappa (X, Z \ Y) = kappa (X, Z \/ Y) = kappa (X,Z);
theorem :: ROUGHIF1:26 :: Proposition 2 e)
Z misses W implies
kappa (Y \/ Z, W) <= kappa (Y, W) <= kappa (Y \ Z,W);
theorem :: ROUGHIF1:27 :: Proposition 2 f)
Z misses Y & Z c= W implies
kappa (Y \ Z, W) <= kappa (Y, W) <= kappa (Y \/ Z,W);
begin :: Proposition 4
registration let R;
let X be non empty Subset of R;
cluster kappa (X,{}R) -> empty;
end;
theorem :: ROUGHIF1:28
kappa_1 (X,Y) = 0 implies X misses Y;
theorem :: ROUGHIF1:29
kappa_2 (X,Y) = 0 implies X misses Y;
registration let R; :: Proposition 4 c)
cluster kappa R -> satisfying_RIF4;
cluster kappa_1 R -> satisfying_RIF4;
cluster kappa_2 R -> satisfying_RIF4;
end;
theorem :: ROUGHIF1:30 :: Proposition 4 d)
kappa(X,Y) <= kappa_1(X,Y) <= kappa_2(X,Y);
theorem :: ROUGHIF1:31 :: Proposition 4 e)
kappa_1 (X,Y) = kappa (X \/ Y,Y);
theorem :: ROUGHIF1:32 :: Proposition 4 f)
kappa_2 (X,Y) = kappa ([#]R, X` \/ Y) =
kappa ([#]R,X`) + kappa ([#]R, X /\ Y);
theorem :: ROUGHIF1:33 :: Proposition 4 g)
kappa(X,Y) = kappa(X,X /\ Y) = kappa_1(X,X /\ Y) = kappa_1(X \ Y,X /\ Y);
theorem :: ROUGHIF1:34 :: Proposition 4 h)
X \/ Y = [#]R implies kappa_1(X,Y) = kappa_2(X,Y);
theorem :: ROUGHIF1:35 :: false for X = {}!
X <> {} implies 1 - kappa (X,Y) = kappa (X,Y`);
begin :: An Example of Aproximation Space where all three kappa mappings
:: 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 #);
end;
registration let X be set;
cluster DiscreteApproxSpace X -> with_equivalence;
end;
registration let X be non empty set;
cluster DiscreteApproxSpace X -> non empty;
end;
registration let X be finite set;
cluster DiscreteApproxSpace X -> finite;
end;
definition
func ExampleRIFSpace -> strict finite Approximation_Space equals
:: ROUGHIF1:def 15
DiscreteApproxSpace {1,2,3,4,5};
end;
theorem :: ROUGHIF1:36 :: Example 1, kappa is not symmetric
for X,Y being Subset of ExampleRIFSpace
st X = {1,2} & Y = {2,3,4} holds
kappa (X,Y) <> kappa (Y,X);
theorem :: ROUGHIF1:37 :: Example 1, kappa is not monotone wrt 1st coordinate
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);
theorem :: ROUGHIF1:38 :: Example 2, simplified: all three RIFs are different
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;
begin :: Continuing Formalization of Theorem 4.1 from Anna Gomolinska's
:: A Comparative Study of Some Generalized Rough Approximations"
:: Fundamenta Informaticae, 51(2002), pp. 103-119
theorem :: ROUGHIF1:39
::: Theorem 4.1 c) from Gomolinska's "A Comparative Study..."
for R being finite Approximation_Space,
u being Element of R,
x,y being Subset of R st
u in (f_1 R).x & (UncertaintyMap R).u = y
holds kappa (y, x) > 0;
theorem :: ROUGHIF1:40
::: Theorem 4.1 d) from Gomolinska's "A Comparative Study..."
for R being finite Approximation_Space,
u being Element of R,
x,y being Subset of R st
u in (Flip f_1 R).x & (UncertaintyMap R).u = y
holds kappa (y, x) = 1;