:: 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;