proposition: Theorem interleaved_mrec : forall t1 t2, interleaved t1 t2 -> Recursion.interp_mrec (cat f (case_ g inr_)) t1 ≈ Recursion.interp_mrec (cat g (case_ f inr_)) t2.
proof: Proof. einit; ecofix CIH; intros. induction H0. - rewrite 2 unfold_interp_mrec; cbn. estep. - rewrite (itree_eta t); destruct (observe t). + rewrite interp_ret, 2 bind_ret_l. auto. + rewrite interp_tau, 2 bind_tau, 2 unfold_interp_mrec; cbn. estep. + rewrite interp_vis, bind_vis. rewrite bind_bind. rewrite (unfold_interp_mrec _ _ (Vis _ _)); cbn. destruct e; cbn. setoid_rewrite (tau_euttge (interp _ _)). * unfold cat at 3, Cat_Handler at 3, Handler.cat. change (g X b) with (Tau (g0 X b)). rewrite bind_tau, unfold_interp_mrec; cbn. etau. rewrite tau_euttge. ebase. * unfold inr_, Inr_sum1_Handler, Handler.inr_, Handler.htrigger. rewrite bind_trigger. rewrite unfold_interp_mrec; cbn. evis; intros; etau. rewrite tau_euttge. ebase. - rewrite (itree_eta t); destruct (observe t). + rewrite interp_ret, 2 bind_ret_l. auto. + rewrite interp_tau, 2 bind_tau, 2 unfold_interp_mrec; cbn. estep. + rewrite interp_vis, bind_vis. rewrite bind_bind. rewrite (unfold_interp_mrec _ _ (Vis _ _)); cbn. destruct e; cbn. setoid_rewrite (tau_euttge (interp _ _)). * unfold cat at 2, Cat_Handler at 2, Handler.cat. change (f X a) with (Tau (f0 X a)). rewrite !bind_tau, (unfold_interp_mrec _ _ (Tau _)); cbn. etau. rewrite tau_euttge. ebase. * unfold inr_, Inr_sum1_Handler, Handler.inr_, Handler.htrigger. rewrite bind_trigger. rewrite unfold_interp_mrec; cbn. evis; intros; etau. rewrite tau_euttge. ebase. Qed.
imports: Coq(Setoid Morphisms RelationClasses) Paco(paco) ITree(Basics.Basics Basics.Category Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Indexed.Sum Interp.Interp Interp.Handler Interp.TranslateFacts Interp.InterpFacts Interp.RecursionFacts)