proposition: Lemma sorted_iter1 (p : nat) (s : seq bool) i : i < `2^ p -> let s1 := iter1 (`2^ p) s in sorted <=%O (eotake p.+1 i s) -> sorted <=%O (eotake p.+1 (`2^ p + i) s) -> [/\ sorted <=%O (eotake p.+1 i s1), sorted <=%O (eotake p.+1 (`2^p + i) s1) & noF (eotake p.+1 (`2^p + i) s1) <= noF (eotake p.+1 i s1)].
proof: Proof. move=> iL2p s1. set s2 := eotake _ _ _; set s3 := eotake _ _ _. pose d : nat := (size s2 != size s3). move=> /isorted_boolP[[a1 b1] s2E] /isorted_boolP[[a2 b2] s3E]. pose sl := eotake p i s. have ss2E : size s2 = uphalf (size sl) by rewrite -size_etake etake_eotake. have ss3E : size s3 = (size sl)./2 by rewrite -size_otake otake_eotake. have dE : d = odd (size sl). rewrite /d ss2E ss3E uphalf_half; case odd; rewrite /= ?eqxx ?add1n //. by case: ltngtP (leqnn (size sl)./2.+1). rewrite uphalf_half -dE s2E size_cat !size_nseq in ss2E. rewrite s3E size_cat !size_nseq in ss3E. have a1b1E : a1 + b1 = a2 + b2 + d by rewrite ss2E addnC ss3E. pose s4 := nseq (maxn a1 a2) false ++ nseq (minn b1 (d + b2)) true. have s4S : size s4 = size (eotake p.+1 i s1). rewrite size_cat !size_nseq. rewrite (eq_size_eotake _ _ (size_iter1 s (e2n_gt0 _))). rewrite -/s2 s2E size_cat !size_nseq. lia. pose s5 := nseq (minn a1 a2) false ++ nseq (maxn b1 (d + b2) - d) true. have s5S : size s5 = size (eotake p.+1 (`2^ p + i) s1). rewrite size_cat !size_nseq. rewrite (eq_size_eotake _ _ (size_iter1 s (e2n_gt0 _))). rewrite -/s3 s3E size_cat !size_nseq. lia. have <- : s4 = eotake p.+1 i s1. apply: (@eq_from_nth _ true) => // k kLs. rewrite !nth_cat !nth_nseq if_same. rewrite nth_eotake nth_iter1 ?e2n_gt0 //. rewrite -nth_eotake -/s2 !modn_small; last first. by rewrite (leq_trans iL2p) // leq_addr. rewrite [_ + `2^ _]addnC addnA. rewrite -[_ + i](modn_small (_ : _ < `2^ p.+1)); last first. by rewrite e2Sn ltn_add2l. rewrite -nth_eotake -/s3. rewrite [X in (i + X * _) %/ _]e2Sn addnn -muln2 -mulnA mulnC. rewrite divnDMl ?e2n_gt0 // oddD mul2n odd_double addbF. rewrite divn_small //= modn_small ?ltn_add2l //. rewrite s2E s3E !nth_cat !nth_nseq !size_nseq !if_same. case: (ltnP a1 a2) => [a1La2|a2La1]. case: (ltnP k a1) => [a1Lk|kLa1]. rewrite !(leq_trans a1Lk (ltnW _)) //=; last first. by rewrite minxx if_same. case: (ltnP k a2) => [a2Lk|kLa2]. suff /gtn_size_eotake-> : k < size (eotake p.+1 (`2^ p + i) s). - by rewrite minbF. - by rewrite ltn_add2l. have : k < size s5. rewrite size_cat !size_nseq. have -> : minn a1 a2 = a1 by lia. have -> : maxn b1 (d + b2) = b1 by lia. have -> : a1 + (b1 - d) = a2 + b2 by lia. by apply: leq_trans (leq_addr _ _). rewrite s5S. by rewrite (eq_size_eotake _ _ (size_iter1 _ _)) // e2n_gt0. by rewrite !if_same. case: (ltnP k a2) => [a2Lk|kLa2]. by rewrite !(leq_trans a2Lk _) // minxx if_same. by case: (ltnP k a1) => [a1Lk|kLa1]; rewrite if_same. have <- : nseq (minn a1 a2) false ++ nseq (maxn b1 (d + b2) - d) true = eotake p.+1 (`2^ p + i) s1. apply: (@eq_from_nth _ true) => [|k]. rewrite size_cat !size_nseq. rewrite (eq_size_eotake _ _ (size_iter1 s (e2n_gt0 _))). rewrite -/s3 s3E size_cat !size_nseq. lia. rewrite nth_cat !nth_nseq !size_cat !size_nseq if_same. rewrite nth_eotake nth_iter1 ?e2n_gt0 //. rewrite -nth_eotake -/s2 !modn_small; last first. by rewrite e2Sn ltn_add2l. rewrite [_ + `2^ _]addnC addnA. rewrite -[X in X - `2^ _]addnA [X in X - `2^ _]addnC addnK. rewrite -[in i + _ * k](modn_small (_ : i < `2^ p.+1)); last first. by rewrite (leq_trans iL2p (leq_addr _ _)). rewrite -nth_eotake -/s2 -/s3. rewrite [X in (_ + X * _) %/ _]e2Sn addnn -muln2 -mulnA mulnC. rewrite divnDMl ?e2n_gt0 // oddD mul2n odd_double addbF. rewrite -[X in X + i]mul1n [1 * _ + _]addnC divnDMl ?e2n_gt0 //. rewrite divn_small //= mul1n. rewrite s2E s3E !nth_cat !nth_nseq !size_nseq !if_same. case: (ltnP a1 a2) => [a1La2|a2La1]. have -> : maxn b1 (d + b2) = b1 by lia. case: (ltnP k a1) => [a1Lk|kLa1]. rewrite !(leq_trans a1Lk _) //=; last first. - by apply: (leq_addr _ _). - by apply: ltnW. by rewrite maxxx if_same. case: (ltnP k a2) => [a2Lk|kLa2]. rewrite ifT // -e2Sn [i + _]addnC. suff /gtn_size_eotake-> : k < size (eotake p.+1 (`2^ p + i) s) => //. by rewrite ltn_add2l. have : k < size s5. rewrite size_cat !size_nseq. have -> : minn a1 a2 = a1 by lia. have -> : maxn b1 (d + b2) = b1 by lia. have -> : a1 + (b1 - d) = a2 + b2 by lia. by apply: leq_trans (leq_addr _ _). rewrite s5S. by rewrite (eq_size_eotake _ _ (size_iter1 _ _)) // e2n_gt0. by rewrite !if_same. have -> : maxn b1 (d + b2) = d + b2 by lia. case: (ltnP k a2) => [a2Lk|kLa2] _. by rewrite !(leq_trans a2Lk _) // maxxx if_same. by case: (ltnP k a1) => [a1Lk|kLa1]; rewrite if_same. split. - by apply/isorted_boolP; exists (maxn a1 a2, minn b1 (d + b2)). - by apply/isorted_boolP; exists (minn a1 a2, maxn b1 (d + b2) - d). by rewrite !noE; case: (ltnP a1 a2) => // ?; rewrite ltnW. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort