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