1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "arithmetics/nat.ma".
16 include "datatypes/bool.ma".
18 ndefinition two ≝ S (S O).
19 ndefinition natone ≝ S O.
20 ndefinition four ≝ two * two.
21 ndefinition eight ≝ two * four.
24 include "topology/igft.ma".
26 nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
30 ninductive Sigma (A: Type[0]) (P: A → CProp[0]) : Type[0] ≝
31 mk_Sigma: ∀a:A. P a → Sigma A P.
33 (*<< To be moved in igft.ma *)
34 ninductive ncover (A : nAx) (U : Ω^A) : A → CProp[0] ≝
35 | ncreflexivity : ∀a. a ∈ U → ncover A U a
36 | ncinfinity : ∀a. ∀i. (∀y.Sigma ? (λj.y = 𝐝 a i j) → ncover A U y) → ncover A U a.
38 interpretation "ncovers" 'covers a U = (ncover ? U a).
40 ntheorem ncover_cover_ok: ∀A:nAx.∀U.∀a:A. a ◃ U → cover (Ax_of_nAx A) U a.
41 #A; #U; #a; #H; nelim H
42 [ #n; #H1; @1; nassumption
43 | #a; #i; #IH; #H; @2 [ napply i ]
44 nnormalize; #y; *; #j; #E; nrewrite > E;
49 ntheorem cover_ncover_ok: ∀A:Ax.∀U.∀a:A. a ◃ U → ncover (nAx_of_Ax A) U a.
50 #A; #U; #a; #H; nelim H
51 [ #n; #H1; @1; nassumption
52 | #a; #i; #IH; #H; @2 [ napply i ] #y; *; #j; #E; nrewrite > E; ncases j; #x; #K;
53 napply H; nnormalize; nassumption.
56 ndefinition ncoverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
58 interpretation "ncoverage cover" 'coverage U = (ncoverage ? U).
60 (*>> To be moved in igft.ma *)
65 (U ⊆ P) → (∀a:A.∀i:𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j. 𝐝 a i j ∈ P) → a ∈ P) →
67 #A; #U; #P; #refl; #infty; #a; #H; nelim H
68 [ nauto | (*nauto depth=4;*) #b; #j; #K1; #K2;
69 napply infty; nauto; ##]
72 alias symbol "covers" (instance 3) = "ncovers".
74 ∀A:nAx.∀U:Ω^A.∀P:A → CProp[0].
75 (∀a. a ∈ U → P a) → (∀a:A.∀i:𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j. P (𝐝 a i j)) → P a) →
77 #A; #U; #P; nletin V ≝ {x | P x}; napply (ncover_ind' … V).
81 (*********** from Cantor **********)
82 ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
85 notation "hvbox( a break ∼ b)" non associative with precedence 40
88 interpretation "eq between types" 'eqT a b = (eq1 a b).
90 ninductive unit : Type[0] ≝ one : unit.
92 ninductive option (A: Type[0]) : Type[0] ≝
95 | Twice: A → A → option A.
97 nrecord uuAx : Type[1] ≝ {
99 uuC : uuS → option uuS
102 ndefinition uuax : uuAx → nAx.
104 [ #a; ncases (uuC … a) [ napply False | #_; napply unit | #_; #_; napply unit]
105 ##| #a; ncases (uuC … a); nnormalize
106 [ #H; napply (False_rect_Type1 … H)
107 | #_; #_; napply unit
108 | #_; #_; #_; napply bool ]
109 ##| #a; ncases (uuC … a); nnormalize
110 [ #H; napply (False_rect_Type1 … H)
111 | #b; #_; #_; napply b
112 | #b1; #b2; #_; * [ napply b1 | napply b2]##]##]
115 ncoercion uuax : ∀u:uuAx. nAx ≝ uuax on _u : uuAx to nAx.
117 nlemma eq_rect_Type0_r':
118 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
119 #A; #a; #x; #p; ncases p; nauto;
122 nlemma eq_rect_Type0_r:
123 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
124 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
127 nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
128 { decide_mem:> A → bool;
129 decide_mem_ok: ∀x. decide_mem x = true → x ∈ U;
130 decide_mem_ko: ∀x. decide_mem x = false → ¬ (x ∈ U)
133 (*********** end from Cantor ********)
135 nlemma csc_sym_eq: ∀A,x,y. eq A x y → eq A y x.
136 #A; #x; #y; #H; ncases H; @1.
139 nlemma csc_eq_rect_CProp0_r':
140 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. CProp[0]. P a → P x.
141 #A; #a; #x; #p; #P; #H;
142 napply (match csc_sym_eq ??? p return λa.λ_.P a with [ refl ⇒ H ]).
146 (A:uuAx) (U:Ω^(uuax A)) (memdec: memdec … U) (P:uuax A → Type[0])
147 (refl: ∀a:uuax A. a ∈ U → P a)
148 (infty: ∀a:uuax A.∀i: 𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j.P (𝐝 a i j)) → P a)
149 (b:uuax A) (p: b ◃ U) on p : P b
151 nlapply (decide_mem_ok … memdec b); nlapply (decide_mem_ko … memdec b);
152 ncases (decide_mem … memdec b)
153 [ #_; #H; napply refl; nauto
154 | #H; #_; ncut (uuC … b=uuC … b) [nauto] ncases (uuC … b) in ⊢ (???% → ?)
155 [ #E; napply False_rect_Type0; ncut (b=b) [nauto] ncases p in ⊢ (???% → ?)
156 [ #a; #K; #E2; napply H [ nauto | nrewrite > E2; nauto ]
157 ##| #a; #i; #K; #E2; nrewrite < E2 in i; nnormalize; nrewrite > E; nnormalize;
161 [ nlapply E; nlapply (H ?) [nauto] ncases p
162 [ #x; #Hx; #K1; #_; ncases (K1 Hx)
163 ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
164 nrewrite > E2; nnormalize; /2/ ]##]
166 nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
169 ##| napply (cover_rect A U memdec P refl infty a); nauto ]
172 [ nlapply E; nlapply (H ?) [nauto] ncases p
173 [ #x; #Hx; #K1; #_; ncases (K1 Hx)
174 ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
175 nrewrite > E2; nnormalize; #_; @1 (true); /2/ ]##]
178 [ nlapply E; nlapply (H ?) [nauto] ncases p
179 [ #x; #Hx; #K1; #_; ncases (K1 Hx)
180 ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
181 nrewrite > E2; nnormalize; #_; @1 (false); /2/ ]##]
183 nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
184 napply (H2 one); #y; ncases y; nnormalize
186 | napply (cover_rect A U memdec P refl infty a); nauto
187 | napply (cover_rect A U memdec P refl infty a1); nauto]
197 | S _ ⇒ S m * skipfact (pred m) * skipfact O ]]
200 ntheorem psym_plus: ∀n,m. n + m = m + n.
202 [ #m; nelim m; //; #n0; #H;
203 nchange with (natS n0 = natS (n0 + O));
205 | #n0; #H; #m; nchange with (S (n0 + m) = m + S n0);
208 #n1; #E; nrewrite > E; //]
211 nlemma easy1: ∀n:nat. two * (S n) = two + two * n.
214 nrewrite > (psym_plus ??);
215 nrewrite > H; nnormalize;
216 nrewrite > (psym_plus ??);
220 ndefinition skipfact_dom: uuAx.
221 @ nat; #n; ncases n [ napply None | #m; ncases m [ napply (Some … O) | #_; napply (Twice … (pred m) O) ]
224 ntheorem skipfact_base_dec:
225 memdec (uuax skipfact_dom) (mk_powerclass ? (λx: uuax skipfact_dom. x=O)).
226 nnormalize; @ (λx. match x with [ O ⇒ true | S _ ⇒ false ]); #n; nelim n;
227 nnormalize; //; #X; ndestruct; #Y; #Z; ndestruct; #W; ndestruct.
230 ntheorem skipfact_partial:
231 ∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O).
234 | #m; nelim m; nnormalize
237 | #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; // ]
238 ##| #p; #H1; #H2; @2; nnormalize
240 | #y; *; #a; #E; nrewrite > E; ncases a; nnormalize
241 [ nrewrite < (plus_n_Sm …); //
245 ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.
246 #n; #D; napply (cover_rect … skipfact_base_dec … n D)
247 [ #a; #_; napply natone
249 [ nnormalize; #i; nelim i
251 [ nnormalize; #_; #_; #H; napply H; @1
252 | #p; #i; nnormalize in i; #K;
254 napply (S m * H true * H false) ]
257 nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)]