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 (********************************* simulation *********************************)
 494
 495 axiom sU : nat → nat.
 496
 497 axiom monotonic_sU: ∀i1,i2,x1,x2,s1,s2. i1 ≤ i2 → x1 ≤ x2 → s1 ≤ s2 →
 498   sU 〈i1,〈x1,s1〉〉 ≤ sU 〈i2,〈x2,s2〉〉.
 499
 500 lemma monotonic_sU_aux : ∀x1,x2. fst x1 ≤ fst x2 → fst (snd x1) ≤ fst (snd x2) →
 501 snd (snd x1) ≤ snd (snd x2) → sU x1 ≤ sU x2.
 502 #x1 #x2 cases (surj_pair x1) #a1 * #y #eqx1 >eqx1 -eqx1 cases (surj_pair y)
 503 #b1 * #c1 #eqy >eqy -eqy
 504 cases (surj_pair x2) #a2 * #y2 #eqx2 >eqx2 -eqx2 cases (surj_pair y2)
 505 #b2 * #c2 #eqy2 >eqy2 -eqy2 >fst_pair >snd_pair >fst_pair >snd_pair
 506 >fst_pair >snd_pair >fst_pair >snd_pair @monotonic_sU
 507 qed.
 508
 509 axiom sU_le: ∀i,x,s. s ≤ sU 〈i,〈x,s〉〉.
 510 axiom sU_le_i: ∀i,x,s. MSC i ≤ sU 〈i,〈x,s〉〉.
 511 axiom sU_le_x: ∀i,x,s. MSC x ≤ sU 〈i,〈x,s〉〉.
 512
 513 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
 514
 515 axiom CF_U : CF sU pU_unary.
 516
 517 definition termb_unary ≝ λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)).
 518 definition out_unary ≝ λx:ℕ.out (fst x) (fst (snd x)) (snd (snd x)).
 519
 520 lemma CF_termb: CF sU termb_unary.
 521 @(ext_CF (fst ∘ pU_unary)) [2: @CF_comp_fst @CF_U]
 522 #n whd in ⊢ (??%?); whd in  ⊢ (??(?%)?); >fst_pair %
 523 qed.
 524
 525 lemma CF_out: CF sU out_unary.
 526 @(ext_CF (snd ∘ pU_unary)) [2: @CF_comp_snd @CF_U]
 527 #n whd in ⊢ (??%?); whd in  ⊢ (??(?%)?); >snd_pair %
 528 qed.
 529
 530 (*
 531 lemma CF_termb_comp: ∀f.CF (sU ∘ f) (termb_unary ∘ f).
 532 #f @(CF_comp … CF_termb) *)
 533
 534 (******************** complexity of g ********************)
 535
 536 definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
 537 definition auxg ≝
 538   λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
 539     (out i (snd ux) (h (S i) (snd ux))).
 540
 541 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
 542 #h #s #H1 @(CF_compS ? (auxg h) H1)
 543 qed.
 544
 545 definition aux1g ≝
 546   λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
 547     ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
 548
 549 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
 550 #h #x @same_bigop
 551   [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
 552 qed.
 553
 554 lemma compl_g2 : ∀h,s1,s2,s.
 555   CF s1
 556     (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
 557   CF s2
 558     (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
 559   O s (λx.MSC x + ∑_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
 560   CF s (auxg h).
 561 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
 562   [#n whd in ⊢ (??%%); @eq_aux]
 563 @(CF_max … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
 564 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
 565 qed.
 566
 567 lemma compl_g3 : ∀h,s.
 568   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
 569   CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
 570 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (proj1 … H))
 571 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
 572 qed.
 573
 574 definition min_input_aux ≝ λh,p.
 575   μ_{y ∈ [S (fst p),snd (snd p)] }
 576     ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
 577
 578 lemma min_input_eq : ∀h,p.
 579     min_input_aux h p  =
 580     min_input h (fst p) (snd (snd p)).
 581 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
 582 whd in ⊢ (??%%); >fst_pair >snd_pair //
 583 qed.
 584
 585 definition termb_aux ≝ λh.
 586   termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
 587
 588 (*
 589 lemma termb_aux : ∀h,p.
 590   (λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)))
 591     〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉 =
 592   termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)) .
 593 #h #p normalize >fst_pair >snd_pair >fst_pair >snd_pair //
 594 qed. *)
 595
 596 lemma compl_g4 : ∀h,s1,s.
 597   (CF s1
 598     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
 599    (O s (λx.MSC x + ∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
 600   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
 601 #h #s1 #s #Hs1 #HO @(ext_CF (min_input_aux h))
 602  [#n whd in ⊢ (??%%); @min_input_eq]
 603 @(CF_mu … MSC MSC … Hs1)
 604   [@CF_compS @CF_fst
 605   |@CF_comp_snd @CF_snd
 606   |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
 607 (* @(ext_CF (btotal (termb_aux h)))
 608   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
 609 @(CF_compb … CF_termb) *)
 610 qed.
 611
 612 (************************* a couple of technical lemmas ***********************)
 613 lemma minus_to_0: ∀a,b. a ≤ b → minus a b = 0.
 614 #a elim a // #n #Hind *
 615   [#H @False_ind /2 by absurd/ | #b normalize #H @Hind @le_S_S_to_le /2/]
 616 qed.
 617
 618 lemma sigma_bound:  ∀h,a,b. monotonic nat le h →
 619   ∑_{i ∈ [a,S b[ }(h i) ≤  (S b-a)*h b.
 620 #h #a #b #H cases (decidable_le a b)
 621   [#leab cut (b = pred (S b - a + a))
 622     [<plus_minus_m_m // @le_S //] #Hb >Hb in match (h b);
 623    generalize in match (S b -a);
 624    #n elim n
 625     [//
 626     |#m #Hind >bigop_Strue [2://] @le_plus
 627       [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
 628     ]
 629   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
 630    cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
 631   ]
 632 qed.
 633
 634 lemma sigma_bound_decr:  ∀h,a,b. (∀a1,a2. a1 ≤ a2 → a2 < b → h a2 ≤ h a1) →
 635   ∑_{i ∈ [a,b[ }(h i) ≤  (b-a)*h a.
 636 #h #a #b #H cases (decidable_le a b)
 637   [#leab cut ((b -a) +a ≤ b) [/2 by le_minus_to_plus_r/] generalize in match (b -a);
 638    #n elim n
 639     [//
 640     |#m #Hind >bigop_Strue [2://] #Hm
 641      cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
 642      @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
 643     ]
 644   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
 645    cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
 646   ]
 647 qed.
 648
 649 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
 650 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
 651   (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
 652 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
 653 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
 654 qed.
 655
 656 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
 657 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
 658 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
 659 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
 660 qed.
 661
 662 lemma compl_g5 : ∀h,s1.(∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
 663   (CF s1
 664     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
 665   CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
 666     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 667 #h #s1 #Hmono #Hs1 @(compl_g4 … Hs1) @O_plus
 668 [@O_plus_l // |@O_plus_r @coroll @Hmono]
 669 qed.
 670
 671 (*
 672 axiom compl_g6: ∀h.
 673   (* constructible (λx. h (fst x) (snd x)) → *)
 674   (CF (λx. max (MSC x) (sU 〈fst (snd x),〈fst x,h (S (fst (snd x))) (fst x)〉〉))
 675     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
 676 *)
 677
 678 lemma compl_g6: ∀h.
 679   (∀x.MSC x≤h (S (fst (snd x))) (fst x)) →
 680   constructible (λx. h (fst x) (snd x)) →
 681   (CF (λx. sU 〈fst (snd x),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
 682     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
 683 #h #hle #hconstr @(ext_CF (termb_aux h))
 684   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
 685 @(CF_comp … (λx.h (S (fst (snd x))) (fst x)) … CF_termb)
 686   [@CF_comp_pair
 687     [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
 688     |@CF_comp_pair
 689       [@(monotonic_CF … CF_fst) #x //
 690       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
 691         [#n normalize >fst_pair >snd_pair %]
 692        @(CF_comp … MSC …hconstr)
 693         [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
 694         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
 695         ]
 696       ]
 697     ]
 698   |@O_plus [@le_to_O #n @sU_le | // ]
 699   ]
 700 qed.
 701
 702
 703 definition faux1 ≝ λh.
 704   (λ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〉).
 705
 706 (* complexity of min_input *)
 707 lemma compl_g7: ∀h.
 708   (∀x.MSC x≤h (S (fst (snd x))) (fst x)) →
 709   constructible (λx. h (fst x) (snd x)) →
 710   (∀n. monotonic ? le (h n)) →
 711   CF (λx.MSC x + (snd (snd x)-fst x)*sU 〈fst x,〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
 712     (λp:ℕ.min_input h (fst p) (snd (snd p))).
 713 #h #hle #hcostr #hmono @(monotonic_CF … (faux1 h))
 714   [#n normalize >fst_pair >snd_pair //]
 715 @compl_g5 [2:@(compl_g6 h hle hcostr)] #n #x #y #lexy >fst_pair >snd_pair
 716 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
 717 qed.
 718
 719 definition big : nat →nat ≝ λx.
 720   let m ≝ max (fst x) (snd x) in 〈m,m〉.
 721
 722 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
 723 #a #b normalize >fst_pair >snd_pair // qed.
 724
 725 lemma le_big : ∀x. x ≤ big x.
 726 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
 727 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
 728 qed.
 729
 730 (* proviamo con x *)
 731 lemma compl_g71: ∀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 (big x) + (snd (snd x)-fst x)*sU 〈max (fst x) (snd 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 … (compl_g7 h hle hcostr hmono)) #x
 738 @le_plus [@monotonic_MSC //]
 739 cases (decidable_le (fst x) (snd(snd x)))
 740   [#Hle @le_times // @monotonic_sU // @(le_maxl … (le_n … ))
 741   |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
 742   ]
 743 qed.
 744
 745 (*
 746 axiom compl_g8: ∀h.
 747   CF (λx. sU 〈fst x,〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
 748     (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))). *)
 749
 750 definition out_aux ≝ λh.
 751   out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
 752
 753 lemma compl_g8: ∀h.
 754   constructible (λx. h (fst x) (snd x)) →
 755   (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
 756     (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
 757 #h #hconstr @(ext_CF (out_aux h))
 758   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
 759 @(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
 760   [@CF_comp_pair
 761     [@(monotonic_CF … CF_fst) #x //
 762     |@CF_comp_pair
 763       [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
 764       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
 765         [#n normalize >fst_pair >snd_pair %]
 766        @(CF_comp … MSC …hconstr)
 767         [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
 768         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
 769         ]
 770       ]
 771     ]
 772   |@O_plus
 773     [@O_plus
 774       [@le_to_O #n @sU_le
 775       |@(O_trans … (λx.MSC (max (fst x) (snd x))))
 776         [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
 777          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
 778          whd in ⊢ (??%); @le_plus
 779           [@monotonic_MSC @(le_maxl … (le_n …))
 780           |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
 781           ]
 782         |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
 783         ]
 784       ]
 785     |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
 786   ]
 787 qed.
 788
 789 (*
 790 lemma compl_g81: ∀h.
 791   (∀x.MSC x≤h (S (fst x)) (snd(snd x))) →
 792   constructible (λx. h (fst x) (snd x)) →
 793   CF (λx. sU 〈max (fst x) (snd x),〈snd (snd x),h (S (fst x)) (snd (snd x))〉〉)
 794     (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))).
 795 #h #hle #hconstr @(monotonic_CF ???? (compl_g8 h hle hconstr)) #x @monotonic_sU // @(le_maxl … (le_n … ))
 796 qed. *)
 797
 798 (* axiom daemon : False. *)
 799
 800 lemma compl_g9 : ∀h.
 801   (∀x.MSC x≤h (S (fst (snd x))) (fst x)) →
 802   (∀x.MSC x≤h (S (fst x)) (snd(snd x))) →
 803   constructible (λx. h (fst x) (snd x)) →
 804   (∀n. monotonic ? le (h n)) →
 805   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
 806   CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
 807       (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
 808    (auxg h).
 809 #h #hle #hle1 #hconstr #hmono #hantimono
 810 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hle hconstr hmono)) (compl_g81 h hle1 hconstr))
 811 @O_plus
 812   [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
 813     [// | @monotonic_MSC // ]]
 814 @(O_trans … (coroll2 ??))
 815   [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
 816    cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
 817    cut (max a n = n)
 818     [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
 819    cut (max b n = n) [normalize >le_to_leb_true //] #maxb
 820    @le_plus
 821     [@le_plus [>big_def >big_def >maxa >maxb //]
 822      @le_times
 823       [/2 by monotonic_le_minus_r/
 824       |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
 825       ]
 826     |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
 827     ]
 828   |@le_to_O #n >fst_pair >snd_pair
 829    cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
 830    >associative_plus >distributive_times_plus
 831    @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
 832   ]
 833 qed.
 834
 835 definition sg ≝ λh,x.
 836   (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)〉〉.
 837
 838 lemma sg_def : ∀h,a,b.
 839   sg h 〈a,b〉 = (S (b-a))*MSC 〈〈a,b〉,〈a,b〉〉 +
 840    (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
 841 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
 842 qed.
 843
 844 lemma compl_g11 : ∀h.
 845   (∀x.MSC x≤h (S (fst (snd x))) (fst x)) →
 846   (∀x.MSC x≤h (S (fst x)) (snd(snd x))) →
 847   constructible (λx. h (fst x) (snd x)) →
 848   (∀n. monotonic ? le (h n)) →
 849   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
 850   CF (sg h) (unary_g h).
 851 #h #hle #hle1 #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hle hle1 hconstr Hm Ham)
 852 qed.
 853
 854 (**************************** closing the argument ****************************)
 855
 856 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
 857   match d with
 858   [ O ⇒ c (* MSC 〈〈b,b〉,〈b,b〉〉 *)
 859   | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
 860      d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
 861
 862 lemma h_of_aux_O: ∀r,c,b.
 863   h_of_aux r c O b  = c (* MSC 〈〈b,b〉,〈b,b〉〉*) .
 864 // qed.
 865
 866 lemma h_of_aux_S : ∀r,c,d,b.
 867   h_of_aux r c (S d) b =
 868     (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
 869       (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
 870 // qed.
 871
 872 definition h_of ≝ λr,p.
 873   let m ≝ max (fst p) (snd p) in
 874   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
 875
 876 lemma h_of_O: ∀r,a,b. b ≤ a →
 877   h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
 878 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
 879 qed.
 880
 881 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
 882   let m ≝ max a b in
 883   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
 884 #r #a #b normalize >fst_pair >snd_pair //
 885 qed.
 886
 887 lemma h_le1 : ∀r.(∀x. x ≤ r x) → monotonic ? le r →
 888 (∀x:ℕ.MSC x≤r (h_of r 〈S (fst x),snd (snd x)〉)).
 889 #r #Hr #Hmono #x @(transitive_le ???? (Hr …))
 890 >h_of_def
 891
 892 (*  (∀x.MSC x≤h (S (fst x)) (snd(snd x))) → *)
 893
 894 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
 895   ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
 896   h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
 897 #r #Hr #monor #d #d1 lapply d -d elim d1
 898   [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
 899    >h_of_aux_O >h_of_aux_O  //
 900   |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
 901     [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
 902      >h_of_aux_S @(transitive_le ???? (le_plus_n …))
 903      >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
 904      >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
 905     |#Hd >Hd >h_of_aux_S >h_of_aux_S
 906      cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
 907      @le_plus [@le_times //]
 908       [@monotonic_MSC @le_pair @le_pair //
 909       |@le_times [//] @monotonic_sU
 910         [@le_pair // |// |@monor @Hind //]
 911       ]
 912     ]
 913   ]
 914 qed.
 915
 916 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
 917   ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
 918 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
 919 cut (max i a ≤ max i b)
 920   [@to_max
 921     [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
 922 #Hmax @(mono_h_of_aux r Hr Hmono)
 923   [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
 924 qed.
 925
 926 lemma speed_compl: ∀r:nat →nat.
 927   (∀x. x ≤ r x) → monotonic ? le r →
 928   CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
 929 #r #Hr #Hmono @(monotonic_CF … (compl_g11 …))
 930   [#x cases (surj_pair x) #a * #b #eqx >eqx
 931    >sg_def cases (decidable_le b a)
 932     [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
 933      <plus_n_O <plus_n_O >h_of_def
 934      cut (max a b = a)
 935       [normalize cases (le_to_or_lt_eq … leba)
 936         [#ltba >(lt_to_leb_false … ltba) %
 937         |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
 938      #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
 939      @monotonic_MSC @le_pair @le_pair //
 940     |#ltab >h_of_def >h_of_def
 941      cut (max a b = b)
 942       [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
 943      #Hmax >Hmax
 944      cut (max (S a) b = b)
 945       [whd in ⊢ (??%?);  >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
 946      #Hmax1 >Hmax1
 947      cut (∃d.b - a = S d)
 948        [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
 949      * #d #eqd >eqd
 950      cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
 951      cut (b - S d = a)
 952        [@plus_to_minus >commutative_plus @minus_to_plus
 953          [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
 954      normalize //
 955     ]
 956   |#n #a #b #leab #lebn >h_of_def >h_of_def
 957    cut (max a n = n)
 958     [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
 959    cut (max b n = n)
 960     [normalize >(le_to_leb_true … lebn) %] #Hmaxb
 961    >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
 962   |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
 963   ]
 964 qed.
 965
 966 (*
 967 lemma unary_g_def : ∀h,i,x. g h i x = unary_g h 〈i,x〉.
 968 #h #i #x whd in ⊢ (???%); >fst_pair >snd_pair %
 969 qed.  *)
 970
 971 (* smn *)
 972 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
 973
 974 lemma speed_compl_i: ∀r:nat →nat.
 975   (∀x. x ≤ r x) → monotonic ? le r →
 976   ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
 977 #r #Hr #Hmono #i
 978 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
 979   [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
 980 @smn @(ext_CF … (speed_compl r Hr Hmono)) #n //
 981 qed.
 982
 983 theorem pseudo_speedup:
 984   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r →
 985   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
 986 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
 987 #r #Hr #Hmono
 988 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
 989 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
 990 #Hcodei #HCi
 991 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
 992 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
 993 (* sg is (λx.h_of r 〈i,x〉) *)
 994 %{(λx. h_of r 〈S i,x〉)}
 995 lapply (speed_compl_i … Hr Hmono (S i)) #Hg
 996 %[%[@condition_1 |@Hg]
 997  |cases Hg #H1 * #j * #Hcodej #HCj
 998   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
 999   cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
1000   @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
1001   [@(transitive_le … ltin) @(le_maxl … (le_n …))]
1002   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
1003   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
1004  ]
1005 qed.
1006
1007 theorem pseudo_speedup':
1008   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r →
1009   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
1010   (* ¬ O (r ∘ sg) sf. *)
1011   ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
1012 #r #Hr #Hmono
1013 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
1014 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
1015 #Hcodei #HCi
1016 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
1017 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
1018 (* sg is (λx.h_of r 〈i,x〉) *)
1019 %{(λx. h_of r 〈S i,x〉)}
1020 lapply (speed_compl_i … Hr Hmono (S i)) #Hg
1021 %[%[@condition_1 |@Hg]
1022  |cases Hg #H1 * #j * #Hcodej #HCj
1023   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
1024   cases HCi #m * #a #Ha
1025   %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2 #Hlesf
1026   %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
1027   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
1028   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
1029   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
1030  ]
1031 qed.
1032