proposition: Lemma eqit_trans {E R1 R2 R3} (RR1: R1->R2->Prop) (RR2: R2->R3->Prop) b1 b2 t1 t2 t3 (INL: eqit RR1 b1 b2 t1 t2) (INR: eqit RR2 b1 b2 t2 t3): @eqit E _ _ (rcompose RR1 RR2) b1 b2 t1 t3.
proof: Proof. revert_until b2. pcofix CIH. intros. pstep. punfold INL. punfold INR. red in INL, INR |- *. genobs_clear t3 ot3. hinduction INL before CIH; intros; subst; clear t1 t2. - remember (RetF r2) as ot. hinduction INR before CIH; intros; inv Heqot; eauto with paco itree. - assert (DEC: (exists m3, ot3 = TauF m3) \/ (forall m3, ot3 <> TauF m3)). { destruct ot3; eauto; right; red; intros; inv H. } destruct DEC as [EQ | EQ]. + destruct EQ as [m3 ?]; subst. econstructor. right. pclearbot. eapply CIH; eauto with paco. eapply eqit_inv_Tau. eauto with itree. + inv INR; try (exfalso; eapply EQ; eauto; fail). econstructor; eauto. pclearbot. punfold REL. red in REL. hinduction REL0 before CIH; intros; try (exfalso; eapply EQ; eauto; fail). * remember (RetF r1) as ot. hinduction REL0 before CIH; intros; inv Heqot; eauto with paco itree. * remember (VisF e k1) as ot. hinduction REL0 before CIH; intros; try discriminate; [ inv_Vis | eauto with itree ]. econstructor. intros. right. destruct (REL v), (REL0 v); try contradiction. eauto. * eapply IHREL0; eauto. pstep_reverse. destruct b1; inv CHECK0. apply eqit_inv_Tau_r. eauto with itree. - remember (VisF e k2) as ot. hinduction INR before CIH; intros; try discriminate; [ inv_Vis | eauto with itree ]. econstructor. intros. destruct (REL v), (REL0 v); try contradiction; eauto with itree. - eauto with itree. - remember (TauF t0) as ot. hinduction INR before CIH; intros; try inversion Heqot; subst. 2,3: eauto 3 with itree. eapply IHINL. pclearbot. punfold REL. eauto with itree. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)