proposition: Lemma bitonic_boolP (s : seq bool) : reflect (exists t, let: (b,i,j,k) := t in s = nseq i b ++ nseq j (~~ b) ++ nseq k b) (s \is bitonic).
proof: Proof. apply: (iffP existsP) => /= [[x /existsP[n /andP[isort dsort]]]| [[[[b i] j] k] ->]]; last first. rewrite !size_cat !size_nseq. case: b => /=. have iL : i < (i + (j + k)).+1 by lia. have jL : j < (i + (j + k)).+1 by lia. exists (Ordinal iL); apply/existsP; exists (Ordinal jL) => /=. rewrite -[X in rot X](size_nseq i true) rot_size_cat. rewrite -catA take_cat size_nseq ltnn subnn take0 cats0. rewrite isorted_bool_nseq /= drop_cat size_nseq ltnn subnn drop0. by rewrite -nseqD dsorted_bool_nseq. have iL : i < (i + (j + k)).+1 by lia. exists (Ordinal iL); apply/existsP; exists ord0 => /=. rewrite take0 drop0 /= -[X in rot X](size_nseq i false) rot_size_cat. by rewrite -catA -nseqD; apply/dsorted_boolP; exists (j, k + i). have /isorted_boolP[[j1 k1] Hirot] := isort. have /dsorted_boolP[[j2 k2] Hdrot] := dsort. have -> : s = rotr x (nseq j1 false ++ nseq (k1 + j2) true ++ nseq k2 false). apply: (@rot_inj x); rewrite rotrK. by rewrite -[LHS](cat_take_drop n) Hirot Hdrot nseqD !catA. rewrite /rotr !size_cat !size_nseq. set i1 := j1 + (k1 + j2 + k2) - x. have [i1Lj1|j1Li1] := leqP i1 j1. rewrite -(subnK i1Lj1) addnC nseqD -catA. rewrite -{1}[i1](size_nseq i1 false) rot_size_cat. by exists (false, j1 - i1, k1 + j2, k2 + i1); rewrite !nseqD !catA. have [i1j1Lk1j2|k1j2Li1j1] := leqP (i1 - j1) (k1 + j2). rewrite -(subnK i1j1Lk1j2) addnC !nseqD -!catA catA. have {1}-> : i1 = size (nseq j1 false ++ nseq (i1 - j1) true). by rewrite size_cat !size_nseq addnC subnK // ltnW. rewrite rot_size_cat. by exists (true, k1 + j2 - (i1 - j1), k2 + j1, i1 - j1); rewrite nseqD !catA. have [i1j1k1j2Lk2|k2Li1j1k1j2] := leqP (i1 - j1 - (k1 + j2)) k2. rewrite -(subnK i1j1k1j2Lk2) [k2 - _ + _]addnC !nseqD -nseqD. have {1}-> : i1 = size (nseq j1 false ++ nseq (j2 + k1) true ++ nseq (i1 - j1 - (j2 + k1)) false). rewrite !size_cat !size_nseq [j2 + k1 + _]addnC subnK 1?ltnW //. by rewrite [j1 + _]addnC subnK // ltnW. by rewrite addnC. rewrite [k1 + _]addnC !catA -catA rot_size_cat. exists (false, k2 - (i1 - j1 - (j2 + k1)) + j1, j2 + k1, (i1 - j1 - (j2 + k1))). by rewrite !nseqD !catA. rewrite rot_oversize. by exists (false, j1, k1 + j2, k2); rewrite !catA. rewrite !size_cat !size_nseq. rewrite -leq_subRL; last by apply: ltnW. by rewrite -leq_subRL ltnW. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort