From 1110bdf814f976ef0a36a024d2cba847ce06347e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 12 Sep 2008 15:22:31 +0000 Subject: [PATCH] 1) as usual, I took the reverse notation for composition. "fixed" according to the internatinal tradition 2) partial proof that basic_topologies form a category --- .../matita/library/datatypes/categories.ma | 8 +- .../library/formal_topology/basic_pairs.ma | 33 ++-- .../formal_topology/basic_topologies.ma | 151 ++++++++++++++++++ .../formal_topology/concrete_spaces.ma | 20 +-- .../library/formal_topology/relations.ma | 2 +- 5 files changed, 182 insertions(+), 32 deletions(-) create mode 100644 helm/software/matita/library/formal_topology/basic_topologies.ma diff --git a/helm/software/matita/library/datatypes/categories.ma b/helm/software/matita/library/datatypes/categories.ma index e90e1457d..692f977df 100644 --- a/helm/software/matita/library/datatypes/categories.ma +++ b/helm/software/matita/library/datatypes/categories.ma @@ -192,14 +192,14 @@ record category1 : Type ≝ comp1: ∀o1,o2,o3. binary_morphism1 (arrows1 o1 o2) (arrows1 o2 o3) (arrows1 o1 o3); comp_assoc1: ∀o1,o2,o3,o4. ∀a12,a23,a34. comp1 o1 o3 o4 (comp1 o1 o2 o3 a12 a23) a34 = comp1 o1 o2 o4 a12 (comp1 o2 o3 o4 a23 a34); - id_neutral_left1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? (id1 o1) a = a; - id_neutral_right1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? a (id1 o2) = a + id_neutral_right1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? (id1 o1) a = a; + id_neutral_left1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? a (id1 o2) = a }. notation "'ASSOC'" with precedence 90 for @{'assoc}. notation "'ASSOC1'" with precedence 90 for @{'assoc1}. -interpretation "category1 composition" 'compose x y = (fun1 ___ (comp1 ____) x y). +interpretation "category1 composition" 'compose x y = (fun1 ___ (comp1 ____) y x). interpretation "category1 assoc" 'assoc1 = (comp_assoc1 ________). -interpretation "category composition" 'compose x y = (fun ___ (comp ____) x y). +interpretation "category composition" 'compose x y = (fun ___ (comp ____) y x). interpretation "category assoc" 'assoc = (comp_assoc ________). diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma index f19e39d2a..475445720 100644 --- a/helm/software/matita/library/formal_topology/basic_pairs.ma +++ b/helm/software/matita/library/formal_topology/basic_pairs.ma @@ -30,7 +30,7 @@ interpretation "basic pair relation (non applied)" 'Vdash = (rel _). record relation_pair (BP1,BP2: basic_pair): Type ≝ { concr_rel: arrows1 ? (concr BP1) (concr BP2); form_rel: arrows1 ? (form BP1) (form BP2); - commute: concr_rel ∘ ⊩ = ⊩ ∘ form_rel + commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩ }. notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}. @@ -43,7 +43,7 @@ definition relation_pair_equality: ∀o1,o2. equivalence_relation1 (relation_pair o1 o2). intros; constructor 1; - [ apply (λr,r'. r \sub\c ∘ ⊩ = r' \sub\c ∘ ⊩); + [ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c); | simplify; intros; apply refl1; @@ -64,7 +64,7 @@ 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' → ⊩ \circ r \sub\f = ⊩ \circ r'\sub\f. +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; @@ -80,8 +80,8 @@ definition id_relation_pair: ∀o:basic_pair. relation_pair o o. intro; constructor 1; [1,2: apply id1; - | lapply (id_neutral_left1 ? (concr o) ? (⊩)) as H; - lapply (id_neutral_right1 ?? (form o) (⊩)) as H1; + | lapply (id_neutral_right1 ? (concr o) ? (⊩)) as H; + lapply (id_neutral_left1 ?? (form o) (⊩)) as H1; apply (.= H); apply (H1 \sup -1);] qed. @@ -92,8 +92,8 @@ definition relation_pair_composition: constructor 1; [ intros (r r1); constructor 1; - [ apply (r \sub\c ∘ r1 \sub\c) - | apply (r \sub\f ∘ r1 \sub\f) + [ apply (r1 \sub\c ∘ r \sub\c) + | apply (r1 \sub\f ∘ r \sub\f) | lapply (commute ?? r) as H; lapply (commute ?? r1) as H1; apply (.= ASSOC1); @@ -102,9 +102,9 @@ definition relation_pair_composition: apply (.= H‡#); apply ASSOC1] | intros; - change with (a\sub\c ∘ b\sub\c ∘ ⊩ = a'\sub\c ∘ b'\sub\c ∘ ⊩); - change in H with (a \sub\c ∘ ⊩ = a' \sub\c ∘ ⊩); - change in H1 with (b \sub\c ∘ ⊩ = b' \sub\c ∘ ⊩); + change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c)); + change in H with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c); + change in H1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c); apply (.= ASSOC1); apply (.= #‡H1); apply (.= #‡(commute ?? b')); @@ -122,16 +122,15 @@ definition BP: category1. | apply id_relation_pair | apply relation_pair_composition | intros; - change with (a12\sub\c ∘ a23\sub\c ∘ a34\sub\c ∘ ⊩ = - (a12\sub\c ∘ (a23\sub\c ∘ a34\sub\c) ∘ ⊩)); + change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) = + ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c)); apply (ASSOC1‡#); | intros; - change with ((id_relation_pair o1)\sub\c ∘ a\sub\c ∘ ⊩ = a\sub\c ∘ ⊩); - apply ((id_neutral_left1 ????)‡#); - | intros; - change with (a\sub\c ∘ (id_relation_pair o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩); + change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c); apply ((id_neutral_right1 ????)‡#); - ] + | intros; + change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c); + apply ((id_neutral_left1 ????)‡#);] qed. definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o). diff --git a/helm/software/matita/library/formal_topology/basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies.ma new file mode 100644 index 000000000..b961e1e6b --- /dev/null +++ b/helm/software/matita/library/formal_topology/basic_topologies.ma @@ -0,0 +1,151 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "formal_topology/relations.ma". +include "datatypes/categories.ma". + +definition is_saturation ≝ + λC:REL.λA:unary_morphism (Ω \sup C) (Ω \sup C). + ∀U,V. (U ⊆ A V) = (A U ⊆ A V). + +definition is_reduction ≝ + λC:REL.λJ:unary_morphism (Ω \sup C) (Ω \sup C). + ∀U,V. (J U ⊆ V) = (J U ⊆ J V). + +record basic_topology: Type ≝ + { carrbt:> REL; + A: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt); + J: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt); + A_is_saturation: is_saturation ? A; + J_is_reduction: is_reduction ? J; + compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V) + }. + +(* the same as ⋄ for a basic pair *) +definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V). + intros; constructor 1; + [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S}); + intros; simplify; split; intro; cases H1; exists [1,3: apply w] + [ apply (. (#‡H)‡#); assumption + | apply (. (#‡H \sup -1)‡#); assumption] + | intros; split; simplify; intros; cases H2; exists [1,3: apply w] + [ apply (. #‡(#‡H1)); cases x; split; try assumption; + apply (if ?? (H ??)); assumption + | apply (. #‡(#‡H1 \sup -1)); cases x; split; try assumption; + apply (if ?? (H \sup -1 ??)); assumption]] +qed. + +(* the same as □ for a basic pair *) +definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V). + intros; constructor 1; + [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S}); + intros; simplify; split; intros; apply H1; + [ apply (. #‡H \sup -1); assumption + | apply (. #‡H); assumption] + | intros; split; simplify; intros; [ apply (. #‡H1); | apply (. #‡H1 \sup -1)] + apply H2; [ apply (if ?? (H \sup -1 ??)); | apply (if ?? (H ??)) ] assumption] +qed. + +(* 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; + [ change with (a ∈ U); + cases H; cases x; change in f with (eq1 ? w a); apply (. f‡#); assumption + | change in f with (a ∈ U); + exists; [apply a] split; [ change with (a = a); apply refl | 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; + [ change with (a ∈ U); apply H; change with (a=a); apply refl + | change in f1 with (eq1 ? x a); apply (. f1 \sup -1‡#); apply f] +qed. + +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 H; clear H; 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. +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 H; exists; try assumption; split; assumption + | change with (x ∈ X); cases f; cases x1; apply H; assumption] +qed. + +record continuous_relation (S,T: basic_topology) : Type ≝ + { 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) + }. + +definition continuous_relation_setoid: basic_topology → basic_topology → setoid1. + intros (S T); constructor 1; + [ apply (continuous_relation S T) + | constructor 1; + [ apply (λr,s:continuous_relation S T.∀b. A ? (ext ?? r b) = A ? (ext ?? s b)); + | simplify; intros; apply refl1; + | simplify; intros; apply sym1; apply H + | 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 BTop: category1. + constructor 1; + [ apply basic_topology + | apply continuous_relation_setoid + | intro; constructor 1; + [ apply id1 + | intros; + apply (.= (image_id ??)); + apply sym1; + apply (.= †(image_id ??)); + apply sym1; + assumption + | intros; + apply (.= (minus_star_image_id ??)); + apply sym1; + apply (.= †(minus_star_image_id ??)); + apply sym1; + assumption] + | intros; constructor 1; + [ intros (r s); constructor 1; + [ apply (s ∘ r) + | intros; + apply sym1; + apply (.= †(image_comp ??????)); + apply (.= (reduced ?????)\sup -1); + [ apply (.= (reduced ?????)); [ assumption | apply refl1 ] + | apply (.= (image_comp ??????)\sup -1); + apply refl1] + | intros; + apply sym1; + apply (.= †(minus_star_image_comp ??????)); + apply (.= (saturated ?????)\sup -1); + [ apply (.= (saturated ?????)); [ assumption | apply refl1 ] + | apply (.= (minus_star_image_comp ??????)\sup -1); + apply refl1]]] + | intros; simplify; intro; simplify; + | intros; simplify; intro; simplify; + | intros; simplify; intro; simplify; + ] +qed. +*) \ No newline at end of file diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma index d95072cb9..3c03b4e66 100644 --- a/helm/software/matita/library/formal_topology/concrete_spaces.ma +++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma @@ -67,23 +67,23 @@ definition convergent_relation_space_composition: constructor 1; [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption] | intros; - change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c); + change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c); change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?))) - with (c \sub \f ∘ c1 \sub \f); + with (c1 \sub \f ∘ c \sub \f); change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?)))) - with (c \sub \f ∘ c1 \sub \f); + with (c1 \sub \f ∘ c \sub \f); apply (.= (extS_com ??????)); apply (.= (†(respects_converges ?????))); apply (.= (respects_converges ?????)); apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1))); apply refl1; - | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c); + | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c); apply (.= (extS_com ??????)); apply (.= (†(respects_all_covered ???))); apply (.= respects_all_covered ???); apply refl1] | intros; - change with (a ∘ b = a' ∘ b'); + change with (b ∘ a = b' ∘ a'); change in H with (rp'' ?? a = rp'' ?? a'); change in H1 with (rp'' ?? b = rp ?? b'); apply (.= (H‡H1)); @@ -106,15 +106,15 @@ definition CSPA: category1. apply refl1] | apply convergent_relation_space_composition | intros; simplify; - change with ((a12 ∘ a23) ∘ a34 = a12 ∘ (a23 ∘ a34)); + change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12); apply (.= ASSOC1); apply refl1 | intros; simplify; - change with (id1 ? o1 ∘ a = a); - apply (.= id_neutral_left1 ????); + change with (a ∘ id1 ? o1 = a); + apply (.= id_neutral_right1 ????); apply refl1 | intros; simplify; - change with (a ∘ id1 ? o2 = a); - apply (.= id_neutral_right1 ????); + change with (id1 ? o2 ∘ a = a); + apply (.= id_neutral_left1 ????); apply refl1] qed. diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma index 72e12aa9d..1ab9ec3f1 100644 --- a/helm/software/matita/library/formal_topology/relations.ma +++ b/helm/software/matita/library/formal_topology/relations.ma @@ -154,7 +154,7 @@ lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X. | change with (a = a); apply refl]]] qed. -lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c1 ∘ c2) S = extS o1 o2 c1 (extS o2 o3 c2 S). +lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c2 ∘ c1) S = extS o1 o2 c1 (extS o2 o3 c2 S). intros; unfold extS; simplify; split; intros; simplify; intros; [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption] cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6; -- 2.39.2