proposition: Lemma throw_prefix_bind : forall E Err R S (t : itree (exceptE Err +' E) R ) (k : R -> itree (exceptE Err +' E) S), throw_prefix (ITree.bind t k) ≅ ITree.bind (throw_prefix t) (fun r : R + Err => match r with | inl r' => throw_prefix (k r') | inr e => Ret (inr e) end ).
proof: Proof. intros. revert t. ginit. gcofix CIH. intros. destruct (observe t) eqn : Heq; symmetry in Heq; apply simpobs in Heq. - rewrite Heq. rewrite throw_prefix_ret. repeat rewrite bind_ret_l. gfinal; right. apply paco2_mon with (r := bot2); intros; try contradiction. enough (throw_prefix (k r0) ≅ throw_prefix (k r0)); auto; try reflexivity. - rewrite Heq. rewrite throw_prefix_tau. repeat rewrite bind_tau. rewrite throw_prefix_tau. gstep. constructor. gfinal; eauto. - destruct e. + destruct e. rewrite Heq. rewrite throw_prefix_exc. rewrite bind_vis. rewrite throw_prefix_exc. rewrite bind_ret_l. gstep; constructor; auto. + rewrite Heq. rewrite throw_prefix_ev. repeat rewrite bind_vis. rewrite throw_prefix_ev. gstep. constructor. intros. red. rewrite bind_tau. gstep. constructor. gfinal. eauto. Qed.
imports: Coq(Morphisms) ExtLib(Structures.Monad) Paco(paco) ITree(ITree ITreeFacts Events.Exception)