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/connectives.ma".
  16 include "logic/equality.ma".
  17
  18 record powerset (A: Type) : Type ≝ { char: A → Prop }.
  19
  20 notation "hvbox(2 \sup A)" non associative with precedence 45
  21 for @{ 'powerset $A }.
  22
  23 interpretation "powerset" 'powerset A = (powerset A).
  24
  25 definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
  26
  27 notation "hvbox(a break ∈ b)" non associative with precedence 45
  28 for @{ 'mem $a $b }.
  29
  30 interpretation "mem" 'mem a S = (mem _ S a).
  31
  32 record axiom_set : Type ≝
  33  { A:> Type;
  34    i: A → Type;
  35    C: ∀a:A. i a → 2 \sup A
  36  }.
  37
  38 inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
  39    refl: ∀a:A. a ∈ U → covers A U a
  40  | infinity: ∀a:A. ∀j: i ? a. coversl A U (C ? a j) → covers A U a
  41 with coversl : (2 \sup A) → CProp ≝
  42    iter: ∀V:2 \sup A.(∀a:A.a ∈ V → covers A U a) → coversl A U V.
  43
  44 notation "hvbox(a break ◃ b)" non associative with precedence 45
  45 for @{ 'covers $a $b }.
  46
  47 interpretation "covers" 'covers a U = (covers _ U a).
  48 interpretation "coversl" 'covers A U = (coversl _ U A).
  49
  50 definition covers_elim ≝
  51  λA:axiom_set.λU: 2 \sup A.λP:A → CProp.
  52   λH1:∀a:A. a ∈ U → P a.
  53    λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → P b) → P a.
  54     let rec aux (a:A) (p:a ◃ U) on p : P a ≝
  55      match p return λaa.λ_:aa ◃ U.P aa with
  56       [ refl a q ⇒ H1 a q
  57       | infinity a j q ⇒ H2 a j q (auxl (C ? a j) q)
  58       ]
  59     and auxl (V: 2 \sup A) (q: V ◃ U) on q : ∀b. b ∈ V → P b ≝
  60      match q return λVV.λ_:VV ◃ U.∀b. b ∈ VV → P b with
  61       [ iter VV f ⇒ λb.λr. aux b (f b r) ]
  62     in
  63      aux.
  64
  65 coinductive fish (A:axiom_set) (U: 2 \sup A) : A → Prop ≝
  66  mk_fish: ∀a:A. (a ∈ U ∧ ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ fish A U y) → fish A U a.
  67
  68 notation "hvbox(a break ⋉ b)" non associative with precedence 45
  69 for @{ 'fish $a $b }.
  70
  71 interpretation "fish" 'fish a U = (fish _ U a).
  72
  73 let corec fish_rec (A:axiom_set) (U: 2 \sup A)
  74  (P: 2 \sup A) (H1: ∀a:A. a ∈ P → a ∈ U)
  75   (H2: ∀a:A. a ∈ P → ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ y ∈ P) :
  76    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝
  77  λa,p.
  78   mk_fish A U a
  79    (conj ? ? (H1 ? p)
  80    (λj: i ? a.
  81     match H2 a p j with
  82      [ ex_intro (y: A) (Ha: y ∈ C ? a j ∧ y ∈ P) ⇒
  83         match Ha with
  84          [ conj (fHa: y ∈ C ? a j) (sHa: y ∈ P) ⇒
  85             ex_intro A (λy.y ∈ C ? a j ∧ fish A U y) y
  86              (conj ? ? fHa (fish_rec A U P H1 H2 y sHa))
  87          ]
  88      ])).
  89
  90 theorem reflexivity: ∀A:axiom_set.∀a:A.∀V. a ∈ V → a ◃ V.
  91  intros;
  92  apply refl;
  93  assumption.
  94 qed.
  95
  96 theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
  97  intros;
  98  elim H using covers_elim;
  99   [ cases H1 in H2;
 100     intro;
 101     apply H2;
 102     assumption
 103   | apply infinity;
 104      [ assumption
 105      | constructor 1;
 106        assumption]]
 107 qed.
 108
 109 theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
 110  intros;
 111  cases H;
 112  cases H1;
 113  assumption.
 114 qed.
 115