proposition: Lemma Leaf_interp_state_iter_inv {E F S R I}: forall (h: E ~> Monads.stateT S (itree F)) (body: I -> itree E (I + R)) (RS: S -> Prop) (RI: I -> Prop) (RR: R -> Prop) (s: S) (i: I), (forall s i, RS s -> RI i -> (forall sx', sx' ∈ interp_state h (body i) s -> prod_pred RS (sum_pred RI RR) sx')) -> RS s -> RI i -> forall sr', sr' ∈ interp_state h (ITree.iter body i) s -> prod_pred RS RR sr'.
proof: Proof. setoid_rewrite <- has_post_Leaf_equiv. setoid_rewrite has_post_post_strong. intros * Hinv Hentrys Hentryi. set (eRI := fun (i1 i2: I) => i1 = i2 /\ RI i1). set (eRR := fun (r1 r2: R) => r1 = r2 /\ RR r1). set (eRS := fun (s1 s2: S) => s1 = s2 /\ RS s1). set (R1 := (fun x y : S * R => x = y /\ prod_pred RS RR x)). set (R2 := (fun a b : S * R => eRS (fst a) (fst b) /\ eRR (snd a) (snd b))). assert (HR1R2: eq_rel R1 R2) by (compute; intuition; subst; now try destruct y). unfold has_post_strong; fold R1; rewrite (eutt_equiv _ _ HR1R2). unshelve eapply (eutt_interp_state_iter eRI eRR eRS h body body _ i i s s _ _); [| subst eRS; intuition | subst eRI; intuition]. intros i1 ? s1 ? [<- Hs1] [<- Hi1]. set (R3 := (fun x y : S * (I + R) => x = y /\ prod_pred RS (sum_pred RI RR) x)). set (R4 := (prod_rel eRS (sum_rel eRI eRR))). assert (HR3R4: eq_rel R3 R4). { split; intros [? [|]] [? [|]]; compute. 1-4: intros [[]]; dintuition; cbn; intuition. all: intros [[[=->] ?] HZ]; inversion HZ; intuition now subst. } rewrite <- (eutt_equiv _ _ HR3R4). now apply Hinv. Qed.
imports: ITree(Basics.Utils Basics.HeterogeneousRelations ITree Eq.Shallow Eq.Eqit Interp.InterpFacts Events.State Events.StateFacts Props.HasPost) Paco(paco) Coq(Morphisms Basics Program.Equality)