proposition: Lemma eqit_inv_bind_ret: forall {E X R1 R2 RR} b1 b2 (ma : itree E X) (kb : X -> itree E R1) (b: R2), @eqit E R1 R2 RR b1 b2 (ITree.bind ma kb) (Ret b) -> exists a, @eqit E X X eq b1 b2 ma (Ret a) /\ @eqit E R1 R2 RR b1 b2 (kb a) (Ret b).
proof: Proof. intros. punfold H. unfold eqit_ in *. cbn in *. remember (observe (ITree.bind ma kb)) as otl. remember (RetF b) as tr. revert ma kb Heqotl b Heqtr. induction H; try discriminate. - intros; subst. inv Heqtr. unfold observe, _observe in Heqotl; cbn in Heqotl. destruct (observe ma) eqn:Ema; try discriminate. exists r. split. * rewrite itree_eta, Ema. reflexivity. * rewrite itree_eta_. unfold _observe. rewrite <- Heqotl. pfold; constructor; auto. - intros. subst. unfold observe, _observe in Heqotl; cbn in Heqotl. destruct (observe ma) eqn:Ema; try discriminate. + exists r. split. * rewrite itree_eta, Ema. reflexivity. * pfold. red. unfold observe at 1; unfold _observe. rewrite <- Heqotl. constructor; auto. + inv Heqotl. specialize (IHeqitF _ _ eq_refl _ eq_refl). destruct IHeqitF as (a & ? & ?); exists a. split; auto. pfold; red; rewrite Ema. constructor; auto. 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)