proposition: Lemma rutt_cong_eutt {E1 E2 R1 R2}: forall REv RAns RR (t1: itree E1 R1) t1' (t2: itree E2 R2), rutt REv RAns RR t1 t2 -> t1 ≈ t1' -> rutt REv RAns RR t1' t2.
proof: Proof. intros * Hrutt Heutt; revert t1 t1' Heutt t2 Hrutt. ginit; gcofix CIH; intros t1 t1' Heutt t2 Hrutt. punfold Hrutt; red in Hrutt. rewrite (itree_eta t1) in Heutt. rewrite (itree_eta t2). move Hrutt before CIH; revert_until Hrutt. induction Hrutt as [r1 r2|m1 m2| |m1 ot2|]; clear t1 t2; intros t1' Heutt. * apply eutt_inv_Ret_l in Heutt. rewrite Heutt. gfinal; right; pstep. now apply EqRet. * punfold Heutt; red in Heutt; cbn in Heutt. rewrite itree_eta. pclearbot. fold_ruttF H. remember (TauF m1) as ot1; revert m1 m2 H Heqot1. induction Heutt as [|m1_bis m1'| |m1_bis ot1' _|t1_bis m1']; intros * Hrutt Heqot1; clear t1'; try discriminate. + inv Heqot1. pclearbot. gfinal; right; pstep; red. apply EqTau. right. now apply (CIH m1). + inv Heqot1. rewrite (itree_eta m1) in Hrutt. desobs m1 Hm1; clear m1 Hm1. { fold_eqitF Heutt. apply eutt_inv_Ret_l in Heutt. rewrite Heutt, tau_euttge. gfinal; right. eapply paco2_mon_bot; eauto. } { apply rutt_inv_Tau_l in Hrutt. eapply IHHeutt; eauto. } { clear IHHeutt. remember (VisF e k) as m1; revert Heqm1. induction Heutt as [| |U1 e1 k1 k1' Hk1k1'| |]; intros; try discriminate. - symmetry in Heqm1; dependent destruction Heqm1. rewrite tau_euttge, (itree_eta m2). punfold Hrutt; red in Hrutt; cbn in Hrutt. remember (VisF e1 k1) as m1; revert Heqm1. induction Hrutt; intros; try discriminate. * dependent destruction Heqm1. gfinal; right. pstep; red; cbn. apply EqVis; auto. intros v1 v2 HAns. specialize (H0 v1 v2 HAns). hnf in H0; hnf. pclearbot; right. apply (CIH (k1 v1)); auto. apply Hk1k1'. * idtac. rewrite tau_euttge, (itree_eta t2). now apply IHHrutt. - idtac. rewrite tau_euttge, itree_eta; now apply IHHeutt. } + inv Heqot1. gfinal; right. pstep; red. apply EqTau. right. fold_eqitF Heutt. rewrite tau_euttge in Heutt. now apply (CIH m1). * rewrite itree_eta. gfinal; right; pstep. rename H0 into HAns. punfold Heutt; red in Heutt; cbn in Heutt. remember (VisF e1 k1) as m1; revert Heqm1. induction Heutt; intros; try discriminate. + dependent destruction Heqm1. apply EqVis; auto. intros a b HAns'. specialize (HAns a b HAns'). hnf in HAns; hnf. pclearbot; right. apply (CIH (k1 a)); auto. apply REL. + now apply EqTauL, IHHeutt. * apply IHHrutt. rewrite <- itree_eta. now rewrite <- tau_eutt. * rewrite tau_euttge. rewrite (itree_eta t0). now apply IHHrutt. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(ITree ITreeFacts Core.Subevent Basics.HeterogeneousRelations Eq.Rutt Props.Leaf)