--- /dev/null
+include "reverse_complexity/bigops_compl.ma".
+
+(********************************* the speedup ********************************)
+
+definition min_input ≝ λh,i,x. μ_{y ∈ [S i,x] } (termb i y (h (S i) y)).
+
+lemma min_input_def : ∀h,i,x.
+ min_input h i x = min (x -i) (S i) (λy.termb i y (h (S i) y)).
+// qed.
+
+lemma min_input_i: ∀h,i,x. x ≤ i → min_input h i x = S i.
+#h #i #x #lexi >min_input_def
+cut (x - i = 0) [@sym_eq /2 by eq_minus_O/] #Hcut //
+qed.
+
+lemma min_input_to_terminate: ∀h,i,x.
+ min_input h i x = x → {i ⊙ x} ↓ (h (S i) x).
+#h #i #x #Hminx
+cases (decidable_le (S i) x) #Hix
+ [cases (true_or_false (termb i x (h (S i) x))) #Hcase
+ [@termb_true_to_term //
+ |<Hminx in Hcase; #H lapply (fmin_false (λx.termb i x (h (S i) x)) (x-i) (S i) H)
+ >min_input_def in Hminx; #Hminx >Hminx in ⊢ (%→?);
+ <plus_n_Sm <plus_minus_m_m [2: @lt_to_le //]
+ #Habs @False_ind /2/
+ ]
+ |@False_ind >min_input_i in Hminx;
+ [#eqix >eqix in Hix; * /2/ | @le_S_S_to_le @not_le_to_lt //]
+ ]
+qed.
+
+lemma min_input_to_lt: ∀h,i,x.
+ min_input h i x = x → i < x.
+#h #i #x #Hminx cases (decidable_le (S i) x) //
+#ltxi @False_ind >min_input_i in Hminx;
+ [#eqix >eqix in ltxi; * /2/ | @le_S_S_to_le @not_le_to_lt //]
+qed.
+
+lemma le_to_min_input: ∀h,i,x,x1. x ≤ x1 →
+ min_input h i x = x → min_input h i x1 = x.
+#h #i #x #x1 #lex #Hminx @(min_exists … (le_S_S … lex))
+ [@(fmin_true … (sym_eq … Hminx)) //
+ |@(min_input_to_lt … Hminx)
+ |#j #H1 <Hminx @lt_min_to_false //
+ |@plus_minus_m_m @le_S_S @(transitive_le … lex) @lt_to_le
+ @(min_input_to_lt … Hminx)
+ ]
+qed.
+
+definition g ≝ λh,u,x.
+ S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
+
+lemma g_def : ∀h,u,x. g h u x =
+ S (max_{i ∈[u,x[ | eqb (min_input h i x) x} (out i x (h (S i) x))).
+// qed.
+
+lemma le_u_to_g_1 : ∀h,u,x. x ≤ u → g h u x = 1.
+#h #u #x #lexu >g_def cut (x-u = 0) [/2 by minus_le_minus_minus_comm/]
+#eq0 >eq0 normalize // qed.
+
+lemma g_lt : ∀h,i,x. min_input h i x = x →
+ out i x (h (S i) x) < g h 0 x.
+#h #i #x #H @le_S_S @(le_MaxI … i) /2 by min_input_to_lt/
+qed.
+
+lemma max_neq0 : ∀a,b. max a b ≠ 0 → a ≠ 0 ∨ b ≠ 0.
+#a #b whd in match (max a b); cases (true_or_false (leb a b)) #Hcase >Hcase
+ [#H %2 @H | #H %1 @H]
+qed.
+
+definition almost_equal ≝ λf,g:nat → nat. ¬ ∀nu.∃x. nu < x ∧ f x ≠ g x.
+interpretation "almost equal" 'napart f g = (almost_equal f g).
+
+lemma eventually_cancelled: ∀h,u.¬∀nu.∃x. nu < x ∧
+ max_{i ∈ [0,u[ | eqb (min_input h i x) x} (out i x (h (S i) x)) ≠ 0.
+#h #u elim u
+ [normalize % #H cases (H u) #x * #_ * #H1 @H1 //
+ |#u0 @not_to_not #Hind #nu cases (Hind nu) #x * #ltx
+ cases (true_or_false (eqb (min_input h (u0+O) x) x)) #Hcase
+ [>bigop_Strue [2:@Hcase] #Hmax cases (max_neq0 … Hmax) -Hmax
+ [2: #H %{x} % // <minus_n_O @H]
+ #Hneq0 (* if x is not enough we retry with nu=x *)
+ cases (Hind x) #x1 * #ltx1
+ >bigop_Sfalse
+ [#H %{x1} % [@transitive_lt //| <minus_n_O @H]
+ |@not_eq_to_eqb_false >(le_to_min_input … (eqb_true_to_eq … Hcase))
+ [@lt_to_not_eq @ltx1 | @lt_to_le @ltx1]
+ ]
+ |>bigop_Sfalse [2:@Hcase] #H %{x} % // <minus_n_O @H
+ ]
+ ]
+qed.
+
+lemma condition_1: ∀h,u.g h 0 ≈ g h u.
+#h #u @(not_to_not … (eventually_cancelled h u))
+#H #nu cases (H (max u nu)) #x * #ltx #Hdiff
+%{x} % [@(le_to_lt_to_lt … ltx) @(le_maxr … (le_n …))] @(not_to_not … Hdiff)
+#H @(eq_f ?? S) >(bigop_sumI 0 u x (λi:ℕ.eqb (min_input h i x) x) nat 0 MaxA)
+ [>H // |@lt_to_le @(le_to_lt_to_lt …ltx) /2 by le_maxr/ |//]
+qed.
+
+(******************************** Condition 2 *********************************)
+
+lemma exists_to_exists_min: ∀h,i. (∃x. i < x ∧ {i ⊙ x} ↓ h (S i) x) → ∃y. min_input h i y = y.
+#h #i * #x * #ltix #Hx %{(min_input h i x)} @min_spec_to_min @found //
+ [@(f_min_true (λy:ℕ.termb i y (h (S i) y))) %{x} % [% // | @term_to_termb_true //]
+ |#y #leiy #lty @(lt_min_to_false ????? lty) //
+ ]
+qed.
+
+lemma condition_2: ∀h,i. code_for (total (g h 0)) i → ¬∃x. i<x ∧ {i ⊙ x} ↓ h (S i) x.
+#h #i whd in ⊢(%→?); #H % #H1 cases (exists_to_exists_min … H1) #y #Hminy
+lapply (g_lt … Hminy)
+lapply (min_input_to_terminate … Hminy) * #r #termy
+cases (H y) -H #ny #Hy
+cut (r = g h 0 y) [@(unique_U … ny … termy) @Hy //] #Hr
+whd in match (out ???); >termy >Hr
+#H @(absurd ? H) @le_to_not_lt @le_n
+qed.
+
+(**************************** complexity of g *********************************)
+
+definition unary_g ≝ λh.λux. g h (fst ux) (snd ux).
+definition auxg ≝
+ λh,ux. max_{i ∈[fst ux,snd ux[ | eqb (min_input h i (snd ux)) (snd ux)}
+ (out i (snd ux) (h (S i) (snd ux))).
+
+lemma compl_g1 : ∀h,s. CF s (auxg h) → CF s (unary_g h).
+#h #s #H1 @(CF_compS ? (auxg h) H1)
+qed.
+
+definition aux1g ≝
+ λh,ux. max_{i ∈[fst ux,snd ux[ | (λp. eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) 〈i,ux〉}
+ ((λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) 〈i,ux〉).
+
+lemma eq_aux : ∀h,x.aux1g h x = auxg h x.
+#h #x @same_bigop
+ [#n #_ >fst_pair >snd_pair // |#n #_ #_ >fst_pair >snd_pair //]
+qed.
+
+lemma compl_g2 : ∀h,s1,s2,s.
+ CF s1
+ (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))) →
+ CF s2
+ (λp:ℕ.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p)))) →
+ O s (λx.MSC x + (snd x - fst x)*Max_{i ∈[fst x ,snd x[ }(s1 〈i,x〉+s2 〈i,x〉)) →
+ CF s (auxg h).
+#h #s1 #s2 #s #Hs1 #Hs2 #HO @(ext_CF (aux1g h))
+ [#n whd in ⊢ (??%%); @eq_aux]
+@(CF_max2 … CF_fst CF_snd Hs1 Hs2 …) @(O_trans … HO)
+@O_plus [@O_plus @O_plus_l // | @O_plus_r //]
+qed.
+
+lemma compl_g3 : ∀h,s.
+ CF s (λp:ℕ.min_input h (fst p) (snd (snd p))) →
+ CF s (λp:ℕ.eqb (min_input h (fst p) (snd (snd p))) (snd (snd p))).
+#h #s #H @(CF_eqb … H) @(CF_comp … CF_snd CF_snd) @(O_trans … (le_to_O … (MSC_in … H)))
+@O_plus // %{1} %{0} #n #_ >commutative_times <times_n_1 @monotonic_MSC //
+qed.
+
+definition min_input_aux ≝ λh,p.
+ μ_{y ∈ [S (fst p),snd (snd p)] }
+ ((λx.termb (fst (snd x)) (fst x) (h (S (fst (snd x))) (fst x))) 〈y,p〉).
+
+lemma min_input_eq : ∀h,p.
+ min_input_aux h p =
+ min_input h (fst p) (snd (snd p)).
+#h #p >min_input_def whd in ⊢ (??%?); >minus_S_S @min_f_g #i #_ #_
+whd in ⊢ (??%%); >fst_pair >snd_pair //
+qed.
+
+definition termb_aux ≝ λh.
+ termb_unary ∘ λp.〈fst (snd p),〈fst p,h (S (fst (snd p))) (fst p)〉〉.
+
+lemma compl_g4 : ∀h,s1,s. (∀x. 0 < s1 x) →
+ (CF s1
+ (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
+ (O s (λx.MSC x + ((snd(snd x) - (fst x)))*Max_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉))) →
+ CF s (λp:ℕ.min_input h (fst p) (snd (snd p))).
+#h #s1 #s #pos_s1 #Hs1 #HO @(ext_CF (min_input_aux h))
+ [#n whd in ⊢ (??%%); @min_input_eq]
+@(CF_mu4 … MSC MSC … pos_s1 … Hs1)
+ [@CF_compS @CF_fst
+ |@CF_comp_snd @CF_snd
+ |@(O_trans … HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
+qed.
+
+(* ??? *)
+
+lemma coroll: ∀s1:nat→nat. (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
+O (λx.(snd (snd x)-fst x)*(s1 〈snd (snd x),x〉))
+ (λx.∑_{i ∈[S(fst x) ,S(snd (snd x))[ }(s1 〈i,x〉)).
+#s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
+@(transitive_le … (sigma_bound …)) [@Hs1|>minus_S_S //]
+qed.
+
+lemma coroll2: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
+O (λx.(snd x - fst x)*s1 〈fst x,x〉) (λx.∑_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
+#s1 #Hs1 %{1} %{0} #n #_ >commutative_times <times_n_1
+@(transitive_le … (sigma_bound_decr …)) [2://] @Hs1
+qed.
+
+lemma coroll3: ∀s1:nat→nat. (∀n,a,b. a ≤ b → b < snd n → s1 〈b,n〉 ≤ s1 〈a,n〉) →
+O (λx.(snd x - fst x)*s1 〈fst x,x〉)
+ (λx.(snd x - fst x)*Max_{i ∈[fst x,snd x[ }(s1 〈i,x〉)).
+#s1 #Hs1 @le_to_O #i @le_times // @Max_le #a #lta #_ @Hs1 //
+@lt_minus_to_plus_r //
+qed.
+
+(**************************** end of technical lemmas *************************)
+
+lemma compl_g5 : ∀h,s1.
+ (∀n. 0 < s1 n) →
+ (∀n. monotonic ℕ le (λa:ℕ.s1 〈a,n〉)) →
+ (CF s1
+ (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) →
+ CF (λx.MSC x + (snd (snd x)-fst x)*s1 〈snd (snd x),x〉)
+ (λp:ℕ.min_input h (fst p) (snd (snd p))).
+#h #s1 #Hpos #Hmono #Hs1 @(compl_g4 … Hpos Hs1) @O_plus
+[@O_plus_l // |@O_plus_r @le_to_O #n @le_times //
+@Max_le #i #lti #_ @Hmono @le_S_S_to_le @lt_minus_to_plus_r @lti
+qed.
+
+lemma compl_g6: ∀h.
+ constructible (λx. h (fst x) (snd x)) →
+ (CF (λx. sU 〈max (fst (snd x)) (snd (snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉)
+ (λp.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))).
+#h #hconstr @(ext_CF (termb_aux h))
+ [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
+@(CF_comp … (λx.MSC x + h (S (fst (snd x))) (fst x)) … CF_termb)
+ [@CF_comp_pair
+ [@CF_comp_fst @(monotonic_CF … CF_snd) #x //
+ |@CF_comp_pair
+ [@(monotonic_CF … CF_fst) #x //
+ |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst (snd x)),fst x〉)))
+ [#n normalize >fst_pair >snd_pair %]
+ @(CF_comp … MSC …hconstr)
+ [@CF_comp_pair [@CF_compS @CF_comp_fst // |//]
+ |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
+ ]
+ ]
+ ]
+ |@O_plus
+ [@O_plus
+ [@(O_trans … (λx.MSC (fst x) + MSC (max (fst (snd x)) (snd (snd x)))))
+ [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
+ >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
+ >distributive_times_plus @le_plus [//]
+ cases (surj_pair b) #c * #d #eqb >eqb
+ >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
+ whd in ⊢ (??%); @le_plus
+ [@monotonic_MSC @(le_maxl … (le_n …))
+ |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
+ ]
+ |@O_plus [@le_to_O #x @sU_le_x |@le_to_O #x @sU_le_i]
+ ]
+ |@le_to_O #n @sU_le
+ ]
+ |@le_to_O #x @monotonic_sU // @(le_maxl … (le_n …)) ]
+ ]
+qed.
+
+definition big : nat →nat ≝ λx.
+ let m ≝ max (fst x) (snd x) in 〈m,m〉.
+
+lemma big_def : ∀a,b. big 〈a,b〉 = 〈max a b,max a b〉.
+#a #b normalize >fst_pair >snd_pair // qed.
+
+lemma le_big : ∀x. x ≤ big x.
+#x cases (surj_pair x) #a * #b #eqx >eqx @le_pair >fst_pair >snd_pair
+[@(le_maxl … (le_n …)) | @(le_maxr … (le_n …))]
+qed.
+
+definition faux2 ≝ λh.
+ (λx.MSC x + (snd (snd x)-fst x)*
+ (λx.sU 〈max (fst(snd x)) (snd(snd x)),〈fst x,h (S (fst (snd x))) (fst x)〉〉) 〈snd (snd x),x〉).
+
+lemma compl_g7: ∀h.
+ constructible (λx. h (fst x) (snd x)) →
+ (∀n. monotonic ? le (h n)) →
+ 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))〉〉)
+ (λp:ℕ.min_input h (fst p) (snd (snd p))).
+#h #hcostr #hmono @(monotonic_CF … (faux2 h))
+ [#n normalize >fst_pair >snd_pair //]
+@compl_g5 [#n @sU_pos | 3:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
+>fst_pair >snd_pair @monotonic_sU // @hmono @lexy
+qed.
+
+lemma compl_g71: ∀h.
+ constructible (λx. h (fst x) (snd x)) →
+ (∀n. monotonic ? le (h n)) →
+ 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))〉〉)
+ (λp:ℕ.min_input h (fst p) (snd (snd p))).
+#h #hcostr #hmono @(monotonic_CF … (compl_g7 h hcostr hmono)) #x
+@le_plus [@monotonic_MSC //]
+cases (decidable_le (fst x) (snd(snd x)))
+ [#Hle @le_times // @monotonic_sU
+ |#Hlt >(minus_to_0 … (lt_to_le … )) [// | @not_le_to_lt @Hlt]
+ ]
+qed.
+
+definition out_aux ≝ λh.
+ out_unary ∘ λp.〈fst p,〈snd(snd p),h (S (fst p)) (snd (snd p))〉〉.
+
+lemma compl_g8: ∀h.
+ constructible (λx. h (fst x) (snd x)) →
+ (CF (λx. sU 〈max (fst x) (snd x),〈snd(snd x),h (S (fst x)) (snd(snd x))〉〉)
+ (λp.out (fst p) (snd (snd p)) (h (S (fst p)) (snd (snd p))))).
+#h #hconstr @(ext_CF (out_aux h))
+ [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
+@(CF_comp … (λx.h (S (fst x)) (snd(snd x)) + MSC x) … CF_out)
+ [@CF_comp_pair
+ [@(monotonic_CF … CF_fst) #x //
+ |@CF_comp_pair
+ [@CF_comp_snd @(monotonic_CF … CF_snd) #x //
+ |@(ext_CF ((λx.h (fst x) (snd x))∘(λx.〈S (fst x),snd(snd x)〉)))
+ [#n normalize >fst_pair >snd_pair %]
+ @(CF_comp … MSC …hconstr)
+ [@CF_comp_pair [@CF_compS // | @CF_comp_snd // ]
+ |@O_plus @le_to_O [//|#n >fst_pair >snd_pair //]
+ ]
+ ]
+ ]
+ |@O_plus
+ [@O_plus
+ [@le_to_O #n @sU_le
+ |@(O_trans … (λx.MSC (max (fst x) (snd x))))
+ [%{2} %{0} #x #_ cases (surj_pair x) #a * #b #eqx >eqx
+ >fst_pair >snd_pair @(transitive_le … (MSC_pair …))
+ whd in ⊢ (??%); @le_plus
+ [@monotonic_MSC @(le_maxl … (le_n …))
+ |>commutative_times <times_n_1 @monotonic_MSC @(le_maxr … (le_n …))
+ ]
+ |@le_to_O #x @(transitive_le ???? (sU_le_i … )) //
+ ]
+ ]
+ |@le_to_O #x @monotonic_sU [@(le_maxl … (le_n …))|//|//]
+ ]
+qed.
+
+lemma compl_g9 : ∀h.
+ constructible (λx. h (fst x) (snd x)) →
+ (∀n. monotonic ? le (h n)) →
+ (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
+ CF (λx. (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)〉〉)
+ (auxg h).
+#h #hconstr #hmono #hantimono
+@(compl_g2 h ??? (compl_g3 … (compl_g71 h hconstr hmono)) (compl_g8 h hconstr))
+@O_plus
+ [@O_plus_l @le_to_O #x >(times_n_1 (MSC x)) >commutative_times @le_times
+ [// | @monotonic_MSC // ]]
+@(O_trans … (coroll3 ??))
+ [#n #a #b #leab #ltb >fst_pair >fst_pair >snd_pair >snd_pair
+ cut (b ≤ n) [@(transitive_le … (le_snd …)) @lt_to_le //] #lebn
+ cut (max a n = n)
+ [normalize >le_to_leb_true [//|@(transitive_le … leab lebn)]] #maxa
+ cut (max b n = n) [normalize >le_to_leb_true //] #maxb
+ @le_plus
+ [@le_plus [>big_def >big_def >maxa >maxb //]
+ @le_times
+ [/2 by monotonic_le_minus_r/
+ |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
+ ]
+ |@monotonic_sU // @hantimono [@le_S_S // |@ltb]
+ ]
+ |@le_to_O #n >fst_pair >snd_pair
+ cut (max (fst n) n = n) [normalize >le_to_leb_true //] #Hmax >Hmax
+ >associative_plus >distributive_times_plus
+ @le_plus [@le_times [@le_S // |>big_def >Hmax //] |//]
+ ]
+qed.
+
+definition c ≝ λx.(S (snd x-fst x))*MSC 〈x,x〉.
+
+definition sg ≝ λh,x.
+ let a ≝ fst x in
+ let b ≝ snd x in
+ c x + (b-a)*(S(b-a))*sU 〈x,〈snd x,h (S a) b〉〉.
+
+lemma sg_def1 : ∀h,a,b.
+ sg h 〈a,b〉 = c 〈a,b〉 +
+ (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
+#h #a #b whd in ⊢ (??%?); >fst_pair >snd_pair //
+qed.
+
+lemma sg_def : ∀h,a,b.
+ sg h 〈a,b〉 =
+ S (b-a)*MSC 〈〈a,b〉,〈a,b〉〉 + (b-a)*(S(b-a))*sU 〈〈a,b〉,〈b,h (S a) b〉〉.
+#h #a #b normalize >fst_pair >snd_pair //
+qed.
+
+lemma compl_g11 : ∀h.
+ constructible (λx. h (fst x) (snd x)) →
+ (∀n. monotonic ? le (h n)) →
+ (∀n,a,b. a ≤ b → b ≤ n → h b n ≤ h a n) →
+ CF (sg h) (unary_g h).
+#h #hconstr #Hm #Ham @compl_g1 @(compl_g9 h hconstr Hm Ham)
+qed.
+
+(**************************** closing the argument ****************************)
+
+let rec h_of_aux (r:nat →nat) (c,d,b:nat) on d : nat ≝
+ match d with
+ [ O ⇒ c
+ | S d1 ⇒ (S d)*(MSC 〈〈b-d,b〉,〈b-d,b〉〉) +
+ d*(S d)*sU 〈〈b-d,b〉,〈b,r (h_of_aux r c d1 b)〉〉].
+
+lemma h_of_aux_O: ∀r,c,b.
+ h_of_aux r c O b = c.
+// qed.
+
+lemma h_of_aux_S : ∀r,c,d,b.
+ h_of_aux r c (S d) b =
+ (S (S d))*(MSC 〈〈b-(S d),b〉,〈b-(S d),b〉〉) +
+ (S d)*(S (S d))*sU 〈〈b-(S d),b〉,〈b,r(h_of_aux r c d b)〉〉.
+// qed.
+
+definition h_of ≝ λr,p.
+ let m ≝ max (fst p) (snd p) in
+ h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (snd p - fst p) (snd p).
+
+lemma h_of_O: ∀r,a,b. b ≤ a →
+ h_of r 〈a,b〉 = let m ≝ max a b in MSC 〈〈m,m〉,〈m,m〉〉.
+#r #a #b #Hle normalize >fst_pair >snd_pair >(minus_to_0 … Hle) //
+qed.
+
+lemma h_of_def: ∀r,a,b.h_of r 〈a,b〉 =
+ let m ≝ max a b in
+ h_of_aux r (MSC 〈〈m,m〉,〈m,m〉〉) (b - a) b.
+#r #a #b normalize >fst_pair >snd_pair //
+qed.
+
+lemma mono_h_of_aux: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
+ ∀d,d1,c,c1,b,b1.c ≤ c1 → d ≤ d1 → b ≤ b1 →
+ h_of_aux r c d b ≤ h_of_aux r c1 d1 b1.
+#r #Hr #monor #d #d1 lapply d -d elim d1
+ [#d #c #c1 #b #b1 #Hc #Hd @(le_n_O_elim ? Hd) #leb
+ >h_of_aux_O >h_of_aux_O //
+ |#m #Hind #d #c #c1 #b #b1 #lec #led #leb cases (le_to_or_lt_eq … led)
+ [#ltd @(transitive_le … (Hind … lec ? leb)) [@le_S_S_to_le @ltd]
+ >h_of_aux_S @(transitive_le ???? (le_plus_n …))
+ >(times_n_1 (h_of_aux r c1 m b1)) in ⊢ (?%?);
+ >commutative_times @le_times [//|@(transitive_le … (Hr ?)) @sU_le]
+ |#Hd >Hd >h_of_aux_S >h_of_aux_S
+ cut (b-S m ≤ b1 - S m) [/2 by monotonic_le_minus_l/] #Hb1
+ @le_plus [@le_times //]
+ [@monotonic_MSC @le_pair @le_pair //
+ |@le_times [//] @monotonic_sU
+ [@le_pair // |// |@monor @Hind //]
+ ]
+ ]
+ ]
+qed.
+
+lemma mono_h_of2: ∀r.(∀x. x ≤ r x) → monotonic ? le r →
+ ∀i,b,b1. b ≤ b1 → h_of r 〈i,b〉 ≤ h_of r 〈i,b1〉.
+#r #Hr #Hmono #i #a #b #leab >h_of_def >h_of_def
+cut (max i a ≤ max i b)
+ [@to_max
+ [@(le_maxl … (le_n …))|@(transitive_le … leab) @(le_maxr … (le_n …))]]
+#Hmax @(mono_h_of_aux r Hr Hmono)
+ [@monotonic_MSC @le_pair @le_pair @Hmax |/2 by monotonic_le_minus_l/ |@leab]
+qed.
+
+axiom h_of_constr : ∀r:nat →nat.
+ (∀x. x ≤ r x) → monotonic ? le r → constructible r →
+ constructible (h_of r).
+
+lemma speed_compl: ∀r:nat →nat.
+ (∀x. x ≤ r x) → monotonic ? le r → constructible r →
+ CF (h_of r) (unary_g (λi,x. r(h_of r 〈i,x〉))).
+#r #Hr #Hmono #Hconstr @(monotonic_CF … (compl_g11 …))
+ [#x cases (surj_pair x) #a * #b #eqx >eqx
+ >sg_def cases (decidable_le b a)
+ [#leba >(minus_to_0 … leba) normalize in ⊢ (?%?);
+ <plus_n_O <plus_n_O >h_of_def
+ cut (max a b = a)
+ [normalize cases (le_to_or_lt_eq … leba)
+ [#ltba >(lt_to_leb_false … ltba) %
+ |#eqba <eqba >(le_to_leb_true … (le_n ?)) % ]]
+ #Hmax >Hmax normalize >(minus_to_0 … leba) normalize
+ @monotonic_MSC @le_pair @le_pair //
+ |#ltab >h_of_def >h_of_def
+ cut (max a b = b)
+ [normalize >(le_to_leb_true … ) [%] @lt_to_le @not_le_to_lt @ltab]
+ #Hmax >Hmax
+ cut (max (S a) b = b)
+ [whd in ⊢ (??%?); >(le_to_leb_true … ) [%] @not_le_to_lt @ltab]
+ #Hmax1 >Hmax1
+ cut (∃d.b - a = S d)
+ [%{(pred(b-a))} >S_pred [//] @lt_plus_to_minus_r @not_le_to_lt @ltab]
+ * #d #eqd >eqd
+ cut (b-S a = d) [//] #eqd1 >eqd1 >h_of_aux_S >eqd1
+ cut (b - S d = a)
+ [@plus_to_minus >commutative_plus @minus_to_plus
+ [@lt_to_le @not_le_to_lt // | //]] #eqd2 >eqd2
+ normalize //
+ ]
+ |#n #a #b #leab #lebn >h_of_def >h_of_def
+ cut (max a n = n)
+ [normalize >le_to_leb_true [%|@(transitive_le … leab lebn)]] #Hmaxa
+ cut (max b n = n)
+ [normalize >(le_to_leb_true … lebn) %] #Hmaxb
+ >Hmaxa >Hmaxb @Hmono @(mono_h_of_aux r … Hr Hmono) // /2 by monotonic_le_minus_r/
+ |#n #a #b #leab @Hmono @(mono_h_of2 … Hr Hmono … leab)
+ |@(constr_comp … Hconstr Hr) @(ext_constr (h_of r))
+ [#x cases (surj_pair x) #a * #b #eqx >eqx >fst_pair >snd_pair //]
+ @(h_of_constr r Hr Hmono Hconstr)
+ ]
+qed.
+
+lemma speed_compl_i: ∀r:nat →nat.
+ (∀x. x ≤ r x) → monotonic ? le r → constructible r →
+ ∀i. CF (λx.h_of r 〈i,x〉) (λx.g (λi,x. r(h_of r 〈i,x〉)) i x).
+#r #Hr #Hmono #Hconstr #i
+@(ext_CF (λx.unary_g (λi,x. r(h_of r 〈i,x〉)) 〈i,x〉))
+ [#n whd in ⊢ (??%%); @eq_f @sym_eq >fst_pair >snd_pair %]
+@smn @(ext_CF … (speed_compl r Hr Hmono Hconstr)) #n //
+qed.
+
+(**************************** the speedup theorem *****************************)
+theorem pseudo_speedup:
+ ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
+ ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧ O sf (r ∘ sg).
+(* ∃m,a.∀n. a≤n → r(sg a) < m * sf n. *)
+#r #Hr #Hmono #Hconstr
+(* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
+%{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #i *
+#Hcodei #HCi
+(* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
+%{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
+(* sg is (λx.h_of r 〈i,x〉) *)
+%{(λx. h_of r 〈S i,x〉)}
+lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
+%[%[@condition_1 |@Hg]
+ |cases Hg #H1 * #j * #Hcodej #HCj
+ lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
+ cases HCi #m * #a #Ha %{m} %{(max (S i) a)} #n #ltin @lt_to_le @not_le_to_lt
+ @(not_to_not … Hcond2) -Hcond2 #Hlesf %{n} %
+ [@(transitive_le … ltin) @(le_maxl … (le_n …))]
+ cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
+ #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf) //
+ ]
+qed.
+
+theorem pseudo_speedup':
+ ∀r:nat →nat. (∀x. x ≤ r x) → monotonic ? le r → constructible r →
+ ∃f.∀sf. CF sf f → ∃g,sg. f ≈ g ∧ CF sg g ∧
+ (* ¬ O (r ∘ sg) sf. *)
+ ∃m,a.∀n. a≤n → r(sg a) < m * sf n.
+#r #Hr #Hmono #Hconstr
+(* f is (g (λi,x. r(h_of r 〈i,x〉)) 0) *)
+%{(g (λi,x. r(h_of r 〈i,x〉)) 0)} #sf * #i *
+#Hcodei #HCi
+(* g is (g (λi,x. r(h_of r 〈i,x〉)) (S i)) *)
+%{(g (λi,x. r(h_of r 〈i,x〉)) (S i))}
+(* sg is (λx.h_of r 〈S i,x〉) *)
+%{(λx. h_of r 〈S i,x〉)}
+lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
+%[%[@condition_1 |@Hg]
+ |cases Hg #H1 * #j * #Hcodej #HCj
+ lapply (condition_2 … Hcodei) #Hcond2 (* @not_to_not *)
+ cases HCi #m * #a #Ha
+ %{m} %{(max (S i) a)} #n #ltin @not_le_to_lt @(not_to_not … Hcond2) -Hcond2
+ #Hlesf %{n} % [@(transitive_le … ltin) @(le_maxl … (le_n …))]
+ cases (Ha n ?) [2: @(transitive_le … ltin) @(le_maxr … (le_n …))]
+ #y #Uy %{y} @(monotonic_U … Uy) @(transitive_le … Hlesf)
+ @Hmono @(mono_h_of2 … Hr Hmono … ltin)
+ ]
+qed.
+
\ No newline at end of file
projects / helm.git / blobdiff