From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 21 Dec 2008 23:56:30 +0000 (+0000)
Subject: 1) no more DAEMONS
X-Git-Tag: make_still_working~4338
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=680b7493de237259ddb589a92be4b8bbc8de3cbf;p=helm.git

1) no more DAEMONS
2) f, f-, f*, f-* are morphisms now
---

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".