matita/matita/lib/reverse_complexity/speedup.ma

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