]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/nlibrary/topology/igft2.ma
Use the inversion!
[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 "arithmetics/nat.ma".
16
17 ndefinition two ≝ S (S O).
18 ndefinition natone ≝ S O.
19 ndefinition four ≝ two * two.
20 ndefinition eight ≝ two * four.
21 ndefinition natS ≝ S.
22
23 include "topology/igft.ma".
24
25 nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
26 nnormalize; /2/;
27 nqed.
28
29 alias symbol "covers" = "covers set".
30 alias symbol "coverage" = "coverage cover".
31 alias symbol "I" = "I".
32 nlemma cover_ind':
33  ∀A:Ax.∀U,P:Ω^A.
34    (U ⊆ P) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → 𝐂 a j ⊆ P → a ∈ P) →
35     ◃ U ⊆ P.
36  #A; #U; #P; #refl; #infty; #a; #H; nelim H; /3/. 
37 nqed.
38
39 alias symbol "covers" (instance 1) = "covers".
40 nlemma cover_ind'':
41  ∀A:Ax.∀U:Ω^A.∀P:A → CProp[0].
42   (∀a. a ∈ U → P a) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → (∀b. b ∈ 𝐂 a j → P b) → P a) →
43    ∀b. b ◃ U → P b.
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; //;
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" (instance 9) = "covers".
100 alias symbol "covers" (instance 8) = "covers".
101 nlet rec cover_rect
102  (A:uuAx) (U:Ω^(uuax A)) (memdec: memdec … U) (P:uuax A → Type[0])
103   (refl: ∀a:uuax A. a ∈ U → P a)
104   (infty: ∀a:uuax A.∀i: 𝐈 a. 𝐂 a i ◃ U → (∀b. b ∈ 𝐂 a i → P b) → P a)
105    (b:uuax A) (p: b ◃ U) on p : P b
106 ≝ ?.
107  nlapply (decide_mem_ok … memdec b); nlapply (decide_mem_ko … memdec b);
108  ncases (decide_mem … memdec b)
109   [ #_; #H; napply refl; /2/
110   | #H; #_; ncut (uuC … b=uuC … b) [//] ncases (uuC … b) in ⊢ (???% → ?)
111     [ #E; napply False_rect_Type0; ncut (b=b) [//] ncases p in ⊢ (???% → ?)
112       [ #a; #K; #E2; napply H [ // | nrewrite > E2; // ]
113     ##| #a; #i; #K; #E2; nrewrite < E2 in i; nnormalize; nrewrite > E; nnormalize;
114         //]
115   ##| #a; #E;
116       ncut (a ◃ U)
117        [ nlapply E; nlapply (H ?) [//] ncases p
118           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
119         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
120             nrewrite > E2; nnormalize; #_; //]##]
121       #Hcut; 
122       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
123       napply (H2 one); #y; #E2; nrewrite > E2 
124       (* [##2: napply cover_rect] //; *)
125        [ napply Hcut
126      ##| napply (cover_rect A U memdec P refl infty a); // ]##]
127 nqed.
128
129 (********* Esempio:
130    let rec skipfact n =
131      match n with
132       [ O ⇒ 1
133       | S m ⇒ S m * skipfact (pred m) ]
134 **)
135
136 ntheorem psym_plus: ∀n,m. n + m = m + n.//.
137 nqed.
138
139 nlemma easy1: ∀n:nat. two * (S n) = two + two * n.//.
140 nqed.
141
142 ndefinition skipfact_dom: uuAx.
143  @ nat; #n; ncases n [ napply None | #m; napply (Some … (pred m)) ]
144 nqed.
145
146 ntheorem skipfact_base_dec:
147  memdec (uuax skipfact_dom) (mk_powerclass ? (λx: uuax skipfact_dom. x=O)).
148  nnormalize; @ (λx. match x with [ O ⇒ true | S _ ⇒ false ]); #n; nelim n;
149   nnormalize; //; #X; ndestruct; #Y; #Z; ndestruct; #W; ndestruct.
150 nqed.
151
152 ntheorem skipfact_partial:
153  ∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O).
154  #n; nelim n
155   [ @1; nnormalize; @1
156   | #m; #H; @2
157      [ nnormalize; @1
158      | nnormalize; #y; nchange in ⊢ (% → ?) with (y = pred (pred (two * (natone + m))));
159        nnormalize; nrewrite < (plus_n_Sm …); nnormalize;
160        #E; nrewrite > E; napply H ]##]
161 nqed.
162
163 ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.
164  #n; #D; napply (cover_rect … skipfact_base_dec … n D)
165   [ #a; #_; napply natone
166   | #a; ncases a
167     [ nnormalize; #i; nelim i
168     | #m; #i; nnormalize in i; #d; #H;
169       napply (S m * H (pred m) …); //]
170 nqed.
171
172 nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)] //.
173 nqed.