ITree.Eq.SimUpToTaus

Simulation up to taus

A preorder sutt , where every visible step (RetF or VisF) on the left must be matched with a corresponding step on the right, ignoring TauF.
In particular, spin := Tau spin is less than everything.
The induced equivalence relation is eutt.
  Theorem sutt_eutt : sutt eq t usutt eq u teutt eq t u.
Various lemmas about eutt may be more easily proved as Proper lemmas about sutt first, and then symmetrizing using eutt_sutt and sutt_eutt.

From Paco Require Import paco.

From Coq Require Import
     Morphisms.

From ITree Require Import
     Axioms
     Basics.Tacs
     Core.ITreeDefinition
     Eq.Eqit
     Eq.UpToTaus
     Eq.Shallow
     Eq.Paco2.

Section SUTT.

Context {E : Type Type} {R1 R2 : Type} (RR : Prop).

Inductive suttF (sutt: itree' E itree' E Prop) :
  itree' E itree' E Prop :=
| suttF_ret r1 r2 : RR suttF sutt (RetF ) (RetF )
| suttF_vis u (e : E u) k1 k2
      (SUTTK: x, sutt (observe ( x)) (observe ( x))):
    suttF sutt (VisF e ) (VisF e )
| suttF_tau_right ot1 t2
      (EQTAUS: suttF sutt (observe )):
    suttF sutt (TauF )
| suttF_tau_left t1 ot2
      (EQTAUS: sutt (observe ) ):
    suttF sutt (TauF )
.
Hint Constructors suttF : itree.

Definition sutt (t1 : itree E ) (t2 : itree E ) :=
   suttF (observe ) (observe ).
Hint Unfold sutt : itree.

End SUTT.

Global Hint Constructors suttF : itree.
Global Hint Unfold sutt : itree.

Section SUTT_rel.

Context {E : Type Type} {R : Type} (RR : R R Prop).

