proposition: Lemma theorem44 (xs : seq A) : foldr (opmul op) (Ret [::]) xs >>= (fun ys => guard (all ok ys) >> Ret xs) = foldr opdot (Ret [::]) xs.
proof: Proof. elim: xs => [|x xs IH]; first by rewrite /= bindretf /= guardT bindskipf. rewrite [in LHS]/=. rewrite {1}/opmul. rewrite {1}bindA. transitivity (get >>= (fun x0 => put (op x0 x) >> foldr (opmul op) (Ret [::]) xs >>= (fun ys => guard (all ok (op x0 x :: ys))) >> Ret (x :: xs)) : M _). bind_ext => st. by rewrite bind_fmap !bindA. transitivity (get >>= (fun x0 => put (op x0 x) >> foldr (opmul op) (Ret [::]) xs >>= (fun ys => guard (all ok ys) >> guard (ok (op x0 x))) >> Ret (x :: xs)) : M _). bind_ext => st. rewrite !bindA. bind_ext; case. bind_ext => ys. rewrite -guard_and. congr (guard _ >> _). by rewrite -cat1s all_cat andbC all_seq1. transitivity (get >>= (fun st => guard (ok (op st x)) >> put (op st x) >> foldr (opmul op) (Ret [::]) xs >>= (fun ys => guard (all ok ys)) >> Ret (x :: xs)) : M _). bind_ext => st. rewrite -!bindA. congr (_ >> _). rewrite !bindA. by rewrite put_foldr. transitivity (get >>= (fun st => guard (ok (op st x)) >> put (op st x) >> fmap (cons x) (foldr (opmul op) (Ret [::]) xs >>= (fun ys => guard (all ok ys)) >> Ret xs)) : M _). bind_ext => st. rewrite !bindA. bind_ext; case. bind_ext; case. rewrite !fmap_bind. bind_ext => s. rewrite fcompE fmap_bind /=. bind_ext; case. by rewrite fcompE fmapE bindretf. by rewrite [in RHS]/= -IH /opdot !bindA. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib