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