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