matita/matita/lib/reverse_complexity/speedup.ma

   1 (*
   2 <<<<<<< HEAD:matita/matita/broken_lib/reverse_complexity/toolkit.ma
   3 include "basics/types.ma".
   4 include "arithmetics/minimization.ma".
   5 include "arithmetics/bigops.ma".
   6 include "arithmetics/sigma_pi.ma".
   7 include "arithmetics/bounded_quantifiers.ma".
   8 include "reverse_complexity/big_O.ma".
   9 include "basics/core_notation/napart_2.ma".
  10
  11 (************************* notation for minimization *****************************)
  12 notation "μ_{ ident i < n } p"
  13   with precedence 80 for @{min $n 0 (λ${ident i}.$p)}.
  14
  15 notation "μ_{ ident i ≤ n } p"
  16   with precedence 80 for @{min (S $n) 0 (λ${ident i}.$p)}.
  17
  18 notation "μ_{ ident i ∈ [a,b[ } p"
  19   with precedence 80 for @{min ($b-$a) $a (λ${ident i}.$p)}.
  20
  21 notation "μ_{ ident i ∈ [a,b] } p"
  22   with precedence 80 for @{min (S $b-$a) $a (λ${ident i}.$p)}.
  23
  24 (************************************ MAX *************************************)
  25 notation "Max_{ ident i < n | p } f"
  26   with precedence 80
  27 for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
  28
  29 notation "Max_{ ident i < n } f"
  30   with precedence 80
  31 for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}.
  32
  33 notation "Max_{ ident j ∈ [a,b[ } f"
  34   with precedence 80
  35 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
  36   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  37
  38 notation "Max_{ ident j ∈ [a,b[ | p } f"
  39   with precedence 80
  40 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
  41   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  42
  43 lemma Max_assoc: ∀a,b,c. max (max a b) c = max a (max b c).
  44 #a #b #c normalize cases (true_or_false (leb a b)) #leab >leab normalize
  45   [cases (true_or_false (leb b c )) #lebc >lebc normalize
  46     [>(le_to_leb_true a c) // @(transitive_le ? b) @leb_true_to_le //
  47     |>leab //
  48     ]
  49   |cases (true_or_false (leb b c )) #lebc >lebc normalize //
  50    >leab normalize >(not_le_to_leb_false a c) // @lt_to_not_le
  51    @(transitive_lt ? b) @not_le_to_lt @leb_false_to_not_le //
  52   ]
  53 qed.
  54
  55 lemma Max0 : ∀n. max 0 n = n.
  56 // qed.
  57
  58 lemma Max0r : ∀n. max n 0 = n.
  59 #n >commutative_max //
  60 qed.
  61
  62 definition MaxA ≝
  63   mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)).
  64
  65 definition MaxAC ≝ mk_ACop nat 0 MaxA commutative_max.
  66
  67 lemma le_Max: ∀f,p,n,a. a < n → p a = true →
  68   f a ≤  Max_{i < n | p i}(f i).
  69 #f #p #n #a #ltan #pa
  70 >(bigop_diff p ? 0 MaxAC f a n) // @(le_maxl … (le_n ?))
  71 qed.
  72
  73 lemma le_MaxI: ∀f,p,n,m,a. m ≤ a → a < n → p a = true →
  74   f a ≤  Max_{i ∈ [m,n[ | p i}(f i).
  75 #f #p #n #m #a #lema #ltan #pa
  76 >(bigop_diff ? ? 0 MaxAC (λi.f (i+m)) (a-m) (n-m))
  77   [<plus_minus_m_m // @(le_maxl … (le_n ?))
  78   |<plus_minus_m_m //
  79   |/2 by monotonic_lt_minus_l/
  80   ]
  81 qed.
  82
  83 lemma Max_le: ∀f,p,n,b.
  84   (∀a.a < n → p a = true → f a ≤ b) → Max_{i < n | p i}(f i) ≤ b.
  85 #f #p #n elim n #b #H //
  86 #b0 #H1 cases (true_or_false (p b)) #Hb
  87   [>bigop_Strue [2:@Hb] @to_max [@H1 // | @H #a #ltab #pa @H1 // @le_S //]
  88   |>bigop_Sfalse [2:@Hb] @H #a #ltab #pa @H1 // @le_S //
  89   ]
  90 qed.
  91
  92 (********************************** pairing ***********************************)
  93 axiom pair: nat → nat → nat.
  94 axiom fst : nat → nat.
  95 axiom snd : nat → nat.
  96
  97 interpretation "abstract pair" 'pair f g = (pair f g).
  98
  99 axiom fst_pair: ∀a,b. fst 〈a,b〉 = a.
 100 axiom snd_pair: ∀a,b. snd 〈a,b〉 = b.
 101 axiom surj_pair: ∀x. ∃a,b. x = 〈a,b〉.
 102
 103 axiom le_fst : ∀p. fst p ≤ p.
 104 axiom le_snd : ∀p. snd p ≤ p.
 105 axiom le_pair: ∀a,a1,b,b1. a ≤ a1 → b ≤ b1 → 〈a,b〉 ≤ 〈a1,b1〉.
 106
 107 (************************************* U **************************************)
 108 axiom U: nat → nat →nat → option nat.
 109
 110 axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
 111   U i x n = Some ? y → U i x m = Some ? y.
 112
 113 lemma unique_U: ∀i,x,n,m,yn,ym.
 114   U i x n = Some ? yn → U i x m = Some ? ym → yn = ym.
 115 #i #x #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
 116   [#lenm lapply (monotonic_U … lenm Hn) >Hm #HS destruct (HS) //
 117   |#ltmn lapply (monotonic_U … n … Hm) [@lt_to_le @not_le_to_lt //]
 118    >Hn #HS destruct (HS) //
 119   ]
 120 qed.
 121
 122 definition code_for ≝ λf,i.∀x.
 123   ∃n.∀m. n ≤ m → U i x m = f x.
 124
 125 definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y.
 126
 127 notation "{i ⊙ x} ↓ r" with precedence 60 for @{terminate $i $x $r}.
 128
 129 lemma terminate_dec: ∀i,x,n. {i ⊙ x} ↓ n ∨ ¬ {i ⊙ x} ↓ n.
 130 #i #x #n normalize cases (U i x n)
 131   [%2 % * #y #H destruct|#y %1 %{y} //]
 132 qed.
 133
 134 lemma monotonic_terminate: ∀i,x,n,m.
 135   n ≤ m → {i ⊙ x} ↓ n → {i ⊙ x} ↓ m.
 136 #i #x #n #m #lenm * #z #H %{z} @(monotonic_U … H) //
 137 qed.
 138
 139 definition termb ≝ λi,x,t.
 140   match U i x t with [None ⇒ false |Some y ⇒ true].
 141
 142 lemma termb_true_to_term: ∀i,x,t. termb i x t = true → {i ⊙ x} ↓ t.
 143 #i #x #t normalize cases (U i x t) normalize [#H destruct | #y #_ %{y} //]
 144 qed.
 145
 146 lemma term_to_termb_true: ∀i,x,t. {i ⊙ x} ↓ t → termb i x t = true.
 147 #i #x #t * #y #H normalize >H //
 148 qed.
 149
 150 definition out ≝ λi,x,r.
 151   match U i x r with [ None ⇒ 0 | Some z ⇒ z].
 152
 153 definition bool_to_nat: bool → nat ≝
 154   λb. match b with [true ⇒ 1 | false ⇒ 0].
 155
 156 coercion bool_to_nat.
 157
 158 definition pU : nat → nat → nat → nat ≝ λi,x,r.〈termb i x r,out i x r〉.
 159
 160 lemma pU_vs_U_Some : ∀i,x,r,y. pU i x r = 〈1,y〉 ↔ U i x r = Some ? y.
 161 #i #x #r #y % normalize
 162   [cases (U i x r) normalize
 163     [#H cut (0=1) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H @H]
 164      #H1 destruct
 165     |#a #H cut (a=y) [lapply (eq_f … snd … H) >snd_pair >snd_pair #H1 @H1]
 166      #H1 //
 167     ]
 168   |#H >H //]
 169 qed.
 170
 171 lemma pU_vs_U_None : ∀i,x,r. pU i x r = 〈0,0〉 ↔ U i x r = None ?.
 172 #i #x #r % normalize
 173   [cases (U i x r) normalize //
 174    #a #H cut (1=0) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H1 @H1]
 175    #H1 destruct
 176   |#H >H //]
 177 qed.
 178
 179 lemma fst_pU: ∀i,x,r. fst (pU i x r) = termb i x r.
 180 #i #x #r normalize cases (U i x r) normalize >fst_pair //
 181 qed.
 182
 183 lemma snd_pU: ∀i,x,r. snd (pU i x r) = out i x r.
 184 #i #x #r normalize cases (U i x r) normalize >snd_pair //
 185 qed.
 186 =======
 187 include "reverse_complexity/bigops_compl.ma".
 188 >>>>>>> reverse_complexity lib restored:matita/matita/lib/reverse_complexity/speedup.ma
 189 *)
 190
 191 (********************************* the speedup ********************************)
 192
 193 definition min_input ≝ λh,i,x. μ_{y ∈ [S i,x] } (termb i y (h (S i) y)).
 194
 195 lemma min_input_def : ∀h,i,x.
 196   min_input h i x = min (x -i) (S i) (λy.termb i y (h (S i) y)).
 197 // qed.
 198
 199 lemma min_input_i: ∀h,i,x. x ≤ i → min_input h i x = S i.
 200 #h #i #x #lexi >min_input_def
 201 cut (x - i = 0) [@sym_eq /2 by eq_minus_O/] #Hcut //
 202 qed.
 203
 204 lemma min_input_to_terminate: ∀h,i,x.
 205   min_input h i x = x → {i ⊙ x} ↓ (h (S i) x).
 206 #h #i #x #Hminx
 207 cases (decidable_le (S i) x) #Hix
 208   [cases (true_or_false (termb i x (h (S i) x))) #Hcase
 209     [@termb_true_to_term //
 210     |<Hminx in Hcase; #H lapply (fmin_false (λx.termb i x (h (S i) x)) (x-i) (S i) H)
 211      >min_input_def in Hminx; #Hminx >Hminx in ⊢ (%→?);
 212      <plus_n_Sm <plus_minus_m_m [2: @lt_to_le //]
 213      #Habs @False_ind /2/
 214     ]
 215   |@False_ind >min_input_i in Hminx;
 216     [#eqix >eqix in Hix; * /2/ | @le_S_S_to_le @not_le_to_lt //]
 217   ]
 218 qed.
 219
 220 lemma min_input_to_lt: ∀h,i,x.
 221   min_input h i x = x → i < x.
 222 #h #i #x #Hminx cases (decidable_le (S i) x) //
 223 #ltxi @False_ind >min_input_i in Hminx;
 224   [#eqix >eqix in ltxi; * /2/ | @le_S_S_to_le @not_le_to_lt //]
 225 qed.
 226
 227 lemma le_to_min_input: ∀h,i,x,x1. x ≤ x1 →
 228   min_input h i x = x → min_input h i x1 = x.
 229 #h #i #x #x1 #lex #Hminx @(min_exists … (le_S_S … lex))
 230   [@(fmin_true … (sym_eq … Hminx)) //
 231   |@(min_input_to_lt … Hminx)
 232   |#j #H1 <Hminx @lt_min_to_false //
 233   |@plus_minus_m_m @le_S_S @(transitive_le … lex) @lt_to_le
 234    @(min_input_to_lt … Hminx)
 235   ]
 236 qed.
 237
 238 definition g ≝ λh,u,x.
 239   S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
 240
 241 lemma g_def : ∀h,u,x. g h u x =
 242   S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
 243 // qed.
 244
 245 lemma le_u_to_g_1 : ∀h,u,x. x ≤ u → g h u x = 1.
 246 #h #u #x #lexu >g_def cut (x-u = 0) [/2 by minus_le_minus_minus_comm/]
 247 #eq0 >eq0 normalize // qed.
 248
 249 lemma g_lt : ∀h,i,x. min_input h i x = x →
 250   out i x (h (S i) x) < g h 0 x.
 251 #h #i #x #H @le_S_S @(le_MaxI … i) /2 by min_input_to_lt/
 252 qed.
 253
 254 lemma max_neq0 : ∀a,b. max a b ≠ 0 → a ≠ 0 ∨ b ≠ 0.
 255 #a #b whd in match (max a b); cases (true_or_false (leb a b)) #Hcase >Hcase
 256   [#H %2 @H | #H %1 @H]
 257 qed.
 258
 259 definition almost_equal ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
 260 interpretation "almost equal" 'napart f g = (almost_equal f g).
 261
 262 lemma eventually_cancelled: ∀h,u.¬∀nu.∃x. nu < x ∧
 263   max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) ≠ 0.
 264 #h #u elim u
 265   [normalize % #H cases (H u) #x * #_ * #H1 @H1 //
 266   |#u0 @not_to_not #Hind #nu cases (Hind nu) #x * #ltx
 267    cases (true_or_false (eqb (min_input h (u0+O) x) x)) #Hcase
 268     [>bigop_Strue [2:@Hcase] #Hmax cases (max_neq0 … Hmax) -Hmax
 269       [2: #H %{x} % // <minus_n_O @H]
 270      #Hneq0 (* if x is not enough we retry with nu=x *)
 271      cases (Hind x) #x1 * #ltx1
 272      >bigop_Sfalse
 273       [#H %{x1} % [@transitive_lt //| <minus_n_O @H]
 274       |@not_eq_to_eqb_false >(le_to_min_input … (eqb_true_to_eq … Hcase))
 275         [@lt_to_not_eq @ltx1 | @lt_to_le @ltx1]
 276       ]
 277     |>bigop_Sfalse [2:@Hcase] #H %{x} % // <minus_n_O @H
 278     ]
 279   ]
 280 qed.
 281
 282 lemma condition_1: ∀h,u.g h 0 ≈ g h u.
 283 #h #u @(not_to_not … (eventually_cancelled h u))
 284 #H #nu cases (H (max u nu)) #x * #ltx #Hdiff
 285 %{x} % [@(le_to_lt_to_lt … ltx) @(le_maxr … (le_n …))] @(not_to_not … Hdiff)
 286 #H @(eq_f ?? S) >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat  0 MaxA)
 287   [>H // |@lt_to_le @(le_to_lt_to_lt …ltx) /2 by le_maxr/ |//]
 288 qed.
 289
 290 (******************************** Condition 2 *********************************)
 291
 292 lemma exists_to_exists_min: ∀h,i. (∃x. i < x ∧ {i ⊙ x} ↓ h (S i) x) → ∃y. min_input h i y = y.
 293 #h #i * #x * #ltix #Hx %{(min_input h i x)} @min_spec_to_min @found //
 294   [@(f_min_true (λy:ℕ.termb i y (h (S i) y))) %{x} % [% // | @term_to_termb_true //]
 295   |#y #leiy #lty @(lt_min_to_false ????? lty) //
 296   ]
 297 qed.
 298
 299 lemma condition_2: ∀h,i. code_for (total (g h 0)) i → ¬∃x. i<x ∧ {i ⊙ x} ↓ h (S i) x.
 300 #h #i whd in ⊢(%→?); #H % #H1 cases (exists_to_exists_min … H1) #y #Hminy
 301 lapply (g_lt … Hminy)
 302 lapply (min_input_to_terminate … Hminy) * #r #termy
 303 cases (H y) -H #ny #Hy
 304 cut (r = g h 0 y) [@(unique_U … ny … termy) @Hy //] #Hr
 305 whd in match (out ???); >termy >Hr
 306 #H @(absurd ? H) @le_to_not_lt @le_n
 307 qed.
 308
 309 (**************************** complexity of g *********************************)
 310
 311 definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
 312 definition auxg ≝
 313   λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
 314     (out i (snd ux) (h (S i) (snd ux))).
 315
 316 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
 317 #h #s #H1 @(CF_compS ? (auxg h) H1)
 318 qed.
 319
 320 definition aux1g ≝
 321   λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
 322     ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
 323
 324 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
 325 #h #x @same_bigop
 326   [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
 327 qed.
 328
 329 lemma compl_g2 : ∀h,s1,s2,s.
 330   CF s1
 331     (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
 332   CF s2
 333     (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
 334   O s (λx.MSC x + (snd x - fst x)*Max_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
 335   CF s (auxg h).
 336 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
 337   [#n whd in ⊢ (??%%); @eq_aux]
 338 @(CF_max2 … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
 339 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
 340 qed.
 341
 342 lemma compl_g3 : ∀h,s.
 343   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
 344   CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
 345 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (le_to_O … (MSC_in … H)))
 346 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
 347 qed.
 348
 349 definition min_input_aux ≝ λh,p.
 350   μ_{y ∈ [S (fst p),snd (snd p)] }
 351     ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
 352
 353 lemma min_input_eq : ∀h,p.
 354     min_input_aux h p  =
 355     min_input h (fst p) (snd (snd p)).
 356 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
 357 whd in ⊢ (??%%); >fst_pair >snd_pair //
 358 qed.
 359
 360 definition termb_aux ≝ λh.
 361   termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
 362
 363 lemma compl_g4 : ∀h,s1,s. (∀x. 0 < s1 x) →
 364   (CF s1
 365     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
 366    (O s (λx.MSC x + ((snd(snd x) - (fst x)))*Max_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
 367   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
 368 #h #s1 #s #pos_s1 #Hs1 #HO @(ext_CF (min_input_aux h))
 369  [#n whd in ⊢ (??%%); @min_input_eq]
 370 @(CF_mu4 … MSC MSC … pos_s1 … Hs1)
 371   [@CF_compS @CF_fst
 372   |@CF_comp_snd @CF_snd
 373   |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
 374 qed.
 375
 376 (* ??? *)
 377
 378 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
 379 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
 380   (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
 381 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
 382 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
 383 qed.
 384
 385 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
 386 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
 387 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
 388 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
 389 qed.
 390
 391 lemma coroll3: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
 392 O (λx.(snd x - fst x)*s1 〈fst x,x〉)
 393   (λx.(snd x - fst x)*Max_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
 394 #s1 #Hs1 @le_to_O #i @le_times // @Max_le #a #lta #_ @Hs1 //
 395 @lt_minus_to_plus_r //
 396 qed.
 397
 398 (**************************** end of technical lemmas *************************)
 399
 400 lemma compl_g5 : ∀h,s1.
 401   (∀n. 0 < s1 n) →
 402   (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
 403   (CF s1
 404     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
 405   CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
 406     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 407 #h #s1 #Hpos #Hmono #Hs1 @(compl_g4 … Hpos Hs1) @O_plus
 408 [@O_plus_l // |@O_plus_r @le_to_O #n @le_times //
 409 @Max_le #i #lti #_ @Hmono @le_S_S_to_le @lt_minus_to_plus_r @lti
 410 qed.
 411
 412 lemma compl_g6: ∀h.
 413   constructible (λx. h (fst x) (snd x)) →
 414   (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
 415     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
 416 #h #hconstr @(ext_CF (termb_aux h))
 417   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
 418 @(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
 419   [@CF_comp_pair
 420     [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
 421     |@CF_comp_pair
 422       [@(monotonic_CF … CF_fst) #x //
 423       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
 424         [#n normalize >fst_pair >snd_pair %]
 425        @(CF_comp … MSC …hconstr)
 426         [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
 427         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
 428         ]
 429       ]
 430     ]
 431   |@O_plus
 432     [@O_plus
 433       [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
 434         [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
 435          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
 436          >distributive_times_plus @le_plus [//]
 437          cases (surj_pair b) #c * #d #eqb >eqb
 438          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
 439          whd in ⊢ (??%); @le_plus
 440           [@monotonic_MSC @(le_maxl … (le_n …))
 441           |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
 442           ]
 443         |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
 444         ]
 445       |@le_to_O #n @sU_le
 446       ]
 447     |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
 448   ]
 449 qed.
 450
 451 definition big : nat →nat ≝ λx.
 452   let m ≝ max (fst x) (snd x) in 〈m,m〉.
 453
 454 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
 455 #a #b normalize >fst_pair >snd_pair // qed.
 456
 457 lemma le_big : ∀x. x ≤ big x.
 458 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
 459 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
 460 qed.
 461
 462 definition faux2 ≝ λh.
 463   (λx.MSC x + (snd (snd x)-fst x)*
 464     (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
 465
 466 lemma compl_g7: ∀h.
 467   constructible (λx. h (fst x) (snd x)) →
 468   (∀n. monotonic ? le (h n)) →
 469   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))〉〉)
 470     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 471 #h #hcostr #hmono @(monotonic_CF … (faux2 h))
 472   [#n normalize >fst_pair >snd_pair //]
 473 @compl_g5 [#n @sU_pos | 3:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
 474 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
 475 qed.
 476
 477 lemma compl_g71: ∀h.
 478   constructible (λx. h (fst x) (snd x)) →
 479   (∀n. monotonic ? le (h n)) →
 480   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))〉〉)
 481     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 482 #h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x
 483 @le_plus [@monotonic_MSC //]
 484 cases (decidable_le (fst x) (snd(snd x)))
 485   [#Hle @le_times // @monotonic_sU
 486   |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
 487   ]
 488 qed.
 489
 490 definition out_aux ≝ λh.
 491   out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
 492
 493 lemma compl_g8: ∀h.
 494   constructible (λx. h (fst x) (snd x)) →
 495   (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
 496     (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
 497 #h #hconstr @(ext_CF (out_aux h))
 498   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
 499 @(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
 500   [@CF_comp_pair
 501     [@(monotonic_CF … CF_fst) #x //
 502     |@CF_comp_pair
 503       [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
 504       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
 505         [#n normalize >fst_pair >snd_pair %]
 506        @(CF_comp … MSC …hconstr)
 507         [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
 508         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
 509         ]
 510       ]
 511     ]
 512   |@O_plus
 513     [@O_plus
 514       [@le_to_O #n @sU_le
 515       |@(O_trans … (λx.MSC (max (fst x) (snd x))))
 516         [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
 517          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
 518          whd in ⊢ (??%); @le_plus
 519           [@monotonic_MSC @(le_maxl … (le_n …))
 520           |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
 521           ]
 522         |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
 523         ]
 524       ]
 525     |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
 526   ]
 527 qed.
 528
 529 lemma compl_g9 : ∀h.
 530   constructible (λx. h (fst x) (snd x)) →
 531   (∀n. monotonic ? le (h n)) →
 532   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
 533   CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
 534       (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
 535    (auxg h).
 536 #h #hconstr #hmono #hantimono
 537 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
 538 @O_plus
 539   [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
 540     [// | @monotonic_MSC // ]]
 541 @(O_trans … (coroll3 ??))
 542   [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
 543    cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
 544    cut (max a n = n)
 545     [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
 546    cut (max b n = n) [normalize >le_to_leb_true //] #maxb
 547    @le_plus
 548     [@le_plus [>big_def >big_def >maxa >maxb //]
 549      @le_times
 550       [/2 by monotonic_le_minus_r/
 551       |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
 552       ]
 553     |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
 554     ]
 555   |@le_to_O #n >fst_pair >snd_pair
 556    cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
 557    >associative_plus >distributive_times_plus
 558    @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
 559   ]
 560 qed.
 561
 562 definition c ≝ λx.(S (snd x-fst x))*MSC 〈x,x〉.
 563
 564 definition sg ≝ λh,x.
 565   let a ≝ fst x in
 566   let b ≝ snd x in
 567   c x + (b-a)*(S(b-a))*sU 〈x,〈snd x,h (S a) b〉〉.
 568
 569 lemma sg_def1 : ∀h,a,b.
 570   sg h 〈a,b〉 = c 〈a,b〉 +
 571    (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
 572 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
 573 qed.
 574
 575 lemma sg_def : ∀h,a,b.
 576   sg h 〈a,b〉 =
 577    S (b-a)*MSC 〈〈a,b〉,〈a,b〉〉 + (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
 578 #h #a #b normalize >fst_pair >snd_pair //
 579 qed.
 580
 581 lemma compl_g11 : ∀h.
 582   constructible (λx. h (fst x) (snd x)) →
 583   (∀n. monotonic ? le (h n)) →
 584   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
 585   CF (sg h) (unary_g h).
 586 #h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)
 587 qed.
 588
 589 (**************************** closing the argument ****************************)
 590
 591 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
 592   match d with
 593   [ O ⇒ c
 594   | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
 595      d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
 596
 597 lemma h_of_aux_O: ∀r,c,b.
 598   h_of_aux r c O b  = c.
 599 // qed.
 600
 601 lemma h_of_aux_S : ∀r,c,d,b.
 602   h_of_aux r c (S d) b =
 603     (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
 604       (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
 605 // qed.
 606
 607 definition h_of ≝ λr,p.
 608   let m ≝ max (fst p) (snd p) in
 609   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
 610
 611 lemma h_of_O: ∀r,a,b. b ≤ a →
 612   h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
 613 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
 614 qed.
 615
 616 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
 617   let m ≝ max a b in
 618   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
 619 #r #a #b normalize >fst_pair >snd_pair //
 620 qed.
 621
 622 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
 623   ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
 624   h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
 625 #r #Hr #monor #d #d1 lapply d -d elim d1
 626   [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
 627    >h_of_aux_O >h_of_aux_O  //
 628   |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
 629     [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
 630      >h_of_aux_S @(transitive_le ???? (le_plus_n …))
 631      >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
 632      >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
 633     |#Hd >Hd >h_of_aux_S >h_of_aux_S
 634      cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
 635      @le_plus [@le_times //]
 636       [@monotonic_MSC @le_pair @le_pair //
 637       |@le_times [//] @monotonic_sU
 638         [@le_pair // |// |@monor @Hind //]
 639       ]
 640     ]
 641   ]
 642 qed.
 643
 644 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
 645   ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
 646 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
 647 cut (max i a ≤ max i b)
 648   [@to_max
 649     [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
 650 #Hmax @(mono_h_of_aux r Hr Hmono)
 651   [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
 652 qed.
 653
 654 axiom h_of_constr : ∀r:nat →nat.
 655   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 656   constructible (h_of r).
 657
 658 lemma speed_compl: ∀r:nat →nat.
 659   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 660   CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
 661 #r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …))
 662   [#x cases (surj_pair x) #a * #b #eqx >eqx
 663    >sg_def cases (decidable_le b a)
 664     [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
 665      <plus_n_O <plus_n_O >h_of_def
 666      cut (max a b = a)
 667       [normalize cases (le_to_or_lt_eq … leba)
 668         [#ltba >(lt_to_leb_false … ltba) %
 669         |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
 670      #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
 671      @monotonic_MSC @le_pair @le_pair //
 672     |#ltab >h_of_def >h_of_def
 673      cut (max a b = b)
 674       [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
 675      #Hmax >Hmax
 676      cut (max (S a) b = b)
 677       [whd in ⊢ (??%?);  >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
 678      #Hmax1 >Hmax1
 679      cut (∃d.b - a = S d)
 680        [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
 681      * #d #eqd >eqd
 682      cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
 683      cut (b - S d = a)
 684        [@plus_to_minus >commutative_plus @minus_to_plus
 685          [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
 686      normalize //
 687     ]
 688   |#n #a #b #leab #lebn >h_of_def >h_of_def
 689    cut (max a n = n)
 690     [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
 691    cut (max b n = n)
 692     [normalize >(le_to_leb_true … lebn) %] #Hmaxb
 693    >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
 694   |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
 695   |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
 696     [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]
 697    @(h_of_constr r Hr Hmono Hconstr)
 698   ]
 699 qed.
 700
 701 lemma speed_compl_i: ∀r:nat →nat.
 702   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 703   ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
 704 #r #Hr #Hmono #Hconstr #i
 705 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
 706   [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
 707 @smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //
 708 qed.
 709
 710 (**************************** the speedup theorem *****************************)
 711 theorem pseudo_speedup:
 712   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 713   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
 714 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
 715 #r #Hr #Hmono #Hconstr
 716 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
 717 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #i *
 718 #Hcodei #HCi
 719 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
 720 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 721 (* sg is (λx.h_of r 〈i,x〉) *)
 722 %{(λx. h_of r 〈S i,x〉)}
 723 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
 724 %[%[@condition_1 |@Hg]
 725  |cases Hg #H1 * #j * #Hcodej #HCj
 726   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
 727   cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
 728   @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
 729   [@(transitive_le … ltin) @(le_maxl … (le_n …))]
 730   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
 731   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
 732  ]
 733 qed.
 734
 735 theorem pseudo_speedup':
 736   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
 737   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
 738   (* ¬ O (r ∘ sg) sf. *)
 739   ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
 740 #r #Hr #Hmono #Hconstr
 741 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
 742 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #i *
 743 #Hcodei #HCi
 744 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
 745 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 746 (* sg is (λx.h_of r 〈S i,x〉) *)
 747 %{(λx. h_of r 〈S i,x〉)}
 748 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
 749 %[%[@condition_1 |@Hg]
 750  |cases Hg #H1 * #j * #Hcodej #HCj
 751   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
 752   cases HCi #m * #a #Ha
 753   %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2
 754   #Hlesf %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
 755   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
 756   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
 757   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
 758  ]
 759 qed.
 760