proposition: Lemma iter_dinatural_ktree {E A B C} (f : ktree E A (C + B)) (g : ktree E C (A + B)) (a0 : A) : iter (C := ktree E) (fun a => ITree.bind (f a) (fun cb => match cb with | inl c => Tau (g c) | inr b => Ret (inr b) end)) a0 ≅ ITree.bind (f a0) (fun cb => match cb with | inl c0 => Tau (iter (C := ktree E) (fun c => ITree.bind (g c) (fun ab => match ab with | inl a => Tau (f a) | inr b => Ret (inr b) end)) c0) | inr b => Ret b end).
proof: Proof. revert f g a0. ginit. pcofix CIH. intros. rewrite unfold_iter_ktree. rewrite bind_bind. guclo eqit_clo_bind. econstructor. try reflexivity. intros [] ? []. { rewrite bind_tau. rewrite unfold_iter_ktree. gstep; econstructor. rewrite bind_bind. guclo eqit_clo_bind; econstructor; try reflexivity. intros [] ? []. * rewrite bind_tau. gstep; constructor. eauto with paco. * rewrite bind_ret_l. gstep; econstructor; auto. } { rewrite bind_ret_l. gstep; constructor; auto. } 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)