From c96d1f2066d37b84a34412f7c49fb3e4f54bd9a2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Sep 2008 11:29:35 +0000 Subject: [PATCH] Major reordering of theorems in the appropriate files. --- .../matita/library/datatypes/subsets.ma | 10 +- .../formal_topology/basic_topologies.ma | 166 +++--------------- .../formal_topology/formal_topologies.ma | 20 ++- .../library/formal_topology/relations.ma | 79 +++++++++ .../formal_topology/saturations_reductions.ma | 40 +++++ 5 files changed, 172 insertions(+), 143 deletions(-) create mode 100644 helm/software/matita/library/formal_topology/saturations_reductions.ma diff --git a/helm/software/matita/library/datatypes/subsets.ma b/helm/software/matita/library/datatypes/subsets.ma index d6bcf4dda..7c9a13195 100644 --- a/helm/software/matita/library/datatypes/subsets.ma +++ b/helm/software/matita/library/datatypes/subsets.ma @@ -74,6 +74,14 @@ qed. interpretation "subseteq" 'subseteq U V = (fun1 ___ (subseteq _) U V). +theorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S. + intros 4; assumption. +qed. + +theorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3. + intros; apply transitive_subseteq_operator; [apply S2] assumption. +qed. + definition overlaps: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP. intros; constructor 1; @@ -127,4 +135,4 @@ definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A). [ apply a |4: apply a'] try assumption; apply sym; assumption] qed. -interpretation "singleton" 'singl a = (fun_1 __ (singleton _) a). \ No newline at end of file +interpretation "singleton" 'singl a = (fun_1 __ (singleton _) a). diff --git a/helm/software/matita/library/formal_topology/basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies.ma index 92f4cdf46..36a0d24c8 100644 --- a/helm/software/matita/library/formal_topology/basic_topologies.ma +++ b/helm/software/matita/library/formal_topology/basic_topologies.ma @@ -14,39 +14,7 @@ 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). - -theorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S. - intros 4; assumption. -qed. - -theorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3. - intros; apply transitive_subseteq_operator; [apply S2] assumption. -qed. - -theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ⊆ A U. - intros; apply (fi ?? (H ??)); apply subseteq_refl. -qed. - -theorem saturation_monotone: - ∀C,A. is_saturation C A → - ∀U,V. U ⊆ V → A U ⊆ A V. - intros; apply (if ?? (H ??)); apply subseteq_trans; [apply V|3: apply saturation_expansive ] - assumption. -qed. - -theorem saturation_idempotent: ∀C,A. is_saturation C A → ∀U. A (A U) = A U. - intros; split; - [ apply (if ?? (H ??)); apply subseteq_refl - | apply saturation_expansive; assumption] -qed. +include "formal_topology/saturations_reductions.ma". record basic_topology: Type ≝ { carrbt:> REL; @@ -57,62 +25,6 @@ record basic_topology: Type ≝ 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); @@ -137,46 +49,6 @@ definition cont_rel'': ∀S,T: basic_topology. continuous_relation_setoid S T coercion cont_rel''. -theorem ext_comp: - ∀o1,o2,o3: REL. - ∀a: arrows1 ? o1 o2. - ∀b: arrows1 ? o2 o3. - ∀x. ext ?? (b∘a) x = extS ?? a (ext ?? b x). - intros; - unfold ext; unfold extS; simplify; split; intro; simplify; intros; - cases f; clear f; split; try assumption; - [ cases f2; clear f2; cases x1; clear x1; exists; [apply w] split; - [1: split] assumption; - | cases H; clear H; cases x1; clear x1; exists [apply w]; split; - [2: cases f] assumption] -qed. - -(* -(* this proof is more logic-oriented than set/lattice oriented *) -theorem continuous_relation_eqS: - ∀o1,o2:basic_topology.∀a,a': continuous_relation_setoid o1 o2. - a = a' → ∀X. A ? (extS ?? a X) = A ? (extS ?? a' X). - intros; - cut (∀a: arrows1 ? o1 ?.∀x. x ∈ extS ?? a X → ∃y:o2.y ∈ X ∧ x ∈ ext ?? a y); - [2: intros; cases f; clear f; cases H1; exists [apply w] cases x1; split; - try assumption; split; assumption] - cut (∀a,a':continuous_relation_setoid o1 o2.eq1 ? a a' → ∀x. x ∈ extS ?? a X → ∃y:o2. y ∈ X ∧ x ∈ A ? (ext ?? a' y)); - [2: intros; cases (Hcut ?? f); exists; [apply w] cases x1; split; try assumption; - apply (. #‡(H1 ?)); - apply (saturation_expansive ?? (A_is_saturation o1) (ext ?? a1 w) x); - assumption;] clear Hcut; - split; apply (if ?? (A_is_saturation ???)); intros 2; - [lapply (Hcut1 a a' H a1 f) | lapply (Hcut1 a' a (H \sup -1) a1 f)] - cases Hletin; clear Hletin; cases x; clear x; - cut (∀a: arrows1 ? o1 ?. ext ?? a w ⊆ extS ?? a X); - [2,4: intros 3; cases f3; clear f3; simplify in f5; split; try assumption; - exists [1,3: apply w] split; assumption;] - cut (∀a. A ? (ext o1 o2 a w) ⊆ A ? (extS o1 o2 a X)); - [2,4: intros; apply saturation_monotone; try (apply A_is_saturation); apply Hcut;] - apply Hcut2; assumption. -qed. -*) - 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). @@ -195,15 +67,6 @@ theorem continuous_relation_eq': [ apply I | assumption ]] qed. -theorem extS_singleton: - ∀o1,o2.∀a:arrows1 ? o1 o2.∀x.extS o1 o2 a (singleton o2 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. - theorem 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'. @@ -308,4 +171,29 @@ definition BTop: category1. | intros; simplify; intro; simplify; apply (.= †((id_neutral_left1 ????)‡#)); apply refl1] -qed. \ No newline at end of file +qed. + +(*CSC: unused! *) +(* this proof is more logic-oriented than set/lattice oriented *) +theorem continuous_relation_eqS: + ∀o1,o2:basic_topology.∀a,a': continuous_relation_setoid o1 o2. + a = a' → ∀X. A ? (extS ?? a X) = A ? (extS ?? a' X). + intros; + cut (∀a: arrows1 ? o1 ?.∀x. x ∈ extS ?? a X → ∃y:o2.y ∈ X ∧ x ∈ ext ?? a y); + [2: intros; cases f; clear f; cases H1; exists [apply w] cases x1; split; + try assumption; split; assumption] + cut (∀a,a':continuous_relation_setoid o1 o2.eq1 ? a a' → ∀x. x ∈ extS ?? a X → ∃y:o2. y ∈ X ∧ x ∈ A ? (ext ?? a' y)); + [2: intros; cases (Hcut ?? f); exists; [apply w] cases x1; split; try assumption; + apply (. #‡(H1 ?)); + apply (saturation_expansive ?? (A_is_saturation o1) (ext ?? a1 w) x); + assumption;] clear Hcut; + split; apply (if ?? (A_is_saturation ???)); intros 2; + [lapply (Hcut1 a a' H a1 f) | lapply (Hcut1 a' a (H \sup -1) a1 f)] + cases Hletin; clear Hletin; cases x; clear x; + cut (∀a: arrows1 ? o1 ?. ext ?? a w ⊆ extS ?? a X); + [2,4: intros 3; cases f3; clear f3; simplify in f5; split; try assumption; + exists [1,3: apply w] split; assumption;] + cut (∀a. A ? (ext o1 o2 a w) ⊆ A ? (extS o1 o2 a X)); + [2,4: intros; apply saturation_monotone; try (apply A_is_saturation); apply Hcut;] + apply Hcut2; assumption. +qed. diff --git a/helm/software/matita/library/formal_topology/formal_topologies.ma b/helm/software/matita/library/formal_topology/formal_topologies.ma index 62b11676a..ba2d65ba0 100644 --- a/helm/software/matita/library/formal_topology/formal_topologies.ma +++ b/helm/software/matita/library/formal_topology/formal_topologies.ma @@ -60,10 +60,15 @@ interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U record formal_map (S,T: formal_topology) : Type ≝ { cr:> continuous_relation_setoid S T; - C1: ∀b,c. extS ?? cr (b ↓ c) = (ext ?? cr b) ↓ (ext ?? cr c); + C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c; 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); @@ -74,12 +79,18 @@ 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 ≝ +definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝ λFT1,FT2,c.cr ?? c. -coercion cr'. +coercion cr''. (* +theorem 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. + intros; +qed. + definition formal_map_composition: ∀o1,o2,o3: formal_topology. binary_morphism1 @@ -90,4 +101,7 @@ definition formal_map_composition: [ intros; whd in c c1; constructor 1; [ apply (comp1 BTop ??? c c1); | intros; + apply (.= (extS_com ??? c c1 ?)); + apply (.= †(C1 ?????)); + apply (.= (C1 ?????)); *) \ No newline at end of file diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma index 5e2274047..f81e19eec 100644 --- a/helm/software/matita/library/formal_topology/relations.ma +++ b/helm/software/matita/library/formal_topology/relations.ma @@ -166,3 +166,82 @@ lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c2 ∘ c1) S = extS o1 o2 c1 (e assumption] qed. +(* 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. + +(*CSC: unused! *) +theorem ext_comp: + ∀o1,o2,o3: REL. + ∀a: arrows1 ? o1 o2. + ∀b: arrows1 ? o2 o3. + ∀x. ext ?? (b∘a) x = extS ?? a (ext ?? b x). + intros; + unfold ext; unfold extS; simplify; split; intro; simplify; intros; + cases f; clear f; split; try assumption; + [ cases f2; clear f2; cases x1; clear x1; exists; [apply w] split; + [1: split] assumption; + | cases H; clear H; cases x1; clear x1; exists [apply w]; split; + [2: cases f] assumption] +qed. + +theorem extS_singleton: + ∀o1,o2.∀a:arrows1 ? o1 o2.∀x.extS o1 o2 a (singleton o2 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. \ No newline at end of file diff --git a/helm/software/matita/library/formal_topology/saturations_reductions.ma b/helm/software/matita/library/formal_topology/saturations_reductions.ma new file mode 100644 index 000000000..d87ea9e1f --- /dev/null +++ b/helm/software/matita/library/formal_topology/saturations_reductions.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "datatypes/subsets.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). + +theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ⊆ A U. + intros; apply (fi ?? (H ??)); apply subseteq_refl. +qed. + +theorem saturation_monotone: + ∀C,A. is_saturation C A → + ∀U,V. U ⊆ V → A U ⊆ A V. + intros; apply (if ?? (H ??)); apply subseteq_trans; [apply V|3: apply saturation_expansive ] + assumption. +qed. + +theorem saturation_idempotent: ∀C,A. is_saturation C A → ∀U. A (A U) = A U. + intros; split; + [ apply (if ?? (H ??)); apply subseteq_refl + | apply saturation_expansive; assumption] +qed. -- 2.39.2