proposition: Lemma interp_state_bind {E F : Type -> Type} {A B S : Type} (f : forall T, E T -> S -> itree F (S * T)%type) (t : itree E A) (k : A -> itree E B) (s : S) : (interp_state f (t >>= k) s) ≅ (interp_state f t s >>= fun st => interp_state f (k (snd st)) (fst st)).
proof: Proof. revert t k s. ginit. pcofix CIH. intros t k s. rewrite unfold_bind. rewrite (unfold_interp_state f t). destruct (observe t). - cbn. rewrite !bind_ret_l. cbn. apply reflexivity. - cbn. rewrite !bind_tau, interp_state_tau. gstep. econstructor. gbase. apply CIH. - cbn. rewrite interp_state_vis, bind_bind. guclo eqit_clo_bind. econstructor. + reflexivity. + intros u2 ? []. rewrite bind_tau. gstep; constructor. ITree.fold_subst. auto with paco. Qed.
imports: Coq(Program.Tactics Morphisms) Paco(paco) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.HeterogeneousRelations Basics.Monad Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Interp.Interp Interp.InterpFacts Interp.RecursionFacts Events.State)