From 680b7493de237259ddb589a92be4b8bbc8de3cbf Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 21 Dec 2008 23:56:30 +0000 Subject: [PATCH] 1) no more DAEMONS 2) f, f-, f*, f-* are morphisms now --- .../formal_topology/overlap/o-algebra.ma | 70 +++++++++++++------ .../overlap/o-concrete_spaces.ma | 13 ++-- 2 files changed, 59 insertions(+), 24 deletions(-) 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 12b348cc3..9cadd514c 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -143,8 +143,6 @@ notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}. notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}. interpretation "o-relation f⎻" 'OR_f_minus r = (or_f_minus _ _ r). -axiom DAEMON: False. - definition ORelation_setoid : OAlgebra → OAlgebra → setoid1. intros (P Q); constructor 1; @@ -170,36 +168,64 @@ coercion hint3. lemma hint2: OAlgebra → setoid. intros; apply (oa_P o). qed. coercion hint2. +definition or_f_minus_star2: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q. + intros; constructor 1; + [ apply or_f_minus_star; + | intros; cases H; assumption] +qed. + +definition or_f2: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q. + intros; constructor 1; + [ apply or_f; + | intros; cases H; assumption] +qed. + +definition or_f_minus2: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET Q P. + intros; constructor 1; + [ apply or_f_minus; + | intros; cases H; assumption] +qed. + +definition or_f_star2: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET Q P. + intros; constructor 1; + [ apply or_f_star; + | intros; cases H; assumption] +qed. + +interpretation "o-relation f⎻* 2" 'OR_f_minus_star r = (fun_1 __ (or_f_minus_star2 _ _) r). +interpretation "o-relation f⎻ 2" 'OR_f_minus r = (fun_1 __ (or_f_minus2 _ _) r). +interpretation "o-relation f* 2" 'OR_f_star r = (fun_1 __ (or_f_star2 _ _) r). +coercion or_f2. + definition ORelation_composition : ∀P,Q,R. binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R). intros; constructor 1; [ intros (F G); constructor 1; - [ apply (G ∘ F); - | apply (G⎻* ∘ F⎻* ); + [ apply (or_f2 ?? G ∘ or_f2 ?? F); + | alias symbol "compose" = "category1 composition". + apply (G⎻* ∘ F⎻* ); | apply (F* ∘ G* ); | apply (F⎻ ∘ G⎻); - | intros; change with ((G (F p) ≤ q) = (p ≤ (F* (G* q)))); + | intros; + alias symbol "eq" = "setoid1 eq". + change with ((G (F p) ≤ q) = (p ≤ (F* (G* q)))); apply (.= or_prop1 ??? (F p) ?); apply (.= or_prop1 ??? p ?); apply refl1 - | intros; change with ((F⎻ (G⎻ p) ≤ q) = (p ≤ (G⎻* (F⎻* q)))); - apply (.= or_prop2 ??? (G⎻ p) ?); - apply (.= or_prop2 ??? p ?); + | intros; alias symbol "eq" = "setoid1 eq". + change with ((F⎻ (G⎻ p) ≤ q) = (p ≤ (G⎻* (F⎻* q)))); + alias symbol "trans" = "trans1". + apply (.= or_prop2 ?? F ??); + apply (.= or_prop2 ?? G ??); apply refl1; | intros; change with ((G (F (p)) >< q) = (p >< (F⎻ (G⎻ q)))); apply (.= or_prop3 ??? (F p) ?); apply (.= or_prop3 ??? p ?); apply refl1 ] -| intros; repeat split; simplify; cases DAEMON (* - [ apply trans1; [2: apply prop1; [3: apply rule #; | skip | 4: - apply rule (†?); - - lapply (.= ((†H1)‡#)); [8: apply Hletin; - [ apply trans1; [2: lapply (prop1); [apply Hletin; -*)] +| intros; split; simplify; [1,3: apply ((†H)‡(†H1)); | 2,4: apply ((†H1)‡(†H));]] qed. definition OA : category1. @@ -210,8 +236,12 @@ split; [1,2,3,4: apply id1; |5,6,7:intros; apply refl1;] | apply ORelation_composition; -| intros; repeat split; unfold ORelation_composition; simplify; - [1,3: apply (comp_assoc1); | 2,4: apply ((comp_assoc1 :?) ^ -1);] -| intros; repeat split; unfold ORelation_composition; simplify; apply id_neutral_left1; -| intros; repeat split; unfold ORelation_composition; simplify; apply id_neutral_right1;] -qed. +| intros; split; + [ apply (comp_assoc1 ????? (a12⎻* ) (a23⎻* ) (a34⎻* )); + | alias symbol "invert" = "setoid1 symmetry". + apply ((comp_assoc1 ????? (a34⎻) (a23⎻) (a12⎻)) \sup -1); + | apply (comp_assoc1 ????? a12 a23 a34); + | apply ((comp_assoc1 ????? (a34* ) (a23* ) (a12* )) \sup -1);] +| intros; split; unfold ORelation_composition; simplify; apply id_neutral_left1; +| intros; split; unfold ORelation_composition; simplify; apply id_neutral_right1;] +qed. \ 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 index 4e989cb14..61b8f77e7 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma @@ -32,15 +32,20 @@ notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b} interpretation "Existential pre-image ⊩⎻" 'ext x = (or_f_minus _ _ (rel x)). definition A : ∀b:BP. unary_morphism (oa_P (form b)) (oa_P (form b)). -intros; constructor 1; [ apply (λx.□_b (Ext⎽b x)); | intros; apply (†(†H));] qed. +intros; constructor 1; + [ apply (λx.□_b (Ext⎽b x)); + | do 2 unfold FunClass_1_OF_carr1; intros; apply (†(†H));] +qed. lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed. coercion xxx. definition d_p_i : - ∀S:setoid.∀I:setoid.∀d:unary_morphism S S.∀p:ums I S.ums I S. -intros; constructor 1; [ apply (λi:I. u (c i));| intros; apply (†(†H));]. -qed. + ∀S,I:SET.∀d:unary_morphism S S.∀p:arrows1 SET I S.arrows1 SET I S. +intros; constructor 1; + [ apply (λi:I. u (c i)); + | unfold FunClass_1_OF_carr1; intros; apply (†(†H));]. +qed. alias symbol "eq" = "setoid eq". alias symbol "and" = "o-algebra binary meet". -- 2.39.2