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".
17 ndefinition two ≝ S (S O).
18 ndefinition natone ≝ S O.
19 ndefinition four ≝ two * two.
20 ndefinition eight ≝ two * four.
23 include "topology/igft.ma".
25 nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
29 alias symbol "covers" = "covers set".
30 alias symbol "coverage" = "coverage cover".
31 alias symbol "I" = "I".
34 (U ⊆ P) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → 𝐂 a j ⊆ P → a ∈ P) →
36 #A; #U; #P; #refl; #infty; #a; #H; nelim H
37 [ nauto | (*nauto depth=4;*) #b; #j; #K1; #K2;
38 napply infty; nauto; ##]
41 alias symbol "covers" (instance 1) = "covers".
43 ∀A:Ax.∀U:Ω^A.∀P:A → CProp[0].
44 (∀a. a ∈ U → P a) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → (∀b. b ∈ 𝐂 a j → P b) → P a) →
46 #A; #U; #P; nletin V ≝ {x | P x}; napply (cover_ind' … V).
49 (*********** from Cantor **********)
50 ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
53 notation "hvbox( a break ∼ b)" non associative with precedence 40
56 interpretation "eq between types" 'eqT a b = (eq1 a b).
58 ninductive unit : Type[0] ≝ one : unit.
60 ninductive option (A: Type[0]) : Type[0] ≝
64 nrecord uuAx : Type[1] ≝ {
66 uuC : uuS → option uuS
69 ndefinition uuax : uuAx → Ax.
71 [ #a; ncases (uuC … a) [ napply False | #_; napply unit]
72 ##| #a; ncases (uuC … a)
73 [ nnormalize; #H; napply (False_rect_Type1 … H)
74 | nnormalize; #b; #_; napply {x | x=b }]##]
77 ncoercion uuax : ∀u:uuAx. Ax ≝ uuax on _u : uuAx to Ax.
79 nlemma eq_rect_Type0_r':
80 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
81 #A; #a; #x; #p; ncases p; nauto;
84 nlemma eq_rect_Type0_r:
85 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
86 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
89 ninductive bool: Type[0] ≝
93 nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
94 { decide_mem:> A → bool;
95 decide_mem_ok: ∀x. decide_mem x = true → x ∈ U;
96 decide_mem_ko: ∀x. decide_mem x = false → ¬ (x ∈ U)
99 (*********** end from Cantor ********)
101 alias symbol "covers" (instance 9) = "covers".
102 alias symbol "covers" (instance 8) = "covers".
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
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;
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]##]
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; *)
128 ##| napply (cover_rect A U memdec P refl infty a); nauto ]##]
135 | S m ⇒ S m * skipfact (pred m) ]
138 ntheorem psym_plus: ∀n,m. n + m = m + n.
140 [ #m; nelim m; //; #n0; #H;
141 nchange with (natS n0 = natS (n0 + O));
143 | #n0; #H; #m; nchange with (S (n0 + m) = m + S n0);
146 #n1; #E; nrewrite > E; //]
149 nlemma easy1: ∀n:nat. two * (S n) = two + two * n.
152 nrewrite > (psym_plus ??);
153 nrewrite > H; nnormalize;
154 nrewrite > (psym_plus ??);
158 ndefinition skipfact_dom: uuAx.
159 @ nat; #n; ncases n [ napply None | #m; napply (Some … (pred m)) ]
162 ntheorem skipfact_base_dec:
163 memdec (uuax skipfact_dom) (mk_powerclass ? (λx: uuax skipfact_dom. x=O)).
164 nnormalize; @ (λx. match x with [ O ⇒ true | S _ ⇒ false ]); #n; nelim n;
165 nnormalize; //; #X; ndestruct; #Y; #Z; ndestruct; #W; ndestruct.
168 ntheorem skipfact_partial:
169 ∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O).
174 | nnormalize; #y; nchange in ⊢ (% → ?) with (y = pred (pred (two * (natone + m))));
175 nrewrite > (easy1 …); nchange in ⊢ (% → ?) with (y = two * m);
176 #E; nrewrite > E; nassumption ]##]
179 ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.
180 #n; #D; napply (cover_rect … skipfact_base_dec … n D)
181 [ #a; #_; napply natone
183 [ nnormalize; #i; nelim i
184 | #m; #i; nnormalize in i; #d; #H;
185 napply (S m * H (pred m) …); //]
188 nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)]