From: Claudio Sacerdoti Coen Date: Sun, 4 Jan 2009 15:36:21 +0000 (+0000) Subject: Yet another universe problem :-( X-Git-Tag: make_still_working~4298 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8dddbb8d9eac4bc85f071b192f8ae7e8b6ac7060;p=helm.git Yet another universe problem :-( --- diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends index 1ff1aea9c..fb3dc8f87 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/depends +++ b/helm/software/matita/contribs/formal_topology/overlap/depends @@ -1,10 +1,10 @@ -o-basic_pairs.ma datatypes/categories.ma o-algebra.ma +o-basic_pairs.ma o-algebra.ma o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma o-saturations.ma o-algebra.ma o-algebra.ma categories.ma logic/cprop_connectives.ma o-formal_topologies.ma o-basic_topologies.ma categories.ma logic/cprop_connectives.ma subsets.ma categories.ma o-algebra.ma +relations.ma subsets.ma o-basic_topologies.ma o-algebra.ma o-saturations.ma -datatypes/categories.ma logic/cprop_connectives.ma diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma index c6d91db94..55d692190 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -134,9 +134,7 @@ intros; split; intro x; simplify; cases x; simplify; assumption;] qed. -notation "hovbox(a ∧ b)" left associative with precedence 35 -for @{ 'oa_meet_bin $a $b }. -interpretation "o-algebra binary meet" 'oa_meet_bin a b = +interpretation "o-algebra binary meet" 'and a b = (fun21 ___ (binary_meet _) a b). coercion Type1_OF_OAlgebra nocomposites. @@ -349,4 +347,4 @@ coercion objs2_SET1_OF_OA. lemma Type_OF_category2_OF_SET1_OF_OA: OA → Type_OF_category2 SET1. intro; apply (oa_P t); qed. -coercion Type_OF_category2_OF_SET1_OF_OA. \ No newline at end of file +coercion Type_OF_category2_OF_SET1_OF_OA. diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma new file mode 100644 index 000000000..3653d3a64 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma @@ -0,0 +1,249 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "subsets.ma". + +record binary_relation (A,B: SET) : Type1 ≝ + { satisfy:> binary_morphism1 A B CPROP }. + +notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{'satisfy $r $x $y}. +notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}. +interpretation "relation applied" 'satisfy r x y = (fun21 ___ (satisfy __ r) x y). + +definition binary_relation_setoid: SET → SET → SET1. + intros (A B); + constructor 1; + [ apply (binary_relation A B) + | constructor 1; + [ apply (λA,B.λr,r': binary_relation A B. ∀x,y. r x y ↔ r' x y) + | simplify; intros 3; split; intro; assumption + | simplify; intros 5; split; intro; + [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption + | simplify; intros 7; split; intro; + [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ] + [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ] + assumption]] +qed. + +definition composition: + ∀A,B,C. + binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C). + intros; + constructor 1; + [ intros (R12 R23); + constructor 1; + constructor 1; + [ alias symbol "and" = "and_morphism". + (* carr to avoid universe inconsistency *) + apply (λs1:carr A.λs3:carr C.∃s2:carr B. s1 ♮R12 s2 ∧ s2 ♮R23 s3); + | intros; + split; intro; cases H (w H3); clear H; exists; [1,3: apply w ] + [ apply (. (e‡#)‡(#‡e1)); assumption + | apply (. ((e \sup -1)‡#)‡(#‡(e1 \sup -1))); assumption]] + | intros 8; split; intro H2; simplify in H2 ⊢ %; + cases H2 (w H3); clear H2; exists [1,3: apply w] cases H3 (H2 H4); clear H3; + [ lapply (if ?? (e x w) H2) | lapply (fi ?? (e x w) H2) ] + [ lapply (if ?? (e1 w y) H4)| lapply (fi ?? (e1 w y) H4) ] + exists; try assumption; + split; assumption] +qed. +axiom daemon: False. +definition REL: category1. + constructor 1; + [ apply setoid + | intros (T T1); apply (binary_relation_setoid T T1) + | intros; constructor 1; + constructor 1; unfold setoid1_of_setoid; simplify; + [ change with (carr o → carr o → CProp); intros; apply (eq1 ? c c1) ]] cases daemon; qed. + | intros; split; intro; + [ apply (.= (e ^ -1)); + apply (.= e2); + apply e1 + | apply (.= e); + apply (.= e2); + apply (e1 ^ -1)]] + | apply composition + | intros 9; + split; intro; + cases f (w H); clear f; cases H; clear H; + [cases f (w1 H); clear f | cases f1 (w1 H); clear f1] + cases H; clear H; + exists; try assumption; + split; try assumption; + exists; try assumption; + split; assumption + |6,7: intros 5; unfold composition; simplify; split; intro; + unfold setoid1_of_setoid in x y; simplify in x y; + [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold; + [ apply (. (e ^ -1 : eq1 ? w x)‡#); assumption + | apply (. #‡(e : eq1 ? w y)); assumption] + |2,4: exists; try assumption; split; first [apply refl1 | assumption]]] +qed. + +definition full_subset: ∀s:REL. Ω \sup s. + apply (λs.{x | True}); + intros; simplify; split; intro; assumption. +qed. + +coercion full_subset. + +definition setoid1_of_REL: REL → setoid ≝ λS. S. + +coercion setoid1_of_REL. + +definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b. + apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x}); + intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1. +qed. + +interpretation "subset comprehension" 'comprehension s p = + (comprehension s (mk_unary_morphism __ p _)). + +definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X). + apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?); + [ intros; simplify; apply (.= (H‡#)); apply refl1 + | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption; + [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption + | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]] +qed. + +definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X. + (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*) + intros (X S r); constructor 1; + [ intro F; constructor 1; constructor 1; + [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a); + | intros; split; intro; cases f (H1 H2); clear f; split; + [ apply (. (H‡#)); assumption + |3: apply (. (H\sup -1‡#)); assumption + |2,4: cases H2 (w H3); exists; [1,3: apply w] + [ apply (. (#‡(H‡#))); assumption + | apply (. (#‡(H \sup -1‡#))); assumption]]] + | intros; split; simplify; intros; cases f; cases H1; split; + [1,3: assumption + |2,4: exists; [1,3: apply w] + [ apply (. (#‡H)‡#); assumption + | apply (. (#‡H\sup -1)‡#); assumption]]] +qed. + +lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X. + intros; + unfold extS; simplify; + split; simplify; + [ intros 2; change with (a ∈ X); + cases f; clear f; + cases H; clear H; + cases x; clear x; + change in f2 with (eq1 ? a w); + apply (. (f2\sup -1‡#)); + assumption + | intros 2; change in f with (a ∈ X); + split; + [ whd; exact I + | exists; [ apply a ] + split; + [ assumption + | change with (a = a); apply refl]]] +qed. + +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; + exists; [apply w1] split [2: assumption] constructor 1; [assumption] + exists; [apply w] split; assumption + | cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption] + cases H3 (H4 H5); cases H4 (w1 H6); clear H3 H4; cases H6 (w2 H7); clear H6; + cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split; + 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