]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/broken_lib/reverse_complexity/hierarchy.ma
Matita 0.99.* bug fixed: new alias insertion
[helm.git] / matita / matita / broken_lib / reverse_complexity / hierarchy.ma
1
2 include "arithmetics/nat.ma".
3 include "arithmetics/log.ma".
4 (* include "arithmetics/ord.ma". *)
5 include "arithmetics/bigops.ma".
6 include "arithmetics/bounded_quantifiers.ma".
7 include "arithmetics/pidgeon_hole.ma".
8 include "basics/sets.ma".
9 include "basics/types.ma".
10
11 (************************************ MAX *************************************)
12 notation "Max_{ ident i < n | p } f"
13   with precedence 80
14 for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
15
16 notation "Max_{ ident i < n } f"
17   with precedence 80
18 for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}.
19
20 notation "Max_{ ident j ∈ [a,b[ } f"
21   with precedence 80
22 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
23   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
24   
25 notation "Max_{ ident j ∈ [a,b[ | p } f"
26   with precedence 80
27 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
28   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
29
30 lemma Max_assoc: ∀a,b,c. max (max a b) c = max a (max b c).
31 #a #b #c normalize cases (true_or_false (leb a b)) #leab >leab normalize
32   [cases (true_or_false (leb b c )) #lebc >lebc normalize
33     [>(le_to_leb_true a c) // @(transitive_le ? b) @leb_true_to_le //
34     |>leab //
35     ]
36   |cases (true_or_false (leb b c )) #lebc >lebc normalize //
37    >leab normalize >(not_le_to_leb_false a c) // @lt_to_not_le 
38    @(transitive_lt ? b) @not_le_to_lt @leb_false_to_not_le //
39   ]
40 qed.
41
42 lemma Max0 : ∀n. max 0 n = n.
43 // qed.
44
45 lemma Max0r : ∀n. max n 0 = n.
46 #n >commutative_max //
47 qed.
48
49 definition MaxA ≝ 
50   mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)). 
51
52 definition MaxAC ≝ mk_ACop nat 0 MaxA commutative_max.
53
54 lemma le_Max: ∀f,p,n,a. a < n → p a = true →
55   f a ≤  Max_{i < n | p i}(f i).
56 #f #p #n #a #ltan #pa 
57 >(bigop_diff p ? 0 MaxAC f a n) // @(le_maxl … (le_n ?))
58 qed.
59
60 lemma Max_le: ∀f,p,n,b. 
61   (∀a.a < n → p a = true → f a ≤ b) → Max_{i < n | p i}(f i) ≤ b.
62 #f #p #n elim n #b #H // 
63 #b0 #H1 cases (true_or_false (p b)) #Hb
64   [>bigop_Strue [2:@Hb] @to_max [@H1 // | @H #a #ltab #pa @H1 // @le_S //]
65   |>bigop_Sfalse [2:@Hb] @H #a #ltab #pa @H1 // @le_S //
66   ]
67 qed.
68
69 (******************************** big O notation ******************************)
70
71 (*  O f g means g ∈ O(f) *)
72 definition O: relation (nat→nat) ≝
73   λf,g. ∃c.∃n0.∀n. n0 ≤ n → g n ≤ c* (f n).
74   
75 lemma O_refl: ∀s. O s s.
76 #s %{1} %{0} #n #_ >commutative_times <times_n_1 @le_n qed.
77
78 lemma O_trans: ∀s1,s2,s3. O s2 s1 → O s3 s2 → O s3 s1. 
79 #s1 #s2 #s3 * #c1 * #n1 #H1 * #c2 * # n2 #H2 %{(c1*c2)}
80 %{(max n1 n2)} #n #Hmax 
81 @(transitive_le … (H1 ??)) [@(le_maxl … Hmax)]
82 >associative_times @le_times [//|@H2 @(le_maxr … Hmax)]
83 qed.
84
85 lemma sub_O_to_O: ∀s1,s2. O s1 ⊆ O s2 → O s2 s1.
86 #s1 #s2 #H @H // qed.
87
88 lemma O_to_sub_O: ∀s1,s2. O s2 s1 → O s1 ⊆ O s2.
89 #s1 #s2 #H #g #Hg @(O_trans … H) // qed. 
90
91 definition sum_f ≝ λf,g:nat→nat.λn.f n + g n.
92 interpretation "function sum" 'plus f g = (sum_f f g).
93
94 lemma O_plus: ∀f,g,s. O s f → O s g → O s (f+g).
95 #f #g #s * #cf * #nf #Hf * #cg * #ng #Hg
96 %{(cf+cg)} %{(max nf ng)} #n #Hmax normalize 
97 >distributive_times_plus_r @le_plus 
98   [@Hf @(le_maxl … Hmax) |@Hg @(le_maxr … Hmax) ]
99 qed.
100  
101 lemma O_plus_l: ∀f,s1,s2. O s1 f → O (s1+s2) f.
102 #f #s1 #s2 * #c * #a #Os1f %{c} %{a} #n #lean 
103 @(transitive_le … (Os1f n lean)) @le_times //
104 qed.
105
106 lemma O_plus_r: ∀f,s1,s2. O s2 f → O (s1+s2) f.
107 #f #s1 #s2 * #c * #a #Os1f %{c} %{a} #n #lean 
108 @(transitive_le … (Os1f n lean)) @le_times //
109 qed.
110
111 lemma O_absorbl: ∀f,g,s. O s f → O f g → O s (g+f).
112 #f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) //
113 qed.
114
115 lemma O_absorbr: ∀f,g,s. O s f → O f g → O s (f+g).
116 #f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) //
117 qed.
118
119 (* 
120 lemma O_ff: ∀f,s. O s f → O s (f+f).
121 #f #s #Osf /2/ 
122 qed. *)
123
124 lemma O_ext2: ∀f,g,s. O s f → (∀x.f x = g x) → O s g.
125 #f #g #s * #c * #a #Osf #eqfg %{c} %{a} #n #lean <eqfg @Osf //
126 qed.    
127
128
129 definition not_O ≝ λf,g.∀c,n0.∃n. n0 ≤ n ∧ c* (f n) < g n .
130
131 (* this is the only classical result *)
132 axiom not_O_def: ∀f,g. ¬ O f g → not_O f g.
133
134 (******************************* small O notation *****************************)
135
136 (*  o f g means g ∈ o(f) *)
137 definition o: relation (nat→nat) ≝
138   λf,g.∀c.∃n0.∀n. n0 ≤ n → c * (g n) < f n.
139   
140 lemma o_irrefl: ∀s. ¬ o s s.
141 #s % #oss cases (oss 1) #n0 #H @(absurd ? (le_n (s n0))) 
142 @lt_to_not_le >(times_n_1 (s n0)) in ⊢ (?%?); >commutative_times @H //
143 qed.
144
145 lemma o_trans: ∀s1,s2,s3. o s2 s1 → o s3 s2 → o s3 s1. 
146 #s1 #s2 #s3 #H1 #H2 #c cases (H1 c) #n1 -H1 #H1 cases (H2 1) #n2 -H2 #H2
147 %{(max n1 n2)} #n #Hmax 
148 @(transitive_lt … (H1 ??)) [@(le_maxl … Hmax)]
149 >(times_n_1 (s2 n)) in ⊢ (?%?); >commutative_times @H2 @(le_maxr … Hmax)
150 qed.
151
152
153 (*********************************** pairing **********************************) 
154
155 axiom pair: nat →nat →nat.
156 axiom fst : nat → nat.
157 axiom snd : nat → nat.
158 axiom fst_pair: ∀a,b. fst (pair a b) = a.
159 axiom snd_pair: ∀a,b. snd (pair a b) = b. 
160
161 interpretation "abstract pair" 'pair f g = (pair f g).
162
163 (************************ basic complexity notions ****************************)
164
165 (* u is the deterministic configuration relation of the universal machine (one 
166    step) 
167
168 axiom u: nat → option nat.
169
170 let rec U c n on n ≝ 
171   match n with  
172   [ O ⇒ None ?
173   | S m ⇒ match u c with 
174     [ None ⇒ Some ? c (* halting case *)
175     | Some c1 ⇒ U c1 m
176     ]
177   ].
178  
179 lemma halt_U: ∀i,n,y. u i = None ? → U i n = Some ? y → y = i.
180 #i #n #y #H cases n
181   [normalize #H1 destruct |#m normalize >H normalize #H1 destruct //]
182 qed. 
183
184 lemma Some_to_halt: ∀n,i,y. U i n = Some ? y → u y = None ? .
185 #n elim n
186   [#i #y normalize #H destruct (H)
187   |#m #Hind #i #y normalize 
188    cut (u i = None ? ∨ ∃c. u i = Some ? c) 
189     [cases (u i) [/2/ | #c %2 /2/ ]] 
190    *[#H >H normalize #H1 destruct (H1) // |* #c #H >H normalize @Hind ]
191   ]
192 qed. *)
193
194 axiom U: nat → nat → nat → option nat. 
195 (*
196 lemma monotonici_U: ∀y,n,m,i.
197   U i m = Some ? y → U i (n+m) = Some ? y.
198 #y #n #m elim m 
199   [#i normalize #H destruct 
200   |#p #Hind #i <plus_n_Sm normalize
201     cut (u i = None ? ∨ ∃c. u i = Some ? c) 
202     [cases (u i) [/2/ | #c %2 /2/ ]] 
203    *[#H1 >H1 normalize // |* #c #H >H normalize #H1 @Hind //]
204   ]
205 qed. *)
206
207 axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
208   U i x n = Some ? y → U i x m = Some ? y.
209 (* #i #n #m #y #lenm #H >(plus_minus_m_m m n) // @monotonici_U //
210 qed. *)
211
212 (* axiom U: nat → nat → option nat. *)
213 (* axiom monotonic_U: ∀i,n,m,y.n ≤m →
214    U i n = Some ? y → U i m = Some ? y. *)
215   
216 lemma unique_U: ∀i,x,n,m,yn,ym.
217   U i x n = Some ? yn → U i x m = Some ? ym → yn = ym.
218 #i #x #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
219   [#lenm lapply (monotonic_U … lenm Hn) >Hm #HS destruct (HS) //
220   |#ltmn lapply (monotonic_U … n … Hm) [@lt_to_le @not_le_to_lt //]
221    >Hn #HS destruct (HS) //
222   ]
223 qed.
224
225 definition code_for ≝ λf,i.∀x.
226   ∃n.∀m. n ≤ m → U i x m = f x.
227
228 definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y.
229 notation "[i,x] ↓ r" with precedence 60 for @{terminate $i $x $r}.
230
231 definition lang ≝ λi,x.∃r,y. U i x r = Some ? y ∧ 0  < y. 
232
233 lemma lang_cf :∀f,i,x. code_for f i → 
234   lang i x ↔ ∃y.f x = Some ? y ∧ 0 < y.
235 #f #i #x normalize #H %
236   [* #n * #y * #H1 #posy %{y} % // 
237    cases (H x) -H #m #H <(H (max n m)) [2:@(le_maxr … n) //]
238    @(monotonic_U … H1) @(le_maxl … m) //
239   |cases (H x) -H #m #Hm * #y #Hy %{m} %{y} >Hm // 
240   ]
241 qed.
242
243 (******************************* complexity classes ***************************)
244
245 axiom size: nat → nat.
246 axiom of_size: nat → nat.
247
248 interpretation "size" 'card n = (size n).
249
250 axiom size_of_size: ∀n. |of_size n| = n.
251 axiom monotonic_size: monotonic ? le size.
252
253 axiom of_size_max: ∀i,n. |i| = n → i ≤ of_size n.
254
255 axiom size_fst : ∀n. |fst n| ≤ |n|.
256
257 definition size_f ≝ λf,n.Max_{i < S (of_size n) | eqb (|i|) n}|(f i)|.
258
259 lemma size_f_def: ∀f,n. size_f f n = 
260   Max_{i < S (of_size n) | eqb (|i|) n}|(f i)|.
261 // qed.
262
263 (*
264 definition Max_const : ∀f,p,n,a. a < n → p a →
265   ∀n. f n = g n →
266   Max_{i < n | p n}(f n) = *)
267
268 lemma size_f_size : ∀f,n. size_f (f ∘ size) n = |(f n)|.
269 #f #n @le_to_le_to_eq
270   [@Max_le #a #lta #Ha normalize >(eqb_true_to_eq  … Ha) //
271   |<(size_of_size n) in ⊢ (?%?); >size_f_def
272    @(le_Max (λi.|f (|i|)|) ? (S (of_size n)) (of_size n) ??)
273     [@le_S_S // | @eq_to_eqb_true //]
274   ]
275 qed.
276
277 lemma size_f_id : ∀n. size_f (λx.x) n = n.
278 #n @le_to_le_to_eq
279   [@Max_le #a #lta #Ha >(eqb_true_to_eq  … Ha) //
280   |<(size_of_size n) in ⊢ (?%?); >size_f_def
281    @(le_Max (λi.|i|) ? (S (of_size n)) (of_size n) ??)
282     [@le_S_S // | @eq_to_eqb_true //]
283   ]
284 qed.
285
286 lemma size_f_fst : ∀n. size_f fst n ≤ n.
287 #n @Max_le #a #lta #Ha <(eqb_true_to_eq  … Ha) //
288 qed.
289
290 (* definition def ≝ λf:nat → option nat.λx.∃y. f x = Some ? y.*)
291
292 (* C s i means that the complexity of i is O(s) *)
293
294 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ |x| → ∃y. 
295   U i x (c*(s(|x|))) = Some ? y.
296
297 definition CF ≝ λs,f.∃i.code_for f i ∧ C s i.
298
299 lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
300 #f #g #s #Hext * #i * #Hcode #HC %{i} %
301   [#x cases (Hcode x) #a #H %{a} <Hext @H | //] 
302 qed. 
303
304 lemma monotonic_CF: ∀s1,s2,f. O s2 s1 → CF s1 f → CF s2 f.
305 #s1 #s2 #f * #c1 * #a #H * #i * #Hcodef #HCs1 %{i} % //
306 cases HCs1 #c2 * #b #H2 %{(c2*c1)} %{(max a b)} 
307 #x #Hmax cases (H2 x ?) [2:@(le_maxr … Hmax)] #y #Hy
308 %{y} @(monotonic_U …Hy) >associative_times @le_times // @H @(le_maxl … Hmax)
309 qed. 
310
311 (************************** The diagonal language *****************************)
312
313 (* the diagonal language used for the hierarchy theorem *)
314
315 definition diag ≝ λs,i. 
316   U (fst i) i (s (|i|)) = Some ? 0. 
317
318 lemma equiv_diag: ∀s,i. 
319   diag s i ↔ [fst i,i] ↓ s (|i|) ∧ ¬lang (fst i) i.
320 #s #i %
321   [whd in ⊢ (%→?); #H % [%{0} //] % * #x * #y *
322    #H1 #Hy cut (0 = y) [@(unique_U … H H1)] #eqy /2/
323   |* * #y cases y //
324    #y0 #H * #H1 @False_ind @H1 -H1 whd %{(s (|i|))} %{(S y0)} % //
325   ]
326 qed.
327
328 (* Let us define the characteristic function diag_cf for diag, and prove
329 it correctness *)
330
331 definition diag_cf ≝ λs,i.
332   match U (fst i) i (s (|i|)) with
333   [ None ⇒ None ?
334   | Some y ⇒ if (eqb y 0) then (Some ? 1) else (Some ? 0)].
335
336 lemma diag_cf_OK: ∀s,x. diag s x ↔ ∃y.diag_cf s x = Some ? y ∧ 0 < y.
337 #s #x % 
338   [whd in ⊢ (%→?); #H %{1} % // whd in ⊢ (??%?); >H // 
339   |* #y * whd in ⊢ (??%?→?→%); 
340    cases (U (fst x) x (s (|x|))) normalize
341     [#H destruct
342     |#x cases (true_or_false (eqb x 0)) #Hx >Hx 
343       [>(eqb_true_to_eq … Hx) // 
344       |normalize #H destruct #H @False_ind @(absurd ? H) @lt_to_not_le //  
345       ]
346     ]
347   ]
348 qed.
349
350 lemma diag_spec: ∀s,i. code_for (diag_cf s) i → ∀x. lang i x ↔ diag s x.
351 #s #i #Hcode #x @(iff_trans  … (lang_cf … Hcode)) @iff_sym @diag_cf_OK
352 qed. 
353
354 (******************************************************************************)
355
356 lemma absurd1: ∀P. iff P (¬ P) →False.
357 #P * #H1 #H2 cut (¬P) [% #H2 @(absurd … H2) @H1 //] 
358 #H3 @(absurd ?? H3) @H2 @H3 
359 qed.
360
361 (* axiom weak_pad : ∀a,∃a0.∀n. a0 < n → ∃b. |〈a,b〉| = n. *)
362 lemma weak_pad1 :∀n,a.∃b. n ≤ 〈a,b〉. 
363 #n #a 
364 cut (∀i.decidable (〈a,i〉 < n))
365   [#i @decidable_le ] 
366    #Hdec cases(decidable_forall (λb. 〈a,b〉 < n) Hdec n)
367   [#H cut (∀i. i < n → ∃b. b < n ∧ 〈a,b〉 = i)
368     [@(injective_to_exists … H) //]
369    #Hcut %{n} @not_lt_to_le % #Han
370    lapply(Hcut ? Han) * #x * #Hx #Hx2 
371    cut (x = n) [//] #Hxn >Hxn in Hx; /2 by absurd/ 
372   |#H lapply(not_forall_to_exists … Hdec H) 
373    * #b * #H1 #H2 %{b} @not_lt_to_le @H2
374   ]
375 qed. 
376
377 lemma pad : ∀n,a. ∃b. n ≤ |〈a,b〉|.
378 #n #a cases (weak_pad1 (of_size n) a) #b #Hb 
379 %{b} <(size_of_size n) @monotonic_size //
380 qed.
381
382 lemma o_to_ex: ∀s1,s2. o s1 s2 → ∀i. C s2 i →
383   ∃b.[i, 〈i,b〉] ↓ s1 (|〈i,b〉|).
384 #s1 #s2  #H #i * #c * #x0 #H1 
385 cases (H c) #n0 #H2 cases (pad (max x0 n0) i) #b #Hmax
386 %{b} cases (H1 〈i,b〉 ?)
387   [#z #H3 %{z} @(monotonic_U … H3) @lt_to_le @H2
388    @(le_maxr … Hmax)
389   |@(le_maxl … Hmax)
390   ]
391 qed. 
392
393 lemma diag1_not_s1: ∀s1,s2. o s1 s2 → ¬ CF s2 (diag_cf s1).
394 #s1 #s2 #H1 % * #i * #Hcode_i #Hs2_i 
395 cases (o_to_ex  … H1 ? Hs2_i) #b #H2
396 lapply (diag_spec … Hcode_i) #H3
397 @(absurd1 (lang i 〈i,b〉))
398 @(iff_trans … (H3 〈i,b〉)) 
399 @(iff_trans … (equiv_diag …)) >fst_pair 
400 %[* #_ // |#H6 % // ]
401 qed.
402
403 (******************************************************************************)
404
405 definition to_Some ≝ λf.λx:nat. Some nat (f x).
406
407 definition deopt ≝ λn. match n with 
408   [ None ⇒ 1
409   | Some n ⇒ n].
410   
411 definition opt_comp ≝ λf,g:nat → option nat. λx.
412   match g x with 
413   [ None ⇒ None ?
414   | Some y ⇒ f y ].   
415
416 (* axiom CFU: ∀h,g,s. CF s (to_Some h)  → CF s (to_Some (of_size ∘ g)) → 
417   CF (Slow s) (λx.U (h x) (g x)). *)
418   
419 axiom sU2: nat → nat → nat.
420 axiom sU: nat → nat → nat → nat.
421
422 (* axiom CFU: CF sU (λx.U (fst x) (snd x)). *)
423
424 axiom CFU_new: ∀h,g,f,s. 
425   CF s (to_Some h)  → CF s (to_Some g) → CF s (to_Some f) → 
426   O s (λx. sU (size_f h x) (size_f g x) (size_f f x)) → 
427   CF s (λx.U (h x) (g x) (|f x|)).
428     
429 lemma CFU: ∀h,g,f,s1,s2,s3. 
430   CF s1 (to_Some h)  → CF s2 (to_Some g) → CF s3 (to_Some f) → 
431   CF (λx. s1 x + s2 x + s3 x + sU (size_f h x) (size_f g x) (size_f f x)) 
432     (λx.U (h x) (g x) (|f x|)).
433 #h #g #f #s1 #s2 #s3 #Hh #Hg #Hf @CFU_new
434   [@(monotonic_CF … Hh) @O_plus_l @O_plus_l @O_plus_l //
435   |@(monotonic_CF … Hg) @O_plus_l @O_plus_l @O_plus_r //
436   |@(monotonic_CF … Hf) @O_plus_l @O_plus_r //
437   |@O_plus_r //
438   ]
439 qed.
440     
441 axiom monotonic_sU: ∀a1,a2,b1,b2,c1,c2. a1 ≤ a2 → b1 ≤ b2 → c1 ≤c2 →
442   sU a1 b1 c1 ≤ sU a2 b2 c2.
443
444 axiom superlinear_sU: ∀i,x,r. r ≤ sU i x r.
445
446 definition sU_space ≝ λi,x,r.i+x+r.
447 definition sU_time ≝ λi,x,r.i+x+(i^2)*r*(log 2 r).
448
449 (*
450 axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g → 
451   CF (λx.s2 x + s1 (size (deopt (g x)))) (opt_comp f g).
452
453 (* axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g → 
454   CF (s1 ∘ (λx. size (deopt (g x)))) (opt_comp f g). *)
455   
456 axiom CF_comp_strong: ∀f,g,s1,s2. CF s1 f → CF s2 g → 
457   CF (s1 ∘ s2) (opt_comp f g). *)
458
459 definition IF ≝ λb,f,g:nat →option nat. λx.
460   match b x with 
461   [None ⇒ None ?
462   |Some n ⇒ if (eqb n 0) then f x else g x].
463   
464 axiom IF_CF_new: ∀b,f,g,s. CF s b → CF s f → CF s g → CF s (IF b f g).
465
466 lemma IF_CF: ∀b,f,g,sb,sf,sg. CF sb b → CF sf f → CF sg g → 
467   CF (λn. sb n + sf n + sg n) (IF b f g).
468 #b #f #g #sb #sf #sg #Hb #Hf #Hg @IF_CF_new
469   [@(monotonic_CF … Hb) @O_plus_l @O_plus_l //
470   |@(monotonic_CF … Hf) @O_plus_l @O_plus_r //
471   |@(monotonic_CF … Hg) @O_plus_r //
472   ]
473 qed.
474
475 lemma diag_cf_def : ∀s.∀i. 
476   diag_cf s i =  
477     IF (λi.U (fst i) i (|of_size (s (|i|))|)) (λi.Some ? 1) (λi.Some ? 0) i.
478 #s #i normalize >size_of_size // qed. 
479
480 (* and now ... *)
481 axiom CF_pair: ∀f,g,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (g x)) → 
482   CF s (λx.Some ? (pair (f x) (g x))).
483
484 axiom CF_fst: ∀f,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (fst (f x))).
485
486 definition minimal ≝ λs. CF s (λn. Some ? n) ∧ ∀c. CF s (λn. Some ? c).
487
488
489 (*
490 axiom le_snd: ∀n. |snd n| ≤ |n|.
491 axiom daemon: ∀P:Prop.P. *)
492
493 definition constructible ≝ λs. CF s (λx.Some ? (of_size (s (|x|)))).
494
495 lemma diag_s: ∀s. minimal s → constructible s → 
496   CF (λx.sU x x (s x)) (diag_cf s).
497 #s * #Hs_id #Hs_c #Hs_constr 
498 cut (O (λx:ℕ.sU x x (s x)) s) [%{1} %{0} #n //]
499 #O_sU_s @ext_CF [2: #n @sym_eq @diag_cf_def | skip]
500 @IF_CF_new [2,3:@(monotonic_CF … (Hs_c ?)) // ] 
501 @CFU_new
502   [@CF_fst @(monotonic_CF … Hs_id) //
503   |@(monotonic_CF … Hs_id) //
504   |@(monotonic_CF … Hs_constr) //
505   |%{1} %{0} #n #_ >commutative_times <times_n_1
506    @monotonic_sU // >size_f_size >size_of_size //
507   ]
508 qed. 
509
510 (*
511 lemma diag_s: ∀s. minimal s → constructible s → 
512   CF (λx.s x + sU x x (s x)) (diag_cf s).
513 #s * #Hs_id #Hs_c #Hs_constr 
514 @ext_CF [2: #n @sym_eq @diag_cf_def | skip]
515 @IF_CF_new [2,3:@(monotonic_CF … (Hs_c ?)) @O_plus_l //]
516 @CFU_new
517   [@CF_fst @(monotonic_CF … Hs_id) @O_plus_l //
518   |@(monotonic_CF … Hs_id) @O_plus_l //
519   |@(monotonic_CF … Hs_constr) @O_plus_l //
520   |@O_plus_r %{1} %{0} #n #_ >commutative_times <times_n_1
521    @monotonic_sU // >size_f_size >size_of_size //
522   ]
523 qed. *)
524
525 (* proof with old axioms
526 lemma diag_s: ∀s. minimal s → constructible s → 
527   CF (λx.s x + sU x x (s x)) (diag_cf s).
528 #s * #Hs_id #Hs_c #Hs_constr 
529 @ext_CF [2: #n @sym_eq @diag_cf_def | skip]
530 @(monotonic_CF ???? (IF_CF (λi:ℕ.U (pair (fst i) i) (|of_size (s (|i|))|))
531    … (λi.s i + s i + s i + (sU (size_f fst i) (size_f (λi.i) i) (size_f (λi.of_size (s (|i|))) i))) … (Hs_c 1) (Hs_c 0) … ))
532   [2: @CFU [@CF_fst // | // |@Hs_constr]
533   |@(O_ext2 (λn:ℕ.s n+sU (size_f fst n) n (s n) + (s n+s n+s n+s n))) 
534     [2: #i >size_f_size >size_of_size >size_f_id //] 
535    @O_absorbr 
536     [%{1} %{0} #n #_ >commutative_times <times_n_1 @le_plus //
537      @monotonic_sU // 
538     |@O_plus_l @(O_plus … (O_refl s)) @(O_plus … (O_refl s)) 
539      @(O_plus … (O_refl s)) //
540   ]
541 qed.
542 *)
543
544 (*************************** The hierachy theorem *****************************)
545
546 (*
547 theorem hierarchy_theorem_right: ∀s1,s2:nat→nat. 
548   O s1 idN → constructible s1 →
549     not_O s2 s1 → ¬ CF s1 ⊆ CF s2.
550 #s1 #s2 #Hs1 #monos1 #H % #H1 
551 @(absurd … (CF s2 (diag_cf s1)))
552   [@H1 @diag_s // |@(diag1_not_s1 … H)]
553 qed.
554 *)
555
556 theorem hierarchy_theorem_left: ∀s1,s2:nat→nat.
557    O(s1) ⊆ O(s2) → CF s1 ⊆ CF s2.
558 #s1 #s2 #HO #f * #i * #Hcode * #c * #a #Hs1_i %{i} % //
559 cases (sub_O_to_O … HO) -HO #c1 * #b #Hs1s2 
560 %{(c*c1)} %{(max a b)} #x #lemax 
561 cases (Hs1_i x ?) [2: @(le_maxl …lemax)]
562 #y #Hy %{y} @(monotonic_U … Hy) >associative_times
563 @le_times // @Hs1s2 @(le_maxr … lemax)
564 qed.
565