Require Import Definitions.


Section comp_assoc.
Variables A B C D : Type.
Variable r : @relation A B.
Variable r' : @relation B C.
Variable r'' : @relation C D.
Theorem composition_associativity : (r'' `o` r') `o` r == r'' `o` (r' `o` r).
proof.
have ((r'' `o` r') `o` r == {{ [a,d] | exists b : _, exists c : _, a [r] b /\ b [r'] c /\ c [r''] d }}).
then ((r'' `o` r') `o` r == {{ [a,d] | exists c : _, a [r' `o` r] c /\ c [r''] d }}).
hence ((r'' `o` r') `o` r == r'' `o` (r' `o` r)).
end proof.
Qed.
End comp_assoc.

Section identity_laws.
Variables A B : Type.
Variable r : @relation A B.

Theorem id_law_1 : forall s : set, r `o` identity s \subseteq r.
proof.
let s : (@set A).
have H1:(r `o` identity s == {{ [x,y] | x \in s /\ x [r] y }}) using myauto.
have (forall x : _, forall y : _, x \in s /\ x [r] y -> x [r] y).
then ( {{ [x,y] | x \in s /\ x [r] y }} \subseteq r) using myauto.
hence thesis by H1.
end proof.
Qed.

Theorem id_law_2 : forall S : set, identity S `o` r \subseteq r.
proof.
thus thesis using myauto.
end proof.
Qed.

Theorem id_law_3 : forall S : set, dom r \subseteq S -> r `o` identity S == r.
proof.
let s : (@set A).
assume H1: (dom r \subseteq s).
suffices to have H2 : (r \subseteq r `o` identity s) to show thesis by id_law_1, H2.
have (forall x : _, forall y : _, x [r] y -> x \in s) by H1.
then (r \subseteq {{ [x,y] | x \in s /\ x [r] y }}) using myauto.
hence thesis.
end proof.
Qed.

Theorem id_law_4 : forall S : set, ran r \subseteq S -> identity S `o` r == r.
proof.
thus thesis using myauto.
end proof.
Qed.

