proposition: Lemma to_hoare_pre_bind_assoc `{MayProvide ix i} `(c : contract i Ω) `(p : impure ix a) `(Hp : pre (to_hoare c p) ω) `(f : a -> impure ix b) (run : forall (x : a) (ω' : Ω), post (to_hoare c p) ω x ω' -> pre (to_hoare c (f x)) ω') : pre (to_hoare c (p >>= f)) ω.
proof: Proof. revert ω Hp run. induction p; intros ω Hp run. + now apply run. + cbn in Hp. destruct Hp as [He Hn]. change (request_then e f0 >>= f) with (request_then e (fun x => f0 x >>= f)). split. ++ exact He. ++ intros x ω' Hpost. specialize Hn with x ω'. destruct Hpost. rewrite H2 in *. assert (Hpre : pre (to_hoare c (f0 x)) (gen_witness_update c ω e x)) by now apply Hn. apply H0; [ apply Hpre |]. intros y ω'' Hpost. apply run. cbn. exists x. exists ω'. split; [split |]. +++ exact H1. +++ exact H2. +++ rewrite H2. exact Hpost. Qed.
imports: FreeSpec.Core(Interface ImpureFacts Contract)