matita/matita/lib/reverse_complexity/speedup.ma

   1 include "reverse_complexity/bigops_compl.ma".
   2 include "basics/core_notation/napart_2.ma".
   3
   4 (********************************* the speedup ********************************)
   5
   6 definition min_input ≝ λh,i,x. μ_{y ∈ [S i,x] } (termb i y (h (S i) y)).
   7
   8 lemma min_input_def : ∀h,i,x.
   9   min_input h i x = min (x -i) (S i) (λy.termb i y (h (S i) y)).
  10 // qed.
  11
  12 lemma min_input_i: ∀h,i,x. x ≤ i → min_input h i x = S i.
  13 #h #i #x #lexi >min_input_def
  14 cut (x - i = 0) [@sym_eq /2 by eq_minus_O/] #Hcut //
  15 qed.
  16
  17 lemma min_input_to_terminate: ∀h,i,x.
  18   min_input h i x = x → {i ⊙ x} ↓ (h (S i) x).
  19 #h #i #x #Hminx
  20 cases (decidable_le (S i) x) #Hix
  21   [cases (true_or_false (termb i x (h (S i) x))) #Hcase
  22     [@termb_true_to_term //
  23     |<Hminx in Hcase; #H lapply (fmin_false (λx.termb i x (h (S i) x)) (x-i) (S i) H)
  24      >min_input_def in Hminx; #Hminx >Hminx in ⊢ (%→?);
  25      <plus_n_Sm <plus_minus_m_m [2: @lt_to_le //]
  26      #Habs @False_ind /2/
  27     ]
  28   |@False_ind >min_input_i in Hminx;
  29     [#eqix >eqix in Hix; * /2/ | @le_S_S_to_le @not_le_to_lt //]
  30   ]
  31 qed.
  32
  33 lemma min_input_to_lt: ∀h,i,x.
  34   min_input h i x = x → i < x.
  35 #h #i #x #Hminx cases (decidable_le (S i) x) //
  36 #ltxi @False_ind >min_input_i in Hminx;
  37   [#eqix >eqix in ltxi; * /2/ | @le_S_S_to_le @not_le_to_lt //]
  38 qed.
  39
  40 lemma le_to_min_input: ∀h,i,x,x1. x ≤ x1 →
  41   min_input h i x = x → min_input h i x1 = x.
  42 #h #i #x #x1 #lex #Hminx @(min_exists … (le_S_S … lex))
  43   [@(fmin_true … (sym_eq … Hminx)) //
  44   |@(min_input_to_lt … Hminx)
  45   |#j #H1 <Hminx @lt_min_to_false //
  46   |@plus_minus_m_m @le_S_S @(transitive_le … lex) @lt_to_le
  47    @(min_input_to_lt … Hminx)
  48   ]
  49 qed.
  50
  51 definition g ≝ λh,u,x.
  52   S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
  53
  54 lemma g_def : ∀h,u,x. g h u x =
  55   S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
  56 // qed.
  57
  58 lemma le_u_to_g_1 : ∀h,u,x. x ≤ u → g h u x = 1.
  59 #h #u #x #lexu >g_def cut (x-u = 0) [/2 by minus_le_minus_minus_comm/]
  60 #eq0 >eq0 normalize // qed.
  61
  62 lemma g_lt : ∀h,i,x. min_input h i x = x →
  63   out i x (h (S i) x) < g h 0 x.
  64 #h #i #x #H @le_S_S @(le_MaxI … i) /2 by min_input_to_lt/
  65 qed.
  66
  67 lemma max_neq0 : ∀a,b. max a b ≠ 0 → a ≠ 0 ∨ b ≠ 0.
  68 #a #b whd in match (max a b); cases (true_or_false (leb a b)) #Hcase >Hcase
  69   [#H %2 @H | #H %1 @H]
  70 qed.
  71
  72 definition almost_equal ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
  73 interpretation "almost equal" 'napart f g = (almost_equal f g).
  74
  75 lemma eventually_cancelled: ∀h,u.¬∀nu.∃x. nu < x ∧
  76   max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) ≠ 0.
  77 #h #u elim u
  78   [normalize % #H cases (H u) #x * #_ * #H1 @H1 //
  79   |#u0 @not_to_not #Hind #nu cases (Hind nu) #x * #ltx
  80    cases (true_or_false (eqb (min_input h (u0+O) x) x)) #Hcase
  81     [>bigop_Strue [2:@Hcase] #Hmax cases (max_neq0 … Hmax) -Hmax
  82       [2: #H %{x} % // <minus_n_O @H]
  83      #Hneq0 (* if x is not enough we retry with nu=x *)
  84      cases (Hind x) #x1 * #ltx1
  85      >bigop_Sfalse
  86       [#H %{x1} % [@transitive_lt //| <minus_n_O @H]
  87       |@not_eq_to_eqb_false >(le_to_min_input … (eqb_true_to_eq … Hcase))
  88         [@lt_to_not_eq @ltx1 | @lt_to_le @ltx1]
  89       ]
  90     |>bigop_Sfalse [2:@Hcase] #H %{x} % // <minus_n_O @H
  91     ]
  92   ]
  93 qed.
  94
  95 lemma condition_1: ∀h,u.g h 0 ≈ g h u.
  96 #h #u @(not_to_not … (eventually_cancelled h u))
  97 #H #nu cases (H (max u nu)) #x * #ltx #Hdiff
  98 %{x} % [@(le_to_lt_to_lt … ltx) @(le_maxr … (le_n …))] @(not_to_not … Hdiff)
  99 #H @(eq_f ?? S) >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat  0 MaxA)
 100   [>H // |@lt_to_le @(le_to_lt_to_lt …ltx) /2 by le_maxr/ |//]
 101 qed.
 102
 103 (******************************** Condition 2 *********************************)
 104
 105 lemma exists_to_exists_min: ∀h,i. (∃x. i < x ∧ {i ⊙ x} ↓ h (S i) x) → ∃y. min_input h i y = y.
 106 #h #i * #x * #ltix #Hx %{(min_input h i x)} @min_spec_to_min @found //
 107   [@(f_min_true (λy:ℕ.termb i y (h (S i) y))) %{x} % [% // | @term_to_termb_true //]
 108   |#y #leiy #lty @(lt_min_to_false ????? lty) //
 109   ]
 110 qed.
 111
 112 lemma condition_2: ∀h,i. code_for (total (g h 0)) i → ¬∃x. i<x ∧ {i ⊙ x} ↓ h (S i) x.
 113 #h #i whd in ⊢(%→?); #H % #H1 cases (exists_to_exists_min … H1) #y #Hminy
 114 lapply (g_lt … Hminy)
 115 lapply (min_input_to_terminate … Hminy) * #r #termy
 116 cases (H y) -H #ny #Hy
 117 cut (r = g h 0 y) [@(unique_U … ny … termy) @Hy //] #Hr
 118 whd in match (out ???); >termy >Hr
 119 #H @(absurd ? H) @le_to_not_lt @le_n
 120 qed.
 121
 122 (**************************** complexity of g *********************************)
 123
 124 definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
 125 definition auxg ≝
 126   λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
 127     (out i (snd ux) (h (S i) (snd ux))).
 128
 129 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
 130 #h #s #H1 @(CF_compS ? (auxg h) H1)
 131 qed.
 132
 133 definition aux1g ≝
 134   λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
 135     ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
 136
 137 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
 138 #h #x @same_bigop
 139   [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
 140 qed.
 141
 142 lemma compl_g2 : ∀h,s1,s2,s.
 143   CF s1
 144     (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
 145   CF s2
 146     (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
 147   O s (λx.MSC x + (snd x - fst x)*Max_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
 148   CF s (auxg h).
 149 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
 150   [#n whd in ⊢ (??%%); @eq_aux]
 151 @(CF_max2 … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
 152 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
 153 qed.
 154
 155 lemma compl_g3 : ∀h,s.
 156   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
 157   CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
 158 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (le_to_O … (MSC_in … H)))
 159 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
 160 qed.
 161
 162 definition min_input_aux ≝ λh,p.
 163   μ_{y ∈ [S (fst p),snd (snd p)] }
 164     ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
 165
 166 lemma min_input_eq : ∀h,p.
 167     min_input_aux h p  =
 168     min_input h (fst p) (snd (snd p)).
 169 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
 170 whd in ⊢ (??%%); >fst_pair >snd_pair //
 171 qed.
 172
 173 definition termb_aux ≝ λh.
 174   termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
 175
 176 lemma compl_g4 : ∀h,s1,s. (∀x. 0 < s1 x) →
 177   (CF s1
 178     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
 179    (O s (λx.MSC x + ((snd(snd x) - (fst x)))*Max_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
 180   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
 181 #h #s1 #s #pos_s1 #Hs1 #HO @(ext_CF (min_input_aux h))
 182  [#n whd in ⊢ (??%%); @min_input_eq]
 183 @(CF_mu4 … MSC MSC … pos_s1 … Hs1)
 184   [@CF_compS @CF_fst
 185   |@CF_comp_snd @CF_snd
 186   |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
 187 qed.
 188
 189 (* ??? *)
 190
 191 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
 192 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
 193   (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
 194 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
 195 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
 196 qed.
 197
 198 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
 199 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
 200 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
 201 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
 202 qed.
 203
 204 lemma coroll3: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
 205 O (λx.(snd x - fst x)*s1 〈fst x,x〉)
 206   (λx.(snd x - fst x)*Max_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
 207 #s1 #Hs1 @le_to_O #i @le_times // @Max_le #a #lta #_ @Hs1 //
 208 @lt_minus_to_plus_r //
 209 qed.
 210
 211 (**************************** end of technical lemmas *************************)
 212
 213 lemma compl_g5 : ∀h,s1.
 214   (∀n. 0 < s1 n) →
 215   (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
 216   (CF s1
 217     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
 218   CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
 219     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 220 #h #s1 #Hpos #Hmono #Hs1 @(compl_g4 … Hpos Hs1) @O_plus
 221 [@O_plus_l // |@O_plus_r @le_to_O #n @le_times //
 222 @Max_le #i #lti #_ @Hmono @le_S_S_to_le @lt_minus_to_plus_r @lti
 223 qed.
 224
 225 lemma compl_g6: ∀h.
 226   constructible (λx. h (fst x) (snd x)) →
 227   (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
 228     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
 229 #h #hconstr @(ext_CF (termb_aux h))
 230   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
 231 @(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
 232   [@CF_comp_pair
 233     [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
 234     |@CF_comp_pair
 235       [@(monotonic_CF … CF_fst) #x //
 236       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
 237         [#n normalize >fst_pair >snd_pair %]
 238        @(CF_comp … MSC …hconstr)
 239         [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
 240         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
 241         ]
 242       ]
 243     ]
 244   |@O_plus
 245     [@O_plus
 246       [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
 247         [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
 248          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
 249          >distributive_times_plus @le_plus [//]
 250          cases (surj_pair b) #c * #d #eqb >eqb
 251          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
 252          whd in ⊢ (??%); @le_plus
 253           [@monotonic_MSC @(le_maxl … (le_n …))
 254           |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
 255           ]
 256         |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
 257         ]
 258       |@le_to_O #n @sU_le
 259       ]
 260     |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
 261   ]
 262 qed.
 263
 264 definition big : nat →nat ≝ λx.
 265   let m ≝ max (fst x) (snd x) in 〈m,m〉.
 266
 267 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
 268 #a #b normalize >fst_pair >snd_pair // qed.
 269
 270 lemma le_big : ∀x. x ≤ big x.
 271 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
 272 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
 273 qed.
 274
 275 definition faux2 ≝ λh.
 276   (λx.MSC x + (snd (snd x)-fst x)*
 277     (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
 278
 279 lemma compl_g7: ∀h.
 280   constructible (λx. h (fst x) (snd x)) →
 281   (∀n. monotonic ? le (h n)) →
 282   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))〉〉)
 283     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 284 #h #hcostr #hmono @(monotonic_CF … (faux2 h))
 285   [#n normalize >fst_pair >snd_pair //]
 286 @compl_g5 [#n @sU_pos | 3:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
 287 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
 288 qed.
 289
 290 lemma compl_g71: ∀h.
 291   constructible (λx. h (fst x) (snd x)) →
 292   (∀n. monotonic ? le (h n)) →
 293   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))〉〉)
 294     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 295 #h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x
 296 @le_plus [@monotonic_MSC //]
 297 cases (decidable_le (fst x) (snd(snd x)))
 298   [#Hle @le_times // @monotonic_sU
 299   |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
 300   ]
 301 qed.
 302
 303 definition out_aux ≝ λh.
 304   out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
 305
 306 lemma compl_g8: ∀h.
 307   constructible (λx. h (fst x) (snd x)) →
 308   (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
 309     (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
 310 #h #hconstr @(ext_CF (out_aux h))
 311   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
 312 @(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
 313   [@CF_comp_pair
 314     [@(monotonic_CF … CF_fst) #x //
 315     |@CF_comp_pair
 316       [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
 317       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
 318         [#n normalize >fst_pair >snd_pair %]
 319        @(CF_comp … MSC …hconstr)
 320         [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
 321         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
 322         ]
 323       ]
 324     ]
 325   |@O_plus
 326     [@O_plus
 327       [@le_to_O #n @sU_le
 328       |@(O_trans … (λx.MSC (max (fst x) (snd x))))
 329         [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
 330          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
 331          whd in ⊢ (??%); @le_plus
 332           [@monotonic_MSC @(le_maxl … (le_n …))
 333           |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
 334           ]
 335         |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
 336         ]
 337       ]
 338     |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
 339   ]
 340 qed.
 341
 342 lemma compl_g9 : ∀h.
 343   constructible (λx. h (fst x) (snd x)) →
 344   (∀n. monotonic ? le (h n)) →
 345   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
 346   CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
 347       (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
 348    (auxg h).
 349 #h #hconstr #hmono #hantimono
 350 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
 351 @O_plus
 352   [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
 353     [// | @monotonic_MSC // ]]
 354 @(O_trans … (coroll3 ??))
 355   [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
 356    cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
 357    cut (max a n = n)
 358     [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
 359    cut (max b n = n) [normalize >le_to_leb_true //] #maxb
 360    @le_plus
 361     [@le_plus [>big_def >big_def >maxa >maxb //]
 362      @le_times
 363       [/2 by monotonic_le_minus_r/
 364       |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
 365       ]
 366     |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
 367     ]
 368   |@le_to_O #n >fst_pair >snd_pair
 369    cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
 370    >associative_plus >distributive_times_plus
 371    @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
 372   ]
 373 qed.
 374
 375 definition c ≝ λx.(S (snd x-fst x))*MSC 〈x,x〉.
 376
 377 definition sg ≝ λh,x.
 378   let a ≝ fst x in
 379   let b ≝ snd x in
 380   c x + (b-a)*(S(b-a))*sU 〈x,〈snd x,h (S a) b〉〉.
 381
 382 lemma sg_def1 : ∀h,a,b.
 383   sg h 〈a,b〉 = c 〈a,b〉 +
 384    (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
 385 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
 386 qed.
 387
 388 lemma sg_def : ∀h,a,b.
 389   sg h 〈a,b〉 =
 390    S (b-a)*MSC 〈〈a,b〉,〈a,b〉〉 + (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
 391 #h #a #b normalize >fst_pair >snd_pair //
 392 qed.
 393
 394 lemma compl_g11 : ∀h.
 395   constructible (λx. h (fst x) (snd x)) →
 396   (∀n. monotonic ? le (h n)) →
 397   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
 398   CF (sg h) (unary_g h).
 399 #h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)
 400 qed.
 401
 402 (**************************** closing the argument ****************************)
 403
 404 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
 405   match d with
 406   [ O ⇒ c
 407   | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
 408      d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
 409
 410 lemma h_of_aux_O: ∀r,c,b.
 411   h_of_aux r c O b  = c.
 412 // qed.
 413
 414 lemma h_of_aux_S : ∀r,c,d,b.
 415   h_of_aux r c (S d) b =
 416     (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
 417       (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
 418 // qed.
 419
 420 definition h_of ≝ λr,p.
 421   let m ≝ max (fst p) (snd p) in
 422   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
 423
 424 lemma h_of_O: ∀r,a,b. b ≤ a →
 425   h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
 426 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
 427 qed.
 428
 429 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
 430   let m ≝ max a b in
 431   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
 432 #r #a #b normalize >fst_pair >snd_pair //
 433 qed.
 434
 435 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
 436   ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
 437   h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
 438 #r #Hr #monor #d #d1 lapply d -d elim d1
 439   [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
 440    >h_of_aux_O >h_of_aux_O  //
 441   |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
 442     [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
 443      >h_of_aux_S @(transitive_le ???? (le_plus_n …))
 444      >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
 445      >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
 446     |#Hd >Hd >h_of_aux_S >h_of_aux_S
 447      cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
 448      @le_plus [@le_times //]
 449       [@monotonic_MSC @le_pair @le_pair //
 450       |@le_times [//] @monotonic_sU
 451         [@le_pair // |// |@monor @Hind //]
 452       ]
 453     ]
 454   ]
 455 qed.
 456
 457 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
 458   ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
 459 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
 460 cut (max i a ≤ max i b)
 461   [@to_max
 462     [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
 463 #Hmax @(mono_h_of_aux r Hr Hmono)
 464   [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
 465 qed.
 466
 467 axiom h_of_constr : ∀r:nat →nat.
 468   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 469   constructible (h_of r).
 470
 471 lemma speed_compl: ∀r:nat →nat.
 472   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 473   CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
 474 #r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …))
 475   [#x cases (surj_pair x) #a * #b #eqx >eqx
 476    >sg_def cases (decidable_le b a)
 477     [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
 478      <plus_n_O <plus_n_O >h_of_def
 479      cut (max a b = a)
 480       [normalize cases (le_to_or_lt_eq … leba)
 481         [#ltba >(lt_to_leb_false … ltba) %
 482         |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
 483      #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
 484      @monotonic_MSC @le_pair @le_pair //
 485     |#ltab >h_of_def >h_of_def
 486      cut (max a b = b)
 487       [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
 488      #Hmax >Hmax
 489      cut (max (S a) b = b)
 490       [whd in ⊢ (??%?);  >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
 491      #Hmax1 >Hmax1
 492      cut (∃d.b - a = S d)
 493        [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
 494      * #d #eqd >eqd
 495      cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
 496      cut (b - S d = a)
 497        [@plus_to_minus >commutative_plus @minus_to_plus
 498          [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
 499      normalize //
 500     ]
 501   |#n #a #b #leab #lebn >h_of_def >h_of_def
 502    cut (max a n = n)
 503     [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
 504    cut (max b n = n)
 505     [normalize >(le_to_leb_true … lebn) %] #Hmaxb
 506    >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
 507   |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
 508   |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
 509     [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]
 510    @(h_of_constr r Hr Hmono Hconstr)
 511   ]
 512 qed.
 513
 514 lemma speed_compl_i: ∀r:nat →nat.
 515   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 516   ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
 517 #r #Hr #Hmono #Hconstr #i
 518 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
 519   [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
 520 @smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //
 521 qed.
 522
 523 (**************************** the speedup theorem *****************************)
 524 theorem pseudo_speedup:
 525   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 526   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
 527 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
 528 #r #Hr #Hmono #Hconstr
 529 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
 530 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #i *
 531 #Hcodei #HCi
 532 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
 533 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 534 (* sg is (λx.h_of r 〈i,x〉) *)
 535 %{(λx. h_of r 〈S i,x〉)}
 536 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
 537 %[%[@condition_1 |@Hg]
 538  |cases Hg #H1 * #j * #Hcodej #HCj
 539   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
 540   cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
 541   @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
 542   [@(transitive_le … ltin) @(le_maxl … (le_n …))]
 543   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
 544   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
 545  ]
 546 qed.
 547
 548 theorem pseudo_speedup':
 549   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 550   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
 551   (* ¬ O (r ∘ sg) sf. *)
 552   ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
 553 #r #Hr #Hmono #Hconstr
 554 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
 555 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #i *
 556 #Hcodei #HCi
 557 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
 558 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 559 (* sg is (λx.h_of r 〈S i,x〉) *)
 560 %{(λx. h_of r 〈S i,x〉)}
 561 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
 562 %[%[@condition_1 |@Hg]
 563  |cases Hg #H1 * #j * #Hcodej #HCj
 564   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
 565   cases HCi #m * #a #Ha
 566   %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2
 567   #Hlesf %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
 568   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
 569   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
 570   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
 571  ]
 572 qed.
 573