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