Section law_5.
Variable A' : Type.
Variable r' : @relation A' A'.
Theorem id_law_5 : forall S : @set A', r' \subseteq identity S <-> exists T : set, T \subseteq S /\ r' == identity T.
clear A B r.
proof.
let S : (@set A').
focus on (r' \subseteq identity S -> exists T : set, T \subseteq S /\ r' == identity T).
  assume H:(r' \subseteq identity S).
  take (dom r').
  focus on (dom r' \subseteq S).
    have (forall x : _, forall y : _, x [r'] y -> x \in S) by H.
    hence thesis.
  end focus.
  focus on (r' \subseteq identity (dom r')).
    have (forall x : _, forall y : _, x [r'] y -> x \in dom r' /\ x = y) by H.
    hence thesis using myauto.
  end focus.
  focus on (identity (dom r') \subseteq r').
    claim (forall x: _, forall y : _, x \in dom r' /\ x = y -> x [r'] y).
      given x : A', y : A' such that H1:(x \in dom r') and H2:(x=y).
      consider y' : A' such that H3:(x [r'] y') from H1.
      then (x = y') by H.
      then (y = y') by H2.
      then (x [r'] y) by H3.
      hence thesis.
    end claim.
    hence thesis using myauto.
  end focus.
end focus.
focus on ((exists T : set, T \subseteq S /\ r' == identity T) -> r' \subseteq identity S).
  given T such that H2:(T \subseteq S) and H3:(r' == identity T).
  have (identity T \subseteq identity S) by H2.
  hence thesis by H3.
end focus.
end proof.
Qed.

End law_5.

Theorem id_law_6 : forall S T : @set A, identity T `o` identity S == identity (intersect S T).
proof.
let S : (@set A), T : (@set A).
have (identity T `o` identity S == {{ [x,y] | x \in S /\ x \in T /\ x = y }}) using myauto.
then (identity T `o` identity S == {{ [x,y] | x \in (intersect S T) /\ x = y}}).
hence thesis.
end proof.
Qed.

Theorem id_law_7 : forall S : @set A, dom (identity S) == S.
proof.
let S : (@set A).
focus on (S \subseteq dom (identity S)).
  claim (forall x : _, x \in S -> exists y : _, x \in S /\ x = y).
    given x such that H:(x \in S).
    take x.
    hence thesis by H.
  end claim.
  hence thesis.
end focus.
thus thesis.
end proof.
Qed.

Theorem id_law_8 : forall S : @set A, ran (identity S) == S.
proof.
let S : (@set A).
have (ran (identity S) == {{ y | exists x : _, x \in S /\ x = y }}).
then (ran (identity S) == {{ y | y \in S }}).
hence thesis.
end proof.
Qed.

End identity_laws.

Section reflection_laws.
Variables A B C : Type.
Variable r : @relation A B.
Variable r' : @relation B C.

Theorem refl_law_1 : (r ^+) ^+ == r.
proof.
have ( (r^+)^+ == ({{ [x,y] | x [r] y }}^+)^+ ).
then ( (r^+)^+ == {{ [x,y] | y [r] x}}^+ ).
then ( (r^+)^+ == {{ [x,y] | x [r] y}} ).
hence ( (r^+)^+ == r ) using myauto.
end proof.
Qed.

Theorem refl_law_2 : (r' `o` r) ^+ == (r^+) `o` (r'^+).
proof.
have ( (r' `o` r) ^+ == {{ [z,x] | exists y : _, x [r] y /\ y [r'] z }} ).
then ( (r' `o` r) ^+ == {{ [z,x] | exists y : _, y [r^+] x /\ z [r'^+] y }} ).
then ( (r' `o` r) ^+ == {{ [z,x] | exists y : _, z [r'^+] y /\ y [r^+] x }} ).
hence thesis.
end proof.
Qed.

Theorem refl_law_3 : forall S : @set A, (identity S) ^+ == identity S.
proof.
let S : (@set A).
have ( (identity S)^+ == {{ [y,x] | x \in S /\ x = y }} ).
then ( (identity S)^+ == {{ [x,y] | y \in S /\ x = y }} ).
then ( (identity S)^+ == {{ [x,y] | x \in S /\ x = y }} ) using myauto.
hence thesis.
end proof.
Qed.

End reflection_laws.

Section additivity_laws.
Variables A B C : Type.
Variable R : @set (@relation A B).
Variable R' : @set (@relation B C).

Theorem add_law_1 : (union_of_sets R') `o` (union_of_sets R) == union_of_sets {{ r0 | exists r : relation, exists r' : relation, r0 == r' `o` r /\ r \in R /\ r' \in R' }}.
proof.
claim CL1:(forall x : _, forall z : _,
        x [union_of_sets R' `o` union_of_sets R] z ->
        x [union_of_sets {{ r0 | exists r : relation, exists r' : relation, r0 == r' `o` r /\
                                    r \in R /\ r' \in R' }}] z).
  given x : A, z : C such that H:(x [union_of_sets R' `o` union_of_sets R] z).
  consider y : B such that H1:(x [union_of_sets R] y) and H2:(y [union_of_sets R'] z) from H.
  consider r : _ such that H3:(r \in R) and H4:(x [r] y) from H1.
  consider r' : _ such that H5:(r' \in R') and H6:(y [r'] z) from H2.
  take (r' `o` r).
  hence thesis by H3, H4, H5, H6.
end claim.
hence ((union_of_sets R') `o` (union_of_sets R) \subseteq
        union_of_sets {{ r0 | exists r : relation, exists r' : relation,
                              r0 == r' `o` r /\ r \in R /\ r' \in R' }}) using myauto.
claim CL2:(forall x : _, forall z : _,
        x [union_of_sets {{ r0 | exists r : relation, exists r' : relation, r0 == r' `o` r /\
                                    r \in R /\ r' \in R' }}] z ->
        x [union_of_sets R' `o` union_of_sets R] z).
  given x : A, z : C such that H:(x [union_of_sets {{ r0 | exists r : relation, exists r' : relation, r0 == r' `o` r /\
                                    r \in R /\ r' \in R' }}] z).
  consider r0 : _ such that H1:(exists r : relation, exists r' : relation, r0 == r' `o` r /\
                                    r \in R /\ r' \in R') and H2:(x [r0] z) from H.
  consider r : _, r' : _ such that H3:(r0 == r' `o` r) and H4:(r \in R) and H5:(r' \in R') from H1.
  have H6:(exists y : _, x [r] y /\ y [r'] z) by H2, H3.
  consider y such that H7:(x [r] y) and H8:(y [r'] z) from H6.
  take y.
  take r, r'.
  hence thesis by H7, H8, H4, H5.
end claim.
hence thesis.
end proof.
Qed.

Theorem add_law_2 : (union_of_sets R) ^+ == union_of_sets {{ r0 | exists r : relation, r \in R /\ r0 == r ^+ }}.
proof.
claim (forall x : _, forall y : _,
       x [(union_of_sets R)^+] y ->
       x [(union_of_sets {{ r0 | exists r : relation, r \in R /\ r0 == r^+}})] y).
  given x, y such that H1:(x [(union_of_sets R)^+] y).
  reconsider H1 as (y [union_of_sets R] x).
  consider r : _ such that H2:(r \in R) and H3:(y [r] x) from H1.
  take (r^+).
  hence thesis by H2, H3.
end claim.
hence ((union_of_sets R) ^+ \subseteq union_of_sets {{ r0 | exists r : relation, r \in R /\ r0 == r ^+ }})
      using myauto.
claim (forall x : _, forall y : _,
       x [(union_of_sets {{ r0 | exists r : relation, r \in R /\ r0 == r^+}})] y ->
       x [(union_of_sets R)^+] y).
  given x, y such that H1:(x [union_of_sets {{ r0 | exists r : relation, r \in R /\ r0 == r^+ }}] y).
  consider r0 : _ such that H2:(exists r : relation, r \in R /\ r0 == r^+) and H3:(x [r0] y) from H1.
  consider r : _ such that H4:(r \in R) and H5:(r0 == r^+) from H2.
  reconsider thesis as (y [union_of_sets R] x).
  take r.
  have (y [r] x) by H3, H5.
  hence thesis by H4.
end claim.
hence thesis using myauto.
end proof.
Qed.

End additivity_laws.