proposition: Lemma dlabelsC t u (m : _ -> _ -> M (seq Symbol * seq Symbol)%type) : dlabels t >>= (fun x => relabel u >>= fun x0 => m x0 x) = relabel u >>= (fun x0 => dlabels t >>= fun x => m x0 x).
proof: Proof. elim: t u m => [a u /= m|t1 H1 t2 H2 u m]. rewrite /dlabels /= bindretf. by under [in RHS]eq_bind do rewrite bindretf. rewrite (_ : dlabels _ = drBin (dlabels t1, dlabels t2)) //. rewrite [in RHS]/drBin [in RHS]/bassert 2!compE ![in RHS]bindA. transitivity (do x0 <- relabel u; (do x <- dlabels t1; do x <- (do x1 <- (do y <- dlabels t2; Ret (x, y)); (do x <- assert q x1; (Ret \o ucat) x)); m x0 x))%Do; last first. bind_ext => u'; rewrite bind_fmap bindA; bind_ext => sS. rewrite 4!bindA; bind_ext => x; rewrite 2!bindretf !bindA. by under eq_bind do rewrite bindretf. rewrite -H1. rewrite [in LHS]/drBin bind_fmap [in LHS]/bassert /= ![in LHS]bindA. bind_ext => s. rewrite !bindA. transitivity (do x0 <- relabel u; (do x <- dlabels t2; (do x <- (do x1 <- Ret (s, x); (do x3 <- assert q x1; Ret (ucat x3))); m x0 x)))%Do; last by bind_ext => y2; rewrite bindA. rewrite -H2. bind_ext => s'. rewrite !bindretf. rewrite assertE. rewrite bindA. transitivity (guard (q (s, s')) >> (do x1 <- (Ret \o ucat) (s, s'); relabel u >>= (m^~ x1)))%Do. bind_ext; case; by rewrite 2!bindretf. rewrite guardsC; last exact: failfresh_bindmfail. rewrite !bindA !bindretf !bindA. bind_ext => u'. rewrite bindA guardsC; last exact: failfresh_bindmfail. by rewrite bindA bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib