proposition: Lemma try_catch_to_throw_prefix : forall E Err R (ttry : itree (exceptE Err +' E) R ) (kcatch : Err -> itree (exceptE Err +' E) R), try_catch ttry kcatch ≈ ITree.bind (throw_prefix ttry) (fun r => match r with | inr e => kcatch e | inl a => Ret a end).
proof: Proof. intros. revert ttry. ginit. gcofix CIH. intros. destruct (observe ttry) eqn : Heq; symmetry in Heq; apply simpobs in Heq. - rewrite Heq. rewrite try_catch_ret. rewrite throw_prefix_ret. rewrite bind_ret_l. gfinal. right. pfold; constructor; auto. - rewrite Heq. rewrite try_catch_tau. rewrite throw_prefix_tau. rewrite bind_tau. gstep. constructor. gfinal; left; auto. - destruct e. + destruct e. rewrite Heq. rewrite try_catch_exc. rewrite throw_prefix_exc. rewrite bind_ret_l. gfinal; right. apply paco2_mon with (r := bot2); intros; try contradiction. enough (kcatch e ≈ kcatch e); auto. reflexivity. + rewrite Heq. rewrite try_catch_ev. rewrite throw_prefix_ev. rewrite bind_vis. setoid_rewrite tau_euttge. gstep. constructor. intros. gfinal. left. auto. Qed.
imports: Coq(Morphisms) ExtLib(Structures.Monad) Paco(paco) ITree(ITree ITreeFacts Events.Exception)