proposition: Lemma refin_ipartl p i (xs zs ys : seq E) : write3L i (ys, zs, xs) >>= uncurry3 (ipartl p i) `<=` qperm_partl (M := M) p ys zs xs >>= write2L i.
proof: Proof. elim: xs i p zs ys => [|h t ih] i p zs ys. apply: eq_refin. by rewrite /= bindretf cats0 bindA bindretf. have : (forall ys zs, writeList i (ys ++ zs ++ t) >> ipartl (M := M) p i (size ys) (size zs) (size t) `<=` qperm_partl p ys zs t >>= write2L i). move=> {}ys {}zs; apply: (refin_trans _ (ih i p _ _)). by rewrite write3LE; exact: refin_refl. move=> /(@refin_qperm_partl_writeList _ E M p h ys zs t i). apply: refin_trans. apply: (@refin_trans _ _ (writeList (i + (size ys + size zs).+1) t >> (if h <= p then writeList i (rcons (ys ++ zs) h) >> aswap (i + size ys) (i + size (ys ++ zs)) >> ipartl p i (size ys).+1 (size zs) (size t) else writeList i (rcons (ys ++ zs) h) >> ipartl p i (size ys) (size zs).+1 (size t)))); last first. apply: refin_bindl => -[]. apply: refin_if => hp; last first. apply: (@refin_trans _ _ (Ret (rcons zs h) >>= fun zs' => writeList i (ys ++ zs') >> ipartl p i (size ys) (size zs') (size t))); last first. exact/refin_bindr/refin_qperm_ret. by rewrite bindretf size_rcons rcons_cat; exact: refin_refl. rewrite -[X in _ `<=` X](qperm_preserves_size2 zs (fun a b => writeList i (ys ++ h :: a) >> ipartl p i (size ys).+1 b (size t))). rewrite -[in X in _ `<=` X]bindA. exact/refin_bindr/refin_writeList_rcons_cat_aswap. rewrite -size_cat. rewrite bindA writeList_ipartl write3LE. rewrite /uncurry3 /= -addnA -size_cat. by rewrite bindA -catA; exact: refin_refl. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)