]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/nlibrary/topology/igft4.ma
Use the inversion!
[helm.git] / helm / software / matita / nlibrary / topology / igft4.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 "arithmetics/nat.ma".
16 include "datatypes/bool.ma".
17
18 ndefinition two ≝ S (S O).
19 ndefinition natone ≝ S O.
20 ndefinition four ≝ two * two.
21 ndefinition eight ≝ two * four.
22 ndefinition natS ≝ S.
23
24 include "topology/igft.ma".
25
26 nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V./2/.nqed.
27
28 ninductive Sigma (A: Type[0]) (P: A → CProp[0]) : Type[0] ≝
29  mk_Sigma: ∀a:A. P a → Sigma A P.
30
31 (*<< To be moved in igft.ma *)
32 ninductive ncover (A : nAx) (U : Ω^A) : A → CProp[0] ≝
33 | ncreflexivity : ∀a. a ∈ U → ncover A U a
34 | ncinfinity    : ∀a. ∀i. (∀y.Sigma ? (λj.y = 𝐝 a i j) → ncover A U y) → ncover A U a.
35
36 interpretation "ncovers" 'covers a U = (ncover ? U a).
37
38 ntheorem ncover_cover_ok: ∀A:nAx.∀U.∀a:A. a ◃ U → cover (Ax_of_nAx A) U a.
39  #A; #U; #a; #H; nelim H
40   [ #n; #H1; @1; nassumption
41   | #a; #i; #IH; #H; @2 [ napply i ]
42     nnormalize; #y; *; #j; #E; nrewrite > E;
43     napply H;
44     /2/ ]
45 nqed.
46
47 ntheorem cover_ncover_ok: ∀A:Ax.∀U.∀a:A. a ◃ U → ncover (nAx_of_Ax A) U a.
48  #A; #U; #a; #H; nelim H
49   [ #n; #H1; @1; nassumption
50   | #a; #i; #IH; #H; @2 [ napply i ] #y; *; #j; #E; nrewrite > E; ncases j; #x; #K;
51     napply H; nnormalize; //.
52 nqed.
53
54 ndefinition ncoverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
55
56 interpretation "ncoverage cover" 'coverage U = (ncoverage ? U).
57
58 (*>> To be moved in igft.ma *)
59
60 (*XXX
61 nlemma ncover_ind':
62  ∀A:nAx.∀U,P:Ω^A.
63    (U ⊆ P) → (∀a:A.∀i:𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j. 𝐝 a i j ∈ P) → a ∈ P) →
64     ◃ U ⊆ P.
65  #A; #U; #P; #refl; #infty; #a; #H; nelim H
66   [ // | #b; #j; #K1; #K2; napply infty; //; ##] 
67 nqed.
68
69 alias symbol "covers" (instance 3) = "ncovers".
70 nlemma cover_ind'':
71  ∀A:nAx.∀U:Ω^A.∀P:A → CProp[0].
72   (∀a. a ∈ U → P a) → (∀a:A.∀i:𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j. P (𝐝 a i j)) → P a) →
73    ∀b. b ◃ U → P b.
74  #A; #U; #P; nletin V ≝ {x | P x}; napply (ncover_ind' … V).
75 nqed.
76 *)
77
78 (*********** from Cantor **********)
79 ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
80 | refl1 : eq1 A A.
81
82 notation "hvbox( a break ∼ b)" non associative with precedence 40
83 for @{ 'eqT $a $b }.
84
85 interpretation "eq between types" 'eqT a b = (eq1 a b).
86
87 ninductive unit : Type[0] ≝ one : unit.
88
89 ninductive option (A: Type[0]) : Type[0] ≝
90    None: option A
91  | Some: A → option A
92  | Twice: A → A → option A.
93
94 nrecord uuAx : Type[1] ≝ {
95   uuS : Type[0];
96   uuC : uuS → option uuS
97 }.
98
99 ndefinition uuax : uuAx → nAx.
100 #A; @ (uuS A)
101   [ #a; napply unit
102 ##| #a; ncases (uuC … a); nnormalize
103      [ #_; napply False
104      | #_; #_; napply unit
105      | #_; #_; #_; napply bool ]
106 ##| #a; ncases (uuC … a); nnormalize
107      [ #_; #H; napply (False_rect_Type1 … H)
108      | #b; #_; #_; napply b
109      | #b1; #b2; #_; * [ napply b1 | napply b2]##]##]
110 nqed.
111
112 ncoercion uuax : ∀u:uuAx. nAx ≝ uuax on _u : uuAx to nAx.
113
114 nlemma eq_rect_Type0_r':
115  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
116  #A; #a; #x; #p; ncases p; //;
117 nqed.
118
119 nlemma eq_rect_Type0_r:
120  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
121  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); //.
122 nqed.
123
124 nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
125  { decide_mem:> A → bool;
126    decide_mem_ok: ∀x. decide_mem x = true → x ∈ U;
127    decide_mem_ko: ∀x. decide_mem x = false → ¬ (x ∈ U)
128  }.
129
130 (*********** end from Cantor ********)
131
132 nlemma csc_sym_eq: ∀A,x,y. eq A x y → eq A y x.
133  #A; #x; #y; #H; ncases H; @1.
134 nqed.
135
136 nlemma csc_eq_rect_CProp0_r':
137  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. CProp[0]. P a → P x.
138  #A; #a; #x; #p; #P; #H;
139  napply (match csc_sym_eq ??? p return λa.λ_.P a with [ refl ⇒ H ]).
140 nqed.
141  
142 nlet rec cover_rect
143  (A:uuAx) (U:Ω^(uuax A)) (memdec: memdec … U) (P:uuax A → Type[0])
144   (refl: ∀a:uuax A. a ∈ U → P a)
145   (infty: ∀a:uuax A.∀i: 𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j.P (𝐝 a i j)) → P a)
146    (b:uuax A) (p: b ◃ U) on p : P b
147 ≝ ?.
148  nlapply (decide_mem_ok … memdec b); nlapply (decide_mem_ko … memdec b);
149  ncases (decide_mem … memdec b)
150   [ #_; #H; napply refl; /2/
151   | #H; #_; ncut (uuC … b=uuC … b) [//] ncases (uuC … b) in ⊢ (???% → ?)
152     [ #E;
153       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
154       napply (H2 one); #y; nelim y
155   ##| #a; #E;
156       ncut (a ◃ U)
157        [ nlapply E; nlapply (H ?); //; ncases p
158           [ #x; #Hx; #K1; #_; ncases (K1 Hx)  
159         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
160             nrewrite > E2; nnormalize; /2/ ]##]
161       #Hcut;
162       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
163       napply (H2 one); #y
164        [ napply Hcut
165      ##| napply (cover_rect A U memdec P refl infty a); // ]
166   ##| #a; #a1; #E;
167       ncut (a ◃ U)
168        [ nlapply E; nlapply (H ?) [//] ncases p
169           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
170         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
171             nrewrite > E2; nnormalize; #_; @1 (true); /2/ ]##]
172       #Hcut;
173       ncut (a1 ◃ U)
174        [ nlapply E; nlapply (H ?) [//] ncases p
175           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
176         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
177             nrewrite > E2; nnormalize; #_; @1 (false); /2/ ]##]
178       #Hcut1;
179       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
180       napply (H2 one); #y; ncases y; nnormalize
181        [##1,2: nassumption
182        | napply (cover_rect A U memdec P refl infty a); //
183        | napply (cover_rect A U memdec P refl infty a1); //]
184 nqed.
185
186 (********* Esempio:
187    let rec skip n =
188      match n with
189       [ O ⇒ 1
190       | S m ⇒
191          match m with
192           [ O ⇒ skipfact O
193           | S _ ⇒ S m * skipfact (pred m) * skipfact (pred m) ]]
194 **)
195
196 ntheorem psym_plus: ∀n,m. n + m = m + n.//.
197 nqed.
198
199 nlemma easy1: ∀n:nat. two * (S n) = two + two * n.//.
200 nqed.
201
202 ndefinition skipfact_dom: uuAx.
203  @ nat; #n; ncases n [ napply None | #m; ncases m [ napply (Some … O) | #_; napply (Twice … (pred m) (pred m)) ]
204 nqed.
205
206 ntheorem skipfact_base_dec:
207  memdec (uuax skipfact_dom) (mk_powerclass ? (λx: uuax skipfact_dom. False)).
208  nnormalize; @ (λ_.false); //. #_; #H; ndestruct.
209 nqed.
210
211 ntheorem skipfact_partial:
212  ∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.False).
213  #n; nelim n
214   [ @2; nnormalize; //; #y; *; #a; ncases a
215   |
216  #m; nelim m; nnormalize
217      [ #H; @2; nnormalize; //;
218        #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; //
219    ##| #p; #H1; #H2; @2; nnormalize; //;
220        #y; *; #a; #E; nrewrite > E; ncases a; nnormalize;
221        nrewrite < (plus_n_Sm …); // ]
222 nqed.
223
224 ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.False) → nat.
225  #n; #D; napply (cover_rect … skipfact_base_dec … n D)
226   [ #a; #H; nelim H
227   | #a; ncases a
228     [ nnormalize; #i; #_; #_; napply natone
229     | #m; ncases m
230        [ nnormalize; #_; #_; #H; napply H; @1
231        | #p; #i; nnormalize in i; #K;
232          #H; nnormalize in H;
233          napply (S m * H true * H false) ]
234 nqed.
235
236 nlemma test: skipfact four ? = four * two * two. ##[##2: napply (skipfact_partial two)]//.
237 nqed.