A Practical Guide To Mizar/Relations and Functions

For this section, this will be the environment used:

environ

 vocabularies XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, RELAT_1, VALUED_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, RELAT_1;
 constructors TARSKI, SUBSET_1, ZFMISC_1, XBOOLE_0, XTUPLE_0, RELAT_1;
 registrations XBOOLE_0, ZFMISC_1, RELAT_1;
 requirements SUBSET, BOOLE;
 theorems XBOOLE_0, ZFMISC_1, XTUPLE_0, RELAT_1;

begin

A relation is just a set consisting only of ordered pairs:

definition
  let IT be set;
  attr IT is Relation-like means
:: RELAT_1:def 1

  x in IT implies ex y,z st x = [y,z];
end;

registration
  cluster empty -> Relation-like for set;
end;

definition
  mode Relation is Relation-like set;
end;

where x,y,z are objects. For the rest of this section let P,Q,R denote relations. Then we can redefine P = R and P c= R as follows:

definition
  let P,R;
  redefine pred P = R means
:: RELAT_1:def 2
  for a,b holds [a,b] in P iff [a,b] in R;
end;

definition
  let P,A;
  redefine pred P c= R means
:: RELAT_1:def 3
  for a,b holds [a,b] in P implies [a,b] in R;
end;

We can also infer that the intersection and set difference of a relation with a set is a relation again:

registration
  let P;
  let X be set;
  cluster P /\ X -> Relation-like;
  coherence
  proof
    for z being object st z in P /\ X ex x,y being object st z = [x,y]
    proof
      let z be object;
      assume z in P /\ X;
      then z in P by XBOOLE_0:def 4;
      hence thesis by RELAT_1:def 1;
    end;
    hence thesis by RELAT_1:def 1;
  end;
  cluster P \ X -> Relation-like;
  coherence
  proof
    for z being object st z in P \ X ex x,y being object st z = [x,y]
    proof
      let z be object;
      assume z in P \ X;
      then z in P by XBOOLE_0:def 5;
      hence thesis by RELAT_1:def 1;
    end;
    hence thesis by RELAT_1:def 1;
  end;
end;

Similarly, the union of two relations is a relation again.

Exercise 1: Prove cluster P \/ R -> Relation-like;.

Note that the Cartesian product of two sets is of course a relation as well:

registration
  let a, b be set;
  cluster [:a,b:] -> Relation-like;
  coherence
  proof
    for z being object st z in [:a,b:] ex x,y being object st z = [x,y]
    proof
      let z be object;
      assume z in [:a,b:];
      then consider c,d being object such that
        A1: c in a & d in b & z = [c,d] by ZFMISC_1:def 2;
      take c,d;
      thus thesis by A1;
    end;
    hence thesis by RELAT_1:def 1;
  end;
end;

Of course there are functors to get the set of the first or second coordinates of a set containing pairs:

definition
  let X be set;
  func proj1 X -> set means
:: XTUPLE_0:def 12

  x in it iff ex y st [x,y] in X;
  func proj2 X -> set means
:: XTUPLE_0:def 13

  x in it iff ex y st [y,x] in X;
end;

proj is short for projection. If the set X is already a relation, we call the projection to the first coordinate the domain and the projection to the second coordinate the range (or codomain or image) of the relation:

notation
  let R be Relation;
  synonym dom R for proj1 R;
end;

notation
  let R be Relation;
  synonym rng R for proj2 R;
end;

The notation construct is useful to avoid functor definitions like e.g.

definition
  let R be Relation;
  func dom R -> set equals proj1 R;
end;

notation has the advantage that we don't need to reference a definition for Mizar to recognize the equality.

RELAT_1 (as well as XTUPLE_0) contains several statements regarding domain and range for relations, for example:

theorem :: RELAT_1:12
  rng(P \/ R) = rng P \/ rng R;

theorem :: RELAT_1:13
  rng(P /\ R) c= rng P /\ rng R;

Exercise 2: Find P,R such that the subset predicate in RELAT_1:13 becomes proper. I.e. prove ex P,R st rng(P /\ R) <> rng P /\ rng R. You can use RELAT_1:9.

The field of a relation is the union of its domain and range:

definition
  let R;
  func field R -> set equals
:: RELAT_1:def 6
  dom R \/ rng R;
end;

Exercise 3: Prove field(P \/ R) = field P \/ field R (RELAT_1:18) using XTUPLE_0:23, 27 and the commutativity (in-built) and associativity (XBOOLE_1:4) law of the set union.

Exercise 1:

registration
  let P,R;
  cluster P \/ R -> Relation-like;
  coherence
  proof
    for z being object st z in P \/ R ex x,y being object st z = [x,y]
    proof
      let z be object;
      assume z in P \/ R;
      then per cases by XBOOLE_0:def 3;
      suppose z in P;
        hence thesis by RELAT_1:def 1;
      end;
      suppose z in R;
        hence thesis by RELAT_1:def 1;
      end;
    end;
    hence thesis by RELAT_1:def 1;
  end;
end;

Exercise 2:

ex P,R st rng(P /\ R) <> rng P /\ rng R
proof
  set a = {}, b = {{}};
  set P = {[b,a]}, R = {[a,a]};
  take P,R;
  [b,a] <> [a,a] by XTUPLE_0:1;
  then P misses R by ZFMISC_1:11;
  then P /\ R = {} by XBOOLE_0:def 7;
  then A1: rng(P /\ R) = {};
  rng P /\ rng R = {a} /\ rng R by RELAT_1:9
    .= {a} /\ {a} by RELAT_1:9;
  hence thesis by A1;
end;

Exercise 3:

field(P \/ R) = field P \/ field R
proof
  thus field(P \/ R) = dom(P \/ R) \/ rng(P \/ R) by RELAT_1:def 6
    .= dom P \/ dom R \/ rng(P \/ R) by XTUPLE_0:23
    .= dom P \/ dom R \/ (rng P \/ rng R) by XTUPLE_0:27
    .= dom P \/ (dom R \/ (rng P \/ rng R)) by XBOOLE_1:4
    .= dom P \/ (rng P \/ dom R \/ rng R) by XBOOLE_1:4
    .= dom P \/ (rng P \/ (dom R \/ rng R)) by XBOOLE_1:4
    .= dom P \/ (rng P \/ field R) by RELAT_1:def 6
    .= (dom P \/ rng P) \/ field R by XBOOLE_1:4
    .= field P \/ field R by RELAT_1:def 6;
end;