matita/matita/lib/reverse_complexity/speed_clean.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 (********************************* the speedup ********************************)
 177
 178 definition min_input ≝ λh,i,x. μ_{y ∈ [S i,x] } (termb i y (h (S i) y)).
 179
 180 lemma min_input_def : ∀h,i,x.
 181   min_input h i x = min (x -i) (S i) (λy.termb i y (h (S i) y)).
 182 // qed.
 183
 184 lemma min_input_i: ∀h,i,x. x ≤ i → min_input h i x = S i.
 185 #h #i #x #lexi >min_input_def
 186 cut (x - i = 0) [@sym_eq /2 by eq_minus_O/] #Hcut //
 187 qed.
 188
 189 lemma min_input_to_terminate: ∀h,i,x.
 190   min_input h i x = x → {i ⊙ x} ↓ (h (S i) x).
 191 #h #i #x #Hminx
 192 cases (decidable_le (S i) x) #Hix
 193   [cases (true_or_false (termb i x (h (S i) x))) #Hcase
 194     [@termb_true_to_term //
 195     |<Hminx in Hcase; #H lapply (fmin_false (λx.termb i x (h (S i) x)) (x-i) (S i) H)
 196      >min_input_def in Hminx; #Hminx >Hminx in ⊢ (%→?);
 197      <plus_n_Sm <plus_minus_m_m [2: @lt_to_le //]
 198      #Habs @False_ind /2/
 199     ]
 200   |@False_ind >min_input_i in Hminx;
 201     [#eqix >eqix in Hix; * /2/ | @le_S_S_to_le @not_le_to_lt //]
 202   ]
 203 qed.
 204
 205 lemma min_input_to_lt: ∀h,i,x.
 206   min_input h i x = x → i < x.
 207 #h #i #x #Hminx cases (decidable_le (S i) x) //
 208 #ltxi @False_ind >min_input_i in Hminx;
 209   [#eqix >eqix in ltxi; * /2/ | @le_S_S_to_le @not_le_to_lt //]
 210 qed.
 211
 212 lemma le_to_min_input: ∀h,i,x,x1. x ≤ x1 →
 213   min_input h i x = x → min_input h i x1 = x.
 214 #h #i #x #x1 #lex #Hminx @(min_exists … (le_S_S … lex))
 215   [@(fmin_true … (sym_eq … Hminx)) //
 216   |@(min_input_to_lt … Hminx)
 217   |#j #H1 <Hminx @lt_min_to_false //
 218   |@plus_minus_m_m @le_S_S @(transitive_le … lex) @lt_to_le
 219    @(min_input_to_lt … Hminx)
 220   ]
 221 qed.
 222
 223 definition g ≝ λh,u,x.
 224   S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
 225
 226 lemma g_def : ∀h,u,x. g h u x =
 227   S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
 228 // qed.
 229
 230 lemma le_u_to_g_1 : ∀h,u,x. x ≤ u → g h u x = 1.
 231 #h #u #x #lexu >g_def cut (x-u = 0) [/2 by minus_le_minus_minus_comm/]
 232 #eq0 >eq0 normalize // qed.
 233
 234 lemma g_lt : ∀h,i,x. min_input h i x = x →
 235   out i x (h (S i) x) < g h 0 x.
 236 #h #i #x #H @le_S_S @(le_MaxI … i) /2 by min_input_to_lt/
 237 qed.
 238
 239 (*
 240 axiom ax1: ∀h,i.
 241    (∃y.i < y ∧ (termb i y (h (S i) y)=true)) ∨
 242     ∀y. i < y → (termb i y (h (S i) y)=false).
 243
 244 lemma eventually_0: ∀h,u.∃nu.∀x. nu < x →
 245   max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) = 0.
 246 #h #u elim u
 247   [%{0} normalize //
 248   |#u0 * #nu0 #Hind cases (ax1 h u0)
 249     [* #x0 * #leu0x0 #Hx0 %{(max nu0 x0)}
 250      #x #Hx >bigop_Sfalse
 251       [>(minus_n_O u0) @Hind @(le_to_lt_to_lt … Hx) /2 by le_maxl/
 252       |@not_eq_to_eqb_false % #Hf @(absurd (x ≤ x0))
 253         [<Hf @true_to_le_min //
 254         |@lt_to_not_le @(le_to_lt_to_lt … Hx) /2 by le_maxl/
 255         ]
 256       ]
 257     |#H %{(max u0 nu0)} #x #Hx >bigop_Sfalse
 258       [>(minus_n_O u0) @Hind @(le_to_lt_to_lt … Hx) @le_maxr //
 259       |@not_eq_to_eqb_false >min_input_def
 260        >(min_not_exists (λy.(termb (u0+0) y (h (S (u0+0)) y))))
 261         [<plus_n_O <plus_n_Sm <plus_minus_m_m
 262           [% #H1 /2/
 263           |@lt_to_le @(le_to_lt_to_lt … Hx) @le_maxl //
 264           ]
 265         |/2 by /
 266         ]
 267       ]
 268     ]
 269   ]
 270 qed.
 271
 272 definition almost_equal ≝ λf,g:nat → nat. ∃nu.∀x. nu < x → f x = g x.
 273
 274 definition almost_equal1 ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
 275
 276 interpretation "almost equal" 'napart f g = (almost_equal f g).
 277
 278 lemma condition_1: ∀h,u.g h 0 ≈ g h u.
 279 #h #u cases (eventually_0 h u) #nu #H %{(max u nu)} #x #Hx @(eq_f ?? S)
 280 >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat  0 MaxA)
 281   [>H // @(le_to_lt_to_lt …Hx) /2 by le_maxl/
 282   |@lt_to_le @(le_to_lt_to_lt …Hx) /2 by le_maxr/
 283   |//
 284   ]
 285 qed. *)
 286
 287 lemma max_neq0 : ∀a,b. max a b ≠ 0 → a ≠ 0 ∨ b ≠ 0.
 288 #a #b whd in match (max a b); cases (true_or_false (leb a b)) #Hcase >Hcase
 289   [#H %2 @H | #H %1 @H]
 290 qed.
 291
 292 definition almost_equal ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
 293 interpretation "almost equal" 'napart f g = (almost_equal f g).
 294
 295 lemma eventually_cancelled: ∀h,u.¬∀nu.∃x. nu < x ∧
 296   max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) ≠ 0.
 297 #h #u elim u
 298   [normalize % #H cases (H u) #x * #_ * #H1 @H1 //
 299   |#u0 @not_to_not #Hind #nu cases (Hind nu) #x * #ltx
 300    cases (true_or_false (eqb (min_input h (u0+O) x) x)) #Hcase
 301     [>bigop_Strue [2:@Hcase] #Hmax cases (max_neq0 … Hmax) -Hmax
 302       [2: #H %{x} % // <minus_n_O @H]
 303      #Hneq0 (* if x is not enough we retry with nu=x *)
 304      cases (Hind x) #x1 * #ltx1
 305      >bigop_Sfalse
 306       [#H %{x1} % [@transitive_lt //| <minus_n_O @H]
 307       |@not_eq_to_eqb_false >(le_to_min_input … (eqb_true_to_eq … Hcase))
 308         [@lt_to_not_eq @ltx1 | @lt_to_le @ltx1]
 309       ]
 310     |>bigop_Sfalse [2:@Hcase] #H %{x} % // <minus_n_O @H
 311     ]
 312   ]
 313 qed.
 314
 315
 316 lemma condition_1_weak: ∀h,u.g h 0 ≈ g h u.
 317 #h #u @(not_to_not … (eventually_cancelled h u))
 318 #H #nu cases (H (max u nu)) #x * #ltx #Hdiff
 319 %{x} % [@(le_to_lt_to_lt … ltx) @(le_maxr … (le_n …))] @(not_to_not … Hdiff)
 320 #H @(eq_f ?? S) >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat  0 MaxA)
 321   [>H // |@lt_to_le @(le_to_lt_to_lt …ltx) /2 by le_maxr/ |//]
 322 qed.
 323
 324 (******************************** Condition 2 *********************************)
 325 definition total ≝ λf.λx:nat. Some nat (f x).
 326
 327 lemma exists_to_exists_min: ∀h,i. (∃x. i < x ∧ {i ⊙ x} ↓ h (S i) x) → ∃y. min_input h i y = y.
 328 #h #i * #x * #ltix #Hx %{(min_input h i x)} @min_spec_to_min @found //
 329   [@(f_min_true (λy:ℕ.termb i y (h (S i) y))) %{x} % [% // | @term_to_termb_true //]
 330   |#y #leiy #lty @(lt_min_to_false ????? lty) //
 331   ]
 332 qed.
 333
 334 lemma condition_2: ∀h,i. code_for (total (g h 0)) i → ¬∃x. i<x ∧ {i ⊙ x} ↓ h (S i) x.
 335 #h #i whd in ⊢(%→?); #H % #H1 cases (exists_to_exists_min … H1) #y #Hminy
 336 lapply (g_lt … Hminy)
 337 lapply (min_input_to_terminate … Hminy) * #r #termy
 338 cases (H y) -H #ny #Hy
 339 cut (r = g h 0 y) [@(unique_U … ny … termy) @Hy //] #Hr
 340 whd in match (out ???); >termy >Hr
 341 #H @(absurd ? H) @le_to_not_lt @le_n
 342 qed.
 343
 344
 345 (********************** complexity ***********************)
 346
 347 (* We assume operations have a minimal structural complexity MSC.
 348 For instance, for time complexity, MSC is equal to the size of input.
 349 For space complexity, MSC is typically 0, since we only measure the
 350 space required in addition to dimension of the input. *)
 351
 352 axiom MSC : nat → nat.
 353 axiom MSC_le: ∀n. MSC n ≤ n.
 354 axiom monotonic_MSC: monotonic ? le MSC.
 355
 356 (* C s i means i is running in O(s) *)
 357
 358 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ x → ∃y.
 359   U i x (c*(s x)) = Some ? y.
 360
 361 (* C f s means f ∈ O(s) where MSC ∈O(s) *)
 362 definition CF ≝ λs,f.O s MSC ∧ ∃i.code_for (total f) i ∧ C s i.
 363
 364 lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
 365 #f #g #s #Hext * #HO  * #i * #Hcode #HC % // %{i} %
 366   [#x cases (Hcode x) #a #H %{a} whd in match (total ??); <Hext @H | //]
 367 qed.
 368
 369 (* lemma ext_CF_total : ∀f,g,s. (∀n. f n = g n) → CF s (total f) → CF s (total g).
 370 #f #g #s #Hext * #HO * #i * #Hcode #HC % // %{i} % [2:@HC]
 371 #x cases (Hcode x) #a #H %{a} #m #leam >(H m leam) normalize @eq_f @Hext
 372 qed. *)
 373
 374 lemma monotonic_CF: ∀s1,s2,f.(∀x. s1 x ≤  s2 x) → CF s1 f → CF s2 f.
 375 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
 376   [cases HO #c * #a -HO #HO %{c} %{a} #n #lean @(transitive_le … (HO n lean))
 377    @le_times //
 378   |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1 %{c} %{a} #n #lean
 379    cases(Hs1 n lean) #y #Hy %{y} @(monotonic_U …Hy) @le_times //
 380   ]
 381 qed.
 382
 383 lemma O_to_CF: ∀s1,s2,f.O s2 s1 → CF s1 f → CF s2 f.
 384 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
 385   [@(O_trans … H) //
 386   |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1
 387    cases H #c1 * #a1 #Ha1 %{(c*c1)} %{(a+a1)} #n #lean
 388    cases(Hs1 n ?) [2:@(transitive_le … lean) //] #y #Hy %{y} @(monotonic_U …Hy)
 389    >associative_times @le_times // @Ha1 @(transitive_le … lean) //
 390   ]
 391 qed.
 392
 393 lemma timesc_CF: ∀s,f,c.CF (λx.c*s x) f → CF s f.
 394 #s #f #c @O_to_CF @O_times_c
 395 qed.
 396
 397 (********************************* composition ********************************)
 398 axiom CF_comp: ∀f,g,sf,sg,sh. CF sg g → CF sf f →
 399   O sh (λx. sg x + sf (g x)) → CF sh (f ∘ g).
 400
 401 lemma CF_comp_ext: ∀f,g,h,sh,sf,sg. CF sg g → CF sf f →
 402   (∀x.f(g x) = h x) → O sh (λx. sg x + sf (g x)) → CF sh h.
 403 #f #g #h #sh #sf #sg #Hg #Hf #Heq #H @(ext_CF (f ∘ g))
 404   [#n normalize @Heq | @(CF_comp … H) //]
 405 qed.
 406
 407 (*
 408 lemma CF_comp1: ∀f,g,s. CF s (total g) → CF s (total f) →
 409   CF s (total (f ∘ g)).
 410 #f #g #s #Hg #Hf @(timesc_CF … 2) @(monotonic_CF … (CF_comp … Hg Hf))
 411 *)
 412
 413 (*
 414 axiom CF_comp_ext2: ∀f,g,h,sf,sh. CF sh (total g) → CF sf (total f) →
 415   (∀x.f(g x) = h x) →
 416   (∀x. sf (g x) ≤ sh x) → CF sh (total h). *)
 417
 418 (* axiom main_MSC: ∀h,f. CF h f → O h (λx.MSC (f x)).
 419
 420 axiom CF_S: CF MSC (total S).
 421 axiom CF_fst: CF MSC (total fst).
 422 axiom CF_snd: CF MSC (total snd).
 423
 424 lemma CF_compS: ∀h,f. CF h (total f) → CF h (total (S ∘ f)).
 425 #h #f #Hf @(CF_comp … Hf CF_S) @O_plus // @main_MSC //
 426 qed.
 427
 428 lemma CF_comp_fst: ∀h,f. CF h (total f) → CF h (total (fst ∘ f)).
 429 #h #f #Hf @(CF_comp … Hf CF_fst) @O_plus // @main_MSC //
 430 qed.
 431
 432 lemma CF_comp_snd: ∀h,f. CF h (total f) → CF h (total (snd ∘ f)).
 433 #h #f #Hf @(CF_comp … Hf CF_snd) @O_plus // @main_MSC //
 434 qed. *)
 435
 436 axiom CF_compS: ∀h,f. CF h f → CF h (S ∘ f).
 437 axiom CF_comp_fst: ∀h,f. CF h f → CF h (fst ∘ f).
 438 axiom CF_comp_snd: ∀h,f. CF h f → CF h (snd ∘ f).
 439
 440 (************************************** eqb ***********************************)
 441 (* definition btotal ≝
 442   λf.λx:nat. match f x with [true ⇒ Some ? 0 |false ⇒ Some ? 1]. *)
 443
 444 axiom CF_eqb: ∀h,f,g.
 445   CF h f → CF h g → CF h (λx.eqb (f x) (g x)).
 446
 447 (*
 448 axiom eqb_compl2: ∀h,f,g.
 449   CF2 h (total2 f) → CF2 h (total2 g) →
 450     CF2 h (btotal2 (λx1,x2.eqb (f x1 x2) (g x1 x2))).
 451
 452 axiom eqb_min_input_compl:∀h,x.
 453    CF (λi.∑_{y ∈ [S i,S x[ }(h i y))
 454    (btotal (λi.eqb (min_input h i x) x)). *)
 455 (*********************************** maximum **********************************)
 456
 457 axiom CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
 458   CF ha a → CF hb b → CF hp p → CF hf f →
 459   O s (λx.ha x + hb x + ∑_{i ∈[a x ,b x[ }(hp 〈i,x〉 + hf 〈i,x〉)) →
 460   CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
 461
 462 (******************************** minimization ********************************)
 463
 464 axiom CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
 465   CF sa a → CF sb b → CF sf f →
 466   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
 467   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
 468
 469 (********************************* simulation *********************************)
 470
 471 axiom sU : nat → nat.
 472 definition termb_unary ≝ λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)).
 473
 474 axiom monotonic_sU: ∀i1,i2,x1,x2,s1,s2. i1 ≤ i2 → x1 ≤ x2 → s1 ≤ s2 →
 475   sU 〈i1,〈x1,s1〉〉 ≤ sU 〈i2,〈x2,s2〉〉.
 476
 477 axiom sU_le: ∀i,x,s. s ≤ sU 〈i,〈x,s〉〉.
 478
 479 lemma monotonic_sU_aux : ∀x1,x2. fst x1 ≤ fst x2 → fst (snd x1) ≤ fst (snd x2) →
 480 snd (snd x1) ≤ snd (snd x2) → sU x1 ≤ sU x2.
 481 #x1 #x2 cases (surj_pair x1) #a1 * #y #eqx1 >eqx1 -eqx1 cases (surj_pair y)
 482 #b1 * #c1 #eqy >eqy -eqy
 483 cases (surj_pair x2) #a2 * #y2 #eqx2 >eqx2 -eqx2 cases (surj_pair y2)
 484 #b2 * #c2 #eqy2 >eqy2 -eqy2 >fst_pair >snd_pair >fst_pair >snd_pair
 485 >fst_pair >snd_pair >fst_pair >snd_pair @monotonic_sU
 486 qed.
 487
 488 axiom CF_termb: CF sU (btotal (termb_unary)).
 489
 490 axiom CF_compb: ∀f,g,sf,sg,sh. CF sg (total g) → CF sf (btotal f) →
 491   O sh (λx. sg x + sf (g x)) → CF sh (btotal (f ∘ g)).
 492
 493 (*
 494 lemma CF_termb_comp: ∀f.CF (sU ∘ f) (btotal (termb_unary ∘ f)).
 495 #f @(CF_compb … CF_termb) *)
 496
 497 (******************** complexity of g ********************)
 498
 499 definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
 500 definition auxg ≝
 501   λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
 502     (out i (snd ux) (h (S i) (snd ux))).
 503
 504 lemma compl_g1 : ∀h,s.
 505   CF s (total (auxg h)) → CF s (total (unary_g h)).
 506 #h #s #H1 @(CF_compS ? (auxg h) H1)
 507 qed.
 508
 509 definition aux1g ≝
 510   λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
 511     ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
 512
 513 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
 514 #h #x @same_bigop
 515   [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
 516 qed.
 517
 518 lemma compl_g2 : ∀h,s1,s2,s.
 519   CF s1
 520     (btotal (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p)))) →
 521   CF s2
 522     (total (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))) →
 523   O s (λx.MSC x + ∑_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
 524   CF s (total (auxg h)).
 525 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (total (aux1g h)))
 526   [#n whd in ⊢ (??%%); @eq_f @eq_aux]
 527 @(CF_max … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
 528 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
 529 qed.
 530
 531 lemma compl_g3 : ∀h,s.
 532   CF s (total (λp:ℕ.min_input h (fst p) (snd (snd p)))) →
 533   CF s (btotal (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p)))).
 534 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (proj1 … H))
 535 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
 536 qed.
 537
 538 definition min_input_aux ≝ λh,p.
 539   μ_{y ∈ [S (fst p),snd (snd p)] }
 540     ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
 541
 542 lemma min_input_eq : ∀h,p.
 543     min_input_aux h p  =
 544     min_input h (fst p) (snd (snd p)).
 545 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
 546 whd in ⊢ (??%%); >fst_pair >snd_pair //
 547 qed.
 548
 549 definition termb_aux ≝ λh.
 550   termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
 551
 552 (*
 553 lemma termb_aux : ∀h,p.
 554   (λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)))
 555     〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉 =
 556   termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)) .
 557 #h #p normalize >fst_pair >snd_pair >fst_pair >snd_pair //
 558 qed. *)
 559
 560 lemma compl_g4 : ∀h,s1,s.
 561   (CF s1
 562    (btotal
 563     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p))))) →
 564    (O s (λx.MSC x + ∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
 565   CF s (total (λp:ℕ.min_input h (fst p) (snd (snd p)))).
 566 #h #s1 #s #Hs1 #HO @(ext_CF (total (min_input_aux h)))
 567  [#n whd in ⊢ (??%%); @eq_f @min_input_eq]
 568 @(CF_mu … MSC MSC … Hs1)
 569   [@CF_compS @CF_fst
 570   |@CF_comp_snd @CF_snd
 571   |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
 572 (* @(ext_CF (btotal (termb_aux h)))
 573   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
 574 @(CF_compb … CF_termb) *)
 575 qed.
 576
 577 (************************* a couple of technical lemmas ***********************)
 578 lemma minus_to_0: ∀a,b. a ≤ b → minus a b = 0.
 579 #a elim a // #n #Hind *
 580   [#H @False_ind /2 by absurd/ | #b normalize #H @Hind @le_S_S_to_le /2/]
 581 qed.
 582
 583 lemma sigma_bound:  ∀h,a,b. monotonic nat le h →
 584   ∑_{i ∈ [a,S b[ }(h i) ≤  (S b-a)*h b.
 585 #h #a #b #H cases (decidable_le a b)
 586   [#leab cut (b = pred (S b - a + a))
 587     [<plus_minus_m_m // @le_S //] #Hb >Hb in match (h b);
 588    generalize in match (S b -a);
 589    #n elim n
 590     [//
 591     |#m #Hind >bigop_Strue [2://] @le_plus
 592       [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
 593     ]
 594   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
 595    cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
 596   ]
 597 qed.
 598
 599 lemma sigma_bound_decr:  ∀h,a,b. (∀a1,a2. a1 ≤ a2 → a2 < b → h a2 ≤ h a1) →
 600   ∑_{i ∈ [a,b[ }(h i) ≤  (b-a)*h a.
 601 #h #a #b #H cases (decidable_le a b)
 602   [#leab cut ((b -a) +a ≤ b) [/2 by le_minus_to_plus_r/] generalize in match (b -a);
 603    #n elim n
 604     [//
 605     |#m #Hind >bigop_Strue [2://] #Hm
 606      cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
 607      @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
 608     ]
 609   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
 610    cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
 611   ]
 612 qed.
 613
 614
 615 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
 616 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
 617   (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
 618 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
 619 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
 620 qed.
 621
 622 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
 623 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
 624 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
 625 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
 626 qed.
 627
 628 lemma compl_g5 : ∀h,s1.(∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
 629   (CF s1
 630    (btotal
 631     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p))))) →
 632   CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
 633     (total (λp:ℕ.min_input h (fst p) (snd (snd p)))).
 634 #h #s1 #Hmono #Hs1 @(compl_g4 … Hs1) @O_plus
 635 [@O_plus_l // |@O_plus_r @coroll @Hmono]
 636 qed.
 637
 638 axiom compl_g6: ∀h.
 639   (CF (λx. sU 〈fst (snd x),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
 640    (btotal
 641     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p))))).
 642 (* #h #s1 @(ext_CF (btotal (termb_aux h)))
 643   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
 644 @(CF_compb … CF_termb) *)
 645
 646 definition faux1 ≝ λh.
 647   (λx.MSC x + (snd (snd x)-fst x)*(λx.sU 〈fst (snd x),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
 648
 649 (* complexity of min_input *)
 650 lemma compl_g7: ∀h. (∀n. monotonic ? le (h n)) →
 651   CF (λx.MSC x + (snd (snd x)-fst x)*sU 〈fst x,〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
 652     (total (λp:ℕ.min_input h (fst p) (snd (snd p)))).
 653 #h #hmono @(monotonic_CF … (faux1 h))
 654   [#n normalize >fst_pair >snd_pair //]
 655 @compl_g5 [2:@compl_g6] #n #x #y #lexy >fst_pair >snd_pair
 656 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
 657 qed.
 658
 659 definition big : nat →nat ≝ λx.
 660   let m ≝ max (fst x) (snd x) in 〈m,m〉.
 661
 662 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
 663 #a #b normalize >fst_pair >snd_pair // qed.
 664
 665 lemma le_big : ∀x. x ≤ big x.
 666 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
 667 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
 668 qed.
 669
 670 (* proviamo con x *)
 671 lemma compl_g71: ∀h. (∀n. monotonic ? le (h n)) →
 672   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))〉〉)
 673     (total (λp:ℕ.min_input h (fst p) (snd (snd p)))).
 674 #h #hmono @(monotonic_CF … (compl_g7 h hmono)) #x
 675 @le_plus [@monotonic_MSC //]
 676 cases (decidable_le (fst x) (snd(snd x)))
 677   [#Hle @le_times // @monotonic_sU // @(le_maxl … (le_n … ))
 678   |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
 679   ]
 680 qed.
 681
 682 axiom compl_g8: ∀h.
 683   CF (λx. sU 〈fst x,〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
 684     (total (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
 685
 686 lemma compl_g81: ∀h.
 687   CF (λx. sU 〈max (fst x) (snd x),〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
 688     (total (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
 689 #h @(monotonic_CF … (compl_g8 h)) #x @monotonic_sU // @(le_maxl … (le_n … ))
 690 qed.
 691
 692 axiom daemon : False.
 693
 694 lemma compl_g9 : ∀h.
 695   (∀n. monotonic ? le (h n)) →
 696   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
 697   CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
 698       (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
 699    (total (auxg h)).
 700 #h #hmono #hantimono @(compl_g2 h ??? (compl_g3 … (compl_g71 h hmono)) (compl_g81 h))
 701 @O_plus [@O_plus_l @le_to_O #x elim daemon]
 702 @(O_trans … (coroll2 ??))
 703   [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
 704    cut (max a n = n)
 705      [normalize >le_to_leb_true [//|elim daemon (*@(transitive_le … leab lebn)*)]] #maxa
 706    cut (max b n = n) [elim daemon (*normalize >le_to_leb_true //*)] #maxb
 707    @le_plus
 708     [@le_plus [>big_def >big_def >maxa >maxb //]
 709      @le_times
 710       [/2 by monotonic_le_minus_r/
 711       |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
 712       ]
 713     |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
 714     ]
 715   |@le_to_O #n >fst_pair >snd_pair
 716    cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
 717    >associative_plus >distributive_times_plus
 718    @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
 719   ]
 720 qed.
 721
 722 definition sg ≝ λh,x.
 723   (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)〉〉.
 724
 725 lemma sg_def : ∀h,a,b.
 726   sg h 〈a,b〉 = (S (b-a))*MSC 〈〈a,b〉,〈a,b〉〉 +
 727    (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
 728 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
 729 qed.
 730
 731 lemma compl_g11 : ∀h.
 732   (∀n. monotonic ? le (h n)) →
 733   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
 734   CF (sg h) (total (unary_g h)).
 735 #h #Hm #Ham @compl_g1 @(compl_g9 h Hm Ham)
 736 qed.
 737
 738 (**************************** closing the argument ****************************)
 739
 740 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
 741   match d with
 742   [ O ⇒ c (* MSC 〈〈b,b〉,〈b,b〉〉 *)
 743   | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
 744      d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
 745
 746 lemma h_of_aux_O: ∀r,c,b.
 747   h_of_aux r c O b  = c (* MSC 〈〈b,b〉,〈b,b〉〉*) .
 748 // qed.
 749
 750 lemma h_of_aux_S : ∀r,c,d,b.
 751   h_of_aux r c (S d) b =
 752     (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
 753       (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
 754 // qed.
 755
 756 definition h_of ≝ λr,p.
 757   let m ≝ max (fst p) (snd p) in
 758   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
 759
 760 lemma h_of_O: ∀r,a,b. b ≤ a →
 761   h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
 762 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
 763 qed.
 764
 765 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
 766   let m ≝ max a b in
 767   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
 768 #r #a #b normalize >fst_pair >snd_pair //
 769 qed.
 770
 771 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
 772   ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
 773   h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
 774 #r #Hr #monor #d #d1 lapply d -d elim d1
 775   [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
 776    >h_of_aux_O >h_of_aux_O  //
 777   |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
 778     [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
 779      >h_of_aux_S @(transitive_le ???? (le_plus_n …))
 780      >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
 781      >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
 782     |#Hd >Hd >h_of_aux_S >h_of_aux_S
 783      cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
 784      @le_plus [@le_times //]
 785       [@monotonic_MSC @le_pair @le_pair //
 786       |@le_times [//] @monotonic_sU
 787         [@le_pair // |// |@monor @Hind //]
 788       ]
 789     ]
 790   ]
 791 qed.
 792
 793 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
 794   ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
 795 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
 796 cut (max i a ≤ max i b)
 797   [@to_max
 798     [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
 799 #Hmax @(mono_h_of_aux r Hr Hmono)
 800   [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
 801 qed.
 802
 803 lemma speed_compl: ∀r:nat →nat.
 804   (∀x. x ≤ r x) → monotonic ? le r →
 805   CF (h_of r) (total (unary_g (λi,x. r(h_of r 〈i,x〉)))).
 806 #r #Hr #Hmono @(monotonic_CF … (compl_g11 …))
 807   [#x cases (surj_pair x) #a * #b #eqx >eqx
 808    >sg_def cases (decidable_le b a)
 809     [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
 810      <plus_n_O <plus_n_O >h_of_def
 811      cut (max a b = a)
 812       [normalize cases (le_to_or_lt_eq … leba)
 813         [#ltba >(lt_to_leb_false … ltba) %
 814         |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
 815      #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
 816      @monotonic_MSC @le_pair @le_pair //
 817     |#ltab >h_of_def >h_of_def
 818      cut (max a b = b)
 819       [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
 820      #Hmax >Hmax
 821      cut (max (S a) b = b)
 822       [whd in ⊢ (??%?);  >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
 823      #Hmax1 >Hmax1
 824      cut (∃d.b - a = S d) [elim daemon] * #d #eqd >eqd
 825      cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
 826      cut (b - S d = a)
 827        [@plus_to_minus >commutative_plus @minus_to_plus
 828          [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
 829      normalize //
 830     ]
 831   |#n #a #b #leab #lebn >h_of_def >h_of_def
 832    cut (max a n = n)
 833     [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
 834    cut (max b n = n)
 835     [normalize >(le_to_leb_true … lebn) %] #Hmaxb
 836    >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
 837   |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
 838   ]
 839 qed.
 840
 841 lemma unary_g_def : ∀h,i,x. g h i x = unary_g h 〈i,x〉.
 842 #h #i #x whd in ⊢ (???%); >fst_pair >snd_pair %
 843 qed.
 844
 845 (* smn *)
 846 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
 847
 848 lemma speed_compl_i: ∀r:nat →nat.
 849   (∀x. x ≤ r x) → monotonic ? le r →
 850   ∀i. CF (λx.h_of r 〈i,x〉) (total (λx.g (λi,x. r(h_of r 〈i,x〉)) i x)).
 851 #r #Hr #Hmono #i
 852 @(ext_CF (total (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉)))
 853   [#n whd in ⊢ (??%%); @eq_f @sym_eq @unary_g_def]
 854 @smn @(ext_CF … (speed_compl r Hr Hmono)) #n //
 855 qed.
 856
 857 theorem pseudo_speedup:
 858   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r →
 859   ∃f.∀sf. CF sf (total f) → ∃g,sg. f ≈ g ∧ CF sg (total g) ∧ O sf (r ∘ sg).
 860 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
 861 #r #Hr #Hmono
 862 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
 863 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
 864 #Hcodei #HCi
 865 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
 866 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 867 (* sg is (λx.h_of r 〈i,x〉) *)
 868 %{(λx. h_of r 〈S i,x〉)}
 869 lapply (speed_compl_i … Hr Hmono (S i)) #Hg
 870 %[%[@condition_1 |@Hg]
 871  |cases Hg #H1 * #j * #Hcodej #HCj
 872   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
 873   cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
 874   @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
 875   [@(transitive_le … ltin) @(le_maxl … (le_n …))]
 876   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
 877   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
 878  ]
 879 qed.
 880
 881 theorem pseudo_speedup':
 882   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r →
 883   ∃f.∀sf. CF sf (total f) → ∃g,sg. f ≈ g ∧ CF sg (total g) ∧
 884   (* ¬ O (r ∘ sg) sf. *)
 885   ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
 886 #r #Hr #Hmono
 887 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
 888 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
 889 #Hcodei #HCi
 890 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
 891 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 892 (* sg is (λx.h_of r 〈i,x〉) *)
 893 %{(λx. h_of r 〈S i,x〉)}
 894 lapply (speed_compl_i … Hr Hmono (S i)) #Hg
 895 %[%[@condition_1 |@Hg]
 896  |cases Hg #H1 * #j * #Hcodej #HCj
 897   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
 898   cases HCi #m * #a #Ha
 899   %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2 #Hlesf
 900   %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
 901   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
 902   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
 903   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
 904  ]
 905 qed.
 906