X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fo-concrete_spaces.ma;h=d7e0bf649754b0e995b3e791585e729de854a1a4;hb=fc577dad1529b2d90c40dad8e6e3429281107c99;hp=6a9d7794db701429f657746dc1b41dc4922aad58;hpb=02ce2fd650a68d04fff678441cca9086c8310005;p=helm.git 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 6a9d7794d..d7e0bf649 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,26 +15,10 @@ include "o-basic_pairs.ma". include "o-saturations.ma". -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)). - -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)). - -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)). - -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)). - definition A : ∀b:BP. unary_morphism1 (form b) (form b). intros; constructor 1; [ apply (λx.□_b (Ext⎽b x)); - | do 2 unfold FunClass_1_OF_Type_OF_setoid21; intros; apply (†(†e));] + | intros; apply (†(†e));] qed. lemma down_p : ∀S:SET1.∀I:SET.∀u:S⇒S.∀c:arrows2 SET1 I S.∀a:I.∀a':I.a=a'→u (c a)=u (c a'). @@ -45,7 +29,7 @@ record concrete_space : Type2 ≝ { bp:> BP; (*distr : is_distributive (form bp);*) downarrow: unary_morphism1 (form bp) (form bp); - downarrow_is_sat: is_saturation ? downarrow; + 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); @@ -58,18 +42,10 @@ record concrete_space : Type2 ≝ interpretation "o-concrete space downarrow" 'downarrow x = (fun11 __ (downarrow _) x). -definition bp': concrete_space → basic_pair ≝ λc.bp c. -coercion bp'. - -definition bp'': concrete_space → objs2 BP. - intro; apply (bp' c); -qed. -coercion bp''. - definition binary_downarrow : ∀C:concrete_space.binary_morphism1 (form C) (form C) (form C). intros; constructor 1; -[ intros; apply (↓ t ∧ ↓ t1); +[ intros; apply (↓ c ∧ ↓ c1); | intros; alias symbol "prop2" = "prop21". alias symbol "prop1" = "prop11". @@ -87,10 +63,6 @@ record convergent_relation_pair (CS1,CS2: concrete_space) : Type2 ≝ (Ext⎽CS1 (oa_one (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 → setoid2. intros; constructor 1; @@ -103,18 +75,10 @@ definition convergent_relation_space_setoid: concrete_space → concrete_space | intros 3; apply trans2]] qed. - -definition rp'': ∀CS1,CS2.carr2 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝ - λCS1,CS2,c.rp ?? c. -coercion rp''. - -definition rp''': ∀CS1,CS2.Type_OF_setoid2 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝ - λCS1,CS2,c.rp ?? c. -coercion rp'''. - -definition rp'''': ∀CS1,CS2.Type_OF_setoid2 (convergent_relation_space_setoid CS1 CS2) → carr2 (arrows2 BP CS1 CS2) ≝ - λCS1,CS2,c.rp ?? c. -coercion rp''''. +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 convergent_relation_space_composition: ∀o1,o2,o3: concrete_space. @@ -125,21 +89,19 @@ definition convergent_relation_space_composition: intros; constructor 1; [ intros; whd in t t1 ⊢ %; constructor 1; - [ apply (t1 ∘ t); + [ apply (c1 ∘ c); | intros; - change in ⊢ (? ? ? % ?) with (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (b↓c)))); - unfold FunClass_1_OF_Type_OF_setoid21; + change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (b↓c2)))); alias symbol "trans" = "trans1". apply (.= († (respects_converges : ?))); - apply (respects_converges ?? t (t1\sub\f⎻ b) (t1\sub\f⎻ c)); - | change in ⊢ (? ? ? % ?) with (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (oa_one (form o3))))); - unfold FunClass_1_OF_Type_OF_setoid21; + 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 ?? t);] + apply rule (respects_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 (rp ?? a = rp ?? a'); + change in e1 with (rp ?? b = rp ?? b'); apply (e‡e1);] qed. @@ -156,9 +118,17 @@ definition CSPA: category2. change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12); apply rule ASSOC; | intros; simplify; - change with (a ∘ id2 ? o1 = a); + change with (a ∘ id2 BP o1 = a); apply (id_neutral_right2 : ?); | intros; simplify; change with (id2 ? o2 ∘ a = a); apply (id_neutral_left2 : ?);] -qed. \ No newline at end of file +qed. + +definition concrete_space_of_CSPA : objs2 CSPA → concrete_space ≝ λx.x. +coercion concrete_space_of_CSPA. + +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. +