proposition: Lemma scanlM_of_scanl s xs : Ret (scanl op s xs) = protect (scanlM s xs).
proof: Proof. elim: xs s => [/=|x xs IH] s. by rewrite scanlM_nil protect_put_ret. rewrite /scanlM [in RHS]/=. set mul := fun (a : A) m => _. under [RHS]eq_bind do rewrite -!bindA. transitivity (do y <- get; (put s >> get) >>= fun z => do a <- fmap (cons (op z x)) (put (op z x) >> foldr mul (Ret [::]) xs); put y >> Ret a)%Do; last first. by under [LHS]eq_bind do rewrite -!bindA. under eq_bind do rewrite putget bindA bindretf. rewrite scanlM_of_scanl_helper. transitivity (fmap (cons (op s x)) (do y <- get; put (op s x) >> (do a <- foldr mul (Ret [::]) xs; put y >> Ret a)))%Do; last first. by congr (fmap _ _); under [RHS]eq_bind do rewrite putput. transitivity (fmap (cons (op s x)) (protect (scanlM (op s x) xs))); last first. by congr (fmap _ _); under eq_bind do rewrite -bindA. by rewrite -IH fmapE bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib