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/
250 (∃y.i < y ∧ (termb i y (h (S i) y)=true)) ∨
251 ∀y. i < y → (termb i y (h (S i) y)=false).
253 lemma eventually_0: ∀h,u.∃nu.∀x. nu < x →
254 max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) = 0.
257 |#u0 * #nu0 #Hind cases (ax1 h u0)
258 [* #x0 * #leu0x0 #Hx0 %{(max nu0 x0)}
260 [>(minus_n_O u0) @Hind @(le_to_lt_to_lt … Hx) /2 by le_maxl/
261 |@not_eq_to_eqb_false % #Hf @(absurd (x ≤ x0))
262 [<Hf @true_to_le_min //
263 |@lt_to_not_le @(le_to_lt_to_lt … Hx) /2 by le_maxl/
266 |#H %{(max u0 nu0)} #x #Hx >bigop_Sfalse
267 [>(minus_n_O u0) @Hind @(le_to_lt_to_lt … Hx) @le_maxr //
268 |@not_eq_to_eqb_false >min_input_def
269 >(min_not_exists (λy.(termb (u0+0) y (h (S (u0+0)) y))))
270 [<plus_n_O <plus_n_Sm <plus_minus_m_m
272 |@lt_to_le @(le_to_lt_to_lt … Hx) @le_maxl //
281 definition almost_equal ≝ λf,g:nat → nat. ∃nu.∀x. nu < x → f x = g x.
283 definition almost_equal1 ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
285 interpretation "almost equal" 'napart f g = (almost_equal f g).
287 lemma condition_1: ∀h,u.g h 0 ≈ g h u.
288 #h #u cases (eventually_0 h u) #nu #H %{(max u nu)} #x #Hx @(eq_f ?? S)
289 >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat 0 MaxA)
290 [>H // @(le_to_lt_to_lt …Hx) /2 by le_maxl/
291 |@lt_to_le @(le_to_lt_to_lt …Hx) /2 by le_maxr/
296 lemma max_neq0 : ∀a,b. max a b ≠ 0 → a ≠ 0 ∨ b ≠ 0.
297 #a #b whd in match (max a b); cases (true_or_false (leb a b)) #Hcase >Hcase
298 [#H %2 @H | #H %1 @H]
301 definition almost_equal ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
302 interpretation "almost equal" 'napart f g = (almost_equal f g).
304 lemma eventually_cancelled: ∀h,u.¬∀nu.∃x. nu < x ∧
305 max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) ≠ 0.
307 [normalize % #H cases (H u) #x * #_ * #H1 @H1 //
308 |#u0 @not_to_not #Hind #nu cases (Hind nu) #x * #ltx
309 cases (true_or_false (eqb (min_input h (u0+O) x) x)) #Hcase
310 [>bigop_Strue [2:@Hcase] #Hmax cases (max_neq0 … Hmax) -Hmax
311 [2: #H %{x} % // <minus_n_O @H]
312 #Hneq0 (* if x is not enough we retry with nu=x *)
313 cases (Hind x) #x1 * #ltx1
315 [#H %{x1} % [@transitive_lt //| <minus_n_O @H]
316 |@not_eq_to_eqb_false >(le_to_min_input … (eqb_true_to_eq … Hcase))
317 [@lt_to_not_eq @ltx1 | @lt_to_le @ltx1]
319 |>bigop_Sfalse [2:@Hcase] #H %{x} % // <minus_n_O @H
324 lemma condition_1: ∀h,u.g h 0 ≈ g h u.
325 #h #u @(not_to_not … (eventually_cancelled h u))
326 #H #nu cases (H (max u nu)) #x * #ltx #Hdiff
327 %{x} % [@(le_to_lt_to_lt … ltx) @(le_maxr … (le_n …))] @(not_to_not … Hdiff)
328 #H @(eq_f ?? S) >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat 0 MaxA)
329 [>H // |@lt_to_le @(le_to_lt_to_lt …ltx) /2 by le_maxr/ |//]
332 (******************************** Condition 2 *********************************)
333 definition total ≝ λf.λx:nat. Some nat (f x).
335 lemma exists_to_exists_min: ∀h,i. (∃x. i < x ∧ {i ⊙ x} ↓ h (S i) x) → ∃y. min_input h i y = y.
336 #h #i * #x * #ltix #Hx %{(min_input h i x)} @min_spec_to_min @found //
337 [@(f_min_true (λy:ℕ.termb i y (h (S i) y))) %{x} % [% // | @term_to_termb_true //]
338 |#y #leiy #lty @(lt_min_to_false ????? lty) //
342 lemma condition_2: ∀h,i. code_for (total (g h 0)) i → ¬∃x. i<x ∧ {i ⊙ x} ↓ h (S i) x.
343 #h #i whd in ⊢(%→?); #H % #H1 cases (exists_to_exists_min … H1) #y #Hminy
344 lapply (g_lt … Hminy)
345 lapply (min_input_to_terminate … Hminy) * #r #termy
346 cases (H y) -H #ny #Hy
347 cut (r = g h 0 y) [@(unique_U … ny … termy) @Hy //] #Hr
348 whd in match (out ???); >termy >Hr
349 #H @(absurd ? H) @le_to_not_lt @le_n
353 (********************** complexity ***********************)
355 (* We assume operations have a minimal structural complexity MSC.
356 For instance, for time complexity, MSC is equal to the size of input.
357 For space complexity, MSC is typically 0, since we only measure the
358 space required in addition to dimension of the input. *)
360 axiom MSC : nat → nat.
361 axiom MSC_le: ∀n. MSC n ≤ n.
362 axiom monotonic_MSC: monotonic ? le MSC.
363 axiom MSC_pair: ∀a,b. MSC 〈a,b〉 ≤ MSC a + MSC b.
365 (* C s i means i is running in O(s) *)
367 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ x → ∃y.
368 U i x (c*(s x)) = Some ? y.
370 (* C f s means f ∈ O(s) where MSC ∈O(s) *)
371 definition CF ≝ λs,f.O s MSC ∧ ∃i.code_for (total f) i ∧ C s i.
373 lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
374 #f #g #s #Hext * #HO * #i * #Hcode #HC % // %{i} %
375 [#x cases (Hcode x) #a #H %{a} whd in match (total ??); <Hext @H | //]
378 (* lemma ext_CF_total : ∀f,g,s. (∀n. f n = g n) → CF s (total f) → CF s (total g).
379 #f #g #s #Hext * #HO * #i * #Hcode #HC % // %{i} % [2:@HC]
380 #x cases (Hcode x) #a #H %{a} #m #leam >(H m leam) normalize @eq_f @Hext
383 lemma monotonic_CF: ∀s1,s2,f.(∀x. s1 x ≤ s2 x) → CF s1 f → CF s2 f.
384 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
385 [cases HO #c * #a -HO #HO %{c} %{a} #n #lean @(transitive_le … (HO n lean))
387 |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1 %{c} %{a} #n #lean
388 cases(Hs1 n lean) #y #Hy %{y} @(monotonic_U …Hy) @le_times //
392 lemma O_to_CF: ∀s1,s2,f.O s2 s1 → CF s1 f → CF s2 f.
393 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
395 |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1
396 cases H #c1 * #a1 #Ha1 %{(c*c1)} %{(a+a1)} #n #lean
397 cases(Hs1 n ?) [2:@(transitive_le … lean) //] #y #Hy %{y} @(monotonic_U …Hy)
398 >associative_times @le_times // @Ha1 @(transitive_le … lean) //
402 lemma timesc_CF: ∀s,f,c.CF (λx.c*s x) f → CF s f.
403 #s #f #c @O_to_CF @O_times_c
406 (********************************* composition ********************************)
407 axiom CF_comp: ∀f,g,sf,sg,sh. CF sg g → CF sf f →
408 O sh (λx. sg x + sf (g x)) → CF sh (f ∘ g).
410 lemma CF_comp_ext: ∀f,g,h,sh,sf,sg. CF sg g → CF sf f →
411 (∀x.f(g x) = h x) → O sh (λx. sg x + sf (g x)) → CF sh h.
412 #f #g #h #sh #sf #sg #Hg #Hf #Heq #H @(ext_CF (f ∘ g))
413 [#n normalize @Heq | @(CF_comp … H) //]
417 lemma CF_comp1: ∀f,g,s. CF s (total g) → CF s (total f) →
418 CF s (total (f ∘ g)).
419 #f #g #s #Hg #Hf @(timesc_CF … 2) @(monotonic_CF … (CF_comp … Hg Hf))
423 axiom CF_comp_ext2: ∀f,g,h,sf,sh. CF sh (total g) → CF sf (total f) →
425 (∀x. sf (g x) ≤ sh x) → CF sh (total h).
427 lemma main_MSC: ∀h,f. CF h f → O h (λx.MSC (f x)).
429 axiom CF_S: CF MSC S.
430 axiom CF_fst: CF MSC fst.
431 axiom CF_snd: CF MSC snd.
433 lemma CF_compS: ∀h,f. CF h f → CF h (S ∘ f).
434 #h #f #Hf @(CF_comp … Hf CF_S) @O_plus // @main_MSC //
437 lemma CF_comp_fst: ∀h,f. CF h (total f) → CF h (total (fst ∘ f)).
438 #h #f #Hf @(CF_comp … Hf CF_fst) @O_plus // @main_MSC //
441 lemma CF_comp_snd: ∀h,f. CF h (total f) → CF h (total (snd ∘ f)).
442 #h #f #Hf @(CF_comp … Hf CF_snd) @O_plus // @main_MSC //
445 definition id ≝ λx:nat.x.
447 axiom CF_id: CF MSC id.
448 axiom CF_compS: ∀h,f. CF h f → CF h (S ∘ f).
449 axiom CF_comp_fst: ∀h,f. CF h f → CF h (fst ∘ f).
450 axiom CF_comp_snd: ∀h,f. CF h f → CF h (snd ∘ f).
451 axiom CF_comp_pair: ∀h,f,g. CF h f → CF h g → CF h (λx. 〈f x,g x〉).
453 lemma CF_fst: CF MSC fst.
454 @(ext_CF (fst ∘ id)) [#n //] @(CF_comp_fst … CF_id)
457 lemma CF_snd: CF MSC snd.
458 @(ext_CF (snd ∘ id)) [#n //] @(CF_comp_snd … CF_id)
461 (************************************** eqb ***********************************)
462 (* definition btotal ≝
463 λf.λx:nat. match f x with [true ⇒ Some ? 0 |false ⇒ Some ? 1]. *)
465 axiom CF_eqb: ∀h,f,g.
466 CF h f → CF h g → CF h (λx.eqb (f x) (g x)).
469 axiom eqb_compl2: ∀h,f,g.
470 CF2 h (total2 f) → CF2 h (total2 g) →
471 CF2 h (btotal2 (λx1,x2.eqb (f x1 x2) (g x1 x2))).
473 axiom eqb_min_input_compl:∀h,x.
474 CF (λi.∑_{y ∈ [S i,S x[ }(h i y))
475 (btotal (λi.eqb (min_input h i x) x)). *)
476 (*********************************** maximum **********************************)
478 axiom CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
479 CF ha a → CF hb b → CF hp p → CF hf f →
480 O s (λx.ha x + hb x + ∑_{i ∈[a x ,b x[ }(hp 〈i,x〉 + hf 〈i,x〉)) →
481 CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
483 (******************************** minimization ********************************)
485 axiom CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
486 CF sa a → CF sb b → CF sf f →
487 O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
488 CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
490 (****************************** constructibility ******************************)
492 definition constructible ≝ λs. CF s s.
494 lemma constr_comp : ∀s1,s2. constructible s1 → constructible s2 →
495 (∀x. x ≤ s2 x) → constructible (s2 ∘ s1).
496 #s1 #s2 #Hs1 #Hs2 #Hle @(CF_comp … Hs1 Hs2) @O_plus @le_to_O #x [@Hle | //]
499 lemma ext_constr: ∀s1,s2. (∀x.s1 x = s2 x) →
500 constructible s1 → constructible s2.
501 #s1 #s2 #Hext #Hs1 @(ext_CF … Hext) @(monotonic_CF … Hs1) #x >Hext //
504 (********************************* simulation *********************************)
506 axiom sU : nat → nat.
508 axiom monotonic_sU: ∀i1,i2,x1,x2,s1,s2. i1 ≤ i2 → x1 ≤ x2 → s1 ≤ s2 →
509 sU 〈i1,〈x1,s1〉〉 ≤ sU 〈i2,〈x2,s2〉〉.
511 lemma monotonic_sU_aux : ∀x1,x2. fst x1 ≤ fst x2 → fst (snd x1) ≤ fst (snd x2) →
512 snd (snd x1) ≤ snd (snd x2) → sU x1 ≤ sU x2.
513 #x1 #x2 cases (surj_pair x1) #a1 * #y #eqx1 >eqx1 -eqx1 cases (surj_pair y)
514 #b1 * #c1 #eqy >eqy -eqy
515 cases (surj_pair x2) #a2 * #y2 #eqx2 >eqx2 -eqx2 cases (surj_pair y2)
516 #b2 * #c2 #eqy2 >eqy2 -eqy2 >fst_pair >snd_pair >fst_pair >snd_pair
517 >fst_pair >snd_pair >fst_pair >snd_pair @monotonic_sU
520 axiom sU_le: ∀i,x,s. s ≤ sU 〈i,〈x,s〉〉.
521 axiom sU_le_i: ∀i,x,s. MSC i ≤ sU 〈i,〈x,s〉〉.
522 axiom sU_le_x: ∀i,x,s. MSC x ≤ sU 〈i,〈x,s〉〉.
524 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
526 axiom CF_U : CF sU pU_unary.
528 definition termb_unary ≝ λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)).
529 definition out_unary ≝ λx:ℕ.out (fst x) (fst (snd x)) (snd (snd x)).
531 lemma CF_termb: CF sU termb_unary.
532 @(ext_CF (fst ∘ pU_unary)) [2: @CF_comp_fst @CF_U]
533 #n whd in ⊢ (??%?); whd in ⊢ (??(?%)?); >fst_pair %
536 lemma CF_out: CF sU out_unary.
537 @(ext_CF (snd ∘ pU_unary)) [2: @CF_comp_snd @CF_U]
538 #n whd in ⊢ (??%?); whd in ⊢ (??(?%)?); >snd_pair %
542 lemma CF_termb_comp: ∀f.CF (sU ∘ f) (termb_unary ∘ f).
543 #f @(CF_comp … CF_termb) *)
545 (******************** complexity of g ********************)
547 definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
549 λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
550 (out i (snd ux) (h (S i) (snd ux))).
552 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
553 #h #s #H1 @(CF_compS ? (auxg h) H1)
557 λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
558 ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
560 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
562 [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
565 lemma compl_g2 : ∀h,s1,s2,s.
567 (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
569 (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
570 O s (λx.MSC x + ∑_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
572 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
573 [#n whd in ⊢ (??%%); @eq_aux]
574 @(CF_max … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
575 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
578 lemma compl_g3 : ∀h,s.
579 CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
580 CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
581 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (proj1 … H))
582 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
585 definition min_input_aux ≝ λh,p.
586 μ_{y ∈ [S (fst p),snd (snd p)] }
587 ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
589 lemma min_input_eq : ∀h,p.
591 min_input h (fst p) (snd (snd p)).
592 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
593 whd in ⊢ (??%%); >fst_pair >snd_pair //
596 definition termb_aux ≝ λh.
597 termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
600 lemma termb_aux : ∀h,p.
601 (λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)))
602 〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉 =
603 termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)) .
604 #h #p normalize >fst_pair >snd_pair >fst_pair >snd_pair //
607 lemma compl_g4 : ∀h,s1,s.
609 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
610 (O s (λx.MSC x + ∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
611 CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
612 #h #s1 #s #Hs1 #HO @(ext_CF (min_input_aux h))
613 [#n whd in ⊢ (??%%); @min_input_eq]
614 @(CF_mu … MSC MSC … Hs1)
616 |@CF_comp_snd @CF_snd
617 |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
618 (* @(ext_CF (btotal (termb_aux h)))
619 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
620 @(CF_compb … CF_termb) *)
623 (************************* a couple of technical lemmas ***********************)
624 lemma minus_to_0: ∀a,b. a ≤ b → minus a b = 0.
625 #a elim a // #n #Hind *
626 [#H @False_ind /2 by absurd/ | #b normalize #H @Hind @le_S_S_to_le /2/]
629 lemma sigma_bound: ∀h,a,b. monotonic nat le h →
630 ∑_{i ∈ [a,S b[ }(h i) ≤ (S b-a)*h b.
631 #h #a #b #H cases (decidable_le a b)
632 [#leab cut (b = pred (S b - a + a))
633 [<plus_minus_m_m // @le_S //] #Hb >Hb in match (h b);
634 generalize in match (S b -a);
637 |#m #Hind >bigop_Strue [2://] @le_plus
638 [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
640 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
641 cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
645 lemma sigma_bound_decr: ∀h,a,b. (∀a1,a2. a1 ≤ a2 → a2 < b → h a2 ≤ h a1) →
646 ∑_{i ∈ [a,b[ }(h i) ≤ (b-a)*h a.
647 #h #a #b #H cases (decidable_le a b)
648 [#leab cut ((b -a) +a ≤ b) [/2 by le_minus_to_plus_r/] generalize in match (b -a);
651 |#m #Hind >bigop_Strue [2://] #Hm
652 cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
653 @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
655 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
656 cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
660 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
661 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
662 (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
663 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
664 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
667 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
668 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
669 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
670 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
673 lemma compl_g5 : ∀h,s1.(∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
675 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
676 CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
677 (λp:ℕ.min_input h (fst p) (snd (snd p))).
678 #h #s1 #Hmono #Hs1 @(compl_g4 … Hs1) @O_plus
679 [@O_plus_l // |@O_plus_r @coroll @Hmono]
684 (* constructible (λx. h (fst x) (snd x)) → *)
685 (CF (λx. max (MSC x) (sU 〈fst (snd x),〈fst x,h (S (fst (snd x))) (fst x)〉〉))
686 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
690 constructible (λx. h (fst x) (snd x)) →
691 (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
692 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
693 #h #hconstr @(ext_CF (termb_aux h))
694 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
695 @(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
697 [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
699 [@(monotonic_CF … CF_fst) #x //
700 |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
701 [#n normalize >fst_pair >snd_pair %]
702 @(CF_comp … MSC …hconstr)
703 [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
704 |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
710 [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
711 [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
712 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
713 >distributive_times_plus @le_plus [//]
714 cases (surj_pair b) #c * #d #eqb >eqb
715 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
716 whd in ⊢ (??%); @le_plus
717 [@monotonic_MSC @(le_maxl … (le_n …))
718 |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
720 |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
724 |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
728 (* definition faux1 ≝ λh.
729 (λx.MSC x + (snd (snd x)-fst x)*(λx.sU 〈fst (snd x),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
731 (* complexity of min_input *)
733 (∀x.MSC x≤h (S (fst (snd x))) (fst x)) →
734 constructible (λx. h (fst x) (snd x)) →
735 (∀n. monotonic ? le (h n)) →
736 CF (λx.MSC x + (snd (snd x)-fst x)*sU 〈fst x,〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
737 (λp:ℕ.min_input h (fst p) (snd (snd p))).
738 #h #hle #hcostr #hmono @(monotonic_CF … (faux1 h))
739 [#n normalize >fst_pair >snd_pair //]
740 @compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
741 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
744 definition big : nat →nat ≝ λx.
745 let m ≝ max (fst x) (snd x) in 〈m,m〉.
747 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
748 #a #b normalize >fst_pair >snd_pair // qed.
750 lemma le_big : ∀x. x ≤ big x.
751 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
752 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
755 definition faux2 ≝ λh.
756 (λx.MSC x + (snd (snd x)-fst x)*
757 (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
761 constructible (λx. h (fst x) (snd x)) →
762 (∀n. monotonic ? le (h n)) →
763 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))〉〉)
764 (λp:ℕ.min_input h (fst p) (snd (snd p))).
765 #h #hcostr #hmono @(monotonic_CF … (faux2 h))
766 [#n normalize >fst_pair >snd_pair //]
767 @compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
768 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
773 constructible (λx. h (fst x) (snd x)) →
774 (∀n. monotonic ? le (h n)) →
775 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))〉〉)
776 (λp:ℕ.min_input h (fst p) (snd (snd p))).
777 #h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x
778 @le_plus [@monotonic_MSC //]
779 cases (decidable_le (fst x) (snd(snd x)))
780 [#Hle @le_times // @monotonic_sU
781 |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
787 CF (λx. sU 〈fst x,〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
788 (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))). *)
790 definition out_aux ≝ λh.
791 out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
794 constructible (λx. h (fst x) (snd x)) →
795 (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
796 (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
797 #h #hconstr @(ext_CF (out_aux h))
798 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
799 @(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
801 [@(monotonic_CF … CF_fst) #x //
803 [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
804 |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
805 [#n normalize >fst_pair >snd_pair %]
806 @(CF_comp … MSC …hconstr)
807 [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
808 |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
815 |@(O_trans … (λx.MSC (max (fst x) (snd x))))
816 [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
817 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
818 whd in ⊢ (??%); @le_plus
819 [@monotonic_MSC @(le_maxl … (le_n …))
820 |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
822 |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
825 |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
831 (∀x.MSC x≤h (S (fst x)) (snd(snd x))) →
832 constructible (λx. h (fst x) (snd x)) →
833 CF (λx. sU 〈max (fst x) (snd x),〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
834 (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))).
835 #h #hle #hconstr @(monotonic_CF ???? (compl_g8 h hle hconstr)) #x @monotonic_sU // @(le_maxl … (le_n … ))
838 (* axiom daemon : False. *)
841 constructible (λx. h (fst x) (snd x)) →
842 (∀n. monotonic ? le (h n)) →
843 (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
844 CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
845 (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
847 #h #hconstr #hmono #hantimono
848 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
850 [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
851 [// | @monotonic_MSC // ]]
852 @(O_trans … (coroll2 ??))
853 [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
854 cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
856 [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
857 cut (max b n = n) [normalize >le_to_leb_true //] #maxb
859 [@le_plus [>big_def >big_def >maxa >maxb //]
861 [/2 by monotonic_le_minus_r/
862 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
864 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
866 |@le_to_O #n >fst_pair >snd_pair
867 cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
868 >associative_plus >distributive_times_plus
869 @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
873 definition sg ≝ λh,x.
874 (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)〉〉.
876 lemma sg_def : ∀h,a,b.
877 sg h 〈a,b〉 = (S (b-a))*MSC 〈〈a,b〉,〈a,b〉〉 +
878 (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
879 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
882 lemma compl_g11 : ∀h.
883 constructible (λx. h (fst x) (snd x)) →
884 (∀n. monotonic ? le (h n)) →
885 (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
886 CF (sg h) (unary_g h).
887 #h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)
890 (**************************** closing the argument ****************************)
892 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
894 [ O ⇒ c (* MSC 〈〈b,b〉,〈b,b〉〉 *)
895 | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
896 d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
898 lemma h_of_aux_O: ∀r,c,b.
899 h_of_aux r c O b = c.
902 lemma h_of_aux_S : ∀r,c,d,b.
903 h_of_aux r c (S d) b =
904 (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
905 (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
908 definition h_of ≝ λr,p.
909 let m ≝ max (fst p) (snd p) in
910 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
912 lemma h_of_O: ∀r,a,b. b ≤ a →
913 h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
914 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
917 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
919 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
920 #r #a #b normalize >fst_pair >snd_pair //
923 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
924 ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
925 h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
926 #r #Hr #monor #d #d1 lapply d -d elim d1
927 [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
928 >h_of_aux_O >h_of_aux_O //
929 |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
930 [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
931 >h_of_aux_S @(transitive_le ???? (le_plus_n …))
932 >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
933 >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
934 |#Hd >Hd >h_of_aux_S >h_of_aux_S
935 cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
936 @le_plus [@le_times //]
937 [@monotonic_MSC @le_pair @le_pair //
938 |@le_times [//] @monotonic_sU
939 [@le_pair // |// |@monor @Hind //]
945 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
946 ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
947 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
948 cut (max i a ≤ max i b)
950 [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
951 #Hmax @(mono_h_of_aux r Hr Hmono)
952 [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
955 axiom h_of_constr : ∀r:nat →nat.
956 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
957 constructible (h_of r).
959 lemma speed_compl: ∀r:nat →nat.
960 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
961 CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
962 #r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …))
963 [#x cases (surj_pair x) #a * #b #eqx >eqx
964 >sg_def cases (decidable_le b a)
965 [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
966 <plus_n_O <plus_n_O >h_of_def
968 [normalize cases (le_to_or_lt_eq … leba)
969 [#ltba >(lt_to_leb_false … ltba) %
970 |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
971 #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
972 @monotonic_MSC @le_pair @le_pair //
973 |#ltab >h_of_def >h_of_def
975 [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
977 cut (max (S a) b = b)
978 [whd in ⊢ (??%?); >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
981 [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
983 cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
985 [@plus_to_minus >commutative_plus @minus_to_plus
986 [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
989 |#n #a #b #leab #lebn >h_of_def >h_of_def
991 [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
993 [normalize >(le_to_leb_true … lebn) %] #Hmaxb
994 >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
995 |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
996 |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
997 [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]
998 @(h_of_constr r Hr Hmono Hconstr)
1003 lemma unary_g_def : ∀h,i,x. g h i x = unary_g h 〈i,x〉.
1004 #h #i #x whd in ⊢ (???%); >fst_pair >snd_pair %
1008 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
1010 lemma speed_compl_i: ∀r:nat →nat.
1011 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1012 ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
1013 #r #Hr #Hmono #Hconstr #i
1014 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
1015 [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
1016 @smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //
1019 theorem pseudo_speedup:
1020 ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1021 ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
1022 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
1023 #r #Hr #Hmono #Hconstr
1024 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
1025 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
1027 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
1028 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
1029 (* sg is (λx.h_of r 〈i,x〉) *)
1030 %{(λx. h_of r 〈S i,x〉)}
1031 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
1032 %[%[@condition_1 |@Hg]
1033 |cases Hg #H1 * #j * #Hcodej #HCj
1034 lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
1035 cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
1036 @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
1037 [@(transitive_le … ltin) @(le_maxl … (le_n …))]
1038 cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
1039 #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
1043 theorem pseudo_speedup':
1044 ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1045 ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
1046 (* ¬ O (r ∘ sg) sf. *)
1047 ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
1048 #r #Hr #Hmono #Hconstr
1049 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
1050 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
1052 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
1053 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
1054 (* sg is (λx.h_of r 〈i,x〉) *)
1055 %{(λx. h_of r 〈S i,x〉)}
1056 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
1057 %[%[@condition_1 |@Hg]
1058 |cases Hg #H1 * #j * #Hcodej #HCj
1059 lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
1060 cases HCi #m * #a #Ha
1061 %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2 #Hlesf
1062 %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
1063 cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
1064 #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
1065 @Hmono @(mono_h_of2 … Hr Hmono … ltin)