- intros (s1 s3);
- apply (∃s2. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
-qed.
-
-interpretation "binary relation composition" 'compose x y = (composition ______ x y).
-
-definition equal_relations ≝
- λA,B,U,V.λr,r': binary_relation A B U V.
- ∀x,y. r x y ↔ r' x y.
-
-interpretation "equal relation" 'eq x y = (equal_relations ____ x y).
-
-lemma refl_equal_relations: ∀A,B,U,V. reflexive ? (equal_relations A B U V).
- intros 5; intros 2; split; intro; assumption.
-qed.
-
-lemma sym_equal_relations: ∀A,B,U,V. symmetric ? (equal_relations A B U V).
- intros 7; intros 2; split; intro;
- [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption.
-qed.
-
-lemma trans_equal_relations: ∀A,B,U,V. transitive ? (equal_relations A B U V).
- intros 9; intros 2; split; intro;
- [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
- [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
- assumption.
-qed.
-
-lemma associative_composition:
- ∀A,B,C,D.∀U1,U2,U3,U4.
- ∀r1:binary_relation A B U1 U2.
- ∀r2:binary_relation B C U2 U3.
- ∀r3:binary_relation C D U3 U4.
- (r1 ∘ r2) ∘ r3 = r1 ∘ (r2 ∘ r3).
- intros 13;
- split; intro;
- cases H; clear H; cases H1; clear H1;
- [cases H; clear H | cases H2; clear H2]
- cases H1; clear H1;
- exists; try assumption;
- split; try assumption;
- exists; try assumption;
- split; assumption.
-qed.
-
-lemma composition_morphism:
- ∀A,B,C.∀U1,U2,U3.
- ∀r1,r1':binary_relation A B U1 U2.
- ∀r2,r2':binary_relation B C U2 U3.
- r1 = r1' → r2 = r2' → r1 ∘ r2 = r1' ∘ r2'.
- intros 14; split; intro;
- cases H2; clear H2; cases H3; clear H3;
- [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
- [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
- exists; try assumption;
- split; assumption.
+ [ apply (binary_relation A B)
+ | constructor 1;
+ [ apply (λA,B.λr,r': binary_relation A B. ∀x,y. r x y ↔ r' x y)
+ | simplify; intros 3; split; intro; assumption
+ | simplify; intros 5; split; intro;
+ [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption
+ | simplify; intros 7; split; intro;
+ [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
+ [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
+ assumption]]