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