From 13088dbb8e54833dfbe2d6c38b08d78fc36452a8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 10 Jul 2010 16:29:47 +0000 Subject: [PATCH] big mess of notation --- .../library/formal_topology/basic_pairs.ma | 9 +- .../basic_pairs_to_basic_topologies.ma | 4 +- .../formal_topology/basic_topologies.ma | 57 +++++---- .../basic_topologies_to_o-basic_topologies.ma | 46 +++++-- .../library/formal_topology/categories.ma | 9 ++ .../library/formal_topology/o-algebra.ma | 11 +- .../library/formal_topology/relations.ma | 121 ++++++++++-------- .../formal_topology/relations_to_o-algebra.ma | 121 +++++++++--------- .../matita/library/formal_topology/subsets.ma | 2 +- 9 files changed, 219 insertions(+), 161 deletions(-) diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma index 8235b2571..ecf27345d 100644 --- a/helm/software/matita/library/formal_topology/basic_pairs.ma +++ b/helm/software/matita/library/formal_topology/basic_pairs.ma @@ -24,7 +24,7 @@ interpretation "basic pair relation (non applied)" 'Vdash c = (rel c). record relation_pair (BP1,BP2: basic_pair): Type1 ≝ { concr_rel: (concr BP1) ⇒_\r1 (concr BP2); form_rel: (form BP1) ⇒_\r1 (form BP2); - commute: ⊩ ∘ concr_rel =_1 form_rel ∘ ⊩ + commute: comp1 REL ??? concr_rel (rel ?) =_1 form_rel ∘ ⊩ }. interpretation "concrete relation" 'concr_rel r = (concr_rel ?? r). @@ -49,8 +49,9 @@ 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. +alias symbol "compose" (instance 1) = "category1 composition". lemma eq_to_eq': - ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r =_1 r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩. + ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r =_1 r' → r \sub\f ∘ ⊩ =_1 r'\sub\f ∘ ⊩. intros 5 (o1 o2 r r' H); apply (.= (commute ?? r)^-1); change in H with (⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c); @@ -65,7 +66,7 @@ definition id_relation_pair: ∀o:basic_pair. relation_pair o o. | lapply (id_neutral_right1 ? (concr o) ? (⊩)) as H; lapply (id_neutral_left1 ?? (form o) (⊩)) as H1; apply (.= H); - apply (H1 \sup -1);] + apply (H1^-1);] qed. lemma relation_pair_composition: @@ -106,7 +107,7 @@ intros 3 (o1 o2 o3); apply (.= ASSOC ^ -1); apply (.= e‡#); apply (.= ASSOC); - apply (.= #‡(commute ?? b')\sup -1); + apply (.= #‡(commute ?? b')^-1); apply (ASSOC ^ -1); qed. diff --git a/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma index fe4cbd10f..fb8891613 100644 --- a/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma +++ b/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma @@ -52,11 +52,13 @@ record functor1 (C1: category1) (C2: category1) : Type2 ≝ (* definition BTop_of_BP: functor1 BP BTop. - lapply OR as F; constructor 1; [ apply basic_topology_of_basic_pair | intros; constructor 1 [ apply continuous_relation_of_relation_pair; ] | simplify; intro; ] qed. + +lemma BBBB_faithful : failthful2 ?? VVV +FIXME *) \ No newline at end of file diff --git a/helm/software/matita/library/formal_topology/basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies.ma index 0c153b9d3..7ebec5e3f 100644 --- a/helm/software/matita/library/formal_topology/basic_topologies.ma +++ b/helm/software/matita/library/formal_topology/basic_topologies.ma @@ -24,10 +24,12 @@ 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:> arrows1 ? S T; - reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U); - saturated: ∀U. U = A ? U → minus_star_image ?? cont_rel U = A ? (minus_star_image ?? cont_rel U) + { 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) }. definition continuous_relation_setoid: basic_topology → basic_topology → setoid1. @@ -46,7 +48,7 @@ coercion continuos_relation_of_continuous_relation_setoid. axiom 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). + a = a' → ∀X.(foo ?? a)⎻* (A o1 X) = (foo ?? 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,7 +67,7 @@ qed.*) axiom continuous_relation_eq_inv': ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2. - (∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X)) → a=a'. + (∀X.(foo ?? a)⎻* (A o1 X) = (foo ?? 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)) → @@ -99,20 +101,24 @@ definition continuous_relation_comp: continuous_relation_setoid o2 o3 → continuous_relation_setoid o1 o3. intros (o1 o2 o3 r s); constructor 1; - [ apply (s ∘ r) + [ alias symbol "compose" (instance 1) = "category1 composition". +apply (s ∘ r) | intros; - apply sym1; + apply sym1; + (*change in ⊢ (? ? ? (? ? ? ? %) ?) with (image_coercion ?? (s ∘ r) U);*) apply (.= †(image_comp ??????)); - apply (.= (reduced ?????)\sup -1); + apply (.= (reduced ?? s (image_coercion ?? r U) ?)^-1); [ apply (.= (reduced ?????)); [ assumption | apply refl1 ] - | apply (.= (image_comp ??????)\sup -1); + | change in ⊢ (? ? ? % ?) with ((image_coercion ?? s ∘ image_coercion ?? r) U); + apply (.= (image_comp ??????)^-1); apply refl1] | intros; - apply sym1; + apply sym1; unfold foo; apply (.= †(minus_star_image_comp ??????)); - apply (.= (saturated ?????)\sup -1); + apply (.= (saturated ?? s ((foo ?? r)⎻* U) ?)^-1); [ apply (.= (saturated ?????)); [ assumption | apply refl1 ] - | apply (.= (minus_star_image_comp ??????)\sup -1); + | change in ⊢ (? ? ? % ?) with (((foo ?? s)⎻* ∘ (foo ?? r)⎻* ) U); + apply (.= (minus_star_image_comp ??????)^-1); apply refl1]] qed. @@ -139,24 +145,29 @@ 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 ?? a (A ? X))); clearbody K; + letin K ≝ (λX.H1' (minus_star_image ?? (foo ?? a) (A ? X))); clearbody K; cut (∀X:Ω \sup o1. - minus_star_image o2 o3 b (A o2 (minus_star_image o1 o2 a (A o1 X))) - = minus_star_image o2 o3 b' (A o2 (minus_star_image o1 o2 a' (A o1 X)))); - [2: intro; apply sym1; apply (.= #‡(†((H' ?)\sup -1))); apply sym1; apply (K X);] + 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)))); + [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". cut (∀X:Ω^o1. - minus_star_image ?? (b ∘ a) (A o1 X) =_1 minus_star_image ?? (b'∘a') (A o1 X)); - [2: intro; + minus_star_image ?? (foo ?? (b ∘ a)) (A o1 X) =_1 minus_star_image ?? (foo ?? (b'∘a')) (A o1 X)); + [2: intro; unfold foo; apply (.= (minus_star_image_comp ??????)); - apply (.= #‡(saturated ?????)); - [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ] + change in ⊢ (? ? ? % ?) with ((foo ?? b)⎻* ((foo ?? a)⎻* (A o1 X))); + apply (.= †(saturated ?????)); + [ apply ((saturation_idempotent ????)^-1); apply A_is_saturation ] apply sym1; apply (.= (minus_star_image_comp ??????)); - apply (.= #‡(saturated ?????)); - [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ] - apply ((Hcut X) \sup -1)] + change in ⊢ (? ? ? % ?) with ((foo ?? b')⎻* ((foo ?? a')⎻* (A o1 X))); + apply (.= †(saturated ?????)); + [ apply ((saturation_idempotent ????)^-1); apply A_is_saturation ] + apply ((Hcut X)^-1)] clear Hcut; generalize in match x; clear x; apply (continuous_relation_eq_inv'); apply Hcut1;] 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 b1592f6ea..0d997a5af 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,19 +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: - ∀S,T.∀f,g:arrows2 (category2_of_category1 BTop) S T. - map_arrows2 ?? BTop_to_OBTop ?? f = map_arrows2 ?? BTop_to_OBTop ?? g → f=g. - intros; change with (∀b.A ? (ext ?? f b) = A ? (ext ?? g b)); - apply (POW_faithful); - apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) f \sub \c (⊩ \sub T)); - apply sym2; - apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) g \sub \c (⊩ \sub T)); - apply sym2; - apply e; +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; qed. include "formal_topology/notation.ma". diff --git a/helm/software/matita/library/formal_topology/categories.ma b/helm/software/matita/library/formal_topology/categories.ma index 30769e536..015e245f3 100644 --- a/helm/software/matita/library/formal_topology/categories.ma +++ b/helm/software/matita/library/formal_topology/categories.ma @@ -511,3 +511,12 @@ definition faithful2 ≝ λA,B:CAT2.λF:carr3 (arrows3 CAT2 A B). ∀o1,o2:A.∀f,g:arrows2 A o1 o2.F⎽⇒ f =_2 F⎽⇒ g → f =_2 g. + +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}. + +notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}. +notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}. + +notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}. +notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}. diff --git a/helm/software/matita/library/formal_topology/o-algebra.ma b/helm/software/matita/library/formal_topology/o-algebra.ma index 67ff5140e..fb508aa92 100644 --- a/helm/software/matita/library/formal_topology/o-algebra.ma +++ b/helm/software/matita/library/formal_topology/o-algebra.ma @@ -241,21 +241,12 @@ intros; apply (or_f ?? c); qed. 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}. - -notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}. -notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}. - -notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}. -notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}. - interpretation "o-relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (or_f_minus_star ? ?) r). interpretation "o-relation f⎻" 'OR_f_minus r = (fun12 ?? (or_f_minus ? ?) r). interpretation "o-relation f*" 'OR_f_star r = (fun12 ?? (or_f_star ? ?) r). definition or_prop1 : ∀P,Q:OAlgebra.∀F:ORelation_setoid P Q.∀p,q. - (F p ≤ q) = (p ≤ F* q). + (F p ≤ q) =_1 (p ≤ F* q). intros; apply (or_prop1_ ?? F p q); qed. diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma index 4b6c63635..1503fa5de 100644 --- a/helm/software/matita/library/formal_topology/relations.ma +++ b/helm/software/matita/library/formal_topology/relations.ma @@ -193,86 +193,107 @@ qed. *) (* the same as ⋄ for a basic pair *) -definition image: ∀U,V:REL. (U ⇒_\r1 V) × Ω^U ⇒_1 Ω^V. +definition image: ∀U,V:REL. (U ⇒_\r1 V) ⇒_2 (Ω^U ⇒_2 Ω^V). intros; constructor 1; - [ apply (λr:U ⇒_\r1 V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S }); - intros; simplify; split; intro; cases e1; exists [1,3: apply w] + [ intro r; constructor 1; + [ apply (λS: Ω^U. {y | ∃x:U. x ♮r y ∧ x ∈ S }); + intros; simplify; split; intro; cases e1; exists [1,3: apply w] [ apply (. (#‡e^-1)‡#); assumption | apply (. (#‡e)‡#); assumption] - | intros; split; simplify; intros; cases e2; exists [1,3: apply w] - [ apply (. #‡(#‡e1^-1)); cases x; split; try assumption; - apply (if ?? (e ??)); assumption - | apply (. #‡(#‡e1)); cases x; split; try assumption; - apply (if ?? (e ^ -1 ??)); assumption]] + | intros; split; + [ intro y; simplify; intro yA; cases yA; exists; [ apply w ]; + apply (. #‡(#‡e^-1)); assumption; + | intro y; simplify; intro yA; cases yA; exists; [ apply w ]; + apply (. #‡(#‡e)); assumption;]] + | simplify; intros; intro y; simplify; split; simplify; intros (b H); cases H; + exists; [1,3: apply w]; cases x; split; try assumption; + [ apply (if ?? (e ??)); | apply (fi ?? (e ??)); ] assumption;] qed. (* the same as □ for a basic pair *) -definition minus_star_image: ∀U,V:REL. (U ⇒_\r1 V) × Ω^U ⇒_1 Ω^V. - intros; constructor 1; - [ apply (λr:U ⇒_\r1 V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S}); - intros; simplify; split; intros; apply f; - [ apply (. #‡e); assumption - | apply (. #‡e ^ -1); assumption] - | intros; split; simplify; intros; [ apply (. #‡e1^ -1); | apply (. #‡e1 )] - apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption] +definition minus_star_image: ∀U,V:REL. (U ⇒_\r1 V) ⇒_2 (Ω^U ⇒_2 Ω^V). + intros; constructor 1; intros; + [ constructor 1; + [ apply (λS: Ω^U. {y | ∀x:U. x ♮c y → x ∈ S}); + intros; simplify; split; intros; apply f; + [ apply (. #‡e); | apply (. #‡e ^ -1)] assumption; + | intros; split; intro; simplify; intros; + [ apply (. #‡e^-1);| apply (. #‡e); ] apply f; assumption;] + | intros; intro; simplify; split; simplify; intros; apply f; + [ apply (. (e x a2)); assumption | apply (. (e^-1 x a2)); assumption]] qed. (* the same as Rest for a basic pair *) -definition star_image: ∀U,V:REL. (U ⇒_\r1 V) × Ω^V ⇒_1 Ω^U. +definition star_image: ∀U,V:REL. (U ⇒_\r1 V) ⇒_2 (Ω^V ⇒_2 Ω^U). intros; constructor 1; - [ apply (λr:U ⇒_\r1 V.λS: Ω \sup V. {x | ∀y:V. x ♮r y → y ∈ S}); - intros; simplify; split; intros; apply f; - [ apply (. e ‡#); assumption - | apply (. e^ -1‡#); assumption] - | intros; split; simplify; intros; [ apply (. #‡e1 ^ -1); | apply (. #‡e1)] - apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption] + [ intro r; constructor 1; + [ apply (λS: Ω \sup V. {x | ∀y:V. x ♮r y → y ∈ S}); + intros; simplify; split; intros; apply f; + [ apply (. e ‡#);| apply (. e^ -1‡#);] assumption; + | intros; split; simplify; intros; + [ apply (. #‡e^-1);| apply (. #‡e); ] apply f; assumption;] + | intros; intro; simplify; split; simplify; intros; apply f; + [ apply (. e a2 y); | apply (. e^-1 a2 y)] assumption;] qed. (* the same as Ext for a basic pair *) -definition minus_image: ∀U,V:REL. (U ⇒_\r1 V) × Ω^V ⇒_1 Ω^U. +definition minus_image: ∀U,V:REL. (U ⇒_\r1 V) ⇒_2 (Ω^V ⇒_2 Ω^U). intros; constructor 1; - [ apply (λr:U ⇒_\r1 V.λS: Ω \sup V. {x | (*∃x:U. x ♮r y ∧ x ∈ S*) - exT ? (λy:V.x ♮r y ∧ y ∈ S) }); - intros; simplify; split; intro; cases e1; exists [1,3: apply w] - [ apply (. (e ^ -1‡#)‡#); assumption - | apply (. (e‡#)‡#); assumption] - | intros; split; simplify; intros; cases e2; exists [1,3: apply w] - [ apply (. #‡(#‡e1 ^ -1)); cases x; split; try assumption; - apply (if ?? (e ??)); assumption - | apply (. #‡(#‡e1)); cases x; split; try assumption; - apply (if ?? (e ^ -1 ??)); assumption]] + [ intro r; constructor 1; + [ apply (λS: Ω^V. {x | ∃y:V. x ♮r y ∧ y ∈ S }). + intros; simplify; split; intros; cases e1; cases x; exists; [1,3: apply w] + split; try assumption; [ apply (. (e^-1‡#)); | apply (. (e‡#));] assumption; + | intros; simplify; split; simplify; intros; cases e1; cases x; + exists [1,3: apply w] split; try assumption; + [ apply (. (#‡e^-1)); | apply (. (#‡e));] assumption] + | intros; intro; simplify; split; simplify; intros; cases e1; exists [1,3: apply w] + cases x; split; try assumption; + [ 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 image_coercion: ∀U,V:REL. (U ⇒_\r1 V) → Ω^U ⇒_2 Ω^V. +intros (U V r Us); apply (image U V r); qed. +coercion image_coercion. + (* minus_image is the same as ext *) -theorem image_id: ∀o,U. image o o (id1 REL o) U = U. - intros; unfold image; simplify; split; simplify; intros; +theorem image_id: ∀o. (id1 REL o : carr2 (Ω^o ⇒_2 Ω^o)) =_1 (id2 SET1 Ω^o). + intros; unfold image_coercion; unfold image; simplify; + whd in match (?:carr2 ?); + intro U; simplify; split; simplify; intros; [ change with (a ∈ U); - cases e; cases x; change in f with (eq1 ? w a); apply (. f^-1‡#); assumption + cases e; cases x; change in e1 with (w =_1 a); apply (. e1^-1‡#); assumption | change in f with (a ∈ U); exists; [apply a] split; [ change with (a = a); apply refl1 | assumption]] qed. -theorem minus_star_image_id: ∀o,U. minus_star_image o o (id1 REL o) U = U. - intros; unfold minus_star_image; simplify; split; simplify; intros; +theorem minus_star_image_id: ∀o:REL. (fun12 ?? (minus_star_image o o) (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 | change in f1 with (eq1 ? x a); apply (. f1‡#); apply f] qed. -alias symbol "compose" (instance 2) = "category1 composition". -theorem image_comp: ∀A,B,C,r,s,X. image A C (r ∘ s) X = image B C r (image A B s X). - intros; unfold image; simplify; split; simplify; intros; cases e; clear e; cases x; - clear x; [ cases f; clear f; | cases f1; clear f1 ] - exists; try assumption; cases x; clear x; split; try assumption; - exists; try assumption; split; assumption. +alias symbol "compose" (instance 5) = "category2 composition". +alias symbol "compose" (instance 4) = "category1 composition". +theorem image_comp: ∀A,B,C.∀r:B ⇒_\r1 C.∀s:A ⇒_\r1 B. + ((r ∘ s) : carr2 (Ω^A ⇒_2 Ω^C)) =_1 r ∘ s. + intros; intro U; split; intro x; (unfold image; unfold SET1; simplify); + intro H; cases H; + cases x1; [cases f|cases f1]; exists; [1,3: apply w1] cases x2; split; try assumption; + exists; try assumption; split; assumption; qed. theorem minus_star_image_comp: - ∀A,B,C,r,s,X. - minus_star_image A C (r ∘ s) X = minus_star_image B C r (minus_star_image A B s X). - intros; unfold minus_star_image; simplify; split; simplify; intros; whd; intros; - [ apply f; exists; try assumption; split; assumption - | change with (x ∈ X); cases f1; cases x1; apply f; assumption] + ∀A,B,C.∀r:B ⇒_\r1 C.∀s:A ⇒_\r1 B. + minus_star_image A C (r ∘ s) =_1 minus_star_image B C r ∘ (minus_star_image A B s). + intros; unfold minus_star_image; intro X; simplify; split; simplify; intros; + [ whd; intros; simplify; whd; intros; apply f; exists; try assumption; split; assumption; + | cases f1; cases x1; apply f; assumption] qed. (* 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 93bf2c609..01c06f020 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,39 +51,25 @@ 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; - [ constructor 1; - [ apply (λU.image ?? c U); - | intros; apply (#‡e); ] - | constructor 1; - [ apply (λU.minus_star_image ?? c U); - | intros; apply (#‡e); ] - | constructor 1; - [ apply (λU.star_image ?? c U); - | intros; apply (#‡e); ] - | constructor 1; - [ apply (λU.minus_image ?? c U); - | intros; apply (#‡e); ] - | intros; split; intro; - [ 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 ?? c q); - change with (∀a. a ∈ image ?? c p → a ∈ q); - intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ] + [ apply rule c; + | apply rule ((foo ?? c)⎻* ); + | apply rule ((foo ?? c)* ); + | apply rule ((foo ?? c)⎻); | intros; split; intro; - [ 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 ?? 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; + [ 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; + apply (f w f3); assumption; ] + | unfold foo; intros; split; intro; + [ intros 2; intros 2; apply (f x); exists [apply a] split; assumption; + | intros 2; change with (a ∈ q); cases f1; cases x; apply (f w f3); assumption;] + | intros; split; unfold foo; unfold image_coercion; simplify; intro; cases f; clear f; [ cases x; cases x2; clear x x2; exists; [apply w1] - [ assumption; - | exists; [apply w] split; assumption] + [ assumption | exists; [apply w] split; assumption] | cases x1; cases x2; clear x1 x2; exists; [apply w1] [ exists; [apply w] split; assumption; | assumption; ]]] @@ -92,29 +78,36 @@ qed. lemma orelation_of_relation_preserves_equality: ∀o1,o2:REL.∀t,t': o1 ⇒_\r1 o2. t = t' → orelation_of_relation ?? t =_2 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); - apply (. #‡(e^-1‡#)); - | change with (a1 ∈ minus_star_image ?? t' a → a1 ∈ minus_star_image ?? t a); - apply (. #‡(e‡#)); - | change with (a1 ∈ minus_image ?? t a → a1 ∈ minus_image ?? t' a); - apply (. #‡(e ^ -1‡#)); - | change with (a1 ∈ minus_image ?? t' a → a1 ∈ minus_image ?? t a); - apply (. #‡(e‡#)); - | change with (a1 ∈ image ?? t a → a1 ∈ image ?? t' a); - apply (. #‡(e ^ -1‡#)); - | change with (a1 ∈ image ?? t' a → a1 ∈ image ?? t a); - apply (. #‡(e‡#)); - | change with (a1 ∈ star_image ?? t a → a1 ∈ star_image ?? t' a); - apply (. #‡(e ^ -1‡#)); - | change with (a1 ∈ star_image ?? t' a → a1 ∈ star_image ?? t a); - apply (. #‡(e‡#)); ] + intros; split; unfold orelation_of_relation; unfold foo; simplify; + 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). +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; +| change in f with (a1 ∈ a); exists [ apply a1] split; try assumption; + change with (a1 =_1 a1); apply refl1;] +qed. + +lemma star_image_id : ∀o:REL. (foo ?? (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;] +qed. + lemma orelation_of_relation_preserves_identity: ∀o1:REL. orelation_of_relation ?? (id1 ? o1) =_2 id2 OA (POW' o1). - intros; split; intro; split; whd; intro; + intros; split; + (unfold orelation_of_relation; unfold OA; unfold foo; simplify); + [ apply (minus_star_image_id o1); + | apply (minus_image_id o1); + | apply (image_id o1); + | apply (star_image_id o1) ] +qed. + +(* + 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; | change with (a1 ∈ a → ∀x. x ♮(id1 REL o1) a1→x∈a); intros; @@ -135,6 +128,7 @@ 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. +*) (* CSC: ???? forse un uncertain mancato *) alias symbol "eq" = "setoid2 eq". @@ -173,38 +167,43 @@ qed. theorem POW_faithful: faithful2 ?? POW. intros 5; unfold POW in e; simplify in e; cases e; unfold orelation_of_relation in e3; simplify in e3; clear e e1 e2 e4; - intros 2; cases (e3 {(x)}); + intros 2; simplify; unfold image_coercion in e3; cases (e3 {(x)}); 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 Hletin; cases x1; change in f3 with (x =_1 w); apply (. f3‡#); assumption;] qed. + (* lemma currify: ∀A,B,C. (A × B ⇒_1 C) → A → (B ⇒_1 C). intros; constructor 1; [ apply (b c); | intros; apply (#‡e);] qed. *) +include "formal_topology/notation.ma". + theorem POW_full: full2 ?? POW. intros 3 (S T); exists; [ constructor 1; constructor 1; [ apply (λx:carr S.λy:carr T. y ∈ f {(x)}); - | intros; unfold FunClass_1_OF_carr2; lapply (.= e1‡#); + | apply hide; intros; unfold FunClass_1_OF_carr2; lapply (.= e1‡#); [4: apply mem; |6: apply Hletin;|1,2,3,5: skip] lapply (#‡prop11 ?? f ?? (†e)); [6: apply Hletin; |*:skip ]] - | whd; split; whd; intro; simplify; unfold map_arrows2; simplify; - [ split; + | (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)); ] - | split; - [ change with (∀a1.(∃y:carr T. y ∈ f {(a1):S} ∧ y ∈ a) → a1 ∈ f⎻ a); - | change with (∀a1.a1 ∈ f⎻ a → (∃y:carr T.y ∈ f {(a1):S} ∧ y ∈ a)); ] - | split; - [ change with (∀a1.(∃x:carr S. a1 ∈ f {(x):S} ∧ x ∈ a) → a1 ∈ f a); - | change with (∀a1.a1 ∈. f a → (∃x:carr S. a1 ∈ f {(x):S} ∧ x ∈ a)); ] - | split; - [ change with (∀a1.(∀y. y ∈ f {(a1):S} → y ∈ a) → a1 ∈ f* a); - | change with (∀a1.a1 ∈ f* a → (∀y. y ∈ f {(a1):S} → y ∈ a)); ]] + | change with (∀a1.a1 ∈ f⎻* a → (∀x.a1 ∈ f {(x):S} → x ∈ a)); + | alias symbol "and" (instance 4) = "and_morphism". +change with (∀a1.(∃y:carr T. y ∈ f {(a1):S} ∧ y ∈ a) → a1 ∈ f⎻ a); + | alias symbol "and" (instance 2) = "and_morphism". +change with (∀a1.a1 ∈ f⎻ a → (∃y:carr T.y ∈ f {(a1):S} ∧ y ∈ a)); + | alias symbol "and" (instance 3) = "and_morphism". +change with (∀a1.(∃x:carr S. a1 ∈ f {(x):S} ∧ x ∈ a) → a1 ∈ f a); + | change with (∀a1.a1 ∈. f a → (∃x:carr S. a1 ∈ f {(x):S} ∧ x ∈ a)); + | change with (∀a1.(∀y. y ∈ f {(a1):S} → y ∈ a) → a1 ∈ f* a); + | change with (∀a1.a1 ∈ f* a → (∀y. y ∈ f {(a1):S} → y ∈ a)); ] [ intros; apply ((. (or_prop2 ?? f (singleton ? a1) a)^-1) ? a1); [ intros 2; apply (f1 a2); change in f2 with (a2 ∈ f⎻ (singleton ? a1)); lapply (. (or_prop3 ?? f (singleton ? a2) (singleton ? a1))); diff --git a/helm/software/matita/library/formal_topology/subsets.ma b/helm/software/matita/library/formal_topology/subsets.ma index 108e3c767..254f924dd 100644 --- a/helm/software/matita/library/formal_topology/subsets.ma +++ b/helm/software/matita/library/formal_topology/subsets.ma @@ -131,7 +131,7 @@ definition singleton: ∀A:setoid. A ⇒_1 Ω^A. intros; simplify; split; intro; apply (.= e1); - [ apply e | apply (e \sup -1) ] + [ apply e | apply (e^-1) ] | unfold setoid1_of_setoid; simplify; intros; split; intros 2; simplify in f ⊢ %; apply trans; [ apply a |4: apply a'] try assumption; apply sym; assumption] -- 2.39.2