From 13114a0147a28f8c7359c9c19ee254716eb5f55a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 19 Jan 2009 18:02:22 +0000 Subject: [PATCH] - new notation.ma file with local and common notation - o-bp have now a O as prefix, the same for o-cs - BP_to_OBP proved to be a functor, not faitfull nor full (simply stated) --- .../formal_topology/overlap/basic_pairs.ma | 3 +- .../overlap/basic_pairs_to_o-basic_pairs.ma | 95 ++++++++++----- .../overlap/cprop_connectives.ma | 3 + .../contribs/formal_topology/overlap/depends | 9 +- .../formal_topology/overlap/notation.ma | 16 +++ .../formal_topology/overlap/o-basic_pairs.ma | 100 ++++++++-------- .../o-basic_pairs_to_o-basic_topologies.ma | 10 +- .../overlap/o-concrete_spaces.ma | 108 +++++++++--------- .../overlap/relations_to_o-algebra.ma | 4 +- 9 files changed, 203 insertions(+), 145 deletions(-) create mode 100644 helm/software/matita/contribs/formal_topology/overlap/notation.ma diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma index 6140e278e..84f48c894 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "relations.ma". +include "notation.ma". record basic_pair: Type1 ≝ { concr: REL; @@ -31,8 +32,6 @@ record relation_pair (BP1,BP2: basic_pair): Type1 ≝ commute: ⊩ ∘ concr_rel = 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). diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma index 2dd4147ae..7dbd3a80a 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma @@ -17,42 +17,85 @@ include "o-basic_pairs.ma". include "relations_to_o-algebra.ma". (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) -definition o_basic_pair_of_basic_pair: cic:/matita/formal_topology/basic_pairs/basic_pair.ind#xpointer(1/1) → basic_pair. - intro; +definition o_basic_pair_of_basic_pair: basic_pair → Obasic_pair. + intro b; constructor 1; - [ apply (SUBSETS (concr b)); - | apply (SUBSETS (form b)); - | apply (orelation_of_relation ?? (rel b)); ] + [ apply (map_objs2 ?? SUBSETS' (concr b)); + | apply (map_objs2 ?? SUBSETS' (form b)); + | apply (map_arrows2 ?? SUBSETS' (concr b) (form b) (rel b)); ] qed. definition o_relation_pair_of_relation_pair: - ∀BP1,BP2.cic:/matita/formal_topology/basic_pairs/relation_pair.ind#xpointer(1/1) BP1 BP2 → - relation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2). + ∀BP1,BP2. relation_pair BP1 BP2 → + Orelation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2). intros; constructor 1; - [ apply (orelation_of_relation ?? (r \sub \c)); - | apply (orelation_of_relation ?? (r \sub \f)); - | lapply (commute ?? r); - lapply (orelation_of_relation_preserves_equality ???? Hletin); - apply (.= (orelation_of_relation_preserves_composition (concr BP1) ??? (rel BP2)) ^ -1); - apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r))); - apply (orelation_of_relation_preserves_composition ?? (form BP2) (rel BP1) ?); ] + [ apply (map_arrows2 ?? SUBSETS' (concr BP1) (concr BP2) (r \sub \c)); + | apply (map_arrows2 ?? SUBSETS' (form BP1) (form BP2) (r \sub \f)); + | apply (.= (respects_comp2 ?? SUBSETS' (concr BP1) (concr BP2) (form BP2) r\sub\c (⊩\sub BP2) )^-1); + cut (⊩ \sub BP2∘r \sub \c = r\sub\f ∘ ⊩ \sub BP1) as H; + [ apply (.= †H); + apply (respects_comp2 ?? SUBSETS' (concr BP1) (form BP1) (form BP2) (⊩\sub BP1) r\sub\f); + | apply commute;]] qed. -(* -definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 cic:/matita/formal_topology/basic_pairs/BP.con) BP). +definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP). constructor 1; [ apply o_basic_pair_of_basic_pair; | intros; constructor 1; [ apply (o_relation_pair_of_relation_pair S T); - | intros; split; unfold o_relation_pair_of_relation_pair; simplify; - unfold o_basic_pair_of_basic_pair; simplify; ] - | simplify; intros; whd; split; unfold o_relation_pair_of_relation_pair; simplify; - unfold o_basic_pair_of_basic_pair; -simplify in ⊢ (? ? ? (? % ? ?) ?); -simplify in ⊢ (? ? ? (? ? % ?) ?); -simplify in ⊢ (? ? ? ? (? % ? ?)); -simplify in ⊢ (? ? ? ? (? ? % ?)); - | simplify; intros; whd; split;unfold o_relation_pair_of_relation_pair; simplify; - unfold o_basic_pair_of_basic_pair;simplify; + | intros (a b Eab); split; unfold o_relation_pair_of_relation_pair; simplify; + unfold o_basic_pair_of_basic_pair; simplify; + [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x); + | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x); + | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x); + | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);] + simplify; + apply (prop12); + apply (.= (respects_comp2 ?? SUBSETS' (concr S) (concr T) (form T) (a\sub\c) (⊩\sub T))^-1); + apply sym2; + apply (.= (respects_comp2 ?? SUBSETS' (concr S) (concr T) (form T) (b\sub\c) (⊩\sub T))^-1); + apply sym2; + apply prop12; + apply Eab; + ] + | simplify; intros; whd; split; + [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x); + | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x); + | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x); + | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);] + simplify; + apply prop12; + apply prop22;[2,4,6,8: apply rule #;] + apply (respects_id2 ?? SUBSETS' (concr o)); + | simplify; intros; whd; split; + [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x); + | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x); + | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x); + | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);] + simplify; + apply prop12; + apply prop22;[2,4,6,8: apply rule #;] + apply (respects_comp2 ?? SUBSETS' (concr o1) (concr o2) (concr o3) f1\sub\c f2\sub\c);] +qed. + + +(* +theorem BP_to_OBP_faithful: + ∀S,T.∀f,g:arrows2 (category2_of_category1 BP) S T. + map_arrows2 ?? BP_to_OBP ?? f = map_arrows2 ?? BP_to_OBP ?? g → f=g. + intros; unfold BP_to_OBP in e; simplify in e; cases e; + unfold orelation_of_relation in e3; simplify in e3; clear e e1 e2 e4; + intros 2; change in match or_f_ in e3 with (λq,w,x.fun12 ?? (or_f q w) x); + simplify in e3; STOP lapply (e3 (singleton ? x)); cases Hletin; + split; intro; [ lapply (s y); | lapply (s1 y); ] + [2,4: exists; [1,3:apply x] split; [1,3: assumption |*: change with (x=x); apply rule #] + |*: cases Hletin1; cases x1; change in f3 with (eq1 ? x w); apply (. f3‡#); assumption;] +qed. +*) + +(* +theorem SUBSETS_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BP_to_OBP S T g = f). + intros; exists; + *) \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma index 644acc218..59473882d 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma @@ -142,6 +142,9 @@ interpretation "exT2 \snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y). inductive exT2 (A:Type0) (P,Q:A→CProp0) : CProp0 ≝ ex_introT2: ∀w:A. P w → Q w → exT2 A P Q. +inductive exT22 (A:Type2) (P:A→CProp2) : CProp2 ≝ + ex_introT22: ∀w:A. P w → exT22 A P. + definition Not : CProp0 → Prop ≝ λx:CProp.x → False. interpretation "constructive not" 'not x = (Not x). diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends index 58e985939..f80fe592c 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/depends +++ b/helm/software/matita/contribs/formal_topology/overlap/depends @@ -2,21 +2,22 @@ o-basic_pairs.ma o-algebra.ma basic_pairs_to_basic_topologies.ma basic_pairs.ma basic_pairs_to_o-basic_pairs.ma basic_topologies.ma o-basic_pairs_to_o-basic_topologies.ma o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma o-saturations.ma o-algebra.ma -basic_pairs.ma relations.ma saturations.ma relations.ma +basic_pairs.ma notation.ma relations.ma o-algebra.ma categories.ma o-formal_topologies.ma o-basic_topologies.ma -categories.ma cprop_connectives.ma formal_topologies.ma basic_topologies.ma +categories.ma cprop_connectives.ma saturations_to_o-saturations.ma o-saturations.ma relations_to_o-algebra.ma saturations.ma -subsets.ma categories.ma basic_topologies.ma relations.ma saturations.ma +subsets.ma categories.ma concrete_spaces.ma basic_pairs.ma relations.ma subsets.ma concrete_spaces_to_o-concrete_spaces.ma basic_pairs_to_o-basic_pairs.ma concrete_spaces.ma o-concrete_spaces.ma o-basic_topologies.ma o-algebra.ma o-saturations.ma -basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma basic_topologies_to_o-basic_topologies.ma basic_topologies.ma o-basic_topologies.ma relations_to_o-algebra.ma +basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma +notation.ma cprop_connectives.ma logic/connectives.ma relations_to_o-algebra.ma o-algebra.ma relations.ma o-basic_pairs_to_o-basic_topologies.ma o-basic_pairs.ma o-basic_topologies.ma diff --git a/helm/software/matita/contribs/formal_topology/overlap/notation.ma b/helm/software/matita/contribs/formal_topology/overlap/notation.ma new file mode 100644 index 000000000..97c1a9b6d --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/notation.ma @@ -0,0 +1,16 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}. +notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma index 3ac2f62ee..6476c4aeb 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma @@ -13,15 +13,16 @@ (**************************************************************************) include "o-algebra.ma". +include "notation.ma". -record basic_pair: Type2 ≝ - { concr: OA; - form: OA; - rel: arrows2 ? concr form +record Obasic_pair: Type2 ≝ + { Oconcr: OA; + Oform: OA; + Orel: arrows2 ? Oconcr Oform }. -interpretation "basic pair relation indexed" 'Vdash2 x y c = (rel c x y). -interpretation "basic pair relation (non applied)" 'Vdash c = (rel c). +interpretation "basic pair relation indexed" 'Vdash2 x y c = (Orel c x y). +interpretation "basic pair relation (non applied)" 'Vdash c = (Orel c). alias symbol "eq" = "setoid1 eq". alias symbol "compose" = "category1 composition". @@ -29,20 +30,17 @@ alias symbol "compose" = "category1 composition". alias symbol "eq" = "setoid2 eq". alias symbol "compose" = "category2 composition". -record relation_pair (BP1,BP2: basic_pair): Type2 ≝ - { concr_rel: arrows2 ? (concr BP1) (concr BP2); - form_rel: arrows2 ? (form BP1) (form BP2); - commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩ +record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝ + { Oconcr_rel: arrows2 ? (Oconcr BP1) (Oconcr BP2); + Oform_rel: arrows2 ? (Oform BP1) (Oform BP2); + Ocommute: ⊩ ∘ Oconcr_rel = Oform_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 = (Oconcr_rel __ r). +interpretation "formal relation" 'form_rel r = (Oform_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_relation2 (relation_pair o1 o2). +definition Orelation_pair_equality: + ∀o1,o2. equivalence_relation2 (Orelation_pair o1 o2). intros; constructor 1; [ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c); @@ -59,47 +57,47 @@ definition relation_pair_equality: qed. (* qui setoid1 e' giusto: ma non lo e'!!! *) -definition relation_pair_setoid: basic_pair → basic_pair → setoid2. +definition Orelation_pair_setoid: Obasic_pair → Obasic_pair → setoid2. intros; constructor 1; - [ apply (relation_pair b b1) - | apply relation_pair_equality + [ apply (Orelation_pair o o1) + | apply Orelation_pair_equality ] qed. -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. +definition Orelation_pair_of_Orelation_pair_setoid: + ∀P,Q. Orelation_pair_setoid P Q → Orelation_pair P Q ≝ λP,Q,x.x. +coercion Orelation_pair_of_Orelation_pair_setoid. -lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩. +lemma eq_to_eq': ∀o1,o2.∀r,r': Orelation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩. intros 5 (o1 o2 r r' H); change in H with (⊩ ∘ r\sub\c = ⊩ ∘ r'\sub\c); - apply (.= ((commute ?? r) \sup -1)); + apply (.= ((Ocommute ?? r) ^ -1)); apply (.= H); - apply (.= (commute ?? r')); + apply (.= (Ocommute ?? r')); apply refl2; qed. -definition id_relation_pair: ∀o:basic_pair. relation_pair o o. +definition Oid_relation_pair: ∀o:Obasic_pair. Orelation_pair o o. intro; constructor 1; [1,2: apply id2; - | lapply (id_neutral_right2 ? (concr o) ? (⊩)) as H; - lapply (id_neutral_left2 ?? (form o) (⊩)) as H1; + | lapply (id_neutral_right2 ? (Oconcr o) ? (⊩)) as H; + lapply (id_neutral_left2 ?? (Oform o) (⊩)) as H1; apply (.= H); apply (H1 \sup -1);] qed. -definition relation_pair_composition: - ∀o1,o2,o3. binary_morphism2 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3). +definition Orelation_pair_composition: + ∀o1,o2,o3. binary_morphism2 (Orelation_pair_setoid o1 o2) (Orelation_pair_setoid o2 o3) (Orelation_pair_setoid o1 o3). intros; constructor 1; [ intros (r r1); constructor 1; [ apply (r1 \sub\c ∘ r \sub\c) | apply (r1 \sub\f ∘ r \sub\f) - | lapply (commute ?? r) as H; - lapply (commute ?? r1) as H1; + | lapply (Ocommute ?? r) as H; + lapply (Ocommute ?? r1) as H1; apply rule (.= ASSOC); apply (.= #‡H1); apply rule (.= ASSOC ^ -1); @@ -111,38 +109,38 @@ definition relation_pair_composition: change in e1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c); apply rule (.= ASSOC); apply (.= #‡e1); - apply (.= #‡(commute ?? b')); + apply (.= #‡(Ocommute ?? b')); apply rule (.= ASSOC \sup -1); apply (.= e‡#); apply rule (.= ASSOC); - apply (.= #‡(commute ?? b')\sup -1); + apply (.= #‡(Ocommute ?? b')\sup -1); apply rule (ASSOC \sup -1)] qed. -definition BP: category2. +definition OBP: category2. constructor 1; - [ apply basic_pair - | apply relation_pair_setoid - | apply id_relation_pair - | apply relation_pair_composition + [ apply Obasic_pair + | apply Orelation_pair_setoid + | apply Oid_relation_pair + | apply Orelation_pair_composition | intros; change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) = ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c)); apply rule (ASSOC‡#); | intros; - change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c); + change with (⊩ ∘ (a\sub\c ∘ (Oid_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c); apply ((id_neutral_right2 ????)‡#); | intros; - change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c); + change with (⊩ ∘ ((Oid_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c); apply ((id_neutral_left2 ????)‡#);] qed. -definition basic_pair_of_objs2_BP: objs2 BP → basic_pair ≝ λx.x. -coercion basic_pair_of_objs2_BP. +definition Obasic_pair_of_objs2_OBP: objs2 OBP → Obasic_pair ≝ λx.x. +coercion Obasic_pair_of_objs2_OBP. -definition relation_pair_setoid_of_arrows2_BP: - ∀P,Q.arrows2 BP P Q → relation_pair_setoid P Q ≝ λP,Q,c.c. -coercion relation_pair_setoid_of_arrows2_BP. +definition Orelation_pair_setoid_of_arrows2_OBP: + ∀P,Q.arrows2 OBP P Q → Orelation_pair_setoid P Q ≝ λP,Q,c.c. +coercion Orelation_pair_setoid_of_arrows2_OBP. (* definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o). @@ -197,16 +195,16 @@ interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 __ notation "□ \sub b" non associative with precedence 90 for @{'box $b}. notation > "□_term 90 b" non associative with precedence 90 for @{'box $b}. -interpretation "Universal image ⊩⎻*" 'box x = (fun12 _ _ (or_f_minus_star _ _) (rel x)). +interpretation "Universal image ⊩⎻*" 'box x = (fun12 _ _ (or_f_minus_star _ _) (Orel x)). notation "◊ \sub b" non associative with precedence 90 for @{'diamond $b}. notation > "◊_term 90 b" non associative with precedence 90 for @{'diamond $b}. -interpretation "Existential image ⊩" 'diamond x = (fun12 _ _ (or_f _ _) (rel x)). +interpretation "Existential image ⊩" 'diamond x = (fun12 _ _ (or_f _ _) (Orel x)). notation "'Rest' \sub b" non associative with precedence 90 for @{'rest $b}. notation > "'Rest'⎽term 90 b" non associative with precedence 90 for @{'rest $b}. -interpretation "Universal pre-image ⊩*" 'rest x = (fun12 _ _ (or_f_star _ _) (rel x)). +interpretation "Universal pre-image ⊩*" 'rest x = (fun12 _ _ (or_f_star _ _) (Orel x)). notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}. notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}. -interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 _ _ (or_f_minus _ _) (rel x)). \ No newline at end of file +interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 _ _ (or_f_minus _ _) (Orel x)). \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma index 8555cf00a..b78e7b037 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma @@ -18,10 +18,10 @@ include "o-basic_topologies.ma". alias symbol "eq" = "setoid1 eq". (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) -definition o_basic_topology_of_o_basic_pair: BP → BTop. +definition o_basic_topology_of_o_basic_pair: OBP → BTop. intro t; constructor 1; - [ apply (form t); + [ apply (Oform t); | apply (□_t ∘ Ext⎽t); | apply (◊_t ∘ Rest⎽t); | intros 2; split; intro; @@ -58,7 +58,7 @@ definition o_basic_topology_of_o_basic_pair: BP → BTop. qed. definition o_continuous_relation_of_o_relation_pair: - ∀BP1,BP2.arrows2 BP BP1 BP2 → + ∀BP1,BP2.arrows2 OBP BP1 BP2 → arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2). intros (BP1 BP2 t); constructor 1; @@ -68,7 +68,7 @@ definition o_continuous_relation_of_o_relation_pair: apply (.= †(†e)); change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U)); cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2: - cases (commute ?? t); apply (e3 ^ -1 ((⊩)* U));] + cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩)* U));] apply (.= †COM); change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U)); apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U)))); @@ -81,7 +81,7 @@ definition o_continuous_relation_of_o_relation_pair: apply (.= †(†e)); change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U)); cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2: - cases (commute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));] + cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));] apply (.= †COM); change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U)); apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U)))); diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma index d7e0bf649..90086b4d2 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma @@ -15,7 +15,7 @@ include "o-basic_pairs.ma". include "o-saturations.ma". -definition A : ∀b:BP. unary_morphism1 (form b) (form b). +definition A : ∀b:OBP. unary_morphism1 (Oform b) (Oform b). intros; constructor 1; [ apply (λx.□_b (Ext⎽b x)); | intros; apply (†(†e));] @@ -25,25 +25,25 @@ lemma down_p : ∀S:SET1.∀I:SET.∀u:S⇒S.∀c:arrows2 SET1 I S.∀a:I.∀a': intros; apply (†(†e)); qed. -record concrete_space : Type2 ≝ - { bp:> BP; +record Oconcrete_space : Type2 ≝ + { Obp:> OBP; (*distr : is_distributive (form bp);*) - downarrow: unary_morphism1 (form bp) (form bp); - downarrow_is_sat: is_o_saturation ? downarrow; - converges: ∀q1,q2. - (Ext⎽bp q1 ∧ (Ext⎽bp q2)) = (Ext⎽bp ((downarrow q1) ∧ (downarrow q2))); - all_covered: Ext⎽bp (oa_one (form bp)) = oa_one (concr bp); - il2: ∀I:SET.∀p:arrows2 SET1 I (form bp). - downarrow (∨ { x ∈ I | downarrow (p x) | down_p ???? }) = - ∨ { x ∈ I | downarrow (p x) | down_p ???? }; - il1: ∀q.downarrow (A ? q) = A ? q + Odownarrow: unary_morphism1 (Oform Obp) (Oform Obp); + Odownarrow_is_sat: is_o_saturation ? Odownarrow; + Oconverges: ∀q1,q2. + (Ext⎽Obp q1 ∧ (Ext⎽Obp q2)) = (Ext⎽Obp ((Odownarrow q1) ∧ (Odownarrow q2))); + Oall_covered: Ext⎽Obp (oa_one (Oform Obp)) = oa_one (Oconcr Obp); + Oil2: ∀I:SET.∀p:arrows2 SET1 I (Oform Obp). + Odownarrow (∨ { x ∈ I | Odownarrow (p x) | down_p ???? }) = + ∨ { x ∈ I | Odownarrow (p x) | down_p ???? }; + Oil1: ∀q.Odownarrow (A ? q) = A ? q }. interpretation "o-concrete space downarrow" 'downarrow x = - (fun11 __ (downarrow _) x). + (fun11 __ (Odownarrow _) x). -definition binary_downarrow : - ∀C:concrete_space.binary_morphism1 (form C) (form C) (form C). +definition Obinary_downarrow : + ∀C:Oconcrete_space.binary_morphism1 (Oform C) (Oform C) (Oform C). intros; constructor 1; [ intros; apply (↓ c ∧ ↓ c1); | intros; @@ -52,40 +52,40 @@ intros; constructor 1; apply ((†e)‡(†e1));] qed. -interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 _ _ _ (binary_downarrow _) a b). +interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 _ _ _ (Obinary_downarrow _) a b). -record convergent_relation_pair (CS1,CS2: concrete_space) : Type2 ≝ - { rp:> arrows2 ? CS1 CS2; - respects_converges: - ∀b,c. eq1 ? (rp\sub\c⎻ (Ext⎽CS2 (b ↓ c))) (Ext⎽CS1 (rp\sub\f⎻ b ↓ rp\sub\f⎻ c)); - respects_all_covered: - eq1 ? (rp\sub\c⎻ (Ext⎽CS2 (oa_one (form CS2)))) - (Ext⎽CS1 (oa_one (form CS1))) +record Oconvergent_relation_pair (CS1,CS2: Oconcrete_space) : Type2 ≝ + { Orp:> arrows2 ? CS1 CS2; + Orespects_converges: + ∀b,c. eq1 ? (Orp\sub\c⎻ (Ext⎽CS2 (b ↓ c))) (Ext⎽CS1 (Orp\sub\f⎻ b ↓ Orp\sub\f⎻ c)); + Orespects_all_covered: + eq1 ? (Orp\sub\c⎻ (Ext⎽CS2 (oa_one (Oform CS2)))) + (Ext⎽CS1 (oa_one (Oform CS1))) }. -definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid2. - intros; +definition Oconvergent_relation_space_setoid: Oconcrete_space → Oconcrete_space → setoid2. + intros (c c1); constructor 1; - [ apply (convergent_relation_pair c c1) + [ apply (Oconvergent_relation_pair c c1) | constructor 1; - [ intros; - apply (relation_pair_equality c c1 c2 c3); + [ intros (c2 c3); + apply (Orelation_pair_equality c c1 c2 c3); | intros 1; apply refl2; | intros 2; apply sym2; | intros 3; apply trans2]] qed. -definition convergent_relation_space_of_convergent_relation_space_setoid: - ∀CS1,CS2.carr2 (convergent_relation_space_setoid CS1 CS2) → - convergent_relation_pair CS1 CS2 ≝ λP,Q,c.c. -coercion convergent_relation_space_of_convergent_relation_space_setoid. +definition Oconvergent_relation_space_of_Oconvergent_relation_space_setoid: + ∀CS1,CS2.carr2 (Oconvergent_relation_space_setoid CS1 CS2) → + Oconvergent_relation_pair CS1 CS2 ≝ λP,Q,c.c. +coercion Oconvergent_relation_space_of_Oconvergent_relation_space_setoid. -definition convergent_relation_space_composition: - ∀o1,o2,o3: concrete_space. +definition Oconvergent_relation_space_composition: + ∀o1,o2,o3: Oconcrete_space. binary_morphism2 - (convergent_relation_space_setoid o1 o2) - (convergent_relation_space_setoid o2 o3) - (convergent_relation_space_setoid o1 o3). + (Oconvergent_relation_space_setoid o1 o2) + (Oconvergent_relation_space_setoid o2 o3) + (Oconvergent_relation_space_setoid o1 o3). intros; constructor 1; [ intros; whd in t t1 ⊢ %; constructor 1; @@ -93,42 +93,42 @@ definition convergent_relation_space_composition: | intros; change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (b↓c2)))); alias symbol "trans" = "trans1". - apply (.= († (respects_converges : ?))); - apply (respects_converges ?? c (c1\sub\f⎻ b) (c1\sub\f⎻ c2)); - | change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (oa_one (form o3))))); - apply (.= (†(respects_all_covered :?))); - apply rule (respects_all_covered ?? c);] + apply (.= († (Orespects_converges : ?))); + apply (Orespects_converges ?? c (c1\sub\f⎻ b) (c1\sub\f⎻ c2)); + | change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (oa_one (Oform o3))))); + apply (.= (†(Orespects_all_covered :?))); + apply rule (Orespects_all_covered ?? c);] | intros; change with (b ∘ a = b' ∘ a'); - change in e with (rp ?? a = rp ?? a'); - change in e1 with (rp ?? b = rp ?? b'); + change in e with (Orp ?? a = Orp ?? a'); + change in e1 with (Orp ?? b = Orp ?? b'); apply (e‡e1);] qed. -definition CSPA: category2. +definition OCSPA: category2. constructor 1; - [ apply concrete_space - | apply convergent_relation_space_setoid + [ apply Oconcrete_space + | apply Oconvergent_relation_space_setoid | intro; constructor 1; [ apply id2 | intros; apply refl1; | apply refl1] - | apply convergent_relation_space_composition + | apply Oconvergent_relation_space_composition | intros; simplify; whd in a12 a23 a34; change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12); apply rule ASSOC; | intros; simplify; - change with (a ∘ id2 BP o1 = a); + change with (a ∘ id2 OBP o1 = a); apply (id_neutral_right2 : ?); | intros; simplify; change with (id2 ? o2 ∘ a = a); apply (id_neutral_left2 : ?);] qed. -definition concrete_space_of_CSPA : objs2 CSPA → concrete_space ≝ λx.x. -coercion concrete_space_of_CSPA. +definition Oconcrete_space_of_OCSPA : objs2 OCSPA → Oconcrete_space ≝ λx.x. +coercion Oconcrete_space_of_OCSPA. -definition convergent_relation_space_setoid_of_arrows2_CSPA : - ∀P,Q. arrows2 CSPA P Q → convergent_relation_space_setoid P Q ≝ λP,Q,x.x. -coercion convergent_relation_space_setoid_of_arrows2_CSPA. +definition Oconvergent_relation_space_setoid_of_arrows2_OCSPA : + ∀P,Q. arrows2 OCSPA P Q → Oconvergent_relation_space_setoid P Q ≝ λP,Q,x.x. +coercion Oconvergent_relation_space_setoid_of_arrows2_OCSPA. diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma index 2368affe0..b3939f90b 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma @@ -182,10 +182,8 @@ theorem SUBSETS_faithful: |*: cases Hletin1; cases x1; change in f3 with (eq1 ? x w); apply (. f3‡#); assumption;] qed. -inductive exT2 (A:Type2) (P:A→CProp2) : CProp2 ≝ - ex_introT2: ∀w:A. P w → exT2 A P. -theorem SUBSETS_full: ∀S,T.∀f. exT2 ? (λg. map_arrows2 ?? SUBSETS' S T g = f). +theorem SUBSETS_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? SUBSETS' S T g = f). intros; exists; [ constructor 1; constructor 1; [ apply (λx:carr S.λy:carr T. y ∈ f (singleton S x)); -- 2.39.2