proposition: Lemma eqit_inv_bind_vis : forall {A B C E X RR} b1 b2 (ma : itree E A) (kab : A -> itree E B) (e : E X) (kxc : X -> itree E C), eqit RR b1 b2 (ITree.bind ma kab) (Vis e kxc) -> (exists (kxa : X -> itree E A), (eqit eq b1 b2 ma (Vis e kxa)) /\ forall (x:X), eqit RR b1 b2 (ITree.bind (kxa x) kab) (kxc x)) \/ (exists (a : A), eqit eq b1 b2 ma (Ret a) /\ eqit RR b1 b2 (kab a) (Vis e kxc)).
proof: Proof. intros. punfold H. unfold eqit_ in H. cbn in *. remember (observe (ITree.bind ma kab)) as tl. remember (VisF e kxc) as tr. revert ma kab Heqtl kxc Heqtr. induction H; try discriminate. - intros. unfold observe, _observe in Heqtl; cbn in Heqtl. destruct (observe ma) eqn:Ema; try discriminate. + right. exists r. split. * pfold; red. rewrite Ema. constructor. auto. * pfold; red. unfold observe at 1; unfold _observe. rewrite <- Heqtl. constructor; auto. + left. symmetry in Heqtl. revert k2 REL Heqtr. inv_eq_VisF Heqtl. intros. inv_eq_VisF Heqtr. exists k. split. * pfold; red. rewrite Ema. constructor. red. left. apply reflexivity. * pclearbot. auto. - intros. subst. unfold observe, _observe in Heqtl; cbn in Heqtl. destruct (observe ma) eqn: Ema; try discriminate. + right; exists r; split. * rewrite itree_eta, Ema; reflexivity. * pfold. red. unfold observe at 1; unfold _observe; rewrite <- Heqtl. constructor; auto. + inv Heqtl. specialize (IHeqitF _ _ eq_refl _ eq_refl). destruct IHeqitF as [(k0 & ? & ?) | (a & ? & ?)]; [left | right]. * exists k0. split; auto. pfold; red; rewrite Ema; constructor; punfold H0. * exists a. split; auto. pfold; red; rewrite Ema; constructor; punfold H0. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)