proposition: Lemma partition_spec (p : T) (xs : seq T) : ((@ret M _) \o partition p) xs `<=` splits xs >>= assert (is_partition p).
proof: Proof. elim: xs p => [/=|x xs ih] p. rewrite bindretf !assertE /is_partition guardT bindskipf; exact: refin_refl. rewrite /= bindA. apply: (refin_trans _ (refin_bindl _ _)); last first => [yz|]. rewrite alt_bindDl 2!bindretf 2!assertE. rewrite 2!is_partition_consE 2!guard_and 2!bindA. exact/(refin_alt (refin_refl _))/refin_bindr/refin_guard_le. apply: (refin_trans _ (refin_bindl _ _)); last first => [yz|]. exact: refin_if_guard. under eq_bind do rewrite -bind_if. apply: (@refin_trans _ _ (splits xs >>= fun a => guard (is_partition p a) >> (Ret a >>= fun a => (if x <= p then Ret (x :: a.1, a.2) else Ret (a.1, x :: a.2))))); last first. apply: refin_bindl => ?; apply: refin_bindl => ?. rewrite bindretf; exact: refin_refl. under eq_bind do rewrite -bindA -assertE. rewrite -bindA; apply: (refin_trans _ (refin_bindr _ (ih _))). rewrite bindretf; case: ifPn => ?; exact: refin_refl. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)