proposition: Lemma sorted_nfun_batcher_merge_rec m (t : (`2^ m.+1).-tuple bool) : sorted <=%O (ttake t) -> sorted <=%O (tdrop t) -> sorted <=%O (nfun (batcher_merge_rec_aux m) t).
proof: Proof. elim: m t => [t tS dS|m IH t tS dS /=]. rewrite [batcher_merge_rec_aux 0]/= tsorted2 /=. by rewrite cswapE_min // cswapE_max // ge_min le_max lexx. rewrite nfun_rcons nfun_eodup. set n1 := nfun _ _; set n2 := nfun _ _. have n1P : perm_eq n1 (tetake t) by apply: perm_nfun. have n1S : sorted <=%O n1. apply: IH. by rewrite ttake_etakeE; apply: etake_sorted => // [] [] [] []. by rewrite tdrop_etakeE; apply: etake_sorted => // [] [] [] []. have n2P : perm_eq n2 (totake t) by apply: perm_nfun. have n2S : sorted <=%O n2. apply: IH. - by rewrite ttake_otakeE; apply: otake_sorted => // [] [] [] []. - by rewrite tdrop_otakeE; apply: otake_sorted => // [] [] [] []. apply: sorted_batcher_merge; rewrite ?(tetakeK, totakeK) //. have /isorted_boolP[[a1 b1] n1E] := n1S. have /isorted_boolP[[a2 b2] n2E] := n2S. rewrite !n1E !n2E !noE. have /isorted_boolP[[a3 b3] tSE] := tS. have /isorted_boolP[[a4 b4] dSE] := dS. have /val_eqP tE := cat_ttake_tdrop t; rewrite /= tSE dSE in tE. have /val_eqP eotE := eocat_tetake_totake t. rewrite /= (eqP tE) !(etake_cat, otake_cat, etake_cat_nseq, otake_nseq, etake_nseq, size_cat, size_nseq, otake_cat_nseq) in eotE. have : ~~ odd (size (ttake t)) by rewrite size_tuple addnn odd_double. rewrite tSE size_cat !size_nseq => /negPf b3O. rewrite b3O in eotE; rewrite oddD in b3O. have : ~~ odd (size (tdrop t)) by rewrite size_tuple addnn odd_double. rewrite dSE size_cat !size_nseq oddD => /negPf b4O. rewrite tetakeE totakeE (eqP tE) !(etake_cat, otake_cat, otake_nseq, etake_nseq, size_cat, size_nseq, uphalf_half) oddD n1E n2E in n1P n2P. case: (boolP (odd a3)) b3O => [a3O /negP/negP b3O |/negPf a3E b3E]. case: (boolP (odd a4)) b4O => [a4O /negP/negP b4O|/negPf a4E b4E]. rewrite a3O a4O b3O b4O [if true (+) true then _ else _]/= !add1n in n1P. rewrite a3O a4O b3O b4O [if true (+) true then _ else _]/= !add1n in n2P. have [/eqP Ea1 /eqP Eb1] : a1 == (a3./2 + a4./2).+2 /\ b1 == b3./2 + b4./2. move/allP/(_ false) : (n1P); move/allP/(_ true) : n1P. rewrite /= !(count_cat, count_nseq) /= !(count_cat, count_nseq) /=. rewrite !mul1n !mul0n !(addn0, add0n) !add1n !(addSn, addnS). rewrite !(mem_cat, inE, mem_nseq, eqxx, orbT, orTb, orFb, orbF, andbF, andbT) => Hb1 -> //; split=> //. by case: (b1) Hb1 => [|x] //; (do 2 case (_./2) => [|?]) => // ->. have [/eqP Ea2 /eqP Eb2] : a2 == a3./2 + a4./2 /\ b2 == (b3./2 + b4./2).+2. move/allP/(_ false) : (n2P); move/allP/(_ true) : n2P. rewrite /= !(count_cat, count_nseq) /= !(count_cat, count_nseq) /=. rewrite !mul1n !mul0n !(addn0, add0n, add1n, addSn, addnS). rewrite !(mem_cat, mem_nseq, inE, eqxx, orTb, andTb, andbT, orbT, andbF, orFb, orbF) => -> //. by case: (a2) => [|?]//; (do 2 (case: (_./2) => [|?]//)) => ->. by move=> {a3O b3O a4O b4O n1P n2P}//; lia. rewrite /= in b4E. rewrite a3O b3O a4E b4E [if true (+) true then _ else _]/= !add0n !add1n in n1P. rewrite a3O a4E b3O b4E [if true (+) true then _ else _]/= in n2P. have [/eqP Ea1 /eqP Eb1] : a1 == (a3./2 + a4./2).+1 /\ b1 == b3./2 + b4./2. move/allP/(_ false) : (n1P); move/allP/(_ true) : n1P. rewrite /= !(count_cat, count_nseq) /= . rewrite !mul1n !mul0n !(addn0, add0n) !add1n /=. rewrite !(mem_cat, inE, mem_nseq, eqxx, orbT, orTb, orFb, orbF, andbF, andbT) /= => Hb1 ->; split=> //. by case: (b1) Hb1 => [|x]; (do 2 case (_./2) => [|?]) => // ->. have [/eqP Ea2 /eqP Eb2] : a2 == a3./2 + a4./2 /\ b2 == (b3./2 + b4./2).+1. move/allP/(_ false) : (n2P); move/allP/(_ true) : n2P. rewrite /= !(count_cat, count_nseq) /= !(count_cat, count_nseq) /=. rewrite !mul1n !mul0n !(addn0, add0n, add1n, addSn, addnS). rewrite !(mem_cat, mem_nseq, inE, eqxx, orTb, andTb, andbT, orbT, andbF, orFb, orbF) => -> //. by case: (a2) => [|?]//; (do 2 (case: (_./2) => [|?]//)) => ->. by move=> {a3O b3O a4E b4E n1P n2P}//; lia. case: (boolP (odd a4)) b4O => [a4O /negP/negP b4O|/negPf a4E b4E]. rewrite /= in b3E. rewrite a3E b3E a4O [if false (+) false then _ else _]/= !add0n in n1P. rewrite a3E b3E a4O b4O [if false (+) false then _ else _]/= in n2P. have [/eqP Ea1 /eqP Eb1] : a1 == (a3./2 + a4./2).+1 /\ b1 == b3./2 + b4./2. move/allP/(_ false) : (n1P); move/allP/(_ true) : n1P. rewrite /= !(count_cat, count_nseq) /= !(count_cat, count_nseq) /=. rewrite !mul1n !mul0n !(addn0, add0n) !add1n !(addSn, addnS). rewrite !(mem_cat, inE, mem_nseq, eqxx, orbT, orTb, orFb, orbF, andbF, andbT) => Hb1 -> //; split => //. by case: (b1) Hb1 => // => [|x]; (do 2 case (_./2) => [|?]) => // ->. have [/eqP Ea2 /eqP Eb2] : a2 == a3./2 + a4./2 /\ b2 == (b3./2 + b4./2).+1. move/allP/(_ false) : (n2P); move/allP/(_ true) : n2P. rewrite /= !(count_cat, count_nseq) /= !(count_cat, count_nseq) /=. rewrite !mul1n !mul0n !(addn0, add0n, add1n, addSn, addnS). rewrite !(mem_cat, mem_nseq, inE, eqxx, orTb, andTb, andbT, orbT, andbF, orFb, orbF) => -> // Hb1; split => //. by case: (a2) Hb1 => [|?]//; (do 2 (case: (_./2) => [|?]//)) => ->. by move=> {a3E b3E a4O b4O n1P n2P}//; lia. rewrite /= in a3E b3E b4E. rewrite a3E b3E a4E b4E [if false (+) false then _ else _]/= !add0n in n1P. rewrite a3E b3E a4E b4E [if false (+) false then _ else _]/= in n2P. have [/eqP Ea1 /eqP Eb1] : a1 == a3./2 + a4./2 /\ b1 == b3./2 + b4./2. move/allP/(_ false) : (n1P); move/allP/(_ true) : n1P. rewrite /= !(count_cat, count_nseq) /=. rewrite !mul1n !mul0n !(addn0, add0n). rewrite !(mem_cat, inE, mem_nseq, eqxx, orbT, orTb, orFb, orbF, andbF, andbT) => Hb1 Ha1 //; split. by case: (a1) Ha1 => [|x]; (do 2 case (_./2) => [|?]) => // ->. by case: (b1) Hb1 => [|x]; (do 2 case (_./2) => [|?]) => // ->. have [/eqP Ea2 /eqP Eb2] : a2 == a3./2 + a4./2 /\ b2 == b3./2 + b4./2. move/allP/(_ false) : (n2P); move/allP/(_ true) : n2P. rewrite /= !(count_cat, count_nseq) /=. rewrite !mul1n !mul0n !(addn0, add0n, add1n, addSn, addnS). rewrite !(mem_cat, mem_nseq, inE, eqxx, orTb, andTb, andbT, orbT, andbF, orFb, orbF) => Hb2 Ha2; split. by case: (a2) Ha2 => [|?]//; (do 2 (case: (_./2) => [|?]//)) => ->. by case: (b2) Hb2 => [|?]//; (do 2 (case: (_./2) => [|?]//)) => ->. by move=> {a3E b3E a4E b4E n1P n2P}//; lia. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort