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".
8 (************************* notation for minimization **************************)
9 notation "μ_{ ident i < n } p"
10 with precedence 80 for @{min $n 0 (λ${ident i}.$p)}.
12 notation "μ_{ ident i ≤ n } p"
13 with precedence 80 for @{min (S $n) 0 (λ${ident i}.$p)}.
15 notation "μ_{ ident i ∈ [a,b[ } p"
16 with precedence 80 for @{min ($b-$a) $a (λ${ident i}.$p)}.
18 notation "μ_{ ident i ∈ [a,b] } p"
19 with precedence 80 for @{min (S $b-$a) $a (λ${ident i}.$p)}.
21 (************************************ MAX *************************************)
22 notation "Max_{ ident i < n | p } f"
24 for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
26 notation "Max_{ ident i < n } f"
28 for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}.
30 notation "Max_{ ident j ∈ [a,b[ } f"
32 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
33 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
35 notation "Max_{ ident j ∈ [a,b[ | p } f"
37 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
38 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
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 //
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 //
52 lemma Max0 : ∀n. max 0 n = n.
55 lemma Max0r : ∀n. max n 0 = n.
56 #n >commutative_max //
60 mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)).
62 definition MaxAC ≝ mk_ACop nat 0 MaxA commutative_max.
64 lemma le_Max: ∀f,p,n,a. a < n → p a = true →
65 f a ≤ Max_{i < n | p i}(f i).
67 >(bigop_diff p ? 0 MaxAC f a n) // @(le_maxl … (le_n ?))
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 ?))
76 |/2 by monotonic_lt_minus_l/
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 //
89 (********************************** pairing ***********************************)
90 axiom pair: nat → nat → nat.
91 axiom fst : nat → nat.
92 axiom snd : nat → nat.
94 interpretation "abstract pair" 'pair f g = (pair f g).
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〉.
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〉.
104 lemma expand_pair: ∀x. x = 〈fst x, snd x〉.
105 #x lapply (surj_pair x) * #a * #b #Hx >Hx >fst_pair >snd_pair //
108 (************************************* U **************************************)
109 axiom U: nat → nat →nat → option nat.
111 axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
112 U i x n = Some ? y → U i x m = Some ? y.
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) //
123 definition code_for ≝ λf,i.∀x.
124 ∃n.∀m. n ≤ m → U i x m = f x.
126 definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y.
128 notation "{i ⊙ x} ↓ r" with precedence 60 for @{terminate $i $x $r}.
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} //]
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) //
140 definition termb ≝ λi,x,t.
141 match U i x t with [None ⇒ false |Some y ⇒ true].
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} //]
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 //
151 definition out ≝ λi,x,r.
152 match U i x r with [ None ⇒ 0 | Some z ⇒ z].
154 definition bool_to_nat: bool → nat ≝
155 λb. match b with [true ⇒ 1 | false ⇒ 0].
157 coercion bool_to_nat.
159 definition pU : nat → nat → nat → nat ≝ λi,x,r.〈termb i x r,out i x r〉.
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]
166 |#a #H cut (a=y) [lapply (eq_f … snd … H) >snd_pair >snd_pair #H1 @H1]
172 lemma pU_vs_U_None : ∀i,x,r. pU i x r = 〈0,0〉 ↔ U i x r = None ?.
174 [cases (U i x r) normalize //
175 #a #H cut (1=0) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H1 @H1]
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 //
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 //
189 definition total ≝ λf.λx:nat. Some nat (f x).
192 (********************************* complexity *********************************)
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. *)
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.
204 (* C s i means i is running in O(s) *)
206 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ x → ∃y.
207 U i x (c*(s x)) = Some ? y.
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.
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 | //]
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 | //]
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))
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 //
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 %
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) //
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
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).
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) //]
255 (* primitve recursion *)
259 let rec prim_rec0 (k:nat) (h:nat →nat) n on n ≝
262 | S a ⇒ h 〈a, prim_rec0 k h a〉].
264 lemma prim_rec0_S: ∀k,h,n.
265 prim_rec0 k h (S n) = h 〈n, prim_rec0 k h n〉.
268 let rec prim_rec0_compl (k,sk:nat) (h,sh:nat →nat) n on n ≝
271 | S a ⇒ prim_rec0_compl k sk h sh a + sh (prim_rec0 k h a)].
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).
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
284 (* with argument(s) m *)
285 let rec prim_rec (k,h:nat →nat) n m on n ≝
288 | S a ⇒ h 〈a,〈prim_rec k h a m, m〉〉].
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〉〉.
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 //
301 definition unary_pr ≝ λk,h,x. prim_rec k h (fst x) (snd x).
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 //
309 let rec prim_rec_compl (k,h,sk,sh:nat →nat) n m on n ≝
312 | S a ⇒ prim_rec_compl k h sk sh a m + sh (prim_rec k h a m)].
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).
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
324 (**************************** primitive operations*****************************)
326 definition id ≝ λx:nat.x.
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〉).
335 lemma CF_fst: CF MSC fst.
336 @(ext_CF (fst ∘ id)) [#n //] @(CF_comp_fst … CF_id)
339 lemma CF_snd: CF MSC snd.
340 @(ext_CF (snd ∘ id)) [#n //] @(CF_comp_snd … CF_id)
343 (************************************** eqb ***********************************)
345 axiom CF_eqb: ∀h,f,g.
346 CF h f → CF h g → CF h (λx.eqb (f x) (g x)).
348 (*********************************** maximum **********************************)
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)
364 lemma max_prim_rec_base: ∀a,b,p,f,x. a ≤b →
365 max_{i < b| p 〈i,x〉 }(f 〈i,x〉) =
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
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 // ]
376 lemma max_prim_rec: ∀a,b,p,f,x. a ≤b →
377 max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) =
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
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 // ]
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〉) =
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)
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 // ]
416 lemma sum_prim_rec1: ∀a,b,p,f,x.
417 ∑_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
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)
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 // ]
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〉) =
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)
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 // ]
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〉) =
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)
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 // ]
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〉) =
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)
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 // ]
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 //
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〉) =
511 (λi. plus (f 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉) (fst (snd i)))
513 #a #b #c #f #x normalize elim (b x-a x)
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 // ]
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 //
532 (* the argument is 〈b-a,〈a,x〉〉 *)
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)
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).
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
555 lemma max_unary_pr: ∀a,b,p,f,x.
556 max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) =
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.
562 definition unary_compl ≝ λp,f,hf.
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)〉,
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.
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 .
591 definition aux_compl1 ≝ λhp,hf.λi.
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.
598 lemma aux_compl1_def: ∀k,r,m,hp,hf.
599 aux_compl1 hp hf 〈k,〈r,m〉〉 =
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 //
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 //
613 axiom Oaux_compl: ∀hp,hf. O (aux_compl1 hp hf) (aux_compl hp hf).
616 definition IF ≝ λb,f,g:nat →option nat. λx.
619 |Some n ⇒ if (eqb n 0) then f x else g x].
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).
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 //
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).
641 axiom MSC_prop: ∀f,h. CF h f → ∀x. MSC (f x) ≤ h x.
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))))
648 [@(transitive_le … Hind) @le_maxr //
649 |@(transitive_le … (MSC_prop … hf i)) @le_maxl //
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 +
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))
663 [@CF_minus [@(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
665 [@(O_to_CF … CFa) @O_plus_l //
666 | @(O_to_CF … CF_id) @O_plus_r @(proj1 … CFb)
669 |@(CF_prim_rec … MSC … (aux_compl1 hp hf))
671 |@(O_to_CF … (Oaux_compl … ))
673 [@(CF_comp p … MSC … CFp)
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 //
680 [@(CF_comp f … MSC … CFf)
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 //
686 |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
688 |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
695 +bigop (b x-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus
699 +bigop (b x-a x) (λi1:ℕ.true) ? 0 max
700 (λi1:ℕ.(λi2:ℕ.hf 〈i2,x〉) (i1+a x))) (i+a x))))
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)
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〉)
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))〉)
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 …))
726 |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
728 |@(le_maxr … (le_n …))
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
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)
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)]
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〉)). *)
756 (******************************** minimization ********************************)
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 ≝
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) ].
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) .
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 //
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 //
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) ]
799 (* cambiare qui: togliere S *)
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))
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).
813 definition compl_minim_unary ≝ λhf:nat → nat.λi.
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〉〉.
819 definition compl_minim_unary_aux ≝ λhf,i.
821 let r ≝ fst (snd i) in
822 let b ≝ fst (snd (snd i)) in
823 let x ≝ snd (snd (snd i)) in
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 //
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 //
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 //
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 //
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 *)
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) //
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
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 //
871 axiom sum_inv: ∀a,b,f.∑_{i ∈ [a,S b[ }(f i) = ∑_{i ∈ [a,S b[ }(f (a + b - i)).
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
881 example sum_inv_check : ∑_{i ∈ [3,6[ }(i*i) = ∑_{i ∈ [3,6[ }((8-i)*(8-i)).
884 (* provo rovesciando la somma *)
886 axiom daemon: ∀P:Prop.P.
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]
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
899 |@(CF_comp ??? (λx.ha x + hb x))
901 [@CF_minus [@CF_compS @(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
903 [@(O_to_CF … CFb) @O_plus_r //
904 |@(O_to_CF … CF_id) @O_plus_r @(proj1 … CFb)
907 |@(CF_prim_rec_gen … MSC … (compl_minim_unary_aux hf))
909 +compl_minim_unary hf
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 ))
921 [@(CF_comp f … MSC … CFf)
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 //
928 [@le_to_O #x normalize //
930 [@CF_comp_fst @CF_comp_snd @CF_snd |@CF_fst]
932 |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
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 //]
940 @O_trans [|@le_to_O #x @MSC_pair] @O_plus
941 [@le_to_O #x @monotonic_MSC @(transitive_le ???? (le_fst …))
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 //
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
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)) [//]
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 //
973 |@O_plus [@O_plus_l //] @O_ext2 [||#x @bigop_plus_c]
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 //]
983 |@(O_to_CF … CFa) @(O_trans … HO) @O_plus_l @O_plus_l @O_refl
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))
996 [@CF_minus [@CF_compS @(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
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)
1002 |@(CF_prim_rec … MSC … (compl_minim_unary_aux hf))
1005 [@(CF_comp f … MSC … CFf)
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 //
1012 [@le_to_O #x normalize //
1014 [@CF_comp_fst @CF_comp_snd @CF_snd |@CF_compS @CF_fst]
1016 |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
1020 |@(O_trans … HO) -HO
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)
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))〉)
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 …))
1048 |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
1050 |@(le_maxr … (le_n …))
1056 +bigop (b x-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus
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))))
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)
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)
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))〉)
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 …))
1087 |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
1089 |@(le_maxr … (le_n …))
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
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)
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)]
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〉)).*)
1116 (************************************* smn ************************************)
1117 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
1119 (****************************** constructibility ******************************)
1121 definition constructible ≝ λs. CF s s.
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 | //]
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 //
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 ???);
1138 whd in match (unary_pr ???); >fst_pair >snd_pair elim a
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 //
1147 (********************************* simulation *********************************)
1149 axiom sU : nat → nat.
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〉〉.
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
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〉〉.
1167 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
1169 axiom CF_U : CF sU pU_unary.
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)).
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 %
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 %
1185 (******************** complexity of g ********************)
1187 (*definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
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))).
1192 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
1193 #h #s #H1 @(CF_compS ? (auxg h) H1)
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〉).
1200 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
1202 [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
1205 lemma compl_g2 : ∀h,s1,s2,s.
1207 (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
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〉)) →
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 //]
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 //
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〉).
1229 lemma min_input_eq : ∀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 //
1236 definition termb_aux ≝ λh.
1237 termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
1239 lemma compl_g4 : ∀h,s1,s.
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)
1248 |@CF_comp_snd @CF_snd
1249 |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
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/]
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);
1266 |#m #Hind >bigop_Strue [2://] @le_plus
1267 [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
1269 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
1270 cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
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);
1280 |#m #Hind >bigop_Strue [2://] #Hm
1281 cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
1282 @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
1284 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
1285 cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
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 //]
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
1302 (**************************** end of technical lemmas *************************)
1304 (*lemma compl_g5 : ∀h,s1.(∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
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]
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)
1321 [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
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 //]
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 …))
1344 |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
1348 |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
1352 definition big : nat →nat ≝ λx.
1353 let m ≝ max (fst x) (snd x) in 〈m,m〉.
1355 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
1356 #a #b normalize >fst_pair >snd_pair // qed.
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 …))]
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〉).
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
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]
1391 definition out_aux ≝ λh.
1392 out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
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)
1402 [@(monotonic_CF … CF_fst) #x //
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 //]
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 …))
1423 |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
1426 |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
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)〉〉)
1437 #h #hconstr #hmono #hantimono
1438 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
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
1446 [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
1447 cut (max b n = n) [normalize >le_to_leb_true //] #maxb
1449 [@le_plus [>big_def >big_def >maxa >maxb //]
1451 [/2 by monotonic_le_minus_r/
1452 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
1454 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
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 //] |//]
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)〉〉.
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 //
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)
1480 (**************************** closing the argument ****************************)
1482 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
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)〉〉].
1488 lemma h_of_aux_O: ∀r,c,b.
1489 h_of_aux r c O b = c.
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)〉〉.
1498 lemma h_of_aux_prim_rec : ∀r,c,n,b. h_of_aux r c n b =
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.
1505 [>h_of_aux_O normalize //
1506 |#n1 #Hind >h_of_aux_S >prim_rec_S >snd_pair >snd_pair >fst_pair
1512 lemma h_of_aux_constr :
1513 ∀r,c. constructible (λx.h_of_aux r c (fst x) (snd x)).
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
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).
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) //
1533 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
1535 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
1536 #r #a #b normalize >fst_pair >snd_pair //
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 //]
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)
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]
1571 axiom h_of_constr : ∀r:nat →nat.
1572 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1573 constructible (h_of r).
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
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
1591 [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
1593 cut (max (S a) b = b)
1594 [whd in ⊢ (??%?); >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
1596 cut (∃d.b - a = S d)
1597 [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
1599 cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
1601 [@plus_to_minus >commutative_plus @minus_to_plus
1602 [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
1605 |#n #a #b #leab #lebn >h_of_def >h_of_def
1607 [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
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)
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 //
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 *
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) //
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 *
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)