helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "o-basic_pairs.ma".
  16 include "o-saturations.ma".
  17
  18 notation "□ \sub b" non associative with precedence 90 for @{'box $b}.
  19 notation > "□_term 90 b" non associative with precedence 90 for @{'box $b}.
  20 interpretation "Universal image ⊩⎻*" 'box x = (fun12 _ _ (or_f_minus_star _ _) (rel x)).
  21
  22 notation "◊ \sub b" non associative with precedence 90 for @{'diamond $b}.
  23 notation > "◊_term 90 b" non associative with precedence 90 for @{'diamond $b}.
  24 interpretation "Existential image ⊩" 'diamond x = (fun12 _ _ (or_f _ _) (rel x)).
  25
  26 notation "'Rest' \sub b" non associative with precedence 90 for @{'rest $b}.
  27 notation > "'Rest'⎽term 90 b" non associative with precedence 90 for @{'rest $b}.
  28 interpretation "Universal pre-image ⊩*" 'rest x = (fun12 _ _ (or_f_star _ _) (rel x)).
  29
  30 notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}.
  31 notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}.
  32 interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 _ _ (or_f_minus _ _) (rel x)).
  33
  34 definition A : ∀b:BP. unary_morphism1 (form b) (form b).
  35 intros; constructor 1;
  36  [ apply (λx.□_b (Ext⎽b x));
  37  | do 2 unfold FunClass_1_OF_Type_OF_setoid21; intros; apply  (†(†e));]
  38 qed.
  39
  40 lemma down_p : ∀S:SET1.∀I:SET.∀u:S⇒S.∀c:arrows2 SET1 I S.∀a:I.∀a':I.a=a'→u (c a)=u (c a').
  41 intros; apply (†(†e));
  42 qed.
  43
  44 record concrete_space : Type2 ≝
  45  { bp:> BP;
  46    (*distr : is_distributive (form bp);*)
  47    downarrow: unary_morphism1 (form bp) (form bp);
  48    downarrow_is_sat: is_o_saturation ? downarrow;
  49    converges: ∀q1,q2.
  50      (Ext⎽bp q1 ∧ (Ext⎽bp q2)) = (Ext⎽bp ((downarrow q1) ∧ (downarrow q2)));
  51    all_covered: Ext⎽bp (oa_one (form bp)) = oa_one (concr bp);
  52    il2: ∀I:SET.∀p:arrows2 SET1 I (form bp).
  53      downarrow (∨ { x ∈ I | downarrow (p x) | down_p ???? }) =
  54      ∨ { x ∈ I | downarrow (p x) | down_p ???? };
  55    il1: ∀q.downarrow (A ? q) = A ? q
  56  }.
  57
  58 interpretation "o-concrete space downarrow" 'downarrow x =
  59   (fun11 __ (downarrow _) x).
  60
  61 definition bp': concrete_space → basic_pair ≝ λc.bp c.
  62 coercion bp'.
  63
  64 definition bp'': concrete_space → objs2 BP.
  65  intro; apply (bp' c);
  66 qed.
  67 coercion bp''.
  68
  69 definition binary_downarrow :
  70   ∀C:concrete_space.binary_morphism1 (form C) (form C) (form C).
  71 intros; constructor 1;
  72 [ intros; apply (↓ t ∧ ↓ t1);
  73 | intros;
  74   alias symbol "prop2" = "prop21".
  75   alias symbol "prop1" = "prop11".
  76   apply ((†e)‡(†e1));]
  77 qed.
  78
  79 interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 _ _ _ (binary_downarrow _) a b).
  80
  81 record convergent_relation_pair (CS1,CS2: concrete_space) : Type2 ≝
  82  { rp:> arrows2 ? CS1 CS2;
  83    respects_converges:
  84     ∀b,c. eq1 ? (rp\sub\c⎻ (Ext⎽CS2 (b ↓ c))) (Ext⎽CS1 (rp\sub\f⎻ b ↓ rp\sub\f⎻ c));
  85    respects_all_covered:
  86      eq1 ? (rp\sub\c⎻ (Ext⎽CS2 (oa_one (form CS2))))
  87            (Ext⎽CS1 (oa_one (form CS1)))
  88  }.
  89
  90 definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝
  91  λCS1,CS2,c. rp CS1 CS2 c.
  92 coercion rp'.
  93
  94 definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid2.
  95  intros;
  96  constructor 1;
  97   [ apply (convergent_relation_pair c c1)
  98   | constructor 1;
  99      [ intros;
 100        apply (relation_pair_equality c c1 c2 c3);
 101      | intros 1; apply refl2;
 102      | intros 2; apply sym2;
 103      | intros 3; apply trans2]]
 104 qed.
 105
 106
 107 definition rp'': ∀CS1,CS2.carr2 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝
 108  λCS1,CS2,c.rp ?? c.
 109 coercion rp''.
 110
 111 definition rp''': ∀CS1,CS2.Type_OF_setoid2 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝
 112  λCS1,CS2,c.rp ?? c.
 113 coercion rp'''.
 114
 115 definition rp'''': ∀CS1,CS2.Type_OF_setoid2 (convergent_relation_space_setoid CS1 CS2) → carr2 (arrows2 BP CS1 CS2) ≝
 116  λCS1,CS2,c.rp ?? c.
 117 coercion rp''''.
 118
 119 definition convergent_relation_space_composition:
 120  ∀o1,o2,o3: concrete_space.
 121   binary_morphism2
 122    (convergent_relation_space_setoid o1 o2)
 123    (convergent_relation_space_setoid o2 o3)
 124    (convergent_relation_space_setoid o1 o3).
 125  intros; constructor 1;
 126      [ intros; whd in t t1 ⊢ %;
 127        constructor 1;
 128         [ apply (t1 ∘ t);
 129         | intros;
 130           change in ⊢ (? ? ? % ?) with (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (b↓c))));
 131           unfold FunClass_1_OF_Type_OF_setoid21;
 132           alias symbol "trans" = "trans1".
 133           apply (.= († (respects_converges : ?)));
 134           apply (respects_converges ?? t (t1\sub\f⎻ b) (t1\sub\f⎻ c));
 135         | change in ⊢ (? ? ? % ?) with (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (oa_one (form o3)))));
 136           unfold FunClass_1_OF_Type_OF_setoid21;
 137           apply (.= (†(respects_all_covered :?)));
 138           apply rule (respects_all_covered ?? t);]
 139      | intros;
 140        change with (b ∘ a = b' ∘ a');
 141        change in e with (rp'' ?? a = rp'' ?? a');
 142        change in e1 with (rp'' ?? b = rp ?? b');
 143        apply (e‡e1);]
 144 qed.
 145
 146 definition CSPA: category2.
 147  constructor 1;
 148   [ apply concrete_space
 149   | apply convergent_relation_space_setoid
 150   | intro; constructor 1;
 151      [ apply id2
 152      | intros; apply refl1;
 153      | apply refl1]
 154   | apply convergent_relation_space_composition
 155   | intros; simplify; whd in a12 a23 a34;
 156     change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
 157     apply rule ASSOC;
 158   | intros; simplify;
 159     change with (a ∘ id2 ? o1 = a);
 160     apply (id_neutral_right2 : ?);
 161   | intros; simplify;
 162     change with (id2 ? o2 ∘ a = a);
 163     apply (id_neutral_left2 : ?);]
 164 qed.