:: Binary Relations-Based Rough Sets -- An Automated Approach :: by Adam Grabowski :: :: Received February 15, 2016 :: Copyright (c) 2016-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, CARD_3, RELAT_2, XBOOLE_0, PARTFUN1, SUBSET_1, FUNCT_1, EQREL_1, XXREAL_0, ROUGHS_1, ROUGHS_2, FINSET_1, ROUGHS_3, ROUGHS_4, COHSP_1, FUNCT_2, FINSUB_1, SETWISEO, ALTCAT_2, CLASSES1, NATTRA_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FINSET_1, FINSUB_1, SETWISEO, CLASSES1, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, EQREL_1, ORDERS_3, ROUGHS_1, ROUGHS_2, ALTCAT_2, COHSP_1, ROUGHS_4; constructors EQREL_1, DOMAIN_1, RELSET_1, ROUGHS_1, SETWISEO, COHSP_1, ORDERS_3, YELLOW_3, ROUGHS_2, ROUGHS_4, ALTCAT_2; registrations XBOOLE_0, SUBSET_1, RELAT_1, STRUCT_0, ORDERS_2, RELSET_1, ROUGHS_1, ROUGHS_2, FINSET_1, ROUGHS_4, FUNCT_2, SETWISEO, COHSP_1, WAYBEL_8; requirements BOOLE, SUBSET; begin :: Preliminaries :: The aim of this Mizar article is to provide a formal counterpart :: for the rest of the paper of William Zhu "Generalized Rough Sets :: Based on Relations", Information Sciences, 177, 2007, pp. 4997--5011. :: The first part of our formalization (covering first seven pages) :: is contained in ROUGHS_2. Now we start from page 5003, sec. 3.4. :: We formalized almost all numbered items (definitions, propositions, :: theorems, and corollaries), with the exception of Proposition 7, :: where we stated our theorem only in terms of singletons. :: We provided more thorough discussion of the property "positive_alliance" :: and its connection with seriality and reflexivity (and also transitivity). :: Examples were not covered as a rule as we aim to provide a more :: general mechanism of finding appropriate models for approximation :: spaces in Mizar providing more automatization than it is now. reserve X,a,b,c,x,y,z,t for set; reserve R for Relation; registration let X be non empty set; cluster bool X -> d.union-closed; end; scheme :: ROUGHS_3:sch 1 :: SETWISEO:sch 2 revised FinSubIndA1{ X() -> non empty finite set, P[Subset of X()] } : for B being Subset of X() holds P[B] provided P[{}X()] and for B9 being Subset of X(), b being Element of X() holds P[B9] & not b in B9 implies P[B9 \/ {b}]; scheme :: ROUGHS_3:sch 2 :: similar to SETWISEO:sch 3 FinSubIndA2 { X() -> non empty finite set, P[Subset of X()] } : for B being non empty Subset of X() holds P[B] provided for x being Element of X() holds P[{x}] and for B1,B2 being non empty Subset of X() st P[B1] & P[B2] holds P[B1 \/ B2]; theorem :: ROUGHS_3:1 for f being Function st dom f is subset-closed & dom f is d.union-closed & f is d.union-distributive holds for a, y being set st a in dom f & y in f.a ex b being set st b is finite & b c= a & y in f.b; theorem :: ROUGHS_3:2 for f being Function st dom f is subset-closed & f is union-distributive & dom f is d.union-closed holds for a, y being set st a in dom f & y in f.a ex x being set st x in a & y in f.{x}; begin :: On the Union and the Intersection of Two Relational Structures ::: Should be consulted with PCS_0 definition let R1, R2 be RelStr; func Union (R1,R2) -> strict RelStr means :: ROUGHS_3:def 1 the carrier of it = (the carrier of R1) \/ the carrier of R2 & the InternalRel of it = (the InternalRel of R1) \/ the InternalRel of R2; commutativity; func Meet (R1,R2) -> strict RelStr means :: ROUGHS_3:def 2 the carrier of it = (the carrier of R1) /\ the carrier of R2 & the InternalRel of it = (the InternalRel of R1) /\ the InternalRel of R2; commutativity; end; registration let R1 be RelStr, R2 be non empty RelStr; cluster Union (R1,R2) -> non empty; end; begin :: Ordinary Properties of Maps registration let A be set; cluster /\-preserving \/-preserving for Function of bool A, bool A; end; registration let A be set; let f be /\-preserving Function of bool A, bool A; cluster Flip f -> \/-preserving; end; registration let A be set; let f be \/-preserving Function of bool A, bool A; cluster Flip f -> /\-preserving; end; theorem :: ROUGHS_3:3 for A being non empty set for f, g being Function of bool A, bool A st f cc= g holds Flip g cc= Flip f; registration cluster non empty mediate transitive for RelStr; end; registration let R be total mediate RelStr; cluster the InternalRel of R -> mediate; end; theorem :: ROUGHS_3:4 for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1 is mediate holds L2 is mediate; theorem :: ROUGHS_3:5 for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1 is serial holds L2 is serial; theorem :: ROUGHS_3:6 :: dual version of ROUGHS_2:24 for A being non empty set, L, U being Function of bool A, bool A st U = Flip L & for X being Subset of A holds L.X c= L.(L.X) holds for X being Subset of A holds U.(U.X) c= U.X; theorem :: ROUGHS_3:7 for R being non empty RelStr, a, b being Element of R st [a,b] in the InternalRel of R holds a in UAp {b}; theorem :: ROUGHS_3:8 for R being non empty RelStr, A, B being Subset of R holds (UAp R).(A \/ B) = (UAp R).A \/ (UAp R).B; theorem :: ROUGHS_3:9 for R being non empty RelStr, A, B being Subset of R holds (LAp R).(A /\ B) = (LAp R).A /\ (LAp R).B; theorem :: ROUGHS_3:10 for R being non empty RelStr holds (UAp R).{} = {}; theorem :: ROUGHS_3:11 for R1, R2 being non empty RelStr, X being Subset of R1, Y being Subset of R2 st the RelStr of R1 = the RelStr of R2 & X = Y holds UAp X = UAp Y; theorem :: ROUGHS_3:12 for R1, R2 being non empty RelStr, X being Subset of R1, Y being Subset of R2 st the RelStr of R1 = the RelStr of R2 & X = Y holds LAp X = LAp Y; begin :: On the Relational Structure Generated by Rough Approximation definition let R be non empty RelStr, H be Function of bool the carrier of R, bool the carrier of R; func GeneratedRelation (R,H) -> Relation of the carrier of R means :: ROUGHS_3:def 3 for x,y being Element of R holds [x,y] in it iff x in H.{y}; end; definition let R be non empty RelStr; let H be Function of bool the carrier of R, bool the carrier of R; func GeneratedRelStr (H) -> RelStr equals :: ROUGHS_3:def 4 RelStr (#the carrier of R, GeneratedRelation (R,H)#); end; registration let R be non empty RelStr; let H be Function of bool the carrier of R, bool the carrier of R; cluster GeneratedRelStr (H) -> non empty; end; theorem :: ROUGHS_3:13 for R being finite non empty RelStr, H being Function of bool the carrier of R, bool the carrier of R st H.{} = {} & H is \/-preserving holds UAp GeneratedRelStr H = H; begin :: Construction Revisited: Yao's Theorem 3 theorem :: ROUGHS_3:14 :: Yao Theorem 3 for A being finite non empty set, L, H being Function of bool A, bool A st L = Flip H holds :: (L.A = A & :: (for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) & (H.{} = {} & (for X,Y being Subset of A holds H.(X \/ Y) = H.X \/ H.Y)) iff ex R being non empty finite RelStr st the carrier of R = A & LAp R = L & UAp R = H & for x,y being Element of R holds [x,y] in the InternalRel of R iff x in H.{y}; begin :: Transitive Binary Relations theorem :: ROUGHS_3:15 :: Proposition 9 (5L") for R being non empty transitive RelStr, X being Subset of R holds LAp X c= LAp (LAp X); theorem :: ROUGHS_3:16 :: Proposition 9 (5H") for R being non empty transitive RelStr, X being Subset of R holds UAp (UAp X) c= UAp X; theorem :: ROUGHS_3:17 :: Proposition 9 L for A being finite non empty set, L being Function of bool A, bool A st L.A = A & (for X being Subset of A holds L.X c= L.(L.X)) & (for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds ex R being non empty finite transitive RelStr st the carrier of R = A & L = LAp R; theorem :: ROUGHS_3:18 :: Proposition 9 H for A being non empty finite set, U being Function of bool A, bool A st U.{} = {} & (for X being Subset of A holds U.(U.X) c= U.X) & (for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds ex R being non empty finite transitive RelStr st the carrier of R = A & U = UAp R; begin :: Mediate and Transitive Binary Relations theorem :: ROUGHS_3:19 :: Theorem 1 (5L) for R being non empty mediate transitive RelStr, X being Subset of R holds LAp X = LAp (LAp X); theorem :: ROUGHS_3:20 :: Theorem 1 (5H) for R being non empty mediate transitive RelStr, X being Subset of R holds UAp X = UAp (UAp X); theorem :: ROUGHS_3:21 :: Theorem 1 L for A being non empty finite set, L being Function of bool A, bool A st L.A = A & (for X being Subset of A holds L.X = L.(L.X)) & (for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds ex R being non empty mediate finite transitive RelStr st the carrier of R = A & L = LAp R; theorem :: ROUGHS_3:22 :: Theorem 1 H for A being non empty finite set, U being Function of bool A, bool A st U.{} = {} & (for X being Subset of A holds U.(U.X) = U.X) & (for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds ex R being non empty mediate finite transitive RelStr st the carrier of R = A & U = UAp R; begin :: Alliance Binary Relations :: (7L) L(-L(X)) = -L(X) :: (7L') L(-L(X)) c= -L(X) :: (7L") -L(X) c= L(-L(X)) :: (7H) H(-H(X)) = -H(X) :: (7H') H(-H(X)) c= -H(X) :: (7H") -H(X) c= H(-H(X)) definition let X be set, R be Relation of X; pred R is_positive_alliance_in X means :: ROUGHS_3:def 5 :: Definition 3 for x,y being object st x in X & y in X & not [x,y] in R holds ex z being object st z in X & [x,z] in R & not [z,y] in R; pred R is_negative_alliance_in X means :: ROUGHS_3:def 6 :: Definition 4 for x,y being object st x in X & y in X holds (ex z being object st z in X & [x,z] in R & not [z,y] in R) implies not [x,y] in R; end; definition let X be set, R be Relation of X; pred R is_alliance_in X means :: ROUGHS_3:def 7 :: Definition 5 R is_negative_alliance_in X & R is_positive_alliance_in X; end; definition let R be non empty RelStr; attr R is positive_alliance means :: ROUGHS_3:def 8 the InternalRel of R is_positive_alliance_in the carrier of R; attr R is negative_alliance means :: ROUGHS_3:def 9 the InternalRel of R is_negative_alliance_in the carrier of R; attr R is alliance means :: ROUGHS_3:def 10 the InternalRel of R is_alliance_in the carrier of R; end; registration cluster reflexive -> positive_alliance for non empty RelStr; cluster discrete -> negative_alliance for non empty RelStr; end; registration cluster positive_alliance negative_alliance for non empty RelStr; end; registration cluster alliance -> positive_alliance negative_alliance for non empty RelStr; cluster positive_alliance negative_alliance -> alliance for non empty RelStr; end; :: But soon we realized a more general proof can be provided registration cluster positive_alliance -> serial for non empty RelStr; cluster transitive serial -> positive_alliance for non empty RelStr; end; theorem :: ROUGHS_3:23 for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr of L2 & L1 is negative_alliance holds L2 is negative_alliance; theorem :: ROUGHS_3:24 for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr of L2 & L1 is positive_alliance holds L2 is positive_alliance; theorem :: ROUGHS_3:25 for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr of L2 & L1 is alliance holds L2 is alliance; begin :: Preparation for Translation of Proposition 10 (7H') definition let R be non empty RelStr; attr R is satisfying(7H') means :: ROUGHS_3:def 11 for X being Subset of R holds (UAp X)` c= UAp ((UAp X)`); attr R is satisfying(7L') means :: ROUGHS_3:def 12 for X being Subset of R holds LAp ((LAp X)`) c= (LAp X)`; end; theorem :: ROUGHS_3:26 for R being finite non empty RelStr st R is satisfying(7L') holds R is satisfying(7H'); theorem :: ROUGHS_3:27 :: Unexpected as seriality can be then proven for R being finite non empty RelStr st R is satisfying(7H') holds R is serial; theorem :: ROUGHS_3:28 for R being finite non empty RelStr st R is satisfying(7L') holds R is serial; registration cluster satisfying(7H') -> serial for finite non empty RelStr; end; theorem :: ROUGHS_3:29 for R being non empty RelStr st (for X being Subset of R holds UAp ((UAp X)`) c= (UAp X)`) holds for X being Subset of R holds (LAp X)` c= LAp ((LAp X)`); theorem :: ROUGHS_3:30 for A being non empty set, L, U being Function of bool A, bool A st U = Flip L & (for X being Subset of A holds (L.X)` c= L.((L.X)`)) holds for X being Subset of A holds U.((U.X)`) c= (U.X)`; theorem :: ROUGHS_3:31 for A being non empty set, L, U being Function of bool A, bool A st U = Flip L & (for X being Subset of A holds U.((U.X)`) c= (U.X)`) holds for X being Subset of A holds (L.X)` c= L.((L.X)`); theorem :: ROUGHS_3:32 for A being non empty set, L, U being Function of bool A, bool A st U = Flip L & (for X being Subset of A holds L.((L.X)`) c= (L.X)`) holds for X being Subset of A holds (U.X)` c= U.((U.X)`); ::theorem :: Obvious due to the mechanism of clusters :: for R being non empty RelStr holds :: UAp ((UAp ({}R))`) c= (UAp ({}R))`; begin :: Translation Continued theorem :: ROUGHS_3:33 :: Proposition 10 (7H') for singletons for R being finite positive_alliance non empty RelStr, x being Element of R holds ((UAp R).{x})` c= (UAp R).(((UAp R).{x})`); ::theorem :: Proposition 10 (7H') general case - FAILED :: for R being finite positive_alliance non empty RelStr, :: X being Subset of R holds :: ((UAp R).X)` c= (UAp R).(((UAp R).X)`); theorem :: ROUGHS_3:34 :: Proposition 11 for A being non empty finite set, U being Function of bool A, bool A st U.{} = {} & (for X being Subset of A holds (U.X)` c= U.((U.X)`)) & (for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds ex R being positive_alliance finite non empty RelStr st the carrier of R = A & U = UAp R; theorem :: ROUGHS_3:35 :: Proposition 12 for A being non empty finite set, L being Function of bool A, bool A st L.A = A & (for X being Subset of A holds L.((L.X)`) c= (L.X)`) & (for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds ex R being positive_alliance finite non empty RelStr st the carrier of R = A & L = LAp R; theorem :: ROUGHS_3:36 :: Proposition 13 (7H") for singletons - original proofs for R being finite negative_alliance non empty RelStr, x being Element of R holds (UAp R).(((UAp R).{x})`) c= ((UAp R).{x})`; theorem :: ROUGHS_3:37 :: Proposition 13 (7H") for R being finite negative_alliance non empty RelStr, X being Subset of R holds UAp ((UAp X)`) c= (UAp X)`; theorem :: ROUGHS_3:38 :: Proposition 13 (7L") for R being finite negative_alliance non empty RelStr, X being Subset of R holds (LAp X)` c= LAp ((LAp X)`); theorem :: ROUGHS_3:39 :: Proposition 14 for A being non empty finite set, U being Function of bool A, bool A st U.{} = {} & (for X being Subset of A holds U.((U.X)`) c= (U.X)`) & (for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds ex R being negative_alliance finite non empty RelStr st the carrier of R = A & U = UAp R; theorem :: ROUGHS_3:40 :: Proposition 15 for A being non empty finite set, L being Function of bool A, bool A st L.A = A & (for X being Subset of A holds (L.X)` c= L.((L.X)`)) & (for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds ex R being negative_alliance finite non empty RelStr st the carrier of R = A & L = LAp R; :: Theorem 2 (7H) left without a proof theorem :: ROUGHS_3:41 :: Theorem 2 (H) for A being non empty finite set, U being Function of bool A, bool A st U.{} = {} & (for X being Subset of A holds U.((U.X)`) = (U.X)`) & (for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds ex R being alliance finite non empty RelStr st the carrier of R = A & U = UAp R; theorem :: ROUGHS_3:42 :: Theorem 2 (L) for A being non empty finite set, L being Function of bool A, bool A st L.A = A & (for X being Subset of A holds (L.X)` = L.((L.X)`)) & (for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds ex R being alliance finite non empty RelStr st the carrier of R = A & L = LAp R; begin :: On the Uniqueness of Binary Relations to Generate Rough Sets theorem :: ROUGHS_3:43 :: Theorem 3 (H) for R1, R2, R being non empty RelStr, X being Subset of R, X1 being Subset of R1, X2 being Subset of R2 st R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds UAp X = UAp X1 \/ UAp X2; theorem :: ROUGHS_3:44 :: Theorem 3 (L) for R1, R2, R being non empty RelStr, X being Subset of R, X1 being Subset of R1, X2 being Subset of R2 st R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds LAp X = LAp X1 /\ LAp X2; theorem :: ROUGHS_3:45 :: Proposition 16 (H) for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 holds UAp R1 cc= UAp R2; theorem :: ROUGHS_3:46 :: Proposition 16 (L) for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 holds LAp R2 cc= LAp R1; theorem :: ROUGHS_3:47 :: Theorem 4 (H) for R1, R2, R being non empty RelStr, X being Subset of R, X1 being Subset of R1, X2 being Subset of R2 st R = Meet (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds UAp X c= UAp X1 /\ UAp X2; theorem :: ROUGHS_3:48 :: Theorem 4 (L) for R1, R2, R being non empty RelStr, X being Subset of R, X1 being Subset of R1, X2 being Subset of R2 st R = Meet (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds LAp X1 \/ LAp X2 c= LAp X; theorem :: ROUGHS_3:49 :: Proposition 17 for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 & UAp R1 cc= UAp R2 holds the InternalRel of R1 c= the InternalRel of R2; theorem :: ROUGHS_3:50 :: Corollary 3 for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 & UAp R1 = UAp R2 holds the InternalRel of R1 = the InternalRel of R2; theorem :: ROUGHS_3:51 :: Theorem 5 for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 holds UAp R1 = UAp R2 iff the InternalRel of R1 = the InternalRel of R2; theorem :: ROUGHS_3:52 :: Proposition 18 for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 & LAp R1 cc= LAp R2 holds the InternalRel of R2 c= the InternalRel of R1; theorem :: ROUGHS_3:53 :: Corollary 4 for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 & LAp R1 = LAp R2 holds the InternalRel of R2 = the InternalRel of R1; theorem :: ROUGHS_3:54 :: Theorem 6 for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 holds LAp R1 = LAp R2 iff the InternalRel of R1 = the InternalRel of R2;