Lemma reflexive_suttF `{Reflexive _ RR} sutt (r1:Reflexive sutt) : Reflexive (@suttF E _ _ RR sutt).
Proof.
  unfold Reflexive. intros x.
  destruct x; eauto with itree.
Qed.


End SUTT_rel.

Section SUTT_facts.

Context {E : Type Type} {R1 R2 : Type} (RR : Prop).

Lemma monotone_suttF : (@suttF E _ _ RR).
Proof. repeat red; intros. induction IN; eauto with itree. Qed.
Hint Resolve monotone_suttF : paco.

End SUTT_facts.

Global Hint Resolve monotone_suttF : paco.

Lemma suttF_inv_vis {E R1 R2} (RR : Prop) sutt :
   X e (k1 : X itree E ) (k2 : X itree E ),
    suttF RR sutt (VisF e ) (VisF e )
     x, sutt (observe ( x)) (observe ( x)).
Proof.
  intros. inv H. ddestruction; auto.
Qed.


Lemma sutt_inv_vis {E R1 R2} (RR : Prop) :
   X e (k1 : X itree E ) (k2 : X itree E ),
  sutt RR (Vis e ) (Vis e )
   x, sutt RR ( x) ( x).
Proof.
  intros. pstep. punfold H. simpl in ×.
  eapply suttF_inv_vis in H; pclearbot; punfold H.
Qed.


Lemma sutt_tau_right {E R1 R2} (RR : Prop) :
   (t1 : itree E ) (t2 : itree E ),
    sutt RR
    sutt RR (Tau ).
Proof.
  intros. punfold H. pstep.
  repeat red. repeat red in H. constructor.
  auto.
Qed.


Lemma sutt_tau_left {E R1 R2} (RR : Prop) :
   (t1 : itree E ) (t2 : itree E ),
    sutt RR
    sutt RR (Tau ) .
Proof.
  intros. punfold H. pstep.
  repeat red. repeat red in H. constructor.
  eauto with paco.
Qed.


Lemma sutt_elim_tau_right {E R1 R2} (RR : Prop) :
   (t1: itree E ) (t2: itree E ),
    sutt RR (Tau )
    sutt RR .
Proof.
  pcofix CIH. pstep. intros.
  punfold . repeat red in .
  inv .
  - eapply monotone_suttF; eauto using upaco2_mon_bot with paco.
  - constructor. pclearbot. eauto with paco.
Qed.


Lemma suttF_inv_tau_left {E R1 R2} (RR : Prop) :
   (t1: itree E ) ot2,
    suttF RR ( (suttF RR) ) (TauF )
    suttF RR ( (suttF RR) ) (observe ) .
Proof.
  intros.
  remember (TauF ) as .
  induction H; intros; subst; try dependent destruction ; eauto with itree.
  pclearbot. punfold EQTAUS.
Qed.


Lemma sutt_inv_tau_left {E R1 R2} (RR : Prop) :
   (t1: itree E ) (t2: itree E ),
    sutt RR (Tau )
    sutt RR .
Proof.
  intros.
  punfold H. pstep. repeat red in H |- ×.
  apply suttF_inv_tau_left; auto.
Qed.


Theorem sutt_eutt {E R1 R2} (RR : Prop) :
   (t1 : itree E ) (t2 : itree E ),
    sutt RR sutt (flip RR) eutt RR .
Proof.
  pcofix CIH. intros.
  punfold . punfold H. pstep. red.
  induction ; intros; subst; auto with itree.
  - constructor. intro. right. eapply suttF_inv_vis in H. pclearbot. eauto with paco itree.
  - constructor; eauto. eapply IHsuttF; auto. eapply suttF_inv_tau_left; auto.
  - (* doing induction when one of the trees is a tau doesn't work well *)
    inv H; pclearbot.
    + clear . genobs .
      hinduction before CIH; intros; subst; pclearbot.
      × constructor; eauto. simpobs. constructor. eauto.
      × constructor; eauto. simpobs. constructor. intros.
        right. apply CIH; auto with itree. eapply sutt_inv_vis in EQTAUS; eauto with itree.
      × constructor; eauto. simpobs. eapply ; eauto.
        rewrite (itree_eta' ). apply sutt_inv_tau_left; auto.
      × constructor. right. apply CIH; auto. apply sutt_elim_tau_right; auto.
    + constructor. right. apply CIH; apply sutt_elim_tau_right; auto.
Qed.


Theorem eutt_sutt {E R1 R2} (RR : Prop) :
   (t1 : itree E ) (t2 : itree E ),
    eutt RR sutt RR .
Proof.
  pcofix CIH. pstep. intros.
  punfold . red in .
  induction ; constructor; pclearbot; eauto 7 with paco itree.
Qed.


Generalized heterogeneous version of eutt_bind
Lemma sutt_bind' {E R1 R2 S1 S2} {RR: Prop} {SS: Prop}:
   t1 t2,
    sutt RR
     s1 s2, ( r1 r2, RR sutt SS ( ) ( ))
                  @sutt E _ _ SS (ITree.bind ) (ITree.bind ).
Proof.
  pcofix self. pstep. intros.
  punfold . unfold observe; cbn.
  induction ; intros.
  - simpl. apply in H. punfold H. eapply monotone_suttF; eauto using upaco2_mon_bot.
  - simpl. pclearbot. econstructor. eauto with itree.
  - constructor. eauto with paco.
  - constructor. pclearbot.
    right. specialize (self (go ) EQTAUS _ _ ).
    apply self.
Qed.


(* todo: this could be made stronger with eutt rather than eq_itree
 *)

#[global] Instance Proper_sutt {E : Type Type} {R1 R2 : Type} r
: Proper (eq_itree eq eq_itree eq flip impl)
       (@sutt E r).
Proof.
  repeat red. pcofix CIH; pstep. intros.
  punfold ; punfold ; punfold . red in , .
  (* rename H1 into H2, Hxy into H1.  *)
  hinduction before CIH; subst; intros.
  - inv ; try discriminate. inv ; try discriminate. econstructor. eauto.
  - dependent destruction ; try discriminate.
    dependent destruction ; try discriminate.
    simpobs. pclearbot.
    constructor. intros. right. eauto 7 with paco itree.
  - dependent destruction ; try discriminate.
    simpobs. pclearbot. punfold REL. auto with itree.
  - dependent destruction ; try discriminate.
    simpobs. pclearbot. constructor.
    right. rewrite (itree_eta' ) in ×. eauto with itree.
Qed.