proposition: Lemma refin_qperm_partl_writeList (p x : E) (ys zs xs : seq E) i : (forall ys zs, writeList (M := M) i (ys ++ zs ++ xs) >> ipartl p i (size ys) (size zs) (size xs) `<=` qperm_partl p ys zs xs >>= write2L i) -> (writeList (M := M) (i + (size ys + size zs).+1) xs >> if x <= p then qperm zs >>= (fun zs' => writeList i (ys ++ x :: zs') >> ipartl p i (size ys).+1 (size zs') (size xs)) else qperm (rcons zs x) >>= (fun zs' => writeList i (ys ++ zs') >> ipartl p i (size ys) (size zs') (size xs))) `<=` qperm_partl p ys zs (x :: xs) >>= write2L i.
proof: Proof. move=> ih; rewrite qperm_partl_cons. apply: refin_trans; last exact: (refin_dispatch_Ret_write3L_ipartl ih). rewrite qperm_preserves_length. rewrite bindA; apply refin_bindl => -[]. rewrite if_bind; apply: refin_if => _; rewrite bindA; apply: refin_bindl => zs'. - by rewrite bindretf size_rcons -cats1 -catA /=; exact: refin_refl. - by rewrite bindretf; exact: refin_refl. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)