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".
8 (************************* notation for minimization *****************************)
9 notation "μ_{ ident i < n } p"
10 with precedence 80 for @{min $n 0 (λ${ident i}.$p)}.
12 notation "μ_{ ident i ≤ n } p"
13 with precedence 80 for @{min (S $n) 0 (λ${ident i}.$p)}.
15 notation "μ_{ ident i ∈ [a,b[ } p"
16 with precedence 80 for @{min ($b-$a) $a (λ${ident i}.$p)}.
18 notation "μ_{ ident i ∈ [a,b] } p"
19 with precedence 80 for @{min (S $b-$a) $a (λ${ident i}.$p)}.
21 (************************************ MAX *************************************)
22 notation "Max_{ ident i < n | p } f"
24 for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
26 notation "Max_{ ident i < n } f"
28 for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}.
30 notation "Max_{ ident j ∈ [a,b[ } f"
32 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
33 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
35 notation "Max_{ ident j ∈ [a,b[ | p } f"
37 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
38 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
40 lemma Max_assoc: ∀a,b,c. max (max a b) c = max a (max b c).
41 #a #b #c normalize cases (true_or_false (leb a b)) #leab >leab normalize
42 [cases (true_or_false (leb b c )) #lebc >lebc normalize
43 [>(le_to_leb_true a c) // @(transitive_le ? b) @leb_true_to_le //
46 |cases (true_or_false (leb b c )) #lebc >lebc normalize //
47 >leab normalize >(not_le_to_leb_false a c) // @lt_to_not_le
48 @(transitive_lt ? b) @not_le_to_lt @leb_false_to_not_le //
52 lemma Max0 : ∀n. max 0 n = n.
55 lemma Max0r : ∀n. max n 0 = n.
56 #n >commutative_max //
60 mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)).
62 definition MaxAC ≝ mk_ACop nat 0 MaxA commutative_max.
64 lemma le_Max: ∀f,p,n,a. a < n → p a = true →
65 f a ≤ Max_{i < n | p i}(f i).
67 >(bigop_diff p ? 0 MaxAC f a n) // @(le_maxl … (le_n ?))
70 lemma le_MaxI: ∀f,p,n,m,a. m ≤ a → a < n → p a = true →
71 f a ≤ Max_{i ∈ [m,n[ | p i}(f i).
72 #f #p #n #m #a #lema #ltan #pa
73 >(bigop_diff ? ? 0 MaxAC (λi.f (i+m)) (a-m) (n-m))
74 [<plus_minus_m_m // @(le_maxl … (le_n ?))
76 |/2 by monotonic_lt_minus_l/
80 lemma Max_le: ∀f,p,n,b.
81 (∀a.a < n → p a = true → f a ≤ b) → Max_{i < n | p i}(f i) ≤ b.
82 #f #p #n elim n #b #H //
83 #b0 #H1 cases (true_or_false (p b)) #Hb
84 [>bigop_Strue [2:@Hb] @to_max [@H1 // | @H #a #ltab #pa @H1 // @le_S //]
85 |>bigop_Sfalse [2:@Hb] @H #a #ltab #pa @H1 // @le_S //
89 (********************************** pairing ***********************************)
90 axiom pair: nat → nat → nat.
91 axiom fst : nat → nat.
92 axiom snd : nat → nat.
94 interpretation "abstract pair" 'pair f g = (pair f g).
96 axiom fst_pair: ∀a,b. fst 〈a,b〉 = a.
97 axiom snd_pair: ∀a,b. snd 〈a,b〉 = b.
98 axiom surj_pair: ∀x. ∃a,b. x = 〈a,b〉.
100 axiom le_fst : ∀p. fst p ≤ p.
101 axiom le_snd : ∀p. snd p ≤ p.
102 axiom le_pair: ∀a,a1,b,b1. a ≤ a1 → b ≤ b1 → 〈a,b〉 ≤ 〈a1,b1〉.
104 (************************************* U **************************************)
105 axiom U: nat → nat →nat → option nat.
107 axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
108 U i x n = Some ? y → U i x m = Some ? y.
110 lemma unique_U: ∀i,x,n,m,yn,ym.
111 U i x n = Some ? yn → U i x m = Some ? ym → yn = ym.
112 #i #x #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
113 [#lenm lapply (monotonic_U … lenm Hn) >Hm #HS destruct (HS) //
114 |#ltmn lapply (monotonic_U … n … Hm) [@lt_to_le @not_le_to_lt //]
115 >Hn #HS destruct (HS) //
119 definition code_for ≝ λf,i.∀x.
120 ∃n.∀m. n ≤ m → U i x m = f x.
122 definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y.
124 notation "{i ⊙ x} ↓ r" with precedence 60 for @{terminate $i $x $r}.
126 lemma terminate_dec: ∀i,x,n. {i ⊙ x} ↓ n ∨ ¬ {i ⊙ x} ↓ n.
127 #i #x #n normalize cases (U i x n)
128 [%2 % * #y #H destruct|#y %1 %{y} //]
131 lemma monotonic_terminate: ∀i,x,n,m.
132 n ≤ m → {i ⊙ x} ↓ n → {i ⊙ x} ↓ m.
133 #i #x #n #m #lenm * #z #H %{z} @(monotonic_U … H) //
136 definition termb ≝ λi,x,t.
137 match U i x t with [None ⇒ false |Some y ⇒ true].
139 lemma termb_true_to_term: ∀i,x,t. termb i x t = true → {i ⊙ x} ↓ t.
140 #i #x #t normalize cases (U i x t) normalize [#H destruct | #y #_ %{y} //]
143 lemma term_to_termb_true: ∀i,x,t. {i ⊙ x} ↓ t → termb i x t = true.
144 #i #x #t * #y #H normalize >H //
147 definition out ≝ λi,x,r.
148 match U i x r with [ None ⇒ 0 | Some z ⇒ z].
150 definition bool_to_nat: bool → nat ≝
151 λb. match b with [true ⇒ 1 | false ⇒ 0].
153 coercion bool_to_nat.
155 definition pU : nat → nat → nat → nat ≝ λi,x,r.〈termb i x r,out i x r〉.
157 lemma pU_vs_U_Some : ∀i,x,r,y. pU i x r = 〈1,y〉 ↔ U i x r = Some ? y.
158 #i #x #r #y % normalize
159 [cases (U i x r) normalize
160 [#H cut (0=1) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H @H]
162 |#a #H cut (a=y) [lapply (eq_f … snd … H) >snd_pair >snd_pair #H1 @H1]
168 lemma pU_vs_U_None : ∀i,x,r. pU i x r = 〈0,0〉 ↔ U i x r = None ?.
170 [cases (U i x r) normalize //
171 #a #H cut (1=0) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H1 @H1]
176 lemma fst_pU: ∀i,x,r. fst (pU i x r) = termb i x r.
177 #i #x #r normalize cases (U i x r) normalize >fst_pair //
180 lemma snd_pU: ∀i,x,r. snd (pU i x r) = out i x r.
181 #i #x #r normalize cases (U i x r) normalize >snd_pair //
184 (********************************* the speedup ********************************)
186 definition min_input ≝ λh,i,x. μ_{y ∈ [S i,x] } (termb i y (h (S i) y)).
188 lemma min_input_def : ∀h,i,x.
189 min_input h i x = min (x -i) (S i) (λy.termb i y (h (S i) y)).
192 lemma min_input_i: ∀h,i,x. x ≤ i → min_input h i x = S i.
193 #h #i #x #lexi >min_input_def
194 cut (x - i = 0) [@sym_eq /2 by eq_minus_O/] #Hcut //
197 lemma min_input_to_terminate: ∀h,i,x.
198 min_input h i x = x → {i ⊙ x} ↓ (h (S i) x).
200 cases (decidable_le (S i) x) #Hix
201 [cases (true_or_false (termb i x (h (S i) x))) #Hcase
202 [@termb_true_to_term //
203 |<Hminx in Hcase; #H lapply (fmin_false (λx.termb i x (h (S i) x)) (x-i) (S i) H)
204 >min_input_def in Hminx; #Hminx >Hminx in ⊢ (%→?);
205 <plus_n_Sm <plus_minus_m_m [2: @lt_to_le //]
208 |@False_ind >min_input_i in Hminx;
209 [#eqix >eqix in Hix; * /2/ | @le_S_S_to_le @not_le_to_lt //]
213 lemma min_input_to_lt: ∀h,i,x.
214 min_input h i x = x → i < x.
215 #h #i #x #Hminx cases (decidable_le (S i) x) //
216 #ltxi @False_ind >min_input_i in Hminx;
217 [#eqix >eqix in ltxi; * /2/ | @le_S_S_to_le @not_le_to_lt //]
220 lemma le_to_min_input: ∀h,i,x,x1. x ≤ x1 →
221 min_input h i x = x → min_input h i x1 = x.
222 #h #i #x #x1 #lex #Hminx @(min_exists … (le_S_S … lex))
223 [@(fmin_true … (sym_eq … Hminx)) //
224 |@(min_input_to_lt … Hminx)
225 |#j #H1 <Hminx @lt_min_to_false //
226 |@plus_minus_m_m @le_S_S @(transitive_le … lex) @lt_to_le
227 @(min_input_to_lt … Hminx)
231 definition g ≝ λh,u,x.
232 S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
234 lemma g_def : ∀h,u,x. g h u x =
235 S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
238 lemma le_u_to_g_1 : ∀h,u,x. x ≤ u → g h u x = 1.
239 #h #u #x #lexu >g_def cut (x-u = 0) [/2 by minus_le_minus_minus_comm/]
240 #eq0 >eq0 normalize // qed.
242 lemma g_lt : ∀h,i,x. min_input h i x = x →
243 out i x (h (S i) x) < g h 0 x.
244 #h #i #x #H @le_S_S @(le_MaxI … i) /2 by min_input_to_lt/
247 lemma max_neq0 : ∀a,b. max a b ≠ 0 → a ≠ 0 ∨ b ≠ 0.
248 #a #b whd in match (max a b); cases (true_or_false (leb a b)) #Hcase >Hcase
249 [#H %2 @H | #H %1 @H]
252 definition almost_equal ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
253 interpretation "almost equal" 'napart f g = (almost_equal f g).
255 lemma eventually_cancelled: ∀h,u.¬∀nu.∃x. nu < x ∧
256 max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) ≠ 0.
258 [normalize % #H cases (H u) #x * #_ * #H1 @H1 //
259 |#u0 @not_to_not #Hind #nu cases (Hind nu) #x * #ltx
260 cases (true_or_false (eqb (min_input h (u0+O) x) x)) #Hcase
261 [>bigop_Strue [2:@Hcase] #Hmax cases (max_neq0 … Hmax) -Hmax
262 [2: #H %{x} % // <minus_n_O @H]
263 #Hneq0 (* if x is not enough we retry with nu=x *)
264 cases (Hind x) #x1 * #ltx1
266 [#H %{x1} % [@transitive_lt //| <minus_n_O @H]
267 |@not_eq_to_eqb_false >(le_to_min_input … (eqb_true_to_eq … Hcase))
268 [@lt_to_not_eq @ltx1 | @lt_to_le @ltx1]
270 |>bigop_Sfalse [2:@Hcase] #H %{x} % // <minus_n_O @H
275 lemma condition_1: ∀h,u.g h 0 ≈ g h u.
276 #h #u @(not_to_not … (eventually_cancelled h u))
277 #H #nu cases (H (max u nu)) #x * #ltx #Hdiff
278 %{x} % [@(le_to_lt_to_lt … ltx) @(le_maxr … (le_n …))] @(not_to_not … Hdiff)
279 #H @(eq_f ?? S) >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat 0 MaxA)
280 [>H // |@lt_to_le @(le_to_lt_to_lt …ltx) /2 by le_maxr/ |//]
283 (******************************** Condition 2 *********************************)
284 definition total ≝ λf.λx:nat. Some nat (f x).
286 lemma exists_to_exists_min: ∀h,i. (∃x. i < x ∧ {i ⊙ x} ↓ h (S i) x) → ∃y. min_input h i y = y.
287 #h #i * #x * #ltix #Hx %{(min_input h i x)} @min_spec_to_min @found //
288 [@(f_min_true (λy:ℕ.termb i y (h (S i) y))) %{x} % [% // | @term_to_termb_true //]
289 |#y #leiy #lty @(lt_min_to_false ????? lty) //
293 lemma condition_2: ∀h,i. code_for (total (g h 0)) i → ¬∃x. i<x ∧ {i ⊙ x} ↓ h (S i) x.
294 #h #i whd in ⊢(%→?); #H % #H1 cases (exists_to_exists_min … H1) #y #Hminy
295 lapply (g_lt … Hminy)
296 lapply (min_input_to_terminate … Hminy) * #r #termy
297 cases (H y) -H #ny #Hy
298 cut (r = g h 0 y) [@(unique_U … ny … termy) @Hy //] #Hr
299 whd in match (out ???); >termy >Hr
300 #H @(absurd ? H) @le_to_not_lt @le_n
304 (********************************* complexity *********************************)
306 (* We assume operations have a minimal structural complexity MSC.
307 For instance, for time complexity, MSC is equal to the size of input.
308 For space complexity, MSC is typically 0, since we only measure the
309 space required in addition to dimension of the input. *)
311 axiom MSC : nat → nat.
312 axiom MSC_le: ∀n. MSC n ≤ n.
313 axiom monotonic_MSC: monotonic ? le MSC.
314 axiom MSC_pair: ∀a,b. MSC 〈a,b〉 ≤ MSC a + MSC b.
316 (* C s i means i is running in O(s) *)
318 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ x → ∃y.
319 U i x (c*(s x)) = Some ? y.
321 (* C f s means f ∈ O(s) where MSC ∈O(s) *)
322 definition CF ≝ λs,f.O s MSC ∧ ∃i.code_for (total f) i ∧ C s i.
324 lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
325 #f #g #s #Hext * #HO * #i * #Hcode #HC % // %{i} %
326 [#x cases (Hcode x) #a #H %{a} whd in match (total ??); <Hext @H | //]
329 lemma monotonic_CF: ∀s1,s2,f.(∀x. s1 x ≤ s2 x) → CF s1 f → CF s2 f.
330 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
331 [cases HO #c * #a -HO #HO %{c} %{a} #n #lean @(transitive_le … (HO n lean))
333 |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1 %{c} %{a} #n #lean
334 cases(Hs1 n lean) #y #Hy %{y} @(monotonic_U …Hy) @le_times //
338 lemma O_to_CF: ∀s1,s2,f.O s2 s1 → CF s1 f → CF s2 f.
339 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
341 |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1
342 cases H #c1 * #a1 #Ha1 %{(c*c1)} %{(a+a1)} #n #lean
343 cases(Hs1 n ?) [2:@(transitive_le … lean) //] #y #Hy %{y} @(monotonic_U …Hy)
344 >associative_times @le_times // @Ha1 @(transitive_le … lean) //
348 lemma timesc_CF: ∀s,f,c.CF (λx.c*s x) f → CF s f.
349 #s #f #c @O_to_CF @O_times_c
352 (********************************* composition ********************************)
353 axiom CF_comp: ∀f,g,sf,sg,sh. CF sg g → CF sf f →
354 O sh (λx. sg x + sf (g x)) → CF sh (f ∘ g).
356 lemma CF_comp_ext: ∀f,g,h,sh,sf,sg. CF sg g → CF sf f →
357 (∀x.f(g x) = h x) → O sh (λx. sg x + sf (g x)) → CF sh h.
358 #f #g #h #sh #sf #sg #Hg #Hf #Heq #H @(ext_CF (f ∘ g))
359 [#n normalize @Heq | @(CF_comp … H) //]
362 (* primitve recursion *)
364 let rec prim_rec (k,h:nat →nat) n m on n ≝
367 | S a ⇒ h 〈a,〈prim_rec k h a m, m〉〉].
369 lemma prim_rec_S: ∀k,h,n,m.
370 prim_rec k h (S n) m = h 〈n,〈prim_rec k h n m, m〉〉.
373 definition unary_pr ≝ λk,h,x. prim_rec k h (fst x) (snd x).
375 let rec prim_rec_compl (k,h,sk,sh:nat →nat) n m on n ≝
378 | S a ⇒ prim_rec_compl k h sk sh a m + sh (prim_rec k h a m)].
380 axiom CF_prim_rec: ∀k,h,sk,sh,sf. CF sk k → CF sh h →
381 O sf (unary_pr sk (λx. fst (snd x) + sh 〈fst x,〈unary_pr k h 〈fst x,snd (snd x)〉,snd (snd x)〉〉))
382 → CF sf (unary_pr k h).
385 lemma prim_rec_O: ∀k1,h1,k2,h2. O k1 k2 → O h1 h2 →
386 O (unary_pr k1 h1) (unary_pr k2 h2).
387 #k1 #h1 #k2 #h2 #HO1 #HO2 whd *)
390 (**************************** primitive operations*****************************)
392 definition id ≝ λx:nat.x.
394 axiom CF_id: CF MSC id.
395 axiom CF_compS: ∀h,f. CF h f → CF h (S ∘ f).
396 axiom CF_comp_fst: ∀h,f. CF h f → CF h (fst ∘ f).
397 axiom CF_comp_snd: ∀h,f. CF h f → CF h (snd ∘ f).
398 axiom CF_comp_pair: ∀h,f,g. CF h f → CF h g → CF h (λx. 〈f x,g x〉).
400 lemma CF_fst: CF MSC fst.
401 @(ext_CF (fst ∘ id)) [#n //] @(CF_comp_fst … CF_id)
404 lemma CF_snd: CF MSC snd.
405 @(ext_CF (snd ∘ id)) [#n //] @(CF_comp_snd … CF_id)
408 (************************************** eqb ***********************************)
410 axiom CF_eqb: ∀h,f,g.
411 CF h f → CF h g → CF h (λx.eqb (f x) (g x)).
413 (*********************************** maximum **********************************)
415 axiom CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
416 CF ha a → CF hb b → CF hp p → CF hf f →
417 O s (λx.ha x + hb x + ∑_{i ∈[a x ,b x[ }(hp 〈i,x〉 + hf 〈i,x〉)) →
418 CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
420 (******************************** minimization ********************************)
422 axiom CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
423 CF sa a → CF sb b → CF sf f →
424 O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
425 CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
427 (************************************* smn ************************************)
428 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
430 (****************************** constructibility ******************************)
432 definition constructible ≝ λs. CF s s.
434 lemma constr_comp : ∀s1,s2. constructible s1 → constructible s2 →
435 (∀x. x ≤ s2 x) → constructible (s2 ∘ s1).
436 #s1 #s2 #Hs1 #Hs2 #Hle @(CF_comp … Hs1 Hs2) @O_plus @le_to_O #x [@Hle | //]
439 lemma ext_constr: ∀s1,s2. (∀x.s1 x = s2 x) →
440 constructible s1 → constructible s2.
441 #s1 #s2 #Hext #Hs1 @(ext_CF … Hext) @(monotonic_CF … Hs1) #x >Hext //
444 lemma constr_prim_rec: ∀s1,s2. constructible s1 → constructible s2 →
445 (∀n,r,m. 2 * r ≤ s2 〈n,〈r,m〉〉) → constructible (unary_pr s1 s2).
446 #s1 #s2 #Hs1 #Hs2 #Hincr @(CF_prim_rec … Hs1 Hs2) whd %{2} %{0}
447 #x #_ lapply (surj_pair x) * #a * #b #eqx >eqx whd in match (unary_pr ???);
449 whd in match (unary_pr ???); >fst_pair >snd_pair elim a
451 |#n #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair
452 >prim_rec_S @transitive_le [| @(monotonic_le_plus_l … Hind)]
453 @transitive_le [| @(monotonic_le_plus_l … (Hincr n ? b))]
454 whd in match (unary_pr ???); >fst_pair >snd_pair //
458 (********************************* simulation *********************************)
460 axiom sU : nat → nat.
462 axiom monotonic_sU: ∀i1,i2,x1,x2,s1,s2. i1 ≤ i2 → x1 ≤ x2 → s1 ≤ s2 →
463 sU 〈i1,〈x1,s1〉〉 ≤ sU 〈i2,〈x2,s2〉〉.
465 lemma monotonic_sU_aux : ∀x1,x2. fst x1 ≤ fst x2 → fst (snd x1) ≤ fst (snd x2) →
466 snd (snd x1) ≤ snd (snd x2) → sU x1 ≤ sU x2.
467 #x1 #x2 cases (surj_pair x1) #a1 * #y #eqx1 >eqx1 -eqx1 cases (surj_pair y)
468 #b1 * #c1 #eqy >eqy -eqy
469 cases (surj_pair x2) #a2 * #y2 #eqx2 >eqx2 -eqx2 cases (surj_pair y2)
470 #b2 * #c2 #eqy2 >eqy2 -eqy2 >fst_pair >snd_pair >fst_pair >snd_pair
471 >fst_pair >snd_pair >fst_pair >snd_pair @monotonic_sU
474 axiom sU_le: ∀i,x,s. s ≤ sU 〈i,〈x,s〉〉.
475 axiom sU_le_i: ∀i,x,s. MSC i ≤ sU 〈i,〈x,s〉〉.
476 axiom sU_le_x: ∀i,x,s. MSC x ≤ sU 〈i,〈x,s〉〉.
478 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
480 axiom CF_U : CF sU pU_unary.
482 definition termb_unary ≝ λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)).
483 definition out_unary ≝ λx:ℕ.out (fst x) (fst (snd x)) (snd (snd x)).
485 lemma CF_termb: CF sU termb_unary.
486 @(ext_CF (fst ∘ pU_unary)) [2: @CF_comp_fst @CF_U]
487 #n whd in ⊢ (??%?); whd in ⊢ (??(?%)?); >fst_pair %
490 lemma CF_out: CF sU out_unary.
491 @(ext_CF (snd ∘ pU_unary)) [2: @CF_comp_snd @CF_U]
492 #n whd in ⊢ (??%?); whd in ⊢ (??(?%)?); >snd_pair %
496 (******************** complexity of g ********************)
498 definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
500 λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
501 (out i (snd ux) (h (S i) (snd ux))).
503 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
504 #h #s #H1 @(CF_compS ? (auxg h) H1)
508 λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
509 ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
511 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
513 [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
516 lemma compl_g2 : ∀h,s1,s2,s.
518 (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
520 (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
521 O s (λx.MSC x + ∑_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
523 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
524 [#n whd in ⊢ (??%%); @eq_aux]
525 @(CF_max … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
526 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
529 lemma compl_g3 : ∀h,s.
530 CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
531 CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
532 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (proj1 … H))
533 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
536 definition min_input_aux ≝ λh,p.
537 μ_{y ∈ [S (fst p),snd (snd p)] }
538 ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
540 lemma min_input_eq : ∀h,p.
542 min_input h (fst p) (snd (snd p)).
543 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
544 whd in ⊢ (??%%); >fst_pair >snd_pair //
547 definition termb_aux ≝ λh.
548 termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
550 lemma compl_g4 : ∀h,s1,s.
552 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
553 (O s (λx.MSC x + ∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
554 CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
555 #h #s1 #s #Hs1 #HO @(ext_CF (min_input_aux h))
556 [#n whd in ⊢ (??%%); @min_input_eq]
557 @(CF_mu … MSC MSC … Hs1)
559 |@CF_comp_snd @CF_snd
560 |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
563 (************************* a couple of technical lemmas ***********************)
564 lemma minus_to_0: ∀a,b. a ≤ b → minus a b = 0.
565 #a elim a // #n #Hind *
566 [#H @False_ind /2 by absurd/ | #b normalize #H @Hind @le_S_S_to_le /2/]
569 lemma sigma_bound: ∀h,a,b. monotonic nat le h →
570 ∑_{i ∈ [a,S b[ }(h i) ≤ (S b-a)*h b.
571 #h #a #b #H cases (decidable_le a b)
572 [#leab cut (b = pred (S b - a + a))
573 [<plus_minus_m_m // @le_S //] #Hb >Hb in match (h b);
574 generalize in match (S b -a);
577 |#m #Hind >bigop_Strue [2://] @le_plus
578 [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
580 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
581 cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
585 lemma sigma_bound_decr: ∀h,a,b. (∀a1,a2. a1 ≤ a2 → a2 < b → h a2 ≤ h a1) →
586 ∑_{i ∈ [a,b[ }(h i) ≤ (b-a)*h a.
587 #h #a #b #H cases (decidable_le a b)
588 [#leab cut ((b -a) +a ≤ b) [/2 by le_minus_to_plus_r/] generalize in match (b -a);
591 |#m #Hind >bigop_Strue [2://] #Hm
592 cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
593 @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
595 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
596 cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
600 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
601 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
602 (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
603 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
604 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
607 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
608 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
609 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
610 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
613 (**************************** end of technical lemmas *************************)
615 lemma compl_g5 : ∀h,s1.(∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
617 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
618 CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
619 (λp:ℕ.min_input h (fst p) (snd (snd p))).
620 #h #s1 #Hmono #Hs1 @(compl_g4 … Hs1) @O_plus
621 [@O_plus_l // |@O_plus_r @coroll @Hmono]
625 constructible (λx. h (fst x) (snd x)) →
626 (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
627 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
628 #h #hconstr @(ext_CF (termb_aux h))
629 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
630 @(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
632 [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
634 [@(monotonic_CF … CF_fst) #x //
635 |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
636 [#n normalize >fst_pair >snd_pair %]
637 @(CF_comp … MSC …hconstr)
638 [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
639 |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
645 [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
646 [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
647 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
648 >distributive_times_plus @le_plus [//]
649 cases (surj_pair b) #c * #d #eqb >eqb
650 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
651 whd in ⊢ (??%); @le_plus
652 [@monotonic_MSC @(le_maxl … (le_n …))
653 |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
655 |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
659 |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
663 definition big : nat →nat ≝ λx.
664 let m ≝ max (fst x) (snd x) in 〈m,m〉.
666 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
667 #a #b normalize >fst_pair >snd_pair // qed.
669 lemma le_big : ∀x. x ≤ big x.
670 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
671 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
674 definition faux2 ≝ λh.
675 (λx.MSC x + (snd (snd x)-fst x)*
676 (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
679 constructible (λx. h (fst x) (snd x)) →
680 (∀n. monotonic ? le (h n)) →
681 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))〉〉)
682 (λp:ℕ.min_input h (fst p) (snd (snd p))).
683 #h #hcostr #hmono @(monotonic_CF … (faux2 h))
684 [#n normalize >fst_pair >snd_pair //]
685 @compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
686 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
690 constructible (λx. h (fst x) (snd x)) →
691 (∀n. monotonic ? le (h n)) →
692 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))〉〉)
693 (λp:ℕ.min_input h (fst p) (snd (snd p))).
694 #h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x
695 @le_plus [@monotonic_MSC //]
696 cases (decidable_le (fst x) (snd(snd x)))
697 [#Hle @le_times // @monotonic_sU
698 |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
702 definition out_aux ≝ λh.
703 out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
706 constructible (λx. h (fst x) (snd x)) →
707 (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
708 (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
709 #h #hconstr @(ext_CF (out_aux h))
710 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
711 @(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
713 [@(monotonic_CF … CF_fst) #x //
715 [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
716 |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
717 [#n normalize >fst_pair >snd_pair %]
718 @(CF_comp … MSC …hconstr)
719 [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
720 |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
727 |@(O_trans … (λx.MSC (max (fst x) (snd x))))
728 [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
729 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
730 whd in ⊢ (??%); @le_plus
731 [@monotonic_MSC @(le_maxl … (le_n …))
732 |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
734 |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
737 |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
742 constructible (λx. h (fst x) (snd x)) →
743 (∀n. monotonic ? le (h n)) →
744 (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
745 CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
746 (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
748 #h #hconstr #hmono #hantimono
749 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
751 [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
752 [// | @monotonic_MSC // ]]
753 @(O_trans … (coroll2 ??))
754 [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
755 cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
757 [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
758 cut (max b n = n) [normalize >le_to_leb_true //] #maxb
760 [@le_plus [>big_def >big_def >maxa >maxb //]
762 [/2 by monotonic_le_minus_r/
763 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
765 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
767 |@le_to_O #n >fst_pair >snd_pair
768 cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
769 >associative_plus >distributive_times_plus
770 @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
774 definition sg ≝ λh,x.
775 (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)〉〉.
777 lemma sg_def : ∀h,a,b.
778 sg h 〈a,b〉 = (S (b-a))*MSC 〈〈a,b〉,〈a,b〉〉 +
779 (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
780 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
783 lemma compl_g11 : ∀h.
784 constructible (λx. h (fst x) (snd x)) →
785 (∀n. monotonic ? le (h n)) →
786 (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
787 CF (sg h) (unary_g h).
788 #h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)
791 (**************************** closing the argument ****************************)
793 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
796 | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
797 d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
799 lemma h_of_aux_O: ∀r,c,b.
800 h_of_aux r c O b = c.
803 lemma h_of_aux_S : ∀r,c,d,b.
804 h_of_aux r c (S d) b =
805 (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
806 (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
809 lemma h_of_aux_prim_rec : ∀r,c,n,b. h_of_aux r c n b =
811 (λx.let d ≝ S(fst x) in
812 let b ≝ snd (snd x) in
813 (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
814 d*(S d)*sU 〈〈b-d,b〉,〈b,r (fst (snd x))〉〉) n b.
816 [>h_of_aux_O normalize //
817 |#n1 #Hind >h_of_aux_S >prim_rec_S >snd_pair >snd_pair >fst_pair
822 lemma h_of_aux_constr :
823 ∀r,c. constructible (λx.h_of_aux r c (fst x) (snd x)).
827 (λx.let d ≝ S(fst x) in
828 let b ≝ snd (snd x) in
829 (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
830 d*(S d)*sU 〈〈b-d,b〉,〈b,r (fst (snd x))〉〉)))
831 [#n @sym_eq whd in match (unary_pr ???); @h_of_aux_prim_rec
834 definition h_of ≝ λr,p.
835 let m ≝ max (fst p) (snd p) in
836 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
838 lemma h_of_O: ∀r,a,b. b ≤ a →
839 h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
840 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
843 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
845 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
846 #r #a #b normalize >fst_pair >snd_pair //
849 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
850 ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
851 h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
852 #r #Hr #monor #d #d1 lapply d -d elim d1
853 [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
854 >h_of_aux_O >h_of_aux_O //
855 |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
856 [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
857 >h_of_aux_S @(transitive_le ???? (le_plus_n …))
858 >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
859 >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
860 |#Hd >Hd >h_of_aux_S >h_of_aux_S
861 cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
862 @le_plus [@le_times //]
863 [@monotonic_MSC @le_pair @le_pair //
864 |@le_times [//] @monotonic_sU
865 [@le_pair // |// |@monor @Hind //]
871 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
872 ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
873 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
874 cut (max i a ≤ max i b)
876 [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
877 #Hmax @(mono_h_of_aux r Hr Hmono)
878 [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
881 axiom h_of_constr : ∀r:nat →nat.
882 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
883 constructible (h_of r).
885 lemma speed_compl: ∀r:nat →nat.
886 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
887 CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
888 #r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …))
889 [#x cases (surj_pair x) #a * #b #eqx >eqx
890 >sg_def cases (decidable_le b a)
891 [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
892 <plus_n_O <plus_n_O >h_of_def
894 [normalize cases (le_to_or_lt_eq … leba)
895 [#ltba >(lt_to_leb_false … ltba) %
896 |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
897 #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
898 @monotonic_MSC @le_pair @le_pair //
899 |#ltab >h_of_def >h_of_def
901 [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
903 cut (max (S a) b = b)
904 [whd in ⊢ (??%?); >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
907 [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
909 cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
911 [@plus_to_minus >commutative_plus @minus_to_plus
912 [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
915 |#n #a #b #leab #lebn >h_of_def >h_of_def
917 [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
919 [normalize >(le_to_leb_true … lebn) %] #Hmaxb
920 >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
921 |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
922 |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
923 [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]
924 @(h_of_constr r Hr Hmono Hconstr)
928 lemma speed_compl_i: ∀r:nat →nat.
929 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
930 ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
931 #r #Hr #Hmono #Hconstr #i
932 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
933 [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
934 @smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //
937 (**************************** the speedup theorem *****************************)
938 theorem pseudo_speedup:
939 ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
940 ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
941 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
942 #r #Hr #Hmono #Hconstr
943 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
944 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
946 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
947 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
948 (* sg is (λx.h_of r 〈i,x〉) *)
949 %{(λx. h_of r 〈S i,x〉)}
950 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
951 %[%[@condition_1 |@Hg]
952 |cases Hg #H1 * #j * #Hcodej #HCj
953 lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
954 cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
955 @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
956 [@(transitive_le … ltin) @(le_maxl … (le_n …))]
957 cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
958 #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
962 theorem pseudo_speedup':
963 ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
964 ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
965 (* ¬ O (r ∘ sg) sf. *)
966 ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
967 #r #Hr #Hmono #Hconstr
968 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
969 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
971 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
972 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
973 (* sg is (λx.h_of r 〈i,x〉) *)
974 %{(λx. h_of r 〈S i,x〉)}
975 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
976 %[%[@condition_1 |@Hg]
977 |cases Hg #H1 * #j * #Hcodej #HCj
978 lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
979 cases HCi #m * #a #Ha
980 %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2 #Hlesf
981 %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
982 cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
983 #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
984 @Hmono @(mono_h_of2 … Hr Hmono … ltin)