proposition: Lemma nondetState_commute S (M : nondetStateMonad S) A (m : M A) B (n : M B) C (f : A -> B -> M C) : nondetState_isNondet m -> commute m n f.
proof: Proof. case => x. elim: x m n f => [{}A a m n f <-| B0 {}A n0 H0 n1 H1 m n2 f <- | A0 m n f <- | A0 n0 H0 n1 H1 m n2 f <-]. - rewrite /commute bindretf. by under [RHS]eq_bind do rewrite bindretf. - rewrite /commute /= !bindA. transitivity (do x <- nondetSem n0; do y <- n2; nondetSem (n1 x) >>= f^~ y)%Do. bind_ext => s. by rewrite (H1 s). rewrite H0 //. bind_ext => b. by rewrite bindA. - rewrite /commute /= bindfailf. transitivity (n >> fail : M C); first by rewrite bindmfail. bind_ext => b. by rewrite bindfailf. - rewrite /commute /= alt_bindDl. transitivity (do y <- n2; nondetSem n0 >>= f^~ y [~] nondetSem n1 >>= f^~ y)%Do; last first. bind_ext => a. by rewrite alt_bindDl. by rewrite alt_bindDr H0 // H1. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib