proposition: Lemma eutt_interp_state_aloop {E F S I I' A A'} (RA : A -> A' -> Prop) (RI : I -> I' -> Prop) (RS : S -> S -> Prop) (h : E ~> Monads.stateT S (itree F)) (t1 : I -> itree E (I + A)) (t2 : I' -> itree E (I' + A')): (forall i i' s1 s2, RS s1 s2 -> RI i i' -> eutt (prod_rel RS (sum_rel RI RA)) (interp_state h (t1 i) s1) (interp_state h (t2 i') s2)) -> (forall i i' s1 s2, RS s1 s2 -> RI i i' -> eutt (fun a b => RS (fst a) (fst b) /\ RA (snd a) (snd b)) (interp_state h (ITree.iter t1 i) s1) (interp_state h (ITree.iter t2 i') s2)).
proof: Proof. intro Ht. einit. ecofix CIH. intros. rewrite 2 unfold_iter. rewrite 2 interp_state_bind. ebind; econstructor. - eapply Ht; auto. - intros [s1' i1'] [s2' i2'] [? []]; cbn. + rewrite 2 interp_state_tau. auto with paco. + rewrite 2 interp_state_ret. 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)