proposition: Lemma eqit_inv_bind_tau: forall {E A B C RR} b1 b2 (ma : itree E A) (kab : A -> itree E B) (tc: itree E C), eqit RR b1 b2 (ITree.bind ma kab) (Tau tc) -> (exists (ma' : itree E A), eqit eq b1 b2 ma (Tau ma') /\ eqit RR b1 b2 (ITree.bind ma' kab) tc) \/ (exists (a : A), eqit eq b1 b2 ma (Ret a) /\ eqit RR b1 b2 (kab a) (Tau tc)).
proof: Proof. intros. punfold H. unfold eqit_ in H. cbn in H. remember (observe (ITree.bind ma kab)) as tl. remember (TauF tc) as tr. revert ma kab Heqtl Heqtr. induction H; try discriminate; intros. - inv Heqtr. 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; exists t; split. * pfold; red; rewrite Ema; constructor; left; apply reflexivity. * inv Heqtl. pclearbot. assumption. - subst. 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 4; auto. + inv Heqtl. specialize (IHeqitF _ _ eq_refl eq_refl). destruct IHeqitF as [(t0 & ? & ?) | (a & ? & ?)]; [left | right]. * exists t0. split; auto. pfold; red; rewrite Ema; constructor 4; punfold H0. * exists a. split; auto. pfold; red; rewrite Ema; constructor; punfold H0. - inv Heqtr. left; exists ma; split. + pfold; constructor; auto. apply Reflexive_eqitF_eq. intros ?; left; apply reflexivity. + pfold; assumption. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)