proposition: Lemma throw_prefix_bind_decomp : forall E Err R (t : itree (exceptE Err +' E) R ), t ≈ ITree.bind (throw_prefix t) (fun r => match r with | inr e => v <- trigger (inl1 (Throw e));; match v : void with end | inl a => Ret a end).
proof: Proof. intros E Err R. ginit. gcofix CIH. intros. destruct (observe t) eqn : Heq; symmetry in Heq; apply simpobs in Heq. - rewrite Heq. rewrite throw_prefix_ret. rewrite bind_ret_l. gfinal. right. pfold; constructor; auto. - rewrite Heq. rewrite throw_prefix_tau. rewrite bind_tau. gstep. constructor. gfinal; left. auto. - destruct e. + rewrite Heq. destruct e. rewrite throw_prefix_exc. rewrite bind_ret_l. cbn. rewrite bind_trigger. gstep. constructor. intros []. + rewrite Heq. rewrite throw_prefix_ev. rewrite bind_vis. gstep. constructor. intros. red. rewrite tau_euttge. gfinal; left; auto. Qed.
imports: Coq(Morphisms) ExtLib(Structures.Monad) Paco(paco) ITree(ITree ITreeFacts Events.Exception)