proposition: Lemma transL_closed vclo r (MON: monotone2 vclo) (COMP: wcompatible2 (eqit_ RR true true vclo) (transD RR)) (CLOV: forall r (CLOL: transL r <2= r), transL (vclo r) <2= vclo r) (CLOL: transL r <2= r) (CLOD: transD RR r <2= r): transL (gupaco2 (eqit_ RR true true vclo) (transD RR) r) <2= gupaco2 (eqit_ RR true true vclo) (transD RR) r.
proof: Proof. pcofix CIH. intros t1 t2 []. apply gpaco2_dist in EQR; eauto with paco. destruct EQR; cycle 1. { gbase. apply rclo_transD in H. destruct H. eauto 6 with itree. } assert (REL: paco2 (eqit_ RR true true vclo) r t' t2). { eapply paco2_mon; eauto. intros. apply rclo_transD in PR. apply CLOD. eapply transD_mon; eauto. intros. destruct PR0; eauto. } clear H. punfold EQL. red in EQL. punfold REL. red in REL. genobs t1 ot1. genobs t' ot'. hinduction EQL before CIH; intros; subst. - remember (RetF r2) as ot. genobs t2 ot2. hinduction REL0 before CIH; intros; subst; try inv Heqot. + gstep. red. simpobs. eauto with itree. + gclo. econstructor; auto_ctrans_eq. * rewrite (simpobs Heqot1). reflexivity. * rewrite (simpobs Heqot2), tau_euttge. reflexivity. - pclearbot. apply eqit_Tau_r in REL. rewrite Heqot' in REL, REL0. clear m2 Heqot'. genobs t' ot'. genobs t2 ot2. hinduction REL0 before CIH; intros; subst. + apply eqit_ret_gen in REL0. gclo. econstructor. * eapply eqit_trans; [rewrite (simpobs Heqot1); reflexivity|]. eapply eqit_trans; [rewrite tau_euttge; reflexivity|]. eauto. * rewrite (simpobs Heqot2). reflexivity. * gstep. econstructor. eauto. * auto_ctrans. * auto_ctrans. + gstep. red. simpobs. econstructor. gbase. destruct REL. * eapply CIH. econstructor; [|eauto using paco2_mon with paco|]. -- eapply eqit_trans; [apply REL0|]. rewrite tau_eutt. reflexivity. -- auto_ctrans. * eapply CIH0. apply CLOL. econstructor; [|eauto|]. -- eapply eqit_trans; [apply REL0|]. rewrite tau_eutt. reflexivity. -- auto_ctrans. + punfold REL0. red in REL0. simpl in *. remember (VisF e k1) as ot. genobs m1 ot2. hinduction REL0 before CIH; intros; try discriminate. * inv_Vis. pclearbot. gstep. red. do 2 (simpobs; econstructor; eauto). intros. eapply MON; [|intros; gbase; eapply CIH; eauto]. eapply CLOV. { intros. destruct PR, EQR. econstructor; [|eauto|]; eauto using eqit_trans; auto_ctrans. } econstructor; [ eauto with itree | | auto ]. eapply MON; eauto. intros. econstructor; try reflexivity; auto_ctrans. gfinal. destruct PR; eauto. * gclo; econstructor; auto_ctrans_eq; try reflexivity. rewrite (simpobs Heqot1), tau_euttge. reflexivity. + eapply IHREL0; try eapply eqit_trans; auto_ctrans_eq. rewrite <-itree_eta, tau_eutt. reflexivity. + gclo; econstructor; auto_ctrans_eq; try reflexivity. rewrite (simpobs Heqot2), tau_euttge. reflexivity. - remember (VisF e k2) as ot. genobs t2 ot2. hinduction REL0 before CIH; intros; subst; try discriminate. + inv_Vis. pclearbot. gstep. red. simpobs. econstructor; eauto. intros. eapply MON; [|intros; gbase; eapply CIH; eauto]. eapply CLOV. { intros. destruct PR, EQR. econstructor; swap 1 2; eauto using eqit_trans; auto_ctrans. } econstructor; [ eauto with itree | | auto ]. eapply MON; eauto. intros. econstructor; auto_ctrans_eq; try reflexivity. gfinal. destruct PR; eauto. + gclo; econstructor; auto_ctrans_eq; try reflexivity. rewrite (simpobs Heqot2), tau_euttge. reflexivity. - gclo; econstructor; auto_ctrans_eq; try reflexivity. rewrite (simpobs Heqot1), tau_euttge. reflexivity. - clear t' Heqot'. remember (TauF t2) as ot. genobs t0 ot0. hinduction REL before EQL; intros; subst; try inv Heqot; eauto; cycle 1. + gclo; econstructor; auto_ctrans_eq; try reflexivity. rewrite (simpobs Heqot0), tau_euttge. reflexivity. + destruct REL; cycle 1. * gbase. apply CLOL. econstructor; [ eauto with itree | | auto ]. apply CLOD. econstructor; auto_ctrans_eq; try reflexivity. rewrite (simpobs Heqot0), tau_euttge. reflexivity. * eapply IHEQL; eauto. simpobs. econstructor; eauto. punfold H. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)