proposition: Lemma put_foldr st x xs : put (op st x) >> (do x1 <- foldr (opmul op) (Ret [::]) xs; guard (all ok x1) >> guard (ok (op st x)))%Do = guard (ok (op st x)) >> (put (op st x) >> (do ys <- foldr (opmul op) (Ret [::]) xs; guard (all ok ys))%Do) :> M _.
proof: Proof. elim: xs x => [x|h t _ x]. rewrite /= bindretf /= guardT /= bindskipf /= bindretf. rewrite (_ : guard (_ _ [::]) = skip) //= ?guardT //. rewrite bindmskip; case: guardPn => H. - by rewrite bindskipf bindmskip. - by rewrite bindmfail bindfailf. rewrite /= !bindA. transitivity (put (op st x) >> (do x0 <- get; do x1 <- let st' := op x0 h in fmap (cons st') (put st' >> foldr (opmul op) (Ret [::]) t); guard (ok (op st x)) >> guard (all ok x1))%Do : M _). bind_ext; case. bind_ext => st'. bind_ext => s. by rewrite -guard_and andbC guard_and. rewrite guardsC; last exact: bindmfail. rewrite !bindA. bind_ext; case. bind_ext => st'. rewrite !bindA. bind_ext => s. rewrite guardsC //; exact: bindmfail. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib