proposition: Lemma sorted_eswap m (t : (m + m).-tuple bool) : sorted <=%O (tetake t) -> sorted <=%O (totake t) -> let t1 := cfun ceswap t in [/\ sorted <=%O (tetake t1), sorted <=%O (totake t1) & noF (totake t1) <= noF (tetake t1)].
proof: Proof. rewrite !isorted_noFT => /eqP teE /eqP toE t1. set a := noF (tetake t) in teE; set b := noT (tetake t) in teE. set c := noF (totake t) in toE; set d := noT (totake t) in toE. have mEmaxmin : m = maxn a c + minn b d. case: (leqP a c) => [aLc | cLa]. rewrite (minn_idPr _); first by rewrite size_noFT size_tuple. rewrite -(leq_add2l a) size_noFT size_tuple -(size_tuple (totake t)). by rewrite -size_noFT -/c -/d leq_add2r. rewrite (minn_idPl _); first by rewrite size_noFT size_tuple. rewrite -(leq_add2l a) size_noFT size_tuple -(size_tuple (totake t)). by rewrite -size_noFT -/c -/d leq_add2r ltnW. have mEminmax : m = minn a c + maxn b d. case: (leqP a c) => [aLc | cLa]. rewrite (maxn_idPl _); first by rewrite size_noFT size_tuple. rewrite -(leq_add2l a) size_noFT size_tuple -(size_tuple (totake t)). by rewrite -size_noFT -/c -/d leq_add2r. rewrite (maxn_idPr _); first by rewrite size_noFT size_tuple. rewrite -(leq_add2l a) size_noFT size_tuple -(size_tuple (totake t)). by rewrite -size_noFT -/c -/d leq_add2r ltnW. suff t1E : t1 = eocat (nseq (maxn a c) false ++ nseq (minn b d) true) (nseq (minn a c) false ++ nseq (maxn b d) true) :> seq _. rewrite tetakeE totakeE t1E otakeK ?etakeK. by rewrite !isorted_noFT !noE !eqxx; case: (ltngtP a c) => // /ltnW->. by rewrite !(size_cat, size_nseq) -mEmaxmin. apply: (@eq_from_nth _ true) => [|i]. rewrite /= [LHS]size_tuple card_ord size_eocat size_cat !size_nseq. by rewrite -mEmaxmin. rewrite [X in _ < X -> _]size_tuple => iLab. pose x := Ordinal iLab. rewrite /t1 cfun_eswap /= (nth_map x) /= -[i]/(x : nat); last first. by rewrite -enum_ord size_enum_ord. rewrite -enum_ord !nth_ord_enum. rewrite nth_eocat; last first. by rewrite !size_cat !size_nseq // -mEminmax. rewrite !(tnth_nth true) [t]eocat_tetake_totake /=. rewrite !nth_eocat /=; try by rewrite !size_tuple. have i2Lm : i./2 < m by rewrite ltn_half_double -addnn. have [iO|iE] := boolP (odd _). have i_gt0 : 0 < i by case: (i) iO. have i1E : ~~ odd i.-1 by rewrite -oddS prednK. rewrite val_ipred /= (negPf i1E). have -> : i.-1./2 = i./2. by rewrite -[X in _ = X./2]prednK // -uphalfE uphalf_half (negPf i1E). by rewrite teE toE !nth_cat_seqT -/a -/c geq_min; do 2 case: leqP => ?. rewrite val_inext; case: eqP =>/= [i1E| _]. have := iE; rewrite i1E -oddS prednK ?(leq_ltn_trans _ iLab) //. by rewrite [X in odd X]addnn odd_double. rewrite (negPf iE) /= uphalf_half (negPf iE) /= add0n. by rewrite teE toE !nth_cat_seqT -/a -/c geq_max; do 2 case: leqP => ?. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort