helm/software/matita/library/demo/formal_topology.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 "logic/equality.ma".
  16 include "logic/cprop_connectives.ma".
  17
  18 record powerset (A : Type) : Type ≝ { char : A → CProp }.
  19
  20 interpretation "char" 'subset p = (mk_powerset _ p).
  21
  22 interpretation "pwset" 'powerset a = (powerset a).
  23
  24 interpretation "in" 'mem a X = (char _ X a).
  25
  26 definition subseteq ≝ λA.λu,v:\Omega \sup A.∀x.x ∈ u → x ∈ v.
  27
  28 interpretation "subseteq" 'subseteq u v = (subseteq _ u v).
  29
  30 definition overlaps ≝ λA.λU,V : Ω \sup A. exT2 ? (λx.x ∈ U) (λx.x ∈ V).
  31
  32 interpretation "overlaps" 'overlaps u v = (overlaps _ u v).
  33
  34 definition intersect ≝ λA.λu,v:Ω\sup A.{ y | y ∈ u ∧ y ∈ v }.
  35
  36 interpretation "intersect" 'intersects u v = (intersect _ u v).
  37
  38 record axiom_set : Type ≝ {
  39   A:> Type;
  40   i: A → Type;
  41   C: ∀a:A. i a → Ω \sup A
  42 }.
  43
  44 inductive for_all (A: axiom_set) (U,V: Ω \sup A) (covers: A → CProp) : CProp ≝
  45    iter: (∀a:A.a ∈ V → covers a) → for_all A U V covers.
  46
  47 inductive covers (A: axiom_set) (U: \Omega \sup A) : A → CProp ≝
  48    refl: ∀a:A. a ∈ U → covers A U a
  49  | infinity: ∀a:A. ∀j: i ? a. for_all A U (C ? a j) (covers A U) → covers A U a.
  50
  51 notation "hvbox(a break ◃ b)" non associative with precedence 45
  52 for @{ 'covers $a $b }. (* a \ltri b *)
  53
  54 interpretation "coversl" 'covers A U = (for_all _ U A (covers _ U)).
  55 interpretation "covers" 'covers a U = (covers _ U a).
  56
  57 definition covers_elim ≝
  58  λA:axiom_set.λU: \Omega \sup A.λP:\Omega \sup A.
  59   λH1: U ⊆ P.
  60    λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → C ? a j ⊆ P → a ∈ P.
  61     let rec aux (a:A) (p:a ◃ U) on p : a ∈ P ≝
  62      match p return λaa.λ_:aa ◃ U.aa ∈ P with
  63       [ refl a q ⇒ H1 a q
  64       | infinity a j q ⇒
  65          H2 a j q
  66           match q return λ_:(C ? a j) ◃ U. C ? a j ⊆ P with
  67           [ iter f ⇒ λb.λr. aux b (f b r) ]]
  68     in
  69      aux.
  70
  71 inductive ex_such (A : axiom_set) (U,V : \Omega \sup A) (fish: A → CProp) : CProp ≝
  72  found : ∀a. a ∈ V → fish a → ex_such A U V fish.
  73
  74 coinductive fish (A:axiom_set) (U: \Omega \sup A) : A → CProp ≝
  75  mk_fish: ∀a:A. a ∈ U → (∀j: i ? a. ex_such A U (C ? a j) (fish A U)) → fish A U a.
  76
  77 notation "hvbox(a break ⋉ b)" non associative with precedence 45
  78 for @{ 'fish $a $b }. (* a \ltimes b *)
  79
  80 interpretation "fishl" 'fish A U = (ex_such _ U A (fish _ U)).
  81 interpretation "fish" 'fish a U = (fish _ U a).
  82
  83 let corec fish_rec (A:axiom_set) (U: \Omega \sup A)
  84  (P: Ω \sup A) (H1: P ⊆ U)
  85   (H2: ∀a:A. a ∈ P → ∀j: i ? a. C ? a j ≬ P):
  86    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝
  87  λa,p.
  88   mk_fish A U a
  89    (H1 ? p)
  90    (λj: i ? a.
  91     match H2 a p j with
  92      [ ex_introT2 (y: A) (HyC : y ∈ C ? a j) (HyP : y ∈ P) ⇒
  93          found ???? y HyC (fish_rec A U P H1 H2 y HyP)
  94      ]).
  95
  96 theorem reflexivity: ∀A:axiom_set.∀a:A.∀V. a ∈ V → a ◃ V.
  97  intros;
  98  apply refl;
  99  assumption.
 100 qed.
 101
 102 theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
 103  intros;
 104  apply (covers_elim ?? {a | a ◃ V} ??? H); simplify; intros;
 105   [ cases H1 in H2; apply H2;
 106   | apply infinity;
 107      [ assumption
 108      | constructor 1;
 109        assumption]]
 110 qed.
 111
 112 theorem covers_elim2:
 113  ∀A: axiom_set. ∀U:Ω \sup A.∀P: A → CProp.
 114   (∀a:A. a ∈ U → P a) →
 115    (∀a:A.∀V:Ω \sup A. a ◃ V → V ◃ U → (∀y. y ∈ V → P y) → P a) →
 116      ∀a:A. a ◃ U → P a.
 117  intros;
 118  change with (a ∈ {a | P a});
 119  apply (covers_elim ?????? H2);
 120   [ intros 2; simplify; apply H; assumption
 121   | intros;
 122     simplify in H4 ⊢ %;
 123     apply H1;
 124      [ apply (C ? a1 j);
 125      | autobatch;
 126      | assumption;
 127      | assumption]]
 128 qed.
 129
 130 theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
 131  intros;
 132  cases H;
 133  assumption.
 134 qed.
 135
 136 theorem cotransitivity:
 137  ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V.
 138  intros;
 139  apply (fish_rec ?? {a|a ⋉ U} ??? H); simplify; intros;
 140   [ apply H1; apply H2;
 141   | cases H2 in j; clear H2; intro i;
 142     cases (H4 i); clear H4; exists[apply a3] assumption]
 143 qed.
 144
 145 theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
 146  intros;
 147  generalize in match H; clear H;
 148  apply (covers_elim ?? {a|a ⋉ V → U ⋉ V} ??? H1);
 149  clear H1; simplify; intros;
 150   [ exists [apply x] assumption
 151   | cases H2 in j H H1; clear H2 a1; intros;
 152     cases (H1 i); clear H1; apply (H3 a1); assumption]
 153 qed.
 154
 155 definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}.
 156
 157 interpretation "covered by one" 'leq a b = (leq _ a b).
 158
 159 theorem leq_refl: ∀A:axiom_set.∀a:A. a ≤ a.
 160  intros;
 161  apply refl;
 162  normalize;
 163  reflexivity.
 164 qed.
 165
 166 theorem leq_trans: ∀A:axiom_set.∀a,b,c:A. a ≤ b → b ≤ c → a ≤ c.
 167  intros;
 168  unfold in H H1 ⊢ %;
 169  apply (transitivity ???? H);
 170  constructor 1;
 171  intros;
 172  normalize in H2;
 173  rewrite < H2;
 174  assumption.
 175 qed.
 176
 177 definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
 178
 179 interpretation "uparrow" 'uparrow a = (uparrow _ a).
 180
 181 definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. (↑a) ≬ U).
 182
 183 interpretation "downarrow" 'downarrow a = (downarrow _ a).
 184
 185 definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
 186
 187 interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
 188
 189 record convergent_generated_topology : Type ≝
 190  { AA:> axiom_set;
 191    convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
 192  }.