proposition: Lemma slowsort_splits p s : slowsort (p :: s) = splits s >>= (fun x => guard (is_partition p x) >> slowsort x.1 >>= (fun a => slowsort x.2 >>= (fun b => Ret (a ++ p :: b)))).
proof: Proof. rewrite slowsort_cons; bind_ext=> {s} -[a b]. rewrite /is_partition /slowsort !kleisliE. rewrite guard_and !bindA/= (plus_commute (guard (all (>= p) b)))//=. rewrite (plus_commute (guard (all (<= p) a)))// guard_all_qperm. bind_ext=> a'. rewrite plus_commute// assertE bindA bindretf bindA. rewrite (plus_commute (guard (sorted a')))//. rewrite (plus_commute (guard (all (<= p) a')))// plus_commute// guard_all_qperm. bind_ext=> b'. rewrite (plus_commute (guard (all (>= p) b')))// !assertE bindA bindretf. by rewrite sorted_cat_cons andbC -!andbA andbC !guard_and !bindA. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)