1 include "reverse_complexity/bigops_compl.ma".
3 (********************************* the speedup ********************************)
5 definition min_input ≝ λh,i,x. μ_{y ∈ [S i,x] } (termb i y (h (S i) y)).
7 lemma min_input_def : ∀h,i,x.
8 min_input h i x = min (x -i) (S i) (λy.termb i y (h (S i) y)).
11 lemma min_input_i: ∀h,i,x. x ≤ i → min_input h i x = S i.
12 #h #i #x #lexi >min_input_def
13 cut (x - i = 0) [@sym_eq /2 by eq_minus_O/] #Hcut //
16 lemma min_input_to_terminate: ∀h,i,x.
17 min_input h i x = x → {i ⊙ x} ↓ (h (S i) x).
19 cases (decidable_le (S i) x) #Hix
20 [cases (true_or_false (termb i x (h (S i) x))) #Hcase
21 [@termb_true_to_term //
22 |<Hminx in Hcase; #H lapply (fmin_false (λx.termb i x (h (S i) x)) (x-i) (S i) H)
23 >min_input_def in Hminx; #Hminx >Hminx in ⊢ (%→?);
24 <plus_n_Sm <plus_minus_m_m [2: @lt_to_le //]
27 |@False_ind >min_input_i in Hminx;
28 [#eqix >eqix in Hix; * /2/ | @le_S_S_to_le @not_le_to_lt //]
32 lemma min_input_to_lt: ∀h,i,x.
33 min_input h i x = x → i < x.
34 #h #i #x #Hminx cases (decidable_le (S i) x) //
35 #ltxi @False_ind >min_input_i in Hminx;
36 [#eqix >eqix in ltxi; * /2/ | @le_S_S_to_le @not_le_to_lt //]
39 lemma le_to_min_input: ∀h,i,x,x1. x ≤ x1 →
40 min_input h i x = x → min_input h i x1 = x.
41 #h #i #x #x1 #lex #Hminx @(min_exists … (le_S_S … lex))
42 [@(fmin_true … (sym_eq … Hminx)) //
43 |@(min_input_to_lt … Hminx)
44 |#j #H1 <Hminx @lt_min_to_false //
45 |@plus_minus_m_m @le_S_S @(transitive_le … lex) @lt_to_le
46 @(min_input_to_lt … Hminx)
50 definition g ≝ λh,u,x.
51 S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
53 lemma g_def : ∀h,u,x. g h u x =
54 S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
57 lemma le_u_to_g_1 : ∀h,u,x. x ≤ u → g h u x = 1.
58 #h #u #x #lexu >g_def cut (x-u = 0) [/2 by minus_le_minus_minus_comm/]
59 #eq0 >eq0 normalize // qed.
61 lemma g_lt : ∀h,i,x. min_input h i x = x →
62 out i x (h (S i) x) < g h 0 x.
63 #h #i #x #H @le_S_S @(le_MaxI … i) /2 by min_input_to_lt/
66 lemma max_neq0 : ∀a,b. max a b ≠ 0 → a ≠ 0 ∨ b ≠ 0.
67 #a #b whd in match (max a b); cases (true_or_false (leb a b)) #Hcase >Hcase
71 definition almost_equal ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
72 interpretation "almost equal" 'napart f g = (almost_equal f g).
74 lemma eventually_cancelled: ∀h,u.¬∀nu.∃x. nu < x ∧
75 max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) ≠ 0.
77 [normalize % #H cases (H u) #x * #_ * #H1 @H1 //
78 |#u0 @not_to_not #Hind #nu cases (Hind nu) #x * #ltx
79 cases (true_or_false (eqb (min_input h (u0+O) x) x)) #Hcase
80 [>bigop_Strue [2:@Hcase] #Hmax cases (max_neq0 … Hmax) -Hmax
81 [2: #H %{x} % // <minus_n_O @H]
82 #Hneq0 (* if x is not enough we retry with nu=x *)
83 cases (Hind x) #x1 * #ltx1
85 [#H %{x1} % [@transitive_lt //| <minus_n_O @H]
86 |@not_eq_to_eqb_false >(le_to_min_input … (eqb_true_to_eq … Hcase))
87 [@lt_to_not_eq @ltx1 | @lt_to_le @ltx1]
89 |>bigop_Sfalse [2:@Hcase] #H %{x} % // <minus_n_O @H
94 lemma condition_1: ∀h,u.g h 0 ≈ g h u.
95 #h #u @(not_to_not … (eventually_cancelled h u))
96 #H #nu cases (H (max u nu)) #x * #ltx #Hdiff
97 %{x} % [@(le_to_lt_to_lt … ltx) @(le_maxr … (le_n …))] @(not_to_not … Hdiff)
98 #H @(eq_f ?? S) >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat 0 MaxA)
99 [>H // |@lt_to_le @(le_to_lt_to_lt …ltx) /2 by le_maxr/ |//]
102 (******************************** Condition 2 *********************************)
104 lemma exists_to_exists_min: ∀h,i. (∃x. i < x ∧ {i ⊙ x} ↓ h (S i) x) → ∃y. min_input h i y = y.
105 #h #i * #x * #ltix #Hx %{(min_input h i x)} @min_spec_to_min @found //
106 [@(f_min_true (λy:ℕ.termb i y (h (S i) y))) %{x} % [% // | @term_to_termb_true //]
107 |#y #leiy #lty @(lt_min_to_false ????? lty) //
111 lemma condition_2: ∀h,i. code_for (total (g h 0)) i → ¬∃x. i<x ∧ {i ⊙ x} ↓ h (S i) x.
112 #h #i whd in ⊢(%→?); #H % #H1 cases (exists_to_exists_min … H1) #y #Hminy
113 lapply (g_lt … Hminy)
114 lapply (min_input_to_terminate … Hminy) * #r #termy
115 cases (H y) -H #ny #Hy
116 cut (r = g h 0 y) [@(unique_U … ny … termy) @Hy //] #Hr
117 whd in match (out ???); >termy >Hr
118 #H @(absurd ? H) @le_to_not_lt @le_n
121 (**************************** complexity of g *********************************)
123 definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
125 λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
126 (out i (snd ux) (h (S i) (snd ux))).
128 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
129 #h #s #H1 @(CF_compS ? (auxg h) H1)
133 λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
134 ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
136 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
138 [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
141 lemma compl_g2 : ∀h,s1,s2,s.
143 (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
145 (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
146 O s (λx.MSC x + (snd x - fst x)*Max_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
148 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
149 [#n whd in ⊢ (??%%); @eq_aux]
150 @(CF_max2 … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
151 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
154 lemma compl_g3 : ∀h,s.
155 CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
156 CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
157 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (le_to_O … (MSC_in … H)))
158 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
161 definition min_input_aux ≝ λh,p.
162 μ_{y ∈ [S (fst p),snd (snd p)] }
163 ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
165 lemma min_input_eq : ∀h,p.
167 min_input h (fst p) (snd (snd p)).
168 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
169 whd in ⊢ (??%%); >fst_pair >snd_pair //
172 definition termb_aux ≝ λh.
173 termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
175 lemma compl_g4 : ∀h,s1,s. (∀x. 0 < s1 x) →
177 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
178 (O s (λx.MSC x + ((snd(snd x) - (fst x)))*Max_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
179 CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
180 #h #s1 #s #pos_s1 #Hs1 #HO @(ext_CF (min_input_aux h))
181 [#n whd in ⊢ (??%%); @min_input_eq]
182 @(CF_mu4 … MSC MSC … pos_s1 … Hs1)
184 |@CF_comp_snd @CF_snd
185 |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
190 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
191 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
192 (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
193 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
194 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
197 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
198 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
199 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
200 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
203 lemma coroll3: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
204 O (λx.(snd x - fst x)*s1 〈fst x,x〉)
205 (λx.(snd x - fst x)*Max_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
206 #s1 #Hs1 @le_to_O #i @le_times // @Max_le #a #lta #_ @Hs1 //
207 @lt_minus_to_plus_r //
210 (**************************** end of technical lemmas *************************)
212 lemma compl_g5 : ∀h,s1.
214 (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
216 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
217 CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
218 (λp:ℕ.min_input h (fst p) (snd (snd p))).
219 #h #s1 #Hpos #Hmono #Hs1 @(compl_g4 … Hpos Hs1) @O_plus
220 [@O_plus_l // |@O_plus_r @le_to_O #n @le_times //
221 @Max_le #i #lti #_ @Hmono @le_S_S_to_le @lt_minus_to_plus_r @lti
225 constructible (λx. h (fst x) (snd x)) →
226 (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
227 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
228 #h #hconstr @(ext_CF (termb_aux h))
229 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
230 @(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
232 [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
234 [@(monotonic_CF … CF_fst) #x //
235 |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
236 [#n normalize >fst_pair >snd_pair %]
237 @(CF_comp … MSC …hconstr)
238 [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
239 |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
245 [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
246 [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
247 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
248 >distributive_times_plus @le_plus [//]
249 cases (surj_pair b) #c * #d #eqb >eqb
250 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
251 whd in ⊢ (??%); @le_plus
252 [@monotonic_MSC @(le_maxl … (le_n …))
253 |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
255 |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
259 |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
263 definition big : nat →nat ≝ λx.
264 let m ≝ max (fst x) (snd x) in 〈m,m〉.
266 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
267 #a #b normalize >fst_pair >snd_pair // qed.
269 lemma le_big : ∀x. x ≤ big x.
270 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
271 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
274 definition faux2 ≝ λh.
275 (λx.MSC x + (snd (snd x)-fst x)*
276 (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
279 constructible (λx. h (fst x) (snd x)) →
280 (∀n. monotonic ? le (h n)) →
281 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))〉〉)
282 (λp:ℕ.min_input h (fst p) (snd (snd p))).
283 #h #hcostr #hmono @(monotonic_CF … (faux2 h))
284 [#n normalize >fst_pair >snd_pair //]
285 @compl_g5 [#n @sU_pos | 3:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
286 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
290 constructible (λx. h (fst x) (snd x)) →
291 (∀n. monotonic ? le (h n)) →
292 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))〉〉)
293 (λp:ℕ.min_input h (fst p) (snd (snd p))).
294 #h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x
295 @le_plus [@monotonic_MSC //]
296 cases (decidable_le (fst x) (snd(snd x)))
297 [#Hle @le_times // @monotonic_sU
298 |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
302 definition out_aux ≝ λh.
303 out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
306 constructible (λx. h (fst x) (snd x)) →
307 (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
308 (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
309 #h #hconstr @(ext_CF (out_aux h))
310 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
311 @(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
313 [@(monotonic_CF … CF_fst) #x //
315 [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
316 |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
317 [#n normalize >fst_pair >snd_pair %]
318 @(CF_comp … MSC …hconstr)
319 [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
320 |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
327 |@(O_trans … (λx.MSC (max (fst x) (snd x))))
328 [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
329 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
330 whd in ⊢ (??%); @le_plus
331 [@monotonic_MSC @(le_maxl … (le_n …))
332 |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
334 |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
337 |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
342 constructible (λx. h (fst x) (snd x)) →
343 (∀n. monotonic ? le (h n)) →
344 (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
345 CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
346 (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
348 #h #hconstr #hmono #hantimono
349 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
351 [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
352 [// | @monotonic_MSC // ]]
353 @(O_trans … (coroll3 ??))
354 [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
355 cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
357 [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
358 cut (max b n = n) [normalize >le_to_leb_true //] #maxb
360 [@le_plus [>big_def >big_def >maxa >maxb //]
362 [/2 by monotonic_le_minus_r/
363 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
365 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
367 |@le_to_O #n >fst_pair >snd_pair
368 cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
369 >associative_plus >distributive_times_plus
370 @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
374 definition c ≝ λx.(S (snd x-fst x))*MSC 〈x,x〉.
376 definition sg ≝ λh,x.
379 c x + (b-a)*(S(b-a))*sU 〈x,〈snd x,h (S a) b〉〉.
381 lemma sg_def1 : ∀h,a,b.
382 sg h 〈a,b〉 = c 〈a,b〉 +
383 (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
384 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
387 lemma sg_def : ∀h,a,b.
389 S (b-a)*MSC 〈〈a,b〉,〈a,b〉〉 + (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
390 #h #a #b normalize >fst_pair >snd_pair //
393 lemma compl_g11 : ∀h.
394 constructible (λx. h (fst x) (snd x)) →
395 (∀n. monotonic ? le (h n)) →
396 (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
397 CF (sg h) (unary_g h).
398 #h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)
401 (**************************** closing the argument ****************************)
403 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
406 | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
407 d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
409 lemma h_of_aux_O: ∀r,c,b.
410 h_of_aux r c O b = c.
413 lemma h_of_aux_S : ∀r,c,d,b.
414 h_of_aux r c (S d) b =
415 (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
416 (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
419 definition h_of ≝ λr,p.
420 let m ≝ max (fst p) (snd p) in
421 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
423 lemma h_of_O: ∀r,a,b. b ≤ a →
424 h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
425 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
428 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
430 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
431 #r #a #b normalize >fst_pair >snd_pair //
434 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
435 ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
436 h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
437 #r #Hr #monor #d #d1 lapply d -d elim d1
438 [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
439 >h_of_aux_O >h_of_aux_O //
440 |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
441 [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
442 >h_of_aux_S @(transitive_le ???? (le_plus_n …))
443 >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
444 >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
445 |#Hd >Hd >h_of_aux_S >h_of_aux_S
446 cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
447 @le_plus [@le_times //]
448 [@monotonic_MSC @le_pair @le_pair //
449 |@le_times [//] @monotonic_sU
450 [@le_pair // |// |@monor @Hind //]
456 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
457 ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
458 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
459 cut (max i a ≤ max i b)
461 [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
462 #Hmax @(mono_h_of_aux r Hr Hmono)
463 [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
466 axiom h_of_constr : ∀r:nat →nat.
467 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
468 constructible (h_of r).
470 lemma speed_compl: ∀r:nat →nat.
471 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
472 CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
473 #r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …))
474 [#x cases (surj_pair x) #a * #b #eqx >eqx
475 >sg_def cases (decidable_le b a)
476 [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
477 <plus_n_O <plus_n_O >h_of_def
479 [normalize cases (le_to_or_lt_eq … leba)
480 [#ltba >(lt_to_leb_false … ltba) %
481 |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
482 #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
483 @monotonic_MSC @le_pair @le_pair //
484 |#ltab >h_of_def >h_of_def
486 [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
488 cut (max (S a) b = b)
489 [whd in ⊢ (??%?); >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
492 [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
494 cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
496 [@plus_to_minus >commutative_plus @minus_to_plus
497 [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
500 |#n #a #b #leab #lebn >h_of_def >h_of_def
502 [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
504 [normalize >(le_to_leb_true … lebn) %] #Hmaxb
505 >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
506 |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
507 |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
508 [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]
509 @(h_of_constr r Hr Hmono Hconstr)
513 lemma speed_compl_i: ∀r:nat →nat.
514 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
515 ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
516 #r #Hr #Hmono #Hconstr #i
517 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
518 [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
519 @smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //
522 (**************************** the speedup theorem *****************************)
523 theorem pseudo_speedup:
524 ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
525 ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
526 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
527 #r #Hr #Hmono #Hconstr
528 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
529 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #i *
531 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
532 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
533 (* sg is (λx.h_of r 〈i,x〉) *)
534 %{(λx. h_of r 〈S i,x〉)}
535 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
536 %[%[@condition_1 |@Hg]
537 |cases Hg #H1 * #j * #Hcodej #HCj
538 lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
539 cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
540 @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
541 [@(transitive_le … ltin) @(le_maxl … (le_n …))]
542 cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
543 #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
547 theorem pseudo_speedup':
548 ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
549 ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
550 (* ¬ O (r ∘ sg) sf. *)
551 ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
552 #r #Hr #Hmono #Hconstr
553 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
554 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #i *
556 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
557 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
558 (* sg is (λx.h_of r 〈S i,x〉) *)
559 %{(λx. h_of r 〈S i,x〉)}
560 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
561 %[%[@condition_1 |@Hg]
562 |cases Hg #H1 * #j * #Hcodej #HCj
563 lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
564 cases HCi #m * #a #Ha
565 %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2
566 #Hlesf %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
567 cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
568 #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
569 @Hmono @(mono_h_of2 … Hr Hmono … ltin)