helm/software/matita/nlibrary/topology/igft2.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 "topology/igft.ma".
  16
  17 nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
  18 nnormalize; nauto;
  19 nqed.
  20
  21 alias symbol "covers" = "covers set".
  22 alias symbol "coverage" = "coverage cover".
  23 alias symbol "I" = "I".
  24 nlemma cover_ind':
  25  ∀A:Ax.∀U,P:Ω^A.
  26    (U ⊆ P) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → 𝐂 a j ⊆ P → a ∈ P) →
  27     ◃ U ⊆ P.
  28  #A; #U; #P; #refl; #infty; #a; #H; nelim H
  29   [ nauto | (*nauto depth=4;*) #b; #j; #K1; #K2;
  30             napply infty; nauto; ##]
  31 nqed.
  32
  33 alias symbol "covers" (instance 1) = "covers".
  34 nlemma cover_ind'':
  35  ∀A:Ax.∀U:Ω^A.∀P:A → CProp[0].
  36   (∀a. a ∈ U → P a) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → (∀b. b ∈ 𝐂 a j → P b) → P a) →
  37    ∀b. b ◃ U → P b.
  38  #A; #U; #P; nletin V ≝ {x | P x}; napply (cover_ind' … V).
  39 nqed.
  40
  41 (*********** from Cantor **********)
  42 ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
  43 | refl1 : eq1 A A.
  44
  45 notation "hvbox( a break ∼ b)" non associative with precedence 40
  46 for @{ 'eqT $a $b }.
  47
  48 interpretation "eq between types" 'eqT a b = (eq1 a b).
  49
  50 ninductive unit : Type[0] ≝ one : unit.
  51
  52 ninductive option (A: Type[0]) : Type[0] ≝
  53    None: option A
  54  | Some: A → option A.
  55
  56 nrecord uuAx : Type[1] ≝ {
  57   uuS : Type[0];
  58   uuC : uuS → option uuS
  59 }.
  60
  61 ndefinition uuax : uuAx → Ax.
  62 #A; @ (uuS A)
  63   [ #a; ncases (uuC … a) [ napply False | #_; napply unit]
  64 ##| #a; ncases (uuC … a)
  65      [ nnormalize; #H; napply (False_rect_Type1 … H)
  66      | nnormalize; #b; #_; napply {x | x=b }]##]
  67 nqed.
  68
  69 ncoercion uuax : ∀u:uuAx. Ax ≝ uuax on _u : uuAx to Ax.
  70
  71 nlemma eq_rect_Type0_r':
  72  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
  73  #A; #a; #x; #p; ncases p; nauto;
  74 nqed.
  75
  76 nlemma eq_rect_Type0_r:
  77  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  78  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
  79 nqed.
  80
  81 ninductive bool: Type[0] ≝
  82    true: bool
  83  | false: bool.
  84
  85 nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
  86  { decide_mem:> A → bool;
  87    decide_mem_ok: ∀x. decide_mem x = true → x ∈ U;
  88    decide_mem_ko: ∀x. decide_mem x = false → ¬ (x ∈ U)
  89  }.
  90
  91 (*********** end from Cantor ********)
  92
  93 alias symbol "covers" (instance 9) = "covers".
  94 alias symbol "covers" (instance 8) = "covers".
  95 nlet rec cover_rect
  96  (A:uuAx) (U:Ω^(uuax A)) (memdec: memdec … U) (P:uuax A → Type[0])
  97   (refl: ∀a:uuax A. a ∈ U → P a)
  98   (infty: ∀a:uuax A.∀i: 𝐈 a. 𝐂 a i ◃ U → (∀b. b ∈ 𝐂 a i → P b) → P a)
  99    (b:uuax A) (p: b ◃ U) on p : P b
 100 ≝ ?.
 101  nlapply (decide_mem_ok … memdec b); nlapply (decide_mem_ko … memdec b);
 102  ncases (decide_mem … memdec b)
 103   [ #_; #H; napply refl; nauto
 104   | #H; #_; ncut (uuC … b=uuC … b) [nauto] ncases (uuC … b) in ⊢ (???% → ?)
 105     [ #E; napply False_rect_Type0; ncut (b=b) [nauto] ncases p in ⊢ (???% → ?)
 106       [ #a; #K; #E2; napply H [ nauto | nrewrite > E2; nauto ]
 107     ##| #a; #i; #K; #E2; nrewrite < E2 in i; nnormalize; nrewrite > E; nnormalize;
 108         nauto]
 109   ##| #a; #E;
 110       ncut (a ◃ U)
 111        [ nlapply E; nlapply (H ?) [nauto] ncases p
 112           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
 113         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
 114             nrewrite > E2; nnormalize; #_; nauto]##]
 115       #Hcut;
 116       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
 117       napply (H2 one); #y; #E2; nrewrite > E2
 118       (* [##2: napply cover_rect] nauto depth=1; *)
 119        [ napply Hcut
 120      ##| napply (cover_rect A U memdec P refl infty a); nauto ]##]
 121 nqed.