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
  17 inductive And (A,B:CProp) : CProp ≝
  18  conj: A → B → And A B.
  19
  20 interpretation "constructive and" 'and x y = (And x y).
  21
  22 inductive Or (A,B:CProp) : CProp ≝
  23  | or_intro_l: A → Or A B
  24  | or_intro_r: B → Or A B.
  25
  26 interpretation "constructive or" 'or x y = (Or x y).
  27
  28 inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝
  29   ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
  30
  31 record powerset (A: Type) : Type ≝ { char: A → CProp }.
  32
  33 notation "hvbox(2 \sup A)" non associative with precedence 45
  34 for @{ 'powerset $A }.
  35
  36 interpretation "powerset" 'powerset A = (powerset A).
  37
  38 notation < "hvbox({ ident i | term 19 p })" with precedence 90
  39 for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
  40
  41 notation > "hvbox({ ident i | term 19 p })" with precedence 90
  42 for @{ 'subset (\lambda ${ident i}. $p)}.
  43
  44 interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
  45
  46 definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
  47
  48 notation "hvbox(a break ∈ b)" non associative with precedence 45
  49 for @{ 'mem $a $b }.
  50
  51 interpretation "mem" 'mem a S = (mem _ S a).
  52
  53 definition overlaps ≝ λA:Type.λU,V:2 \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
  54
  55 notation "hvbox(a break ≬ b)" non associative with precedence 45
  56 for @{ 'overlaps $a $b }. (* \between *)
  57
  58 interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
  59
  60 definition subseteq ≝ λA:Type.λU,V:2 \sup A.∀a:A. a ∈ U → a ∈ V.
  61
  62 notation "hvbox(a break ⊆ b)" non associative with precedence 45
  63 for @{ 'subseteq $a $b }. (* \subseteq *)
  64
  65 interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
  66
  67 definition intersects ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∧ a ∈ V}.
  68
  69 notation "hvbox(a break ∩ b)" non associative with precedence 55
  70 for @{ 'intersects $a $b }. (* \cap *)
  71
  72 interpretation "intersects" 'intersects U V = (intersects _ U V).
  73
  74 definition union ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∨ a ∈ V}.
  75
  76 notation "hvbox(a break ∪ b)" non associative with precedence 55
  77 for @{ 'union $a $b }. (* \cup *)
  78
  79 interpretation "union" 'union U V = (union _ U V).
  80
  81 record axiom_set : Type ≝ {
  82   A:> Type;
  83   i: A → Type;
  84   C: ∀a:A. i a → 2 \sup A
  85 }.
  86
  87 inductive for_all (A: axiom_set) (U,V: 2 \sup A) (covers: A → CProp) : CProp ≝
  88    iter: (∀a:A.a ∈ V → covers a) → for_all A U V covers.
  89
  90 inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
  91    refl: ∀a:A. a ∈ U → covers A U a
  92  | infinity: ∀a:A. ∀j: i ? a. for_all A U (C ? a j) (covers A U) → covers A U a.
  93
  94 notation "hvbox(a break ◃ b)" non associative with precedence 45
  95 for @{ 'covers $a $b }. (* a \ltri b *)
  96
  97 interpretation "coversl" 'covers A U = (for_all _ U A (covers _ U)).
  98 interpretation "covers" 'covers a U = (covers _ U a).
  99
 100 definition covers_elim ≝
 101  λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
 102   λH1:∀a:A. a ∈ U → a ∈ P.
 103    λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → C ? a j ⊆ P → a ∈ P.
 104     let rec aux (a:A) (p:a ◃ U) on p : a ∈ P ≝
 105      match p return λaa.λ_:aa ◃ U.aa ∈ P with
 106       [ refl a q ⇒ H1 a q
 107       | infinity a j q ⇒
 108          H2 a j q
 109           match q return λ_:(C ? a j) ◃ U. C ? a j ⊆ P with
 110           [ iter f ⇒ λb.λr. aux b (f b r) ]]
 111     in
 112      aux.
 113
 114 inductive ex_such (A : axiom_set) (U,V : 2 \sup A) (fish: A → CProp) : CProp ≝
 115  found : ∀a. a ∈ V → fish a → ex_such A U V fish.
 116
 117 coinductive fish (A:axiom_set) (U: 2 \sup A) : A → CProp ≝
 118  mk_fish: ∀a:A. a ∈ U → (∀j: i ? a. ex_such A U (C ? a j) (fish A U)) → fish A U a.
 119
 120 notation "hvbox(a break ⋉ b)" non associative with precedence 45
 121 for @{ 'fish $a $b }. (* a \ltimes b *)
 122
 123 interpretation "fishl" 'fish A U = (ex_such _ U A (fish _ U)).
 124 interpretation "fish" 'fish a U = (fish _ U a).
 125
 126 let corec fish_rec (A:axiom_set) (U: 2 \sup A)
 127  (P: 2 \sup A) (H1: ∀a:A. a ∈ P → a ∈ U)
 128   (H2: ∀a:A. a ∈ P → ∀j: i ? a. C ? a j ≬ P):
 129    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝
 130  λa,p.
 131   mk_fish A U a
 132    (H1 ? p)
 133    (λj: i ? a.
 134     match H2 a p j with
 135      [ ex_introT2 (y: A) (HyC : y ∈ C ? a j) (HyP : y ∈ P) ⇒
 136          found ???? y HyC (fish_rec A U P H1 H2 y HyP)
 137      ]).
 138
 139 theorem reflexivity: ∀A:axiom_set.∀a:A.∀V. a ∈ V → a ◃ V.
 140  intros;
 141  apply refl;
 142  assumption.
 143 qed.
 144
 145 theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
 146  intros;
 147  apply (covers_elim ?? {a | a ◃ V} ??? H); simplify; intros;
 148   [ cases H1 in H2; apply H2;
 149   | apply infinity;
 150      [ assumption
 151      | constructor 1;
 152        assumption]]
 153 qed.
 154
 155 theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
 156  intros;
 157  cases H;
 158  assumption.
 159 qed.
 160
 161 theorem cotransitivity:
 162  ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V.
 163  intros;
 164  apply (fish_rec ?? {a|a ⋉ U} ??? H); simplify; intros;
 165   [ apply H1; apply H2;
 166   | cases H2 in j; clear H2; intro i;
 167     cases (H4 i); clear H4; exists[apply a3] assumption]
 168 qed.
 169
 170 theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
 171  intros;
 172  generalize in match H; clear H;
 173  apply (covers_elim ?? {a|a ⋉ V → U ⋉ V} ??? H1);
 174  clear H1; simplify; intros;
 175   [ exists [apply a1] assumption
 176   | cases H2 in j H H1; clear H2 a1; intros;
 177     cases (H1 i); clear H1; apply (H3 a1); assumption]
 178 qed.
 179
 180 definition singleton ≝ λA:axiom_set.λa:A.{b | a=b}.
 181
 182 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
 183
 184 interpretation "singleton" 'singl a = (singleton _ a).
 185
 186 definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {b}.
 187
 188 interpretation "covered by one" 'leq a b = (leq _ a b).
 189
 190 theorem leq_refl: ∀A:axiom_set.∀a:A. a ≤ a.
 191  intros;
 192  apply refl;
 193  normalize;
 194  reflexivity.
 195 qed.
 196
 197 theorem leq_trans: ∀A:axiom_set.∀a,b,c:A. a ≤ b → b ≤ c → a ≤ c.
 198  intros;
 199  unfold in H H1 ⊢ %;
 200  apply (transitivity ???? H);
 201  constructor 1;
 202  intros;
 203  normalize in H2;
 204  rewrite < H2;
 205  assumption.
 206 qed.
 207
 208 definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
 209
 210 notation "↑a" with precedence 80 for @{ 'uparrow $a }.
 211
 212 interpretation "uparrow" 'uparrow a = (uparrow _ a).
 213
 214 definition downarrow ≝ λA:axiom_set.λU:2 \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
 215
 216 notation "↓a" with precedence 80 for @{ 'downarrow $a }.
 217
 218 interpretation "downarrow" 'downarrow a = (downarrow _ a).
 219
 220 definition fintersects ≝ λA:axiom_set.λU,V:2 \sup A.↓U ∩ ↓V.
 221
 222 notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }.
 223
 224 interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
 225
 226 record convergent_generated_topology : Type ≝
 227  { AA:> axiom_set;
 228    convergence: ∀a:AA.∀U,V:2 \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
 229  }.
 230