(* *)
(**************************************************************************)
-include "datatypes/subsets.ma".
-include "logic/cprop_connectives.ma".
-include "formal_topology/categories.ma".
-
-record basic_pair: Type ≝
- { carr1: Type;
- carr2: Type;
- concr: Ω \sup carr1;
- form: Ω \sup carr2;
- rel: binary_relation ?? concr form
- }.
+include "formal_topology/relations.ma".
+include "formal_topology/notation.ma".
-notation "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y}.
-notation "⊩" with precedence 60 for @{'Vdash}.
+record basic_pair: Type1 ≝ {
+ concr: REL; form: REL; rel: concr ⇒_\r1 form
+}.
-interpretation "basic pair relation" 'Vdash2 x y = (rel _ x y).
-interpretation "basic pair relation (non applied)" 'Vdash = (rel _).
+interpretation "basic pair relation" 'Vdash2 x y c = (fun21 ??? (rel c) x y).
+interpretation "basic pair relation (non applied)" 'Vdash c = (rel c).
-alias symbol "eq" = "equal relation".
-alias symbol "compose" = "binary relation composition".
-record relation_pair (BP1,BP2: basic_pair): Type ≝
- { concr_rel: binary_relation ?? (concr BP1) (concr BP2);
- form_rel: binary_relation ?? (form BP1) (form BP2);
- commute: concr_rel ∘ ⊩ = ⊩ ∘ form_rel
+record relation_pair (BP1,BP2: basic_pair): Type1 ≝ {
+ concr_rel: (concr BP1) ⇒_\r1 (concr BP2); form_rel: (form BP1) ⇒_\r1 (form BP2);
+ commute: comp1 REL ??? concr_rel (rel ?) =_1 form_rel ∘ ⊩
}.
-notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}.
-notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}.
-
-interpretation "concrete relation" 'concr_rel r = (concr_rel __ r).
-interpretation "formal relation" 'form_rel r = (form_rel __ r).
-
+interpretation "concrete relation" 'concr_rel r = (concr_rel ?? r).
+interpretation "formal relation" 'form_rel r = (form_rel ?? r).
-definition relation_pair_equality:
- ∀o1,o2. equivalence_relation (relation_pair o1 o2).
- intros;
- constructor 1;
- [ apply (λr,r'. r \sub\c ∘ ⊩ = r' \sub\c ∘ ⊩);
- | simplify;
- intros;
- apply refl_equal_relations;
- | simplify;
- intros;
- apply sym_equal_relations;
- assumption
- | simplify;
- intros;
- apply (trans_equal_relations ??????? H);
- assumption
- ]
+definition relation_pair_equality: ∀o1,o2. equivalence_relation1 (relation_pair o1 o2).
+ intros; constructor 1; [ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c);
+ | simplify; intros; apply refl1;
+ | simplify; intros 2; apply sym1;
+ | simplify; intros 3; apply trans1; ]
qed.
-definition relation_pair_setoid: basic_pair → basic_pair → setoid.
+definition relation_pair_setoid: basic_pair → basic_pair → setoid1.
intros;
constructor 1;
[ apply (relation_pair b b1)
]
qed.
-definition eq' ≝
- λo1,o2.λr,r':relation_pair o1 o2.⊩ ∘ r \sub\f = ⊩ ∘ r' \sub\f.
-
-alias symbol "eq" = "setoid eq".
-lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → eq' ?? r r'.
- intros 7 (o1 o2 r r' H c1 f2);
- split; intro;
- [ lapply (fi ?? (commute ?? r c1 f2) H1) as H2;
- lapply (if ?? (H c1 f2) H2) as H3;
- apply (if ?? (commute ?? r' c1 f2) H3);
- | lapply (fi ?? (commute ?? r' c1 f2) H1) as H2;
- lapply (fi ?? (H c1 f2) H2) as H3;
- apply (if ?? (commute ?? r c1 f2) H3);
- ]
+definition relation_pair_of_relation_pair_setoid :
+ ∀P,Q. relation_pair_setoid P Q → relation_pair P Q ≝ λP,Q,x.x.
+coercion relation_pair_of_relation_pair_setoid.
+
+alias symbol "compose" (instance 1) = "category1 composition".
+lemma eq_to_eq':
+ ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r =_1 r' → r \sub\f ∘ ⊩ =_1 r'\sub\f ∘ ⊩.
+ intros 5 (o1 o2 r r' H);
+ apply (.= (commute ?? r)^-1);
+ change in H with (⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c);
+ apply rule (.= H);
+ apply (commute ?? r').
qed.
-
-definition id: ∀o:basic_pair. relation_pair o o.
+definition id_relation_pair: ∀o:basic_pair. relation_pair o o.
intro;
constructor 1;
- [1,2: constructor 1;
- intros;
- apply (s=s1)
- | simplify; intros;
- split;
- intro;
- cases H;
- cases H1; clear H H1;
- [ exists [ apply y ]
- split
- [ rewrite > H2; assumption
- | reflexivity ]
- | exists [ apply x ]
- split
- [2: rewrite < H3; assumption
- | reflexivity ]]]
+ [1,2: apply id1;
+ | lapply (id_neutral_right1 ? (concr o) ? (⊩)) as H;
+ lapply (id_neutral_left1 ?? (form o) (⊩)) as H1;
+ apply (.= H);
+ apply (H1^-1);]
qed.
-definition relation_pair_composition:
- ∀o1,o2,o3. binary_morphism (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
- intros;
- constructor 1;
- [ intros (r r1);
+lemma relation_pair_composition:
+ ∀o1,o2,o3: basic_pair.
+ relation_pair_setoid o1 o2 → relation_pair_setoid o2 o3 → relation_pair_setoid o1 o3.
+intros 3 (o1 o2 o3);
+ intros (r r1);
constructor 1;
- [ apply (r \sub\c ∘ r1 \sub\c)
- | apply (r \sub\f ∘ r1 \sub\f)
+ [ apply (r1 \sub\c ∘ r \sub\c)
+ | apply (r1 \sub\f ∘ r \sub\f)
| lapply (commute ?? r) as H;
lapply (commute ?? r1) as H1;
- apply (equal_morphism ???? (r\sub\c ∘ (r1\sub\c ∘ ⊩)) ? ((⊩ ∘ r\sub\f) ∘ r1\sub\f));
- [1,2: apply associative_composition]
- apply (equal_morphism ???? (r\sub\c ∘ (⊩ ∘ r1\sub\f)) ? ((r\sub\c ∘ ⊩) ∘ r1\sub\f));
- [1,2: apply composition_morphism; first [assumption | apply refl_equal_relations]
- | apply sym_equal_relations;
- apply associative_composition
- ]]
- | intros;
- alias symbol "eq" = "equal relation".
- change with (a\sub\c ∘ b\sub\c ∘ ⊩ = a'\sub\c ∘ b'\sub\c ∘ ⊩);
- apply (equal_morphism ???? (a\sub\c ∘ (b\sub\c ∘ ⊩)) ? (a'\sub\c ∘ (b'\sub\c ∘ ⊩)));
- [ apply associative_composition
- | apply sym_equal_relations; apply associative_composition]
- apply (equal_morphism ???? (a\sub\c ∘ (b'\sub\c ∘ ⊩)) ? (a' \sub \c∘(b' \sub \c∘⊩)));
- [2: apply refl_equal_relations;
- |1: apply composition_morphism;
- [ apply refl_equal_relations
- | assumption]]
- apply (equal_morphism ???? (a\sub\c ∘ (⊩ ∘ b'\sub\f)) ? (a'\sub\c ∘ (⊩ ∘ b'\sub\f)));
- [1,2: apply composition_morphism;
- [1,3: apply refl_equal_relations
- | apply (commute ?? b');
- | apply sym_equal_relations; apply (commute ?? b');]]
- apply (equal_morphism ???? ((a\sub\c ∘ ⊩) ∘ b'\sub\f) ? ((a'\sub\c ∘ ⊩) ∘ b'\sub\f));
- [2: apply associative_composition
- |1: apply sym_equal_relations; apply associative_composition]
- apply composition_morphism;
- [ assumption
- | apply refl_equal_relations]]
+ alias symbol "trans" = "trans1".
+ alias symbol "assoc" = "category1 assoc".
+ apply (.= ASSOC);
+ apply (.= #‡H1);
+ alias symbol "invert" = "setoid1 symmetry".
+ apply (.= ASSOC ^ -1);
+ apply (.= H‡#);
+ apply ASSOC]
+qed.
+
+lemma relation_pair_composition_is_morphism:
+ ∀o1,o2,o3: basic_pair.
+ ∀a,a':relation_pair_setoid o1 o2.
+ ∀b,b':relation_pair_setoid o2 o3.
+ a=a' → b=b' →
+ relation_pair_composition o1 o2 o3 a b
+ = relation_pair_composition o1 o2 o3 a' b'.
+intros 3 (o1 o2 o3);
+ intros;
+ change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c));
+ change in e with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c);
+ change in e1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c);
+ apply (.= ASSOC);
+ apply (.= #‡e1);
+ apply (.= #‡(commute ?? b'));
+ apply (.= ASSOC ^ -1);
+ apply (.= e‡#);
+ apply (.= ASSOC);
+ apply (.= #‡(commute ?? b')^-1);
+ apply (ASSOC ^ -1);
+qed.
+
+definition relation_pair_composition_morphism:
+ ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
+ intros;
+ constructor 1;
+ [ apply relation_pair_composition;
+ | apply relation_pair_composition_is_morphism;]
+qed.
+
+lemma relation_pair_composition_morphism_assoc:
+Πo1:basic_pair
+.Πo2:basic_pair
+ .Πo3:basic_pair
+ .Πo4:basic_pair
+ .Πa12:relation_pair_setoid o1 o2
+ .Πa23:relation_pair_setoid o2 o3
+ .Πa34:relation_pair_setoid o3 o4
+ .relation_pair_composition_morphism o1 o3 o4
+ (relation_pair_composition_morphism o1 o2 o3 a12 a23) a34
+ =relation_pair_composition_morphism o1 o2 o4 a12
+ (relation_pair_composition_morphism o2 o3 o4 a23 a34).
+ intros;
+ change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) =
+ ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c));
+ alias symbol "refl" = "refl1".
+ alias symbol "prop2" = "prop21".
+ apply (ASSOC‡#);
+qed.
+
+lemma relation_pair_composition_morphism_respects_id:
+ ∀o1,o2:basic_pair.∀a:relation_pair_setoid o1 o2.
+ relation_pair_composition_morphism o1 o1 o2 (id_relation_pair o1) a=a.
+ intros;
+ change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c);
+ apply ((id_neutral_right1 ????)‡#);
+qed.
+
+lemma relation_pair_composition_morphism_respects_id_r:
+ ∀o1,o2:basic_pair.∀a:relation_pair_setoid o1 o2.
+ relation_pair_composition_morphism o1 o2 o2 a (id_relation_pair o2)=a.
+ intros;
+ change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c);
+ apply ((id_neutral_left1 ????)‡#);
qed.
-definition BP: category.
+definition BP: category1.
constructor 1;
[ apply basic_pair
| apply relation_pair_setoid
- | apply id
- | apply relation_pair_composition
- | intros;
- change with (a12\sub\c ∘ a23\sub\c ∘ a34\sub\c ∘ ⊩ =
- (a12\sub\c ∘ (a23\sub\c ∘ a34\sub\c) ∘ ⊩));
- apply composition_morphism;
- [2: apply refl_equal_relations]
- apply associative_composition
- | intros;
- change with ((id o1)\sub\c ∘ a\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
- apply composition_morphism;
- [2: apply refl_equal_relations]
- intros 2; unfold id; simplify;
- split; intro;
- [ cases H; cases H1; rewrite > H2; assumption
- | exists; [assumption] split; [reflexivity| assumption]]
+ | apply id_relation_pair
+ | apply relation_pair_composition_morphism
+ | apply relation_pair_composition_morphism_assoc;
+ | apply relation_pair_composition_morphism_respects_id;
+ | apply relation_pair_composition_morphism_respects_id_r;]
+qed.
+
+definition basic_pair_of_BP : objs1 BP → basic_pair ≝ λx.x.
+coercion basic_pair_of_BP.
+
+definition relation_pair_setoid_of_arrows1_BP :
+ ∀P,Q. arrows1 BP P Q → relation_pair_setoid P Q ≝ λP,Q,x.x.
+coercion relation_pair_setoid_of_arrows1_BP.
+
+(*
+definition BPext: ∀o: BP. (form o) ⇒_1 Ω^(concr o).
+ intros; constructor 1;
+ [ apply (ext ? ? (rel o));
| intros;
- change with (a\sub\c ∘ (id o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
- apply composition_morphism;
- [2: apply refl_equal_relations]
- intros 2; unfold id; simplify;
- split; intro;
- [ cases H; cases H1; rewrite < H3; assumption
- | exists; [assumption] split; [assumption|reflexivity]]
- ]
+ apply (.= #‡e);
+ apply refl1]
+qed.
+
+definition BPextS: ∀o: BP. Ω^(form o) ⇒_1 Ω^(concr o).
+ intros; constructor 1;
+ [ apply (minus_image ?? (rel o));
+ | intros; apply (#‡e); ]
+qed.
+
+definition fintersects: ∀o: BP. (form o) × (form o) ⇒_1 Ω^(form o).
+ intros (o); constructor 1;
+ [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
+ intros; simplify; apply (.= (†e)‡#); apply refl1
+ | intros; split; simplify; intros;
+ [ apply (. #‡((†e^-1)‡(†e1^-1))); assumption
+ | apply (. #‡((†e)‡(†e1))); assumption]]
+qed.
+
+interpretation "fintersects" 'fintersects U V = (fun21 ??? (fintersects ?) U V).
+
+definition fintersectsS:
+ ∀o:BP. Ω^(form o) × Ω^(form o) ⇒_1 Ω^(form o).
+ intros (o); constructor 1;
+ [ apply (λo: basic_pair.λa,b: Ω^(form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
+ intros; simplify; apply (.= (†e)‡#); apply refl1
+ | intros; split; simplify; intros;
+ [ apply (. #‡((†e^-1)‡(†e1^-1))); assumption
+ | apply (. #‡((†e)‡(†e1))); assumption]]
qed.
+
+interpretation "fintersectsS" 'fintersects U V = (fun21 ??? (fintersectsS ?) U V).
+
+definition relS: ∀o: BP. (concr o) × Ω^(form o) ⇒_1 CPROP.
+ intros (o); constructor 1;
+ [ apply (λx:concr o.λS: Ω^(form o).∃y:form o.y ∈ S ∧ x ⊩⎽o y);
+ | intros; split; intros; cases e2; exists [1,3: apply w]
+ [ apply (. (#‡e1^-1)‡(e^-1‡#)); assumption
+ | apply (. (#‡e1)‡(e‡#)); assumption]]
+qed.
+
+interpretation "basic pair relation for subsets" 'Vdash2 x y c = (fun21 (concr ?) ?? (relS c) x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash c = (fun21 ??? (relS c)).
+*)
projects / helm.git / blobdiff