From 62e9e8296d172d6497f9ad29bad402fbad2014c3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 17 Dec 2008 17:35:00 +0000 Subject: [PATCH] foo overlap --- .../contribs/formal_topology/overlap/Makefile | 16 ++ .../contribs/formal_topology/overlap/depends | 7 + .../{ => overlap}/o-algebra.ma | 9 +- .../formal_topology/overlap/o-basic_pairs.ma | 187 ++++++++++++++++++ .../overlap/o-concrete_spaces.ma | 131 ++++++++++++ .../formal_topology/overlap/o-saturations.ma | 51 +++++ .../contribs/formal_topology/overlap/root | 1 + 7 files changed, 398 insertions(+), 4 deletions(-) create mode 100644 helm/software/matita/contribs/formal_topology/overlap/Makefile create mode 100644 helm/software/matita/contribs/formal_topology/overlap/depends rename helm/software/matita/contribs/formal_topology/{ => overlap}/o-algebra.ma (97%) create mode 100644 helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma create mode 100644 helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma create mode 100644 helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma create mode 100644 helm/software/matita/contribs/formal_topology/overlap/root diff --git a/helm/software/matita/contribs/formal_topology/overlap/Makefile b/helm/software/matita/contribs/formal_topology/overlap/Makefile new file mode 100644 index 000000000..92a16d1f0 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/Makefile @@ -0,0 +1,16 @@ +include ../../Makefile.defs + +DIR=$(shell basename $$PWD) + +$(DIR) all: + $(BIN)../matitac +$(DIR).opt opt all.opt: + $(BIN)../matitac.opt +clean: + $(BIN)../matitaclean +clean.opt: + $(BIN)../matitaclean.opt +depend: + $(BIN)../matitadep -dot && rm depends.dot +depend.opt: + $(BIN)../matitadep.opt -dot && rm depends.dot diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends new file mode 100644 index 000000000..039a5df4e --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/depends @@ -0,0 +1,7 @@ +o-basic_pairs.ma datatypes/categories.ma o-algebra.ma +o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma +o-saturations.ma o-algebra.ma +o-algebra.ma datatypes/bool.ma datatypes/categories.ma logic/cprop_connectives.ma +datatypes/bool.ma +datatypes/categories.ma +logic/cprop_connectives.ma diff --git a/helm/software/matita/contribs/formal_topology/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma similarity index 97% rename from helm/software/matita/contribs/formal_topology/o-algebra.ma rename to helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma index b1ef232ff..f04b0a70c 100644 --- a/helm/software/matita/contribs/formal_topology/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -118,12 +118,12 @@ interpretation "o-algebra join" 'oa_join \eta.f = (oa_join _ _ f). record ORelation (P,Q : OAlgebra) : Type ≝ { or_f : P → Q; - or_f_minus : P → Q; + or_f_minus_star : P → Q; or_f_star : Q → P; - or_f_minus_star : Q → P; + or_f_minus : Q → P; or_prop1 : ∀p,q. or_f p ≤ q ⇔ p ≤ or_f_star q; or_prop2 : ∀p,q. or_f_minus p ≤ q ⇔ p ≤ or_f_minus_star q; - or_prop3 : ∀p,q. or_f_minus q >< p ⇔ q >< or_f_minus p + or_prop3 : ∀p,q. or_f p >< q ⇔ p >< or_f_minus q }. notation < "⨍ \sub (term 90 r)" non associative with precedence 90 for @{'OR_f $r}. @@ -132,6 +132,7 @@ notation > "⨍_(term 90 r)" non associative with precedence 90 for @{'OR_f $r}. interpretation "o-relation f" 'OR_f r = (or_f _ _ r). interpretation "o-relation f x" 'OR_f_app1 r a = (or_f _ _ r a). + definition ORelation_setoid : OAlgebra → OAlgebra → setoid1. intros (P Q); constructor 1; @@ -162,7 +163,7 @@ split; | intros; apply (ORelation_setoid o o1); | intro O; split; [1,2,3,4: apply (λx.x); - |*:intros;split;intros; assumption; + |*:intros;split;intros; assumption; ] |*: elim DAEMON;] qed. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma new file mode 100644 index 000000000..9bd76ebeb --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma @@ -0,0 +1,187 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "o-algebra.ma". +include "datatypes/categories.ma". + +record basic_pair: Type ≝ + { concr: OA; + form: OA; + rel: arrows1 ? concr form + }. + +notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}. +notation < "x (⊩ \below c) y" with precedence 45 for @{'Vdash2 $x $y $c}. +notation < "⊩ \sub c" with precedence 60 for @{'Vdash $c}. +notation > "⊩ " with precedence 60 for @{'Vdash ?}. + +interpretation "basic pair relation indexed" 'Vdash2 x y c = (rel c x y). +interpretation "basic pair relation (non applied)" 'Vdash c = (rel c). + +alias symbol "eq" = "setoid1 eq". +alias symbol "compose" = "category1 composition". +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 ∘ ⊩ + }. + +notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}. +notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}. + +interpretation "concrete relation" 'concr_rel r = (concr_rel __ r). +interpretation "formal relation" 'form_rel r = (form_rel __ r). + +definition relation_pair_equality: + ∀o1,o2. equivalence_relation1 (relation_pair o1 o2). + intros; + constructor 1; + [ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c); + | simplify; + intros; + apply refl1; + | simplify; + intros 2; + apply sym1; + | simplify; + intros 3; + apply trans1; + ] +qed. + +definition relation_pair_setoid: basic_pair → basic_pair → setoid1. + intros; + constructor 1; + [ apply (relation_pair b b1) + | apply relation_pair_equality + ] +qed. + +lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩. + intros 5 (o1 o2 r r' H); change in H with (⊩ ∘ r\sub\c = ⊩ ∘ r'\sub\c); + apply (.= (commute ?? r \sup -1)); + apply (.= H); + apply (.= (commute ?? r')); + apply refl1; +qed. + + +definition id_relation_pair: ∀o:basic_pair. relation_pair o o. + intro; + constructor 1; + [1,2: apply id1; + | lapply (id_neutral_right1 ? (concr o) ? (⊩)) as H; + lapply (id_neutral_left1 ?? (form o) (⊩)) as H1; + apply (.= H); + apply (H1 \sup -1);] +qed. + +definition relation_pair_composition: + ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3). + intros; + constructor 1; + [ intros (r r1); + constructor 1; + [ 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); + apply (.= #‡H1); + apply (.= ASSOC1\sup -1); + apply (.= H‡#); + apply ASSOC1] + | intros; + 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')); + apply (.= ASSOC1 \sup -1); + apply (.= H‡#); + apply (.= ASSOC1); + apply (.= #‡(commute ?? b')\sup -1); + apply (ASSOC1 \sup -1)] +qed. + +definition BP: category1. + constructor 1; + [ apply basic_pair + | apply relation_pair_setoid + | apply id_relation_pair + | apply relation_pair_composition + | intros; + 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 (⊩ ∘ (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). + intros; constructor 1; + [ apply (ext ? ? (rel o)); + | intros; + apply (.= #‡H); + apply refl1] +qed. + +definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝ + λo.extS ?? (rel o). +*) + +(* +definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)). + intros (o); constructor 1; + [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b }); + intros; simplify; apply (.= (†H)‡#); apply refl1 + | intros; split; simplify; intros; + [ apply (. #‡((†H)‡(†H1))); assumption + | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]] +qed. + +interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V). + +definition fintersectsS: + ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)). + intros (o); constructor 1; + [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b }); + intros; simplify; apply (.= (†H)‡#); apply refl1 + | intros; split; simplify; intros; + [ apply (. #‡((†H)‡(†H1))); assumption + | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]] +qed. + +interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V). +*) + +(* +definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP. + intros (o); constructor 1; + [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y); + | intros; split; intros; cases H2; exists [1,3: apply w] + [ apply (. (#‡H1)‡(H‡#)); assumption + | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]] +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 _)). +*) \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma new file mode 100644 index 000000000..135dae3c9 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma @@ -0,0 +1,131 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "o-basic_pairs.ma". +include "o-saturations.ma". + +lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed. +coercion xxx. + +record concrete_space : Type ≝ + { bp:> BP; + downarrow: form bp → oa_P (form bp); + downarrow_is_sat: is_saturation ? downarrow; + converges: ∀q1,q2:form bp. + or_f_minus ?? (⊩) q1 ∧ or_f_minus ?? (⊩) q2 = + or_f_minus ?? (⊩) ((downarrow q1) ∧ (downarrow q2)); + all_covered: (*⨍^-_bp*) or_f_minus ?? (⊩) (oa_one (form bp)) = oa_one (concr bp); + il2: ∀I:setoid.∀p:ums I (oa_P (form bp)). + downarrow (oa_join ? I (mk_unary_morphism ?? (λi:I. downarrow (p i)) ?)) = + oa_join ? I (mk_unary_morphism ?? (λi:I. downarrow (p i)) ?) + }. + +definition bp': concrete_space → basic_pair ≝ λc.bp c. + +coercion bp'. + +record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝ + { rp:> arrows1 ? CS1 CS2; + respects_converges: + ∀b,c. + extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) = + BPextS CS1 ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c)); + respects_all_covered: + extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1) + }. + +definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝ + λCS1,CS2,c. rp CS1 CS2 c. + +coercion rp'. + +definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1. + intros; + constructor 1; + [ apply (convergent_relation_pair c c1) + | constructor 1; + [ intros; + apply (relation_pair_equality c c1 c2 c3); + | intros 1; apply refl1; + | intros 2; apply sym1; + | intros 3; apply trans1]] +qed. + +definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝ + λCS1,CS2,c.rp ?? c. + +coercion rp''. + +definition convergent_relation_space_composition: + ∀o1,o2,o3: concrete_space. + binary_morphism1 + (convergent_relation_space_setoid o1 o2) + (convergent_relation_space_setoid o2 o3) + (convergent_relation_space_setoid o1 o3). + intros; constructor 1; + [ intros; whd in c c1 ⊢ %; + constructor 1; + [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption] + | intros; + change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c); + change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?))) + with (c1 \sub \f ∘ c \sub \f); + change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?)))) + 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 (c1 \sub \c ∘ c \sub \c); + apply (.= (extS_com ??????)); + apply (.= (†(respects_all_covered ???))); + apply (.= respects_all_covered ???); + apply refl1] + | intros; + 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)); + apply refl1] +qed. + +definition CSPA: category1. + constructor 1; + [ apply concrete_space + | apply convergent_relation_space_setoid + | intro; constructor 1; + [ apply id1 + | intros; + unfold id; simplify; + apply (.= (equalset_extS_id_X_X ??)); + apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡ + (equalset_extS_id_X_X ??)\sup -1))); + apply refl1; + | apply (.= (equalset_extS_id_X_X ??)); + apply refl1] + | apply convergent_relation_space_composition + | intros; simplify; + change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12); + apply (.= ASSOC1); + apply refl1 + | intros; simplify; + change with (a ∘ id1 ? o1 = a); + apply (.= id_neutral_right1 ????); + apply refl1 + | intros; simplify; + change with (id1 ? o2 ∘ a = a); + apply (.= id_neutral_left1 ????); + apply refl1] +qed. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma new file mode 100644 index 000000000..9b68972b4 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "o-algebra.ma". + +definition hint1: OA → Type ≝ λc:OA.carr (oa_P c). +coercion hint1. + +definition hint2: ∀C.hint1 C → carr1 ((λx.x) (setoid1_of_setoid (oa_P C))). +intros; assumption; +qed. +coercion hint2. + +alias symbol "eq" = "setoid1 eq". +definition is_saturation ≝ + λC:OA.λA:C → C. + ∀U,V. (U ≤ A V) = (A U ≤ A V). + +definition is_reduction ≝ + λC:OA.λJ:C → 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 (oa_leq_refl C). +qed. + +theorem saturation_monotone: + ∀C,A. is_saturation C A → + ∀U,V:C. U ≤ V → A U ≤ A V. + intros; apply (if ?? (H ??)); apply (oa_leq_trans C); + [apply V|3: apply saturation_expansive ] + assumption. +qed. + +theorem saturation_idempotent: ∀C,A. is_saturation C A → ∀U. + eq (oa_P C) (A (A U)) (A U). + intros; apply (oa_leq_antisym C); + [ apply (if ?? (H (A U) U)); apply (oa_leq_refl C). + | apply saturation_expansive; assumption] +qed. diff --git a/helm/software/matita/contribs/formal_topology/overlap/root b/helm/software/matita/contribs/formal_topology/overlap/root new file mode 100644 index 000000000..d57275734 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/root @@ -0,0 +1 @@ +baseuri=cic:/matita/formal_topology -- 2.39.2