proposition: Lemma eutt_interp_state_loop {E F S A B C} (RS : S -> S -> Prop) (h : E ~> Monads.stateT S (itree F)) (t1 t2 : C + A -> itree E (C + B)) : (forall ca s1 s2, RS s1 s2 -> eutt (fun a b => RS (fst a) (fst b) /\ snd a = snd b) (interp_state h (t1 ca) s1) (interp_state h (t2 ca) s2)) -> (forall a s1 s2, RS s1 s2 -> eutt (fun a b => RS (fst a) (fst b) /\ snd a = snd b) (interp_state h (loop (C := ktree E) t1 a) s1) (interp_state h (loop (C := ktree E) t2 a) s2)).
proof: Proof. intros. unfold loop, bimap, Bimap_Coproduct, case_, Case_Kleisli, Function.case_sum, id_, Id_Kleisli, cat, Cat_Kleisli, inr_, Inr_Kleisli, inl_, Inl_Kleisli, lift_ktree_; cbn. rewrite 2 bind_ret_l. eapply (eutt_interp_state_iter eq eq); auto; intros. rewrite 2 interp_state_bind. subst. eapply eutt_clo_bind; eauto. intros. cbn in H2; destruct (snd u1); rewrite <- (proj2 H2). - rewrite bind_ret_l, 2 interp_state_ret. pstep. constructor. split; cbn; auto using (proj1 H2). - rewrite bind_ret_l, 2 interp_state_ret. pstep. constructor. split; cbn; auto using (proj1 H2). 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)