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/
249 (∃y.i < y ∧ (termb i y (h (S i) y)=true)) ∨
250 ∀y. i < y → (termb i y (h (S i) y)=false).
252 lemma eventually_0: ∀h,u.∃nu.∀x. nu < x →
253 max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) = 0.
256 |#u0 * #nu0 #Hind cases (ax1 h u0)
257 [* #x0 * #leu0x0 #Hx0 %{(max nu0 x0)}
259 [>(minus_n_O u0) @Hind @(le_to_lt_to_lt … Hx) /2 by le_maxl/
260 |@not_eq_to_eqb_false % #Hf @(absurd (x ≤ x0))
261 [<Hf @true_to_le_min //
262 |@lt_to_not_le @(le_to_lt_to_lt … Hx) /2 by le_maxl/
265 |#H %{(max u0 nu0)} #x #Hx >bigop_Sfalse
266 [>(minus_n_O u0) @Hind @(le_to_lt_to_lt … Hx) @le_maxr //
267 |@not_eq_to_eqb_false >min_input_def
268 >(min_not_exists (λy.(termb (u0+0) y (h (S (u0+0)) y))))
269 [<plus_n_O <plus_n_Sm <plus_minus_m_m
271 |@lt_to_le @(le_to_lt_to_lt … Hx) @le_maxl //
280 definition almost_equal ≝ λf,g:nat → nat. ∃nu.∀x. nu < x → f x = g x.
282 definition almost_equal1 ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
284 interpretation "almost equal" 'napart f g = (almost_equal f g).
286 lemma condition_1: ∀h,u.g h 0 ≈ g h u.
287 #h #u cases (eventually_0 h u) #nu #H %{(max u nu)} #x #Hx @(eq_f ?? S)
288 >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat 0 MaxA)
289 [>H // @(le_to_lt_to_lt …Hx) /2 by le_maxl/
290 |@lt_to_le @(le_to_lt_to_lt …Hx) /2 by le_maxr/
295 lemma max_neq0 : ∀a,b. max a b ≠ 0 → a ≠ 0 ∨ b ≠ 0.
296 #a #b whd in match (max a b); cases (true_or_false (leb a b)) #Hcase >Hcase
297 [#H %2 @H | #H %1 @H]
300 definition almost_equal ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
301 interpretation "almost equal" 'napart f g = (almost_equal f g).
303 lemma eventually_cancelled: ∀h,u.¬∀nu.∃x. nu < x ∧
304 max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) ≠ 0.
306 [normalize % #H cases (H u) #x * #_ * #H1 @H1 //
307 |#u0 @not_to_not #Hind #nu cases (Hind nu) #x * #ltx
308 cases (true_or_false (eqb (min_input h (u0+O) x) x)) #Hcase
309 [>bigop_Strue [2:@Hcase] #Hmax cases (max_neq0 … Hmax) -Hmax
310 [2: #H %{x} % // <minus_n_O @H]
311 #Hneq0 (* if x is not enough we retry with nu=x *)
312 cases (Hind x) #x1 * #ltx1
314 [#H %{x1} % [@transitive_lt //| <minus_n_O @H]
315 |@not_eq_to_eqb_false >(le_to_min_input … (eqb_true_to_eq … Hcase))
316 [@lt_to_not_eq @ltx1 | @lt_to_le @ltx1]
318 |>bigop_Sfalse [2:@Hcase] #H %{x} % // <minus_n_O @H
323 lemma condition_1: ∀h,u.g h 0 ≈ g h u.
324 #h #u @(not_to_not … (eventually_cancelled h u))
325 #H #nu cases (H (max u nu)) #x * #ltx #Hdiff
326 %{x} % [@(le_to_lt_to_lt … ltx) @(le_maxr … (le_n …))] @(not_to_not … Hdiff)
327 #H @(eq_f ?? S) >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat 0 MaxA)
328 [>H // |@lt_to_le @(le_to_lt_to_lt …ltx) /2 by le_maxr/ |//]
331 (******************************** Condition 2 *********************************)
332 definition total ≝ λf.λx:nat. Some nat (f x).
334 lemma exists_to_exists_min: ∀h,i. (∃x. i < x ∧ {i ⊙ x} ↓ h (S i) x) → ∃y. min_input h i y = y.
335 #h #i * #x * #ltix #Hx %{(min_input h i x)} @min_spec_to_min @found //
336 [@(f_min_true (λy:ℕ.termb i y (h (S i) y))) %{x} % [% // | @term_to_termb_true //]
337 |#y #leiy #lty @(lt_min_to_false ????? lty) //
341 lemma condition_2: ∀h,i. code_for (total (g h 0)) i → ¬∃x. i<x ∧ {i ⊙ x} ↓ h (S i) x.
342 #h #i whd in ⊢(%→?); #H % #H1 cases (exists_to_exists_min … H1) #y #Hminy
343 lapply (g_lt … Hminy)
344 lapply (min_input_to_terminate … Hminy) * #r #termy
345 cases (H y) -H #ny #Hy
346 cut (r = g h 0 y) [@(unique_U … ny … termy) @Hy //] #Hr
347 whd in match (out ???); >termy >Hr
348 #H @(absurd ? H) @le_to_not_lt @le_n
352 (********************** complexity ***********************)
354 (* We assume operations have a minimal structural complexity MSC.
355 For instance, for time complexity, MSC is equal to the size of input.
356 For space complexity, MSC is typically 0, since we only measure the
357 space required in addition to dimension of the input. *)
359 axiom MSC : nat → nat.
360 axiom MSC_le: ∀n. MSC n ≤ n.
361 axiom monotonic_MSC: monotonic ? le MSC.
362 axiom MSC_pair: ∀a,b. MSC 〈a,b〉 ≤ MSC a + MSC b.
364 (* C s i means i is running in O(s) *)
366 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ x → ∃y.
367 U i x (c*(s x)) = Some ? y.
369 (* C f s means f ∈ O(s) where MSC ∈O(s) *)
370 definition CF ≝ λs,f.O s MSC ∧ ∃i.code_for (total f) i ∧ C s i.
372 lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
373 #f #g #s #Hext * #HO * #i * #Hcode #HC % // %{i} %
374 [#x cases (Hcode x) #a #H %{a} whd in match (total ??); <Hext @H | //]
377 (* lemma ext_CF_total : ∀f,g,s. (∀n. f n = g n) → CF s (total f) → CF s (total g).
378 #f #g #s #Hext * #HO * #i * #Hcode #HC % // %{i} % [2:@HC]
379 #x cases (Hcode x) #a #H %{a} #m #leam >(H m leam) normalize @eq_f @Hext
382 lemma monotonic_CF: ∀s1,s2,f.(∀x. s1 x ≤ s2 x) → CF s1 f → CF s2 f.
383 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
384 [cases HO #c * #a -HO #HO %{c} %{a} #n #lean @(transitive_le … (HO n lean))
386 |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1 %{c} %{a} #n #lean
387 cases(Hs1 n lean) #y #Hy %{y} @(monotonic_U …Hy) @le_times //
391 lemma O_to_CF: ∀s1,s2,f.O s2 s1 → CF s1 f → CF s2 f.
392 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
394 |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1
395 cases H #c1 * #a1 #Ha1 %{(c*c1)} %{(a+a1)} #n #lean
396 cases(Hs1 n ?) [2:@(transitive_le … lean) //] #y #Hy %{y} @(monotonic_U …Hy)
397 >associative_times @le_times // @Ha1 @(transitive_le … lean) //
401 lemma timesc_CF: ∀s,f,c.CF (λx.c*s x) f → CF s f.
402 #s #f #c @O_to_CF @O_times_c
405 (********************************* composition ********************************)
406 axiom CF_comp: ∀f,g,sf,sg,sh. CF sg g → CF sf f →
407 O sh (λx. sg x + sf (g x)) → CF sh (f ∘ g).
409 lemma CF_comp_ext: ∀f,g,h,sh,sf,sg. CF sg g → CF sf f →
410 (∀x.f(g x) = h x) → O sh (λx. sg x + sf (g x)) → CF sh h.
411 #f #g #h #sh #sf #sg #Hg #Hf #Heq #H @(ext_CF (f ∘ g))
412 [#n normalize @Heq | @(CF_comp … H) //]
416 lemma CF_comp1: ∀f,g,s. CF s (total g) → CF s (total f) →
417 CF s (total (f ∘ g)).
418 #f #g #s #Hg #Hf @(timesc_CF … 2) @(monotonic_CF … (CF_comp … Hg Hf))
422 axiom CF_comp_ext2: ∀f,g,h,sf,sh. CF sh (total g) → CF sf (total f) →
424 (∀x. sf (g x) ≤ sh x) → CF sh (total h).
426 lemma main_MSC: ∀h,f. CF h f → O h (λx.MSC (f x)).
428 axiom CF_S: CF MSC S.
429 axiom CF_fst: CF MSC fst.
430 axiom CF_snd: CF MSC snd.
432 lemma CF_compS: ∀h,f. CF h f → CF h (S ∘ f).
433 #h #f #Hf @(CF_comp … Hf CF_S) @O_plus // @main_MSC //
436 lemma CF_comp_fst: ∀h,f. CF h (total f) → CF h (total (fst ∘ f)).
437 #h #f #Hf @(CF_comp … Hf CF_fst) @O_plus // @main_MSC //
440 lemma CF_comp_snd: ∀h,f. CF h (total f) → CF h (total (snd ∘ f)).
441 #h #f #Hf @(CF_comp … Hf CF_snd) @O_plus // @main_MSC //
444 definition id ≝ λx:nat.x.
446 axiom CF_id: CF MSC id.
447 axiom CF_compS: ∀h,f. CF h f → CF h (S ∘ f).
448 axiom CF_comp_fst: ∀h,f. CF h f → CF h (fst ∘ f).
449 axiom CF_comp_snd: ∀h,f. CF h f → CF h (snd ∘ f).
450 axiom CF_comp_pair: ∀h,f,g. CF h f → CF h g → CF h (λx. 〈f x,g x〉).
452 lemma CF_fst: CF MSC fst.
453 @(ext_CF (fst ∘ id)) [#n //] @(CF_comp_fst … CF_id)
456 lemma CF_snd: CF MSC snd.
457 @(ext_CF (snd ∘ id)) [#n //] @(CF_comp_snd … CF_id)
460 (************************************** eqb ***********************************)
461 (* definition btotal ≝
462 λf.λx:nat. match f x with [true ⇒ Some ? 0 |false ⇒ Some ? 1]. *)
464 axiom CF_eqb: ∀h,f,g.
465 CF h f → CF h g → CF h (λx.eqb (f x) (g x)).
468 axiom eqb_compl2: ∀h,f,g.
469 CF2 h (total2 f) → CF2 h (total2 g) →
470 CF2 h (btotal2 (λx1,x2.eqb (f x1 x2) (g x1 x2))).
472 axiom eqb_min_input_compl:∀h,x.
473 CF (λi.∑_{y ∈ [S i,S x[ }(h i y))
474 (btotal (λi.eqb (min_input h i x) x)). *)
475 (*********************************** maximum **********************************)
477 axiom CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
478 CF ha a → CF hb b → CF hp p → CF hf f →
479 O s (λx.ha x + hb x + ∑_{i ∈[a x ,b x[ }(hp 〈i,x〉 + hf 〈i,x〉)) →
480 CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
482 (******************************** minimization ********************************)
484 axiom CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
485 CF sa a → CF sb b → CF sf f →
486 O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
487 CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
489 (****************************** constructibility ******************************)
491 definition constructible ≝ λs. CF s s.
493 lemma constr_comp : ∀s1,s2. constructible s1 → constructible s2 →
494 (∀x. x ≤ s2 x) → constructible (s2 ∘ s1).
495 #s1 #s2 #Hs1 #Hs2 #Hle @(CF_comp … Hs1 Hs2) @O_plus @le_to_O #x [@Hle | //]
498 lemma ext_constr: ∀s1,s2. (∀x.s1 x = s2 x) →
499 constructible s1 → constructible s2.
500 #s1 #s2 #Hext #Hs1 @(ext_CF … Hext) @(monotonic_CF … Hs1) #x >Hext //
503 (********************************* simulation *********************************)
505 axiom sU : nat → nat.
507 axiom monotonic_sU: ∀i1,i2,x1,x2,s1,s2. i1 ≤ i2 → x1 ≤ x2 → s1 ≤ s2 →
508 sU 〈i1,〈x1,s1〉〉 ≤ sU 〈i2,〈x2,s2〉〉.
510 lemma monotonic_sU_aux : ∀x1,x2. fst x1 ≤ fst x2 → fst (snd x1) ≤ fst (snd x2) →
511 snd (snd x1) ≤ snd (snd x2) → sU x1 ≤ sU x2.
512 #x1 #x2 cases (surj_pair x1) #a1 * #y #eqx1 >eqx1 -eqx1 cases (surj_pair y)
513 #b1 * #c1 #eqy >eqy -eqy
514 cases (surj_pair x2) #a2 * #y2 #eqx2 >eqx2 -eqx2 cases (surj_pair y2)
515 #b2 * #c2 #eqy2 >eqy2 -eqy2 >fst_pair >snd_pair >fst_pair >snd_pair
516 >fst_pair >snd_pair >fst_pair >snd_pair @monotonic_sU
519 axiom sU_le: ∀i,x,s. s ≤ sU 〈i,〈x,s〉〉.
520 axiom sU_le_i: ∀i,x,s. MSC i ≤ sU 〈i,〈x,s〉〉.
521 axiom sU_le_x: ∀i,x,s. MSC x ≤ sU 〈i,〈x,s〉〉.
523 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
525 axiom CF_U : CF sU pU_unary.
527 definition termb_unary ≝ λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)).
528 definition out_unary ≝ λx:ℕ.out (fst x) (fst (snd x)) (snd (snd x)).
530 lemma CF_termb: CF sU termb_unary.
531 @(ext_CF (fst ∘ pU_unary)) [2: @CF_comp_fst @CF_U]
532 #n whd in ⊢ (??%?); whd in ⊢ (??(?%)?); >fst_pair %
535 lemma CF_out: CF sU out_unary.
536 @(ext_CF (snd ∘ pU_unary)) [2: @CF_comp_snd @CF_U]
537 #n whd in ⊢ (??%?); whd in ⊢ (??(?%)?); >snd_pair %
541 lemma CF_termb_comp: ∀f.CF (sU ∘ f) (termb_unary ∘ f).
542 #f @(CF_comp … CF_termb) *)
544 (******************** complexity of g ********************)
546 definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
548 λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
549 (out i (snd ux) (h (S i) (snd ux))).
551 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
552 #h #s #H1 @(CF_compS ? (auxg h) H1)
556 λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
557 ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
559 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
561 [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
564 lemma compl_g2 : ∀h,s1,s2,s.
566 (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
568 (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
569 O s (λx.MSC x + ∑_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
571 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
572 [#n whd in ⊢ (??%%); @eq_aux]
573 @(CF_max … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
574 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
577 lemma compl_g3 : ∀h,s.
578 CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
579 CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
580 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (proj1 … H))
581 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
584 definition min_input_aux ≝ λh,p.
585 μ_{y ∈ [S (fst p),snd (snd p)] }
586 ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
588 lemma min_input_eq : ∀h,p.
590 min_input h (fst p) (snd (snd p)).
591 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
592 whd in ⊢ (??%%); >fst_pair >snd_pair //
595 definition termb_aux ≝ λh.
596 termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
599 lemma termb_aux : ∀h,p.
600 (λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)))
601 〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉 =
602 termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)) .
603 #h #p normalize >fst_pair >snd_pair >fst_pair >snd_pair //
606 lemma compl_g4 : ∀h,s1,s.
608 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
609 (O s (λx.MSC x + ∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
610 CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
611 #h #s1 #s #Hs1 #HO @(ext_CF (min_input_aux h))
612 [#n whd in ⊢ (??%%); @min_input_eq]
613 @(CF_mu … MSC MSC … Hs1)
615 |@CF_comp_snd @CF_snd
616 |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
617 (* @(ext_CF (btotal (termb_aux h)))
618 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
619 @(CF_compb … CF_termb) *)
622 (************************* a couple of technical lemmas ***********************)
623 lemma minus_to_0: ∀a,b. a ≤ b → minus a b = 0.
624 #a elim a // #n #Hind *
625 [#H @False_ind /2 by absurd/ | #b normalize #H @Hind @le_S_S_to_le /2/]
628 lemma sigma_bound: ∀h,a,b. monotonic nat le h →
629 ∑_{i ∈ [a,S b[ }(h i) ≤ (S b-a)*h b.
630 #h #a #b #H cases (decidable_le a b)
631 [#leab cut (b = pred (S b - a + a))
632 [<plus_minus_m_m // @le_S //] #Hb >Hb in match (h b);
633 generalize in match (S b -a);
636 |#m #Hind >bigop_Strue [2://] @le_plus
637 [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
639 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
640 cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
644 lemma sigma_bound_decr: ∀h,a,b. (∀a1,a2. a1 ≤ a2 → a2 < b → h a2 ≤ h a1) →
645 ∑_{i ∈ [a,b[ }(h i) ≤ (b-a)*h a.
646 #h #a #b #H cases (decidable_le a b)
647 [#leab cut ((b -a) +a ≤ b) [/2 by le_minus_to_plus_r/] generalize in match (b -a);
650 |#m #Hind >bigop_Strue [2://] #Hm
651 cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
652 @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
654 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
655 cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
659 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
660 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
661 (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
662 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
663 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
666 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
667 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
668 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
669 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
672 lemma compl_g5 : ∀h,s1.(∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
674 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
675 CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
676 (λp:ℕ.min_input h (fst p) (snd (snd p))).
677 #h #s1 #Hmono #Hs1 @(compl_g4 … Hs1) @O_plus
678 [@O_plus_l // |@O_plus_r @coroll @Hmono]
683 (* constructible (λx. h (fst x) (snd x)) → *)
684 (CF (λx. max (MSC x) (sU 〈fst (snd x),〈fst x,h (S (fst (snd x))) (fst x)〉〉))
685 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
689 constructible (λx. h (fst x) (snd x)) →
690 (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
691 (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
692 #h #hconstr @(ext_CF (termb_aux h))
693 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
694 @(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
696 [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
698 [@(monotonic_CF … CF_fst) #x //
699 |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
700 [#n normalize >fst_pair >snd_pair %]
701 @(CF_comp … MSC …hconstr)
702 [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
703 |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
709 [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
710 [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
711 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
712 >distributive_times_plus @le_plus [//]
713 cases (surj_pair b) #c * #d #eqb >eqb
714 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
715 whd in ⊢ (??%); @le_plus
716 [@monotonic_MSC @(le_maxl … (le_n …))
717 |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
719 |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
723 |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
727 (* definition faux1 ≝ λh.
728 (λ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〉).
730 (* complexity of min_input *)
732 (∀x.MSC x≤h (S (fst (snd x))) (fst x)) →
733 constructible (λx. h (fst x) (snd x)) →
734 (∀n. monotonic ? le (h n)) →
735 CF (λx.MSC x + (snd (snd x)-fst x)*sU 〈fst x,〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
736 (λp:ℕ.min_input h (fst p) (snd (snd p))).
737 #h #hle #hcostr #hmono @(monotonic_CF … (faux1 h))
738 [#n normalize >fst_pair >snd_pair //]
739 @compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
740 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
743 definition big : nat →nat ≝ λx.
744 let m ≝ max (fst x) (snd x) in 〈m,m〉.
746 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
747 #a #b normalize >fst_pair >snd_pair // qed.
749 lemma le_big : ∀x. x ≤ big x.
750 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
751 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
754 definition faux2 ≝ λh.
755 (λx.MSC x + (snd (snd x)-fst x)*
756 (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
760 constructible (λx. h (fst x) (snd x)) →
761 (∀n. monotonic ? le (h n)) →
762 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))〉〉)
763 (λp:ℕ.min_input h (fst p) (snd (snd p))).
764 #h #hcostr #hmono @(monotonic_CF … (faux2 h))
765 [#n normalize >fst_pair >snd_pair //]
766 @compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
767 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
772 constructible (λx. h (fst x) (snd x)) →
773 (∀n. monotonic ? le (h n)) →
774 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))〉〉)
775 (λp:ℕ.min_input h (fst p) (snd (snd p))).
776 #h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x
777 @le_plus [@monotonic_MSC //]
778 cases (decidable_le (fst x) (snd(snd x)))
779 [#Hle @le_times // @monotonic_sU
780 |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
786 CF (λx. sU 〈fst x,〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
787 (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))). *)
789 definition out_aux ≝ λh.
790 out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
793 constructible (λx. h (fst x) (snd x)) →
794 (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
795 (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
796 #h #hconstr @(ext_CF (out_aux h))
797 [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
798 @(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
800 [@(monotonic_CF … CF_fst) #x //
802 [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
803 |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
804 [#n normalize >fst_pair >snd_pair %]
805 @(CF_comp … MSC …hconstr)
806 [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
807 |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
814 |@(O_trans … (λx.MSC (max (fst x) (snd x))))
815 [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
816 >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
817 whd in ⊢ (??%); @le_plus
818 [@monotonic_MSC @(le_maxl … (le_n …))
819 |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
821 |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
824 |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
830 (∀x.MSC x≤h (S (fst x)) (snd(snd x))) →
831 constructible (λx. h (fst x) (snd x)) →
832 CF (λx. sU 〈max (fst x) (snd x),〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
833 (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))).
834 #h #hle #hconstr @(monotonic_CF ???? (compl_g8 h hle hconstr)) #x @monotonic_sU // @(le_maxl … (le_n … ))
837 (* axiom daemon : False. *)
840 constructible (λx. h (fst x) (snd x)) →
841 (∀n. monotonic ? le (h n)) →
842 (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
843 CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
844 (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
846 #h #hconstr #hmono #hantimono
847 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
849 [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
850 [// | @monotonic_MSC // ]]
851 @(O_trans … (coroll2 ??))
852 [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
853 cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
855 [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
856 cut (max b n = n) [normalize >le_to_leb_true //] #maxb
858 [@le_plus [>big_def >big_def >maxa >maxb //]
860 [/2 by monotonic_le_minus_r/
861 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
863 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
865 |@le_to_O #n >fst_pair >snd_pair
866 cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
867 >associative_plus >distributive_times_plus
868 @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
872 definition sg ≝ λh,x.
873 (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)〉〉.
875 lemma sg_def : ∀h,a,b.
876 sg h 〈a,b〉 = (S (b-a))*MSC 〈〈a,b〉,〈a,b〉〉 +
877 (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
878 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
881 lemma compl_g11 : ∀h.
882 constructible (λx. h (fst x) (snd x)) →
883 (∀n. monotonic ? le (h n)) →
884 (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
885 CF (sg h) (unary_g h).
886 #h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)
889 (**************************** closing the argument ****************************)
891 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
893 [ O ⇒ c (* MSC 〈〈b,b〉,〈b,b〉〉 *)
894 | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
895 d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
897 lemma h_of_aux_O: ∀r,c,b.
898 h_of_aux r c O b = c.
901 lemma h_of_aux_S : ∀r,c,d,b.
902 h_of_aux r c (S d) b =
903 (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
904 (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
907 definition h_of ≝ λr,p.
908 let m ≝ max (fst p) (snd p) in
909 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
911 lemma h_of_O: ∀r,a,b. b ≤ a →
912 h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
913 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
916 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
918 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
919 #r #a #b normalize >fst_pair >snd_pair //
922 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
923 ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
924 h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
925 #r #Hr #monor #d #d1 lapply d -d elim d1
926 [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
927 >h_of_aux_O >h_of_aux_O //
928 |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
929 [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
930 >h_of_aux_S @(transitive_le ???? (le_plus_n …))
931 >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
932 >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
933 |#Hd >Hd >h_of_aux_S >h_of_aux_S
934 cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
935 @le_plus [@le_times //]
936 [@monotonic_MSC @le_pair @le_pair //
937 |@le_times [//] @monotonic_sU
938 [@le_pair // |// |@monor @Hind //]
944 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
945 ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
946 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
947 cut (max i a ≤ max i b)
949 [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
950 #Hmax @(mono_h_of_aux r Hr Hmono)
951 [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
954 axiom h_of_constr : ∀r:nat →nat.
955 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
956 constructible (h_of r).
958 lemma speed_compl: ∀r:nat →nat.
959 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
960 CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
961 #r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …))
962 [#x cases (surj_pair x) #a * #b #eqx >eqx
963 >sg_def cases (decidable_le b a)
964 [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
965 <plus_n_O <plus_n_O >h_of_def
967 [normalize cases (le_to_or_lt_eq … leba)
968 [#ltba >(lt_to_leb_false … ltba) %
969 |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
970 #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
971 @monotonic_MSC @le_pair @le_pair //
972 |#ltab >h_of_def >h_of_def
974 [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
976 cut (max (S a) b = b)
977 [whd in ⊢ (??%?); >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
980 [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
982 cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
984 [@plus_to_minus >commutative_plus @minus_to_plus
985 [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
988 |#n #a #b #leab #lebn >h_of_def >h_of_def
990 [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
992 [normalize >(le_to_leb_true … lebn) %] #Hmaxb
993 >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
994 |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
995 |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
996 [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]
997 @(h_of_constr r Hr Hmono Hconstr)
1002 lemma unary_g_def : ∀h,i,x. g h i x = unary_g h 〈i,x〉.
1003 #h #i #x whd in ⊢ (???%); >fst_pair >snd_pair %
1007 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
1009 lemma speed_compl_i: ∀r:nat →nat.
1010 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1011 ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
1012 #r #Hr #Hmono #Hconstr #i
1013 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
1014 [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
1015 @smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //
1018 theorem pseudo_speedup:
1019 ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1020 ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
1021 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
1022 #r #Hr #Hmono #Hconstr
1023 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
1024 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
1026 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
1027 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
1028 (* sg is (λx.h_of r 〈i,x〉) *)
1029 %{(λx. h_of r 〈S i,x〉)}
1030 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
1031 %[%[@condition_1 |@Hg]
1032 |cases Hg #H1 * #j * #Hcodej #HCj
1033 lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
1034 cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
1035 @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
1036 [@(transitive_le … ltin) @(le_maxl … (le_n …))]
1037 cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
1038 #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
1042 theorem pseudo_speedup':
1043 ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1044 ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
1045 (* ¬ O (r ∘ sg) sf. *)
1046 ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
1047 #r #Hr #Hmono #Hconstr
1048 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
1049 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
1051 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
1052 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
1053 (* sg is (λx.h_of r 〈i,x〉) *)
1054 %{(λx. h_of r 〈S i,x〉)}
1055 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
1056 %[%[@condition_1 |@Hg]
1057 |cases Hg #H1 * #j * #Hcodej #HCj
1058 lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
1059 cases HCi #m * #a #Ha
1060 %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2 #Hlesf
1061 %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
1062 cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
1063 #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
1064 @Hmono @(mono_h_of2 … Hr Hmono … ltin)