include "datatypes/subsets.ma".
-record binary_relation (A,B: Type) : Type ≝
- { satisfy:2> A → B → CProp }.
+record binary_relation (A,B: setoid) : Type ≝
+ { satisfy:> binary_morphism1 A B CPROP }.
notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{'satisfy $r $x $y}.
notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}.
-interpretation "relation applied" 'satisfy r x y = (satisfy __ r x y).
+interpretation "relation applied" 'satisfy r x y = (fun1 ___ (satisfy __ r) x y).
-definition composition:
- ∀A,B,C.
- binary_relation A B → binary_relation B C →
- binary_relation A C.
- intros (A B C R12 R23);
+definition binary_relation_setoid: setoid → setoid → setoid1.
+ intros (A B);
constructor 1;
- 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.λr,r': binary_relation A B.
- ∀x,y. r x y ↔ r' x y.
-
-interpretation "equal relation" 'eq x y = (equal_relations __ x y).
-
-lemma refl_equal_relations: ∀A,B. reflexive ? (equal_relations A B).
- intros 3; intros 2; split; intro; assumption.
-qed.
-
-lemma sym_equal_relations: ∀A,B. symmetric ? (equal_relations A B).
- intros 5; intros 2; split; intro;
- [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption.
-qed.
-
-lemma trans_equal_relations: ∀A,B. transitive ? (equal_relations A B).
- intros 7; 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.
- ∀r1:binary_relation A B.
- ∀r2:binary_relation B C.
- ∀r3:binary_relation C D.
- (r1 ∘ r2) ∘ r3 = r1 ∘ (r2 ∘ r3).
- intros 9;
- 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.
+ [ 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]]
qed.
-lemma composition_morphism:
+definition composition:
∀A,B,C.
- ∀r1,r1':binary_relation A B.
- ∀r2,r2':binary_relation B C.
- r1 = r1' → r2 = r2' → r1 ∘ r2 = r1' ∘ r2'.
- intros 11; 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.
-qed.
-
-definition binary_relation_setoid: Type → Type → setoid.
- intros (A B);
+ binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C).
+ intros;
constructor 1;
- [ apply (binary_relation A B)
- | constructor 1;
- [ apply equal_relations
- | apply refl_equal_relations
- | apply sym_equal_relations
- | apply trans_equal_relations
- ]]
+ [ intros (R12 R23);
+ constructor 1;
+ constructor 1;
+ [ apply (λs1:A.λs3:C.∃s2:B. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
+ | intros;
+ split; intro; cases H2 (w H3); clear H2; exists; [1,3: apply w ]
+ [ apply (. (H‡#)‡(#‡H1)); assumption
+ | apply (. ((H \sup -1)‡#)‡(#‡(H1 \sup -1))); assumption]]
+ | intros 8; split; intro H2; simplify in H2 ⊢ %;
+ cases H2 (w H3); clear H2; exists [1,3: apply w] cases H3 (H2 H4); 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]
qed.
-definition REL: category.
+definition REL: category1.
constructor 1;
- [ apply Type
- | intros; apply (binary_relation_setoid T T1)
- | intros; constructor 1; intros; apply (eq ? o1 o2);
+ [ apply setoid
+ | intros (T T1); apply (binary_relation_setoid T T1)
| intros; constructor 1;
- [ apply composition
- | apply composition_morphism
- ]
- | intros; unfold mk_binary_morphism; simplify;
- apply associative_composition
- |6,7: intros 5; simplify; split; intro;
- [1,3: cases H; clear H; cases H1; clear H1;
- [ alias id "eq_elim_r''" = "cic:/matita/logic/equality/eq_elim_r''.con".
- apply (eq_elim_r'' ? w ?? x H); assumption
- | alias id "eq_rect" = "cic:/matita/logic/equality/eq_rect.con".
- apply (eq_rect ? w ?? y H2); assumption ]
- assumption
- |*: exists; try assumption; split;
- alias id "refl_eq" = "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)".
- first [ apply refl_eq | assumption ]]]
+ constructor 1; unfold setoid1_of_setoid; simplify;
+ [ intros; apply (c = c1)
+ | intros; split; intro;
+ [ apply (trans ????? (H \sup -1));
+ apply (trans ????? H2);
+ apply H1
+ | apply (trans ????? H);
+ apply (trans ????? H2);
+ apply (H1 \sup -1)]]
+ | apply composition
+ | intros 9;
+ split; intro;
+ cases f (w H); clear f; cases H; clear H;
+ [cases f (w1 H); clear f | cases f1 (w1 H); clear f1]
+ cases H; clear H;
+ exists; try assumption;
+ split; try assumption;
+ exists; try assumption;
+ split; assumption
+ |6,7: intros 5; unfold composition; simplify; split; intro;
+ unfold setoid1_of_setoid in x y; simplify in x y;
+ [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold;
+ [ apply (. (H \sup -1 : eq1 ? w x)‡#); assumption
+ | apply (. #‡(H : eq1 ? w y)); assumption]
+ |2,4: exists; try assumption; split; first [apply refl | assumption]]]
qed.
-definition full_subset: ∀s:REL. Ω \sup s ≝ λs.{x | True}.
+definition full_subset: ∀s:REL. Ω \sup s.
+ apply (λs.{x | True});
+ intros; simplify; split; intro; assumption.
+qed.
+
+coercion full_subset.
+
+definition setoid1_of_REL: REL → setoid ≝ λS. S.
-coercion full_subset.
\ No newline at end of file
+coercion setoid1_of_REL.
\ No newline at end of file
projects / helm.git / blobdiff