+include "basics/types.ma".
+include "arithmetics/minimization.ma".
+include "arithmetics/bigops.ma".
+include "arithmetics/sigma_pi.ma".
+include "arithmetics/bounded_quantifiers.ma".
+include "reverse_complexity/big_O.ma".
+include "basics/core_notation/napart_2.ma".
+
+(************************* notation for minimization *****************************)
+notation "ΞΌ_{ ident i < n } p"
+ with precedence 80 for @{min $n 0 (Ξ»${ident i}.$p)}.
+
+notation "ΞΌ_{ ident i β€ n } p"
+ with precedence 80 for @{min (S $n) 0 (Ξ»${ident i}.$p)}.
+
+notation "ΞΌ_{ ident i β [a,b[ } p"
+ with precedence 80 for @{min ($b-$a) $a (Ξ»${ident i}.$p)}.
+
+notation "ΞΌ_{ ident i β [a,b] } p"
+ with precedence 80 for @{min (S $b-$a) $a (Ξ»${ident i}.$p)}.
+
+(************************************ MAX *************************************)
+notation "Max_{ ident i < n | p } f"
+ with precedence 80
+for @{'bigop $n max 0 (Ξ»${ident i}. $p) (Ξ»${ident i}. $f)}.
+
+notation "Max_{ ident i < n } f"
+ with precedence 80
+for @{'bigop $n max 0 (Ξ»${ident i}.true) (Ξ»${ident i}. $f)}.
+
+notation "Max_{ ident j β [a,b[ } f"
+ with precedence 80
+for @{'bigop ($b-$a) max 0 (Ξ»${ident j}.((Ξ»${ident j}.true) (${ident j}+$a)))
+ (Ξ»${ident j}.((Ξ»${ident j}.$f)(${ident j}+$a)))}.
+
+notation "Max_{ ident j β [a,b[ | p } f"
+ with precedence 80
+for @{'bigop ($b-$a) max 0 (Ξ»${ident j}.((Ξ»${ident j}.$p) (${ident j}+$a)))
+ (Ξ»${ident j}.((Ξ»${ident j}.$f)(${ident j}+$a)))}.
+
+lemma Max_assoc: βa,b,c. max (max a b) c = max a (max b c).
+#a #b #c normalize cases (true_or_false (leb a b)) #leab >leab normalize
+ [cases (true_or_false (leb b c )) #lebc >lebc normalize
+ [>(le_to_leb_true a c) // @(transitive_le ? b) @leb_true_to_le //
+ |>leab //
+ ]
+ |cases (true_or_false (leb b c )) #lebc >lebc normalize //
+ >leab normalize >(not_le_to_leb_false a c) // @lt_to_not_le
+ @(transitive_lt ? b) @not_le_to_lt @leb_false_to_not_le //
+ ]
+qed.
+
+lemma Max0 : βn. max 0 n = n.
+// qed.
+
+lemma Max0r : βn. max n 0 = n.
+#n >commutative_max //
+qed.
+
+definition MaxA β
+ mk_Aop nat 0 max Max0 Max0r (Ξ»a,b,c.sym_eq β¦ (Max_assoc a b c)).
+
+definition MaxAC β mk_ACop nat 0 MaxA commutative_max.
+
+lemma le_Max: βf,p,n,a. a < n β p a = true β
+ f a β€ Max_{i < n | p i}(f i).
+#f #p #n #a #ltan #pa
+>(bigop_diff p ? 0 MaxAC f a n) // @(le_maxl β¦ (le_n ?))
+qed.
+
+lemma le_MaxI: βf,p,n,m,a. m β€ a β a < n β p a = true β
+ f a β€ Max_{i β [m,n[ | p i}(f i).
+#f #p #n #m #a #lema #ltan #pa
+>(bigop_diff ? ? 0 MaxAC (Ξ»i.f (i+m)) (a-m) (n-m))
+ [<plus_minus_m_m // @(le_maxl β¦ (le_n ?))
+ |<plus_minus_m_m //
+ |/2 by monotonic_lt_minus_l/
+ ]
+qed.
+
+lemma Max_le: βf,p,n,b.
+ (βa.a < n β p a = true β f a β€ b) β Max_{i < n | p i}(f i) β€ b.
+#f #p #n elim n #b #H //
+#b0 #H1 cases (true_or_false (p b)) #Hb
+ [>bigop_Strue [2:@Hb] @to_max [@H1 // | @H #a #ltab #pa @H1 // @le_S //]
+ |>bigop_Sfalse [2:@Hb] @H #a #ltab #pa @H1 // @le_S //
+ ]
+qed.
+
+(********************************** pairing ***********************************)
+axiom pair: nat β nat β nat.
+axiom fst : nat β nat.
+axiom snd : nat β nat.
+
+interpretation "abstract pair" 'pair f g = (pair f g).
+
+axiom fst_pair: βa,b. fst β©a,bβͺ = a.
+axiom snd_pair: βa,b. snd β©a,bβͺ = b.
+axiom surj_pair: βx. βa,b. x = β©a,bβͺ.
+
+axiom le_fst : βp. fst p β€ p.
+axiom le_snd : βp. snd p β€ p.
+axiom le_pair: βa,a1,b,b1. a β€ a1 β b β€ b1 β β©a,bβͺ β€ β©a1,b1βͺ.
+
+(************************************* U **************************************)
+axiom U: nat β nat βnat β option nat.
+
+axiom monotonic_U: βi,x,n,m,y.n β€m β
+ U i x n = Some ? y β U i x m = Some ? y.
+
+lemma unique_U: βi,x,n,m,yn,ym.
+ U i x n = Some ? yn β U i x m = Some ? ym β yn = ym.
+#i #x #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
+ [#lenm lapply (monotonic_U β¦ lenm Hn) >Hm #HS destruct (HS) //
+ |#ltmn lapply (monotonic_U β¦ n β¦ Hm) [@lt_to_le @not_le_to_lt //]
+ >Hn #HS destruct (HS) //
+ ]
+qed.
+
+definition code_for β Ξ»f,i.βx.
+ βn.βm. n β€ m β U i x m = f x.
+
+definition terminate β Ξ»i,x,r. βy. U i x r = Some ? y.
+
+notation "{i β x} β r" with precedence 60 for @{terminate $i $x $r}.
+
+lemma terminate_dec: βi,x,n. {i β x} β n β¨ Β¬ {i β x} β n.
+#i #x #n normalize cases (U i x n)
+ [%2 % * #y #H destruct|#y %1 %{y} //]
+qed.
+
+lemma monotonic_terminate: βi,x,n,m.
+ n β€ m β {i β x} β n β {i β x} β m.
+#i #x #n #m #lenm * #z #H %{z} @(monotonic_U β¦ H) //
+qed.
+
+definition termb β Ξ»i,x,t.
+ match U i x t with [None β false |Some y β true].
+
+lemma termb_true_to_term: βi,x,t. termb i x t = true β {i β x} β t.
+#i #x #t normalize cases (U i x t) normalize [#H destruct | #y #_ %{y} //]
+qed.
+
+lemma term_to_termb_true: βi,x,t. {i β x} β t β termb i x t = true.
+#i #x #t * #y #H normalize >H //
+qed.
+
+definition out β Ξ»i,x,r.
+ match U i x r with [ None β 0 | Some z β z].
+
+definition bool_to_nat: bool β nat β
+ Ξ»b. match b with [true β 1 | false β 0].
+
+coercion bool_to_nat.
+
+definition pU : nat β nat β nat β nat β Ξ»i,x,r.β©termb i x r,out i x rβͺ.
+
+lemma pU_vs_U_Some : βi,x,r,y. pU i x r = β©1,yβͺ β U i x r = Some ? y.
+#i #x #r #y % normalize
+ [cases (U i x r) normalize
+ [#H cut (0=1) [lapply (eq_f β¦ fst β¦ H) >fst_pair >fst_pair #H @H]
+ #H1 destruct
+ |#a #H cut (a=y) [lapply (eq_f β¦ snd β¦ H) >snd_pair >snd_pair #H1 @H1]
+ #H1 //
+ ]
+ |#H >H //]
+qed.
+
+lemma pU_vs_U_None : βi,x,r. pU i x r = β©0,0βͺ β U i x r = None ?.
+#i #x #r % normalize
+ [cases (U i x r) normalize //
+ #a #H cut (1=0) [lapply (eq_f β¦ fst β¦ H) >fst_pair >fst_pair #H1 @H1]
+ #H1 destruct
+ |#H >H //]
+qed.
+
+lemma fst_pU: βi,x,r. fst (pU i x r) = termb i x r.
+#i #x #r normalize cases (U i x r) normalize >fst_pair //
+qed.
+
+lemma snd_pU: βi,x,r. snd (pU i x r) = out i x r.
+#i #x #r normalize cases (U i x r) normalize >snd_pair //
+qed.
+
+(********************************* 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.
+
+(*
+axiom ax1: βh,i.
+ (βy.i < y β§ (termb i y (h (S i) y)=true)) β¨
+ βy. i < y β (termb i y (h (S i) y)=false).
+
+lemma eventually_0: β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
+ [%{0} normalize //
+ |#u0 * #nu0 #Hind cases (ax1 h u0)
+ [* #x0 * #leu0x0 #Hx0 %{(max nu0 x0)}
+ #x #Hx >bigop_Sfalse
+ [>(minus_n_O u0) @Hind @(le_to_lt_to_lt β¦ Hx) /2 by le_maxl/
+ |@not_eq_to_eqb_false % #Hf @(absurd (x β€ x0))
+ [<Hf @true_to_le_min //
+ |@lt_to_not_le @(le_to_lt_to_lt β¦ Hx) /2 by le_maxl/
+ ]
+ ]
+ |#H %{(max u0 nu0)} #x #Hx >bigop_Sfalse
+ [>(minus_n_O u0) @Hind @(le_to_lt_to_lt β¦ Hx) @le_maxr //
+ |@not_eq_to_eqb_false >min_input_def
+ >(min_not_exists (Ξ»y.(termb (u0+0) y (h (S (u0+0)) y))))
+ [<plus_n_O <plus_n_Sm <plus_minus_m_m
+ [% #H1 /2/
+ |@lt_to_le @(le_to_lt_to_lt β¦ Hx) @le_maxl //
+ ]
+ |/2 by /
+ ]
+ ]
+ ]
+ ]
+qed.
+
+definition almost_equal β Ξ»f,g:nat β nat. βnu.βx. nu < x β f x = g x.
+
+definition almost_equal1 β Ξ»f,g:nat β nat. Β¬ βnu.βx. nu < x β§ f x β g x.
+
+interpretation "almost equal" 'napart f g = (almost_equal f g).
+
+lemma condition_1: βh,u.g h 0 β g h u.
+#h #u cases (eventually_0 h u) #nu #H %{(max u nu)} #x #Hx @(eq_f ?? S)
+>(bigop_sumI 0 u x (Ξ»i:β.eqb (min_input h i x) x) nat 0 MaxA)
+ [>H // @(le_to_lt_to_lt β¦Hx) /2 by le_maxl/
+ |@lt_to_le @(le_to_lt_to_lt β¦Hx) /2 by le_maxr/
+ |//
+ ]
+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 *********************************)
+definition total β Ξ»f.Ξ»x:nat. Some nat (f x).
+
+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 ***********************)
+
+(* We assume operations have a minimal structural complexity MSC.
+For instance, for time complexity, MSC is equal to the size of input.
+For space complexity, MSC is typically 0, since we only measure the
+space required in addition to dimension of the input. *)
+
+axiom MSC : nat β nat.
+axiom MSC_le: βn. MSC n β€ n.
+axiom monotonic_MSC: monotonic ? le MSC.
+axiom MSC_pair: βa,b. MSC β©a,bβͺ β€ MSC a + MSC b.
+
+(* C s i means i is running in O(s) *)
+
+definition C β Ξ»s,i.βc.βa.βx.a β€ x β βy.
+ U i x (c*(s x)) = Some ? y.
+
+(* C f s means f β O(s) where MSC βO(s) *)
+definition CF β Ξ»s,f.O s MSC β§ βi.code_for (total f) i β§ C s i.
+
+lemma ext_CF : βf,g,s. (βn. f n = g n) β CF s f β CF s g.
+#f #g #s #Hext * #HO * #i * #Hcode #HC % // %{i} %
+ [#x cases (Hcode x) #a #H %{a} whd in match (total ??); <Hext @H | //]
+qed.
+
+(* lemma ext_CF_total : βf,g,s. (βn. f n = g n) β CF s (total f) β CF s (total g).
+#f #g #s #Hext * #HO * #i * #Hcode #HC % // %{i} % [2:@HC]
+#x cases (Hcode x) #a #H %{a} #m #leam >(H m leam) normalize @eq_f @Hext
+qed. *)
+
+lemma monotonic_CF: βs1,s2,f.(βx. s1 x β€ s2 x) β CF s1 f β CF s2 f.
+#s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
+ [cases HO #c * #a -HO #HO %{c} %{a} #n #lean @(transitive_le β¦ (HO n lean))
+ @le_times //
+ |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1 %{c} %{a} #n #lean
+ cases(Hs1 n lean) #y #Hy %{y} @(monotonic_U β¦Hy) @le_times //
+ ]
+qed.
+
+lemma O_to_CF: βs1,s2,f.O s2 s1 β CF s1 f β CF s2 f.
+#s1 #s2 #f #H * #HO * #i * #Hcode #Hs1 %
+ [@(O_trans β¦ H) //
+ |%{i} % [//] cases Hs1 #c * #a -Hs1 #Hs1
+ cases H #c1 * #a1 #Ha1 %{(c*c1)} %{(a+a1)} #n #lean
+ cases(Hs1 n ?) [2:@(transitive_le β¦ lean) //] #y #Hy %{y} @(monotonic_U β¦Hy)
+ >associative_times @le_times // @Ha1 @(transitive_le β¦ lean) //
+ ]
+qed.
+
+lemma timesc_CF: βs,f,c.CF (Ξ»x.c*s x) f β CF s f.
+#s #f #c @O_to_CF @O_times_c
+qed.
+
+(********************************* composition ********************************)
+axiom CF_comp: βf,g,sf,sg,sh. CF sg g β CF sf f β
+ O sh (Ξ»x. sg x + sf (g x)) β CF sh (f β g).
+
+lemma CF_comp_ext: βf,g,h,sh,sf,sg. CF sg g β CF sf f β
+ (βx.f(g x) = h x) β O sh (Ξ»x. sg x + sf (g x)) β CF sh h.
+#f #g #h #sh #sf #sg #Hg #Hf #Heq #H @(ext_CF (f β g))
+ [#n normalize @Heq | @(CF_comp β¦ H) //]
+qed.
+
+(*
+lemma CF_comp1: βf,g,s. CF s (total g) β CF s (total f) β
+ CF s (total (f β g)).
+#f #g #s #Hg #Hf @(timesc_CF β¦ 2) @(monotonic_CF β¦ (CF_comp β¦ Hg Hf))
+*)
+
+(*
+axiom CF_comp_ext2: βf,g,h,sf,sh. CF sh (total g) β CF sf (total f) β
+ (βx.f(g x) = h x) β
+ (βx. sf (g x) β€ sh x) β CF sh (total h).
+
+lemma main_MSC: βh,f. CF h f β O h (Ξ»x.MSC (f x)).
+
+axiom CF_S: CF MSC S.
+axiom CF_fst: CF MSC fst.
+axiom CF_snd: CF MSC snd.
+
+lemma CF_compS: βh,f. CF h f β CF h (S β f).
+#h #f #Hf @(CF_comp β¦ Hf CF_S) @O_plus // @main_MSC //
+qed.
+
+lemma CF_comp_fst: βh,f. CF h (total f) β CF h (total (fst β f)).
+#h #f #Hf @(CF_comp β¦ Hf CF_fst) @O_plus // @main_MSC //
+qed.
+
+lemma CF_comp_snd: βh,f. CF h (total f) β CF h (total (snd β f)).
+#h #f #Hf @(CF_comp β¦ Hf CF_snd) @O_plus // @main_MSC //
+qed. *)
+
+definition id β Ξ»x:nat.x.
+
+axiom CF_id: CF MSC id.
+axiom CF_compS: βh,f. CF h f β CF h (S β f).
+axiom CF_comp_fst: βh,f. CF h f β CF h (fst β f).
+axiom CF_comp_snd: βh,f. CF h f β CF h (snd β f).
+axiom CF_comp_pair: βh,f,g. CF h f β CF h g β CF h (Ξ»x. β©f x,g xβͺ).
+
+lemma CF_fst: CF MSC fst.
+@(ext_CF (fst β id)) [#n //] @(CF_comp_fst β¦ CF_id)
+qed.
+
+lemma CF_snd: CF MSC snd.
+@(ext_CF (snd β id)) [#n //] @(CF_comp_snd β¦ CF_id)
+qed.
+
+(************************************** eqb ***********************************)
+(* definition btotal β
+ Ξ»f.Ξ»x:nat. match f x with [true β Some ? 0 |false β Some ? 1]. *)
+
+axiom CF_eqb: βh,f,g.
+ CF h f β CF h g β CF h (Ξ»x.eqb (f x) (g x)).
+
+(*
+axiom eqb_compl2: βh,f,g.
+ CF2 h (total2 f) β CF2 h (total2 g) β
+ CF2 h (btotal2 (Ξ»x1,x2.eqb (f x1 x2) (g x1 x2))).
+
+axiom eqb_min_input_compl:βh,x.
+ CF (Ξ»i.β_{y β [S i,S x[ }(h i y))
+ (btotal (Ξ»i.eqb (min_input h i x) x)). *)
+(*********************************** maximum **********************************)
+
+axiom CF_max: βa,b.βp:nat βbool.βf,ha,hb,hp,hf,s.
+ CF ha a β CF hb b β CF hp p β CF hf f β
+ O s (Ξ»x.ha x + hb x + β_{i β[a x ,b x[ }(hp β©i,xβͺ + hf β©i,xβͺ)) β
+ CF s (Ξ»x.max_{i β[a x,b x[ | p β©i,xβͺ }(f β©i,xβͺ)).
+
+(******************************** minimization ********************************)
+
+axiom CF_mu: βa,b.βf:nat βbool.βsa,sb,sf,s.
+ CF sa a β CF sb b β CF sf f β
+ O s (Ξ»x.sa x + sb x + β_{i β[a x ,S(b x)[ }(sf β©i,xβͺ)) β
+ CF s (Ξ»x.ΞΌ_{i β[a x,b x] }(f β©i,xβͺ)).
+
+(****************************** constructibility ******************************)
+
+definition constructible β Ξ»s. CF s s.
+
+lemma constr_comp : βs1,s2. constructible s1 β constructible s2 β
+ (βx. x β€ s2 x) β constructible (s2 β s1).
+#s1 #s2 #Hs1 #Hs2 #Hle @(CF_comp β¦ Hs1 Hs2) @O_plus @le_to_O #x [@Hle | //]
+qed.
+
+lemma ext_constr: βs1,s2. (βx.s1 x = s2 x) β
+ constructible s1 β constructible s2.
+#s1 #s2 #Hext #Hs1 @(ext_CF β¦ Hext) @(monotonic_CF β¦ Hs1) #x >Hext //
+qed.
+
+(********************************* simulation *********************************)
+
+axiom sU : nat β nat.
+
+axiom monotonic_sU: βi1,i2,x1,x2,s1,s2. i1 β€ i2 β x1 β€ x2 β s1 β€ s2 β
+ sU β©i1,β©x1,s1βͺβͺ β€ sU β©i2,β©x2,s2βͺβͺ.
+
+lemma monotonic_sU_aux : βx1,x2. fst x1 β€ fst x2 β fst (snd x1) β€ fst (snd x2) β
+snd (snd x1) β€ snd (snd x2) β sU x1 β€ sU x2.
+#x1 #x2 cases (surj_pair x1) #a1 * #y #eqx1 >eqx1 -eqx1 cases (surj_pair y)
+#b1 * #c1 #eqy >eqy -eqy
+cases (surj_pair x2) #a2 * #y2 #eqx2 >eqx2 -eqx2 cases (surj_pair y2)
+#b2 * #c2 #eqy2 >eqy2 -eqy2 >fst_pair >snd_pair >fst_pair >snd_pair
+>fst_pair >snd_pair >fst_pair >snd_pair @monotonic_sU
+qed.
+
+axiom sU_le: βi,x,s. s β€ sU β©i,β©x,sβͺβͺ.
+axiom sU_le_i: βi,x,s. MSC i β€ sU β©i,β©x,sβͺβͺ.
+axiom sU_le_x: βi,x,s. MSC x β€ sU β©i,β©x,sβͺβͺ.
+
+definition pU_unary β Ξ»p. pU (fst p) (fst (snd p)) (snd (snd p)).
+
+axiom CF_U : CF sU pU_unary.
+
+definition termb_unary β Ξ»x:β.termb (fst x) (fst (snd x)) (snd (snd x)).
+definition out_unary β Ξ»x:β.out (fst x) (fst (snd x)) (snd (snd x)).
+
+lemma CF_termb: CF sU termb_unary.
+@(ext_CF (fst β pU_unary)) [2: @CF_comp_fst @CF_U]
+#n whd in β’ (??%?); whd in β’ (??(?%)?); >fst_pair %
+qed.
+
+lemma CF_out: CF sU out_unary.
+@(ext_CF (snd β pU_unary)) [2: @CF_comp_snd @CF_U]
+#n whd in β’ (??%?); whd in β’ (??(?%)?); >snd_pair %
+qed.
+
+(*
+lemma CF_termb_comp: βf.CF (sU β f) (termb_unary β f).
+#f @(CF_comp β¦ CF_termb) *)
+
+(******************** 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 + β_{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_max β¦ 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 β¦ (proj1 β¦ 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 termb_aux : βh,p.
+ (Ξ»x:β.termb (fst x) (fst (snd x)) (snd (snd x)))
+ β©fst (snd p),β©fst p,h (S (fst (snd p))) (fst p)βͺβͺ =
+ termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)) .
+#h #p normalize >fst_pair >snd_pair >fst_pair >snd_pair //
+qed. *)
+
+lemma compl_g4 : βh,s1,s.
+ (CF s1
+ (Ξ»p.termb (fst (snd p)) (fst p) (h (S (fst (snd p))) (fst p)))) β
+ (O s (Ξ»x.MSC x + β_{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 #Hs1 #HO @(ext_CF (min_input_aux h))
+ [#n whd in β’ (??%%); @min_input_eq]
+@(CF_mu β¦ MSC MSC β¦ Hs1)
+ [@CF_compS @CF_fst
+ |@CF_comp_snd @CF_snd
+ |@(O_trans β¦ HO) @O_plus [@O_plus @O_plus_l // | @O_plus_r //]
+(* @(ext_CF (btotal (termb_aux h)))
+ [#n normalize >fst_pair >snd_pair >fst_pair >snd_pair // ]
+@(CF_compb β¦ CF_termb) *)
+qed.
+
+(************************* a couple of technical lemmas ***********************)
+lemma minus_to_0: βa,b. a β€ b β minus a b = 0.
+#a elim a // #n #Hind *
+ [#H @False_ind /2 by absurd/ | #b normalize #H @Hind @le_S_S_to_le /2/]
+qed.
+
+lemma sigma_bound: βh,a,b. monotonic nat le h β
+ β_{i β [a,S b[ }(h i) β€ (S b-a)*h b.
+#h #a #b #H cases (decidable_le a b)
+ [#leab cut (b = pred (S b - a + a))
+ [<plus_minus_m_m // @le_S //] #Hb >Hb in match (h b);
+ generalize in match (S b -a);
+ #n elim n
+ [//
+ |#m #Hind >bigop_Strue [2://] @le_plus
+ [@H @le_n |@(transitive_le β¦ Hind) @le_times [//] @H //]
+ ]
+ |#ltba lapply (not_le_to_lt β¦ ltba) -ltba #ltba
+ cut (S b -a = 0) [@minus_to_0 //] #Hcut >Hcut //
+ ]
+qed.
+
+lemma sigma_bound_decr: βh,a,b. (βa1,a2. a1 β€ a2 β a2 < b β h a2 β€ h a1) β
+ β_{i β [a,b[ }(h i) β€ (b-a)*h a.
+#h #a #b #H cases (decidable_le a b)
+ [#leab cut ((b -a) +a β€ b) [/2 by le_minus_to_plus_r/] generalize in match (b -a);
+ #n elim n
+ [//
+ |#m #Hind >bigop_Strue [2://] #Hm
+ cut (m+a β€ b) [@(transitive_le β¦ Hm) //] #Hm1
+ @le_plus [@H // |@(transitive_le β¦ (Hind Hm1)) //]
+ ]
+ |#ltba lapply (not_le_to_lt β¦ ltba) -ltba #ltba
+ cut (b -a = 0) [@minus_to_0 @lt_to_le @ltba] #Hcut >Hcut //
+ ]
+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 compl_g5 : βh,s1.(β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 #Hmono #Hs1 @(compl_g4 β¦ Hs1) @O_plus
+[@O_plus_l // |@O_plus_r @coroll @Hmono]
+qed.
+
+(*
+axiom compl_g6: βh.
+ (* constructible (Ξ»x. h (fst x) (snd x)) β *)
+ (CF (Ξ»x. max (MSC x) (sU β©fst (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)))).
+*)
+
+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 faux1 β Ξ»h.
+ (Ξ»x.MSC x + (snd (snd x)-fst x)*(Ξ»x.sU β©fst (snd x),β©fst x,h (S (fst (snd x))) (fst x)βͺβͺ) β©snd (snd x),xβͺ).
+
+(* complexity of min_input *)
+lemma compl_g7: βh.
+ (βx.MSC xβ€h (S (fst (snd x))) (fst x)) β
+ constructible (Ξ»x. h (fst x) (snd x)) β
+ (βn. monotonic ? le (h n)) β
+ CF (Ξ»x.MSC x + (snd (snd x)-fst x)*sU β©fst x,β©snd (snd x),h (S (fst x)) (snd (snd x))βͺβͺ)
+ (Ξ»p:β.min_input h (fst p) (snd (snd p))).
+#h #hle #hcostr #hmono @(monotonic_CF β¦ (faux1 h))
+ [#n normalize >fst_pair >snd_pair //]
+@compl_g5 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
+>fst_pair >snd_pair @monotonic_sU // @hmono @lexy
+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βͺ).
+
+(* proviamo con 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 [2:@(compl_g6 h hcostr)] #n #x #y #lexy >fst_pair >snd_pair
+>fst_pair >snd_pair @monotonic_sU // @hmono @lexy
+qed.
+
+(* proviamo con x *)
+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.
+
+(*
+axiom compl_g8: βh.
+ CF (Ξ»x. sU β©fst 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)))). *)
+
+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_g81: βh.
+ (βx.MSC xβ€h (S (fst x)) (snd(snd x))) β
+ 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 #hle #hconstr @(monotonic_CF ???? (compl_g8 h hle hconstr)) #x @monotonic_sU // @(le_maxl β¦ (le_n β¦ ))
+qed. *)
+
+(* axiom daemon : False. *)
+
+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 β¦ (coroll2 ??))
+ [#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 sg β Ξ»h,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)βͺβͺ.
+
+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 whd in β’ (??%?); >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 (* MSC β©β©b,bβͺ,β©b,bβͺβͺ *)
+ | 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 unary_g_def : βh,i,x. g h i x = unary_g h β©i,xβͺ.
+#h #i #x whd in β’ (???%); >fst_pair >snd_pair %
+qed. *)
+
+(* smn *)
+axiom smn: βf,s. CF s f β βx. CF (Ξ»y.s β©x,yβͺ) (Ξ»y.f β©x,yβͺ).
+
+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.
+
+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 * #H * #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 * #H * #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 @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.
+