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