X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fconcrete_spaces.ma;h=d95072cb973a2fa4c65f3ecd60212f84ba71438a;hb=dd7f52dfd7f80b80368661fce5b58b644c102d7b;hp=568f3c0528488ec22c45a10378ebb0e5861f8435;hpb=80c5d1841a5ea1d302f9b6865a6f1539d9361524;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index 568f3c052..d95072cb9 100644
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -14,124 +14,107 @@
 
 include "formal_topology/basic_pairs.ma".
 
-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. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
- apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
-  [ intros; simplify; apply (.= (H‡#)); apply refl1
-  | intros; simplify; split; intros; simplify; intros;
-     [ apply (. #‡(#‡H)); assumption
-     | apply (. #‡(#‡H\sup -1)); 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.
-
-definition fintersects: ∀o: basic_pair. form o → form o → Ω \sup (form o).
- apply
-  (λo: basic_pair.λa,b: form o.
-    {c | ext ?? (rel o) c ⊆ ext ?? (rel o) a ∩ ext ?? (rel o) b });
- intros; simplify; apply (.= (†H)‡#); apply refl1.
-qed.
-
-interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
-
-definition fintersectsS:
- ∀o:basic_pair. Ω \sup (form o) → Ω \sup (form o) → Ω \sup (form o).
- apply (λo: basic_pair.λa,b: Ω \sup (form o).
-  {c | ext ?? (rel o) c ⊆ extS ?? (rel o) a ∩ extS ?? (rel o) b });
- intros; simplify; apply (.= (†H)‡#); apply refl1.
-qed.
-
-interpretation "fintersectsS" 'fintersects U V = (fintersectsS _ U V).
-
-(*
-definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp.
- apply (λo:basic_pair.λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y);
-
-interpretation "basic pair relation for subsets" 'Vdash2 x y = (relS _ x y).
-interpretation "basic pair relation for subsets (non applied)" 'Vdash = (relS _).
-
 record concrete_space : Type ≝
- { bp:> basic_pair;
+ { bp:> BP;
    converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
    all_covered: ∀x: concr bp. x ⊩ form bp
  }.
 
+definition bp': concrete_space → basic_pair ≝ λc.bp c.
+
+coercion bp'.
+
 record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
- { rp:> relation_pair CS1 CS2;
+ { rp:> arrows1 ? CS1 CS2;
    respects_converges:
     ∀b,c.
-     extS ?? rp \sub\c (extS ?? (rel CS2) (b ↓ c)) =
-     extS ?? (rel CS1) ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f 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 (extS ?? (rel CS2) (form CS2)) =
-    extS ?? (rel CS1) (form CS1)
+    extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1)
  }.
 
-definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid.
+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 refl;
-     | intros 2; apply sym; 
-     | intros 3; apply trans]]
+     | intros 1; apply refl1;
+     | intros 2; apply sym1; 
+     | intros 3; apply trans1]]
 qed.
 
-lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id ? o) X = X.
- intros;
- unfold extS;
- split;
-  [ intros 2;
-    cases m; clear m;
-    cases H; clear H;
-    cases H1; clear H1;
-    whd in H;
-    apply (eq_elim_r'' ????? H);
-    assumption
-  | intros 2;
-    constructor 1;
-     [ whd; exact I 
-     | exists; [ apply a ]
-       split;
-        [ assumption
-        | whd; constructor 1]]]
+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 (c \sub \c ∘ c1 \sub \c);
+          change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
+            with (c \sub \f ∘ c1 \sub \f);
+          change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
+            with (c \sub \f ∘ c1 \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 (c \sub \c ∘ c1 \sub \c);
+          apply (.= (extS_com ??????));
+          apply (.= (†(respects_all_covered ???)));
+          apply (.= respects_all_covered ???);
+          apply refl1]
+     | intros;
+       change with (a ∘ b = a' ∘ b');
+       change in H with (rp'' ?? a = rp'' ?? a');
+       change in H1 with (rp'' ?? b = rp ?? b');
+       apply (.= (H‡H1));
+       apply refl1]
 qed.
 
-definition CSPA: category.
+definition CSPA: category1.
  constructor 1;
   [ apply concrete_space
   | apply convergent_relation_space_setoid
   | intro; constructor 1;
-     [ apply id
+     [ apply id1
      | intros;
        unfold id; simplify;
        apply (.= (equalset_extS_id_X_X ??));
-
-     |
-     ]
-  |*)
\ No newline at end of file
+       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 ((a12 ∘ a23) ∘ a34 = a12 ∘ (a23 ∘ a34));
+    apply (.= ASSOC1);
+    apply refl1
+  | intros; simplify;
+    change with (id1 ? o1 ∘ a = a);
+    apply (.= id_neutral_left1 ????);
+    apply refl1
+  | intros; simplify;
+    change with (a ∘ id1 ? o2 = a);
+    apply (.= id_neutral_right1 ????);
+    apply refl1]
+qed.