proposition: Lemma throw_prefix_iter : forall E Err A B (body : A -> itree (exceptE Err +' E) (A + B) ) (init : A), throw_prefix (ITree.iter body init) ≅ ITree.iter (R := B + Err) (fun a : A => r <- throw_prefix (body a);; match (r : (A + B) + Err) with | inl (inl a) => Ret (inl a) | inl (inr b) => Ret (inr (inl b)) | inr e => Ret (inr (inr e)) end) init.
proof: Proof. intros E Err A B. ginit. gcofix CIH. intros. setoid_rewrite unfold_iter_ktree at 2 3. destruct (observe (body init) ) eqn : Heq; symmetry in Heq; apply simpobs in Heq. - rewrite Heq at 1. rewrite bind_ret_l. setoid_rewrite bind_bind. rewrite Heq at 1. rewrite throw_prefix_ret. rewrite bind_ret_l. destruct r0; rewrite bind_ret_l. + rewrite throw_prefix_tau. gstep. constructor. gfinal. eauto. + rewrite throw_prefix_ret. gfinal. right. pfold; constructor; auto. - rewrite Heq at 1. setoid_rewrite bind_bind. rewrite Heq at 1. rewrite throw_prefix_tau. repeat rewrite bind_tau. rewrite throw_prefix_tau. gstep. constructor. setoid_rewrite throw_prefix_bind at 1. guclo eqit_clo_bind. econstructor; try reflexivity. intros; subst. destruct u2 as [ [ a | b] | e ]. + rewrite bind_ret_l. rewrite throw_prefix_tau. gstep. constructor. gfinal. eauto. + rewrite bind_ret_l. rewrite throw_prefix_ret. gstep; constructor; auto. + rewrite bind_ret_l. gstep; constructor; auto. - rewrite Heq at 1. setoid_rewrite bind_bind. rewrite Heq at 1. destruct e. + destruct e. rewrite bind_vis. rewrite throw_prefix_exc. setoid_rewrite throw_prefix_exc. repeat rewrite bind_ret_l. gstep; constructor; auto. + rewrite bind_vis. rewrite throw_prefix_ev. setoid_rewrite throw_prefix_ev. rewrite bind_vis. setoid_rewrite bind_tau. gstep; constructor. intros. red. gstep; constructor. rewrite throw_prefix_bind. guclo eqit_clo_bind. econstructor; try reflexivity. intros; subst. destruct u2 as [ [ a | b] | e' ]. * rewrite bind_ret_l. rewrite throw_prefix_tau. gstep; constructor. gfinal. eauto. * rewrite bind_ret_l. rewrite throw_prefix_ret. gstep; constructor; auto. * rewrite bind_ret_l. gstep; constructor; auto. Qed.
imports: Coq(Morphisms) ExtLib(Structures.Monad) Paco(paco) ITree(ITree ITreeFacts Events.Exception)