matita/matita/lib/reverse_complexity/speed_new.ma

   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".
   8
   9 (************************* notation for minimization *****************************)
  10 notation "μ_{ ident i < n } p"
  11   with precedence 80 for @{min $n 0 (λ${ident i}.$p)}.
  12
  13 notation "μ_{ ident i ≤ n } p"
  14   with precedence 80 for @{min (S $n) 0 (λ${ident i}.$p)}.
  15
  16 notation "μ_{ ident i ∈ [a,b[ } p"
  17   with precedence 80 for @{min ($b-$a) $a (λ${ident i}.$p)}.
  18
  19 notation "μ_{ ident i ∈ [a,b] } p"
  20   with precedence 80 for @{min (S $b-$a) $a (λ${ident i}.$p)}.
  21
  22 (************************************ MAX *************************************)
  23 notation "Max_{ ident i < n | p } f"
  24   with precedence 80
  25 for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
  26
  27 notation "Max_{ ident i < n } f"
  28   with precedence 80
  29 for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}.
  30
  31 notation "Max_{ ident j ∈ [a,b[ } f"
  32   with precedence 80
  33 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
  34   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  35
  36 notation "Max_{ ident j ∈ [a,b[ | p } f"
  37   with precedence 80
  38 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
  39   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  40
  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 //
  45     |>leab //
  46     ]
  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 //
  50   ]
  51 qed.
  52
  53 lemma Max0 : ∀n. max 0 n = n.
  54 // qed.
  55
  56 lemma Max0r : ∀n. max n 0 = n.
  57 #n >commutative_max //
  58 qed.
  59
  60 definition MaxA ≝
  61   mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)).
  62
  63 definition MaxAC ≝ mk_ACop nat 0 MaxA commutative_max.
  64
  65 lemma le_Max: ∀f,p,n,a. a < n → p a = true →
  66   f a ≤  Max_{i < n | p i}(f i).
  67 #f #p #n #a #ltan #pa
  68 >(bigop_diff p ? 0 MaxAC f a n) // @(le_maxl … (le_n ?))
  69 qed.
  70
  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 ?))
  76   |<plus_minus_m_m //
  77   |/2 by monotonic_lt_minus_l/
  78   ]
  79 qed.
  80
  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 //
  87   ]
  88 qed.
  89
  90 (********************************** pairing ***********************************)
  91 axiom pair: nat → nat → nat.
  92 axiom fst : nat → nat.
  93 axiom snd : nat → nat.
  94
  95 interpretation "abstract pair" 'pair f g = (pair f g).
  96
  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〉.
 100
 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〉.
 104
 105 (************************************* U **************************************)
 106 axiom U: nat → nat →nat → option nat.
 107
 108 axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
 109   U i x n = Some ? y → U i x m = Some ? y.
 110
 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) //
 117   ]
 118 qed.
 119
 120 definition code_for ≝ λf,i.∀x.
 121   ∃n.∀m. n ≤ m → U i x m = f x.
 122
 123 definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y.
 124
 125 notation "{i ⊙ x} ↓ r" with precedence 60 for @{terminate $i $x $r}.
 126
 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} //]
 130 qed.
 131
 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) //
 135 qed.
 136
 137 definition termb ≝ λi,x,t.
 138   match U i x t with [None ⇒ false |Some y ⇒ true].
 139
 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} //]
 142 qed.
 143
 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 //
 146 qed.
 147
 148 definition out ≝ λi,x,r.
 149   match U i x r with [ None ⇒ 0 | Some z ⇒ z].
 150
 151 definition bool_to_nat: bool → nat ≝
 152   λb. match b with [true ⇒ 1 | false ⇒ 0].
 153
 154 coercion bool_to_nat.
 155
 156 definition pU : nat → nat → nat → nat ≝ λi,x,r.〈termb i x r,out i x r〉.
 157
 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]
 162      #H1 destruct
 163     |#a #H cut (a=y) [lapply (eq_f … snd … H) >snd_pair >snd_pair #H1 @H1]
 164      #H1 //
 165     ]
 166   |#H >H //]
 167 qed.
 168
 169 lemma pU_vs_U_None : ∀i,x,r. pU i x r = 〈0,0〉 ↔ U i x r = None ?.
 170 #i #x #r % normalize
 171   [cases (U i x r) normalize //
 172    #a #H cut (1=0) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H1 @H1]
 173    #H1 destruct
 174   |#H >H //]
 175 qed.
 176
 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 //
 179 qed.
 180
 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 //
 183 qed.
 184
 185 (********************************* the speedup ********************************)
 186
 187 definition min_input ≝ λh,i,x. μ_{y ∈ [S i,x] } (termb i y (h (S i) y)).
 188
 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)).
 191 // qed.
 192
 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 //
 196 qed.
 197
 198 lemma min_input_to_terminate: ∀h,i,x.
 199   min_input h i x = x → {i ⊙ x} ↓ (h (S i) x).
 200 #h #i #x #Hminx
 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 //]
 207      #Habs @False_ind /2/
 208     ]
 209   |@False_ind >min_input_i in Hminx;
 210     [#eqix >eqix in Hix; * /2/ | @le_S_S_to_le @not_le_to_lt //]
 211   ]
 212 qed.
 213
 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 //]
 219 qed.
 220
 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)
 229   ]
 230 qed.
 231
 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))).
 234
 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))).
 237 // qed.
 238
 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.
 242
 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/
 246 qed.
 247
 248 lemma max_neq0 : ∀a,b. max a b ≠ 0 → a ≠ 0 ∨ b ≠ 0.
 249 #a #b whd in match (max a b); cases (true_or_false (leb a b)) #Hcase >Hcase
 250   [#H %2 @H | #H %1 @H]
 251 qed.
 252
 253 definition almost_equal ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
 254 interpretation "almost equal" 'napart f g = (almost_equal f g).
 255
 256 lemma eventually_cancelled: ∀h,u.¬∀nu.∃x. nu < x ∧
 257   max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) ≠ 0.
 258 #h #u elim u
 259   [normalize % #H cases (H u) #x * #_ * #H1 @H1 //
 260   |#u0 @not_to_not #Hind #nu cases (Hind nu) #x * #ltx
 261    cases (true_or_false (eqb (min_input h (u0+O) x) x)) #Hcase
 262     [>bigop_Strue [2:@Hcase] #Hmax cases (max_neq0 … Hmax) -Hmax
 263       [2: #H %{x} % // <minus_n_O @H]
 264      #Hneq0 (* if x is not enough we retry with nu=x *)
 265      cases (Hind x) #x1 * #ltx1
 266      >bigop_Sfalse
 267       [#H %{x1} % [@transitive_lt //| <minus_n_O @H]
 268       |@not_eq_to_eqb_false >(le_to_min_input … (eqb_true_to_eq … Hcase))
 269         [@lt_to_not_eq @ltx1 | @lt_to_le @ltx1]
 270       ]
 271     |>bigop_Sfalse [2:@Hcase] #H %{x} % // <minus_n_O @H
 272     ]
 273   ]
 274 qed.
 275
 276 lemma condition_1: ∀h,u.g h 0 ≈ g h u.
 277 #h #u @(not_to_not … (eventually_cancelled h u))
 278 #H #nu cases (H (max u nu)) #x * #ltx #Hdiff
 279 %{x} % [@(le_to_lt_to_lt … ltx) @(le_maxr … (le_n …))] @(not_to_not … Hdiff)
 280 #H @(eq_f ?? S) >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat  0 MaxA)
 281   [>H // |@lt_to_le @(le_to_lt_to_lt …ltx) /2 by le_maxr/ |//]
 282 qed.
 283
 284 (******************************** Condition 2 *********************************)
 285 definition total ≝ λf.λx:nat. Some nat (f x).
 286
 287 lemma exists_to_exists_min: ∀h,i. (∃x. i < x ∧ {i ⊙ x} ↓ h (S i) x) → ∃y. min_input h i y = y.
 288 #h #i * #x * #ltix #Hx %{(min_input h i x)} @min_spec_to_min @found //
 289   [@(f_min_true (λy:ℕ.termb i y (h (S i) y))) %{x} % [% // | @term_to_termb_true //]
 290   |#y #leiy #lty @(lt_min_to_false ????? lty) //
 291   ]
 292 qed.
 293
 294 lemma condition_2: ∀h,i. code_for (total (g h 0)) i → ¬∃x. i<x ∧ {i ⊙ x} ↓ h (S i) x.
 295 #h #i whd in ⊢(%→?); #H % #H1 cases (exists_to_exists_min … H1) #y #Hminy
 296 lapply (g_lt … Hminy)
 297 lapply (min_input_to_terminate … Hminy) * #r #termy
 298 cases (H y) -H #ny #Hy
 299 cut (r = g h 0 y) [@(unique_U … ny … termy) @Hy //] #Hr
 300 whd in match (out ???); >termy >Hr
 301 #H @(absurd ? H) @le_to_not_lt @le_n
 302 qed.
 303
 304
 305 (********************************* complexity *********************************)
 306
 307 (* We assume operations have a minimal structural complexity MSC.
 308 For instance, for time complexity, MSC is equal to the size of input.
 309 For space complexity, MSC is typically 0, since we only measure the
 310 space required in addition to dimension of the input. *)
 311
 312 axiom MSC : nat → nat.
 313 axiom MSC_le: ∀n. MSC n ≤ n.
 314 axiom monotonic_MSC: monotonic ? le MSC.
 315 axiom MSC_pair: ∀a,b. MSC 〈a,b〉 ≤ MSC a + MSC b.
 316
 317 (* C s i means i is running in O(s) *)
 318
 319 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ x → ∃y.
 320   U i x (c*(s x)) = Some ? y.
 321
 322 (* C f s means f ∈ O(s) where MSC ∈O(s) *)
 323 definition CF ≝ λs,f.O s MSC ∧ ∃i.code_for (total f) i ∧ C s i.
 324
 325 lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
 326 #f #g #s #Hext * #HO  * #i * #Hcode #HC % // %{i} %
 327   [#x cases (Hcode x) #a #H %{a} whd in match (total ??); <Hext @H | //]
 328 qed.
 329
 330 lemma monotonic_CF: ∀s1,s2,f.(∀x. s1 x ≤  s2 x) → CF s1 f → CF s2 f.
 331 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
 332   [cases HO #c * #a -HO #HO %{c} %{a} #n #lean @(transitive_le … (HO n lean))
 333    @le_times //
 334   |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1 %{c} %{a} #n #lean
 335    cases(Hs1 n lean) #y #Hy %{y} @(monotonic_U …Hy) @le_times //
 336   ]
 337 qed.
 338
 339 lemma O_to_CF: ∀s1,s2,f.O s2 s1 → CF s1 f → CF s2 f.
 340 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
 341   [@(O_trans … H) //
 342   |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1
 343    cases H #c1 * #a1 #Ha1 %{(c*c1)} %{(a+a1)} #n #lean
 344    cases(Hs1 n ?) [2:@(transitive_le … lean) //] #y #Hy %{y} @(monotonic_U …Hy)
 345    >associative_times @le_times // @Ha1 @(transitive_le … lean) //
 346   ]
 347 qed.
 348
 349 lemma timesc_CF: ∀s,f,c.CF (λx.c*s x) f → CF s f.
 350 #s #f #c @O_to_CF @O_times_c
 351 qed.
 352
 353 (********************************* composition ********************************)
 354 axiom CF_comp: ∀f,g,sf,sg,sh. CF sg g → CF sf f →
 355   O sh (λx. sg x + sf (g x)) → CF sh (f ∘ g).
 356
 357 lemma CF_comp_ext: ∀f,g,h,sh,sf,sg. CF sg g → CF sf f →
 358   (∀x.f(g x) = h x) → O sh (λx. sg x + sf (g x)) → CF sh h.
 359 #f #g #h #sh #sf #sg #Hg #Hf #Heq #H @(ext_CF (f ∘ g))
 360   [#n normalize @Heq | @(CF_comp … H) //]
 361 qed.
 362
 363
 364 (**************************** primitive operations*****************************)
 365
 366 definition id ≝ λx:nat.x.
 367
 368 axiom CF_id: CF MSC id.
 369 axiom CF_compS: ∀h,f. CF h f → CF h (S ∘ f).
 370 axiom CF_comp_fst: ∀h,f. CF h f → CF h (fst ∘ f).
 371 axiom CF_comp_snd: ∀h,f. CF h f → CF h (snd ∘ f).
 372 axiom CF_comp_pair: ∀h,f,g. CF h f → CF h g → CF h (λx. 〈f x,g x〉).
 373
 374 lemma CF_fst: CF MSC fst.
 375 @(ext_CF (fst ∘ id)) [#n //] @(CF_comp_fst … CF_id)
 376 qed.
 377
 378 lemma CF_snd: CF MSC snd.
 379 @(ext_CF (snd ∘ id)) [#n //] @(CF_comp_snd … CF_id)
 380 qed.
 381
 382 (************************************** eqb ***********************************)
 383
 384 axiom CF_eqb: ∀h,f,g.
 385   CF h f → CF h g → CF h (λx.eqb (f x) (g x)).
 386
 387 (*********************************** maximum **********************************)
 388
 389 axiom CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
 390   CF ha a → CF hb b → CF hp p → CF hf f →
 391   O s (λx.ha x + hb x + ∑_{i ∈[a x ,b x[ }(hp 〈i,x〉 + hf 〈i,x〉)) →
 392   CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
 393
 394 (******************************** minimization ********************************)
 395
 396 axiom CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
 397   CF sa a → CF sb b → CF sf f →
 398   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
 399   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
 400
 401 (************************************* smn ************************************)
 402 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
 403
 404 (****************************** constructibility ******************************)
 405
 406 definition constructible ≝ λs. CF s s.
 407
 408 lemma constr_comp : ∀s1,s2. constructible s1 → constructible s2 →
 409   (∀x. x ≤ s2 x) → constructible (s2 ∘ s1).
 410 #s1 #s2 #Hs1 #Hs2 #Hle @(CF_comp … Hs1 Hs2) @O_plus @le_to_O #x [@Hle | //]
 411 qed.
 412
 413 lemma ext_constr: ∀s1,s2. (∀x.s1 x = s2 x) →
 414   constructible s1 → constructible s2.
 415 #s1 #s2 #Hext #Hs1 @(ext_CF … Hext) @(monotonic_CF … Hs1)  #x >Hext //
 416 qed.
 417
 418 (********************************* simulation *********************************)
 419
 420 axiom sU : nat → nat.
 421
 422 axiom monotonic_sU: ∀i1,i2,x1,x2,s1,s2. i1 ≤ i2 → x1 ≤ x2 → s1 ≤ s2 →
 423   sU 〈i1,〈x1,s1〉〉 ≤ sU 〈i2,〈x2,s2〉〉.
 424
 425 lemma monotonic_sU_aux : ∀x1,x2. fst x1 ≤ fst x2 → fst (snd x1) ≤ fst (snd x2) →
 426 snd (snd x1) ≤ snd (snd x2) → sU x1 ≤ sU x2.
 427 #x1 #x2 cases (surj_pair x1) #a1 * #y #eqx1 >eqx1 -eqx1 cases (surj_pair y)
 428 #b1 * #c1 #eqy >eqy -eqy
 429 cases (surj_pair x2) #a2 * #y2 #eqx2 >eqx2 -eqx2 cases (surj_pair y2)
 430 #b2 * #c2 #eqy2 >eqy2 -eqy2 >fst_pair >snd_pair >fst_pair >snd_pair
 431 >fst_pair >snd_pair >fst_pair >snd_pair @monotonic_sU
 432 qed.
 433
 434 axiom sU_le: ∀i,x,s. s ≤ sU 〈i,〈x,s〉〉.
 435 axiom sU_le_i: ∀i,x,s. MSC i ≤ sU 〈i,〈x,s〉〉.
 436 axiom sU_le_x: ∀i,x,s. MSC x ≤ sU 〈i,〈x,s〉〉.
 437
 438 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
 439
 440 axiom CF_U : CF sU pU_unary.
 441
 442 definition termb_unary ≝ λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)).
 443 definition out_unary ≝ λx:ℕ.out (fst x) (fst (snd x)) (snd (snd x)).
 444
 445 lemma CF_termb: CF sU termb_unary.
 446 @(ext_CF (fst ∘ pU_unary)) [2: @CF_comp_fst @CF_U]
 447 #n whd in ⊢ (??%?); whd in  ⊢ (??(?%)?); >fst_pair %
 448 qed.
 449
 450 lemma CF_out: CF sU out_unary.
 451 @(ext_CF (snd ∘ pU_unary)) [2: @CF_comp_snd @CF_U]
 452 #n whd in ⊢ (??%?); whd in  ⊢ (??(?%)?); >snd_pair %
 453 qed.
 454
 455
 456 (******************** complexity of g ********************)
 457
 458 definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
 459 definition auxg ≝
 460   λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
 461     (out i (snd ux) (h (S i) (snd ux))).
 462
 463 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
 464 #h #s #H1 @(CF_compS ? (auxg h) H1)
 465 qed.
 466
 467 definition aux1g ≝
 468   λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
 469     ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
 470
 471 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
 472 #h #x @same_bigop
 473   [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
 474 qed.
 475
 476 lemma compl_g2 : ∀h,s1,s2,s.
 477   CF s1
 478     (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
 479   CF s2
 480     (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
 481   O s (λx.MSC x + ∑_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
 482   CF s (auxg h).
 483 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
 484   [#n whd in ⊢ (??%%); @eq_aux]
 485 @(CF_max … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
 486 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
 487 qed.
 488
 489 lemma compl_g3 : ∀h,s.
 490   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
 491   CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
 492 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (proj1 … H))
 493 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
 494 qed.
 495
 496 definition min_input_aux ≝ λh,p.
 497   μ_{y ∈ [S (fst p),snd (snd p)] }
 498     ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
 499
 500 lemma min_input_eq : ∀h,p.
 501     min_input_aux h p  =
 502     min_input h (fst p) (snd (snd p)).
 503 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
 504 whd in ⊢ (??%%); >fst_pair >snd_pair //
 505 qed.
 506
 507 definition termb_aux ≝ λh.
 508   termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
 509
 510 lemma compl_g4 : ∀h,s1,s.
 511   (CF s1
 512     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
 513    (O s (λx.MSC x + ∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
 514   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
 515 #h #s1 #s #Hs1 #HO @(ext_CF (min_input_aux h))
 516  [#n whd in ⊢ (??%%); @min_input_eq]
 517 @(CF_mu … MSC MSC … Hs1)
 518   [@CF_compS @CF_fst
 519   |@CF_comp_snd @CF_snd
 520   |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
 521 qed.
 522
 523 (************************* a couple of technical lemmas ***********************)
 524 lemma minus_to_0: ∀a,b. a ≤ b → minus a b = 0.
 525 #a elim a // #n #Hind *
 526   [#H @False_ind /2 by absurd/ | #b normalize #H @Hind @le_S_S_to_le /2/]
 527 qed.
 528
 529 lemma sigma_bound:  ∀h,a,b. monotonic nat le h →
 530   ∑_{i ∈ [a,S b[ }(h i) ≤  (S b-a)*h b.
 531 #h #a #b #H cases (decidable_le a b)
 532   [#leab cut (b = pred (S b - a + a))
 533     [<plus_minus_m_m // @le_S //] #Hb >Hb in match (h b);
 534    generalize in match (S b -a);
 535    #n elim n
 536     [//
 537     |#m #Hind >bigop_Strue [2://] @le_plus
 538       [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
 539     ]
 540   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
 541    cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
 542   ]
 543 qed.
 544
 545 lemma sigma_bound_decr:  ∀h,a,b. (∀a1,a2. a1 ≤ a2 → a2 < b → h a2 ≤ h a1) →
 546   ∑_{i ∈ [a,b[ }(h i) ≤  (b-a)*h a.
 547 #h #a #b #H cases (decidable_le a b)
 548   [#leab cut ((b -a) +a ≤ b) [/2 by le_minus_to_plus_r/] generalize in match (b -a);
 549    #n elim n
 550     [//
 551     |#m #Hind >bigop_Strue [2://] #Hm
 552      cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
 553      @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
 554     ]
 555   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
 556    cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
 557   ]
 558 qed.
 559
 560 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
 561 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
 562   (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
 563 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
 564 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
 565 qed.
 566
 567 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
 568 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
 569 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
 570 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
 571 qed.
 572
 573 (**************************** end of technical lemmas *************************)
 574
 575 lemma compl_g5 : ∀h,s1.(∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
 576   (CF s1
 577     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
 578   CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
 579     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 580 #h #s1 #Hmono #Hs1 @(compl_g4 … Hs1) @O_plus
 581 [@O_plus_l // |@O_plus_r @coroll @Hmono]
 582 qed.
 583
 584 lemma compl_g6: ∀h.
 585   constructible (λx. h (fst x) (snd x)) →
 586   (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
 587     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
 588 #h #hconstr @(ext_CF (termb_aux h))
 589   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
 590 @(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
 591   [@CF_comp_pair
 592     [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
 593     |@CF_comp_pair
 594       [@(monotonic_CF … CF_fst) #x //
 595       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
 596         [#n normalize >fst_pair >snd_pair %]
 597        @(CF_comp … MSC …hconstr)
 598         [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
 599         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
 600         ]
 601       ]
 602     ]
 603   |@O_plus
 604     [@O_plus
 605       [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
 606         [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
 607          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
 608          >distributive_times_plus @le_plus [//]
 609          cases (surj_pair b) #c * #d #eqb >eqb
 610          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
 611          whd in ⊢ (??%); @le_plus
 612           [@monotonic_MSC @(le_maxl … (le_n …))
 613           |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
 614           ]
 615         |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
 616         ]
 617       |@le_to_O #n @sU_le
 618       ]
 619     |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
 620   ]
 621 qed.
 622
 623 definition big : nat →nat ≝ λx.
 624   let m ≝ max (fst x) (snd x) in 〈m,m〉.
 625
 626 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
 627 #a #b normalize >fst_pair >snd_pair // qed.
 628
 629 lemma le_big : ∀x. x ≤ big x.
 630 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
 631 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
 632 qed.
 633
 634 definition faux2 ≝ λh.
 635   (λx.MSC x + (snd (snd x)-fst x)*
 636     (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
 637
 638 lemma compl_g7: ∀h.
 639   constructible (λx. h (fst x) (snd x)) →
 640   (∀n. monotonic ? le (h n)) →
 641   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))〉〉)
 642     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 643 #h #hcostr #hmono @(monotonic_CF … (faux2 h))
 644   [#n normalize >fst_pair >snd_pair //]
 645 @compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
 646 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
 647 qed.
 648
 649 lemma compl_g71: ∀h.
 650   constructible (λx. h (fst x) (snd x)) →
 651   (∀n. monotonic ? le (h n)) →
 652   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))〉〉)
 653     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 654 #h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x
 655 @le_plus [@monotonic_MSC //]
 656 cases (decidable_le (fst x) (snd(snd x)))
 657   [#Hle @le_times // @monotonic_sU
 658   |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
 659   ]
 660 qed.
 661
 662 definition out_aux ≝ λh.
 663   out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
 664
 665 lemma compl_g8: ∀h.
 666   constructible (λx. h (fst x) (snd x)) →
 667   (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
 668     (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
 669 #h #hconstr @(ext_CF (out_aux h))
 670   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
 671 @(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
 672   [@CF_comp_pair
 673     [@(monotonic_CF … CF_fst) #x //
 674     |@CF_comp_pair
 675       [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
 676       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
 677         [#n normalize >fst_pair >snd_pair %]
 678        @(CF_comp … MSC …hconstr)
 679         [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
 680         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
 681         ]
 682       ]
 683     ]
 684   |@O_plus
 685     [@O_plus
 686       [@le_to_O #n @sU_le
 687       |@(O_trans … (λx.MSC (max (fst x) (snd x))))
 688         [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
 689          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
 690          whd in ⊢ (??%); @le_plus
 691           [@monotonic_MSC @(le_maxl … (le_n …))
 692           |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
 693           ]
 694         |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
 695         ]
 696       ]
 697     |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
 698   ]
 699 qed.
 700
 701 lemma compl_g9 : ∀h.
 702   constructible (λx. h (fst x) (snd x)) →
 703   (∀n. monotonic ? le (h n)) →
 704   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
 705   CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
 706       (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
 707    (auxg h).
 708 #h #hconstr #hmono #hantimono
 709 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
 710 @O_plus
 711   [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
 712     [// | @monotonic_MSC // ]]
 713 @(O_trans … (coroll2 ??))
 714   [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
 715    cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
 716    cut (max a n = n)
 717     [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
 718    cut (max b n = n) [normalize >le_to_leb_true //] #maxb
 719    @le_plus
 720     [@le_plus [>big_def >big_def >maxa >maxb //]
 721      @le_times
 722       [/2 by monotonic_le_minus_r/
 723       |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
 724       ]
 725     |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
 726     ]
 727   |@le_to_O #n >fst_pair >snd_pair
 728    cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
 729    >associative_plus >distributive_times_plus
 730    @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
 731   ]
 732 qed.
 733
 734 definition sg ≝ λh,x.
 735   (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)〉〉.
 736
 737 lemma sg_def : ∀h,a,b.
 738   sg h 〈a,b〉 = (S (b-a))*MSC 〈〈a,b〉,〈a,b〉〉 +
 739    (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
 740 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
 741 qed.
 742
 743 lemma compl_g11 : ∀h.
 744   constructible (λx. h (fst x) (snd x)) →
 745   (∀n. monotonic ? le (h n)) →
 746   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
 747   CF (sg h) (unary_g h).
 748 #h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)
 749 qed.
 750
 751 (**************************** closing the argument ****************************)
 752
 753 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
 754   match d with
 755   [ O ⇒ c
 756   | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
 757      d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
 758
 759 lemma h_of_aux_O: ∀r,c,b.
 760   h_of_aux r c O b  = c.
 761 // qed.
 762
 763 lemma h_of_aux_S : ∀r,c,d,b.
 764   h_of_aux r c (S d) b =
 765     (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
 766       (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
 767 // qed.
 768
 769 definition h_of ≝ λr,p.
 770   let m ≝ max (fst p) (snd p) in
 771   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
 772
 773 lemma h_of_O: ∀r,a,b. b ≤ a →
 774   h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
 775 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
 776 qed.
 777
 778 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
 779   let m ≝ max a b in
 780   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
 781 #r #a #b normalize >fst_pair >snd_pair //
 782 qed.
 783
 784 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
 785   ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
 786   h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
 787 #r #Hr #monor #d #d1 lapply d -d elim d1
 788   [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
 789    >h_of_aux_O >h_of_aux_O  //
 790   |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
 791     [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
 792      >h_of_aux_S @(transitive_le ???? (le_plus_n …))
 793      >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
 794      >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
 795     |#Hd >Hd >h_of_aux_S >h_of_aux_S
 796      cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
 797      @le_plus [@le_times //]
 798       [@monotonic_MSC @le_pair @le_pair //
 799       |@le_times [//] @monotonic_sU
 800         [@le_pair // |// |@monor @Hind //]
 801       ]
 802     ]
 803   ]
 804 qed.
 805
 806 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
 807   ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
 808 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
 809 cut (max i a ≤ max i b)
 810   [@to_max
 811     [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
 812 #Hmax @(mono_h_of_aux r Hr Hmono)
 813   [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
 814 qed.
 815
 816 axiom h_of_constr : ∀r:nat →nat.
 817   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 818   constructible (h_of r).
 819
 820 lemma speed_compl: ∀r:nat →nat.
 821   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 822   CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
 823 #r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …))
 824   [#x cases (surj_pair x) #a * #b #eqx >eqx
 825    >sg_def cases (decidable_le b a)
 826     [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
 827      <plus_n_O <plus_n_O >h_of_def
 828      cut (max a b = a)
 829       [normalize cases (le_to_or_lt_eq … leba)
 830         [#ltba >(lt_to_leb_false … ltba) %
 831         |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
 832      #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
 833      @monotonic_MSC @le_pair @le_pair //
 834     |#ltab >h_of_def >h_of_def
 835      cut (max a b = b)
 836       [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
 837      #Hmax >Hmax
 838      cut (max (S a) b = b)
 839       [whd in ⊢ (??%?);  >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
 840      #Hmax1 >Hmax1
 841      cut (∃d.b - a = S d)
 842        [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
 843      * #d #eqd >eqd
 844      cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
 845      cut (b - S d = a)
 846        [@plus_to_minus >commutative_plus @minus_to_plus
 847          [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
 848      normalize //
 849     ]
 850   |#n #a #b #leab #lebn >h_of_def >h_of_def
 851    cut (max a n = n)
 852     [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
 853    cut (max b n = n)
 854     [normalize >(le_to_leb_true … lebn) %] #Hmaxb
 855    >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
 856   |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
 857   |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
 858     [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]
 859    @(h_of_constr r Hr Hmono Hconstr)
 860   ]
 861 qed.
 862
 863 lemma speed_compl_i: ∀r:nat →nat.
 864   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 865   ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
 866 #r #Hr #Hmono #Hconstr #i
 867 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
 868   [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
 869 @smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //
 870 qed.
 871
 872 (**************************** the speedup theorem *****************************)
 873 theorem pseudo_speedup:
 874   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 875   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
 876 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
 877 #r #Hr #Hmono #Hconstr
 878 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
 879 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
 880 #Hcodei #HCi
 881 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
 882 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 883 (* sg is (λx.h_of r 〈i,x〉) *)
 884 %{(λx. h_of r 〈S i,x〉)}
 885 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
 886 %[%[@condition_1 |@Hg]
 887  |cases Hg #H1 * #j * #Hcodej #HCj
 888   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
 889   cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
 890   @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
 891   [@(transitive_le … ltin) @(le_maxl … (le_n …))]
 892   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
 893   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
 894  ]
 895 qed.
 896
 897 theorem pseudo_speedup':
 898   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 899   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
 900   (* ¬ O (r ∘ sg) sf. *)
 901   ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
 902 #r #Hr #Hmono #Hconstr
 903 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
 904 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
 905 #Hcodei #HCi
 906 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
 907 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 908 (* sg is (λx.h_of r 〈i,x〉) *)
 909 %{(λx. h_of r 〈S i,x〉)}
 910 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
 911 %[%[@condition_1 |@Hg]
 912  |cases Hg #H1 * #j * #Hcodej #HCj
 913   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
 914   cases HCi #m * #a #Ha
 915   %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2 #Hlesf
 916   %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
 917   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
 918   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
 919   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
 920  ]
 921 qed.
 922