proposition: Lemma safe3E crs : safe3 crs = foldr (@step3 unit) skip crs :> M _.
proof: Proof. transitivity (((fun x => x >>= (guard : _ -> M _)) \o (foldr step2 start2)) crs). by []. apply foldr_fusion_ext => [|cr {crs}k]. by rewrite /= /safe3 /= /start2 /= bindretf guardT. transitivity ((do b' <- k ; do uds <- get ; let (b, uds') := test cr uds in put uds' >> Ret (b && b')) >>= guard). by rewrite /step2. transitivity (do b' <- k ; do uds <- get ; let (b, uds') := test cr uds in put uds' >> guard (b && b')). rewrite bindA; bind_ext => x. rewrite bindA; bind_ext => y. case: (test cr y) => a b. by rewrite bindA bindretf. transitivity (do b' <- k ; do uds <- get ; let (b, uds') := test cr uds in put uds' >> guard b >> guard b'). bind_ext => x. bind_ext => y. case: (test cr y) => a b. by rewrite bindA guard_and. transitivity (do b' <- k ; guard b' >> (do uds <- get ; let (b, uds') := test cr uds in put uds' >> guard b)). bind_ext => b'. rewrite guardsC; last exact: bindmfail. rewrite bindA. bind_ext => x. case: test => h t. rewrite 2!bindA. bind_ext; case. rewrite -guard_and andbC guard_and guardsC //. exact: bindmfail. transitivity ((k >>= guard) >> do uds <- get ; let (b, uds') := test cr uds in put uds' >> guard b). by rewrite bindA. by []. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib