From cb98bd7054893edee16aadd6741ec5210b04afbc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 Jan 2009 15:38:23 +0000 Subject: [PATCH] the new coercion behaviour (variants + composition with ID) and the new discipline of declaring hints for carrier of structures (setoids and categories) and no other hints simplified many passages --- .../formal_topology/overlap/basic_pairs.ma | 23 +++-- .../overlap/basic_topologies.ma | 13 --- .../formal_topology/overlap/categories.ma | 62 ++++++------- .../overlap/concrete_spaces.ma | 16 ---- .../overlap/cprop_connectives.ma | 18 ++-- .../overlap/formal_topologies.ma | 25 ----- .../formal_topology/overlap/o-algebra.ma | 92 +++++-------------- .../formal_topology/overlap/o-basic_pairs.ma | 19 +++- .../o-basic_pairs_to_o-basic_topologies.ma | 61 +++++------- .../overlap/o-basic_topologies.ma | 62 +++++-------- .../overlap/o-concrete_spaces.ma | 57 +++++------- .../overlap/o-formal_topologies.ma | 22 ----- .../formal_topology/overlap/relations.ma | 24 +++-- .../overlap/relations_to_o-algebra.ma | 46 ++++------ .../overlap/saturations_to_o-saturations.ma | 2 +- .../formal_topology/overlap/subsets.ma | 4 +- 16 files changed, 194 insertions(+), 352 deletions(-) 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 2635d51ce..a7be5cc6c 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma @@ -20,11 +20,8 @@ record basic_pair: Type1 ≝ rel: arrows1 ? concr form }. -notation "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y}. -notation "⊩" with precedence 60 for @{'Vdash}. - -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" = "setoid1 eq". alias symbol "compose" = "category1 composition". @@ -65,7 +62,12 @@ definition relation_pair_setoid: basic_pair → basic_pair → setoid1. ] qed. -lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩. +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. + +lemma eq_to_eq': + ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩. intros 7 (o1 o2 r r' H c1 f2); split; intro H1; [ lapply (fi ?? (commute ?? r c1 f2) H1) as H2; @@ -139,6 +141,13 @@ definition BP: category1. apply ((id_neutral_left1 ????)‡#);] 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 ⇒ Ω \sup (concr o). intros; constructor 1; [ apply (ext ? ? (rel o)); @@ -178,7 +187,7 @@ 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); + [ apply (λx:concr o.λS: Ω \sup (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]] diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma index 4b53407d1..013ddb94d 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma @@ -24,11 +24,6 @@ record basic_topology: Type1 ≝ compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V) }. -lemma hint: basic_topology → objs1 REL. - intro; apply (carrbt b); -qed. -coercion hint. - record continuous_relation (S,T: basic_topology) : Type1 ≝ { cont_rel:> arrows1 ? S T; reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U); @@ -45,14 +40,6 @@ definition continuous_relation_setoid: basic_topology → basic_topology → set | simplify; intros; apply trans1; [2: apply H |3: apply H1; |1: skip]]] qed. -definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel. - -coercion cont_rel'. - -definition cont_rel'': ∀S,T: basic_topology. continuous_relation_setoid S T → binary_relation S T ≝ cont_rel. - -coercion cont_rel''. - theorem continuous_relation_eq': ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2. a = a' → ∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X). diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma index e22402d9f..c5db6ad60 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma @@ -156,6 +156,9 @@ definition CPROP: setoid1. [ apply (f2 (f x1)) | apply (f1 (f3 z1))]]] qed. +definition CProp0_of_CPROP: carr1 CPROP → CProp0 ≝ λx.x. +coercion CProp0_of_CPROP. + alias symbol "eq" = "setoid1 eq". definition fi': ∀A,B:CPROP. A = B → B → A. intros; apply (fi ?? e); assumption. @@ -196,11 +199,12 @@ definition if_morphism: binary_morphism1 CPROP CPROP CPROP. | apply (fi ?? e1); apply f; apply (if ?? e); assumption]] qed. + record category : Type1 ≝ { objs:> Type0; arrows: objs → objs → setoid; id: ∀o:objs. arrows o o; - comp: ∀o1,o2,o3. binary_morphism1 (arrows o1 o2) (arrows o2 o3) (arrows o1 o3); + comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3); comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34. comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34); id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a; @@ -252,9 +256,9 @@ qed. definition SET: category1. constructor 1; [ apply setoid; - | apply rule (λS,T:setoid.unary_morphism_setoid S T); + | apply rule (λS,T:setoid.setoid1_of_setoid (unary_morphism_setoid S T)); | intros; constructor 1; [ apply (λx:carr o.x); | intros; assumption ] - | intros; constructor 1; [ intros; constructor 1; [ apply (λx. t1 (t x)); | intros; + | intros; constructor 1; [ intros; constructor 1; [ apply (λx. c1 (c x)); | intros; apply († (†e));] | intros; whd; intros; simplify; whd in H1; whd in H; apply trans; [ apply (b (a' a1)); | lapply (prop1 ?? b (a a1) (a' a1)); @@ -265,10 +269,13 @@ definition SET: category1. ] qed. -definition setoid_of_SET: objs1 SET → setoid. - intros; apply o; qed. +definition setoid_of_SET: objs1 SET → setoid ≝ λx.x. coercion setoid_of_SET. +definition unary_morphism_setoid_of_arrows1_SET: + ∀P,Q.arrows1 SET P Q → unary_morphism_setoid P Q ≝ λP,Q,x.x. +coercion unary_morphism_setoid_of_arrows1_SET. + notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }. interpretation "unary morphism" 'Imply a b = (arrows1 SET a b). @@ -285,12 +292,16 @@ definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1. | simplify; intros; apply trans1; [2: apply f; | skip | apply f1]]] qed. +definition unary_morphism1_of_unary_morphism1_setoid1 : + ∀S,T. unary_morphism1_setoid1 S T → unary_morphism1 S T ≝ λP,Q,x.x. +coercion unary_morphism1_of_unary_morphism1_setoid1. + definition SET1: category2. constructor 1; [ apply setoid1; - | apply rule (λS,T.unary_morphism1_setoid1 S T); + | apply rule (λS,T.setoid2_of_setoid1 (unary_morphism1_setoid1 S T)); | intros; constructor 1; [ apply (λx.x); | intros; assumption ] - | intros; constructor 1; [ intros; constructor 1; [ apply (λx. t1 (t x)); | intros; + | intros; constructor 1; [ intros; constructor 1; [ apply (λx. c1 (c x)); | intros; apply († (†e));] | intros; whd; intros; simplify; whd in H1; whd in H; apply trans1; [ apply (b (a' a1)); | lapply (prop11 ?? b (a a1) (a' a1)); @@ -301,36 +312,17 @@ definition SET1: category2. ] qed. -definition setoid1_OF_SET1: objs2 SET1 → setoid1. - intros; apply o; qed. +definition setoid1_of_SET1: objs2 SET1 → setoid1 ≝ λx.x. +coercion setoid1_of_SET1. -coercion setoid1_OF_SET1. +definition unary_morphism1_setoid1_of_arrows2_SET1: + ∀P,Q.arrows2 SET1 P Q → unary_morphism1_setoid1 P Q ≝ λP,Q,x.x. +coercion unary_morphism1_setoid1_of_arrows2_SET1. -definition setoid2_OF_category2: Type_OF_category2 SET1 → setoid2. - intro; apply (setoid2_of_setoid1 t); qed. -coercion setoid2_OF_category2. - -definition objs2_OF_category1: Type_OF_category1 SET → objs2 SET1. - intro; apply (setoid1_of_setoid t); qed. -coercion objs2_OF_category1. +variant objs2_of_category1: objs1 SET → objs2 SET1 ≝ setoid1_of_setoid. +coercion objs2_of_category1. -definition Type1_OF_SET1: Type_OF_category2 SET1 → Type1. - intro; whd in t; apply (carr1 t); -qed. -coercion Type1_OF_SET1. - -definition Type_OF_setoid1_of_carr: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*). - [ apply rule U; - | intros; apply c;] -qed. -coercion Type_OF_setoid1_of_carr. - -definition carr' ≝ λx:Type_OF_category1 SET.Type_OF_Type0 (carr x). -coercion carr'. (* we prefer the lower carrier projection *) +prefer coercion Type_OF_setoid. (* we prefer the lower carrier projection *) +prefer coercion Type_OF_objs1. interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b). - -lemma unary_morphism1_of_arrows1_SET1: ∀S,T. (S ⇒ T) → unary_morphism1 S T. - intros; apply t; -qed. -coercion unary_morphism1_of_arrows1_SET1. diff --git a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma index 5ce337c6f..07a067e73 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma @@ -21,12 +21,6 @@ record concrete_space : Type1 ≝ 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) : Type1 ≝ { rp:> arrows1 ? CS1 CS2; respects_converges: @@ -37,11 +31,6 @@ record convergent_relation_pair (CS1,CS2: concrete_space) : Type1 ≝ 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; @@ -54,11 +43,6 @@ definition convergent_relation_space_setoid: concrete_space → concrete_space | 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 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 aff6849b3..d6c7084b0 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma @@ -19,14 +19,14 @@ definition Type2 : Type3 := Type. definition Type1 : Type2 := Type. definition Type0 : Type1 := Type. -definition Type_OF_Type0: Type0 → Type := λx.x. -definition Type_OF_Type1: Type1 → Type := λx.x. -definition Type_OF_Type2: Type2 → Type := λx.x. -definition Type_OF_Type3: Type3 → Type := λx.x. -coercion Type_OF_Type0. -coercion Type_OF_Type1. -coercion Type_OF_Type2. -coercion Type_OF_Type3. +definition Type_of_Type0: Type0 → Type := λx.x. +definition Type_of_Type1: Type1 → Type := λx.x. +definition Type_of_Type2: Type2 → Type := λx.x. +definition Type_of_Type3: Type3 → Type := λx.x. +coercion Type_of_Type0. +coercion Type_of_Type1. +coercion Type_of_Type2. +coercion Type_of_Type3. definition CProp0 : Type1 := Type0. definition CProp1 : Type2 := Type1. @@ -148,4 +148,4 @@ definition antisymmetric: ∀A:Type0. ∀R:A→A→CProp0. ∀eq:A→A→Prop.CP definition reflexive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x:A.R x x. -definition transitive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x,y,z:A.R x y → R y z → R x z. \ No newline at end of file +definition transitive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x,y,z:A.R x y → R y z → R x z. diff --git a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma index eb2b0b1f7..a611e22ea 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma @@ -14,13 +14,6 @@ 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; @@ -46,9 +39,6 @@ record formal_topology: Type ≝ 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; @@ -64,11 +54,6 @@ record formal_map (S,T: formal_topology) : Type ≝ 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); @@ -79,16 +64,6 @@ definition formal_map_setoid: formal_topology → formal_topology → setoid1. | 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. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma index ca3d0379b..41f9bfd0e 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -63,7 +63,9 @@ record OAlgebra : Type2 := { oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b; oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c; oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a; - oa_meet_inf: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq p (oa_meet I p_i) = ∀i:I.oa_leq p (p_i i); + oa_meet_inf: + ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P. + oa_leq p (oa_meet I p_i) = ∀i:I.oa_leq p (p_i i); oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq (oa_join I p_i) p = ∀i:I.oa_leq (p_i i) p; oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p; oa_one_top: ∀p:oa_P.oa_leq p oa_one; @@ -113,16 +115,6 @@ interpretation "o-algebra join" 'oa_join f = interpretation "o-algebra join with explicit function" 'oa_join_mk f = (fun12 __ (oa_join __) (mk_unary_morphism _ _ f _)). -definition hint3: OAlgebra → setoid1. - intro; apply (oa_P o); -qed. -coercion hint3. - -definition hint4: ∀A. setoid2_OF_OAlgebra A → hint3 A. - intros; apply t; -qed. -coercion hint4. - definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O. intros; split; [ intros (p q); @@ -178,16 +170,11 @@ interpretation "o-algebra join" 'oa_join f = interpretation "o-algebra join with explicit function" 'oa_join_mk f = (fun12 __ (oa_join __) (mk_unary_morphism _ _ f _)). -definition hint5: OAlgebra → objs2 SET1. - intro; apply (oa_P o); -qed. -coercion hint5. - record ORelation (P,Q : OAlgebra) : Type2 ≝ { - or_f_ : P ⇒ Q; - or_f_minus_star_ : P ⇒ Q; - or_f_star_ : Q ⇒ P; - or_f_minus_ : Q ⇒ P; + or_f_ : carr2 (P ⇒ Q); + or_f_minus_star_ : carr2(P ⇒ Q); + or_f_star_ : carr2(Q ⇒ P); + or_f_minus_ : carr2(Q ⇒ P); or_prop1_ : ∀p,q. (or_f_ p ≤ q) = (p ≤ or_f_star_ q); or_prop2_ : ∀p,q. (or_f_minus_ p ≤ q) = (p ≤ or_f_minus_star_ q); or_prop3_ : ∀p,q. (or_f_ p >< q) = (p >< or_f_minus_ q) @@ -214,6 +201,10 @@ constructor 1; | apply (.= (e3 a)); apply e7;]]] qed. +definition ORelation_of_ORelation_setoid : + ∀P,Q.ORelation_setoid P Q → ORelation P Q ≝ λP,Q,x.x. +coercion ORelation_of_ORelation_setoid. + definition or_f_minus_star: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (P ⇒ Q). intros; constructor 1; @@ -227,8 +218,6 @@ definition or_f: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (P ⇒ Q | intros; cases e; assumption] qed. -coercion or_f. - definition or_f_minus: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (Q ⇒ P). intros; constructor 1; [ apply or_f_minus_; @@ -241,36 +230,10 @@ definition or_f_star: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (Q | intros; cases e; assumption] qed. -lemma arrows1_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → (P ⇒ Q). -intros; apply (or_f ?? t); -qed. - -coercion arrows1_OF_ORelation_setoid. - -lemma umorphism_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → unary_morphism1 P Q. -intros; apply (or_f ?? t); +lemma arrows1_of_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → (P ⇒ Q). +intros; apply (or_f ?? c); qed. - -coercion umorphism_OF_ORelation_setoid. - -lemma umorphism_setoid_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → unary_morphism1_setoid1 P Q. -intros; apply (or_f ?? t); -qed. - -coercion umorphism_setoid_OF_ORelation_setoid. - -lemma uncurry_arrows : ∀B,C. ORelation_setoid B C → B → C. -intros; apply (t t1); -qed. - -coercion uncurry_arrows 1. - -(* -lemma hint6: ∀P,Q. Type_OF_setoid2 (hint5 P ⇒ hint5 Q) → unary_morphism1 P Q. - intros; apply t; -qed. -coercion hint6. -*) +coercion arrows1_of_ORelation_setoid. notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}. notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}. @@ -323,7 +286,9 @@ constructor 1; apply or_prop3; ] | intros; split; simplify; - [1,3: unfold umorphism_setoid_OF_ORelation_setoid; unfold arrows1_OF_ORelation_setoid; apply ((†e)‡(†e1)); + [3: unfold arrows1_of_ORelation_setoid; + apply ((†e)‡(†e1)); + |1: apply ((†e)‡(†e1)); |2,4: apply ((†e1)‡(†e));]] qed. @@ -345,22 +310,11 @@ split; | intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;] qed. -lemma setoid1_of_OA: OA → setoid1. - intro; apply (oa_P t); -qed. -coercion setoid1_of_OA. - -lemma SET1_of_OA: OA → SET1. - intro; whd; apply (setoid1_of_OA t); -qed. -coercion SET1_of_OA. +definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x. +coercion OAlgebra_of_objs2_OA. -lemma objs2_SET1_OF_OA: OA → objs2 SET1. - intro; whd; apply (setoid1_of_OA t); -qed. -coercion objs2_SET1_OF_OA. +definition ORelation_setoid_of_arrows2_OA: + ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c. +coercion ORelation_setoid_of_arrows2_OA. -lemma Type_OF_category2_OF_SET1_OF_OA: OA → Type_OF_category2 SET1. - intro; apply (oa_P t); -qed. -coercion Type_OF_category2_OF_SET1_OF_OA. +prefer coercion Type_OF_objs2. \ No newline at end of file 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 956a26af9..6517689a1 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 @@ -20,16 +20,15 @@ record basic_pair: Type2 ≝ rel: arrows2 ? concr form }. -notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}. -notation < "x (⊩ \below c) y" with precedence 45 for @{'Vdash2 $x $y $c}. -notation < "⊩ \sub c" with precedence 60 for @{'Vdash $c}. -notation > "⊩ " with precedence 60 for @{'Vdash ?}. - interpretation "basic pair relation indexed" 'Vdash2 x y c = (rel c x y). interpretation "basic pair relation (non applied)" 'Vdash c = (rel c). alias symbol "eq" = "setoid1 eq". alias symbol "compose" = "category1 composition". +(*DIFFER*) + +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); @@ -68,6 +67,10 @@ definition relation_pair_setoid: basic_pair → basic_pair → setoid2. ] 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. + lemma eq_to_eq': ∀o1,o2.∀r,r': relation_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)); @@ -134,6 +137,12 @@ definition BP: category2. apply ((id_neutral_left2 ????)‡#);] qed. +definition basic_pair_of_objs2_BP: objs2 BP → basic_pair ≝ λx.x. +coercion basic_pair_of_objs2_BP. + +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 BPext: ∀o: BP. form o ⇒ Ω \sup (concr o). 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 f2f6af020..c66e709dd 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 @@ -15,8 +15,10 @@ include "o-basic_pairs.ma". include "o-basic_topologies.ma". +alias symbol "eq" = "setoid1 eq". + (* qui la notazione non va *) -lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = binary_join ? p q. +lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = (binary_join ? p q). intros; apply oa_leq_antisym; [ apply oa_density; intros; @@ -126,18 +128,12 @@ lemma lemma_10_3_d: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R qed. lemma lemma_10_4_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p). - intros; - (* BAD *) - lapply (†(lemma_10_3_a ?? R p)); [2: apply (R⎻* ); | skip | apply Hletin ] + intros; apply (†(lemma_10_3_a ?? R p)); qed. -(* VEERY BAD! *) -axiom lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p). -(* - intros; - (* BAD *) - lapply (†(lemma_10_3_b ?? R p)); [2: apply rule R; | skip | apply Hletin ] -qed. *) +lemma lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p). +intros; unfold in ⊢ (? ? ? % %); apply (†(lemma_10_3_b ?? R p)); +qed. lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U). intros; split; intro; apply oa_overlap_sym; assumption. @@ -145,7 +141,7 @@ qed. (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) definition o_basic_topology_of_o_basic_pair: BP → BTop. - intro; + intro t; constructor 1; [ apply (form t); | apply (□_t ∘ Ext⎽t); @@ -186,42 +182,35 @@ qed. definition o_continuous_relation_of_o_relation_pair: ∀BP1,BP2.arrows2 BP BP1 BP2 → arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2). - intros; + intros (BP1 BP2 t); constructor 1; [ apply (t \sub \f); | unfold o_basic_topology_of_o_basic_pair; simplify; intros; apply sym1; - alias symbol "refl" = "refl1". - apply (.= †?); [1: apply (t \sub \f (((◊_BP1∘(⊩)* ) U))); | - lapply (†e); [2: apply rule t \sub \f; | skip | apply Hletin]] - change in ⊢ (? ? ? % ?) with ((◊_BP2 ∘(⊩)* ) ((t \sub \f ∘ (◊_BP1∘(⊩)* )) U)); - lapply (comp_assoc2 ????? (⊩)* (⊩) t \sub \f); - apply (.= †(Hletin ?)); clear Hletin; + unfold in ⊢ (? ? ? (? ? ? ? %) ?); + apply (.= †(†e)); change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U)); - cut ?; - [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e3 ^ -1 ((⊩)* U));] | 2,4: skip] - apply (.= †Hcut); + cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2: + cases (commute ?? t); apply (e3 ^ -1 ((⊩)* U));] + apply (.= †COM); change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U)); apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U)))); - apply (.= Hcut ^ -1); + apply (.= COM ^ -1); change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U)); - apply (prop11 ?? t \sub \f); - apply (e ^ -1); + change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U); + unfold in ⊢ (? ? ? % %); apply (†e^-1); | unfold o_basic_topology_of_o_basic_pair; simplify; intros; apply sym1; - apply (.= †?); [1: apply (t \sub \f⎻* ((((⊩)⎻* ∘ (⊩)⎻) U))); | - lapply (†e); [2: apply rule (t \sub \f⎻* ); | skip | apply Hletin]] - change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘(⊩)⎻ ) ((t \sub \f⎻* ∘ ((⊩)⎻*∘(⊩)⎻ )) U)); - lapply (comp_assoc2 ????? (⊩)⎻ (⊩)⎻* t \sub \f⎻* ); - apply (.= †(Hletin ?)); clear Hletin; + unfold in ⊢ (? ? ? (? ? ? ? %) ?); + apply (.= †(†e)); change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U)); - cut ?; - [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e1 ^ -1 ((⊩)⎻ U));] | 2,4: skip] - apply (.= †Hcut); + cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2: + cases (commute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));] + apply (.= †COM); change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U)); apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U)))); - apply (.= Hcut ^ -1); + apply (.= COM ^ -1); change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U)); - apply (prop11 ?? t \sub \f⎻* ); - apply (e ^ -1); ] + change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U); + unfold in ⊢ (? ? ? % %); apply (†e^-1);] qed. \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma index 68b9befb8..8847eef31 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma @@ -1,4 +1,4 @@ -(**************************************************************************) + (**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) @@ -24,11 +24,6 @@ record basic_topology: Type2 ≝ compatibility: ∀U,V. (A U >< J V) = (U >< J V) }. -lemma hint: OA → objs2 OA. - intro; apply t; -qed. -coercion hint. - record continuous_relation (S,T: basic_topology) : Type2 ≝ { cont_rel:> arrows2 OA S T; (* reduces uses eq1, saturated uses eq!!! *) @@ -40,24 +35,17 @@ definition continuous_relation_setoid: basic_topology → basic_topology → set intros (S T); constructor 1; [ apply (continuous_relation S T) | constructor 1; - [ (*apply (λr,s:continuous_relation S T.∀b. eq1 (oa_P (carrbt S)) (A ? (r⎻ b)) (A ? (s⎻ b)));*) - apply (λr,s:continuous_relation S T.r⎻* ∘ (A S) = s⎻* ∘ (A ?)); + [ alias symbol "eq" = "setoid2 eq". + alias symbol "compose" = "category2 composition". + apply (λr,s:continuous_relation S T. (r⎻* ) ∘ (A S) = (s⎻* ∘ (A ?))); | simplify; intros; apply refl2; | simplify; intros; apply sym2; apply e | simplify; intros; apply trans2; [2: apply e |3: apply e1; |1: skip]]] qed. -definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows2 ? S T ≝ cont_rel. - -coercion cont_rel'. - -definition cont_rel'': - ∀S,T: basic_topology. - carr2 (continuous_relation_setoid S T) → ORelation_setoid (carrbt S) (carrbt T). - intros; apply rule cont_rel; apply c; -qed. - -coercion cont_rel''. +definition continuous_relation_of_continuous_relation_setoid: + ∀P,Q. continuous_relation_setoid P Q → continuous_relation P Q ≝ λP,Q,c.c. +coercion continuous_relation_of_continuous_relation_setoid. (* theorem continuous_relation_eq': @@ -118,11 +106,8 @@ definition continuous_relation_comp: | intros; apply sym1; change in match ((s ∘ r) U) with (s (r U)); - (**) unfold FunClass_1_OF_Type_OF_setoid21; - unfold objs2_OF_basic_topology1; unfold hint; - letin reduced := reduced; clearbody reduced; - unfold uncurry_arrows in reduced ⊢ %; (**) - apply (.= (reduced : ?)\sup -1); + (**) unfold FunClass_1_OF_carr2; + apply (.= (reduced : ?)\sup -1); [ (*BAD*) change with (eq1 ? (r U) (J ? (r U))); (* BAD U *) apply (.= (reduced ??? U ?)); [ assumption | apply refl1 ] | apply refl1] @@ -150,20 +135,15 @@ definition BTop: category2. change in e with (a⎻* ∘ A o1 = a'⎻* ∘ A o1); change in e1 with (b⎻* ∘ A o2 = b'⎻* ∘ A o2); apply (.= e‡#); - intro x; - change with (b⎻* (a'⎻* (A o1 x)) = b'⎻*(a'⎻* (A o1 x))); - alias symbol "trans" = "trans1". - alias symbol "prop1" = "prop11". - alias symbol "invert" = "setoid1 symmetry". - lapply (.= †(saturated o1 o2 a' (A o1 x) : ?)); - [3: apply (b⎻* ); | 5: apply Hletin; |1,2: skip; - |apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1); ] - change in e1 with (∀x.b⎻* (A o2 x) = b'⎻* (A o2 x)); + intro x; + change with (eq1 ? (b⎻* (a'⎻* (A o1 x))) (b'⎻*(a'⎻* (A o1 x)))); + apply (.= †(saturated o1 o2 a' (A o1 x) ?)); [ + apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);] apply (.= (e1 (a'⎻* (A o1 x)))); - alias symbol "invert" = "setoid1 symmetry". - lapply (†((saturated ?? a' (A o1 x) : ?) ^ -1)); - [2: apply (b'⎻* ); |4: apply Hletin; | skip; - |apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);]] + change with (eq1 ? (b'⎻* (A o2 (a'⎻* (A o1 x)))) (b'⎻*(a'⎻* (A o1 x)))); + apply (.= †(saturated o1 o2 a' (A o1 x):?)^-1); [ + apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);] + apply rule #;] | intros; simplify; change with (((a34⎻* ∘ a23⎻* ) ∘ a12⎻* ) ∘ A o1 = ((a34⎻* ∘ (a23⎻* ∘ a12⎻* )) ∘ A o1)); apply rule (#‡ASSOC ^ -1); @@ -175,8 +155,12 @@ definition BTop: category2. apply (#‡(id_neutral_left2 : ?));] qed. -definition btop_carr: BTop → Type1 ≝ λo:BTop. carr1 (oa_P (carrbt o)). -coercion btop_carr. +definition basic_topology_of_BTop: objs2 BTop → basic_topology ≝ λx.x. +coercion basic_topology_of_BTop. + +definition continuous_relation_setoid_of_arrows2_BTop : + ∀P,Q. arrows2 BTop P Q → continuous_relation_setoid P Q ≝ λP,Q,x.x. +coercion continuous_relation_setoid_of_arrows2_BTop. (* (*CSC: unused! *) 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 b00521633..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 @@ -18,7 +18,7 @@ include "o-saturations.ma". 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'). @@ -42,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". @@ -71,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; @@ -87,19 +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_setoid21 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝ - λCS1,CS2,c.rp ?? c. -coercion rp'''. - -definition rp'''': ∀CS1,CS2.Type_OF_setoid21 (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. @@ -110,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. @@ -147,3 +124,11 @@ definition CSPA: category2. 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 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. + diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma index 4b667546b..e750dcc90 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma @@ -15,10 +15,6 @@ include "o-basic_topologies.ma". (* -definition btop_carr': BTop → setoid1 ≝ λ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)}); @@ -45,9 +41,6 @@ record formal_topology: Type ≝ }. (* -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; @@ -63,11 +56,6 @@ record formal_map (S,T: formal_topology) : Type ≝ 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); @@ -78,16 +66,6 @@ definition formal_map_setoid: formal_topology → formal_topology → setoid1. | 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. diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma index 5678b6a89..74a7c7d78 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma @@ -21,7 +21,7 @@ notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{ notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}. interpretation "relation applied" 'satisfy r x y = (fun21 ___ (satisfy __ r) x y). -definition binary_relation_setoid: SET → SET → SET1. +definition binary_relation_setoid: SET → SET → setoid1. intros (A B); constructor 1; [ apply (binary_relation A B) @@ -36,6 +36,10 @@ definition binary_relation_setoid: SET → SET → SET1. assumption]] qed. +definition binary_relation_of_binary_relation_setoid : + ∀A,B.binary_relation_setoid A B → binary_relation A B ≝ λA,B,c.c. +coercion binary_relation_of_binary_relation_setoid. + definition composition: ∀A,B,C. binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C). @@ -94,6 +98,15 @@ definition REL: category1. first [apply refl | assumption]]] qed. +(* +definition setoid_of_REL : objs1 REL → setoid ≝ λx.x. +coercion setoid_of_REL. +*) + +definition binary_relation_setoid_of_arrow1_REL : + ∀P,Q. arrows1 REL P Q → binary_relation_setoid P Q ≝ λP,Q,x.x. +coercion binary_relation_setoid_of_arrow1_REL. + definition full_subset: ∀s:REL. Ω \sup s. apply (λs.{x | True}); intros; simplify; split; intro; assumption. @@ -101,15 +114,6 @@ qed. coercion full_subset. -definition setoid1_of_REL: REL → setoid ≝ λS. S. -coercion setoid1_of_REL. - -lemma Type_OF_setoid1_of_REL: ∀o1:Type_OF_category1 REL. Type_OF_objs1 o1 → Type_OF_setoid1 ?(*(setoid1_of_SET o1)*). - [ apply rule o1; - | intros; apply t;] -qed. -coercion Type_OF_setoid1_of_REL. - definition comprehension: ∀b:REL. (unary_morphism1 b CPROP) → Ω \sup b. apply (λb:REL. λP: b ⇒ CPROP. {x | P x}); intros; simplify; 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 856a7e0ae..3317c0e64 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 @@ -52,30 +52,30 @@ definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA ( intros; constructor 1; [ constructor 1; - [ apply (λU.image ?? t U); + [ apply (λU.image ?? c U); | intros; apply (#‡e); ] | constructor 1; - [ apply (λU.minus_star_image ?? t U); + [ apply (λU.minus_star_image ?? c U); | intros; apply (#‡e); ] | constructor 1; - [ apply (λU.star_image ?? t U); + [ apply (λU.star_image ?? c U); | intros; apply (#‡e); ] | constructor 1; - [ apply (λU.minus_image ?? t U); + [ apply (λU.minus_image ?? c U); | intros; apply (#‡e); ] | intros; split; intro; - [ change in f with (∀a. a ∈ image ?? t p → a ∈ q); - change with (∀a:o1. a ∈ p → a ∈ star_image ?? t q); + [ change in f with (∀a. a ∈ image ?? c p → a ∈ q); + change with (∀a:o1. a ∈ p → a ∈ star_image ?? c q); intros 4; apply f; exists; [apply a] split; assumption; - | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? t q); - change with (∀a. a ∈ image ?? t p → a ∈ q); + | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? c q); + change with (∀a. a ∈ image ?? c p → a ∈ q); intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ] | intros; split; intro; - [ change in f with (∀a. a ∈ minus_image ?? t p → a ∈ q); - change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q); + [ change in f with (∀a. a ∈ minus_image ?? c p → a ∈ q); + change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? c q); intros 4; apply f; exists; [apply a] split; assumption; - | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q); - change with (∀a. a ∈ minus_image ?? t p → a ∈ q); + | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? c q); + change with (∀a. a ∈ minus_image ?? c p → a ∈ q); intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ] | intros; split; intro; cases f; clear f; [ cases x; cases x2; clear x x2; exists; [apply w1] @@ -87,7 +87,7 @@ definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA ( qed. lemma orelation_of_relation_preserves_equality: - ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2. eq1 ? t t' → orelation_of_relation ?? t = orelation_of_relation ?? t'. + ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2. t = t' → eq2 ? (orelation_of_relation ?? t) (orelation_of_relation ?? t'). intros; split; unfold orelation_of_relation; simplify; intro; split; intro; simplify; whd in o1 o2; [ change with (a1 ∈ minus_star_image ?? t a → a1 ∈ minus_star_image ?? t' a); @@ -108,13 +108,8 @@ lemma orelation_of_relation_preserves_equality: apply (. #‡(e‡#)); ] qed. -lemma hint: ∀o1,o2:OA. Type_OF_setoid21 (arrows2 ? o1 o2) → carr2 (arrows2 OA o1 o2). - intros; apply t; -qed. -coercion hint. - lemma orelation_of_relation_preserves_identity: - ∀o1:REL. orelation_of_relation ?? (id1 ? o1) = id2 OA (SUBSETS o1). + ∀o1:REL. eq2 ? (orelation_of_relation ?? (id1 ? o1)) (id2 OA (SUBSETS o1)). intros; split; intro; split; whd; intro; [ change with ((∀x. x ♮(id1 REL o1) a1→x∈a) → a1 ∈ a); intros; apply (f a1); change with (a1 = a1); apply refl1; @@ -136,13 +131,10 @@ lemma orelation_of_relation_preserves_identity: | change with (a1 ∈ a → ∀y.a1 ♮(id1 REL o1) y→y∈a); intros; change in f1 with (a1 = y); apply (. f1^-1‡#); apply f;] qed. -(* -lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid21 (arrows2 OA S T). - intros; apply c; -qed. -coercion hint2. -*) + (* CSC: ???? forse un uncertain mancato *) +alias symbol "eq" = "setoid2 eq". +alias symbol "compose" = "category1 composition". lemma orelation_of_relation_preserves_composition: ∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3. orelation_of_relation ?? (G ∘ F) = @@ -156,10 +148,10 @@ lemma orelation_of_relation_preserves_composition: split; [ assumption | exists; [apply w] split; assumption ] | cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ] split; [ exists; [apply w] split; assumption | assumption ] - | unfold arrows1_OF_ORelation_setoid; + | unfold arrows1_of_ORelation_setoid; cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ] split; [ assumption | exists; [apply w] split; assumption ] - | unfold arrows1_OF_ORelation_setoid in e; + | unfold arrows1_of_ORelation_setoid in e; cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ] split; [ exists; [apply w] split; assumption | assumption ] | whd; intros; apply f; exists; [ apply y] split; assumption; diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma index ce6c6f110..97bfcd6c9 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma @@ -20,7 +20,7 @@ include "relations_to_o-algebra.ma". definition o_operator_of_operator: ∀C:REL. (Ω \sup C => Ω \sup C) → (SUBSETS C ⇒ SUBSETS C). - intros;apply t; + intros (C t);apply t; qed. definition is_o_saturation_of_is_saturation: diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma index eaa6954a4..e6d187216 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma @@ -145,7 +145,7 @@ definition big_intersects: ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)). intros; constructor 1; [ intro; whd; whd in I; - apply ({x | ∀i:I. x ∈ t i}); + apply ({x | ∀i:I. x ∈ c i}); simplify; intros; split; intros; [ apply (. (e^-1‡#)); | apply (. e‡#); ] apply f; | intros; split; intros 2; simplify in f ⊢ %; intro; @@ -157,7 +157,7 @@ definition big_union: ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)). intros; constructor 1; [ intro; whd; whd in A; whd in I; - apply ({x | ∃i:I. x ∈ t i }); + apply ({x | ∃i:I. x ∈ c i }); simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w] [ apply (. (e^-1‡#)); | apply (. (e‡#)); ] apply x; -- 2.39.2