From 5bed3ef9523751da77b0c57a85fd880083cde248 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 22 Jul 2010 08:11:22 +0000 Subject: [PATCH] ... --- .../formal_topology/basic_topologies.ma | 56 +++++++-------- .../basic_topologies_to_o-basic_topologies.ma | 70 +++++++------------ .../library/formal_topology/relations.ma | 45 ++++++------ .../formal_topology/relations_to_o-algebra.ma | 15 ++-- 4 files changed, 80 insertions(+), 106 deletions(-) diff --git a/helm/software/matita/library/formal_topology/basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies.ma index 7ebec5e3f..0177afb63 100644 --- a/helm/software/matita/library/formal_topology/basic_topologies.ma +++ b/helm/software/matita/library/formal_topology/basic_topologies.ma @@ -24,12 +24,10 @@ record basic_topology: Type1 ≝ compatibility: ∀U,V. (A U ≬ J V) =_1 (U ≬ J V) }. -definition foo : ∀o1,o2:REL.carr1 (o1 ⇒_\r1 o2) → carr2 (setoid2_of_setoid1 (o1 ⇒_\r1 o2)) ≝ λo1,o2,x.x. - record continuous_relation (S,T: basic_topology) : Type1 ≝ { cont_rel:> S ⇒_\r1 T; reduced: ∀U. U =_1 J ? U → image_coercion ?? cont_rel U =_1 J ? (image_coercion ?? cont_rel U); - saturated: ∀U. U =_1 A ? U → (foo ?? cont_rel)⎻* U = _1A ? ((foo ?? cont_rel)⎻* U) + saturated: ∀U. U =_1 A ? U → (cont_rel)⎻* U = _1A ? ((cont_rel)⎻* U) }. definition continuous_relation_setoid: basic_topology → basic_topology → setoid1. @@ -48,7 +46,7 @@ coercion continuos_relation_of_continuous_relation_setoid. axiom continuous_relation_eq': ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2. - a = a' → ∀X.(foo ?? a)⎻* (A o1 X) = (foo ?? a')⎻* (A o1 X). + a = a' → ∀X.a⎻* (A o1 X) = a'⎻* (A o1 X). (* intros; split; intro; unfold minus_star_image; simplify; intros; [ cut (ext ?? a a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;] @@ -65,35 +63,34 @@ axiom continuous_relation_eq': [ apply I | assumption ]] qed.*) -axiom continuous_relation_eq_inv': +lemma continuous_relation_eq_inv': ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2. - (∀X.(foo ?? a)⎻* (A o1 X) = (foo ?? a')⎻* (A o1 X)) → a=a'. -(* intros 6; + (∀X.a⎻* (A o1 X) = a'⎻* (A o1 X)) → a=a'. + intros 6; cut (∀a,a': continuous_relation_setoid o1 o2. - (∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X)) → + (∀X.a⎻* (A o1 X) = a'⎻* (A o1 X)) → ∀V:o2. A ? (ext ?? a' V) ⊆ A ? (ext ?? a V)); - [2: clear b H a' a; intros; + [2: clear b f a' a; intros; lapply depth=0 (λV.saturation_expansive ??? (extS ?? a V)); [2: apply A_is_saturation;|skip] (* fundamental adjunction here! to be taken out *) - cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a (A ? (extS ?? a V))); + cut (∀V:Ω^o2.V ⊆ a⎻* (A ? (extS ?? a V))); [2: intro; intros 2; unfold minus_star_image; simplify; intros; apply (Hletin V1 x); whd; split; [ exact I | exists; [apply a1] split; assumption]] clear Hletin; - cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a' (A ? (extS ?? a V))); - [2: intro; apply (. #‡(H ?)); apply Hcut] clear H Hcut; + cut (∀V:Ω^o2.V ⊆ a'⎻* (A ? (extS ?? a V))); + [2: intro; apply (. #‡(f ?)^-1); apply Hcut] clear f Hcut; (* second half of the fundamental adjunction here! to be taken out too *) - intro; lapply (Hcut1 (singleton ? V)); clear Hcut1; + intro; lapply (Hcut1 {(V)}); clear Hcut1; unfold minus_star_image in Hletin; unfold singleton in Hletin; simplify in Hletin; whd in Hletin; whd in Hletin:(?→?→%); simplify in Hletin; apply (if ?? (A_is_saturation ???)); intros 2 (x H); lapply (Hletin V ? x ?); - [ apply refl | cases H; assumption; ] + [ apply refl | unfold foo; apply H; ] change with (x ∈ A ? (ext ?? a V)); - apply (. #‡(†(extS_singleton ????))); + apply (. #‡(†(extS_singleton ????)^-1)); assumption;] - split; apply Hcut; [2: assumption | intro; apply sym1; apply H] + split; apply Hcut; [2: assumption | intro; apply sym1; apply f] qed. -*) definition continuous_relation_comp: ∀o1,o2,o3. @@ -113,11 +110,11 @@ apply (s ∘ r) apply (.= (image_comp ??????)^-1); apply refl1] | intros; - apply sym1; unfold foo; - apply (.= †(minus_star_image_comp ??????)); - apply (.= (saturated ?? s ((foo ?? r)⎻* U) ?)^-1); + apply sym1; + apply (.= †(minus_star_image_comp ??? s r ?)); + apply (.= (saturated ?? s ((r)⎻* U) ?)^-1); [ apply (.= (saturated ?????)); [ assumption | apply refl1 ] - | change in ⊢ (? ? ? % ?) with (((foo ?? s)⎻* ∘ (foo ?? r)⎻* ) U); + | change in ⊢ (? ? ? % ?) with ((s⎻* ∘ r⎻* ) U); apply (.= (minus_star_image_comp ??????)^-1); apply refl1]] qed. @@ -145,26 +142,25 @@ definition BTop: category1. | intros; simplify; intro x; simplify; lapply depth=0 (continuous_relation_eq' ???? e) as H'; lapply depth=0 (continuous_relation_eq' ???? e1) as H1'; - letin K ≝ (λX.H1' (minus_star_image ?? (foo ?? a) (A ? X))); clearbody K; + letin K ≝ (λX.H1' ((a)⎻* (A ? X))); clearbody K; cut (∀X:Ω \sup o1. - minus_star_image o2 o3 (foo ?? b) (A o2 (minus_star_image o1 o2 (foo ?? a) (A o1 X))) - =_1 minus_star_image o2 o3 (foo ?? b') (A o2 (minus_star_image o1 o2 (foo ?? a') (A o1 X)))); + (b)⎻* (A o2 ((a)⎻* (A o1 X))) + =_1 (b')⎻* (A o2 ((a')⎻* (A o1 X)))); [2: intro; apply sym1; apply (.= (†(†((H' X)^-1)))); apply sym1; apply (K X);] clear K H' H1'; -alias symbol "compose" (instance 1) = "category1 composition". -alias symbol "compose" (instance 1) = "category1 composition". -alias symbol "compose" (instance 1) = "category1 composition". +alias symbol "powerset" (instance 5) = "powerset low". +alias symbol "compose" (instance 2) = "category1 composition". cut (∀X:Ω^o1. - minus_star_image ?? (foo ?? (b ∘ a)) (A o1 X) =_1 minus_star_image ?? (foo ?? (b'∘a')) (A o1 X)); + ((b ∘ a))⎻* (A o1 X) =_1 ((b'∘a'))⎻* (A o1 X)); [2: intro; unfold foo; apply (.= (minus_star_image_comp ??????)); - change in ⊢ (? ? ? % ?) with ((foo ?? b)⎻* ((foo ?? a)⎻* (A o1 X))); + change in ⊢ (? ? ? % ?) with ((b)⎻* ((a)⎻* (A o1 X))); apply (.= †(saturated ?????)); [ apply ((saturation_idempotent ????)^-1); apply A_is_saturation ] apply sym1; apply (.= (minus_star_image_comp ??????)); - change in ⊢ (? ? ? % ?) with ((foo ?? b')⎻* ((foo ?? a')⎻* (A o1 X))); + change in ⊢ (? ? ? % ?) with ((b')⎻* ((a')⎻* (A o1 X))); apply (.= †(saturated ?????)); [ apply ((saturation_idempotent ????)^-1); apply A_is_saturation ] apply ((Hcut X)^-1)] diff --git a/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma index 0d997a5af..58b75fb68 100644 --- a/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma +++ b/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma @@ -49,63 +49,43 @@ definition BTop_to_OBTop: carr3 ((category2_of_category1 BTop) ⇒_\c3 OBTop). | cases daemon (*apply o_relation_topology_of_relation_topology_morphism_respects_comp*);] qed. -(* FIXME -alias symbol "eq" (instance 2) = "setoid1 eq". -alias symbol "eq" (instance 1) = "setoid2 eq". theorem BTop_to_OBTop_faithful: faithful2 ?? BTop_to_OBTop. - intros 5; - whd in e; unfold BTop_to_OBTop in e; simplify in e; - change in match (oA ?) in e with (A o1); - whd in f g; - alias symbol "OR_f_minus_star" (instance 1) = "relation f⎻*". - change in match ((o_continuous_relation_of_continuous_relation_morphism o1 o2 f)⎻* ) in e with ((foo ?? f)⎻* ); - change in match ((o_continuous_relation_of_continuous_relation_morphism o1 o2 g)⎻* ) in e with ((foo ?? g)⎻* ); - whd; whd in o1 o2; - intro b; - alias symbol "OR_f_minus" (instance 1) = "relation f⎻". - letin fb ≝ ((ext ?? f) b); - lapply (e fb); - whd in Hletin:(? ? ? % %); - cases (Hletin); simplify in s s1; - split; - [2: intro; simplify; - lapply depth=0 (s b); intro; apply (Hletin1 ? a ?) - [ 2: whd in f1; - change in Hletin with ((foo ?? f)⎻* - - alias symbol "OR_f_minus_star" (instance 4) = "relation f⎻*". - alias symbol "OR_f_minus_star" (instance 4) = "relation f⎻*". -change in e with - (comp2 SET1 (Ω^o1) (Ω^o1) (Ω^o2) (A o1) (foo o1 o2 f)⎻* =_1 - comp2 SET1 (Ω^o1) (Ω^o1) (Ω^o2) (A o1) (foo o1 o2 g)⎻* - ); - - - - change in e with (comp1 SET (Ω^o1) ?? (A o1) (foo o1 o2 f)⎻* = ((foo o1 o2 g)⎻* ∘ A o1)); - unfold o_continuous_relation_of_continuous_relation_morphism in e; - unfold o_continuous_relation_of_continuous_relation in e; - simplify in e; + intros 5; apply (continuous_relation_eq_inv' o1 o2 f g); apply e; qed. include "formal_topology/notation.ma". -theorem BTop_to_OBTop_full: - ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BTop_to_OBTop S T g = f). - intros; +theorem BTop_to_OBTop_full: full2 ?? BTop_to_OBTop. + intros 3 (S T); cases (POW_full (carrbt S) (carrbt T) (Ocont_rel ?? f)) (g Hg); - exists[ + (* cases Hg; *) + exists [ constructor 1; [ apply g - | apply hide; intros; lapply (Oreduced ?? f ? e); + | unfold image_coercion; cases daemon (*apply hide; intros; lapply (Oreduced ?? f ? e); unfold image_coercion; cases Hg; lapply (e3 U) as K; apply (.= K); - apply (.= Hletin); apply rule (†(K^-1)); - | apply hide; intros; lapply (Osaturated ?? f ? e); + apply (.= Hletin); apply rule (†(K^-1)); *) + | cases daemon (* apply hide; intros; lapply (Osaturated ?? f ? e); cases Hg; lapply (e1 U) as K; apply (.= K); - apply (.= Hletin); apply rule (†(K^-1)); + apply (.= Hletin); apply rule (†(K^-1)); *) ] | simplify; unfold BTop_to_OBTop; simplify; + cases Hg; unfold o_continuous_relation_of_continuous_relation_morphism; + simplify; + change with ((orelation_of_relation ?? g)⎻* ∘ oA (o_basic_topology_of_basic_topology S) = + f⎻* ∘ oA (o_basic_topology_of_basic_topology S)); + + + change with (g⎻* ∘ oA (o_basic_topology_of_basic_topology S) = + f⎻* ∘ oA (o_basic_topology_of_basic_topology S)); + apply sym2; whd in T; + intro; + apply trans2; [2: apply sym2; [2: apply Hg; + + whd in ⊢ (?(??%%)???); + apply (.= Hg^-1); unfold o_continuous_relation_of_continuous_relation_morphism; simplify; - cases Hg; whd; simplify; intro; + intro; simplify; + unfold image_coercion; cases Hg; whd; simplify; intro; simplify; qed. *) diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma index 1503fa5de..789f312cf 100644 --- a/helm/software/matita/library/formal_topology/relations.ma +++ b/helm/software/matita/library/formal_topology/relations.ma @@ -140,25 +140,24 @@ definition ext: ∀X,S:REL. (X ⇒_\r1 S) × S ⇒_1 (Ω^X). apply (. (#‡e1)); whd in e; apply (fi ?? (e ??));assumption]] qed. -(* -definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X. +definition extS: ∀X,S:REL. ∀r:X ⇒_\r1 S. Ω^S ⇒_1 Ω^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; [ intro F; constructor 1; constructor 1; [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a); | intros; split; intro; cases f (H1 H2); clear f; split; - [ apply (. (H‡#)); assumption - |3: apply (. (H\sup -1‡#)); assumption + [ apply (. (e^-1‡#)); assumption + |3: apply (. (e‡#)); assumption |2,4: cases H2 (w H3); exists; [1,3: apply w] - [ apply (. (#‡(H‡#))); assumption - | apply (. (#‡(H \sup -1‡#))); assumption]]] - | intros; split; simplify; intros; cases f; cases H1; split; + [ apply (. (#‡(e^-1‡#))); assumption + | apply (. (#‡(e‡#))); assumption]]] + | intros; split; simplify; intros; cases f; cases e1; split; [1,3: assumption |2,4: exists; [1,3: apply w] - [ apply (. (#‡H)‡#); assumption - | apply (. (#‡H\sup -1)‡#); assumption]]] + [ apply (. (#‡e^-1)‡#); assumption + | apply (. (#‡e)‡#); assumption]]] qed. - +(* lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X. intros; unfold extS; simplify; @@ -251,9 +250,11 @@ definition minus_image: ∀U,V:REL. (U ⇒_\r1 V) ⇒_2 (Ω^V ⇒_2 Ω^U). [ apply (. e^-1 a2 w); | apply (. e a2 w)] assumption;] qed. -interpretation "relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (minus_star_image ? ?) r). -interpretation "relation f⎻" 'OR_f_minus r = (fun12 ?? (minus_image ? ?) r). -interpretation "relation f*" 'OR_f_star r = (fun12 ?? (star_image ? ?) r). +definition foo : ∀o1,o2:REL.carr1 (o1 ⇒_\r1 o2) → carr2 (setoid2_of_setoid1 (o1 ⇒_\r1 o2)) ≝ λo1,o2,x.x. + +interpretation "relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (minus_star_image ? ?) (foo ?? r)). +interpretation "relation f⎻" 'OR_f_minus r = (fun12 ?? (minus_image ? ?) (foo ?? r)). +interpretation "relation f*" 'OR_f_star r = (fun12 ?? (star_image ? ?) (foo ?? r)). definition image_coercion: ∀U,V:REL. (U ⇒_\r1 V) → Ω^U ⇒_2 Ω^V. intros (U V r Us); apply (image U V r); qed. @@ -271,7 +272,8 @@ theorem image_id: ∀o. (id1 REL o : carr2 (Ω^o ⇒_2 Ω^o)) =_1 (id2 SET1 Ω^o exists; [apply a] split; [ change with (a = a); apply refl1 | assumption]] qed. -theorem minus_star_image_id: ∀o:REL. (fun12 ?? (minus_star_image o o) (id1 REL o) : carr2 (Ω^o ⇒_2 Ω^o)) =_1 (id2 SET1 Ω^o). +theorem minus_star_image_id: ∀o:REL. + ((id1 REL o)⎻* : carr2 (Ω^o ⇒_2 Ω^o)) =_1 (id2 SET1 Ω^o). intros; unfold minus_star_image; simplify; intro U; simplify; split; simplify; intros; [ change with (a ∈ U); apply f; change with (a=a); apply refl1 @@ -296,6 +298,7 @@ theorem minus_star_image_comp: | cases f1; cases x1; apply f; assumption] qed. + (* (*CSC: unused! *) theorem ext_comp: @@ -311,13 +314,13 @@ theorem ext_comp: | cases H; clear H; cases x1; clear x1; exists [apply w]; split; [2: cases f] assumption] qed. +*) + +axiom daemon : False. theorem extS_singleton: - ∀o1,o2.∀a:arrows1 ? o1 o2.∀x.extS o1 o2 a (singleton o2 x) = ext o1 o2 a x. + ∀o1,o2.∀a.∀x.extS o1 o2 a {(x)} = ext o1 o2 a x. intros; unfold extS; unfold ext; unfold singleton; simplify; - split; intros 2; simplify; cases f; split; try assumption; - [ cases H; cases x1; change in f2 with (eq1 ? x w); apply (. #‡f2 \sup -1); - assumption - | exists; try assumption; split; try assumption; change with (x = x); apply refl] -qed. -*) + split; intros 2; simplify; simplify in f; + [ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption; + | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed. \ No newline at end of file diff --git a/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma b/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma index 01c06f020..bc5153d5d 100644 --- a/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma +++ b/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma @@ -51,15 +51,13 @@ qed. definition powerset_of_POW': ∀A.oa_P (POW' A) → Ω^A ≝ λA,x.x. coercion powerset_of_POW'. -definition foo : ∀o1,o2:REL.carr1 (o1 ⇒_\r1 o2) → carr2 (setoid2_of_setoid1 (o1 ⇒_\r1 o2)) ≝ λo1,o2,x.x. - definition orelation_of_relation: ∀o1,o2:REL. o1 ⇒_\r1 o2 → (POW' o1) ⇒_\o2 (POW' o2). intros; constructor 1; [ apply rule c; - | apply rule ((foo ?? c)⎻* ); - | apply rule ((foo ?? c)* ); - | apply rule ((foo ?? c)⎻); + | apply rule (c⎻* ); + | apply rule (c* ); + | apply rule (c⎻); | intros; split; intro; [ intros 2; intros 2; apply (f y); exists[apply a] split; assumption; | intros 2; change with (a ∈ q); cases f1; cases x; clear f1 x; @@ -82,7 +80,7 @@ lemma orelation_of_relation_preserves_equality: change in e with (t =_2 t'); unfold image_coercion; apply (†e); qed. -lemma minus_image_id : ∀o:REL.(foo ?? (id1 REL o))⎻ =_1 (id2 SET1 Ω^o). +lemma minus_image_id : ∀o:REL.((id1 REL o))⎻ =_1 (id2 SET1 Ω^o). unfold foo; intro o; intro; unfold minus_image; simplify; split; simplify; intros; [ cases e; cases x; change with (a1 ∈ a); change in f with (a1 =_1 w); apply (. f‡#); assumption; @@ -90,7 +88,7 @@ unfold foo; intro o; intro; unfold minus_image; simplify; split; simplify; intro change with (a1 =_1 a1); apply refl1;] qed. -lemma star_image_id : ∀o:REL. (foo ?? (id1 REL o))* =_1 (id2 SET1 Ω^o). +lemma star_image_id : ∀o:REL. ((id1 REL o))* =_1 (id2 SET1 Ω^o). unfold foo; intro o; intro; unfold star_image; simplify; split; simplify; intros; [ change with (a1 ∈ a); apply f; change with (a1 =_1 a1); apply rule refl1; | change in f1 with (a1 =_1 y); apply (. f1^-1‡#); apply f;] @@ -190,9 +188,6 @@ theorem POW_full: full2 ?? POW. [4: apply mem; |6: apply Hletin;|1,2,3,5: skip] lapply (#‡prop11 ?? f ?? (†e)); [6: apply Hletin; |*:skip ]] | (split; intro; split; simplify); - (* - whd; split; whd; intro; simplify; unfold map_arrows2; simplify; - [ split;*) [ change with (∀a1.(∀x. a1 ∈ (f {(x):S}) → x ∈ a) → a1 ∈ f⎻* a); | change with (∀a1.a1 ∈ f⎻* a → (∀x.a1 ∈ f {(x):S} → x ∈ a)); | alias symbol "and" (instance 4) = "and_morphism". -- 2.39.2