proposition: Lemma iqsort_slowsort i xs : writeList i xs >> iqsort (M := M) (i, size xs) `<=` slowsort xs >>= writeList i.
proof: Proof. have [n nxs] := ubnP (size xs); elim: n xs i => // n ih xs i in nxs *. move: xs => [|p xs] in nxs *. by rewrite /= iqsort_nil slowsort_nil 2!bindretf /=; exact: refin_refl. pose p1 : M unit := qperm_partl p [::] [::] xs >>= (fun '(ys, zs) => writeList (i + (size ys).+1) zs >> qperm ys >>= (fun ys' => writeList i (rcons ys' p) >> iqsort (i, size ys) >> iqsort (i + (size ys).+1, size zs))). apply: (@refin_trans _ _ p1). - apply: (@refin_trans _ _ (qperm_partl p [::] [::] xs >>= (fun '(ys, zs) => writeList (i + (size ys).+1) zs >> (writeList i (p :: ys) >> aswap i (i + size ys)) >> (iqsort (i, size ys)) >> iqsort (i + (size ys).+1, size zs)))). + rewrite [X in _ `<=` X](_ : _ = qperm_partl p [::] [::] xs >>= (fun '(ys, zs) => aput i p >> writeList i.+1 (ys ++ zs) >> (aswap i (i + size ys)) >> (iqsort (i, size ys)) >> iqsort (i + (size ys).+1, size zs))); last first. bind_ext => -[ys zs]. rewrite -bindA -writeListC//. by rewrite /= bindA writeList_cat !bindA -addSnnS. rewrite [X in _ `<=` X](_ : _ = aput i p >> qperm_partl p [::] [::] xs >>= (fun '(ys, zs) => (writeList i.+1 (ys ++ zs) >> aswap i (i + size ys) >> iqsort (i, size ys) >> iqsort (i + (size ys).+1, size zs)))); last first. rewrite [RHS]bindA. rewrite -(plus_commute (qperm_partl p [::] [::] xs))//. by bind_ext=> -[a b]; rewrite !bindA. rewrite {nxs}. rewrite [X in _ `<=` X](_ : _ = aput i p >> qperm_partl p [::] [::] xs >>= (fun '(ys, zs) => write2L i.+1 (ys, zs)) >>= (fun '(ny, nz) => aswap i (i + ny) >> iqsort (i, ny) >> iqsort (i + ny.+1, nz))); last first. by rewrite [in RHS]bindA; bind_ext => -[a b]; rewrite write2LE !bindA. rewrite [in X in _ `<=` X](bindA (aput i p)). apply: refin_trans; last first. by rewrite bindA; apply: refin_bindl => ttt; exact/refin_bindr/refin_ipartl. rewrite -[in X in _ `<=` X]bindA. rewrite (_ : aput i p >> _ = (writeList i (p :: xs) >> Ret p) >>= (fun p => ipartl p i.+1 0 0 (size xs))); last first. by rewrite /= bindA -[in LHS](bindA (aput i p)) [in RHS]bindA !bindretf. rewrite writeListRet 2![in X in _ `<=` X]bindA. apply: refin_bindl => -[]. rewrite /= iqsort_cons. rewrite bindA; apply: refin_bindl => x. rewrite ipartlE /= fmapE [in X in _ `<=` X]bindA. under [in X in _ `<=` X]eq_bind do rewrite bindretf. exact: refin_refl. + apply: refin_bindl => -[ys sz]. rewrite 4!bindA. apply: refin_bindl => -[]. rewrite -2![in X in _ `<=` X]bindA. rewrite [in X in _ `<=` X](bindA _ (fun _ => iqsort _) (fun _ => iqsort _)). rewrite -2![in X in X `<=` _]bindA. rewrite [in X in X `<=` _](bindA _ (fun _ => iqsort _) (fun _ => iqsort _)). apply: refin_bindr. exact: refin_writeList_cons_aswap. - apply: refin_trans; last exact/refin_bindr/refin_partition_slowsort. rewrite bindretf. move pxs : (partition p xs) => tmp; case: tmp => [ys zs] in pxs *. rewrite -qperm_slowsort 2!kleisliE !bindA. rewrite [X in _ `<=` X](_ : _ = (do zs' <- qperm zs; do ys' <- qperm ys; do ys'' <- slowsort ys'; do zs'' <- slowsort zs'; writeList i (ys'' ++ p :: zs''))%Do); last first. rewrite (plus_commute (qperm zs))//. bind_ext => ys'. rewrite !bindA; under eq_bind do rewrite !bindA. rewrite -(plus_commute (qperm zs))//. bind_ext => zs'; bind_ext => ys''. by rewrite bindA; under eq_bind do rewrite bindretf. apply: refin_trans; first exact/refin_bindr/refin_qperm_partl. rewrite -partition_partl pxs bindA /=. under eq_bind do rewrite bindretf. rewrite bind_qperm_guard [in X in _ `<=` X]bind_qperm_guard . apply: refin_bindl => zs'. apply: refin_bind_guard => /eqP zszs'. rewrite ![in X in X `<=` _]bindA. rewrite -(plus_commute (qperm ys))//. rewrite (qperm_preserves_size2 ys (fun a b => (writeList (i + b.+1) zs' >> (writeList i (rcons a p) >> iqsort (i, b) >> iqsort (i + b.+1, size zs'))))). rewrite bind_qperm_guard [in X in _ `<=` X]bind_qperm_guard . apply: refin_bindl => ys'. apply: refin_bind_guard => /eqP ysys'. rewrite -cats1 writeList_cat writeListC//. rewrite (bindA _ _ (fun _ => iqsort (i, size ys'))). apply: (@refin_trans _ _ ( (writeList (i + (size ys').+1) zs' >> (writeList (i + size ys') [:: p] >> (slowsort ys' >>= writeList i))) >> iqsort (i + (size ys').+1, size zs'))). rewrite !bindA. do 2 apply: refin_bindl => -[]. rewrite 2!bindretf -2!bindA; apply/refin_bindr/ih. move: nxs; rewrite /= ltnS; apply: leq_ltn_trans. by rewrite -ysys' -(size_partition p xs) pxs /= leq_addr. rewrite -[in X in X `<=` _](plus_commute (slowsort ys'))//. rewrite !bindA. rewrite -[in X in X `<=` _](plus_commute (slowsort ys'))//. rewrite (slowsort_preserves_size2 _ (fun a b => writeList (i + b.+1) zs' >> (writeList (i + b) [:: p] >> writeList i a >> iqsort (i + b.+1, size zs')))). rewrite bind_slowsort_guard [in X in _ `<=` X]bind_slowsort_guard. apply: refin_bindl => ys''. apply: refin_bind_guard => /eqP ys'ys''. rewrite -bindA -(writeListC _ _ ys'')//. under [in X in _ `<=` X]eq_bind do rewrite -cat_rcons. under [in X in _ `<=` X]eq_bind do rewrite writeList_cat. rewrite (plus_commute (slowsort zs'))//. rewrite -(writeList_cat i ys'' [:: p]) -(writeListC _ _ _ zs'); last first. by rewrite /= cats1 size_rcons/=. rewrite cats1 bindA; apply: refin_bindl => -[]. rewrite size_rcons; apply: ih. move: nxs; rewrite /= ltnS; apply: leq_ltn_trans. by rewrite -zszs' -(size_partition p xs) pxs /= leq_addl. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)