From 49045bfd9b3038ce30a1911e2345f949ed38ec8a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Jan 2009 17:28:59 +0000 Subject: [PATCH] Some work on concrete spaces. --- .../formal_topology/overlap/basic_pairs.ma | 39 +++--- .../overlap/concrete_spaces.ma | 124 ++++++++++++++++++ .../contribs/formal_topology/overlap/depends | 2 + .../overlap/formal_topologies.ma | 121 +++++++++++++++++ .../formal_topology/overlap/relations.ma | 28 ++-- 5 files changed, 282 insertions(+), 32 deletions(-) create mode 100644 helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma create mode 100644 helm/software/matita/contribs/formal_topology/overlap/formal_topologies.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 97e386c15..d0e4ffd4a 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma @@ -139,49 +139,50 @@ definition BP: category1. apply ((id_neutral_left1 ????)‡#);] qed. -(* definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o). intros; constructor 1; [ apply (ext ? ? (rel o)); | intros; - apply (.= #‡H); + apply (.= #‡e); apply refl1] qed. -definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝ - λo.extS ?? (rel o). +definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o). + intros; constructor 1; + [ apply (minus_image ?? (rel o)); + | intros; apply (#‡e); ] +qed. definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)). intros (o); constructor 1; [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b }); - intros; simplify; apply (.= (†H)‡#); apply refl1 + intros; simplify; apply (.= (†e)‡#); apply refl1 | intros; split; simplify; intros; - [ apply (. #‡((†H)‡(†H1))); assumption - | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]] + [ apply (. #‡((†e)‡(†e1))); assumption + | apply (. #‡((†e\sup -1)‡(†e1\sup -1))); assumption]] qed. -interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V). +interpretation "fintersects" 'fintersects U V = (fun21 ___ (fintersects _) U V). definition fintersectsS: ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)). intros (o); constructor 1; [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b }); - intros; simplify; apply (.= (†H)‡#); apply refl1 + intros; simplify; apply (.= (†e)‡#); apply refl1 | intros; split; simplify; intros; - [ apply (. #‡((†H)‡(†H1))); assumption - | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]] + [ apply (. #‡((†e)‡(†e1))); assumption + | apply (. #‡((†e\sup -1)‡(†e1\sup -1))); assumption]] qed. -interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V). +interpretation "fintersectsS" 'fintersects U V = (fun21 ___ (fintersectsS _) U V). definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP. intros (o); constructor 1; - [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y); - | intros; split; intros; cases H2; exists [1,3: apply w] - [ apply (. (#‡H1)‡(H‡#)); assumption - | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]] + [ apply (λx:concr o.λS: Ω \sup (form o).∃y:carr (form o).y ∈ S ∧ x ⊩ y); + | intros; split; intros; cases e2; exists [1,3: apply w] + [ apply (. (#‡e1)‡(e‡#)); assumption + | apply (. (#‡e1 \sup -1)‡(e \sup -1‡#)); assumption]] qed. -interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y). -interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)). -*) +interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun21 (concr _) __ (relS _) x y). +interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun21 ___ (relS _)). diff --git a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma new file mode 100644 index 000000000..ff6774be3 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma @@ -0,0 +1,124 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "basic_pairs.ma". + +(* full_subset e' una coercion che non mette piu' *) +record concrete_space : Type1 ≝ + { bp:> BP; + converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V); + all_covered: ∀x: concr bp. x ⊩ full_subset (form bp) + }. + +definition bp': concrete_space → basic_pair ≝ λc.bp c. +coercion bp'. + +definition bp'': concrete_space → objs1 BP ≝ λc.bp c. +coercion bp''. + +record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝ + { rp:> arrows1 ? CS1 CS2; + respects_converges: + ∀b,c. + minus_image ?? rp \sub\c (BPextS CS2 (b ↓ c)) = + BPextS CS1 ((minus_image ?? rp \sub\f b) ↓ (minus_image ?? rp \sub\f c)); + respects_all_covered: + minus_image ?? rp\sub\c (BPextS CS2 (full_subset (form CS2))) = BPextS CS1 (full_subset (form CS1)) + }. +(* +definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝ + λCS1,CS2,c. rp CS1 CS2 c. + +coercion rp'. + +definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1. + intros; + constructor 1; + [ apply (convergent_relation_pair c c1) + | constructor 1; + [ intros; + apply (relation_pair_equality c c1 c2 c3); + | intros 1; apply refl1; + | intros 2; apply sym1; + | intros 3; apply trans1]] +qed. + +definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝ + λCS1,CS2,c.rp ?? c. + +coercion rp''. + +definition convergent_relation_space_composition: + ∀o1,o2,o3: concrete_space. + binary_morphism1 + (convergent_relation_space_setoid o1 o2) + (convergent_relation_space_setoid o2 o3) + (convergent_relation_space_setoid o1 o3). + intros; constructor 1; + [ intros; whd in c c1 ⊢ %; + constructor 1; + [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption] + | intros; + change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c); + change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?))) + with (c1 \sub \f ∘ c \sub \f); + change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?)))) + with (c1 \sub \f ∘ c \sub \f); + apply (.= (extS_com ??????)); + apply (.= (†(respects_converges ?????))); + apply (.= (respects_converges ?????)); + apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1))); + apply refl1; + | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c); + apply (.= (extS_com ??????)); + apply (.= (†(respects_all_covered ???))); + apply (.= respects_all_covered ???); + apply refl1] + | intros; + change with (b ∘ a = b' ∘ a'); + change in H with (rp'' ?? a = rp'' ?? a'); + change in H1 with (rp'' ?? b = rp ?? b'); + apply (.= (H‡H1)); + apply refl1] +qed. + +definition CSPA: category1. + constructor 1; + [ apply concrete_space + | apply convergent_relation_space_setoid + | intro; constructor 1; + [ apply id1 + | intros; + unfold id; simplify; + apply (.= (equalset_extS_id_X_X ??)); + apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡ + (equalset_extS_id_X_X ??)\sup -1))); + apply refl1; + | apply (.= (equalset_extS_id_X_X ??)); + apply refl1] + | apply convergent_relation_space_composition + | intros; simplify; + change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12); + apply (.= ASSOC1); + apply refl1 + | intros; simplify; + change with (a ∘ id1 ? o1 = a); + apply (.= id_neutral_right1 ????); + apply refl1 + | intros; simplify; + change with (id1 ? o2 ∘ a = a); + apply (.= id_neutral_left1 ????); + apply refl1] +qed. +*) \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends index 1295f994d..50152aeab 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/depends +++ b/helm/software/matita/contribs/formal_topology/overlap/depends @@ -6,9 +6,11 @@ saturations.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 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 +concrete_spaces.ma basic_pairs.ma relations.ma subsets.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 diff --git a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma new file mode 100644 index 000000000..eb2b0b1f7 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma @@ -0,0 +1,121 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "basic_topologies.ma". + +definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o). + +coercion btop_carr. + +definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o. + +coercion btop_carr'. + +definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S). + intros; constructor 1; + [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)}); + intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w] + split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption + | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split; + try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption] +qed. + +interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a). + +definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S). + intros; constructor 1; + [ apply (λU,V. ↓U ∩ ↓V); + | intros; apply (.= (†H)‡(†H1)); apply refl1] +qed. + +interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V). + +record formal_topology: Type ≝ + { bt:> BTop; + converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V + }. + +definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o. + +coercion bt'. + +definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S). + intros; constructor 1; + [ apply (λb,c:S. (singleton S b) ↓ (singleton S c)); + | intros; apply (.= (†H)‡(†H1)); apply refl1] +qed. + +interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V). + +record formal_map (S,T: formal_topology) : Type ≝ + { cr:> continuous_relation_setoid S T; + C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c; + C2: extS ?? cr T = S + }. + +definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝ + λFT1,FT2,c. cr FT1 FT2 c. + +coercion cr'. + +definition formal_map_setoid: formal_topology → formal_topology → setoid1. + intros (S T); constructor 1; + [ apply (formal_map S T); + | constructor 1; + [ apply (λf,f1: formal_map S T.f=f1); + | simplify; intros 1; apply refl1 + | simplify; intros 2; apply sym1 + | simplify; intros 3; apply trans1]] +qed. + +definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝ + λFT1,FT2,c.cr ?? c. + +coercion cr''. + +definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝ + λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c). + +coercion cr'''. + +axiom C1': + ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T. + extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V. + +definition formal_map_composition: + ∀o1,o2,o3: formal_topology. + binary_morphism1 + (formal_map_setoid o1 o2) + (formal_map_setoid o2 o3) + (formal_map_setoid o1 o3). + intros; constructor 1; + [ intros; whd in c c1; constructor 1; + [ apply (comp1 BTop ??? c c1); + | intros; + apply (.= (extS_com ??? c c1 ?)); + apply (.= †(C1 ?????)); + apply (.= (C1' ?????)); + apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1)))); + apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1); + apply (.= (extS_singleton ????)‡(extS_singleton ????)); + apply refl1; + | apply (.= (extS_com ??? c c1 ?)); + apply (.= (†(C2 ???))); + apply (.= (C2 ???)); + apply refl1;] + | intros; simplify; + change with (comp1 BTop ??? a b = comp1 BTop ??? a' b'); + apply prop1; assumption] +qed. + diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma index dc3c091bb..c4502f3d0 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma @@ -96,14 +96,12 @@ definition REL: category1. first [apply refl | assumption]]] qed. -(* 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 setoid1_of_REL. @@ -114,23 +112,27 @@ lemma Type_OF_setoid1_of_REL: ∀o1:Type_OF_category1 REL. Type_OF_objs1 o1 → qed. coercion Type_OF_setoid1_of_REL. -(* -definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b. - apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x}); - intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1. +definition comprehension: ∀b:REL. (unary_morphism1 b CPROP) → Ω \sup b. + apply (λb:REL. λP: b ⇒ CPROP. {x | P x}); + intros; simplify; + alias symbol "trans" = "trans1". + alias symbol "prop1" = "prop11". + apply (.= †e); apply refl1. qed. interpretation "subset comprehension" 'comprehension s p = - (comprehension s (mk_unary_morphism __ p _)). + (comprehension s (mk_unary_morphism1 __ p _)). definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X). - apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?); - [ intros; simplify; apply (.= (H‡#)); apply refl1 - | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption; - [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption - | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]] + apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 REL X S.λf:S.{x ∈ X | x ♮r f}) ?); + [ intros; simplify; apply (.= (e‡#)); apply refl1 + | intros; simplify; split; intros; simplify; + [ change with (∀x. x ♮a b → x ♮a' b'); intros; + apply (. (#‡e1)); whd in e; apply (if ?? (e ??)); assumption + | change with (∀x. x ♮a' b' → x ♮a b); intros; + apply (. (#‡e1\sup -1)); whd in e; apply (fi ?? (e ??));assumption]] qed. - +(* definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X. (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*) intros (X S r); constructor 1; -- 2.39.2