proposition: Lemma safe2E crs : safe2 crs = get >>= (fun uds => let (ok, uds') := safe1 uds crs in (put uds' >> Ret ok)).
proof: Proof. apply/esym; rewrite /safe2. set f := fun x => get >>= (fun uds => let (ok, uds') := safe1 uds x in put uds' >> Ret ok) : M _. rewrite -(@foldr_universal_ext _ _ _ _ f) //; [apply/esym|move=> cr {}crs; apply/esym]. by rewrite /start2 /f /= -bindA getputskip bindskipf. transitivity (get >>= (fun uds => let (ok, uds') := step1 cr (safe1 uds crs) in put uds'>> Ret ok) : M _); last first. by []. transitivity (get >>= (fun uds => let (b', uds'') := safe1 uds crs in let (ok, uds') := step1 cr (b', uds'') in put uds' >> Ret ok) : M _); last first. bind_ext => x. by case: safe1. transitivity (get >>= (fun uds => let (b', uds'') := safe1 uds crs in let (b, uds''') := test cr uds'' in let (ok, uds') := (b && b', uds''') in put uds' >> Ret ok) : M _); last first. bind_ext => x. case: safe1 => // h t. rewrite /step1 /=. by case: test. transitivity (get >>= (fun uds => let (b', uds'') := safe1 uds crs in let (b, uds''') := test cr uds'' in let (ok, uds') := (b && b', uds''') in (put uds'' >> put uds' >> Ret ok)) : M _); last first. bind_ext => x. case: safe1 => // h t. case: test => // a b. by rewrite putput. transitivity (get >>= (fun uds => let (b', uds'') := safe1 uds crs in put uds'' >> let (b, uds''') := test cr uds'' in let (ok, uds') := (b && b', uds''') in put uds' >> Ret ok) : M _); last first. bind_ext => x. case: safe1 => // h t. case: test => // a b. by rewrite bindA. transitivity (get >>= (fun uds => let (b', uds'') := safe1 uds crs in put uds'' >> (get >>= (fun uds4 => let (b, uds''') := test cr uds4 in let (ok, uds') := (b && b', uds''') in put uds' >> Ret ok))) : M _); last first. bind_ext => x. case: safe1 => // h t. by rewrite -bindA putgetput. transitivity (do b' <- (do uds <- get ; let (ok, uds'') := safe1 uds crs in put uds'' >> Ret ok) ; (do uds'''' <- get; let (b, uds''') := test cr uds'''' in let (ok, uds') := (b && b', uds''') in put uds' >> Ret ok) : M _)%Do; last first. rewrite bindA; bind_ext => x. case: safe1 => // h t. by rewrite bindA; under eq_bind do rewrite bindretf. by []. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib