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 lemma expand_pair: ∀x. x = 〈fst x, snd x〉.
 105 #x lapply (surj_pair x) * #a * #b #Hx >Hx >fst_pair >snd_pair //
 106 qed.
 107
 108 (************************************* U **************************************)
 109 axiom U: nat → nat →nat → option nat.
 110
 111 axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
 112   U i x n = Some ? y → U i x m = Some ? y.
 113
 114 lemma unique_U: ∀i,x,n,m,yn,ym.
 115   U i x n = Some ? yn → U i x m = Some ? ym → yn = ym.
 116 #i #x #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
 117   [#lenm lapply (monotonic_U … lenm Hn) >Hm #HS destruct (HS) //
 118   |#ltmn lapply (monotonic_U … n … Hm) [@lt_to_le @not_le_to_lt //]
 119    >Hn #HS destruct (HS) //
 120   ]
 121 qed.
 122
 123 definition code_for ≝ λf,i.∀x.
 124   ∃n.∀m. n ≤ m → U i x m = f x.
 125
 126 definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y.
 127
 128 notation "{i ⊙ x} ↓ r" with precedence 60 for @{terminate $i $x $r}.
 129
 130 lemma terminate_dec: ∀i,x,n. {i ⊙ x} ↓ n ∨ ¬ {i ⊙ x} ↓ n.
 131 #i #x #n normalize cases (U i x n)
 132   [%2 % * #y #H destruct|#y %1 %{y} //]
 133 qed.
 134
 135 lemma monotonic_terminate: ∀i,x,n,m.
 136   n ≤ m → {i ⊙ x} ↓ n → {i ⊙ x} ↓ m.
 137 #i #x #n #m #lenm * #z #H %{z} @(monotonic_U … H) //
 138 qed.
 139
 140 definition termb ≝ λi,x,t.
 141   match U i x t with [None ⇒ false |Some y ⇒ true].
 142
 143 lemma termb_true_to_term: ∀i,x,t. termb i x t = true → {i ⊙ x} ↓ t.
 144 #i #x #t normalize cases (U i x t) normalize [#H destruct | #y #_ %{y} //]
 145 qed.
 146
 147 lemma term_to_termb_true: ∀i,x,t. {i ⊙ x} ↓ t → termb i x t = true.
 148 #i #x #t * #y #H normalize >H //
 149 qed.
 150
 151 definition out ≝ λi,x,r.
 152   match U i x r with [ None ⇒ 0 | Some z ⇒ z].
 153
 154 definition bool_to_nat: bool → nat ≝
 155   λb. match b with [true ⇒ 1 | false ⇒ 0].
 156
 157 coercion bool_to_nat.
 158
 159 definition pU : nat → nat → nat → nat ≝ λi,x,r.〈termb i x r,out i x r〉.
 160
 161 lemma pU_vs_U_Some : ∀i,x,r,y. pU i x r = 〈1,y〉 ↔ U i x r = Some ? y.
 162 #i #x #r #y % normalize
 163   [cases (U i x r) normalize
 164     [#H cut (0=1) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H @H]
 165      #H1 destruct
 166     |#a #H cut (a=y) [lapply (eq_f … snd … H) >snd_pair >snd_pair #H1 @H1]
 167      #H1 //
 168     ]
 169   |#H >H //]
 170 qed.
 171
 172 lemma pU_vs_U_None : ∀i,x,r. pU i x r = 〈0,0〉 ↔ U i x r = None ?.
 173 #i #x #r % normalize
 174   [cases (U i x r) normalize //
 175    #a #H cut (1=0) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H1 @H1]
 176    #H1 destruct
 177   |#H >H //]
 178 qed.
 179
 180 lemma fst_pU: ∀i,x,r. fst (pU i x r) = termb i x r.
 181 #i #x #r normalize cases (U i x r) normalize >fst_pair //
 182 qed.
 183
 184 lemma snd_pU: ∀i,x,r. snd (pU i x r) = out i x r.
 185 #i #x #r normalize cases (U i x r) normalize >snd_pair //
 186 qed.
 187
 188
 189 definition total ≝ λf.λx:nat. Some nat (f x).
 190
 191
 192 (********************************* complexity *********************************)
 193
 194 (* We assume operations have a minimal structural complexity MSC.
 195 For instance, for time complexity, MSC is equal to the size of input.
 196 For space complexity, MSC is typically 0, since we only measure the
 197 space required in addition to dimension of the input. *)
 198
 199 axiom MSC : nat → nat.
 200 axiom MSC_le: ∀n. MSC n ≤ n.
 201 axiom monotonic_MSC: monotonic ? le MSC.
 202 axiom MSC_pair: ∀a,b. MSC 〈a,b〉 ≤ MSC a + MSC b.
 203
 204 (* C s i means i is running in O(s) *)
 205
 206 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ x → ∃y.
 207   U i x (c*(s x)) = Some ? y.
 208
 209 (* C f s means f ∈ O(s) where MSC ∈O(s) *)
 210 definition CF ≝ λs,f.O s MSC ∧ ∃i.code_for (total f) i ∧ C s i.
 211
 212 lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
 213 #f #g #s #Hext * #HO  * #i * #Hcode #HC % // %{i} %
 214   [#x cases (Hcode x) #a #H %{a} whd in match (total ??); <Hext @H | //]
 215 qed.
 216
 217 lemma ext_CF1 : ∀f,g,s. (∀n. f n = g n) → CF s g → CF s f.
 218 #f #g #s #Hext * #HO  * #i * #Hcode #HC % // %{i} %
 219   [#x cases (Hcode x) #a #H %{a} whd in match (total ??); >Hext @H | //]
 220 qed.
 221
 222 lemma monotonic_CF: ∀s1,s2,f.(∀x. s1 x ≤  s2 x) → CF s1 f → CF s2 f.
 223 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
 224   [cases HO #c * #a -HO #HO %{c} %{a} #n #lean @(transitive_le … (HO n lean))
 225    @le_times //
 226   |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1 %{c} %{a} #n #lean
 227    cases(Hs1 n lean) #y #Hy %{y} @(monotonic_U …Hy) @le_times //
 228   ]
 229 qed.
 230
 231 lemma O_to_CF: ∀s1,s2,f.O s2 s1 → CF s1 f → CF s2 f.
 232 #s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
 233   [@(O_trans … H) //
 234   |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1
 235    cases H #c1 * #a1 #Ha1 %{(c*c1)} %{(a+a1)} #n #lean
 236    cases(Hs1 n ?) [2:@(transitive_le … lean) //] #y #Hy %{y} @(monotonic_U …Hy)
 237    >associative_times @le_times // @Ha1 @(transitive_le … lean) //
 238   ]
 239 qed.
 240
 241 lemma timesc_CF: ∀s,f,c.CF (λx.c*s x) f → CF s f.
 242 #s #f #c @O_to_CF @O_times_c
 243 qed.
 244
 245 (********************************* composition ********************************)
 246 axiom CF_comp: ∀f,g,sf,sg,sh. CF sg g → CF sf f →
 247   O sh (λx. sg x + sf (g x)) → CF sh (f ∘ g).
 248
 249 lemma CF_comp_ext: ∀f,g,h,sh,sf,sg. CF sg g → CF sf f →
 250   (∀x.f(g x) = h x) → O sh (λx. sg x + sf (g x)) → CF sh h.
 251 #f #g #h #sh #sf #sg #Hg #Hf #Heq #H @(ext_CF (f ∘ g))
 252   [#n normalize @Heq | @(CF_comp … H) //]
 253 qed.
 254
 255 (* primitve recursion *)
 256
 257 (* no arguments *)
 258
 259 let rec prim_rec0 (k:nat) (h:nat →nat) n on n ≝
 260   match n with
 261   [ O ⇒ k
 262   | S a ⇒ h 〈a, prim_rec0 k h a〉].
 263
 264 lemma prim_rec0_S: ∀k,h,n.
 265   prim_rec0 k h (S n) = h 〈n, prim_rec0 k h n〉.
 266 // qed.
 267
 268 let rec prim_rec0_compl (k,sk:nat) (h,sh:nat →nat) n on n ≝
 269   match n with
 270   [ O ⇒ sk
 271   | S a ⇒ prim_rec0_compl k sk h sh a + sh (prim_rec0 k h a)].
 272
 273 axiom CF_prim_rec0_gen: ∀k,h,sk,sh,sh1,sf. CF sh h →
 274   O sh1 (λx.snd x + sh 〈fst x,prim_rec0 k h (fst x)〉) →
 275   O sf (prim_rec0 sk sh1) →
 276    CF sf (prim_rec0 k h).
 277
 278 lemma CF_prim_rec0: ∀k,h,sk,sh,sf. CF sh h →
 279   O sf (prim_rec0 sk (λx. snd x + sh 〈fst x,prim_rec0 k h (fst x)〉))
 280    → CF sf (prim_rec0 k h).
 281 #k #h #sk #sh #sf #Hh #HO @(CF_prim_rec0_gen … Hh … HO) @O_refl
 282 qed.
 283
 284 (* with argument(s) m *)
 285 let rec prim_rec (k,h:nat →nat) n m on n ≝
 286   match n with
 287   [ O ⇒ k m
 288   | S a ⇒ h 〈a,〈prim_rec k h a m, m〉〉].
 289
 290 lemma prim_rec_S: ∀k,h,n,m.
 291   prim_rec k h (S n) m = h 〈n,〈prim_rec k h n m, m〉〉.
 292 // qed.
 293
 294 lemma prim_rec_le: ∀k1,k2,h1,h2. (∀x.k1 x ≤ k2 x) →
 295 (∀x,y.x ≤y → h1 x ≤ h2 y) →
 296   ∀x,m. prim_rec k1 h1 x m ≤ prim_rec k2 h2 x m.
 297 #k1 #k2 #h1 #h2 #lek #leh #x #m elim x //
 298 #n #Hind normalize @leh @le_pair // @le_pair //
 299 qed.
 300
 301 definition unary_pr ≝ λk,h,x. prim_rec k h (fst x) (snd x).
 302
 303 lemma prim_rec_unary: ∀k,h,a,b.
 304   prim_rec k h a b = unary_pr k h 〈a,b〉.
 305 #k #h #a #b normalize >fst_pair >snd_pair //
 306 qed.
 307
 308
 309 let rec prim_rec_compl (k,h,sk,sh:nat →nat) n m on n ≝
 310   match n with
 311   [ O ⇒ sk m
 312   | S a ⇒ prim_rec_compl k h sk sh a m + sh (prim_rec k h a m)].
 313
 314 axiom CF_prim_rec_gen: ∀k,h,sk,sh,sh1. CF sk k → CF sh h →
 315   O sh1 (λx. fst (snd x) + sh 〈fst x,〈unary_pr k h 〈fst x,snd (snd x)〉,snd (snd x)〉〉) →
 316    CF (unary_pr sk sh1) (unary_pr k h).
 317
 318 lemma CF_prim_rec: ∀k,h,sk,sh,sf. CF sk k → CF sh h →
 319   O sf (unary_pr sk (λx. fst (snd x) + sh 〈fst x,〈unary_pr k h 〈fst x,snd (snd x)〉,snd (snd x)〉〉))
 320    → CF sf (unary_pr k h).
 321 #k #h #sk #sh #sf #Hk #Hh #Osf @(O_to_CF … Osf) @(CF_prim_rec_gen … Hk Hh) @O_refl
 322 qed.
 323
 324 (**************************** primitive operations*****************************)
 325
 326 definition id ≝ λx:nat.x.
 327
 328 axiom CF_id: CF MSC id.
 329 axiom CF_const: ∀k.CF MSC (λx.k).
 330 axiom CF_compS: ∀h,f. CF h f → CF h (S ∘ f).
 331 axiom CF_comp_fst: ∀h,f. CF h f → CF h (fst ∘ f).
 332 axiom CF_comp_snd: ∀h,f. CF h f → CF h (snd ∘ f).
 333 axiom CF_comp_pair: ∀h,f,g. CF h f → CF h g → CF h (λx. 〈f x,g x〉).
 334
 335 lemma CF_fst: CF MSC fst.
 336 @(ext_CF (fst ∘ id)) [#n //] @(CF_comp_fst … CF_id)
 337 qed.
 338
 339 lemma CF_snd: CF MSC snd.
 340 @(ext_CF (snd ∘ id)) [#n //] @(CF_comp_snd … CF_id)
 341 qed.
 342
 343 (************************************** eqb ***********************************)
 344
 345 axiom CF_eqb: ∀h,f,g.
 346   CF h f → CF h g → CF h (λx.eqb (f x) (g x)).
 347
 348 (*********************************** maximum **********************************)
 349
 350 alias symbol "pair" (instance 13) = "abstract pair".
 351 alias symbol "pair" (instance 12) = "abstract pair".
 352 alias symbol "and" (instance 11) = "boolean and".
 353 alias symbol "plus" (instance 8) = "natural plus".
 354 alias symbol "pair" (instance 7) = "abstract pair".
 355 alias symbol "plus" (instance 6) = "natural plus".
 356 alias symbol "pair" (instance 5) = "abstract pair".
 357 alias id "max" = "cic:/matita/arithmetics/nat/max#def:2".
 358 alias symbol "minus" (instance 3) = "natural minus".
 359 lemma max_gen: ∀a,b,p,f,x. a ≤b →
 360   max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) = max_{i < b | leb a i ∧ p 〈i,x〉 }(f 〈i,x〉).
 361 #a #b #p #f #x @(bigop_I_gen ????? MaxA)
 362 qed.
 363
 364 lemma max_prim_rec_base: ∀a,b,p,f,x. a ≤b →
 365   max_{i < b| p 〈i,x〉 }(f 〈i,x〉) =
 366     prim_rec (λi.0)
 367     (λi.if p 〈fst i,x〉 then max (f 〈fst i,snd (snd i)〉) (fst (snd i)) else fst (snd i)) b x.
 368 #a #b #p #f #x #leab >max_gen // elim b
 369   [normalize //
 370   |#i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
 371    cases (true_or_false (p 〈i,x〉)) #Hcase >Hcase
 372     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 373   ]
 374 qed.
 375
 376 lemma max_prim_rec: ∀a,b,p,f,x. a ≤b →
 377   max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) =
 378     prim_rec (λi.0)
 379     (λi.if leb a (fst i) ∧ p 〈fst i,x〉 then max (f 〈fst i,snd (snd i)〉) (fst (snd i)) else fst (snd i)) b x.
 380 #a #b #p #f #x #leab >max_gen // elim b
 381   [normalize //
 382   |#i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
 383    cases (true_or_false (leb a i ∧ p 〈i,x〉)) #Hcase >Hcase
 384     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 385   ]
 386 qed.
 387
 388 (* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
 389 alias symbol "pair" (instance 15) = "abstract pair".
 390 alias symbol "minus" (instance 14) = "natural minus".
 391 alias symbol "plus" (instance 11) = "natural plus".
 392 alias symbol "pair" (instance 10) = "abstract pair".
 393 alias symbol "plus" (instance 13) = "natural plus".
 394 alias symbol "pair" (instance 12) = "abstract pair".
 395 alias symbol "plus" (instance 8) = "natural plus".
 396 alias symbol "pair" (instance 7) = "abstract pair".
 397 alias symbol "plus" (instance 6) = "natural plus".
 398 alias symbol "pair" (instance 5) = "abstract pair".
 399 alias id "max" = "cic:/matita/arithmetics/nat/max#def:2".
 400 alias symbol "minus" (instance 3) = "natural minus".
 401 lemma max_prim_rec1: ∀a,b,p,f,x.
 402   max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
 403     prim_rec (λi.0)
 404     (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
 405         then max (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
 406         else fst (snd i)) (b x-a x) 〈a x ,x〉.
 407 #a #b #p #f #x elim (b x-a x)
 408   [normalize //
 409   |#i #Hind >prim_rec_S
 410    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 411    cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
 412     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 413   ]
 414 qed.
 415
 416 lemma sum_prim_rec1: ∀a,b,p,f,x.
 417   ∑_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
 418     prim_rec (λi.0)
 419     (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
 420         then plus (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
 421         else fst (snd i)) (b x-a x) 〈a x ,x〉.
 422 #a #b #p #f #x elim (b x-a x)
 423   [normalize //
 424   |#i #Hind >prim_rec_S
 425    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 426    cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
 427     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 428   ]
 429 qed.
 430
 431 (* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
 432 alias symbol "pair" (instance 15) = "abstract pair".
 433 alias symbol "minus" (instance 14) = "natural minus".
 434 alias symbol "plus" (instance 11) = "natural plus".
 435 alias symbol "pair" (instance 10) = "abstract pair".
 436 alias symbol "plus" (instance 13) = "natural plus".
 437 alias symbol "pair" (instance 12) = "abstract pair".
 438 alias symbol "plus" (instance 8) = "natural plus".
 439 alias symbol "pair" (instance 7) = "abstract pair".
 440 alias symbol "pair" (instance 6) = "abstract pair".
 441 alias symbol "plus" (instance 4) = "natural plus".
 442 alias symbol "pair" (instance 3) = "abstract pair".
 443 alias symbol "minus" (instance 2) = "natural minus".
 444 lemma bigop_prim_rec: ∀a,b,c,p,f,x.
 445   bigop (b x-a x) (λi:ℕ.p 〈i+a x,x〉) ? (c 〈a x,x〉) plus (λi:ℕ.f 〈i+a x,x〉) =
 446     prim_rec c
 447     (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
 448         then plus (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
 449         else fst (snd i)) (b x-a x) 〈a x ,x〉.
 450 #a #b #c #p #f #x normalize elim (b x-a x)
 451   [normalize //
 452   |#i #Hind >prim_rec_S
 453    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 454    cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
 455     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 456   ]
 457 qed.
 458
 459 (* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
 460 alias symbol "pair" (instance 15) = "abstract pair".
 461 alias symbol "minus" (instance 14) = "natural minus".
 462 alias symbol "minus" (instance 11) = "natural minus".
 463 alias symbol "pair" (instance 10) = "abstract pair".
 464 alias symbol "minus" (instance 13) = "natural minus".
 465 alias symbol "pair" (instance 12) = "abstract pair".
 466 alias symbol "minus" (instance 8) = "natural minus".
 467 alias symbol "pair" (instance 7) = "abstract pair".
 468 alias symbol "pair" (instance 6) = "abstract pair".
 469 alias symbol "minus" (instance 4) = "natural minus".
 470 alias symbol "pair" (instance 3) = "abstract pair".
 471 alias symbol "minus" (instance 2) = "natural minus".
 472 lemma bigop_prim_rec_dec: ∀a,b,c,p,f,x.
 473   bigop (b x-a x) (λi:ℕ.p 〈b x -i,x〉) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈b x-i,x〉) =
 474     prim_rec c
 475     (λi.if p 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉
 476         then plus (f 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉) (fst (snd i))
 477         else fst (snd i)) (b x-a x) 〈b x ,x〉.
 478 #a #b #c #p #f #x normalize elim (b x-a x)
 479   [normalize //
 480   |#i #Hind >prim_rec_S
 481    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 482    cases (true_or_false (p 〈b x - i,x〉)) #Hcase >Hcase
 483     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 484   ]
 485 qed.
 486
 487 lemma bigop_prim_rec_dec1: ∀a,b,c,p,f,x.
 488   bigop (S(b x)-a x) (λi:ℕ.p 〈b x - i,x〉) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈b x- i,x〉) =
 489     prim_rec c
 490     (λi.if p 〈fst (snd (snd i)) - (fst i),snd (snd (snd i))〉
 491         then plus (f 〈fst (snd (snd i)) - (fst i),snd (snd (snd i))〉) (fst (snd i))
 492         else fst (snd i)) (S(b x)-a x) 〈b x,x〉.
 493 #a #b #c #p #f #x elim (S(b x)-a x)
 494   [normalize //
 495   |#i #Hind >prim_rec_S
 496    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 497    cases (true_or_false (p 〈b x - i,x〉)) #Hcase >Hcase
 498     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 499   ]
 500 qed.
 501
 502 (*
 503 lemma bigop_aux_1: ∀k,c,f.
 504   bigop (S k) (λi:ℕ.true) ? c plus (λi:ℕ.f i) =
 505     f 0 + bigop k (λi:ℕ.true) ? c plus (λi:ℕ.f (S i)).
 506 #k #c #f elim k [normalize //] #i #Hind >bigop_Strue //
 507
 508 lemma bigop_prim_rec_dec: ∀a,b,c,f,x.
 509   bigop (b x-a x) (λi:ℕ.true) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈i+a x,x〉) =
 510     prim_rec c
 511     (λi. plus (f 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉) (fst (snd i)))
 512     (b x-a x) 〈b x ,x〉.
 513 #a #b #c #f #x normalize elim (b x-a x)
 514   [normalize //
 515   |#i #Hind >prim_rec_S
 516    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 517    <Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 518   ]
 519 qed. *)
 520
 521 lemma bigop_plus_c: ∀k,p,f,c.
 522   c k + bigop k (λi.p i) ? 0 plus (λi.f i) =
 523     bigop k (λi.p i) ? (c k) plus (λi.f i).
 524 #k #p #f elim k [normalize //]
 525 #i #Hind #c cases (true_or_false (p i)) #Hcase
 526 [>bigop_Strue // >bigop_Strue // <associative_plus >(commutative_plus ? (f i))
 527  >associative_plus @eq_f @Hind
 528 |>bigop_Sfalse // >bigop_Sfalse //
 529 ]
 530 qed.
 531
 532 (* the argument is 〈b-a,〈a,x〉〉 *)
 533
 534 (* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
 535 alias symbol "plus" (instance 3) = "natural plus".
 536 alias symbol "pair" (instance 2) = "abstract pair".
 537 alias id "max" = "cic:/matita/arithmetics/nat/max#def:2".
 538 alias symbol "plus" (instance 5) = "natural plus".
 539 alias symbol "pair" (instance 4) = "abstract pair".
 540 definition max_unary_pr ≝ λp,f.unary_pr (λx.0)
 541     (λi.
 542       let k ≝ fst i in
 543       let r ≝ fst (snd i) in
 544       let a ≝ fst (snd (snd i)) in
 545       let x ≝ snd (snd (snd i)) in
 546       if p 〈k + a,x〉 then max (f 〈k+a,x〉) r else r).
 547
 548 lemma max_unary_pr1: ∀a,b,p,f,x.
 549   max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
 550     ((max_unary_pr p f) ∘ (λx.〈b x - a x,〈a x,x〉〉)) x.
 551 #a #b #p #f #x normalize >fst_pair >snd_pair @max_prim_rec1
 552 qed.
 553
 554 (*
 555 lemma max_unary_pr: ∀a,b,p,f,x.
 556   max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) =
 557     prim_rec (λi.0)
 558     (λi.if p 〈fst i +a,x〉 then max (f 〈fst i +a ,snd (snd i)〉) (fst (snd i)) else fst (snd i)) (b-a) x.
 559 *)
 560
 561 (*
 562 definition unary_compl ≝ λp,f,hf.
 563   unary_pr MSC
 564    (λx:ℕ
 565     .fst (snd x)
 566      +hf
 567       〈fst x,
 568       〈unary_pr (λx0:ℕ.O)
 569        (λi:ℕ
 570         .(let (k:ℕ) ≝fst i in
 571           let (r:ℕ) ≝fst (snd i) in
 572           let (a:ℕ) ≝fst (snd (snd i)) in
 573           let (x:ℕ) ≝snd (snd (snd i)) in
 574           if p 〈k+a,x〉 then max (f 〈k+a,x〉) r else r )) 〈fst x,snd (snd x)〉,
 575       snd (snd x)〉〉). *)
 576
 577 (* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
 578 alias symbol "plus" (instance 6) = "natural plus".
 579 alias symbol "pair" (instance 5) = "abstract pair".
 580 alias symbol "plus" (instance 4) = "natural plus".
 581 alias symbol "pair" (instance 3) = "abstract pair".
 582 alias symbol "plus" (instance 2) = "natural plus".
 583 alias symbol "plus" (instance 1) = "natural plus".
 584 definition aux_compl ≝ λhp,hf.λi.
 585   let k ≝ fst i in
 586   let r ≝ fst (snd i) in
 587   let a ≝ fst (snd (snd i)) in
 588   let x ≝ snd (snd (snd i)) in
 589   hp 〈k+a,x〉 + hf 〈k+a,x〉 + (* was MSC r*) MSC i .
 590
 591 definition aux_compl1 ≝ λhp,hf.λi.
 592   let k ≝ fst i in
 593   let r ≝ fst (snd i) in
 594   let a ≝ fst (snd (snd i)) in
 595   let x ≝ snd (snd (snd i)) in
 596   hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
 597
 598 lemma aux_compl1_def: ∀k,r,m,hp,hf.
 599   aux_compl1 hp hf 〈k,〈r,m〉〉 =
 600   let a ≝ fst m in
 601   let x ≝ snd m in
 602   hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
 603 #k #r #m #hp #hf normalize >fst_pair >snd_pair >snd_pair >fst_pair //
 604 qed.
 605
 606 lemma aux_compl1_def1: ∀k,r,a,x,hp,hf.
 607   aux_compl1 hp hf 〈k,〈r,〈a,x〉〉〉 = hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
 608 #k #r #a #x #hp #hf normalize >fst_pair >snd_pair >snd_pair >fst_pair
 609 >fst_pair >snd_pair //
 610 qed.
 611
 612
 613 axiom Oaux_compl: ∀hp,hf. O (aux_compl1 hp hf) (aux_compl hp hf).
 614
 615 (*
 616 definition IF ≝ λb,f,g:nat →option nat. λx.
 617   match b x with
 618   [None ⇒ None ?
 619   |Some n ⇒ if (eqb n 0) then f x else g x].
 620 *)
 621
 622 axiom CF_if: ∀b:nat → bool. ∀f,g,s. CF s b → CF s f → CF s g →
 623   CF s (λx. if b x then f x else g x).
 624
 625 (*
 626 lemma IF_CF: ∀b,f,g,sb,sf,sg. CF sb b → CF sf f → CF sg g →
 627   CF (λn. sb n + sf n + sg n) (IF b f g).
 628 #b #f #g #sb #sf #sg #Hb #Hf #Hg @IF_CF_new
 629   [@(monotonic_CF … Hb) @O_plus_l @O_plus_l //
 630   |@(monotonic_CF … Hf) @O_plus_l @O_plus_r //
 631   |@(monotonic_CF … Hg) @O_plus_r //
 632   ]
 633 qed.
 634 *)
 635
 636 axiom CF_le: ∀h,f,g. CF h f → CF h g → CF h (λx. leb (f x) (g x)).
 637 axiom CF_max1: ∀h,f,g. CF h f → CF h g → CF h (λx. max (f x) (g x)).
 638 axiom CF_plus: ∀h,f,g. CF h f → CF h g → CF h (λx. f x + g x).
 639 axiom CF_minus: ∀h,f,g. CF h f → CF h g → CF h (λx. f x - g x).
 640
 641 axiom MSC_prop: ∀f,h. CF h f → ∀x. MSC (f x) ≤ h x.
 642
 643 lemma MSC_max: ∀f,h,x. CF h f → MSC (max_{i < x}(f i)) ≤ max_{i < x}(h i).
 644 #f #h #x #hf elim x // #i #Hind >bigop_Strue [|//] >bigop_Strue [|//]
 645 whd in match (max ??);
 646 cases (true_or_false (leb (f i) (bigop i (λi0:ℕ.true) ? 0 max(λi0:ℕ.f i0))))
 647 #Hcase >Hcase
 648   [@(transitive_le … Hind) @le_maxr //
 649   |@(transitive_le … (MSC_prop … hf i)) @le_maxl //
 650   ]
 651 qed.
 652
 653 lemma CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
 654   CF ha a → CF hb b → CF hp p → CF hf f →
 655   O s (λx.ha x + hb x +
 656        (∑_{i ∈[a x ,b x[ }
 657          (hp 〈i,x〉 + hf 〈i,x〉 + max_{i ∈ [a x, b x [ }(hf 〈i,x〉)))) →
 658   CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
 659 #a #b #p #f #ha #hb #hp #hf #s #CFa #CFb #CFp #CFf #HO
 660 @ext_CF1 [|#x @max_unary_pr1]
 661 @(CF_comp ??? (λx.ha x + hb x))
 662   [|@CF_comp_pair
 663     [@CF_minus [@(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
 664     |@CF_comp_pair
 665       [@(O_to_CF … CFa) @O_plus_l //
 666       | @(O_to_CF … CF_id) @O_plus_r @(proj1 … CFb)
 667       ]
 668     ]
 669   |@(CF_prim_rec … MSC … (aux_compl1 hp hf))
 670      [@CF_const
 671      |@(O_to_CF … (Oaux_compl … ))
 672       @CF_if
 673        [@(CF_comp p … MSC … CFp)
 674          [@CF_comp_pair
 675            [@CF_plus [@CF_fst| @CF_comp_fst @CF_comp_snd @CF_snd]
 676            |@CF_comp_snd @CF_comp_snd @CF_snd]
 677          |@le_to_O #x normalize >commutative_plus >associative_plus @le_plus //
 678          ]
 679        |@CF_max1
 680          [@(CF_comp f … MSC … CFf)
 681            [@CF_comp_pair
 682              [@CF_plus [@CF_fst| @CF_comp_fst @CF_comp_snd @CF_snd]
 683              |@CF_comp_snd @CF_comp_snd @CF_snd]
 684            |@le_to_O #x normalize >commutative_plus //
 685            ]
 686          |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
 687          ]
 688        |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
 689        ]
 690      |@O_refl
 691      ]
 692   |@(O_trans … HO) -HO
 693    @(O_trans ? (λx:ℕ
 694    .ha x+hb x
 695     +bigop (b x-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus
 696      (λi:ℕ
 697       .(λi0:ℕ
 698         .hp 〈i0,x〉+hf 〈i0,x〉
 699          +bigop (b x-a x) (λi1:ℕ.true) ? 0 max
 700           (λi1:ℕ.(λi2:ℕ.hf 〈i2,x〉) (i1+a x))) (i+a x))))
 701     [
 702    @le_to_O #n @le_plus // whd in match (unary_pr ???);
 703    >fst_pair >snd_pair >bigop_prim_rec elim (b n - a n)
 704     [normalize //
 705     |#x #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >aux_compl1_def1
 706      >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >fst_pair
 707      >snd_pair normalize in ⊢ (??%); >commutative_plus @le_plus
 708       [-Hind @le_plus // normalize >fst_pair >snd_pair
 709        @(transitive_le ? (bigop x (λi1:ℕ.true) ? 0 (λn0:ℕ.λm:ℕ.if leb n0 m then m else n0 )
 710          (λi1:ℕ.hf 〈i1+a n,n〉)))
 711         [elim x [normalize @MSC_le]
 712          #x0 #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >snd_pair
 713          >fst_pair >fst_pair cases (p 〈x0+a n,n〉) normalize
 714           [cases (true_or_false (leb (f 〈x0+a n,n〉)
 715             (prim_rec (λx00:ℕ.O)
 716              (λi:ℕ
 717             .if p 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
 718              then if leb (f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉)
 719                            (fst (snd i))
 720                       then fst (snd i)
 721                       else f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
 722              else fst (snd i) ) x0 〈a n,n〉))) #Hcase >Hcase normalize
 723            [@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
 724            |@(transitive_le … (MSC_prop … CFf …)) @(le_maxl … (le_n …))
 725            ]
 726          |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
 727          ]
 728        |@(le_maxr … (le_n …))
 729        ]
 730      |@(transitive_le … Hind) -Hind
 731       generalize in match (bigop x (λi:ℕ.true) ? 0 max
 732               (λi1:ℕ.(λi2:ℕ.hf 〈i2,n〉) (i1+a n))); #c
 733       generalize in match (hf 〈x+a n,n〉); #c1
 734       elim x [//] #x0 #Hind
 735       >prim_rec_S >prim_rec_S normalize >fst_pair >fst_pair >snd_pair
 736       >snd_pair >snd_pair >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair
 737       >fst_pair @le_plus
 738        [@le_plus // cases (true_or_false (leb c1 c)) #Hcase
 739         >Hcase normalize // @lt_to_le @not_le_to_lt @(leb_false_to_not_le ?? Hcase)
 740        |@Hind
 741        ]
 742      ]
 743    ]
 744  |@O_plus [@O_plus_l //] @le_to_O #x
 745   <bigop_plus_c @le_plus // @(transitive_le … (MSC_pair …)) @le_plus
 746    [@MSC_prop @CFa | @MSC_prop @(O_to_CF MSC … (CF_const x)) @(proj1 … CFb)]
 747  ]
 748 qed.
 749
 750 (* old
 751 axiom CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
 752   CF ha a → CF hb b → CF hp p → CF hf f →
 753   O s (λx.ha x + hb x + ∑_{i ∈[a x ,b x[ }(hp 〈i,x〉 + hf 〈i,x〉)) →
 754   CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)). *)
 755
 756 (******************************** minimization ********************************)
 757
 758 alias symbol "plus" (instance 2) = "natural plus".
 759 alias symbol "plus" (instance 5) = "natural plus".
 760 alias symbol "plus" (instance 1) = "natural plus".
 761 alias symbol "plus" (instance 4) = "natural plus".
 762 alias symbol "pair" (instance 3) = "abstract pair".
 763 alias id "O" = "cic:/matita/arithmetics/nat/nat#con:0:1:0".
 764 let rec my_minim a f x k on k ≝
 765   match k with
 766   [O ⇒ a
 767   |S p ⇒ if eqb (my_minim a f x p) (a+p)
 768          then if f 〈a+p,x〉 then a+p else S(a+p)
 769          else (my_minim a f x p) ].
 770
 771 lemma my_minim_S : ∀a,f,x,k.
 772   my_minim a f x (S k) =
 773     if eqb (my_minim a f x k) (a+k)
 774     then if f 〈a+k,x〉 then a+k else S(a+k)
 775     else (my_minim a f x k) .
 776 // qed.
 777
 778 lemma my_minim_fa : ∀a,f,x,k. f〈a,x〉 = true → my_minim a f x k = a.
 779 #a #f #x #k #H elim k // #i #Hind normalize >Hind
 780 cases (true_or_false (eqb a (a+i))) #Hcase >Hcase normalize //
 781 <(eqb_true_to_eq … Hcase) >H //
 782 qed.
 783
 784 lemma my_minim_nfa : ∀a,f,x,k. f〈a,x〉 = false →
 785 my_minim a f x (S k) = my_minim (S a) f x k.
 786 #a #f #x #k #H elim k
 787   [normalize <plus_n_O >H >eq_to_eqb_true //
 788   |#i #Hind >my_minim_S >Hind >my_minim_S <plus_n_Sm //
 789   ]
 790 qed.
 791
 792 lemma my_min_eq : ∀a,f,x,k.
 793   min k a (λi.f 〈i,x〉) = my_minim a f x k.
 794 #a #f #x #k lapply a -a elim k // #i #Hind #a normalize in ⊢ (??%?);
 795 cases (true_or_false (f 〈a,x〉)) #Hcase >Hcase
 796   [>(my_minim_fa … Hcase) // | >Hind @sym_eq @(my_minim_nfa … Hcase) ]
 797 qed.
 798
 799 (* cambiare qui: togliere S *)
 800
 801 (* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
 802 alias symbol "minus" (instance 1) = "natural minus".
 803 alias symbol "minus" (instance 3) = "natural minus".
 804 alias symbol "pair" (instance 2) = "abstract pair".
 805 definition minim_unary_pr ≝ λf.unary_pr (λx.S(fst x))
 806     (λi.
 807       let k ≝ fst i in
 808       let r ≝ fst (snd i) in
 809       let b ≝ fst (snd (snd i)) in
 810       let x ≝ snd (snd (snd i)) in
 811       if f 〈b-k,x〉 then b-k else r).
 812
 813 definition compl_minim_unary ≝ λhf:nat → nat.λi.
 814       let k ≝ fst i in
 815       let b ≝ fst (snd (snd i)) in
 816       let x ≝ snd (snd (snd i)) in
 817       hf 〈b-k,x〉 + MSC 〈k,〈S b,x〉〉.
 818
 819 definition compl_minim_unary_aux ≝ λhf,i.
 820       let k ≝ fst i in
 821       let r ≝ fst (snd i) in
 822       let b ≝ fst (snd (snd i)) in
 823       let x ≝ snd (snd (snd i)) in
 824       hf 〈b-k,x〉 + MSC i.
 825
 826 lemma compl_minim_unary_aux_def : ∀hf,k,r,b,x.
 827   compl_minim_unary_aux hf 〈k,〈r,〈b,x〉〉〉 = hf 〈b-k,x〉 + MSC 〈k,〈r,〈b,x〉〉〉.
 828 #hf #k #r #b #x normalize >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair //
 829 qed.
 830
 831 lemma compl_minim_unary_def : ∀hf,k,r,b,x.
 832   compl_minim_unary hf 〈k,〈r,〈b,x〉〉〉 = hf 〈b-k,x〉 + MSC 〈k,〈S b,x〉〉.
 833 #hf #k #r #b #x normalize >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair //
 834 qed.
 835
 836 lemma compl_minim_unary_aux_def2 : ∀hf,k,r,x.
 837   compl_minim_unary_aux hf 〈k,〈r,x〉〉 = hf 〈fst x-k,snd x〉 + MSC 〈k,〈r,x〉〉.
 838 #hf #k #r #x normalize >snd_pair >snd_pair >fst_pair //
 839 qed.
 840
 841 lemma compl_minim_unary_def2 : ∀hf,k,r,x.
 842   compl_minim_unary hf 〈k,〈r,x〉〉 = hf 〈fst x-k,snd x〉 + MSC 〈k,〈S(fst x),snd x〉〉.
 843 #hf #k #r #x normalize >snd_pair >snd_pair >fst_pair //
 844 qed.
 845
 846 lemma min_aux: ∀a,f,x,k. min (S k) (a x) (λi:ℕ.f 〈i,x〉) =
 847   ((minim_unary_pr f) ∘ (λx.〈S k,〈a x + k,x〉〉)) x.
 848 #a #f #x #k whd in ⊢ (???%); >fst_pair >snd_pair
 849 lapply a -a (* @max_prim_rec1 *)
 850 elim k
 851   [normalize #a >fst_pair >snd_pair >fst_pair >snd_pair >snd_pair >fst_pair
 852    <plus_n_O <minus_n_O >fst_pair //
 853   |#i #Hind #a normalize in ⊢ (??%?); >prim_rec_S >fst_pair >snd_pair
 854    >fst_pair >snd_pair >snd_pair >fst_pair <plus_n_Sm <(Hind (λx.S (a x)))
 855    whd in ⊢ (???%); >minus_S_S <(minus_plus_m_m (a x) i) //
 856 qed.
 857
 858 lemma minim_unary_pr1: ∀a,b,f,x.
 859   μ_{i ∈[a x,b x]}(f 〈i,x〉) =
 860     if leb (a x) (b x) then ((minim_unary_pr f) ∘ (λx.〈S (b x) - a x,〈b x,x〉〉)) x
 861     else (a x).
 862 #a #b #f #x cases (true_or_false (leb (a x) (b x))) #Hcase >Hcase
 863   [cut (b x = a x + (b x - a x))
 864     [>commutative_plus <plus_minus_m_m // @leb_true_to_le // ]
 865    #Hcut whd in ⊢ (???%); >minus_Sn_m [|@leb_true_to_le //]
 866    >min_aux whd in ⊢ (??%?); <Hcut //
 867   |>eq_minus_O // @not_le_to_lt @leb_false_to_not_le //
 868   ]
 869 qed.
 870
 871 axiom sum_inv: ∀a,b,f.∑_{i ∈ [a,S b[ }(f i) = ∑_{i ∈ [a,S b[ }(f (a + b - i)).
 872
 873 (*
 874 #a #b #f @(bigop_iso … plusAC) whd %{(λi.b - a - i)} %{(λi.b - a -i)} %
 875   [%[#i #lti #_ normalize @eq_f >commutative_plus <plus_minus_associative
 876     [2: @le_minus_to_plus_r //
 877      [// @eq_f @@sym_eq @plus_to_minus
 878     |#i #Hi #_ % [% [@le_S_S
 879 *)
 880
 881 example sum_inv_check : ∑_{i ∈ [3,6[ }(i*i) = ∑_{i ∈ [3,6[ }((8-i)*(8-i)).
 882 normalize // qed.
 883
 884 (* provo rovesciando la somma *)
 885
 886 axiom daemon: ∀P:Prop.P.
 887
 888 lemma CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
 889   CF sa a → CF sb b → CF sf f →
 890   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉 + MSC 〈b x - i,〈S(b x),x〉〉)) →
 891   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
 892 #a #b #f #ha #hb #hf #s #CFa #CFb #CFf #HO
 893 @ext_CF1 [|#x @minim_unary_pr1]
 894 @CF_if
 895   [@CF_le @(O_to_CF … HO)
 896     [@(O_to_CF … CFa) @O_plus_l @O_plus_l  @O_refl
 897     |@(O_to_CF … CFb) @O_plus_l @O_plus_r @O_refl
 898     ]
 899   |@(CF_comp ??? (λx.ha x + hb x))
 900     [|@CF_comp_pair
 901       [@CF_minus [@CF_compS @(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
 902       |@CF_comp_pair
 903         [@(O_to_CF … CFb) @O_plus_r //
 904         |@(O_to_CF … CF_id) @O_plus_r @(proj1 … CFb)
 905         ]
 906       ]
 907     |@(CF_prim_rec_gen … MSC … (compl_minim_unary_aux hf))
 908       [@((λx:ℕ.fst (snd x)
 909           +compl_minim_unary hf
 910           〈fst x,
 911           〈unary_pr fst
 912             (λi:ℕ
 913              .(let (k:ℕ) ≝fst i in
 914                let (r:ℕ) ≝fst (snd i) in
 915                let (b:ℕ) ≝fst (snd (snd i)) in
 916                let (x:ℕ) ≝snd (snd (snd i)) in if f 〈b-S k,x〉 then b-S k else r ))
 917           〈fst x,snd (snd x)〉,
 918           snd (snd x)〉〉))
 919       |@CF_compS @CF_fst
 920       |@CF_if
 921         [@(CF_comp f … MSC … CFf)
 922           [@CF_comp_pair
 923             [@CF_minus [@CF_comp_fst @CF_comp_snd @CF_snd|@CF_fst]
 924             |@CF_comp_snd @CF_comp_snd @CF_snd]
 925           |@le_to_O #x normalize >commutative_plus //
 926           ]
 927         |@(O_to_CF … MSC)
 928           [@le_to_O #x normalize //
 929           |@CF_minus
 930             [@CF_comp_fst @CF_comp_snd @CF_snd |@CF_fst]
 931           ]
 932         |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
 933         ]
 934       |@O_plus
 935         [@O_plus_l @O_refl
 936         |@O_plus_r @O_ext2 [||#x >compl_minim_unary_aux_def2 @refl]
 937          @O_trans [||@le_to_O #x >compl_minim_unary_def2 @le_n]
 938          @O_plus [@O_plus_l //]
 939          @O_plus_r
 940          @O_trans [|@le_to_O #x @MSC_pair] @O_plus
 941            [@le_to_O #x @monotonic_MSC @(transitive_le ???? (le_fst …))
 942             >fst_pair @le_n]
 943          @O_trans [|@le_to_O #x @MSC_pair] @O_plus
 944            [@le_to_O #x @monotonic_MSC @(transitive_le ???? (le_snd …))
 945             >snd_pair @(transitive_le ???? (le_fst …)) >fst_pair
 946             normalize >snd_pair >fst_pair lapply (surj_pair x)
 947             * #x1 * #x2 #Hx >Hx >fst_pair >snd_pair elim x1 //
 948             #i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
 949             cases (f ?) [@le_S // | //]]
 950          @le_to_O #x @monotonic_MSC @(transitive_le ???? (le_snd …)) >snd_pair
 951          >(expand_pair (snd (snd x))) in ⊢ (?%?); @le_pair //
 952         ]
 953       ]
 954     |cut (O s (λx.ha x + hb x +
 955             ∑_{i ∈[a x ,S(b x)[ }(hf 〈a x+b x-i,x〉 + MSC 〈b x -(a x+b x-i),〈S(b x),x〉〉)))
 956       [@(O_ext2 … HO) #x @eq_f @sum_inv] -HO #HO
 957      @(O_trans … HO) -HO
 958      @(O_trans ? (λx:ℕ.ha x+hb x
 959        +bigop (S(b x)-a x) (λi:ℕ.true) ?
 960         (MSC 〈b x,x〉) plus (λi:ℕ.(λj.hf j + MSC 〈b x - fst j,〈S(b (snd j)),snd j〉〉) 〈b x- i,x〉)))
 961       [@le_to_O #n @le_plus // whd in match (unary_pr ???);
 962        >fst_pair >snd_pair >(bigop_prim_rec_dec1 a b ? (λi.true))
 963         (* it is crucial to recall that the index is bound by S(b x) *)
 964         cut (S (b n) - a n ≤ S (b n)) [//]
 965         elim (S(b n) - a n)
 966         [normalize //
 967         |#x #Hind #lex >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair
 968          >compl_minim_unary_def >prim_rec_S >fst_pair >snd_pair >fst_pair
 969          >snd_pair >fst_pair >snd_pair >fst_pair whd in ⊢ (??%); >commutative_plus
 970          @le_plus [2:@Hind @le_S @le_S_S_to_le @lex] -Hind >snd_pair
 971          >minus_minus_associative // @le_S_S_to_le //
 972         ]
 973       |@O_plus [@O_plus_l //] @O_ext2 [||#x @bigop_plus_c]
 974        @O_plus
 975         [@O_plus_l @O_trans [|@le_to_O #x @MSC_pair]
 976          @O_plus [@O_plus_r @le_to_O @(MSC_prop … CFb)|@O_plus_r @(proj1 … CFb)]
 977         |@O_plus_r @(O_ext2 … (O_refl …)) #x @same_bigop
 978           [//|#i #H #_ @eq_f2 [@eq_f @eq_f2 //|>fst_pair @eq_f @eq_f2  //]
 979         ]
 980       ]
 981     ]
 982   ]
 983   |@(O_to_CF … CFa) @(O_trans … HO) @O_plus_l @O_plus_l @O_refl
 984   ]
 985 qed.
 986
 987 (*
 988 lemma CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
 989   CF sa a → CF sb b → CF sf f →
 990   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
 991   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
 992 #a #b #f #ha #hb #hf #s #CFa #CFb #CFf #HO
 993 @ext_CF1 [|#x @minim_unary_pr1]
 994 @(CF_comp ??? (λx.ha x + hb x))
 995   [|@CF_comp_pair
 996     [@CF_minus [@CF_compS @(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
 997     |@CF_comp_pair
 998       [@CF_max1 [@(O_to_CF … CFa) @O_plus_l // | @CF_compS @(O_to_CF … CFb) @O_plus_r //]
 999       | @(O_to_CF … CF_id) @O_plus_r @(proj1 … CFb)
1000       ]
1001     ]
1002   |@(CF_prim_rec … MSC … (compl_minim_unary_aux hf))
1003     [@CF_fst
1004     |@CF_if
1005       [@(CF_comp f … MSC … CFf)
1006         [@CF_comp_pair
1007           [@CF_minus [@CF_comp_fst @CF_comp_snd @CF_snd|@CF_compS @CF_fst]
1008           |@CF_comp_snd @CF_comp_snd @CF_snd]
1009         |@le_to_O #x normalize >commutative_plus //
1010         ]
1011       |@(O_to_CF … MSC)
1012         [@le_to_O #x normalize //
1013         |@CF_minus
1014           [@CF_comp_fst @CF_comp_snd @CF_snd |@CF_compS @CF_fst]
1015         ]
1016       |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
1017       ]
1018     |@O_refl
1019     ]
1020   |@(O_trans … HO) -HO
1021    @(O_trans ? (λx:ℕ
1022    .ha x+hb x
1023     +bigop (S(b x)-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus (λi:ℕ.hf 〈i+a x,x〉)))
1024   [@le_to_O #n @le_plus // whd in match (unary_pr ???);
1025    >fst_pair >snd_pair >(bigop_prim_rec ? (λn.S(b n)) ? (λi.true)) elim (S(b n) - a n)
1026     [normalize @monotonic_MSC @le_pair
1027     |#x #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >compl_minim_unary_def
1028      >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >fst_pair
1029      >snd_pair normalize in ⊢ (??%); >commutative_plus @le_plus
1030       [-Hind @le_plus // normalize >fst_pair >snd_pair
1031        @(transitive_le ? (bigop x (λi1:ℕ.true) ? 0 (λn0:ℕ.λm:ℕ.if leb n0 m then m else n0 )
1032          (λi1:ℕ.hf 〈i1+a n,n〉)))
1033         [elim x [normalize @MSC_le]
1034          #x0 #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >snd_pair
1035          >fst_pair >fst_pair cases (p 〈x0+a n,n〉) normalize
1036           [cases (true_or_false (leb (f 〈x0+a n,n〉)
1037             (prim_rec (λx00:ℕ.O)
1038              (λi:ℕ
1039             .if p 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
1040              then if leb (f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉)
1041                            (fst (snd i))
1042                       then fst (snd i)
1043                       else f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
1044              else fst (snd i) ) x0 〈a n,n〉))) #Hcase >Hcase normalize
1045            [@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
1046            |@(transitive_le … (MSC_prop … CFf …)) @(le_maxl … (le_n …))
1047            ]
1048          |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
1049          ]
1050        |@(le_maxr … (le_n …))
1051        ]
1052
1053
1054    @(O_trans ? (λx:ℕ
1055    .ha x+hb x
1056     +bigop (b x-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus
1057      (λi:ℕ
1058       .(λi0:ℕ
1059         .hp 〈i0,x〉+hf 〈i0,x〉
1060          +bigop (b x-a x) (λi1:ℕ.true) ? 0 max
1061           (λi1:ℕ.(λi2:ℕ.hf 〈i2,x〉) (i1+a x))) (i+a x))))
1062     [
1063    @le_to_O #n @le_plus // whd in match (unary_pr ???);
1064    >fst_pair >snd_pair >bigop_prim_rec elim (b n - a n)
1065     [normalize //
1066     |#x #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >aux_compl1_def1
1067      >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >fst_pair
1068      >snd_pair normalize in ⊢ (??%); >commutative_plus @le_plus
1069       [-Hind @le_plus // normalize >fst_pair >snd_pair
1070        @(transitive_le ? (bigop x (λi1:ℕ.true) ? 0 (λn0:ℕ.λm:ℕ.if leb n0 m then m else n0 )
1071          (λi1:ℕ.hf 〈i1+a n,n〉)))
1072         [elim x [normalize @MSC_le]
1073          #x0 #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >snd_pair
1074          >fst_pair >fst_pair cases (p 〈x0+a n,n〉) normalize
1075           [cases (true_or_false (leb (f 〈x0+a n,n〉)
1076             (prim_rec (λx00:ℕ.O)
1077              (λi:ℕ
1078             .if p 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
1079              then if leb (f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉)
1080                            (fst (snd i))
1081                       then fst (snd i)
1082                       else f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
1083              else fst (snd i) ) x0 〈a n,n〉))) #Hcase >Hcase normalize
1084            [@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
1085            |@(transitive_le … (MSC_prop … CFf …)) @(le_maxl … (le_n …))
1086            ]
1087          |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
1088          ]
1089        |@(le_maxr … (le_n …))
1090        ]
1091      |@(transitive_le … Hind) -Hind
1092       generalize in match (bigop x (λi:ℕ.true) ? 0 max
1093               (λi1:ℕ.(λi2:ℕ.hf 〈i2,n〉) (i1+a n))); #c
1094       generalize in match (hf 〈x+a n,n〉); #c1
1095       elim x [//] #x0 #Hind
1096       >prim_rec_S >prim_rec_S normalize >fst_pair >fst_pair >snd_pair
1097       >snd_pair >snd_pair >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair
1098       >fst_pair @le_plus
1099        [@le_plus // cases (true_or_false (leb c1 c)) #Hcase
1100         >Hcase normalize // @lt_to_le @not_le_to_lt @(leb_false_to_not_le ?? Hcase)
1101        |@Hind
1102        ]
1103      ]
1104    ]
1105  |@O_plus [@O_plus_l //] @le_to_O #x
1106   <bigop_plus_c @le_plus // @(transitive_le … (MSC_pair …)) @le_plus
1107    [@MSC_prop @CFa | @MSC_prop @(O_to_CF MSC … (CF_const x)) @(proj1 … CFb)]
1108  ]
1109 qed.
1110
1111 axiom CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
1112   CF sa a → CF sb b → CF sf f →
1113   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
1114   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).*)
1115
1116 (************************************* smn ************************************)
1117 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
1118
1119 (****************************** constructibility ******************************)
1120
1121 definition constructible ≝ λs. CF s s.
1122
1123 lemma constr_comp : ∀s1,s2. constructible s1 → constructible s2 →
1124   (∀x. x ≤ s2 x) → constructible (s2 ∘ s1).
1125 #s1 #s2 #Hs1 #Hs2 #Hle @(CF_comp … Hs1 Hs2) @O_plus @le_to_O #x [@Hle | //]
1126 qed.
1127
1128 lemma ext_constr: ∀s1,s2. (∀x.s1 x = s2 x) →
1129   constructible s1 → constructible s2.
1130 #s1 #s2 #Hext #Hs1 @(ext_CF … Hext) @(monotonic_CF … Hs1)  #x >Hext //
1131 qed.
1132
1133 lemma constr_prim_rec: ∀s1,s2. constructible s1 → constructible s2 →
1134   (∀n,r,m. 2 * r ≤ s2 〈n,〈r,m〉〉) → constructible (unary_pr s1 s2).
1135 #s1 #s2 #Hs1 #Hs2 #Hincr @(CF_prim_rec … Hs1 Hs2) whd %{2} %{0}
1136 #x #_ lapply (surj_pair x) * #a * #b #eqx >eqx whd in match (unary_pr ???);
1137 >fst_pair >snd_pair
1138 whd in match (unary_pr ???); >fst_pair >snd_pair elim a
1139   [normalize //
1140   |#n #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair
1141    >prim_rec_S @transitive_le [| @(monotonic_le_plus_l … Hind)]
1142    @transitive_le [| @(monotonic_le_plus_l … (Hincr n ? b))]
1143    whd in match (unary_pr ???); >fst_pair >snd_pair //
1144   ]
1145 qed.
1146
1147 (********************************* simulation *********************************)
1148
1149 axiom sU : nat → nat.
1150
1151 axiom monotonic_sU: ∀i1,i2,x1,x2,s1,s2. i1 ≤ i2 → x1 ≤ x2 → s1 ≤ s2 →
1152   sU 〈i1,〈x1,s1〉〉 ≤ sU 〈i2,〈x2,s2〉〉.
1153
1154 lemma monotonic_sU_aux : ∀x1,x2. fst x1 ≤ fst x2 → fst (snd x1) ≤ fst (snd x2) →
1155 snd (snd x1) ≤ snd (snd x2) → sU x1 ≤ sU x2.
1156 #x1 #x2 cases (surj_pair x1) #a1 * #y #eqx1 >eqx1 -eqx1 cases (surj_pair y)
1157 #b1 * #c1 #eqy >eqy -eqy
1158 cases (surj_pair x2) #a2 * #y2 #eqx2 >eqx2 -eqx2 cases (surj_pair y2)
1159 #b2 * #c2 #eqy2 >eqy2 -eqy2 >fst_pair >snd_pair >fst_pair >snd_pair
1160 >fst_pair >snd_pair >fst_pair >snd_pair @monotonic_sU
1161 qed.
1162
1163 axiom sU_le: ∀i,x,s. s ≤ sU 〈i,〈x,s〉〉.
1164 axiom sU_le_i: ∀i,x,s. MSC i ≤ sU 〈i,〈x,s〉〉.
1165 axiom sU_le_x: ∀i,x,s. MSC x ≤ sU 〈i,〈x,s〉〉.
1166
1167 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
1168
1169 axiom CF_U : CF sU pU_unary.
1170
1171 definition termb_unary ≝ λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)).
1172 definition out_unary ≝ λx:ℕ.out (fst x) (fst (snd x)) (snd (snd x)).
1173
1174 lemma CF_termb: CF sU termb_unary.
1175 @(ext_CF (fst ∘ pU_unary)) [2: @CF_comp_fst @CF_U]
1176 #n whd in ⊢ (??%?); whd in  ⊢ (??(?%)?); >fst_pair %
1177 qed.
1178
1179 lemma CF_out: CF sU out_unary.
1180 @(ext_CF (snd ∘ pU_unary)) [2: @CF_comp_snd @CF_U]
1181 #n whd in ⊢ (??%?); whd in  ⊢ (??(?%)?); >snd_pair %
1182 qed.
1183
1184
1185 (******************** complexity of g ********************)
1186
1187 (*definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
1188 definition auxg ≝
1189   λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
1190     (out i (snd ux) (h (S i) (snd ux))).
1191
1192 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
1193 #h #s #H1 @(CF_compS ? (auxg h) H1)
1194 qed.
1195
1196 definition aux1g ≝
1197   λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
1198     ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
1199
1200 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
1201 #h #x @same_bigop
1202   [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
1203 qed.
1204
1205 lemma compl_g2 : ∀h,s1,s2,s.
1206   CF s1
1207     (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
1208   CF s2
1209     (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
1210   O s (λx.MSC x + ∑_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
1211   CF s (auxg h).
1212 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
1213   [#n whd in ⊢ (??%%); @eq_aux]
1214 @(CF_max … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
1215 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
1216 qed.
1217
1218 lemma compl_g3 : ∀h,s.
1219   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
1220   CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
1221 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (proj1 … H))
1222 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
1223 qed.
1224
1225 definition min_input_aux ≝ λh,p.
1226   μ_{y ∈ [S (fst p),snd (snd p)] }
1227     ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
1228
1229 lemma min_input_eq : ∀h,p.
1230     min_input_aux h p  =
1231     min_input h (fst p) (snd (snd p)).
1232 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
1233 whd in ⊢ (??%%); >fst_pair >snd_pair //
1234 qed.
1235
1236 definition termb_aux ≝ λh.
1237   termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
1238
1239 lemma compl_g4 : ∀h,s1,s.
1240   (CF s1
1241     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
1242    (O s (λx.MSC x + ∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
1243   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
1244 #h #s1 #s #Hs1 #HO @(ext_CF (min_input_aux h))
1245  [#n whd in ⊢ (??%%); @min_input_eq]
1246 @(CF_mu … MSC MSC … Hs1)
1247   [@CF_compS @CF_fst
1248   |@CF_comp_snd @CF_snd
1249   |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
1250 qed.*)
1251
1252 (************************* a couple of technical lemmas ***********************)
1253 lemma minus_to_0: ∀a,b. a ≤ b → minus a b = 0.
1254 #a elim a // #n #Hind *
1255   [#H @False_ind /2 by absurd/ | #b normalize #H @Hind @le_S_S_to_le /2/]
1256 qed.
1257
1258 lemma sigma_bound:  ∀h,a,b. monotonic nat le h →
1259   ∑_{i ∈ [a,S b[ }(h i) ≤  (S b-a)*h b.
1260 #h #a #b #H cases (decidable_le a b)
1261   [#leab cut (b = pred (S b - a + a))
1262     [<plus_minus_m_m // @le_S //] #Hb >Hb in match (h b);
1263    generalize in match (S b -a);
1264    #n elim n
1265     [//
1266     |#m #Hind >bigop_Strue [2://] @le_plus
1267       [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
1268     ]
1269   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
1270    cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
1271   ]
1272 qed.
1273
1274 lemma sigma_bound_decr:  ∀h,a,b. (∀a1,a2. a1 ≤ a2 → a2 < b → h a2 ≤ h a1) →
1275   ∑_{i ∈ [a,b[ }(h i) ≤  (b-a)*h a.
1276 #h #a #b #H cases (decidable_le a b)
1277   [#leab cut ((b -a) +a ≤ b) [/2 by le_minus_to_plus_r/] generalize in match (b -a);
1278    #n elim n
1279     [//
1280     |#m #Hind >bigop_Strue [2://] #Hm
1281      cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
1282      @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
1283     ]
1284   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
1285    cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
1286   ]
1287 qed.
1288
1289 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
1290 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
1291   (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
1292 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
1293 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
1294 qed.
1295
1296 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
1297 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
1298 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
1299 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
1300 qed.
1301
1302 (**************************** end of technical lemmas *************************)
1303
1304 (*lemma compl_g5 : ∀h,s1.(∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
1305   (CF s1
1306     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
1307   CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
1308     (λp:ℕ.min_input h (fst p) (snd (snd p))).
1309 #h #s1 #Hmono #Hs1 @(compl_g4 … Hs1) @O_plus
1310 [@O_plus_l // |@O_plus_r @coroll @Hmono]
1311 qed.
1312
1313 lemma compl_g6: ∀h.
1314   constructible (λx. h (fst x) (snd x)) →
1315   (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
1316     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
1317 #h #hconstr @(ext_CF (termb_aux h))
1318   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
1319 @(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
1320   [@CF_comp_pair
1321     [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
1322     |@CF_comp_pair
1323       [@(monotonic_CF … CF_fst) #x //
1324       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
1325         [#n normalize >fst_pair >snd_pair %]
1326        @(CF_comp … MSC …hconstr)
1327         [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
1328         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
1329         ]
1330       ]
1331     ]
1332   |@O_plus
1333     [@O_plus
1334       [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
1335         [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
1336          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
1337          >distributive_times_plus @le_plus [//]
1338          cases (surj_pair b) #c * #d #eqb >eqb
1339          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
1340          whd in ⊢ (??%); @le_plus
1341           [@monotonic_MSC @(le_maxl … (le_n …))
1342           |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
1343           ]
1344         |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
1345         ]
1346       |@le_to_O #n @sU_le
1347       ]
1348     |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
1349   ]
1350 qed. *)
1351
1352 definition big : nat →nat ≝ λx.
1353   let m ≝ max (fst x) (snd x) in 〈m,m〉.
1354
1355 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
1356 #a #b normalize >fst_pair >snd_pair // qed.
1357
1358 lemma le_big : ∀x. x ≤ big x.
1359 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
1360 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
1361 qed.
1362
1363 definition faux2 ≝ λh.
1364   (λx.MSC x + (snd (snd x)-fst x)*
1365     (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
1366
1367 (*lemma compl_g7: ∀h.
1368   constructible (λx. h (fst x) (snd x)) →
1369   (∀n. monotonic ? le (h n)) →
1370   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))〉〉)
1371     (λp:ℕ.min_input h (fst p) (snd (snd p))).
1372 #h #hcostr #hmono @(monotonic_CF … (faux2 h))
1373   [#n normalize >fst_pair >snd_pair //]
1374 @compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
1375 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
1376 qed.
1377
1378 lemma compl_g71: ∀h.
1379   constructible (λx. h (fst x) (snd x)) →
1380   (∀n. monotonic ? le (h n)) →
1381   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))〉〉)
1382     (λp:ℕ.min_input h (fst p) (snd (snd p))).
1383 #h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x
1384 @le_plus [@monotonic_MSC //]
1385 cases (decidable_le (fst x) (snd(snd x)))
1386   [#Hle @le_times // @monotonic_sU
1387   |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
1388   ]
1389 qed.*)
1390
1391 definition out_aux ≝ λh.
1392   out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
1393
1394 lemma compl_g8: ∀h.
1395   constructible (λx. h (fst x) (snd x)) →
1396   (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
1397     (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
1398 #h #hconstr @(ext_CF (out_aux h))
1399   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
1400 @(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
1401   [@CF_comp_pair
1402     [@(monotonic_CF … CF_fst) #x //
1403     |@CF_comp_pair
1404       [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
1405       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
1406         [#n normalize >fst_pair >snd_pair %]
1407        @(CF_comp … MSC …hconstr)
1408         [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
1409         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
1410         ]
1411       ]
1412     ]
1413   |@O_plus
1414     [@O_plus
1415       [@le_to_O #n @sU_le
1416       |@(O_trans … (λx.MSC (max (fst x) (snd x))))
1417         [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
1418          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
1419          whd in ⊢ (??%); @le_plus
1420           [@monotonic_MSC @(le_maxl … (le_n …))
1421           |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
1422           ]
1423         |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
1424         ]
1425       ]
1426     |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
1427   ]
1428 qed.
1429
1430 (*lemma compl_g9 : ∀h.
1431   constructible (λx. h (fst x) (snd x)) →
1432   (∀n. monotonic ? le (h n)) →
1433   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
1434   CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
1435       (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
1436    (auxg h).
1437 #h #hconstr #hmono #hantimono
1438 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
1439 @O_plus
1440   [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
1441     [// | @monotonic_MSC // ]]
1442 @(O_trans … (coroll2 ??))
1443   [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
1444    cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
1445    cut (max a n = n)
1446     [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
1447    cut (max b n = n) [normalize >le_to_leb_true //] #maxb
1448    @le_plus
1449     [@le_plus [>big_def >big_def >maxa >maxb //]
1450      @le_times
1451       [/2 by monotonic_le_minus_r/
1452       |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
1453       ]
1454     |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
1455     ]
1456   |@le_to_O #n >fst_pair >snd_pair
1457    cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
1458    >associative_plus >distributive_times_plus
1459    @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
1460   ]
1461 qed.*)
1462
1463 definition sg ≝ λh,x.
1464   (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)〉〉.
1465
1466 lemma sg_def : ∀h,a,b.
1467   sg h 〈a,b〉 = (S (b-a))*MSC 〈〈a,b〉,〈a,b〉〉 +
1468    (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
1469 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
1470 qed.
1471
1472 (*lemma compl_g11 : ∀h.
1473   constructible (λx. h (fst x) (snd x)) →
1474   (∀n. monotonic ? le (h n)) →
1475   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
1476   CF (sg h) (unary_g h).
1477 #h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)
1478 qed.*)
1479
1480 (**************************** closing the argument ****************************)
1481
1482 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
1483   match d with
1484   [ O ⇒ c
1485   | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
1486      d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
1487
1488 lemma h_of_aux_O: ∀r,c,b.
1489   h_of_aux r c O b  = c.
1490 // qed.
1491
1492 lemma h_of_aux_S : ∀r,c,d,b.
1493   h_of_aux r c (S d) b =
1494     (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
1495       (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
1496 // qed.
1497
1498 lemma h_of_aux_prim_rec : ∀r,c,n,b. h_of_aux r c n b =
1499   prim_rec (λx.c)
1500    (λx.let d ≝ S(fst x) in
1501        let b ≝ snd (snd x) in
1502        (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
1503         d*(S d)*sU 〈〈b-d,b〉,〈b,r (fst (snd x))〉〉) n b.
1504 #r #c #n #b elim n
1505   [>h_of_aux_O normalize //
1506   |#n1 #Hind >h_of_aux_S >prim_rec_S >snd_pair >snd_pair >fst_pair
1507    >fst_pair <Hind //
1508   ]
1509 qed.
1510
1511 (*
1512 lemma h_of_aux_constr :
1513 ∀r,c. constructible (λx.h_of_aux r c (fst x) (snd x)).
1514 #r #c
1515   @(ext_constr …
1516     (unary_pr (λx.c)
1517      (λx.let d ≝ S(fst x) in
1518        let b ≝ snd (snd x) in
1519        (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
1520         d*(S d)*sU 〈〈b-d,b〉,〈b,r (fst (snd x))〉〉)))
1521   [#n @sym_eq whd in match (unary_pr ???); @h_of_aux_prim_rec
1522   |@constr_prim_rec*)
1523
1524 definition h_of ≝ λr,p.
1525   let m ≝ max (fst p) (snd p) in
1526   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
1527
1528 lemma h_of_O: ∀r,a,b. b ≤ a →
1529   h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
1530 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
1531 qed.
1532
1533 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
1534   let m ≝ max a b in
1535   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
1536 #r #a #b normalize >fst_pair >snd_pair //
1537 qed.
1538
1539 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
1540   ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
1541   h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
1542 #r #Hr #monor #d #d1 lapply d -d elim d1
1543   [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
1544    >h_of_aux_O >h_of_aux_O  //
1545   |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
1546     [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
1547      >h_of_aux_S @(transitive_le ???? (le_plus_n …))
1548      >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
1549      >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
1550     |#Hd >Hd >h_of_aux_S >h_of_aux_S
1551      cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
1552      @le_plus [@le_times //]
1553       [@monotonic_MSC @le_pair @le_pair //
1554       |@le_times [//] @monotonic_sU
1555         [@le_pair // |// |@monor @Hind //]
1556       ]
1557     ]
1558   ]
1559 qed.
1560
1561 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
1562   ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
1563 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
1564 cut (max i a ≤ max i b)
1565   [@to_max
1566     [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
1567 #Hmax @(mono_h_of_aux r Hr Hmono)
1568   [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
1569 qed.
1570
1571 axiom h_of_constr : ∀r:nat →nat.
1572   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1573   constructible (h_of r).
1574
1575 (*lemma speed_compl: ∀r:nat →nat.
1576   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1577   CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
1578 #r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …))
1579   [#x cases (surj_pair x) #a * #b #eqx >eqx
1580    >sg_def cases (decidable_le b a)
1581     [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
1582      <plus_n_O <plus_n_O >h_of_def
1583      cut (max a b = a)
1584       [normalize cases (le_to_or_lt_eq … leba)
1585         [#ltba >(lt_to_leb_false … ltba) %
1586         |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
1587      #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
1588      @monotonic_MSC @le_pair @le_pair //
1589     |#ltab >h_of_def >h_of_def
1590      cut (max a b = b)
1591       [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
1592      #Hmax >Hmax
1593      cut (max (S a) b = b)
1594       [whd in ⊢ (??%?);  >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
1595      #Hmax1 >Hmax1
1596      cut (∃d.b - a = S d)
1597        [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
1598      * #d #eqd >eqd
1599      cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
1600      cut (b - S d = a)
1601        [@plus_to_minus >commutative_plus @minus_to_plus
1602          [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
1603      normalize //
1604     ]
1605   |#n #a #b #leab #lebn >h_of_def >h_of_def
1606    cut (max a n = n)
1607     [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
1608    cut (max b n = n)
1609     [normalize >(le_to_leb_true … lebn) %] #Hmaxb
1610    >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
1611   |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
1612   |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
1613     [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]
1614    @(h_of_constr r Hr Hmono Hconstr)
1615   ]
1616 qed.
1617
1618 lemma speed_compl_i: ∀r:nat →nat.
1619   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1620   ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
1621 #r #Hr #Hmono #Hconstr #i
1622 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
1623   [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
1624 @smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //
1625 qed.*)
1626
1627 (**************************** the speedup theorem *****************************)
1628 (*theorem pseudo_speedup:
1629   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1630   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
1631 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
1632 #r #Hr #Hmono #Hconstr
1633 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
1634 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
1635 #Hcodei #HCi
1636 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
1637 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
1638 (* sg is (λx.h_of r 〈i,x〉) *)
1639 %{(λx. h_of r 〈S i,x〉)}
1640 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
1641 %[%[@condition_1 |@Hg]
1642  |cases Hg #H1 * #j * #Hcodej #HCj
1643   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
1644   cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
1645   @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
1646   [@(transitive_le … ltin) @(le_maxl … (le_n …))]
1647   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
1648   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
1649  ]
1650 qed.
1651
1652 theorem pseudo_speedup':
1653   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1654   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
1655   (* ¬ O (r ∘ sg) sf. *)
1656   ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
1657 #r #Hr #Hmono #Hconstr
1658 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
1659 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
1660 #Hcodei #HCi
1661 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
1662 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
1663 (* sg is (λx.h_of r 〈i,x〉) *)
1664 %{(λx. h_of r 〈S i,x〉)}
1665 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
1666 %[%[@condition_1 |@Hg]
1667  |cases Hg #H1 * #j * #Hcodej #HCj
1668   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
1669   cases HCi #m * #a #Ha
1670   %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2 #Hlesf
1671   %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
1672   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
1673   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
1674   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
1675  ]
1676 qed.*)
1677