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 lemma max_prim_rec1: ∀a,b,p,f,x.
 389   max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
 390     prim_rec (λi.0)
 391     (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
 392         then max (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
 393         else fst (snd i)) (b x-a x) 〈a x ,x〉.
 394 #a #b #p #f #x elim (b x-a x)
 395   [normalize //
 396   |#i #Hind >prim_rec_S
 397    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 398    cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
 399     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 400   ]
 401 qed.
 402
 403 lemma sum_prim_rec1: ∀a,b,p,f,x.
 404   ∑_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
 405     prim_rec (λi.0)
 406     (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
 407         then plus (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
 408         else fst (snd i)) (b x-a x) 〈a x ,x〉.
 409 #a #b #p #f #x elim (b x-a x)
 410   [normalize //
 411   |#i #Hind >prim_rec_S
 412    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 413    cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
 414     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 415   ]
 416 qed.
 417
 418 lemma bigop_prim_rec: ∀a,b,c,p,f,x.
 419   bigop (b x-a x) (λi:ℕ.p 〈i+a x,x〉) ? (c 〈a x,x〉) plus (λi:ℕ.f 〈i+a x,x〉) =
 420     prim_rec c
 421     (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
 422         then plus (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
 423         else fst (snd i)) (b x-a x) 〈a x ,x〉.
 424 #a #b #c #p #f #x normalize elim (b x-a x)
 425   [normalize //
 426   |#i #Hind >prim_rec_S
 427    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 428    cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
 429     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 430   ]
 431 qed.
 432
 433 lemma bigop_prim_rec_dec: ∀a,b,c,p,f,x.
 434   bigop (b x-a x) (λi:ℕ.p 〈b x -i,x〉) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈b x-i,x〉) =
 435     prim_rec c
 436     (λi.if p 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉
 437         then plus (f 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉) (fst (snd i))
 438         else fst (snd i)) (b x-a x) 〈b x ,x〉.
 439 #a #b #c #p #f #x normalize elim (b x-a x)
 440   [normalize //
 441   |#i #Hind >prim_rec_S
 442    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 443    cases (true_or_false (p 〈b x - i,x〉)) #Hcase >Hcase
 444     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 445   ]
 446 qed.
 447
 448 lemma bigop_prim_rec_dec1: ∀a,b,c,p,f,x.
 449   bigop (S(b x)-a x) (λi:ℕ.p 〈b x - i,x〉) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈b x- i,x〉) =
 450     prim_rec c
 451     (λi.if p 〈fst (snd (snd i)) - (fst i),snd (snd (snd i))〉
 452         then plus (f 〈fst (snd (snd i)) - (fst i),snd (snd (snd i))〉) (fst (snd i))
 453         else fst (snd i)) (S(b x)-a x) 〈b x,x〉.
 454 #a #b #c #p #f #x elim (S(b x)-a x)
 455   [normalize //
 456   |#i #Hind >prim_rec_S
 457    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 458    cases (true_or_false (p 〈b x - i,x〉)) #Hcase >Hcase
 459     [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 460   ]
 461 qed.
 462
 463 (*
 464 lemma bigop_aux_1: ∀k,c,f.
 465   bigop (S k) (λi:ℕ.true) ? c plus (λi:ℕ.f i) =
 466     f 0 + bigop k (λi:ℕ.true) ? c plus (λi:ℕ.f (S i)).
 467 #k #c #f elim k [normalize //] #i #Hind >bigop_Strue //
 468
 469 lemma bigop_prim_rec_dec: ∀a,b,c,f,x.
 470   bigop (b x-a x) (λi:ℕ.true) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈i+a x,x〉) =
 471     prim_rec c
 472     (λi. plus (f 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉) (fst (snd i)))
 473     (b x-a x) 〈b x ,x〉.
 474 #a #b #c #f #x normalize elim (b x-a x)
 475   [normalize //
 476   |#i #Hind >prim_rec_S
 477    >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
 478    <Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
 479   ]
 480 qed. *)
 481
 482 lemma bigop_plus_c: ∀k,p,f,c.
 483   c k + bigop k (λi.p i) ? 0 plus (λi.f i) =
 484     bigop k (λi.p i) ? (c k) plus (λi.f i).
 485 #k #p #f elim k [normalize //]
 486 #i #Hind #c cases (true_or_false (p i)) #Hcase
 487 [>bigop_Strue // >bigop_Strue // <associative_plus >(commutative_plus ? (f i))
 488  >associative_plus @eq_f @Hind
 489 |>bigop_Sfalse // >bigop_Sfalse //
 490 ]
 491 qed.
 492
 493 (* the argument is 〈b-a,〈a,x〉〉 *)
 494
 495
 496 definition max_unary_pr ≝ λp,f.unary_pr (λx.0)
 497     (λi.
 498       let k ≝ fst i in
 499       let r ≝ fst (snd i) in
 500       let a ≝ fst (snd (snd i)) in
 501       let x ≝ snd (snd (snd i)) in
 502       if p 〈k + a,x〉 then max (f 〈k+a,x〉) r else r).
 503
 504 lemma max_unary_pr1: ∀a,b,p,f,x.
 505   max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
 506     ((max_unary_pr p f) ∘ (λx.〈b x - a x,〈a x,x〉〉)) x.
 507 #a #b #p #f #x normalize >fst_pair >snd_pair @max_prim_rec1
 508 qed.
 509
 510 (*
 511 lemma max_unary_pr: ∀a,b,p,f,x.
 512   max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) =
 513     prim_rec (λi.0)
 514     (λ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.
 515 *)
 516
 517 (*
 518 definition unary_compl ≝ λp,f,hf.
 519   unary_pr MSC
 520    (λx:ℕ
 521     .fst (snd x)
 522      +hf
 523       〈fst x,
 524       〈unary_pr (λx0:ℕ.O)
 525        (λi:ℕ
 526         .(let (k:ℕ) ≝fst i in
 527           let (r:ℕ) ≝fst (snd i) in
 528           let (a:ℕ) ≝fst (snd (snd i)) in
 529           let (x:ℕ) ≝snd (snd (snd i)) in
 530           if p 〈k+a,x〉 then max (f 〈k+a,x〉) r else r )) 〈fst x,snd (snd x)〉,
 531       snd (snd x)〉〉). *)
 532
 533 definition aux_compl ≝ λhp,hf.λi.
 534   let k ≝ fst i in
 535   let r ≝ fst (snd i) in
 536   let a ≝ fst (snd (snd i)) in
 537   let x ≝ snd (snd (snd i)) in
 538   hp 〈k+a,x〉 + hf 〈k+a,x〉 + (* was MSC r*) MSC i .
 539
 540 definition aux_compl1 ≝ λhp,hf.λi.
 541   let k ≝ fst i in
 542   let r ≝ fst (snd i) in
 543   let a ≝ fst (snd (snd i)) in
 544   let x ≝ snd (snd (snd i)) in
 545   hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
 546
 547 lemma aux_compl1_def: ∀k,r,m,hp,hf.
 548   aux_compl1 hp hf 〈k,〈r,m〉〉 =
 549   let a ≝ fst m in
 550   let x ≝ snd m in
 551   hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
 552 #k #r #m #hp #hf normalize >fst_pair >snd_pair >snd_pair >fst_pair //
 553 qed.
 554
 555 lemma aux_compl1_def1: ∀k,r,a,x,hp,hf.
 556   aux_compl1 hp hf 〈k,〈r,〈a,x〉〉〉 = hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
 557 #k #r #a #x #hp #hf normalize >fst_pair >snd_pair >snd_pair >fst_pair
 558 >fst_pair >snd_pair //
 559 qed.
 560
 561
 562 axiom Oaux_compl: ∀hp,hf. O (aux_compl1 hp hf) (aux_compl hp hf).
 563
 564 (*
 565 definition IF ≝ λb,f,g:nat →option nat. λx.
 566   match b x with
 567   [None ⇒ None ?
 568   |Some n ⇒ if (eqb n 0) then f x else g x].
 569 *)
 570
 571 axiom CF_if: ∀b:nat → bool. ∀f,g,s. CF s b → CF s f → CF s g →
 572   CF s (λx. if b x then f x else g x).
 573
 574 (*
 575 lemma IF_CF: ∀b,f,g,sb,sf,sg. CF sb b → CF sf f → CF sg g →
 576   CF (λn. sb n + sf n + sg n) (IF b f g).
 577 #b #f #g #sb #sf #sg #Hb #Hf #Hg @IF_CF_new
 578   [@(monotonic_CF … Hb) @O_plus_l @O_plus_l //
 579   |@(monotonic_CF … Hf) @O_plus_l @O_plus_r //
 580   |@(monotonic_CF … Hg) @O_plus_r //
 581   ]
 582 qed.
 583 *)
 584
 585 axiom CF_le: ∀h,f,g. CF h f → CF h g → CF h (λx. leb (f x) (g x)).
 586 axiom CF_max1: ∀h,f,g. CF h f → CF h g → CF h (λx. max (f x) (g x)).
 587 axiom CF_plus: ∀h,f,g. CF h f → CF h g → CF h (λx. f x + g x).
 588 axiom CF_minus: ∀h,f,g. CF h f → CF h g → CF h (λx. f x - g x).
 589
 590 axiom MSC_prop: ∀f,h. CF h f → ∀x. MSC (f x) ≤ h x.
 591
 592 lemma MSC_max: ∀f,h,x. CF h f → MSC (max_{i < x}(f i)) ≤ max_{i < x}(h i).
 593 #f #h #x #hf elim x // #i #Hind >bigop_Strue [|//] >bigop_Strue [|//]
 594 whd in match (max ??);
 595 cases (true_or_false (leb (f i) (bigop i (λi0:ℕ.true) ? 0 max(λi0:ℕ.f i0))))
 596 #Hcase >Hcase
 597   [@(transitive_le … Hind) @le_maxr //
 598   |@(transitive_le … (MSC_prop … hf i)) @le_maxl //
 599   ]
 600 qed.
 601
 602 lemma CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
 603   CF ha a → CF hb b → CF hp p → CF hf f →
 604   O s (λx.ha x + hb x +
 605        (∑_{i ∈[a x ,b x[ }
 606          (hp 〈i,x〉 + hf 〈i,x〉 + max_{i ∈ [a x, b x [ }(hf 〈i,x〉)))) →
 607   CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
 608 #a #b #p #f #ha #hb #hp #hf #s #CFa #CFb #CFp #CFf #HO
 609 @ext_CF1 [|#x @max_unary_pr1]
 610 @(CF_comp ??? (λx.ha x + hb x))
 611   [|@CF_comp_pair
 612     [@CF_minus [@(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
 613     |@CF_comp_pair
 614       [@(O_to_CF … CFa) @O_plus_l //
 615       | @(O_to_CF … CF_id) @O_plus_r @(proj1 … CFb)
 616       ]
 617     ]
 618   |@(CF_prim_rec … MSC … (aux_compl1 hp hf))
 619      [@CF_const
 620      |@(O_to_CF … (Oaux_compl … ))
 621       @CF_if
 622        [@(CF_comp p … MSC … CFp)
 623          [@CF_comp_pair
 624            [@CF_plus [@CF_fst| @CF_comp_fst @CF_comp_snd @CF_snd]
 625            |@CF_comp_snd @CF_comp_snd @CF_snd]
 626          |@le_to_O #x normalize >commutative_plus >associative_plus @le_plus //
 627          ]
 628        |@CF_max1
 629          [@(CF_comp f … MSC … CFf)
 630            [@CF_comp_pair
 631              [@CF_plus [@CF_fst| @CF_comp_fst @CF_comp_snd @CF_snd]
 632              |@CF_comp_snd @CF_comp_snd @CF_snd]
 633            |@le_to_O #x normalize >commutative_plus //
 634            ]
 635          |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
 636          ]
 637        |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
 638        ]
 639      |@O_refl
 640      ]
 641   |@(O_trans … HO) -HO
 642    @(O_trans ? (λx:ℕ
 643    .ha x+hb x
 644     +bigop (b x-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus
 645      (λi:ℕ
 646       .(λi0:ℕ
 647         .hp 〈i0,x〉+hf 〈i0,x〉
 648          +bigop (b x-a x) (λi1:ℕ.true) ? 0 max
 649           (λi1:ℕ.(λi2:ℕ.hf 〈i2,x〉) (i1+a x))) (i+a x))))
 650     [
 651    @le_to_O #n @le_plus // whd in match (unary_pr ???);
 652    >fst_pair >snd_pair >bigop_prim_rec elim (b n - a n)
 653     [normalize //
 654     |#x #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >aux_compl1_def1
 655      >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >fst_pair
 656      >snd_pair normalize in ⊢ (??%); >commutative_plus @le_plus
 657       [-Hind @le_plus // normalize >fst_pair >snd_pair
 658        @(transitive_le ? (bigop x (λi1:ℕ.true) ? 0 (λn0:ℕ.λm:ℕ.if leb n0 m then m else n0 )
 659          (λi1:ℕ.hf 〈i1+a n,n〉)))
 660         [elim x [normalize @MSC_le]
 661          #x0 #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >snd_pair
 662          >fst_pair >fst_pair cases (p 〈x0+a n,n〉) normalize
 663           [cases (true_or_false (leb (f 〈x0+a n,n〉)
 664             (prim_rec (λx00:ℕ.O)
 665              (λi:ℕ
 666             .if p 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
 667              then if leb (f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉)
 668                            (fst (snd i))
 669                       then fst (snd i)
 670                       else f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
 671              else fst (snd i) ) x0 〈a n,n〉))) #Hcase >Hcase normalize
 672            [@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
 673            |@(transitive_le … (MSC_prop … CFf …)) @(le_maxl … (le_n …))
 674            ]
 675          |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
 676          ]
 677        |@(le_maxr … (le_n …))
 678        ]
 679      |@(transitive_le … Hind) -Hind
 680       generalize in match (bigop x (λi:ℕ.true) ? 0 max
 681               (λi1:ℕ.(λi2:ℕ.hf 〈i2,n〉) (i1+a n))); #c
 682       generalize in match (hf 〈x+a n,n〉); #c1
 683       elim x [//] #x0 #Hind
 684       >prim_rec_S >prim_rec_S normalize >fst_pair >fst_pair >snd_pair
 685       >snd_pair >snd_pair >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair
 686       >fst_pair @le_plus
 687        [@le_plus // cases (true_or_false (leb c1 c)) #Hcase
 688         >Hcase normalize // @lt_to_le @not_le_to_lt @(leb_false_to_not_le ?? Hcase)
 689        |@Hind
 690        ]
 691      ]
 692    ]
 693  |@O_plus [@O_plus_l //] @le_to_O #x
 694   <bigop_plus_c @le_plus // @(transitive_le … (MSC_pair …)) @le_plus
 695    [@MSC_prop @CFa | @MSC_prop @(O_to_CF MSC … (CF_const x)) @(proj1 … CFb)]
 696  ]
 697 qed.
 698
 699 (* old
 700 axiom CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
 701   CF ha a → CF hb b → CF hp p → CF hf f →
 702   O s (λx.ha x + hb x + ∑_{i ∈[a x ,b x[ }(hp 〈i,x〉 + hf 〈i,x〉)) →
 703   CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)). *)
 704
 705 (******************************** minimization ********************************)
 706
 707 alias symbol "plus" (instance 2) = "natural plus".
 708 alias symbol "plus" (instance 5) = "natural plus".
 709 alias symbol "plus" (instance 1) = "natural plus".
 710 alias symbol "plus" (instance 4) = "natural plus".
 711 alias symbol "pair" (instance 3) = "abstract pair".
 712 alias id "O" = "cic:/matita/arithmetics/nat/nat#con:0:1:0".
 713 let rec my_minim a f x k on k ≝
 714   match k with
 715   [O ⇒ a
 716   |S p ⇒ if eqb (my_minim a f x p) (a+p)
 717          then if f 〈a+p,x〉 then a+p else S(a+p)
 718          else (my_minim a f x p) ].
 719
 720 lemma my_minim_S : ∀a,f,x,k.
 721   my_minim a f x (S k) =
 722     if eqb (my_minim a f x k) (a+k)
 723     then if f 〈a+k,x〉 then a+k else S(a+k)
 724     else (my_minim a f x k) .
 725 // qed.
 726
 727 lemma my_minim_fa : ∀a,f,x,k. f〈a,x〉 = true → my_minim a f x k = a.
 728 #a #f #x #k #H elim k // #i #Hind normalize >Hind
 729 cases (true_or_false (eqb a (a+i))) #Hcase >Hcase normalize //
 730 <(eqb_true_to_eq … Hcase) >H //
 731 qed.
 732
 733 lemma my_minim_nfa : ∀a,f,x,k. f〈a,x〉 = false →
 734 my_minim a f x (S k) = my_minim (S a) f x k.
 735 #a #f #x #k #H elim k
 736   [normalize <plus_n_O >H >eq_to_eqb_true //
 737   |#i #Hind >my_minim_S >Hind >my_minim_S <plus_n_Sm //
 738   ]
 739 qed.
 740
 741 lemma my_min_eq : ∀a,f,x,k.
 742   min k a (λi.f 〈i,x〉) = my_minim a f x k.
 743 #a #f #x #k lapply a -a elim k // #i #Hind #a normalize in ⊢ (??%?);
 744 cases (true_or_false (f 〈a,x〉)) #Hcase >Hcase
 745   [>(my_minim_fa … Hcase) // | >Hind @sym_eq @(my_minim_nfa … Hcase) ]
 746 qed.
 747
 748 (* cambiare qui: togliere S *)
 749
 750
 751 definition minim_unary_pr ≝ λf.unary_pr (λx.S(fst x))
 752     (λi.
 753       let k ≝ fst i in
 754       let r ≝ fst (snd i) in
 755       let b ≝ fst (snd (snd i)) in
 756       let x ≝ snd (snd (snd i)) in
 757       if f 〈b-k,x〉 then b-k else r).
 758
 759 definition compl_minim_unary ≝ λhf:nat → nat.λi.
 760       let k ≝ fst i in
 761       let b ≝ fst (snd (snd i)) in
 762       let x ≝ snd (snd (snd i)) in
 763       hf 〈b-k,x〉 + MSC 〈k,〈S b,x〉〉.
 764
 765 definition compl_minim_unary_aux ≝ λhf,i.
 766       let k ≝ fst i in
 767       let r ≝ fst (snd i) in
 768       let b ≝ fst (snd (snd i)) in
 769       let x ≝ snd (snd (snd i)) in
 770       hf 〈b-k,x〉 + MSC i.
 771
 772 lemma compl_minim_unary_aux_def : ∀hf,k,r,b,x.
 773   compl_minim_unary_aux hf 〈k,〈r,〈b,x〉〉〉 = hf 〈b-k,x〉 + MSC 〈k,〈r,〈b,x〉〉〉.
 774 #hf #k #r #b #x normalize >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair //
 775 qed.
 776
 777 lemma compl_minim_unary_def : ∀hf,k,r,b,x.
 778   compl_minim_unary hf 〈k,〈r,〈b,x〉〉〉 = hf 〈b-k,x〉 + MSC 〈k,〈S b,x〉〉.
 779 #hf #k #r #b #x normalize >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair //
 780 qed.
 781
 782 lemma compl_minim_unary_aux_def2 : ∀hf,k,r,x.
 783   compl_minim_unary_aux hf 〈k,〈r,x〉〉 = hf 〈fst x-k,snd x〉 + MSC 〈k,〈r,x〉〉.
 784 #hf #k #r #x normalize >snd_pair >snd_pair >fst_pair //
 785 qed.
 786
 787 lemma compl_minim_unary_def2 : ∀hf,k,r,x.
 788   compl_minim_unary hf 〈k,〈r,x〉〉 = hf 〈fst x-k,snd x〉 + MSC 〈k,〈S(fst x),snd x〉〉.
 789 #hf #k #r #x normalize >snd_pair >snd_pair >fst_pair //
 790 qed.
 791
 792 lemma min_aux: ∀a,f,x,k. min (S k) (a x) (λi:ℕ.f 〈i,x〉) =
 793   ((minim_unary_pr f) ∘ (λx.〈S k,〈a x + k,x〉〉)) x.
 794 #a #f #x #k whd in ⊢ (???%); >fst_pair >snd_pair
 795 lapply a -a (* @max_prim_rec1 *)
 796 elim k
 797   [normalize #a >fst_pair >snd_pair >fst_pair >snd_pair >snd_pair >fst_pair
 798    <plus_n_O <minus_n_O >fst_pair //
 799   |#i #Hind #a normalize in ⊢ (??%?); >prim_rec_S >fst_pair >snd_pair
 800    >fst_pair >snd_pair >snd_pair >fst_pair <plus_n_Sm <(Hind (λx.S (a x)))
 801    whd in ⊢ (???%); >minus_S_S <(minus_plus_m_m (a x) i) //
 802 qed.
 803
 804 lemma minim_unary_pr1: ∀a,b,f,x.
 805   μ_{i ∈[a x,b x]}(f 〈i,x〉) =
 806     if leb (a x) (b x) then ((minim_unary_pr f) ∘ (λx.〈S (b x) - a x,〈b x,x〉〉)) x
 807     else (a x).
 808 #a #b #f #x cases (true_or_false (leb (a x) (b x))) #Hcase >Hcase
 809   [cut (b x = a x + (b x - a x))
 810     [>commutative_plus <plus_minus_m_m // @leb_true_to_le // ]
 811    #Hcut whd in ⊢ (???%); >minus_Sn_m [|@leb_true_to_le //]
 812    >min_aux whd in ⊢ (??%?); <Hcut //
 813   |>eq_minus_O // @not_le_to_lt @leb_false_to_not_le //
 814   ]
 815 qed.
 816
 817 axiom sum_inv: ∀a,b,f.∑_{i ∈ [a,S b[ }(f i) = ∑_{i ∈ [a,S b[ }(f (a + b - i)).
 818
 819 (*
 820 #a #b #f @(bigop_iso … plusAC) whd %{(λi.b - a - i)} %{(λi.b - a -i)} %
 821   [%[#i #lti #_ normalize @eq_f >commutative_plus <plus_minus_associative
 822     [2: @le_minus_to_plus_r //
 823      [// @eq_f @@sym_eq @plus_to_minus
 824     |#i #Hi #_ % [% [@le_S_S
 825 *)
 826
 827 example sum_inv_check : ∑_{i ∈ [3,6[ }(i*i) = ∑_{i ∈ [3,6[ }((8-i)*(8-i)).
 828 normalize // qed.
 829
 830 (* provo rovesciando la somma *)
 831
 832 axiom daemon: ∀P:Prop.P.
 833
 834 lemma CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
 835   CF sa a → CF sb b → CF sf f →
 836   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉 + MSC 〈b x - i,〈S(b x),x〉〉)) →
 837   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
 838 #a #b #f #ha #hb #hf #s #CFa #CFb #CFf #HO
 839 @ext_CF1 [|#x @minim_unary_pr1]
 840 @CF_if
 841   [@CF_le @(O_to_CF … HO)
 842     [@(O_to_CF … CFa) @O_plus_l @O_plus_l  @O_refl
 843     |@(O_to_CF … CFb) @O_plus_l @O_plus_r @O_refl
 844     ]
 845   |@(CF_comp ??? (λx.ha x + hb x))
 846     [|@CF_comp_pair
 847       [@CF_minus [@CF_compS @(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
 848       |@CF_comp_pair
 849         [@(O_to_CF … CFb) @O_plus_r //
 850         |@(O_to_CF … CF_id) @O_plus_r @(proj1 … CFb)
 851         ]
 852       ]
 853     |@(CF_prim_rec_gen … MSC … (compl_minim_unary_aux hf))
 854       [@((λx:ℕ.fst (snd x)
 855           +compl_minim_unary hf
 856           〈fst x,
 857           〈unary_pr fst
 858             (λi:ℕ
 859              .(let (k:ℕ) ≝fst i in
 860                let (r:ℕ) ≝fst (snd i) in
 861                let (b:ℕ) ≝fst (snd (snd i)) in
 862                let (x:ℕ) ≝snd (snd (snd i)) in if f 〈b-S k,x〉 then b-S k else r ))
 863           〈fst x,snd (snd x)〉,
 864           snd (snd x)〉〉))
 865       |@CF_compS @CF_fst
 866       |@CF_if
 867         [@(CF_comp f … MSC … CFf)
 868           [@CF_comp_pair
 869             [@CF_minus [@CF_comp_fst @CF_comp_snd @CF_snd|@CF_fst]
 870             |@CF_comp_snd @CF_comp_snd @CF_snd]
 871           |@le_to_O #x normalize >commutative_plus //
 872           ]
 873         |@(O_to_CF … MSC)
 874           [@le_to_O #x normalize //
 875           |@CF_minus
 876             [@CF_comp_fst @CF_comp_snd @CF_snd |@CF_fst]
 877           ]
 878         |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
 879         ]
 880       |@O_plus
 881         [@O_plus_l @O_refl
 882         |@O_plus_r @O_ext2 [||#x >compl_minim_unary_aux_def2 @refl]
 883          @O_trans [||@le_to_O #x >compl_minim_unary_def2 @le_n]
 884          @O_plus [@O_plus_l //]
 885          @O_plus_r
 886          @O_trans [|@le_to_O #x @MSC_pair] @O_plus
 887            [@le_to_O #x @monotonic_MSC @(transitive_le ???? (le_fst …))
 888             >fst_pair @le_n]
 889          @O_trans [|@le_to_O #x @MSC_pair] @O_plus
 890            [@le_to_O #x @monotonic_MSC @(transitive_le ???? (le_snd …))
 891             >snd_pair @(transitive_le ???? (le_fst …)) >fst_pair
 892             normalize >snd_pair >fst_pair lapply (surj_pair x)
 893             * #x1 * #x2 #Hx >Hx >fst_pair >snd_pair elim x1 //
 894             #i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
 895             cases (f ?) [@le_S // | //]]
 896          @le_to_O #x @monotonic_MSC @(transitive_le ???? (le_snd …)) >snd_pair
 897          >(expand_pair (snd (snd x))) in ⊢ (?%?); @le_pair //
 898         ]
 899       ]
 900     |cut (O s (λx.ha x + hb x +
 901             ∑_{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〉〉)))
 902       [@(O_ext2 … HO) #x @eq_f @sum_inv] -HO #HO
 903      @(O_trans … HO) -HO
 904      @(O_trans ? (λx:ℕ.ha x+hb x
 905        +bigop (S(b x)-a x) (λi:ℕ.true) ?
 906         (MSC 〈b x,x〉) plus (λi:ℕ.(λj.hf j + MSC 〈b x - fst j,〈S(b (snd j)),snd j〉〉) 〈b x- i,x〉)))
 907       [@le_to_O #n @le_plus // whd in match (unary_pr ???);
 908        >fst_pair >snd_pair >(bigop_prim_rec_dec1 a b ? (λi.true))
 909         (* it is crucial to recall that the index is bound by S(b x) *)
 910         cut (S (b n) - a n ≤ S (b n)) [//]
 911         elim (S(b n) - a n)
 912         [normalize //
 913         |#x #Hind #lex >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair
 914          >compl_minim_unary_def >prim_rec_S >fst_pair >snd_pair >fst_pair
 915          >snd_pair >fst_pair >snd_pair >fst_pair whd in ⊢ (??%); >commutative_plus
 916          @le_plus [2:@Hind @le_S @le_S_S_to_le @lex] -Hind >snd_pair
 917          >minus_minus_associative // @le_S_S_to_le //
 918         ]
 919       |@O_plus [@O_plus_l //] @O_ext2 [||#x @bigop_plus_c]
 920        @O_plus
 921         [@O_plus_l @O_trans [|@le_to_O #x @MSC_pair]
 922          @O_plus [@O_plus_r @le_to_O @(MSC_prop … CFb)|@O_plus_r @(proj1 … CFb)]
 923         |@O_plus_r @(O_ext2 … (O_refl …)) #x @same_bigop
 924           [//|#i #H #_ @eq_f2 [@eq_f @eq_f2 //|>fst_pair @eq_f @eq_f2  //]
 925         ]
 926       ]
 927     ]
 928   ]
 929   |@(O_to_CF … CFa) @(O_trans … HO) @O_plus_l @O_plus_l @O_refl
 930   ]
 931 qed.
 932
 933 (*
 934 lemma CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
 935   CF sa a → CF sb b → CF sf f →
 936   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
 937   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
 938 #a #b #f #ha #hb #hf #s #CFa #CFb #CFf #HO
 939 @ext_CF1 [|#x @minim_unary_pr1]
 940 @(CF_comp ??? (λx.ha x + hb x))
 941   [|@CF_comp_pair
 942     [@CF_minus [@CF_compS @(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
 943     |@CF_comp_pair
 944       [@CF_max1 [@(O_to_CF … CFa) @O_plus_l // | @CF_compS @(O_to_CF … CFb) @O_plus_r //]
 945       | @(O_to_CF … CF_id) @O_plus_r @(proj1 … CFb)
 946       ]
 947     ]
 948   |@(CF_prim_rec … MSC … (compl_minim_unary_aux hf))
 949     [@CF_fst
 950     |@CF_if
 951       [@(CF_comp f … MSC … CFf)
 952         [@CF_comp_pair
 953           [@CF_minus [@CF_comp_fst @CF_comp_snd @CF_snd|@CF_compS @CF_fst]
 954           |@CF_comp_snd @CF_comp_snd @CF_snd]
 955         |@le_to_O #x normalize >commutative_plus //
 956         ]
 957       |@(O_to_CF … MSC)
 958         [@le_to_O #x normalize //
 959         |@CF_minus
 960           [@CF_comp_fst @CF_comp_snd @CF_snd |@CF_compS @CF_fst]
 961         ]
 962       |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
 963       ]
 964     |@O_refl
 965     ]
 966   |@(O_trans … HO) -HO
 967    @(O_trans ? (λx:ℕ
 968    .ha x+hb x
 969     +bigop (S(b x)-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus (λi:ℕ.hf 〈i+a x,x〉)))
 970   [@le_to_O #n @le_plus // whd in match (unary_pr ???);
 971    >fst_pair >snd_pair >(bigop_prim_rec ? (λn.S(b n)) ? (λi.true)) elim (S(b n) - a n)
 972     [normalize @monotonic_MSC @le_pair
 973     |#x #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >compl_minim_unary_def
 974      >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >fst_pair
 975      >snd_pair normalize in ⊢ (??%); >commutative_plus @le_plus
 976       [-Hind @le_plus // normalize >fst_pair >snd_pair
 977        @(transitive_le ? (bigop x (λi1:ℕ.true) ? 0 (λn0:ℕ.λm:ℕ.if leb n0 m then m else n0 )
 978          (λi1:ℕ.hf 〈i1+a n,n〉)))
 979         [elim x [normalize @MSC_le]
 980          #x0 #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >snd_pair
 981          >fst_pair >fst_pair cases (p 〈x0+a n,n〉) normalize
 982           [cases (true_or_false (leb (f 〈x0+a n,n〉)
 983             (prim_rec (λx00:ℕ.O)
 984              (λi:ℕ
 985             .if p 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
 986              then if leb (f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉)
 987                            (fst (snd i))
 988                       then fst (snd i)
 989                       else f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
 990              else fst (snd i) ) x0 〈a n,n〉))) #Hcase >Hcase normalize
 991            [@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
 992            |@(transitive_le … (MSC_prop … CFf …)) @(le_maxl … (le_n …))
 993            ]
 994          |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
 995          ]
 996        |@(le_maxr … (le_n …))
 997        ]
 998
 999
1000    @(O_trans ? (λx:ℕ
1001    .ha x+hb x
1002     +bigop (b x-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus
1003      (λi:ℕ
1004       .(λi0:ℕ
1005         .hp 〈i0,x〉+hf 〈i0,x〉
1006          +bigop (b x-a x) (λi1:ℕ.true) ? 0 max
1007           (λi1:ℕ.(λi2:ℕ.hf 〈i2,x〉) (i1+a x))) (i+a x))))
1008     [
1009    @le_to_O #n @le_plus // whd in match (unary_pr ???);
1010    >fst_pair >snd_pair >bigop_prim_rec elim (b n - a n)
1011     [normalize //
1012     |#x #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >aux_compl1_def1
1013      >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >fst_pair
1014      >snd_pair normalize in ⊢ (??%); >commutative_plus @le_plus
1015       [-Hind @le_plus // normalize >fst_pair >snd_pair
1016        @(transitive_le ? (bigop x (λi1:ℕ.true) ? 0 (λn0:ℕ.λm:ℕ.if leb n0 m then m else n0 )
1017          (λi1:ℕ.hf 〈i1+a n,n〉)))
1018         [elim x [normalize @MSC_le]
1019          #x0 #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >snd_pair
1020          >fst_pair >fst_pair cases (p 〈x0+a n,n〉) normalize
1021           [cases (true_or_false (leb (f 〈x0+a n,n〉)
1022             (prim_rec (λx00:ℕ.O)
1023              (λi:ℕ
1024             .if p 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
1025              then if leb (f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉)
1026                            (fst (snd i))
1027                       then fst (snd i)
1028                       else f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
1029              else fst (snd i) ) x0 〈a n,n〉))) #Hcase >Hcase normalize
1030            [@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
1031            |@(transitive_le … (MSC_prop … CFf …)) @(le_maxl … (le_n …))
1032            ]
1033          |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
1034          ]
1035        |@(le_maxr … (le_n …))
1036        ]
1037      |@(transitive_le … Hind) -Hind
1038       generalize in match (bigop x (λi:ℕ.true) ? 0 max
1039               (λi1:ℕ.(λi2:ℕ.hf 〈i2,n〉) (i1+a n))); #c
1040       generalize in match (hf 〈x+a n,n〉); #c1
1041       elim x [//] #x0 #Hind
1042       >prim_rec_S >prim_rec_S normalize >fst_pair >fst_pair >snd_pair
1043       >snd_pair >snd_pair >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair
1044       >fst_pair @le_plus
1045        [@le_plus // cases (true_or_false (leb c1 c)) #Hcase
1046         >Hcase normalize // @lt_to_le @not_le_to_lt @(leb_false_to_not_le ?? Hcase)
1047        |@Hind
1048        ]
1049      ]
1050    ]
1051  |@O_plus [@O_plus_l //] @le_to_O #x
1052   <bigop_plus_c @le_plus // @(transitive_le … (MSC_pair …)) @le_plus
1053    [@MSC_prop @CFa | @MSC_prop @(O_to_CF MSC … (CF_const x)) @(proj1 … CFb)]
1054  ]
1055 qed.
1056
1057 axiom CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
1058   CF sa a → CF sb b → CF sf f →
1059   O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
1060   CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).*)
1061
1062 (************************************* smn ************************************)
1063 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
1064
1065 (****************************** constructibility ******************************)
1066
1067 definition constructible ≝ λs. CF s s.
1068
1069 lemma constr_comp : ∀s1,s2. constructible s1 → constructible s2 →
1070   (∀x. x ≤ s2 x) → constructible (s2 ∘ s1).
1071 #s1 #s2 #Hs1 #Hs2 #Hle @(CF_comp … Hs1 Hs2) @O_plus @le_to_O #x [@Hle | //]
1072 qed.
1073
1074 lemma ext_constr: ∀s1,s2. (∀x.s1 x = s2 x) →
1075   constructible s1 → constructible s2.
1076 #s1 #s2 #Hext #Hs1 @(ext_CF … Hext) @(monotonic_CF … Hs1)  #x >Hext //
1077 qed.
1078
1079 lemma constr_prim_rec: ∀s1,s2. constructible s1 → constructible s2 →
1080   (∀n,r,m. 2 * r ≤ s2 〈n,〈r,m〉〉) → constructible (unary_pr s1 s2).
1081 #s1 #s2 #Hs1 #Hs2 #Hincr @(CF_prim_rec … Hs1 Hs2) whd %{2} %{0}
1082 #x #_ lapply (surj_pair x) * #a * #b #eqx >eqx whd in match (unary_pr ???);
1083 >fst_pair >snd_pair
1084 whd in match (unary_pr ???); >fst_pair >snd_pair elim a
1085   [normalize //
1086   |#n #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair
1087    >prim_rec_S @transitive_le [| @(monotonic_le_plus_l … Hind)]
1088    @transitive_le [| @(monotonic_le_plus_l … (Hincr n ? b))]
1089    whd in match (unary_pr ???); >fst_pair >snd_pair //
1090   ]
1091 qed.
1092
1093 (********************************* simulation *********************************)
1094
1095 axiom sU : nat → nat.
1096
1097 axiom monotonic_sU: ∀i1,i2,x1,x2,s1,s2. i1 ≤ i2 → x1 ≤ x2 → s1 ≤ s2 →
1098   sU 〈i1,〈x1,s1〉〉 ≤ sU 〈i2,〈x2,s2〉〉.
1099
1100 lemma monotonic_sU_aux : ∀x1,x2. fst x1 ≤ fst x2 → fst (snd x1) ≤ fst (snd x2) →
1101 snd (snd x1) ≤ snd (snd x2) → sU x1 ≤ sU x2.
1102 #x1 #x2 cases (surj_pair x1) #a1 * #y #eqx1 >eqx1 -eqx1 cases (surj_pair y)
1103 #b1 * #c1 #eqy >eqy -eqy
1104 cases (surj_pair x2) #a2 * #y2 #eqx2 >eqx2 -eqx2 cases (surj_pair y2)
1105 #b2 * #c2 #eqy2 >eqy2 -eqy2 >fst_pair >snd_pair >fst_pair >snd_pair
1106 >fst_pair >snd_pair >fst_pair >snd_pair @monotonic_sU
1107 qed.
1108
1109 axiom sU_le: ∀i,x,s. s ≤ sU 〈i,〈x,s〉〉.
1110 axiom sU_le_i: ∀i,x,s. MSC i ≤ sU 〈i,〈x,s〉〉.
1111 axiom sU_le_x: ∀i,x,s. MSC x ≤ sU 〈i,〈x,s〉〉.
1112
1113 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
1114
1115 axiom CF_U : CF sU pU_unary.
1116
1117 definition termb_unary ≝ λx:ℕ.termb (fst x) (fst (snd x)) (snd (snd x)).
1118 definition out_unary ≝ λx:ℕ.out (fst x) (fst (snd x)) (snd (snd x)).
1119
1120 lemma CF_termb: CF sU termb_unary.
1121 @(ext_CF (fst ∘ pU_unary)) [2: @CF_comp_fst @CF_U]
1122 #n whd in ⊢ (??%?); whd in  ⊢ (??(?%)?); >fst_pair %
1123 qed.
1124
1125 lemma CF_out: CF sU out_unary.
1126 @(ext_CF (snd ∘ pU_unary)) [2: @CF_comp_snd @CF_U]
1127 #n whd in ⊢ (??%?); whd in  ⊢ (??(?%)?); >snd_pair %
1128 qed.
1129
1130
1131 (******************** complexity of g ********************)
1132
1133 (*definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
1134 definition auxg ≝
1135   λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
1136     (out i (snd ux) (h (S i) (snd ux))).
1137
1138 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
1139 #h #s #H1 @(CF_compS ? (auxg h) H1)
1140 qed.
1141
1142 definition aux1g ≝
1143   λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
1144     ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
1145
1146 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
1147 #h #x @same_bigop
1148   [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
1149 qed.
1150
1151 lemma compl_g2 : ∀h,s1,s2,s.
1152   CF s1
1153     (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
1154   CF s2
1155     (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
1156   O s (λx.MSC x + ∑_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
1157   CF s (auxg h).
1158 #h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
1159   [#n whd in ⊢ (??%%); @eq_aux]
1160 @(CF_max … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
1161 @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
1162 qed.
1163
1164 lemma compl_g3 : ∀h,s.
1165   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
1166   CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
1167 #h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (proj1 … H))
1168 @O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
1169 qed.
1170
1171 definition min_input_aux ≝ λh,p.
1172   μ_{y ∈ [S (fst p),snd (snd p)] }
1173     ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
1174
1175 lemma min_input_eq : ∀h,p.
1176     min_input_aux h p  =
1177     min_input h (fst p) (snd (snd p)).
1178 #h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
1179 whd in ⊢ (??%%); >fst_pair >snd_pair //
1180 qed.
1181
1182 definition termb_aux ≝ λh.
1183   termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
1184
1185 lemma compl_g4 : ∀h,s1,s.
1186   (CF s1
1187     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
1188    (O s (λx.MSC x + ∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
1189   CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
1190 #h #s1 #s #Hs1 #HO @(ext_CF (min_input_aux h))
1191  [#n whd in ⊢ (??%%); @min_input_eq]
1192 @(CF_mu … MSC MSC … Hs1)
1193   [@CF_compS @CF_fst
1194   |@CF_comp_snd @CF_snd
1195   |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
1196 qed.*)
1197
1198 (************************* a couple of technical lemmas ***********************)
1199 lemma minus_to_0: ∀a,b. a ≤ b → minus a b = 0.
1200 #a elim a // #n #Hind *
1201   [#H @False_ind /2 by absurd/ | #b normalize #H @Hind @le_S_S_to_le /2/]
1202 qed.
1203
1204 lemma sigma_bound:  ∀h,a,b. monotonic nat le h →
1205   ∑_{i ∈ [a,S b[ }(h i) ≤  (S b-a)*h b.
1206 #h #a #b #H cases (decidable_le a b)
1207   [#leab cut (b = pred (S b - a + a))
1208     [<plus_minus_m_m // @le_S //] #Hb >Hb in match (h b);
1209    generalize in match (S b -a);
1210    #n elim n
1211     [//
1212     |#m #Hind >bigop_Strue [2://] @le_plus
1213       [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
1214     ]
1215   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
1216    cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
1217   ]
1218 qed.
1219
1220 lemma sigma_bound_decr:  ∀h,a,b. (∀a1,a2. a1 ≤ a2 → a2 < b → h a2 ≤ h a1) →
1221   ∑_{i ∈ [a,b[ }(h i) ≤  (b-a)*h a.
1222 #h #a #b #H cases (decidable_le a b)
1223   [#leab cut ((b -a) +a ≤ b) [/2 by le_minus_to_plus_r/] generalize in match (b -a);
1224    #n elim n
1225     [//
1226     |#m #Hind >bigop_Strue [2://] #Hm
1227      cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
1228      @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
1229     ]
1230   |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
1231    cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
1232   ]
1233 qed.
1234
1235 lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
1236 O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
1237   (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
1238 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
1239 @(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
1240 qed.
1241
1242 lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
1243 O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
1244 #s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
1245 @(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
1246 qed.
1247
1248 (**************************** end of technical lemmas *************************)
1249
1250 (*lemma compl_g5 : ∀h,s1.(∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
1251   (CF s1
1252     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
1253   CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
1254     (λp:ℕ.min_input h (fst p) (snd (snd p))).
1255 #h #s1 #Hmono #Hs1 @(compl_g4 … Hs1) @O_plus
1256 [@O_plus_l // |@O_plus_r @coroll @Hmono]
1257 qed.
1258
1259 lemma compl_g6: ∀h.
1260   constructible (λx. h (fst x) (snd x)) →
1261   (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
1262     (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
1263 #h #hconstr @(ext_CF (termb_aux h))
1264   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
1265 @(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
1266   [@CF_comp_pair
1267     [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
1268     |@CF_comp_pair
1269       [@(monotonic_CF … CF_fst) #x //
1270       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
1271         [#n normalize >fst_pair >snd_pair %]
1272        @(CF_comp … MSC …hconstr)
1273         [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
1274         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
1275         ]
1276       ]
1277     ]
1278   |@O_plus
1279     [@O_plus
1280       [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
1281         [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
1282          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
1283          >distributive_times_plus @le_plus [//]
1284          cases (surj_pair b) #c * #d #eqb >eqb
1285          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
1286          whd in ⊢ (??%); @le_plus
1287           [@monotonic_MSC @(le_maxl … (le_n …))
1288           |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
1289           ]
1290         |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
1291         ]
1292       |@le_to_O #n @sU_le
1293       ]
1294     |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
1295   ]
1296 qed. *)
1297
1298 definition big : nat →nat ≝ λx.
1299   let m ≝ max (fst x) (snd x) in 〈m,m〉.
1300
1301 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
1302 #a #b normalize >fst_pair >snd_pair // qed.
1303
1304 lemma le_big : ∀x. x ≤ big x.
1305 #x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
1306 [@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
1307 qed.
1308
1309 definition faux2 ≝ λh.
1310   (λx.MSC x + (snd (snd x)-fst x)*
1311     (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
1312
1313 (*lemma compl_g7: ∀h.
1314   constructible (λx. h (fst x) (snd x)) →
1315   (∀n. monotonic ? le (h n)) →
1316   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))〉〉)
1317     (λp:ℕ.min_input h (fst p) (snd (snd p))).
1318 #h #hcostr #hmono @(monotonic_CF … (faux2 h))
1319   [#n normalize >fst_pair >snd_pair //]
1320 @compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
1321 >fst_pair >snd_pair @monotonic_sU // @hmono @lexy
1322 qed.
1323
1324 lemma compl_g71: ∀h.
1325   constructible (λx. h (fst x) (snd x)) →
1326   (∀n. monotonic ? le (h n)) →
1327   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))〉〉)
1328     (λp:ℕ.min_input h (fst p) (snd (snd p))).
1329 #h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x
1330 @le_plus [@monotonic_MSC //]
1331 cases (decidable_le (fst x) (snd(snd x)))
1332   [#Hle @le_times // @monotonic_sU
1333   |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
1334   ]
1335 qed.*)
1336
1337 definition out_aux ≝ λh.
1338   out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
1339
1340 lemma compl_g8: ∀h.
1341   constructible (λx. h (fst x) (snd x)) →
1342   (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
1343     (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
1344 #h #hconstr @(ext_CF (out_aux h))
1345   [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
1346 @(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
1347   [@CF_comp_pair
1348     [@(monotonic_CF … CF_fst) #x //
1349     |@CF_comp_pair
1350       [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
1351       |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
1352         [#n normalize >fst_pair >snd_pair %]
1353        @(CF_comp … MSC …hconstr)
1354         [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
1355         |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
1356         ]
1357       ]
1358     ]
1359   |@O_plus
1360     [@O_plus
1361       [@le_to_O #n @sU_le
1362       |@(O_trans … (λx.MSC (max (fst x) (snd x))))
1363         [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
1364          >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
1365          whd in ⊢ (??%); @le_plus
1366           [@monotonic_MSC @(le_maxl … (le_n …))
1367           |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
1368           ]
1369         |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
1370         ]
1371       ]
1372     |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
1373   ]
1374 qed.
1375
1376 (*lemma compl_g9 : ∀h.
1377   constructible (λx. h (fst x) (snd x)) →
1378   (∀n. monotonic ? le (h n)) →
1379   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
1380   CF (λx. (S (snd x-fst x))*MSC 〈x,x〉 +
1381       (snd x-fst x)*(S(snd x-fst x))*sU 〈x,〈snd x,h (S (fst x)) (snd x)〉〉)
1382    (auxg h).
1383 #h #hconstr #hmono #hantimono
1384 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
1385 @O_plus
1386   [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
1387     [// | @monotonic_MSC // ]]
1388 @(O_trans … (coroll2 ??))
1389   [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
1390    cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
1391    cut (max a n = n)
1392     [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
1393    cut (max b n = n) [normalize >le_to_leb_true //] #maxb
1394    @le_plus
1395     [@le_plus [>big_def >big_def >maxa >maxb //]
1396      @le_times
1397       [/2 by monotonic_le_minus_r/
1398       |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
1399       ]
1400     |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
1401     ]
1402   |@le_to_O #n >fst_pair >snd_pair
1403    cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
1404    >associative_plus >distributive_times_plus
1405    @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
1406   ]
1407 qed.*)
1408
1409 definition sg ≝ λh,x.
1410   (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)〉〉.
1411
1412 lemma sg_def : ∀h,a,b.
1413   sg h 〈a,b〉 = (S (b-a))*MSC 〈〈a,b〉,〈a,b〉〉 +
1414    (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
1415 #h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
1416 qed.
1417
1418 (*lemma compl_g11 : ∀h.
1419   constructible (λx. h (fst x) (snd x)) →
1420   (∀n. monotonic ? le (h n)) →
1421   (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
1422   CF (sg h) (unary_g h).
1423 #h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)
1424 qed.*)
1425
1426 (**************************** closing the argument ****************************)
1427
1428 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
1429   match d with
1430   [ O ⇒ c
1431   | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
1432      d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
1433
1434 lemma h_of_aux_O: ∀r,c,b.
1435   h_of_aux r c O b  = c.
1436 // qed.
1437
1438 lemma h_of_aux_S : ∀r,c,d,b.
1439   h_of_aux r c (S d) b =
1440     (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
1441       (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
1442 // qed.
1443
1444 lemma h_of_aux_prim_rec : ∀r,c,n,b. h_of_aux r c n b =
1445   prim_rec (λx.c)
1446    (λx.let d ≝ S(fst x) in
1447        let b ≝ snd (snd x) in
1448        (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
1449         d*(S d)*sU 〈〈b-d,b〉,〈b,r (fst (snd x))〉〉) n b.
1450 #r #c #n #b elim n
1451   [>h_of_aux_O normalize //
1452   |#n1 #Hind >h_of_aux_S >prim_rec_S >snd_pair >snd_pair >fst_pair
1453    >fst_pair <Hind //
1454   ]
1455 qed.
1456
1457 (*
1458 lemma h_of_aux_constr :
1459 ∀r,c. constructible (λx.h_of_aux r c (fst x) (snd x)).
1460 #r #c
1461   @(ext_constr …
1462     (unary_pr (λx.c)
1463      (λx.let d ≝ S(fst x) in
1464        let b ≝ snd (snd x) in
1465        (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
1466         d*(S d)*sU 〈〈b-d,b〉,〈b,r (fst (snd x))〉〉)))
1467   [#n @sym_eq whd in match (unary_pr ???); @h_of_aux_prim_rec
1468   |@constr_prim_rec*)
1469
1470 definition h_of ≝ λr,p.
1471   let m ≝ max (fst p) (snd p) in
1472   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
1473
1474 lemma h_of_O: ∀r,a,b. b ≤ a →
1475   h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
1476 #r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
1477 qed.
1478
1479 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
1480   let m ≝ max a b in
1481   h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
1482 #r #a #b normalize >fst_pair >snd_pair //
1483 qed.
1484
1485 lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
1486   ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
1487   h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
1488 #r #Hr #monor #d #d1 lapply d -d elim d1
1489   [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
1490    >h_of_aux_O >h_of_aux_O  //
1491   |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
1492     [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
1493      >h_of_aux_S @(transitive_le ???? (le_plus_n …))
1494      >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
1495      >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
1496     |#Hd >Hd >h_of_aux_S >h_of_aux_S
1497      cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
1498      @le_plus [@le_times //]
1499       [@monotonic_MSC @le_pair @le_pair //
1500       |@le_times [//] @monotonic_sU
1501         [@le_pair // |// |@monor @Hind //]
1502       ]
1503     ]
1504   ]
1505 qed.
1506
1507 lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
1508   ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
1509 #r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
1510 cut (max i a ≤ max i b)
1511   [@to_max
1512     [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
1513 #Hmax @(mono_h_of_aux r Hr Hmono)
1514   [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
1515 qed.
1516
1517 axiom h_of_constr : ∀r:nat →nat.
1518   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1519   constructible (h_of r).
1520
1521 (*lemma speed_compl: ∀r:nat →nat.
1522   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1523   CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
1524 #r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …))
1525   [#x cases (surj_pair x) #a * #b #eqx >eqx
1526    >sg_def cases (decidable_le b a)
1527     [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
1528      <plus_n_O <plus_n_O >h_of_def
1529      cut (max a b = a)
1530       [normalize cases (le_to_or_lt_eq … leba)
1531         [#ltba >(lt_to_leb_false … ltba) %
1532         |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
1533      #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
1534      @monotonic_MSC @le_pair @le_pair //
1535     |#ltab >h_of_def >h_of_def
1536      cut (max a b = b)
1537       [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
1538      #Hmax >Hmax
1539      cut (max (S a) b = b)
1540       [whd in ⊢ (??%?);  >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
1541      #Hmax1 >Hmax1
1542      cut (∃d.b - a = S d)
1543        [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
1544      * #d #eqd >eqd
1545      cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
1546      cut (b - S d = a)
1547        [@plus_to_minus >commutative_plus @minus_to_plus
1548          [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
1549      normalize //
1550     ]
1551   |#n #a #b #leab #lebn >h_of_def >h_of_def
1552    cut (max a n = n)
1553     [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
1554    cut (max b n = n)
1555     [normalize >(le_to_leb_true … lebn) %] #Hmaxb
1556    >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
1557   |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
1558   |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
1559     [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]
1560    @(h_of_constr r Hr Hmono Hconstr)
1561   ]
1562 qed.
1563
1564 lemma speed_compl_i: ∀r:nat →nat.
1565   (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1566   ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
1567 #r #Hr #Hmono #Hconstr #i
1568 @(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
1569   [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
1570 @smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //
1571 qed.*)
1572
1573 (**************************** the speedup theorem *****************************)
1574 (*theorem pseudo_speedup:
1575   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1576   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
1577 (* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
1578 #r #Hr #Hmono #Hconstr
1579 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
1580 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
1581 #Hcodei #HCi
1582 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
1583 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
1584 (* sg is (λx.h_of r 〈i,x〉) *)
1585 %{(λx. h_of r 〈S i,x〉)}
1586 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
1587 %[%[@condition_1 |@Hg]
1588  |cases Hg #H1 * #j * #Hcodej #HCj
1589   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
1590   cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
1591   @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
1592   [@(transitive_le … ltin) @(le_maxl … (le_n …))]
1593   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
1594   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
1595  ]
1596 qed.
1597
1598 theorem pseudo_speedup':
1599   ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1600   ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
1601   (* ¬ O (r ∘ sg) sf. *)
1602   ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
1603 #r #Hr #Hmono #Hconstr
1604 (* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
1605 %{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #H * #i *
1606 #Hcodei #HCi
1607 (* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
1608 %{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
1609 (* sg is (λx.h_of r 〈i,x〉) *)
1610 %{(λx. h_of r 〈S i,x〉)}
1611 lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
1612 %[%[@condition_1 |@Hg]
1613  |cases Hg #H1 * #j * #Hcodej #HCj
1614   lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
1615   cases HCi #m * #a #Ha
1616   %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2 #Hlesf
1617   %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
1618   cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
1619   #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
1620   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
1621  ]
1622 qed.*)
1623