proposition: Lemma bind_iter {E A B C} (f : A -> itree E (A + B)) (g : B -> itree E (B + C)) : forall x, (ITree.bind (ITree.iter f x) (ITree.iter g)) ≈ ITree.iter (fun ab => match ab with | inl a => ITree.map inl (f a) | inr b => ITree.map (bimap inr (id_ _)) (g b) end) (inl x).
proof: Proof. einit. ecofix CIH. intros. rewrite !unfold_iter. rewrite bind_map, bind_bind. ebind; econstructor; try reflexivity. intros [a | b] _ []. - rewrite bind_tau. etau. - rewrite bind_ret_l, tau_euttge. revert b. ecofix CIH'. intros. rewrite !unfold_iter. rewrite bind_map. ebind; econstructor; try reflexivity. intros [b' | c] _ []; cbn. + etau. + reflexivity. Qed.
imports: Coq(Classes.Morphisms Setoids.Setoid Relations.Relations) Paco(paco) ITree(Basics.Basics Basics.CategoryOps Basics.CategoryTheory Basics.CategoryKleisli Basics.CategoryKleisliFacts Basics.Function Basics.HeterogeneousRelations Core.ITreeDefinition Core.ITreeMonad Core.KTree Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2)