helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.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 "notation.ma".
  16 include "o-basic_pairs.ma".
  17 include "o-basic_topologies.ma".
  18
  19 alias symbol "eq" = "setoid1 eq".
  20
  21 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
  22 definition o_basic_topology_of_o_basic_pair: OBP → OBTop.
  23  intro t;
  24  constructor 1;
  25   [ apply (Oform t);
  26   | apply (□⎽t ∘ Ext⎽t);
  27   | apply (◊⎽t ∘ Rest⎽t);
  28   | apply hide; intros 2; split; intro;
  29      [ change with ((⊩) \sup ⎻* ((⊩) \sup ⎻ U) ≤ (⊩) \sup ⎻* ((⊩) \sup ⎻ V));
  30        apply (. (#‡(lemma_10_4_a ?? (⊩) V)^-1));
  31        apply f_minus_star_image_monotone;
  32        apply f_minus_image_monotone;
  33        assumption
  34      | apply oa_leq_trans;
  35         [3: apply f;
  36         | skip
  37         | change with (U ≤ (⊩)⎻* ((⊩)⎻ U));
  38           apply (. (or_prop2 : ?) ^ -1);
  39           apply oa_leq_refl; ]]
  40   | apply hide; intros 2; split; intro;
  41      [ change with (◊⎽t ((⊩) \sup * U) ≤ ◊⎽t ((⊩) \sup * V));
  42        apply (. ((lemma_10_4_b ?? (⊩) U)^-1)‡#);
  43        apply (f_image_monotone ?? (⊩) ? ((⊩)* V));
  44        apply f_star_image_monotone;
  45        assumption;
  46      | apply oa_leq_trans;
  47         [2: apply f;
  48         | skip
  49         | change with ((⊩) ((⊩)* V) ≤ V);
  50           apply (. (or_prop1 : ?));
  51           apply oa_leq_refl; ]]
  52   | apply hide; intros;
  53     apply (.= (oa_overlap_sym' : ?));
  54     change with ((◊⎽t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊⎽t ((⊩)* V))));
  55     apply (.= (or_prop3 ?? (⊩) ((⊩)* V) ?));
  56     apply (.= #‡(lemma_10_3_a : ?));
  57     apply (.= (or_prop3 : ?)^-1);
  58     apply (oa_overlap_sym' ? ((⊩) ((⊩)* V)) U); ]
  59 qed.
  60
  61 definition o_continuous_relation_of_o_relation_pair:
  62  ∀BP1,BP2.arrows2 OBP BP1 BP2 →
  63   arrows2 OBTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
  64  intros (BP1 BP2 t);
  65  constructor 1;
  66   [ apply (t \sub \f);
  67   | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
  68     apply sym1;
  69     apply (.= †(†e));
  70     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
  71     cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
  72       cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩)* U));]
  73     apply (.= †COM);
  74     change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
  75     apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
  76     apply (.= COM ^ -1);
  77     change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
  78     change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
  79     apply (†e^-1);
  80   | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
  81     apply sym1;
  82     apply (.= †(†e));
  83     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
  84     cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
  85       cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
  86     apply (.= †COM);
  87     change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
  88     apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
  89     apply (.= COM ^ -1);
  90     change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
  91     change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
  92     apply (†e^-1);]
  93 qed.
  94
  95
  96 definition OR : carr3 (arrows3 CAT2 OBP OBTop).
  97 constructor 1;
  98 [ apply o_basic_topology_of_o_basic_pair;
  99 | intros; constructor 1;
 100   [ apply o_continuous_relation_of_o_relation_pair;
 101   | apply hide;
 102     intros; whd; unfold o_continuous_relation_of_o_relation_pair; simplify;;
 103     change with ((a \sub \f ⎻* ∘ oA (o_basic_topology_of_o_basic_pair S)) =
 104                  (a' \sub \f ⎻*∘ oA (o_basic_topology_of_o_basic_pair S)));
 105     whd in e; cases e; clear e e2 e3 e4;
 106     change in ⊢ (? ? ? (? ? ? ? ? % ?) ?) with ((⊩\sub S)⎻* ∘ (⊩\sub S)⎻);
 107     apply (.= (comp_assoc2 ? ???? ?? a\sub\f⎻* ));
 108     change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a\sub\f ∘ ⊩\sub S)⎻*;
 109     apply (.= #‡†(Ocommute:?)^-1);
 110     apply (.= #‡e1);
 111     change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (⊩\sub T ∘ a'\sub\c)⎻*;
 112     apply (.= #‡†(Ocommute:?));
 113     change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a'\sub\f⎻* ∘ (⊩\sub S)⎻* );
 114     apply (.= (comp_assoc2 ? ???? ?? a'\sub\f⎻* )^-1);
 115     apply refl2;]
 116 | intros 2 (o a); apply refl1;
 117 | intros 6; apply refl1;]
 118 qed.
 119