1 include "reverse_complexity/complexity.ma".
2 include "reverse_complexity/sigma_diseq.ma".
4 include alias "reverse_complexity/basics.ma".
6 lemma bigop_prim_rec: ∀a,b,c,p,f,x.
7 bigop (b x-a x) (λi:ℕ.p 〈i+a x,x〉) ? (c 〈a x,x〉) plus (λi:ℕ.f 〈i+a x,x〉) =
9 (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
10 then plus (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
11 else fst (snd i)) (b x-a x) 〈a x ,x〉.
12 #a #b #c #p #f #x normalize elim (b x-a x)
15 >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
16 cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
17 [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
21 lemma bigop_prim_rec_dec: ∀a,b,c,p,f,x.
22 bigop (b x-a x) (λi:ℕ.p 〈b x -i,x〉) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈b x-i,x〉) =
24 (λi.if p 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉
25 then plus (f 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉) (fst (snd i))
26 else fst (snd i)) (b x-a x) 〈b x ,x〉.
27 #a #b #c #p #f #x normalize elim (b x-a x)
30 >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
31 cases (true_or_false (p 〈b x - i,x〉)) #Hcase >Hcase
32 [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
36 lemma bigop_prim_rec_dec1: ∀a,b,c,p,f,x.
37 bigop (S(b x)-a x) (λi:ℕ.p 〈b x - i,x〉) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈b x- i,x〉) =
39 (λi.if p 〈fst (snd (snd i)) - (fst i),snd (snd (snd i))〉
40 then plus (f 〈fst (snd (snd i)) - (fst i),snd (snd (snd i))〉) (fst (snd i))
41 else fst (snd i)) (S(b x)-a x) 〈b x,x〉.
42 #a #b #c #p #f #x elim (S(b x)-a x)
45 >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
46 cases (true_or_false (p 〈b x - i,x〉)) #Hcase >Hcase
47 [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
51 lemma sum_prim_rec1: ∀a,b,p,f,x.
52 ∑_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
54 (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
55 then f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉 + fst (snd i)
56 else fst (snd i)) (b x-a x) 〈a x ,x〉.
57 #a #b #p #f #x elim (b x-a x)
60 >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
61 cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
62 [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
66 lemma bigop_plus_c: ∀k,p,f,c.
67 c k + bigop k (λi.p i) ? 0 plus (λi.f i) =
68 bigop k (λi.p i) ? (c k) plus (λi.f i).
69 #k #p #f elim k [normalize //]
70 #i #Hind #c cases (true_or_false (p i)) #Hcase
71 [>bigop_Strue // >bigop_Strue // <associative_plus >(commutative_plus ? (f i))
72 >associative_plus @eq_f @Hind
73 |>bigop_Sfalse // >bigop_Sfalse //
78 (*********************************** maximum **********************************)
80 lemma max_gen: ∀a,b,p,f,x. a ≤b →
81 max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) = max_{i < b | leb a i ∧ p 〈i,x〉 }(f 〈i,x〉).
82 #a #b #p #f #x @(bigop_I_gen ????? MaxA)
85 lemma max_prim_rec_base: ∀a,b,p,f,x. a ≤b →
86 max_{i < b| p 〈i,x〉 }(f 〈i,x〉) =
88 (λi.if p 〈fst i,x〉 then max (f 〈fst i,snd (snd i)〉) (fst (snd i)) else fst (snd i)) b x.
89 #a #b #p #f #x #leab >max_gen // elim b
91 |#i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
92 cases (true_or_false (p 〈i,x〉)) #Hcase >Hcase
93 [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
97 lemma max_prim_rec: ∀a,b,p,f,x. a ≤b →
98 max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) =
100 (λ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.
101 #a #b #p #f #x #leab >max_gen // elim b
103 |#i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
104 cases (true_or_false (leb a i ∧ p 〈i,x〉)) #Hcase >Hcase
105 [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
109 lemma max_prim_rec1: ∀a,b,p,f,x.
110 max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
112 (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
113 then max (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
114 else fst (snd i)) (b x-a x) 〈a x ,x〉.
115 #a #b #p #f #x elim (b x-a x)
117 |#i #Hind >prim_rec_S
118 >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
119 cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
120 [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
124 (* the argument is 〈b-a,〈a,x〉〉 *)
126 definition max_unary_pr ≝ λp,f.unary_pr (λx.0)
129 let r ≝ fst (snd i) in
130 let a ≝ fst (snd (snd i)) in
131 let x ≝ snd (snd (snd i)) in
132 if p 〈k + a,x〉 then max (f 〈k+a,x〉) r else r).
134 lemma max_unary_pr1: ∀a,b,p,f,x.
135 max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
136 ((max_unary_pr p f) ∘ (λx.〈b x - a x,〈a x,x〉〉)) x.
137 #a #b #p #f #x normalize >fst_pair >snd_pair @max_prim_rec1
140 definition aux_compl ≝ λhp,hf.λi.
142 let r ≝ fst (snd i) in
143 let a ≝ fst (snd (snd i)) in
144 let x ≝ snd (snd (snd i)) in
145 hp 〈k+a,x〉 + hf 〈k+a,x〉 + (* was MSC r*) MSC i .
147 definition aux_compl1 ≝ λhp,hf.λi.
149 let r ≝ fst (snd i) in
150 let a ≝ fst (snd (snd i)) in
151 let x ≝ snd (snd (snd i)) in
152 hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
154 lemma aux_compl1_def: ∀k,r,m,hp,hf.
155 aux_compl1 hp hf 〈k,〈r,m〉〉 =
158 hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
159 #k #r #m #hp #hf normalize >fst_pair >snd_pair >snd_pair >fst_pair //
162 lemma aux_compl1_def1: ∀k,r,a,x,hp,hf.
163 aux_compl1 hp hf 〈k,〈r,〈a,x〉〉〉 = hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
164 #k #r #a #x #hp #hf normalize >fst_pair >snd_pair >snd_pair >fst_pair
165 >fst_pair >snd_pair //
168 axiom Oaux_compl: ∀hp,hf. O (aux_compl1 hp hf) (aux_compl hp hf).
170 lemma MSC_max: ∀f,h,x. CF h f → MSC (max_{i < x}(f i)) ≤ max_{i < x}(h i).
171 #f #h #x #hf elim x // #i #Hind >bigop_Strue [|//] >bigop_Strue [|//]
172 whd in match (max ??);
173 cases (true_or_false (leb (f i) (bigop i (λi0:ℕ.true) ? 0 max(λi0:ℕ.f i0))))
175 [@(transitive_le … Hind) @le_maxr //
176 |@(transitive_le … (MSC_out … hf i)) @le_maxl //
180 lemma CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
181 CF ha a → CF hb b → CF hp p → CF hf f →
182 O s (λx.ha x + hb x +
184 (hp 〈i,x〉 + hf 〈i,x〉 + max_{i ∈ [a x, b x [ }(hf 〈i,x〉)))) →
185 CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
186 #a #b #p #f #ha #hb #hp #hf #s #CFa #CFb #CFp #CFf #HO
187 @ext_CF1 [|#x @max_unary_pr1]
188 @(CF_comp ??? (λx.ha x + hb x))
190 [@CF_minus [@(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
192 [@(O_to_CF … CFa) @O_plus_l //
193 | @(O_to_CF … CF_id) @O_plus_r @le_to_O @(MSC_in … CFb)
196 |@(CF_prim_rec … MSC … (aux_compl1 hp hf))
198 |@(O_to_CF … (Oaux_compl … ))
200 [@(CF_comp p … MSC … CFp)
202 [@CF_plus [@CF_fst| @CF_comp_fst @CF_comp_snd @CF_snd]
203 |@CF_comp_snd @CF_comp_snd @CF_snd]
204 |@le_to_O #x normalize >commutative_plus >associative_plus @le_plus //
207 [@(CF_comp f … MSC … CFf)
209 [@CF_plus [@CF_fst| @CF_comp_fst @CF_comp_snd @CF_snd]
210 |@CF_comp_snd @CF_comp_snd @CF_snd]
211 |@le_to_O #x normalize >commutative_plus //
213 |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
215 |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
222 +bigop (b x-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus
226 +bigop (b x-a x) (λi1:ℕ.true) ? 0 max
227 (λi1:ℕ.(λi2:ℕ.hf 〈i2,x〉) (i1+a x))) (i+a x))))
229 @le_to_O #n @le_plus // whd in match (unary_pr ???);
230 >fst_pair >snd_pair >bigop_prim_rec elim (b n - a n)
232 |#x #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >aux_compl1_def1
233 >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >fst_pair
234 >snd_pair normalize in ⊢ (??%); >commutative_plus @le_plus
235 [-Hind @le_plus // normalize >fst_pair >snd_pair
236 @(transitive_le ? (bigop x (λi1:ℕ.true) ? 0 (λn0:ℕ.λm:ℕ.if leb n0 m then m else n0 )
237 (λi1:ℕ.hf 〈i1+a n,n〉)))
238 [elim x [normalize @MSC_le]
239 #x0 #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >snd_pair
240 >fst_pair >fst_pair cases (p 〈x0+a n,n〉) normalize
241 [cases (true_or_false (leb (f 〈x0+a n,n〉)
244 .if p 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
245 then if leb (f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉)
248 else f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
249 else fst (snd i) ) x0 〈a n,n〉))) #Hcase >Hcase normalize
250 [@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
251 |@(transitive_le … (MSC_out … CFf …)) @(le_maxl … (le_n …))
253 |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
255 |@(le_maxr … (le_n …))
257 |@(transitive_le … Hind) -Hind
258 generalize in match (bigop x (λi:ℕ.true) ? 0 max
259 (λi1:ℕ.(λi2:ℕ.hf 〈i2,n〉) (i1+a n))); #c
260 generalize in match (hf 〈x+a n,n〉); #c1
261 elim x [//] #x0 #Hind
262 >prim_rec_S >prim_rec_S normalize >fst_pair >fst_pair >snd_pair
263 >snd_pair >snd_pair >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair
265 [@le_plus // cases (true_or_false (leb c1 c)) #Hcase
266 >Hcase normalize // @lt_to_le @not_le_to_lt @(leb_false_to_not_le ?? Hcase)
271 |@O_plus [@O_plus_l //] @le_to_O #x
272 <bigop_plus_c @le_plus // @(transitive_le … (MSC_pair …)) @le_plus
273 [@MSC_out @CFa | @MSC_out @(O_to_CF MSC … (CF_const x)) @le_to_O @(MSC_in … CFb)]
277 axiom daemon : ∀P:Prop.P.
278 axiom O_extl: ∀s1,s2,f. (∀x.s1 x = s2 x) → O s1 f → O s2 f.
280 lemma CF_max2: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
281 CF ha a → CF hb b → CF hp p → CF hf f →
282 O s (λx.ha x + hb x +
283 (b x - a x)*max_{i ∈ [a x, b x [ }(hp 〈i,x〉 + hf 〈i,x〉)) →
284 CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
285 #a #b #p #f #ha #hb #hp #hf #s #CFa #CFb #CFp #CFf #Os
286 @(O_to_CF … Os (CF_max … CFa CFb CFp CFf ?)) @O_plus
288 |@O_plus_r @O_ext2 [|| #x @(bigop_op … plusAC)]
290 [@le_to_O normalize #x @sigma_to_Max
291 |@le_to_O #x @transitive_le [|@sigma_const] @le_times //
292 @Max_le #i #lti #_ @(transitive_le ???? (le_MaxI … ))
293 [@le_plus_n | // | @lt_minus_to_plus_r // | //]
299 lemma CF_max_monotonic: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
300 CF ha a → CF hb b → CF hp p → CF hf f →
301 O s (λx.ha x + hb x +
302 (b x - a x)*max_{i ∈ [a x, b x [ }(hp 〈i,x〉 + hf 〈i,x〉)) →
303 CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
304 #a #b #p #f #ha #hb #hp #hf #s #CFa #CFb #CFp #CFf #Os
305 @(O_to_CF … Os (CF_max … CFa CFb CFp CFf ?)) @O_plus
307 |@O_plus_r @O_ext2 [|| #x @(bigop_op … plusAC)]
309 [@le_to_O normalize #x @sigma_to_Max
310 |@le_to_O #x @transitive_le [|@sigma_const] @le_times //
311 @Max_le #i #lti #_ @(transitive_le ???? (le_MaxI … ))
312 [@le_plus_n | // | @lt_minus_to_plus_r // | //]
319 axiom CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
320 CF ha a → CF hb b → CF hp p → CF hf f →
321 O s (λx.ha x + hb x + ∑_{i ∈[a x ,b x[ }(hp 〈i,x〉 + hf 〈i,x〉)) →
322 CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)). *)
324 (******************************** minimization ********************************)
326 let rec my_minim a f x k on k ≝
329 |S p ⇒ if eqb (my_minim a f x p) (a+p)
330 then if f 〈a+p,x〉 then a+p else S(a+p)
331 else (my_minim a f x p) ].
333 lemma my_minim_S : ∀a,f,x,k.
334 my_minim a f x (S k) =
335 if eqb (my_minim a f x k) (a+k)
336 then if f 〈a+k,x〉 then a+k else S(a+k)
337 else (my_minim a f x k) .
340 lemma my_minim_fa : ∀a,f,x,k. f〈a,x〉 = true → my_minim a f x k = a.
341 #a #f #x #k #H elim k // #i #Hind normalize >Hind
342 cases (true_or_false (eqb a (a+i))) #Hcase >Hcase normalize //
343 <(eqb_true_to_eq … Hcase) >H //
346 lemma my_minim_nfa : ∀a,f,x,k. f〈a,x〉 = false →
347 my_minim a f x (S k) = my_minim (S a) f x k.
348 #a #f #x #k #H elim k
349 [normalize <plus_n_O >H >eq_to_eqb_true //
350 |#i #Hind >my_minim_S >Hind >my_minim_S <plus_n_Sm //
354 lemma my_min_eq : ∀a,f,x,k.
355 min k a (λi.f 〈i,x〉) = my_minim a f x k.
356 #a #f #x #k lapply a -a elim k // #i #Hind #a normalize in ⊢ (??%?);
357 cases (true_or_false (f 〈a,x〉)) #Hcase >Hcase
358 [>(my_minim_fa … Hcase) // | >Hind @sym_eq @(my_minim_nfa … Hcase) ]
361 (* cambiare qui: togliere S *)
364 definition minim_unary_pr ≝ λf.unary_pr (λx.S(fst x))
367 let r ≝ fst (snd i) in
368 let b ≝ fst (snd (snd i)) in
369 let x ≝ snd (snd (snd i)) in
370 if f 〈b-k,x〉 then b-k else r).
372 definition compl_minim_unary ≝ λhf:nat → nat.λi.
374 let b ≝ fst (snd (snd i)) in
375 let x ≝ snd (snd (snd i)) in
376 hf 〈b-k,x〉 + MSC 〈k,〈S b,x〉〉.
378 definition compl_minim_unary_aux ≝ λhf,i.
380 let r ≝ fst (snd i) in
381 let b ≝ fst (snd (snd i)) in
382 let x ≝ snd (snd (snd i)) in
385 lemma compl_minim_unary_aux_def : ∀hf,k,r,b,x.
386 compl_minim_unary_aux hf 〈k,〈r,〈b,x〉〉〉 = hf 〈b-k,x〉 + MSC 〈k,〈r,〈b,x〉〉〉.
387 #hf #k #r #b #x normalize >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair //
390 lemma compl_minim_unary_def : ∀hf,k,r,b,x.
391 compl_minim_unary hf 〈k,〈r,〈b,x〉〉〉 = hf 〈b-k,x〉 + MSC 〈k,〈S b,x〉〉.
392 #hf #k #r #b #x normalize >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair //
395 lemma compl_minim_unary_aux_def2 : ∀hf,k,r,x.
396 compl_minim_unary_aux hf 〈k,〈r,x〉〉 = hf 〈fst x-k,snd x〉 + MSC 〈k,〈r,x〉〉.
397 #hf #k #r #x normalize >snd_pair >snd_pair >fst_pair //
400 lemma compl_minim_unary_def2 : ∀hf,k,r,x.
401 compl_minim_unary hf 〈k,〈r,x〉〉 = hf 〈fst x-k,snd x〉 + MSC 〈k,〈S(fst x),snd x〉〉.
402 #hf #k #r #x normalize >snd_pair >snd_pair >fst_pair //
405 lemma min_aux: ∀a,f,x,k. min (S k) (a x) (λi:ℕ.f 〈i,x〉) =
406 ((minim_unary_pr f) ∘ (λx.〈S k,〈a x + k,x〉〉)) x.
407 #a #f #x #k whd in ⊢ (???%); >fst_pair >snd_pair
408 lapply a -a (* @max_prim_rec1 *)
410 [normalize #a >fst_pair >snd_pair >fst_pair >snd_pair >snd_pair >fst_pair
411 <plus_n_O <minus_n_O >fst_pair //
412 |#i #Hind #a normalize in ⊢ (??%?); >prim_rec_S >fst_pair >snd_pair
413 >fst_pair >snd_pair >snd_pair >fst_pair <plus_n_Sm <(Hind (λx.S (a x)))
414 whd in ⊢ (???%); >minus_S_S <(minus_plus_m_m (a x) i) //
417 lemma minim_unary_pr1: ∀a,b,f,x.
418 μ_{i ∈[a x,b x]}(f 〈i,x〉) =
419 if leb (a x) (b x) then ((minim_unary_pr f) ∘ (λx.〈S (b x) - a x,〈b x,x〉〉)) x
421 #a #b #f #x cases (true_or_false (leb (a x) (b x))) #Hcase >Hcase
422 [cut (b x = a x + (b x - a x))
423 [>commutative_plus <plus_minus_m_m // @leb_true_to_le // ]
424 #Hcut whd in ⊢ (???%); >minus_Sn_m [|@leb_true_to_le //]
425 >min_aux whd in ⊢ (??%?); <Hcut //
426 |>eq_minus_O // @not_le_to_lt @leb_false_to_not_le //
430 axiom sum_inv: ∀a,b,f.∑_{i ∈ [a,S b[ }(f i) = ∑_{i ∈ [a,S b[ }(f (a + b - i)).
433 #a #b #f @(bigop_iso … plusAC) whd %{(λi.b - a - i)} %{(λi.b - a -i)} %
434 [%[#i #lti #_ normalize @eq_f >commutative_plus <plus_minus_associative
435 [2: @le_minus_to_plus_r //
436 [// @eq_f @@sym_eq @plus_to_minus
437 |#i #Hi #_ % [% [@le_S_S
440 example sum_inv_check : ∑_{i ∈ [3,6[ }(i*i) = ∑_{i ∈ [3,6[ }((8-i)*(8-i)).
443 (* rovesciamo la somma *)
445 lemma CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
446 CF sa a → CF sb b → CF sf f →
447 O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉 + MSC 〈b x - i,〈S(b x),x〉〉)) →
448 CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
449 #a #b #f #ha #hb #hf #s #CFa #CFb #CFf #HO
450 @ext_CF1 [|#x @minim_unary_pr1]
452 [@CF_le @(O_to_CF … HO)
453 [@(O_to_CF … CFa) @O_plus_l @O_plus_l @O_refl
454 |@(O_to_CF … CFb) @O_plus_l @O_plus_r @O_refl
456 |@(CF_comp ??? (λx.ha x + hb x))
458 [@CF_minus [@CF_compS @(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
460 [@(O_to_CF … CFb) @O_plus_r //
461 |@(O_to_CF … CF_id) @O_plus_r @le_to_O @(MSC_in … CFb)
464 |@(CF_prim_rec_gen … MSC … (compl_minim_unary_aux hf))
466 +compl_minim_unary hf
470 .(let (k:ℕ) ≝fst i in
471 let (r:ℕ) ≝fst (snd i) in
472 let (b:ℕ) ≝fst (snd (snd i)) in
473 let (x:ℕ) ≝snd (snd (snd i)) in if f 〈b-S k,x〉 then b-S k else r ))
478 [@(CF_comp f … MSC … CFf)
480 [@CF_minus [@CF_comp_fst @CF_comp_snd @CF_snd|@CF_fst]
481 |@CF_comp_snd @CF_comp_snd @CF_snd]
482 |@le_to_O #x normalize >commutative_plus //
485 [@le_to_O #x normalize //
487 [@CF_comp_fst @CF_comp_snd @CF_snd |@CF_fst]
489 |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
493 |@O_plus_r @O_ext2 [||#x >compl_minim_unary_aux_def2 @refl]
494 @O_trans [||@le_to_O #x >compl_minim_unary_def2 @le_n]
495 @O_plus [@O_plus_l //]
497 @O_trans [|@le_to_O #x @MSC_pair] @O_plus
498 [@le_to_O #x @monotonic_MSC @(transitive_le ???? (le_fst …))
500 @O_trans [|@le_to_O #x @MSC_pair] @O_plus
501 [@le_to_O #x @monotonic_MSC @(transitive_le ???? (le_snd …))
502 >snd_pair @(transitive_le ???? (le_fst …)) >fst_pair
503 normalize >snd_pair >fst_pair lapply (surj_pair x)
504 * #x1 * #x2 #Hx >Hx >fst_pair >snd_pair elim x1 //
505 #i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
506 cases (f ?) [@le_S // | //]]
507 @le_to_O #x @monotonic_MSC @(transitive_le ???? (le_snd …)) >snd_pair
508 >(expand_pair (snd (snd x))) in ⊢ (?%?); @le_pair //
511 |cut (O s (λx.ha x + hb x +
512 ∑_{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〉〉)))
513 [@(O_ext2 … HO) #x @eq_f @sum_inv] -HO #HO
515 @(O_trans ? (λx:ℕ.ha x+hb x
516 +bigop (S(b x)-a x) (λi:ℕ.true) ?
517 (MSC 〈b x,x〉) plus (λi:ℕ.(λj.hf j + MSC 〈b x - fst j,〈S(b (snd j)),snd j〉〉) 〈b x- i,x〉)))
518 [@le_to_O #n @le_plus // whd in match (unary_pr ???);
519 >fst_pair >snd_pair >(bigop_prim_rec_dec1 a b ? (λi.true))
520 (* it is crucial to recall that the index is bound by S(b x) *)
521 cut (S (b n) - a n ≤ S (b n)) [//]
524 |#x #Hind #lex >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair
525 >compl_minim_unary_def >prim_rec_S >fst_pair >snd_pair >fst_pair
526 >snd_pair >fst_pair >snd_pair >fst_pair whd in ⊢ (??%); >commutative_plus
527 @le_plus [2:@Hind @le_S @le_S_S_to_le @lex] -Hind >snd_pair
528 >minus_minus_associative // @le_S_S_to_le //
530 |@O_plus [@O_plus_l //] @O_ext2 [||#x @bigop_plus_c]
532 [@O_plus_l @O_trans [|@le_to_O #x @MSC_pair]
534 [@O_plus_r @le_to_O @(MSC_out … CFb)
535 |@O_plus_r @le_to_O @(MSC_in … CFb)
537 |@O_plus_r @(O_ext2 … (O_refl …)) #x @same_bigop
538 [//|#i #H #_ @eq_f2 [@eq_f @eq_f2 //|>fst_pair @eq_f @eq_f2 //]
543 |@(O_to_CF … CFa) @(O_trans … HO) @O_plus_l @O_plus_l @O_refl
548 lemma CF_mu2: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
549 CF sa a → CF sb b → CF sf f →
550 O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉 + MSC〈S(b x),x〉)) →
551 CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
552 #a #b #f #sa #sb #sf #s #CFa #CFb #CFf #HO
553 @(O_to_CF … HO (CF_mu … CFa CFb CFf ?)) @O_plus [@O_plus_l @O_refl]
554 @O_plus_r @O_ext2 [|| #x @(bigop_op … plusAC)]
555 @O_plus [@le_to_O #x @le_sigma //]
556 @(O_trans ? (λx.∑_{i ∈[a x ,S(b x)[ }(MSC(b x -i)+MSC 〈S(b x),x〉)))
557 [@le_to_O #x @le_sigma //]
558 @O_ext2 [|| #x @(bigop_op … plusAC)] @O_plus
559 [@le_to_O #x @le_sigma // #i #lti #_ @(transitive_le … (MSC 〈S (b x),x〉)) //
560 @monotonic_MSC @(transitive_le … (S(b x))) // @le_S //
561 |@le_to_O #x @le_sigma //
567 lemma CF_mu3: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s. (∀x.sf x > 0) →
568 CF sa a → CF sb b → CF sf f →
569 O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉 + MSC〈b x,x〉)) →
570 CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
571 #a #b #f #sa #sb #sf #s #sfpos #CFa #CFb #CFf #HO
572 @(O_to_CF … HO (CF_mu2 … CFa CFb CFf ?)) @O_plus [@O_plus_l @O_refl]
573 @O_plus_r @O_ext2 [|| #x @(bigop_op … plusAC)]
574 @O_plus [@le_to_O #x @le_sigma //]
575 @le_to_O #x @le_sigma // #x #lti #_ >MSC_pair_eq >MSC_pair_eq <associative_plus
576 @le_plus // @(transitive_le … (MSC_sublinear … )) /2 by monotonic_lt_plus_l/
579 lemma CF_mu4: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s. (∀x.sf x > 0) →
580 CF sa a → CF sb b → CF sf f →
581 O s (λx.sa x + sb x + (S(b x) - a x)*Max_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
582 CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)).
583 #a #b #f #sa #sb #sf #s #sfpos #CFa #CFb #CFf #HO
584 @(O_to_CF … HO (CF_mu3 … sfpos CFa CFb CFf ?)) @O_plus [@O_plus_l @O_refl]
585 @O_ext2 [|| #x @(bigop_op … plusAC)] @O_plus_r @O_plus
586 [@le_to_O #x @sigma_to_Max
587 |lapply (MSC_in … CFf) #Hle
588 %{1} %{0} #n #_ @(transitive_le … (sigma_const …))
589 >(commutative_times 1) <times_n_1
590 cases (decidable_le (S (b n)) (a n)) #H
591 [>(eq_minus_O … H) //
592 |lapply (le_S_S_to_le … (not_le_to_lt … H)) -H #H
593 @le_times // @(transitive_le … (Hle … ))
594 cut (b n = b n - a n + a n) [<plus_minus_m_m // ]
595 #Hcut >Hcut in ⊢ (?%?); @(le_Max (λi.sf 〈i+a n,n〉)) /2/
601 axiom CF_mu: ∀a,b.∀f:nat →bool.∀sa,sb,sf,s.
602 CF sa a → CF sb b → CF sf f →
603 O s (λx.sa x + sb x + ∑_{i ∈[a x ,S(b x)[ }(sf 〈i,x〉)) →
604 CF s (λx.μ_{i ∈[a x,b x] }(f 〈i,x〉)). *)