1 include "basics/types.ma".
2 include "arithmetics/minimization.ma".
3 include "arithmetics/bigops.ma".
4 include "arithmetics/sigma_pi.ma".
5 include "arithmetics/bounded_quantifiers.ma".
6 include "reverse_complexity/big_O.ma".
7 include "basics/core_notation/napart_2.ma".
9 (************************* notation for minimization *****************************)
10 notation "μ_{ ident i < n } p"
11 with precedence 80 for @{min $n 0 (λ${ident i}.$p)}.
13 notation "μ_{ ident i ≤ n } p"
14 with precedence 80 for @{min (S $n) 0 (λ${ident i}.$p)}.
16 notation "μ_{ ident i ∈ [a,b[ } p"
17 with precedence 80 for @{min ($b-$a) $a (λ${ident i}.$p)}.
19 notation "μ_{ ident i ∈ [a,b] } p"
20 with precedence 80 for @{min (S $b-$a) $a (λ${ident i}.$p)}.
22 (************************************ MAX *************************************)
23 notation "Max_{ ident i < n | p } f"
25 for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
27 notation "Max_{ ident i < n } f"
29 for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}.
31 notation "Max_{ ident j ∈ [a,b[ } f"
33 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
34 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
36 notation "Max_{ ident j ∈ [a,b[ | p } f"
38 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
39 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
41 lemma Max_assoc: ∀a,b,c. max (max a b) c = max a (max b c).
42 #a #b #c normalize cases (true_or_false (leb a b)) #leab >leab normalize
43 [cases (true_or_false (leb b c )) #lebc >lebc normalize
44 [>(le_to_leb_true a c) // @(transitive_le ? b) @leb_true_to_le //
47 |cases (true_or_false (leb b c )) #lebc >lebc normalize //
48 >leab normalize >(not_le_to_leb_false a c) // @lt_to_not_le
49 @(transitive_lt ? b) @not_le_to_lt @leb_false_to_not_le //
53 lemma Max0 : ∀n. max 0 n = n.
56 lemma Max0r : ∀n. max n 0 = n.
57 #n >commutative_max //
61 mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)).
63 definition MaxAC ≝ mk_ACop nat 0 MaxA commutative_max.
65 lemma le_Max: ∀f,p,n,a. a < n → p a = true →
66 f a ≤ Max_{i < n | p i}(f i).
68 >(bigop_diff p ? 0 MaxAC f a n) // @(le_maxl … (le_n ?))
71 lemma le_MaxI: ∀f,p,n,m,a. m ≤ a → a < n → p a = true →
72 f a ≤ Max_{i ∈ [m,n[ | p i}(f i).
73 #f #p #n #m #a #lema #ltan #pa
74 >(bigop_diff ? ? 0 MaxAC (λi.f (i+m)) (a-m) (n-m))
75 [<plus_minus_m_m // @(le_maxl … (le_n ?))
77 |/2 by monotonic_lt_minus_l/
81 lemma Max_le: ∀f,p,n,b.
82 (∀a.a < n → p a = true → f a ≤ b) → Max_{i < n | p i}(f i) ≤ b.
83 #f #p #n elim n #b #H //
84 #b0 #H1 cases (true_or_false (p b)) #Hb
85 [>bigop_Strue [2:@Hb] @to_max [@H1 // | @H #a #ltab #pa @H1 // @le_S //]
86 |>bigop_Sfalse [2:@Hb] @H #a #ltab #pa @H1 // @le_S //
90 (********************************** pairing ***********************************)
91 axiom pair: nat → nat → nat.
92 axiom fst : nat → nat.
93 axiom snd : nat → nat.
95 interpretation "abstract pair" 'pair f g = (pair f g).
97 axiom fst_pair: ∀a,b. fst 〈a,b〉 = a.
98 axiom snd_pair: ∀a,b. snd 〈a,b〉 = b.
99 axiom surj_pair: ∀x. ∃a,b. x = 〈a,b〉.
101 axiom le_fst : ∀p. fst p ≤ p.
102 axiom le_snd : ∀p. snd p ≤ p.
103 axiom le_pair: ∀a,a1,b,b1. a ≤ a1 → b ≤ b1 → 〈a,b〉 ≤ 〈a1,b1〉.
105 (************************************* U **************************************)
106 axiom U: nat → nat →nat → option nat.
108 axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
109 U i x n = Some ? y → U i x m = Some ? y.
111 lemma unique_U: ∀i,x,n,m,yn,ym.
112 U i x n = Some ? yn → U i x m = Some ? ym → yn = ym.
113 #i #x #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
114 [#lenm lapply (monotonic_U … lenm Hn) >Hm #HS destruct (HS) //
115 |#ltmn lapply (monotonic_U … n … Hm) [@lt_to_le @not_le_to_lt //]
116 >Hn #HS destruct (HS) //
120 definition code_for ≝ λf,i.∀x.
121 ∃n.∀m. n ≤ m → U i x m = f x.
123 definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y.
125 notation "{i ⊙ x} ↓ r" with precedence 60 for @{terminate $i $x $r}.
127 lemma terminate_dec: ∀i,x,n. {i ⊙ x} ↓ n ∨ ¬ {i ⊙ x} ↓ n.
128 #i #x #n normalize cases (U i x n)
129 [%2 % * #y #H destruct|#y %1 %{y} //]
132 lemma monotonic_terminate: ∀i,x,n,m.
133 n ≤ m → {i ⊙ x} ↓ n → {i ⊙ x} ↓ m.
134 #i #x #n #m #lenm * #z #H %{z} @(monotonic_U … H) //
137 definition termb ≝ λi,x,t.
138 match U i x t with [None ⇒ false |Some y ⇒ true].
140 lemma termb_true_to_term: ∀i,x,t. termb i x t = true → {i ⊙ x} ↓ t.
141 #i #x #t normalize cases (U i x t) normalize [#H destruct | #y #_ %{y} //]
144 lemma term_to_termb_true: ∀i,x,t. {i ⊙ x} ↓ t → termb i x t = true.
145 #i #x #t * #y #H normalize >H //
148 definition out ≝ λi,x,r.
149 match U i x r with [ None ⇒ 0 | Some z ⇒ z].
151 definition bool_to_nat: bool → nat ≝
152 λb. match b with [true ⇒ 1 | false ⇒ 0].
154 coercion bool_to_nat.
156 definition pU : nat → nat → nat → nat ≝ λi,x,r.〈termb i x r,out i x r〉.
158 lemma pU_vs_U_Some : ∀i,x,r,y. pU i x r = 〈1,y〉 ↔ U i x r = Some ? y.
159 #i #x #r #y % normalize
160 [cases (U i x r) normalize
161 [#H cut (0=1) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H @H]
163 |#a #H cut (a=y) [lapply (eq_f … snd … H) >snd_pair >snd_pair #H1 @H1]
169 lemma pU_vs_U_None : ∀i,x,r. pU i x r = 〈0,0〉 ↔ U i x r = None ?.
171 [cases (U i x r) normalize //
172 #a #H cut (1=0) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H1 @H1]
177 lemma fst_pU: ∀i,x,r. fst (pU i x r) = termb i x r.
178 #i #x #r normalize cases (U i x r) normalize >fst_pair //
181 lemma snd_pU: ∀i,x,r. snd (pU i x r) = out i x r.
182 #i #x #r normalize cases (U i x r) normalize >snd_pair //
185 (********************************* the speedup ********************************)
187 definition min_input ≝ λh,i,x. μ_{y ∈ [S i,x] } (termb i y (h (S i) y)).
189 lemma min_input_def : ∀h,i,x.
190 min_input h i x = min (x -i) (S i) (λy.termb i y (h (S i) y)).
193 lemma min_input_i: ∀h,i,x. x ≤ i → min_input h i x = S i.
194 #h #i #x #lexi >min_input_def
195 cut (x - i = 0) [@sym_eq /2 by eq_minus_O/] #Hcut //
198 lemma min_input_to_terminate: ∀h,i,x.
199 min_input h i x = x → {i ⊙ x} ↓ (h (S i) x).
201 cases (decidable_le (S i) x) #Hix
202 [cases (true_or_false (termb i x (h (S i) x))) #Hcase
203 [@termb_true_to_term //
204 |<Hminx in Hcase; #H lapply (fmin_false (λx.termb i x (h (S i) x)) (x-i) (S i) H)
205 >min_input_def in Hminx; #Hminx >Hminx in ⊢ (%→?);
206 <plus_n_Sm <plus_minus_m_m [2: @lt_to_le //]
209 |@False_ind >min_input_i in Hminx;
210 [#eqix >eqix in Hix; * /2/ | @le_S_S_to_le @not_le_to_lt //]
214 lemma min_input_to_lt: ∀h,i,x.
215 min_input h i x = x → i < x.
216 #h #i #x #Hminx cases (decidable_le (S i) x) //
217 #ltxi @False_ind >min_input_i in Hminx;
218 [#eqix >eqix in ltxi; * /2/ | @le_S_S_to_le @not_le_to_lt //]
221 lemma le_to_min_input: ∀h,i,x,x1. x ≤ x1 →
222 min_input h i x = x → min_input h i x1 = x.
223 #h #i #x #x1 #lex #Hminx @(min_exists … (le_S_S … lex))
224 [@(fmin_true … (sym_eq … Hminx)) //
225 |@(min_input_to_lt … Hminx)
226 |#j #H1 <Hminx @lt_min_to_false //
227 |@plus_minus_m_m @le_S_S @(transitive_le … lex) @lt_to_le
228 @(min_input_to_lt … Hminx)
232 definition g ≝ λh,u,x.
233 S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
235 lemma g_def : ∀h,u,x. g h u x =
236 S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
239 lemma le_u_to_g_1 : ∀h,u,x. x ≤ u → g h u x = 1.
240 #h #u #x #lexu >g_def cut (x-u = 0) [/2 by minus_le_minus_minus_comm/]
241 #eq0 >eq0 normalize // qed.
243 lemma g_lt : ∀h,i,x. min_input h i x = x →
244 out i x (h (S i) x) < g h 0 x.
245 #h #i #x #H @le_S_S @(le_MaxI … i) /2 by min_input_to_lt/
248 lemma max_neq0 : ∀a,b. max a b ≠ 0 → a ≠ 0 ∨ b ≠ 0.
249 #a #b whd in match (max a b); cases (true_or_false (leb a b)) #Hcase >Hcase
250 [#H %2 @H | #H %1 @H]
253 definition almost_equal ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
254 interpretation "almost equal" 'napart f g = (almost_equal f g).
256 lemma eventually_cancelled: ∀h,u.¬∀nu.∃x. nu < x ∧
257 max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) ≠ 0.
259 [normalize % #H cases (H u) #x * #_ * #H1 @H1 //
260 |#u0 @not_to_not #Hind #nu cases (Hind nu) #x * #ltx
261 cases (true_or_false (eqb (min_input h (u0+O) x) x)) #Hcase
262 [>bigop_Strue [2:@Hcase] #Hmax cases (max_neq0 … Hmax) -Hmax
263 [2: #H %{x} % // <minus_n_O @H]
264 #Hneq0 (* if x is not enough we retry with nu=x *)
265 cases (Hind x) #x1 * #ltx1
267 [#H %{x1} % [@transitive_lt //| <minus_n_O @H]
268 |@not_eq_to_eqb_false >(le_to_min_input … (eqb_true_to_eq … Hcase))
269 [@lt_to_not_eq @ltx1 | @lt_to_le @ltx1]
271 |>bigop_Sfalse [2:@Hcase] #H %{x} % // <minus_n_O @H
276 lemma condition_1: ∀h,u.g h 0 ≈ g h u.
277 #h #u @(not_to_not … (eventually_cancelled h u))
278 #H #nu cases (H (max u nu)) #x * #ltx #Hdiff
279 %{x} % [@(le_to_lt_to_lt … ltx) @(le_maxr … (le_n …))] @(not_to_not … Hdiff)
280 #H @(eq_f ?? S) >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat 0 MaxA)
281 [>H // |@lt_to_le @(le_to_lt_to_lt …ltx) /2 by le_maxr/ |//]
284 (******************************** Condition 2 *********************************)
285 definition total ≝ λf.λx:nat. Some nat (f x).
287 lemma exists_to_exists_min: ∀h,i. (∃x. i < x ∧ {i ⊙ x} ↓ h (S i) x) → ∃y. min_input h i y = y.
288 #h #i * #x * #ltix #Hx %{(min_input h i x)} @min_spec_to_min @found //
289 [@(f_min_true (λy:ℕ.termb i y (h (S i) y))) %{x} % [% // | @term_to_termb_true //]
290 |#y #leiy #lty @(lt_min_to_false ????? lty) //
294 lemma condition_2: ∀h,i. code_for (total (g h 0)) i → ¬∃x. i<x ∧ {i ⊙ x} ↓ h (S i) x.
295 #h #i whd in ⊢(%→?); #H % #H1 cases (exists_to_exists_min … H1) #y #Hminy
296 lapply (g_lt … Hminy)
297 lapply (min_input_to_terminate … Hminy) * #r #termy
298 cases (H y) -H #ny #Hy
299 cut (r = g h 0 y) [@(unique_U … ny … termy) @Hy //] #Hr
300 whd in match (out ???); >termy >Hr
301 #H @(absurd ? H) @le_to_not_lt @le_n
305 (********************************* complexity *********************************)
307 (* We assume operations have a minimal structural complexity MSC.
308 For instance, for time complexity, MSC is equal to the size of input.
309 For space complexity, MSC is typically 0, since we only measure the
310 space required in addition to dimension of the input. *)
312 axiom MSC : nat → nat.
313 axiom MSC_le: ∀n. MSC n ≤ n.
314 axiom monotonic_MSC: monotonic ? le MSC.
315 axiom MSC_pair: ∀a,b. MSC 〈a,b〉 ≤ MSC a + MSC b.
317 (* C s i means i is running in O(s) *)
319 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ x → ∃y.
320 U i x (c*(s x)) = Some ? y.
322 (* C f s means f ∈ O(s) where MSC ∈O(s) *)
323 definition CF ≝ λs,f.O s MSC ∧ ∃i.code_for (total f) i ∧ C s i.
325 lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
326 #f #g #s #Hext * #HO * #i * #Hcode #HC % // %{i} %
327 [#x cases (Hcode x) #a #H %{a} whd in match (total ??); <Hext @H | //]
330 lemma monotonic_CF: ∀s1,s2,f.(∀x. s1 x ≤ s2 x) → CF s1 f → CF s2 f.
331 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
332 [cases HO #c * #a -HO #HO %{c} %{a} #n #lean @(transitive_le … (HO n lean))
334 |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1 %{c} %{a} #n #lean
335 cases(Hs1 n lean) #y #Hy %{y} @(monotonic_U …Hy) @le_times //
339 lemma O_to_CF: ∀s1,s2,f.O s2 s1 → CF s1 f → CF s2 f.
340 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
342 |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1
343 cases H #c1 * #a1 #Ha1 %{(c*c1)} %{(a+a1)} #n #lean
344 cases(Hs1 n ?) [2:@(transitive_le … lean) //] #y #Hy %{y} @(monotonic_U …Hy)
345 >associative_times @le_times // @Ha1 @(transitive_le … lean) //
349 lemma timesc_CF: ∀s,f,c.CF (λx.c*s x) f → CF s f.
350 #s #f #c @O_to_CF @O_times_c
353 (********************************* composition ********************************)
354 axiom CF_comp: ∀f,g,sf,sg,sh. CF sg g → CF sf f →
355 O sh (λx. sg x + sf (g x)) → CF sh (f ∘ g).
357 lemma CF_comp_ext: ∀f,g,h,sh,sf,sg. CF sg g → CF sf f →
358 (∀x.f(g x) = h x) → O sh (λx. sg x + sf (g x)) → CF sh h.
359 #f #g #h #sh #sf #sg #Hg #Hf #Heq #H @(ext_CF (f ∘ g))
360 [#n normalize @Heq | @(CF_comp … H) //]
363 (* primitve recursion *)
365 let rec prim_rec (k,h:nat →nat) n m on n ≝
368 | S a ⇒ h 〈a,〈prim_rec k h a m, m〉〉].
370 lemma prim_rec_S: ∀k,h,n,m.
371 prim_rec k h (S n) m = h 〈n,〈prim_rec k h n m, m〉〉.
374 definition unary_pr ≝ λk,h,x. prim_rec k h (fst x) (snd x).
376 let rec prim_rec_compl (k,h,sk,sh:nat →nat) n m on n ≝
379 | S a ⇒ prim_rec_compl k h sk sh a m + sh (prim_rec k h a m)].
381 axiom CF_prim_rec: ∀k,h,sk,sh,sf. CF sk k → CF sh h →
382 O sf (unary_pr sk (λx. fst (snd x) + sh 〈fst x,〈unary_pr k h 〈fst x,snd (snd x)〉,snd (snd x)〉〉))
383 → CF sf (unary_pr k h).
386 lemma prim_rec_O: ∀k1,h1,k2,h2. O k1 k2 → O h1 h2 →
387 O (unary_pr k1 h1) (unary_pr k2 h2).
388 #k1 #h1 #k2 #h2 #HO1 #HO2 whd *)
391 (**************************** primitive operations*****************************)
393 definition id ≝ λx:nat.x.
395 axiom CF_id: CF MSC id.
396 axiom CF_compS: ∀h,f. CF h f → CF h (S ∘ f).
397 axiom CF_comp_fst: ∀h,f. CF h f → CF h (fst ∘ f).
398 axiom CF_comp_snd: ∀h,f. CF h f → CF h (snd ∘ f).
399 axiom CF_comp_pair: ∀h,f,g. CF h f → CF h g → CF h (λx. 〈f x,g x〉).
401 lemma CF_fst: CF MSC fst.
402 @(ext_CF (fst ∘ id)) [#n //] @(CF_comp_fst … CF_id)
405 lemma CF_snd: CF MSC snd.
406 @(ext_CF (snd ∘ id)) [#n //] @(CF_comp_snd … CF_id)
409 (************************************** eqb ***********************************)
411 axiom CF_eqb: ∀h,f,g.
412 CF h f → CF h g → CF h (λx.eqb (f x) (g x)).
414 (*********************************** maximum **********************************)
416 axiom CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
417 CF ha a → CF hb b → CF hp p → CF hf f →
418 O s (λx.ha x + hb x + ∑_{i ∈[a x ,b x[ }(hp 〈i,x〉 + hf 〈i,x〉)) →
419 CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
421 (******************************** minimization ********************************)
423 axiom CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
424 CF sa a → CF sb b → CF sf f →
425 O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
426 CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
428 (************************************* smn ************************************)
429 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
431 (****************************** constructibility ******************************)
433 definition constructible ≝ λs. CF s s.
435 lemma constr_comp : ∀s1,s2. constructible s1 → constructible s2 →
436 (∀x. x ≤ s2 x) → constructible (s2 ∘ s1).
437 #s1 #s2 #Hs1 #Hs2 #Hle @(CF_comp … Hs1 Hs2) @O_plus @le_to_O #x [@Hle | //]
440 lemma ext_constr: ∀s1,s2. (∀x.s1 x = s2 x) →
441 constructible s1 → constructible s2.
442 #s1 #s2 #Hext #Hs1 @(ext_CF … Hext) @(monotonic_CF … Hs1) #x >Hext //
445 lemma constr_prim_rec: ∀s1,s2. constructible s1 → constructible s2 →
446 (∀n,r,m. 2 * r ≤ s2 〈n,〈r,m〉〉) → constructible (unary_pr s1 s2).
447 #s1 #s2 #Hs1 #Hs2 #Hincr @(CF_prim_rec … Hs1 Hs2) whd %{2} %{0}
448 #x #_ lapply (surj_pair x) * #a * #b #eqx >eqx whd in match (unary_pr ???);
450 whd in match (unary_pr ???); >fst_pair >snd_pair elim a
452 |#n #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair
453 >prim_rec_S @transitive_le [| @(monotonic_le_plus_l … Hind)]
454 @transitive_le [| @(monotonic_le_plus_l … (Hincr n ? b))]
455 whd in match (unary_pr ???); >fst_pair >snd_pair //
459 (********************************* simulation *********************************)
461 axiom sU : nat → nat.
463 axiom monotonic_sU: ∀i1,i2,x1,x2,s1,s2. i1 ≤ i2 → x1 ≤ x2 → s1 ≤ s2 →
464 sU 〈i1,〈x1,s1〉〉 ≤ sU 〈i2,〈x2,s2〉〉.
466 lemma monotonic_sU_aux : ∀x1,x2. fst x1 ≤ fst x2 → fst (snd x1) ≤ fst (snd x2) →
467 snd (snd x1) ≤ snd (snd x2) → sU x1 ≤ sU x2.
468 #x1 #x2 cases (surj_pair x1) #a1 * #y #eqx1 >eqx1 -eqx1 cases (surj_pair y)
469 #b1 * #c1 #eqy >eqy -eqy
470 cases (surj_pair x2) #a2 * #y2 #eqx2 >eqx2 -eqx2 cases (surj_pair y2)
471 #b2 * #c2 #eqy2 >eqy2 -eqy2 >fst_pair >snd_pair >fst_pair >snd_pair
472 >fst_pair >snd_pair >fst_pair >snd_pair @monotonic_sU
475 axiom sU_le: ∀i,x,s. s ≤ sU 〈i,〈x,s〉〉.
476 axiom sU_le_i: ∀i,x,s. MSC i ≤ sU 〈i,〈x,s〉〉.
477 axiom sU_le_x: ∀i,x,s. MSC x ≤ sU 〈i,〈x,s〉〉.
479 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
481 axiom CF_U : CF sU pU_unary.
483 definition termb_unary ≝ λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)).
484 definition out_unary ≝ λx:ℕ.out (fst x) (fst (snd x)) (snd (snd x)).
486 lemma CF_termb: CF sU termb_unary.
487 @(ext_CF (fst ∘ pU_unary)) [2: @CF_comp_fst @CF_U]
488 #n whd in ⊢ (??%?); whd in ⊢ (??(?%)?); >fst_pair %
491 lemma CF_out: CF sU out_unary.
492 @(ext_CF (snd ∘ pU_unary)) [2: @CF_comp_snd @CF_U]
493 #n whd in ⊢ (??%?); whd in ⊢ (??(?%)?); >snd_pair %
497 (******************** complexity of g ********************)
499 definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
501 λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
502 (out i (snd ux) (h (S i) (snd ux))).
504 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
505 #h #s #H1 @(CF_compS ? (auxg h) H1)
509 λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
510 ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
512 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
514 [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
517 lemma compl_g2 : ∀h,s1,s2,s.
519 (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
521 (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
522 O s (λx.MSC x + ∑_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
524 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
525 [#n whd in ⊢ (??%%); @eq_aux]
526 @(CF_max … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
527 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
530 lemma compl_g3 : ∀h,s.
531 CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
532 CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
533 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (proj1 … H))
534 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
537 definition min_input_aux ≝ λh,p.
538 μ_{y ∈ [S (fst p),snd (snd p)] }
539 ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
541 lemma min_input_eq : ∀h,p.
543 min_input h (fst p) (snd (snd p)).
544 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
545 whd in ⊢ (??%%); >fst_pair >snd_pair //
548 definition termb_aux ≝ λh.
549 termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
551 lemma compl_g4 : ∀h,s1,s.
553 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
554 (O s (λx.MSC x + ∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
555 CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
556 #h #s1 #s #Hs1 #HO @(ext_CF (min_input_aux h))
557 [#n whd in ⊢ (??%%); @min_input_eq]
558 @(CF_mu … MSC MSC … Hs1)
560 |@CF_comp_snd @CF_snd
561 |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
564 (************************* a couple of technical lemmas ***********************)
565 lemma minus_to_0: ∀a,b. a ≤ b → minus a b = 0.
566 #a elim a // #n #Hind *
567 [#H @False_ind /2 by absurd/ | #b normalize #H @Hind @le_S_S_to_le /2/]
570 lemma sigma_bound: ∀h,a,b. monotonic nat le h →
571 ∑_{i ∈ [a,S b[ }(h i) ≤ (S b-a)*h b.
572 #h #a #b #H cases (decidable_le a b)
573 [#leab cut (b = pred (S b - a + a))
574 [<plus_minus_m_m // @le_S //] #Hb >Hb in match (h b);
575 generalize in match (S b -a);
578 |#m #Hind >bigop_Strue [2://] @le_plus
579 [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
581 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
582 cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
586 lemma sigma_bound_decr: ∀h,a,b. (∀a1,a2. a1 ≤ a2 → a2 < b → h a2 ≤ h a1) →
587 ∑_{i ∈ [a,b[ }(h i) ≤ (b-a)*h a.
588 #h #a #b #H cases (decidable_le a b)
589 [#leab cut ((b -a) +a ≤ b) [/2 by le_minus_to_plus_r/] generalize in match (b -a);
592 |#m #Hind >bigop_Strue [2://] #Hm
593 cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
594 @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
596 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
597 cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
601 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
602 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
603 (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
604 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
605 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
608 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
609 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
610 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
611 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
614 (**************************** end of technical lemmas *************************)
616 lemma compl_g5 : ∀h,s1.(∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
618 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
619 CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
620 (λp:ℕ.min_input h (fst p) (snd (snd p))).
621 #h #s1 #Hmono #Hs1 @(compl_g4 … Hs1) @O_plus
622 [@O_plus_l // |@O_plus_r @coroll @Hmono]
626 constructible (λx. h (fst x) (snd x)) →
627 (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
628 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
629 #h #hconstr @(ext_CF (termb_aux h))
630 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
631 @(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
633 [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
635 [@(monotonic_CF … CF_fst) #x //
636 |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
637 [#n normalize >fst_pair >snd_pair %]
638 @(CF_comp … MSC …hconstr)
639 [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
640 |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
646 [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
647 [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
648 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
649 >distributive_times_plus @le_plus [//]
650 cases (surj_pair b) #c * #d #eqb >eqb
651 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
652 whd in ⊢ (??%); @le_plus
653 [@monotonic_MSC @(le_maxl … (le_n …))
654 |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
656 |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
660 |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
664 definition big : nat →nat ≝ λx.
665 let m ≝ max (fst x) (snd x) in 〈m,m〉.
667 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
668 #a #b normalize >fst_pair >snd_pair // qed.
670 lemma le_big : ∀x. x ≤ big x.
671 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
672 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
675 definition faux2 ≝ λh.
676 (λx.MSC x + (snd (snd x)-fst x)*
677 (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
680 constructible (λx. h (fst x) (snd x)) →
681 (∀n. monotonic ? le (h n)) →
682 CF (λx.MSC x + (snd (snd x)-fst x)*sU 〈max (fst x) (snd x),〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
683 (λp:ℕ.min_input h (fst p) (snd (snd p))).
684 #h #hcostr #hmono @(monotonic_CF … (faux2 h))
685 [#n normalize >fst_pair >snd_pair //]
686 @compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
687 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
691 constructible (λx. h (fst x) (snd x)) →
692 (∀n. monotonic ? le (h n)) →
693 CF (λx.MSC (big x) + (snd (snd x)-fst x)*sU 〈max (fst x) (snd x),〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
694 (λp:ℕ.min_input h (fst p) (snd (snd p))).
695 #h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x
696 @le_plus [@monotonic_MSC //]
697 cases (decidable_le (fst x) (snd(snd x)))
698 [#Hle @le_times // @monotonic_sU
699 |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
703 definition out_aux ≝ λh.
704 out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
707 constructible (λx. h (fst x) (snd x)) →
708 (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
709 (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
710 #h #hconstr @(ext_CF (out_aux h))
711 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
712 @(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
714 [@(monotonic_CF … CF_fst) #x //
716 [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
717 |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
718 [#n normalize >fst_pair >snd_pair %]
719 @(CF_comp … MSC …hconstr)
720 [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
721 |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
728 |@(O_trans … (λx.MSC (max (fst x) (snd x))))
729 [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
730 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
731 whd in ⊢ (??%); @le_plus
732 [@monotonic_MSC @(le_maxl … (le_n …))
733 |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
735 |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
738 |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
743 constructible (λx. h (fst x) (snd x)) →
744 (∀n. monotonic ? le (h n)) →
745 (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
746 CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
747 (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
749 #h #hconstr #hmono #hantimono
750 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
752 [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
753 [// | @monotonic_MSC // ]]
754 @(O_trans … (coroll2 ??))
755 [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
756 cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
758 [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
759 cut (max b n = n) [normalize >le_to_leb_true //] #maxb
761 [@le_plus [>big_def >big_def >maxa >maxb //]
763 [/2 by monotonic_le_minus_r/
764 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
766 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
768 |@le_to_O #n >fst_pair >snd_pair
769 cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
770 >associative_plus >distributive_times_plus
771 @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
775 definition sg ≝ λh,x.
776 (S (snd x-fst x))*MSC 〈x,x〉 + (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉.
778 lemma sg_def : ∀h,a,b.
779 sg h 〈a,b〉 = (S (b-a))*MSC 〈〈a,b〉,〈a,b〉〉 +
780 (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
781 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
784 lemma compl_g11 : ∀h.
785 constructible (λx. h (fst x) (snd x)) →
786 (∀n. monotonic ? le (h n)) →
787 (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
788 CF (sg h) (unary_g h).
789 #h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)
792 (**************************** closing the argument ****************************)
794 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
797 | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
798 d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
800 lemma h_of_aux_O: ∀r,c,b.
801 h_of_aux r c O b = c.
804 lemma h_of_aux_S : ∀r,c,d,b.
805 h_of_aux r c (S d) b =
806 (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
807 (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
810 lemma h_of_aux_prim_rec : ∀r,c,n,b. h_of_aux r c n b =
812 (λx.let d ≝ S(fst x) in
813 let b ≝ snd (snd x) in
814 (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
815 d*(S d)*sU 〈〈b-d,b〉,〈b,r (fst (snd x))〉〉) n b.
817 [>h_of_aux_O normalize //
818 |#n1 #Hind >h_of_aux_S >prim_rec_S >snd_pair >snd_pair >fst_pair
823 lemma h_of_aux_constr :
824 ∀r,c. constructible (λx.h_of_aux r c (fst x) (snd x)).
828 (λx.let d ≝ S(fst x) in
829 let b ≝ snd (snd x) in
830 (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
831 d*(S d)*sU 〈〈b-d,b〉,〈b,r (fst (snd x))〉〉)))
832 [#n @sym_eq whd in match (unary_pr ???); @h_of_aux_prim_rec
835 definition h_of ≝ λr,p.
836 let m ≝ max (fst p) (snd p) in
837 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
839 lemma h_of_O: ∀r,a,b. b ≤ a →
840 h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
841 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
844 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
846 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
847 #r #a #b normalize >fst_pair >snd_pair //
850 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
851 ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
852 h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
853 #r #Hr #monor #d #d1 lapply d -d elim d1
854 [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
855 >h_of_aux_O >h_of_aux_O //
856 |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
857 [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
858 >h_of_aux_S @(transitive_le ???? (le_plus_n …))
859 >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
860 >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
861 |#Hd >Hd >h_of_aux_S >h_of_aux_S
862 cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
863 @le_plus [@le_times //]
864 [@monotonic_MSC @le_pair @le_pair //
865 |@le_times [//] @monotonic_sU
866 [@le_pair // |// |@monor @Hind //]
872 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
873 ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
874 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
875 cut (max i a ≤ max i b)
877 [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
878 #Hmax @(mono_h_of_aux r Hr Hmono)
879 [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
882 axiom h_of_constr : ∀r:nat →nat.
883 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
884 constructible (h_of r).
886 lemma speed_compl: ∀r:nat →nat.
887 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
888 CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
889 #r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …))
890 [#x cases (surj_pair x) #a * #b #eqx >eqx
891 >sg_def cases (decidable_le b a)
892 [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
893 <plus_n_O <plus_n_O >h_of_def
895 [normalize cases (le_to_or_lt_eq … leba)
896 [#ltba >(lt_to_leb_false … ltba) %
897 |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
898 #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
899 @monotonic_MSC @le_pair @le_pair //
900 |#ltab >h_of_def >h_of_def
902 [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
904 cut (max (S a) b = b)
905 [whd in ⊢ (??%?); >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
908 [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
910 cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
912 [@plus_to_minus >commutative_plus @minus_to_plus
913 [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
916 |#n #a #b #leab #lebn >h_of_def >h_of_def
918 [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
920 [normalize >(le_to_leb_true … lebn) %] #Hmaxb
921 >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
922 |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
923 |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
924 [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]
925 @(h_of_constr r Hr Hmono Hconstr)
929 lemma speed_compl_i: ∀r:nat →nat.
930 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
931 ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
932 #r #Hr #Hmono #Hconstr #i
933 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
934 [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
935 @smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //
938 (**************************** the speedup theorem *****************************)
939 theorem pseudo_speedup:
940 ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
941 ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
942 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
943 #r #Hr #Hmono #Hconstr
944 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
945 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
947 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
948 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
949 (* sg is (λx.h_of r 〈i,x〉) *)
950 %{(λx. h_of r 〈S i,x〉)}
951 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
952 %[%[@condition_1 |@Hg]
953 |cases Hg #H1 * #j * #Hcodej #HCj
954 lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
955 cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
956 @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
957 [@(transitive_le … ltin) @(le_maxl … (le_n …))]
958 cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
959 #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
963 theorem pseudo_speedup':
964 ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
965 ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
966 (* ¬ O (r ∘ sg) sf. *)
967 ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
968 #r #Hr #Hmono #Hconstr
969 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
970 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
972 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
973 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
974 (* sg is (λx.h_of r 〈i,x〉) *)
975 %{(λx. h_of r 〈S i,x〉)}
976 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
977 %[%[@condition_1 |@Hg]
978 |cases Hg #H1 * #j * #Hcodej #HCj
979 lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
980 cases HCi #m * #a #Ha
981 %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2 #Hlesf
982 %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
983 cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
984 #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
985 @Hmono @(mono_h_of2 … Hr Hmono … ltin)