proposition: Lemma qperm_preserves_length i (x p : E) (ys zs xs : seq E) D (k : nat -> nat -> nat -> M D) : (dispatch_Ret x p (ys, zs, xs) >>= write3L i) >>= uncurry3 k = writeList (i + (size ys + size zs).+1) xs >> dispatch_Ret x p (ys, zs, xs) >>= (fun '(ys', zs', xs') => writeList i (ys' ++ zs') >> k (size ys') (size zs') (size xs')) :> M _.
proof: Proof. rewrite bindA [in RHS]bindA -[in RHS](plus_commute (dispatch_Ret _ _ _))//. rewrite /=; case: ifPn => xp. rewrite !bindA. under eq_bind do rewrite bindretf write3LE. under [in RHS]eq_bind do rewrite bindretf -bindA. rewrite [RHS](qperm_preserves_size2 zs (fun a b => (writeList (i + (size ys + b).+1) xs >> writeList i (rcons ys x ++ a)) >> k (size (rcons ys x)) (size a) (size xs))). bind_ext => zs' /=. rewrite -writeListC; last first. by rewrite size_cat size_rcons addSn. rewrite catA writeList_cat cat_rcons. by rewrite size_cat/= -addnS. rewrite !bindA. under eq_bind do rewrite bindretf write3LE. under [in RHS]eq_bind do rewrite bindretf -bindA. rewrite -addnS -(size_rcons zs x). rewrite [RHS](qperm_preserves_size2 (rcons zs x) (fun a b => (writeList (i + (size ys + b)) xs >> writeList i (ys ++ a)) >> k (size ys) (size a) (size xs))). bind_ext => zs' /=. rewrite (_ : (_ + (_ + _)) = (i + size (ys ++ zs'))); last by rewrite size_cat. by rewrite -writeListC// catA writeList_cat. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)