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.
myauto.
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.
myauto.
Qed.

Theorem id_law_2 : forall S : set, identity S `o` r \subseteq r.
myauto.
Qed.

Theorem id_law_3 : forall S : set, dom r \subseteq S -> r `o` identity S == r.
myauto.
Qed.

Theorem id_law_4 : forall S : set, ran r \subseteq S -> identity S `o` r == r.
myauto.
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.
myauto; exists (dom r'); myauto.
Qed.
End law_5.

Theorem id_law_6 : forall S T : @set A, identity T `o` identity S == identity (intersect S T).
myauto.
Qed.

Theorem id_law_7 : forall S : @set A, dom (identity S) == S.
myauto.
Qed.

Theorem id_law_8 : forall S : @set A, ran (identity S) == S.
myauto.
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.
myauto.
Qed.

Theorem refl_law_2 : (r' `o` r) ^+ == (r^+) `o` (r'^+).
myauto.
Qed.

Theorem refl_law_3 : forall S : @set A, (identity S) ^+ == identity S.
myauto.
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' }}.
myauto;
  (match goal with
    | [ r : set, r' : set, H : ?r \in R, H' : ?r' \in R' |- @ex set ?P ] => exists (r' `o` r)
  end);
myauto.
Qed.

Theorem add_law_2 : (union_of_sets R) ^+ == union_of_sets {{ r0 | exists r : relation, r \in R /\ r0 == r ^+ }}.
myauto; 
  (match goal with
     | [ r : set, H : ?r \in R |- @ex set ?P ] => exists (r^+)
   end);
myauto.
Qed.

End additivity_laws.