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 "o-basic_pairs.ma".
  16 include "o-basic_topologies.ma".
  17
  18 alias symbol "eq" = "setoid1 eq".
  19
  20 (* qui la notazione non va *)
  21 lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = (binary_join ? p q).
  22  intros;
  23  apply oa_leq_antisym;
  24   [ apply oa_density; intros;
  25     apply oa_overlap_sym;
  26     unfold binary_join; simplify;
  27     apply (. (oa_join_split : ?));
  28     exists; [ apply false ]
  29     apply oa_overlap_sym;
  30     assumption
  31   | unfold binary_join; simplify;
  32     apply (. (oa_join_sup : ?)); intro;
  33     cases i; whd in ⊢ (? ? ? ? ? % ?);
  34      [ assumption | apply oa_leq_refl ]]
  35 qed.
  36
  37 lemma overlap_monotone_left: ∀S:OA.∀p,q,r:S. p ≤ q → p >< r → q >< r.
  38  intros;
  39  apply (. (leq_to_eq_join : ?)‡#);
  40   [ apply f;
  41   | skip
  42   | apply oa_overlap_sym;
  43     unfold binary_join; simplify;
  44     apply (. (oa_join_split : ?));
  45     exists [ apply true ]
  46     apply oa_overlap_sym;
  47     assumption; ]
  48 qed.
  49
  50 (* Part of proposition 9.9 *)
  51 lemma f_minus_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R⎻ p ≤ R⎻ q.
  52  intros;
  53  apply (. (or_prop2 : ?));
  54  apply oa_leq_trans; [2: apply f; | skip | apply (. (or_prop2 : ?)^ -1); apply oa_leq_refl;]
  55 qed.
  56
  57 (* Part of proposition 9.9 *)
  58 lemma f_minus_star_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R⎻* p ≤ R⎻* q.
  59  intros;
  60  apply (. (or_prop2 : ?)^ -1);
  61  apply oa_leq_trans; [3: apply f; | skip | apply (. (or_prop2 : ?)); apply oa_leq_refl;]
  62 qed.
  63
  64 (* Part of proposition 9.9 *)
  65 lemma f_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R p ≤ R q.
  66  intros;
  67  apply (. (or_prop1 : ?));
  68  apply oa_leq_trans; [2: apply f; | skip | apply (. (or_prop1 : ?)^ -1); apply oa_leq_refl;]
  69 qed.
  70
  71 (* Part of proposition 9.9 *)
  72 lemma f_star_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R* p ≤ R* q.
  73  intros;
  74  apply (. (or_prop1 : ?)^ -1);
  75  apply oa_leq_trans; [3: apply f; | skip | apply (. (or_prop1 : ?)); apply oa_leq_refl;]
  76 qed.
  77
  78 lemma lemma_10_2_a: ∀S,T.∀R:arrows2 OA S T.∀p. p ≤ R⎻* (R⎻ p).
  79  intros;
  80  apply (. (or_prop2 : ?)^-1);
  81  apply oa_leq_refl.
  82 qed.
  83
  84 lemma lemma_10_2_b: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* p) ≤ p.
  85  intros;
  86  apply (. (or_prop2 : ?));
  87  apply oa_leq_refl.
  88 qed.
  89
  90 lemma lemma_10_2_c: ∀S,T.∀R:arrows2 OA S T.∀p. p ≤ R* (R p).
  91  intros;
  92  apply (. (or_prop1 : ?)^-1);
  93  apply oa_leq_refl.
  94 qed.
  95
  96 lemma lemma_10_2_d: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* p) ≤ p.
  97  intros;
  98  apply (. (or_prop1 : ?));
  99  apply oa_leq_refl.
 100 qed.
 101
 102 lemma lemma_10_3_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* (R⎻ p)) = R⎻ p.
 103  intros; apply oa_leq_antisym;
 104   [ apply lemma_10_2_b;
 105   | apply f_minus_image_monotone;
 106     apply lemma_10_2_a; ]
 107 qed.
 108
 109 lemma lemma_10_3_b: ∀S,T.∀R:arrows2 OA S T.∀p. R* (R (R* p)) = R* p.
 110  intros; apply oa_leq_antisym;
 111   [ apply f_star_image_monotone;
 112     apply (lemma_10_2_d ?? R p);
 113   | apply lemma_10_2_c; ]
 114 qed.
 115
 116 lemma lemma_10_3_c: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R p)) = R p.
 117  intros; apply oa_leq_antisym;
 118   [ apply lemma_10_2_d;
 119   | apply f_image_monotone;
 120     apply (lemma_10_2_c ?? R p); ]
 121 qed.
 122
 123 lemma lemma_10_3_d: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
 124  intros; apply oa_leq_antisym;
 125   [ apply f_minus_star_image_monotone;
 126     apply (lemma_10_2_b ?? R p);
 127   | apply lemma_10_2_a; ]
 128 qed.
 129
 130 lemma lemma_10_4_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
 131  intros; apply (†(lemma_10_3_a ?? R p));
 132 qed.
 133
 134 lemma lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
 135 intros; apply (†(lemma_10_3_b ?? R p));
 136 qed.
 137
 138 lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
 139  intros; split; intro; apply oa_overlap_sym; assumption.
 140 qed.
 141
 142 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
 143 definition o_basic_topology_of_o_basic_pair: BP → BTop.
 144  intro t;
 145  constructor 1;
 146   [ apply (form t);
 147   | apply (□_t ∘ Ext⎽t);
 148   | apply (◊_t ∘ Rest⎽t);
 149   | intros 2; split; intro;
 150      [ change with ((⊩) \sup ⎻* ((⊩) \sup ⎻ U) ≤ (⊩) \sup ⎻* ((⊩) \sup ⎻ V));
 151        apply (. (#‡(lemma_10_4_a ?? (⊩) V)^-1));
 152        apply f_minus_star_image_monotone;
 153        apply f_minus_image_monotone;
 154        assumption
 155      | apply oa_leq_trans;
 156         [3: apply f;
 157         | skip
 158         | change with (U ≤ (⊩)⎻* ((⊩)⎻ U));
 159           apply (. (or_prop2 : ?) ^ -1);
 160           apply oa_leq_refl; ]]
 161   | intros 2; split; intro;
 162      [ change with (◊_t ((⊩) \sup * U) ≤ ◊_t ((⊩) \sup * V));
 163        apply (. ((lemma_10_4_b ?? (⊩) U)^-1)‡#);
 164        apply (f_image_monotone ?? (⊩) ? ((⊩)* V));
 165        apply f_star_image_monotone;
 166        assumption;
 167      | apply oa_leq_trans;
 168         [2: apply f;
 169         | skip
 170         | change with ((⊩) ((⊩)* V) ≤ V);
 171           apply (. (or_prop1 : ?));
 172           apply oa_leq_refl; ]]
 173   | intros;
 174     apply (.= (oa_overlap_sym' : ?));
 175     change with ((◊_t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊_t ((⊩)* V))));
 176     apply (.= (or_prop3 ?? (⊩) ((⊩)* V) ?));
 177     apply (.= #‡(lemma_10_3_a : ?));
 178     apply (.= (or_prop3 : ?)^-1);
 179     apply (oa_overlap_sym' ? ((⊩) ((⊩)* V)) U); ]
 180 qed.
 181
 182 definition o_continuous_relation_of_o_relation_pair:
 183  ∀BP1,BP2.arrows2 BP BP1 BP2 →
 184   arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
 185  intros (BP1 BP2 t);
 186  constructor 1;
 187   [ apply (t \sub \f);
 188   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
 189     apply sym1;
 190     apply (.= †(†e));
 191     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
 192     cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
 193       cases (commute ?? t); apply (e3 ^ -1 ((⊩)* U));]
 194     apply (.= †COM);
 195     change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
 196     apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
 197     apply (.= COM ^ -1);
 198     change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
 199     change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
 200     apply (†e^-1);
 201   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
 202     apply sym1;
 203     apply (.= †(†e));
 204     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
 205     cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
 206       cases (commute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
 207     apply (.= †COM);
 208     change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
 209     apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
 210     apply (.= COM ^ -1);
 211     change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
 212     change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
 213     apply (†e^-1);]
 214 qed.