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 lemma max_prim_rec1: ∀a,b,p,f,x.
389 max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
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)
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 // ]
403 lemma sum_prim_rec1: ∀a,b,p,f,x.
404 ∑_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
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)
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 // ]
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〉) =
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)
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 // ]
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〉) =
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)
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 // ]
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〉) =
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)
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 // ]
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 //
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〉) =
472 (λi. plus (f 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉) (fst (snd i)))
474 #a #b #c #f #x normalize elim (b x-a x)
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 // ]
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 //
493 (* the argument is 〈b-a,〈a,x〉〉 *)
496 definition max_unary_pr ≝ λp,f.unary_pr (λx.0)
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).
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
511 lemma max_unary_pr: ∀a,b,p,f,x.
512 max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) =
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.
518 definition unary_compl ≝ λp,f,hf.
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)〉,
533 definition aux_compl ≝ λhp,hf.λi.
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 .
540 definition aux_compl1 ≝ λhp,hf.λi.
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.
547 lemma aux_compl1_def: ∀k,r,m,hp,hf.
548 aux_compl1 hp hf 〈k,〈r,m〉〉 =
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 //
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 //
562 axiom Oaux_compl: ∀hp,hf. O (aux_compl1 hp hf) (aux_compl hp hf).
565 definition IF ≝ λb,f,g:nat →option nat. λx.
568 |Some n ⇒ if (eqb n 0) then f x else g x].
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).
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 //
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).
590 axiom MSC_prop: ∀f,h. CF h f → ∀x. MSC (f x) ≤ h x.
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))))
597 [@(transitive_le … Hind) @le_maxr //
598 |@(transitive_le … (MSC_prop … hf i)) @le_maxl //
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 +
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))
612 [@CF_minus [@(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
614 [@(O_to_CF … CFa) @O_plus_l //
615 | @(O_to_CF … CF_id) @O_plus_r @(proj1 … CFb)
618 |@(CF_prim_rec … MSC … (aux_compl1 hp hf))
620 |@(O_to_CF … (Oaux_compl … ))
622 [@(CF_comp p … MSC … CFp)
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 //
629 [@(CF_comp f … MSC … CFf)
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 //
635 |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
637 |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
644 +bigop (b x-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus
648 +bigop (b x-a x) (λi1:ℕ.true) ? 0 max
649 (λi1:ℕ.(λi2:ℕ.hf 〈i2,x〉) (i1+a x))) (i+a x))))
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)
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〉)
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))〉)
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 …))
675 |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
677 |@(le_maxr … (le_n …))
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
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)
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)]
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〉)). *)
705 (******************************** minimization ********************************)
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 ≝
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) ].
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) .
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 //
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 //
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) ]
748 (* cambiare qui: togliere S *)
751 definition minim_unary_pr ≝ λf.unary_pr (λx.S(fst x))
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).
759 definition compl_minim_unary ≝ λhf:nat → nat.λi.
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〉〉.
765 definition compl_minim_unary_aux ≝ λhf,i.
767 let r ≝ fst (snd i) in
768 let b ≝ fst (snd (snd i)) in
769 let x ≝ snd (snd (snd i)) in
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 //
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 //
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 //
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 //
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 *)
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) //
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
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 //
817 axiom sum_inv: ∀a,b,f.∑_{i ∈ [a,S b[ }(f i) = ∑_{i ∈ [a,S b[ }(f (a + b - i)).
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
827 example sum_inv_check : ∑_{i ∈ [3,6[ }(i*i) = ∑_{i ∈ [3,6[ }((8-i)*(8-i)).
830 (* provo rovesciando la somma *)
832 axiom daemon: ∀P:Prop.P.
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]
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
845 |@(CF_comp ??? (λx.ha x + hb x))
847 [@CF_minus [@CF_compS @(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
849 [@(O_to_CF … CFb) @O_plus_r //
850 |@(O_to_CF … CF_id) @O_plus_r @(proj1 … CFb)
853 |@(CF_prim_rec_gen … MSC … (compl_minim_unary_aux hf))
855 +compl_minim_unary hf
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 ))
867 [@(CF_comp f … MSC … CFf)
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 //
874 [@le_to_O #x normalize //
876 [@CF_comp_fst @CF_comp_snd @CF_snd |@CF_fst]
878 |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
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 //]
886 @O_trans [|@le_to_O #x @MSC_pair] @O_plus
887 [@le_to_O #x @monotonic_MSC @(transitive_le ???? (le_fst …))
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 //
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
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)) [//]
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 //
919 |@O_plus [@O_plus_l //] @O_ext2 [||#x @bigop_plus_c]
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 //]
929 |@(O_to_CF … CFa) @(O_trans … HO) @O_plus_l @O_plus_l @O_refl
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))
942 [@CF_minus [@CF_compS @(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
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)
948 |@(CF_prim_rec … MSC … (compl_minim_unary_aux hf))
951 [@(CF_comp f … MSC … CFf)
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 //
958 [@le_to_O #x normalize //
960 [@CF_comp_fst @CF_comp_snd @CF_snd |@CF_compS @CF_fst]
962 |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
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〉)
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))〉)
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 …))
994 |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
996 |@(le_maxr … (le_n …))
1002 +bigop (b x-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus
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))))
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)
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)
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))〉)
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 …))
1033 |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
1035 |@(le_maxr … (le_n …))
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
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)
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)]
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〉)).*)
1062 (************************************* smn ************************************)
1063 axiom smn: ∀f,s. CF s f → ∀x. CF (λy.s 〈x,y〉) (λy.f 〈x,y〉).
1065 (****************************** constructibility ******************************)
1067 definition constructible ≝ λs. CF s s.
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 | //]
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 //
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 ???);
1084 whd in match (unary_pr ???); >fst_pair >snd_pair elim a
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 //
1093 (********************************* simulation *********************************)
1095 axiom sU : nat → nat.
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〉〉.
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
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〉〉.
1113 definition pU_unary ≝ λp. pU (fst p) (fst (snd p)) (snd (snd p)).
1115 axiom CF_U : CF sU pU_unary.
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)).
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 %
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 %
1131 (******************** complexity of g ********************)
1133 (*definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
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))).
1138 lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
1139 #h #s #H1 @(CF_compS ? (auxg h) H1)
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〉).
1146 lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
1148 [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
1151 lemma compl_g2 : ∀h,s1,s2,s.
1153 (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
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〉)) →
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 //]
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 //
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〉).
1175 lemma min_input_eq : ∀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 //
1182 definition termb_aux ≝ λh.
1183 termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
1185 lemma compl_g4 : ∀h,s1,s.
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)
1194 |@CF_comp_snd @CF_snd
1195 |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
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/]
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);
1212 |#m #Hind >bigop_Strue [2://] @le_plus
1213 [@H @le_n |@(transitive_le … Hind) @le_times [//] @H //]
1215 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
1216 cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
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);
1226 |#m #Hind >bigop_Strue [2://] #Hm
1227 cut (m+a ≤ b) [@(transitive_le … Hm) //] #Hm1
1228 @le_plus [@H // |@(transitive_le … (Hind Hm1)) //]
1230 |#ltba lapply (not_le_to_lt … ltba) -ltba #ltba
1231 cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
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 //]
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
1248 (**************************** end of technical lemmas *************************)
1250 (*lemma compl_g5 : ∀h,s1.(∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
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]
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)
1267 [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
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 //]
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 …))
1290 |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
1294 |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
1298 definition big : nat →nat ≝ λx.
1299 let m ≝ max (fst x) (snd x) in 〈m,m〉.
1301 lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
1302 #a #b normalize >fst_pair >snd_pair // qed.
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 …))]
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〉).
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
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]
1337 definition out_aux ≝ λh.
1338 out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
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)
1348 [@(monotonic_CF … CF_fst) #x //
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 //]
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 …))
1369 |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
1372 |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
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)〉〉)
1383 #h #hconstr #hmono #hantimono
1384 @(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
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
1392 [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
1393 cut (max b n = n) [normalize >le_to_leb_true //] #maxb
1395 [@le_plus [>big_def >big_def >maxa >maxb //]
1397 [/2 by monotonic_le_minus_r/
1398 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
1400 |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
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 //] |//]
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)〉〉.
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 //
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)
1426 (**************************** closing the argument ****************************)
1428 let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
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)〉〉].
1434 lemma h_of_aux_O: ∀r,c,b.
1435 h_of_aux r c O b = c.
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)〉〉.
1444 lemma h_of_aux_prim_rec : ∀r,c,n,b. h_of_aux r c n b =
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.
1451 [>h_of_aux_O normalize //
1452 |#n1 #Hind >h_of_aux_S >prim_rec_S >snd_pair >snd_pair >fst_pair
1458 lemma h_of_aux_constr :
1459 ∀r,c. constructible (λx.h_of_aux r c (fst x) (snd x)).
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
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).
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) //
1479 lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
1481 h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
1482 #r #a #b normalize >fst_pair >snd_pair //
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 //]
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)
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]
1517 axiom h_of_constr : ∀r:nat →nat.
1518 (∀x. x ≤ r x) → monotonic ? le r → constructible r →
1519 constructible (h_of r).
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
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
1537 [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
1539 cut (max (S a) b = b)
1540 [whd in ⊢ (??%?); >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
1542 cut (∃d.b - a = S d)
1543 [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
1545 cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
1547 [@plus_to_minus >commutative_plus @minus_to_plus
1548 [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
1551 |#n #a #b #leab #lebn >h_of_def >h_of_def
1553 [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
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)
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 //
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 *
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) //
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 *
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)