proposition: Lemma bitonic_half_cleaner fb m (t : (m + m).-tuple bool) : (t : seq _) \is bitonic -> let t1 := cfun (half_cleaner fb m) t in (ttake t1 == nseq m fb :> seq _) && ((tdrop t1 : seq _) \is bitonic) || (tdrop t1 == nseq m (~~fb) :> seq _) && ((ttake t1 : seq _) \is bitonic).
proof: Proof. move=> /bitonic_boolP[[[[b i] j] k] tE] /=; set t1 := cfun _ _. have mmE : m + m = i + j + k. by rewrite -(size_tuple t) tE !size_cat !size_nseq addnA. have [iLm|mLi]:= leqP i m; last first. pose smin := nseq (i - m) b ++ nseq j false ++ nseq k b. pose smax := nseq (i - m) b ++ nseq j true ++ nseq k b. have mE : m = i - m + j + k. by rewrite -addnA addnBAC 1?ltnW // addnA -mmE addnK. have ttE : ttake t1 = (if fb then smax else smin) :> seq bool. apply: (@eq_from_nth _ false) => [|u]. by case: (fb); rewrite size_tuple !size_cat !size_nseq addnA. rewrite size_tuple => uLm. rewrite /ttake val_tcast nth_take // /t1 cfun_half_cleaner /=. have uLi : u < i by apply: ltn_trans mLi. have uLmm : u < m + m by apply: leq_trans uLm (leq_addl _ _). rewrite (nth_map (Ordinal uLmm)) -1?enum_ord ?size_enum_ord //. have {2}->: u = (Ordinal uLmm) :> nat by []. rewrite nth_ord_enum /=; case: splitP => /= u1 uE; last by lia. rewrite !(tnth_nth false) /= tE !nth_cat !size_nseq !nth_nseq -uE. by case: (fb); rewrite !nth_cat !size_nseq !nth_nseq; repeat (case: leqP => ?; try lia); case: (b). have tdE : tdrop t1 = (if fb then smin else smax) :> seq bool. apply: (@eq_from_nth _ false) => [|u]. by rewrite fun_if size_tuple !size_cat !size_nseq addnA if_same. rewrite size_tuple => uLn. rewrite /tdrop val_tcast nth_drop // /t1 cfun_half_cleaner /=. have uLi : u < i by apply: ltn_trans mLi. have muLmm : m + u < m + m by rewrite ltn_add2l. rewrite (nth_map (Ordinal muLmm)) -1?enum_ord ?size_enum_ord //. have {2}->: m + u = (Ordinal muLmm) :> nat by []. rewrite nth_ord_enum /=; case: splitP => /= u1 uE. by have := ltn_ord u1; lia. have {}uE : u = u1 by rewrite -[u](addnK m) addnC uE addnC addnK. rewrite !(tnth_nth false) /= tE !nth_cat !size_nseq !nth_nseq -uE. by case: (fb); rewrite !nth_cat !size_nseq !nth_nseq; repeat (case: leqP => ?; try lia); case: (b). rewrite {}/smin {}/smax in ttE tdE. case: (fb) tE ttE tdE; case: (b); rewrite -!nseqD => /= tE ttE tdE. - apply/orP; left. rewrite ttE addnBAC 1?ltnW // addnA -mmE addnK eqxx /=. by apply/bitonic_boolP; exists (true, i - m, j, k). - apply/orP; right. rewrite tdE addnBAC 1?ltnW // addnA -mmE addnK eqxx /=. by apply/bitonic_boolP; exists (false, i - m, j, k). - apply/orP; right. rewrite tdE addnBAC 1?ltnW // addnA -mmE addnK eqxx /=. by apply/bitonic_boolP; exists (true, i - m, j, k). apply/orP; left. rewrite ttE addnBAC 1?ltnW // addnA -mmE addnK eqxx /=. by apply/bitonic_boolP; exists (false, i - m, j, k). have [ijLm|mLij]:= leqP (i + j) m. have mE : m = i + j + k - m by rewrite -mmE addnK. pose smin := nseq i b ++ nseq j false ++ nseq (m - (i + j)) b. pose smax := nseq i b ++ nseq j true ++ nseq (m - (i + j)) b. have ttE : ttake t1 = (if fb then smax else smin) :> seq bool. apply: (@eq_from_nth _ false) => [|u]. by case: (fb); rewrite size_tuple !size_cat !size_nseq; lia. rewrite size_tuple => uLm. rewrite /ttake val_tcast nth_take // /t1 cfun_half_cleaner /=. have uLmm : u < m + m by apply: leq_trans uLm (leq_addl _ _). rewrite (nth_map (Ordinal uLmm)) -1?enum_ord ?size_enum_ord //. have {2}->: u = (Ordinal uLmm) :> nat by []. rewrite nth_ord_enum /=; case: splitP => /= u1 uE; last by lia. rewrite !(tnth_nth false) /= tE !nth_cat !size_nseq !nth_nseq -uE. by case: (fb); rewrite !nth_cat !size_nseq !nth_nseq; repeat (case: leqP => ?; try lia); case: (b). have tdE : tdrop t1 = (if fb then smin else smax) :> seq bool. apply: (@eq_from_nth _ false) => [|u]. by case: (fb); rewrite size_tuple !size_cat !size_nseq; lia. rewrite size_tuple => uLn. rewrite /tdrop val_tcast nth_drop // /t1 cfun_half_cleaner /=. have uLmm : u < m + m by apply: leq_trans uLn (leq_addl _ _). have muLmm : m + u < m + m by rewrite ltn_add2l. rewrite (nth_map (Ordinal muLmm)) -1?enum_ord ?size_enum_ord //. have {2}->: m + u = (Ordinal muLmm) :> nat by []. rewrite nth_ord_enum /=; case: splitP => /= u1 uE. by move: (ltn_ord u1); lia. have {}uE : u = u1 by rewrite -[u](addnK m) addnC uE addnC addnK. rewrite !(tnth_nth false) /= tE !nth_cat !size_nseq !nth_nseq -uE. by case: (fb); rewrite !nth_cat !size_nseq !nth_nseq; repeat (case: leqP => ?; try lia); case: (b). rewrite {}/smin {}/smax in ttE tdE. case: (fb) tE ttE tdE; case: (b); rewrite -!nseqD => /= tE ttE tdE. - apply/orP; left. rewrite ttE addnA addnC subnK // eqxx /=. by apply/bitonic_boolP; exists (true, i, j, m - (i + j)). - apply/orP; right. rewrite tdE addnA addnC subnK // eqxx /=. by apply/bitonic_boolP; exists (false, i, j, m - (i + j)). - apply/orP; right. rewrite tdE addnA addnC subnK // eqxx /=. by apply/bitonic_boolP; exists (true, i, j, m - (i + j)). apply/orP; left. rewrite ttE addnA addnC subnK // eqxx /=. by apply/bitonic_boolP; exists (false, i, j, m - (i + j)). have mE : m = i + j + k - m by rewrite -mmE addnK. have [jLm|mLj]:= leqP j m. pose smin := nseq (i + j - m) false ++ nseq (m - j) b ++ nseq (m - i) false. pose smax := nseq (i + j - m) true ++ nseq (m - j) b ++ nseq (m - i) true. have ttE : ttake t1 = (if fb then smax else smin) :> seq bool. apply: (@eq_from_nth _ false) => [|u]. by case: (fb); rewrite size_tuple !size_cat !size_nseq; lia. rewrite size_tuple => uLm. rewrite /ttake val_tcast nth_take // /t1 cfun_half_cleaner /=. have uLmm : u < m + m by lia. rewrite (nth_map (Ordinal uLmm)) -1?enum_ord ?size_enum_ord //. have {2}->: u = (Ordinal uLmm) :> nat by []. rewrite nth_ord_enum /=; case: splitP => /= u1 uE; last by lia. rewrite !(tnth_nth false) /= tE !nth_cat !size_nseq !nth_nseq -uE. by case: (fb); rewrite !nth_cat !size_nseq !nth_nseq; repeat (case: leqP => ?; try lia); case: (b). have tdE : tdrop t1 = (if fb then smin else smax) :> seq bool. apply: (@eq_from_nth _ false) => [|u]. by case: (fb); rewrite size_tuple !size_cat !size_nseq; lia. rewrite size_tuple => uLm. rewrite /tdrop val_tcast nth_drop // /t1 cfun_half_cleaner /=. have uLmm : u < m + m by apply: leq_trans uLm (leq_addl _ _). have muLmm : m + u < m + m by rewrite ltn_add2l. rewrite (nth_map (Ordinal muLmm)) -1?enum_ord ?size_enum_ord //. have {2}->: m + u = (Ordinal muLmm) :> nat by []. rewrite nth_ord_enum /=; case: splitP => /= u1 uE. by move: (ltn_ord u1); lia. have {}uE : u = u1 by rewrite -[u](addnK m) addnC uE addnC addnK. rewrite !(tnth_nth false) /= tE !nth_cat !size_nseq !nth_nseq -uE. by case: (fb); rewrite !nth_cat !size_nseq !nth_nseq; repeat (case: leqP => ?; try lia); case: (b). rewrite {}/smin {}/smax in ttE tdE. case: (fb) tE ttE tdE; case: (b); rewrite -!nseqD => /= tE ttE tdE. - apply/orP; left. rewrite ttE; apply/andP; split; first by apply/eqP; congr nseq; lia. by apply/bitonic_boolP; exists (false, i + j - m, m - j, m - i). - apply/orP; right. rewrite tdE; apply/andP; split; first by apply/eqP; congr nseq; lia. by apply/bitonic_boolP; exists (true, i + j - m, m - j, m - i). - apply/orP; right. rewrite tdE; apply/andP; split; first by apply/eqP; congr nseq; lia. by apply/bitonic_boolP; exists (false, i + j - m, m - j, m - i). apply/orP; left. rewrite ttE; apply/andP; split; first by apply/eqP; congr nseq; lia. by apply/bitonic_boolP; exists (true, i + j - m, m - j, m - i). pose smin := nseq i false ++ nseq (j - m) (~~b) ++ nseq k false. pose smax := nseq i true ++ nseq (j - m) (~~ b) ++ nseq k true. have ttE : ttake t1 = (if fb then smax else smin) :> seq bool. apply: (@eq_from_nth _ false) => [|u]. by case: (fb); rewrite size_tuple !size_cat !size_nseq; lia. rewrite size_tuple => uLm. rewrite /ttake val_tcast nth_take // /t1 cfun_half_cleaner /=. have uLmm : u < m + m by lia. rewrite (nth_map (Ordinal uLmm)) -1?enum_ord ?size_enum_ord //. have {2}->: u = (Ordinal uLmm) :> nat by []. rewrite nth_ord_enum /=; case: splitP => /= u1 uE; last by lia. rewrite !(tnth_nth false) /= tE !nth_cat !size_nseq !nth_nseq -uE. by case: (fb); rewrite !nth_cat !size_nseq !nth_nseq; repeat (case: leqP => ?; try lia); case: (b). have tdE : tdrop t1 = (if fb then smin else smax) :> seq bool. apply: (@eq_from_nth _ false) => [|u]. by case: (fb); rewrite size_tuple !size_cat !size_nseq; lia. rewrite size_tuple => uLm. rewrite /tdrop val_tcast nth_drop // /t1 cfun_half_cleaner /=. have uLmm : u < m + m by apply: leq_trans uLm (leq_addl _ _). have muLmm : m + u < m + m by rewrite ltn_add2l. rewrite (nth_map (Ordinal muLmm)) -1?enum_ord ?size_enum_ord //. have {2}->: m + u = (Ordinal muLmm) :> nat by []. rewrite nth_ord_enum /=; case: splitP => /= u1 uE. by move: (ltn_ord u1); lia. have {}uE : u = u1 by rewrite -[u](addnK m) addnC uE addnC addnK. rewrite !(tnth_nth false) /= tE !nth_cat !size_nseq !nth_nseq -uE. by case: (fb); rewrite !nth_cat !size_nseq !nth_nseq; repeat (case: leqP => ?; try lia); case: (b). rewrite {}/smin {}/smax in ttE tdE. case: (fb) tE ttE tdE; case: (b); rewrite -!nseqD => /= tE ttE tdE. - apply/orP; right. rewrite tdE; apply/andP; split; first by apply/eqP; congr nseq; lia. by apply/bitonic_boolP; exists (true, i, j - m, k). - apply/orP; left. rewrite ttE; apply/andP; split; first by apply/eqP; congr nseq; lia. by apply/bitonic_boolP; exists (false, i, j - m, k). - apply/orP; left. rewrite ttE; apply/andP; split; first by apply/eqP; congr nseq; lia. by apply/bitonic_boolP; exists (true, i, j - m, k). apply/orP; right. rewrite tdE; apply/andP; split; first by apply/eqP; congr nseq; lia. by apply/bitonic_boolP; exists (false, i, j - m, k). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort