From 2857d1c432f073379552e1572235a86509b665a4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Jan 2009 16:20:00 +0000 Subject: [PATCH] 1) Some reorganization. 2) Funny: the proof that basic_topologies are an example of o_basic_topology is immediate. --- .../formal_topology/overlap/basic_pairs.ma | 24 --- .../overlap/basic_pairs_to_o-basic_pairs.ma | 40 ++++ .../overlap/basic_topologies.ma | 3 +- .../basic_topologies_to_o-basic_topologies.ma | 39 ++++ .../contribs/formal_topology/overlap/depends | 10 +- .../formal_topology/overlap/relations.ma | 118 ------------ .../overlap/relations_to_o-algebra.ma | 173 ++++++++++++++++++ .../overlap/saturations_to_o-saturations.ma | 36 ++++ .../formal_topology/overlap/subsets.ma | 44 ----- 9 files changed, 297 insertions(+), 190 deletions(-) create mode 100644 helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma create mode 100644 helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma create mode 100644 helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma create mode 100644 helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma 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 058176f4c..97e386c15 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma @@ -185,27 +185,3 @@ qed. interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y). interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)). *) - -include "o-basic_pairs.ma". -(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) -definition o_basic_pair_of_basic_pair: cic:/matita/formal_topology/basic_pairs/basic_pair.ind#xpointer(1/1) → basic_pair. - intro; - constructor 1; - [ apply (SUBSETS (concr b)); - | apply (SUBSETS (form b)); - | apply (orelation_of_relation ?? (rel b)); ] -qed. - -definition o_relation_pair_of_relation_pair: - ∀BP1,BP2.cic:/matita/formal_topology/basic_pairs/relation_pair.ind#xpointer(1/1) BP1 BP2 → - relation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2). - intros; - constructor 1; - [ apply (orelation_of_relation ?? (r \sub \c)); - | apply (orelation_of_relation ?? (r \sub \f)); - | lapply (commute ?? r); - lapply (orelation_of_relation_preserves_equality ???? Hletin); - apply (.= (orelation_of_relation_preserves_composition (concr BP1) ??? (rel BP2)) ^ -1); - apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r))); - apply (orelation_of_relation_preserves_composition ?? (form BP2) (rel BP1) ?); ] -qed. \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma new file mode 100644 index 000000000..7fc6a07f4 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.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 "basic_pairs.ma". +include "o-basic_pairs.ma". +include "relations_to_o-algebra.ma". + +(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) +definition o_basic_pair_of_basic_pair: cic:/matita/formal_topology/basic_pairs/basic_pair.ind#xpointer(1/1) → basic_pair. + intro; + constructor 1; + [ apply (SUBSETS (concr b)); + | apply (SUBSETS (form b)); + | apply (orelation_of_relation ?? (rel b)); ] +qed. + +definition o_relation_pair_of_relation_pair: + ∀BP1,BP2.cic:/matita/formal_topology/basic_pairs/relation_pair.ind#xpointer(1/1) BP1 BP2 → + relation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2). + intros; + constructor 1; + [ apply (orelation_of_relation ?? (r \sub \c)); + | apply (orelation_of_relation ?? (r \sub \f)); + | lapply (commute ?? r); + lapply (orelation_of_relation_preserves_equality ???? Hletin); + apply (.= (orelation_of_relation_preserves_composition (concr BP1) ??? (rel BP2)) ^ -1); + apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r))); + apply (orelation_of_relation_preserves_composition ?? (form BP2) (rel BP1) ?); ] +qed. 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 26562cbb4..4b53407d1 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma @@ -34,7 +34,7 @@ record continuous_relation (S,T: basic_topology) : Type1 ≝ 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) @@ -202,4 +202,5 @@ theorem continuous_relation_eqS: [2,4: intros; apply saturation_monotone; try (apply A_is_saturation); apply Hcut;] apply Hcut2; assumption. qed. +*) *) \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma new file mode 100644 index 000000000..282519dc7 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_topologies.ma". +include "o-basic_topologies.ma". +include "relations_to_o-algebra.ma". + +(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) +definition o_basic_topology_of_basic_topology: cic:/matita/formal_topology/basic_topologies/basic_topology.ind#xpointer(1/1) → basic_topology. + intro; + constructor 1; + [ apply (SUBSETS (carrbt b)); + | apply (A b); + | apply (J b); + | apply (A_is_saturation b); + | apply (J_is_reduction b); + | apply (compatibility b); ] +qed. + +definition o_relation_pair_of_relation_pair: + ∀S,T.cic:/matita/formal_topology/basic_topologies/continuous_relation.ind#xpointer(1/1) S T → + continuous_relation (o_basic_topology_of_basic_topology S) (o_basic_topology_of_basic_topology T). + intros; + constructor 1; + [ apply (orelation_of_relation ?? (cont_rel ?? c)); + | apply (reduced ?? c); + | apply (saturated ?? c); ] +qed. \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends index bd6cd4d14..1295f994d 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/depends +++ b/helm/software/matita/contribs/formal_topology/overlap/depends @@ -1,14 +1,18 @@ o-basic_pairs.ma o-algebra.ma o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma o-saturations.ma o-algebra.ma -basic_pairs.ma o-basic_pairs.ma relations.ma +basic_pairs.ma relations.ma saturations.ma relations.ma o-algebra.ma categories.ma o-formal_topologies.ma o-basic_topologies.ma categories.ma cprop_connectives.ma -subsets.ma categories.ma o-algebra.ma +saturations_to_o-saturations.ma o-saturations.ma relations_to_o-algebra.ma saturations.ma +subsets.ma categories.ma basic_topologies.ma relations.ma saturations.ma -relations.ma o-algebra.ma subsets.ma +relations.ma subsets.ma o-basic_topologies.ma o-algebra.ma o-saturations.ma +basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma +basic_topologies_to_o-basic_topologies.ma basic_topologies.ma o-basic_topologies.ma relations_to_o-algebra.ma cprop_connectives.ma logic/connectives.ma +relations_to_o-algebra.ma o-algebra.ma relations.ma logic/connectives.ma diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma index c9685f220..dc3c091bb 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma @@ -289,121 +289,3 @@ theorem extS_singleton: | exists; try assumption; split; try assumption; change with (x = x); apply refl] qed. *) - -include "o-algebra.ma". - -definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA (SUBSETS o1) (SUBSETS o2). - intros; - constructor 1; - [ constructor 1; - [ apply (λU.image ?? t U); - | intros; apply (#‡e); ] - | constructor 1; - [ apply (λU.minus_star_image ?? t U); - | intros; apply (#‡e); ] - | constructor 1; - [ apply (λU.star_image ?? t U); - | intros; apply (#‡e); ] - | constructor 1; - [ apply (λU.minus_image ?? t 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); - 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); - 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); - 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); - 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] - [ assumption; - | exists; [apply w] split; assumption] - | cases x1; cases x2; clear x1 x2; exists; [apply w1] - [ exists; [apply w] split; assumption; - | assumption; ]]] -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'. - 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‡#)); - | change with (a1 ∈ minus_star_image ?? t' a → a1 ∈ minus_star_image ?? t a); - apply (. #‡(e ^ -1‡#)); - | change with (a1 ∈ minus_image ?? t a → a1 ∈ minus_image ?? t' a); - apply (. #‡(e‡#)); - | change with (a1 ∈ minus_image ?? t' a → a1 ∈ minus_image ?? t a); - apply (. #‡(e ^ -1‡#)); - | change with (a1 ∈ image ?? t a → a1 ∈ image ?? t' a); - apply (. #‡(e‡#)); - | change with (a1 ∈ image ?? t' a → a1 ∈ image ?? t a); - apply (. #‡(e ^ -1‡#)); - | change with (a1 ∈ star_image ?? t a → a1 ∈ star_image ?? t' a); - apply (. #‡(e‡#)); - | change with (a1 ∈ star_image ?? t' a → a1 ∈ star_image ?? t a); - apply (. #‡(e ^ -1‡#)); ] -qed. - -lemma hint: ∀o1,o2:OA. Type_OF_setoid2 (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). - 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; - | change with (a1 ∈ a → ∀x. x ♮(id1 REL o1) a1→x∈a); intros; - change in f1 with (x = a1); apply (. f1 ^ -1‡#); apply f; - | alias symbol "and" = "and_morphism". - change with ((∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a) → a1 ∈ a); - intro; cases e; clear e; cases x; clear x; change in f with (a1=w); - apply (. f^-1‡#); apply f1; - | change with (a1 ∈ a → ∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a); - intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f] - | change with ((∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a) → a1 ∈ a); - intro; cases e; clear e; cases x; clear x; change in f with (w=a1); - apply (. f‡#); apply f1; - | change with (a1 ∈ a → ∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a); - intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f] - | change with ((∀y.a1 ♮(id1 REL o1) y→y∈a) → a1 ∈ a); intros; - apply (f a1); change with (a1 = a1); apply refl1; - | change with (a1 ∈ a → ∀y.a1 ♮(id1 REL o1) y→y∈a); intros; - change in f1 with (a1 = y); apply (. f1‡#); apply f;] -qed. - -lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid2 (arrows2 OA S T). - intros; apply c; -qed. -coercion hint2. - -(* CSC: ???? forse un uncertain mancato *) -lemma orelation_of_relation_preserves_composition: - ∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3. - orelation_of_relation ?? (G ∘ F) = - comp2 OA (SUBSETS o1) (SUBSETS o2) (SUBSETS o3) - ?? (*(orelation_of_relation ?? F) (orelation_of_relation ?? G)*). - [ apply (orelation_of_relation ?? F); | apply (orelation_of_relation ?? G); ] - intros; split; intro; split; whd; intro; whd in ⊢ (% → %); intros; - [ whd; intros; apply f; exists; [ apply x] split; assumption; - | cases f1; clear f1; cases x1; clear x1; apply (f w); assumption; - | cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ] - 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 ] - | cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ] - 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 ] - | whd; intros; apply f; exists; [ apply y] split; assumption; - | cases f1; clear f1; cases x; clear x; apply (f w); assumption;] -qed. \ No newline at end of file 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 new file mode 100644 index 000000000..40db8183f --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma @@ -0,0 +1,173 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "relations.ma". +include "o-algebra.ma". + +definition SUBSETS: objs1 SET → OAlgebra. + intro A; constructor 1; + [ apply (Ω \sup A); + | apply subseteq; + | apply overlaps; + | apply big_intersects; + | apply big_union; + | apply ({x | True}); + simplify; intros; apply (refl1 ? (eq1 CPROP)); + | apply ({x | False}); + simplify; intros; apply (refl1 ? (eq1 CPROP)); + | intros; whd; intros; assumption + | intros; whd; split; assumption + | intros; apply transitive_subseteq_operator; [2: apply f; | skip | assumption] + | intros; cases f; exists [apply w] assumption + | intros; intros 2; apply (f ? f1 i); + | intros; intros 2; apply f; + (* senza questa change, universe inconsistency *) + whd; change in ⊢ (? ? (λ_:%.?)) with (carr I); + exists; [apply i] assumption; + | intros 3; cases f; + | intros 3; constructor 1; + | intros; cases f; exists; [apply w] + [ assumption + | whd; intros; cases i; simplify; assumption] + | intros; split; intro; + [ cases f; cases x1; + (* senza questa change, universe inconsistency *) + change in ⊢ (? ? (λ_:%.?)) with (carr I); + exists [apply w1] exists [apply w] assumption; + | cases e; cases x; exists; [apply w1] + [ assumption + | (* senza questa change, universe inconsistency *) + whd; change in ⊢ (? ? (λ_:%.?)) with (carr I); + exists; [apply w] assumption]] + | intros; intros 2; cases (f (singleton ? a) ?); + [ exists; [apply a] [assumption | change with (a = a); apply refl1;] + | change in x1 with (a = w); change with (mem A a q); apply (. (x1 \sup -1‡#)); + assumption]] +qed. + +definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA (SUBSETS o1) (SUBSETS o2). + intros; + constructor 1; + [ constructor 1; + [ apply (λU.image ?? t U); + | intros; apply (#‡e); ] + | constructor 1; + [ apply (λU.minus_star_image ?? t U); + | intros; apply (#‡e); ] + | constructor 1; + [ apply (λU.star_image ?? t U); + | intros; apply (#‡e); ] + | constructor 1; + [ apply (λU.minus_image ?? t 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); + 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); + 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); + 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); + 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] + [ assumption; + | exists; [apply w] split; assumption] + | cases x1; cases x2; clear x1 x2; exists; [apply w1] + [ exists; [apply w] split; assumption; + | assumption; ]]] +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'. + 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‡#)); + | change with (a1 ∈ minus_star_image ?? t' a → a1 ∈ minus_star_image ?? t a); + apply (. #‡(e ^ -1‡#)); + | change with (a1 ∈ minus_image ?? t a → a1 ∈ minus_image ?? t' a); + apply (. #‡(e‡#)); + | change with (a1 ∈ minus_image ?? t' a → a1 ∈ minus_image ?? t a); + apply (. #‡(e ^ -1‡#)); + | change with (a1 ∈ image ?? t a → a1 ∈ image ?? t' a); + apply (. #‡(e‡#)); + | change with (a1 ∈ image ?? t' a → a1 ∈ image ?? t a); + apply (. #‡(e ^ -1‡#)); + | change with (a1 ∈ star_image ?? t a → a1 ∈ star_image ?? t' a); + apply (. #‡(e‡#)); + | change with (a1 ∈ star_image ?? t' a → a1 ∈ star_image ?? t a); + apply (. #‡(e ^ -1‡#)); ] +qed. + +lemma hint: ∀o1,o2:OA. Type_OF_setoid2 (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). + 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; + | change with (a1 ∈ a → ∀x. x ♮(id1 REL o1) a1→x∈a); intros; + change in f1 with (x = a1); apply (. f1 ^ -1‡#); apply f; + | alias symbol "and" = "and_morphism". + change with ((∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a) → a1 ∈ a); + intro; cases e; clear e; cases x; clear x; change in f with (a1=w); + apply (. f^-1‡#); apply f1; + | change with (a1 ∈ a → ∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a); + intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f] + | change with ((∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a) → a1 ∈ a); + intro; cases e; clear e; cases x; clear x; change in f with (w=a1); + apply (. f‡#); apply f1; + | change with (a1 ∈ a → ∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a); + intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f] + | change with ((∀y.a1 ♮(id1 REL o1) y→y∈a) → a1 ∈ a); intros; + apply (f a1); change with (a1 = a1); apply refl1; + | change with (a1 ∈ a → ∀y.a1 ♮(id1 REL o1) y→y∈a); intros; + change in f1 with (a1 = y); apply (. f1‡#); apply f;] +qed. + +lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid2 (arrows2 OA S T). + intros; apply c; +qed. +coercion hint2. + +(* CSC: ???? forse un uncertain mancato *) +lemma orelation_of_relation_preserves_composition: + ∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3. + orelation_of_relation ?? (G ∘ F) = + comp2 OA (SUBSETS o1) (SUBSETS o2) (SUBSETS o3) + ?? (*(orelation_of_relation ?? F) (orelation_of_relation ?? G)*). + [ apply (orelation_of_relation ?? F); | apply (orelation_of_relation ?? G); ] + intros; split; intro; split; whd; intro; whd in ⊢ (% → %); intros; + [ whd; intros; apply f; exists; [ apply x] split; assumption; + | cases f1; clear f1; cases x1; clear x1; apply (f w); assumption; + | cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ] + 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 ] + | cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ] + 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 ] + | whd; intros; apply f; exists; [ apply y] split; assumption; + | cases f1; clear f1; cases x; clear x; apply (f w); assumption;] +qed. 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 new file mode 100644 index 000000000..ce6c6f110 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "saturations.ma". +include "o-saturations.ma". +include "relations_to_o-algebra.ma". + +(* These are only conversions :-) *) + +definition o_operator_of_operator: + ∀C:REL. (Ω \sup C => Ω \sup C) → (SUBSETS C ⇒ SUBSETS C). + intros;apply t; +qed. + +definition is_o_saturation_of_is_saturation: + ∀C:REL.∀R: unary_morphism1 (Ω \sup C) (Ω \sup C). + is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R). + intros; apply i; +qed. + +definition is_o_reduction_of_is_reduction: + ∀C:REL.∀R: unary_morphism1 (Ω \sup C) (Ω \sup C). + is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R). + intros; apply i; +qed. \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma index 41e29a4fb..3aaf2d3d6 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma @@ -165,47 +165,3 @@ definition big_union: [ apply (. (#‡(e w))); apply x; | apply (. (#‡(e w)\sup -1)); apply x]] qed. - -(* incluso prima non funziona piu' nulla *) -include "o-algebra.ma". - -definition SUBSETS: objs1 SET → OAlgebra. - intro A; constructor 1; - [ apply (Ω \sup A); - | apply subseteq; - | apply overlaps; - | apply big_intersects; - | apply big_union; - | apply ({x | True}); - simplify; intros; apply (refl1 ? (eq1 CPROP)); - | apply ({x | False}); - simplify; intros; apply (refl1 ? (eq1 CPROP)); - | intros; whd; intros; assumption - | intros; whd; split; assumption - | intros; apply transitive_subseteq_operator; [2: apply f; | skip | assumption] - | intros; cases f; exists [apply w] assumption - | intros; intros 2; apply (f ? f1 i); - | intros; intros 2; apply f; - (* senza questa change, universe inconsistency *) - whd; change in ⊢ (? ? (λ_:%.?)) with (carr I); - exists; [apply i] assumption; - | intros 3; cases f; - | intros 3; constructor 1; - | intros; cases f; exists; [apply w] - [ assumption - | whd; intros; cases i; simplify; assumption] - | intros; split; intro; - [ cases f; cases x1; - (* senza questa change, universe inconsistency *) - change in ⊢ (? ? (λ_:%.?)) with (carr I); - exists [apply w1] exists [apply w] assumption; - | cases e; cases x; exists; [apply w1] - [ assumption - | (* senza questa change, universe inconsistency *) - whd; change in ⊢ (? ? (λ_:%.?)) with (carr I); - exists; [apply w] assumption]] - | intros; intros 2; cases (f (singleton ? a) ?); - [ exists; [apply a] [assumption | change with (a = a); apply refl1;] - | change in x1 with (a = w); change with (mem A a q); apply (. (x1 \sup -1‡#)); - assumption]] -qed. -- 2.39.2