Delay Monad

Instead of defining the delay monad from scratch, we construct it as a special case of itree, namely ones with an empty signature ∅ₑ (disallowing Vis nodes) and indexed over the singleton type T1.

The delay monad (Def 4.5) is formalized as an itree over an empty signature: in the absence of events, Tau and Ret are the only possible transitions.

Relevant definitions can be found:

for the underlying itree datatype, in ITree/ITree.v,
for the combinators, in ITree/Structure.v,
for the (strong/weak) bisimilarity, in ITree/Eq.v,
for guarded iteration (§ 6.2), in ITree/Guarded.v.

Definition delay (X : Type) : Type := itree ∅ₑ (fun _ => X) T1_0.

Embedding [delay] into itrees over arbitrary signatures.

Definition emb_delay {I} {E : event I I} {X i} : delay X -> itree E (X @ i) i :=
  cofix _emb_delay x :=
      go (match x.(_observe) with
         | RetF r => RetF (Fib r)
         | TauF t => TauF (_emb_delay t)
         | VisF e k => match e with end
         end).

#[global] Notation "'RetD' x" := (RetF (x : (fun _ : T1 => _) T1_0)) (at level 40).
#[global] Notation "'TauD' t" := (TauF (t : itree ∅ₑ (fun _ : T1 => _) T1_0)) (at level 40).

Specialization of the operations to the delay monad. Most of them are a bit cumbersome since our definition of itree is indexed, but delay should not. As such there is a bit of a dance around the singleton type T1 which is used as index. Too bad, since Coq does not have typed conversion we don't get definitional eta-law for the unit type...

Definition ret_delay {X} : X -> delay X := fun x => Ret' x .

Definition tau_delay {X} : delay X -> delay X :=
  fun t => go (TauF (t : itree ∅ₑ (fun _ : T1 => X) T1_0)) .

Binding a delay computation in the context of an itree.

Definition bind_delay {I} {E : event I I} {X Y i}
  : delay X -> (X -> itree E Y i) -> itree E Y i
  := fun x f => bind (emb_delay x) (fun _ '(Fib x) => f x) .

Simpler definition of bind when the conclusion is again in delay.

Definition bind_delay' {X Y}
  : delay X -> (X -> delay Y) -> delay Y
  := fun x f => bind x (fun 'T1_0 y => f y).

Functorial action on maps.

Definition fmap_delay {X Y} (f : X -> Y) : delay X -> delay Y :=
  fmap (fun _ => f) T1_0 .

Iteration operator.

Definition iter_delay {X Y} : (X -> delay (X + Y)) -> X -> delay Y :=
  fun f => iter (fun 'T1_0 => f) T1_0 .

Alternative to bind_delay, written from scratch.

Definition subst_delay {I} {E : event I I} {X Y i} (f : X -> itree E Y i)
  : delay X -> itree E Y i
  := cofix _subst_delay x := go match x.(_observe) with
                                | RetF r => (f r).(_observe)
                                | TauF t => TauF (_subst_delay t)
                                | VisF e k => match e with end
                                end .

#[global] Instance subst_delay_eq {I E X RX Y RY i}
    : Proper ((RX ==> it_eq RY (i:=i)) ==> (it_eq (fun _ => RX) (i:=T1_0) ==> it_eq RY (i:=i)))
    (@subst_delay I E X Y i).I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
Proper
  ((RX ==> it_eq RY (i:=i)) ==>
   it_eq (fun _ : T1 => RX) (i:=T1_0) ==>
   it_eq RY (i:=i)) subst_delay
Proof.I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
Proper
  ((RX ==> it_eq RY (i:=i)) ==>
   it_eq (fun _ : T1 => RX) (i:=T1_0) ==>
   it_eq RY (i:=i)) subst_delay
  intros ? ? Hf; unfold it_eq at 2; unfold respectful; coinduction R CIH; intros t1 t2 H.I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
x, y: X -> itree E Y i
Hf: (RX ==> it_eq RY (i:=i))%signature x y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall x0 y0 : itree ∅ₑ (fun _ : T1 => X) T1_0,
it_eq (fun _ : T1 => RX) x0 y0 ->
it_eq_t E RY R i (subst_delay x x0) (subst_delay y y0)
t1, t2: itree ∅ₑ (fun _ : T1 => X) T1_0
H: it_eq (fun _ : T1 => RX) t1 t2
it_eq_bt E RY R i (subst_delay x t1)
  (subst_delay y t2)
  apply it_eq_step in H; cbn in *; unfold observe in H.I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
x, y: X -> itree E Y i
Hf: (RX ==> it_eq RY (i:=i))%signature x y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall x0 y0 : itree ∅ₑ (fun _ : T1 => X) T1_0,
it_eq (fun _ : T1 => RX) x0 y0 ->
it_eq_t E RY R i (subst_delay x x0) (subst_delay y y0)
t1, t2: itree ∅ₑ (fun _ : T1 => X) T1_0
H: it_eqF ∅ₑ (fun _ : T1 => RX)
  (it_eq (fun _ : T1 => RX)) T1_0 (_observe t1)
  (_observe t2)
it_eqF E RY (it_eq_t E RY R) i
  match _observe t1 with
  | RetF r => _observe (x r)
  | TauF t => TauF (subst_delay x t)
  | VisF e _ => match e return (itree' E Y i) with
                end
  end
  match _observe t2 with
  | RetF r => _observe (y r)
  | TauF t => TauF (subst_delay y t)
  | VisF e _ => match e return (itree' E Y i) with
                end
  end
  remember (_observe t1) as ot1; clear t1 Heqot1.I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
x, y: X -> itree E Y i
Hf: (RX ==> it_eq RY (i:=i))%signature x y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall x0 y0 : itree ∅ₑ (fun _ : T1 => X) T1_0,
it_eq (fun _ : T1 => RX) x0 y0 ->
it_eq_t E RY R i (subst_delay x x0) (subst_delay y y0)
t2: itree ∅ₑ (fun _ : T1 => X) T1_0
ot1: itree' ∅ₑ (fun _ : T1 => X) T1_0
H: it_eqF ∅ₑ (fun _ : T1 => RX)
  (it_eq (fun _ : T1 => RX)) T1_0 ot1
  (_observe t2)
it_eqF E RY (it_eq_t E RY R) i
  match ot1 with
  | RetF r => _observe (x r)
  | TauF t => TauF (subst_delay x t)
  | VisF e _ => match e return (itree' E Y i) with
                end
  end
  match _observe t2 with
  | RetF r => _observe (y r)
  | TauF t => TauF (subst_delay y t)
  | VisF e _ => match e return (itree' E Y i) with
                end
  end
  remember (_observe t2) as ot2; clear t2 Heqot2.I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
x, y: X -> itree E Y i
Hf: (RX ==> it_eq RY (i:=i))%signature x y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall x0 y0 : itree ∅ₑ (fun _ : T1 => X) T1_0,
it_eq (fun _ : T1 => RX) x0 y0 ->
it_eq_t E RY R i (subst_delay x x0) (subst_delay y y0)
ot1, ot2: itree' ∅ₑ (fun _ : T1 => X) T1_0
H: it_eqF ∅ₑ (fun _ : T1 => RX)
  (it_eq (fun _ : T1 => RX)) T1_0 ot1 ot2
it_eqF E RY (it_eq_t E RY R) i
  match ot1 with
  | RetF r => _observe (x r)
  | TauF t => TauF (subst_delay x t)
  | VisF e _ => match e return (itree' E Y i) with
                end
  end
  match ot2 with
  | RetF r => _observe (y r)
  | TauF t => TauF (subst_delay y t)
  | VisF e _ => match e return (itree' E Y i) with
                end
  end
  dependent elimination H; cbn.I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
x, y: X -> itree E Y i
Hf: (RX ==> it_eq RY (i:=i))%signature x y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall x0 y0 : itree ∅ₑ (fun _ : T1 => X) T1_0,
it_eq (fun _ : T1 => RX) x0 y0 ->
it_eq_t E RY R i (subst_delay x x0) (subst_delay y y0)
r1, r2: (fun _ : T1 => X) T1_0
r_rel: (fun _ : T1 => RX) T1_0 r1 r2
it_eqF E RY (it_eq_t E RY R) i (_observe (x r1))
  (_observe (y r2))
I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
x, y: X -> itree E Y i
Hf: (RX ==> it_eq RY (i:=i))%signature x y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall x0 y0 : itree ∅ₑ (fun _ : T1 => X) T1_0,
it_eq (fun _ : T1 => RX) x0 y0 ->
it_eq_t E RY R i (subst_delay x x0)
  (subst_delay y y0)
t1, t2: itree ∅ₑ (fun _ : T1 => X) T1_0
t_rel: it_eq (fun _ : T1 => RX) t1 t2
it_eqF E RY (it_eq_t E RY R) i
  (TauF (subst_delay x t1)) 
  (TauF (subst_delay y t2))
I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
x, y: X -> itree E Y i
Hf: (RX ==> it_eq RY (i:=i))%signature x y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall x0 y0 : itree ∅ₑ (fun _ : T1 => X) T1_0,
it_eq (fun _ : T1 => RX) x0 y0 ->
it_eq_t E RY R i (subst_delay x x0)
  (subst_delay y y0)
q: e_qry T1_0
k1, k2: forall x : e_rsp q,
itree ∅ₑ (fun _ : T1 => X) (e_nxt x)
k_rel: forall r : e_rsp q,
it_eq (fun _ : T1 => RX) (k1 r) (k2 r)
it_eqF E RY (it_eq_t E RY R) i
  match q return (itree' E Y i) with
  end match q return (itree' E Y i) with
      end
  -I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
x, y: X -> itree E Y i
Hf: (RX ==> it_eq RY (i:=i))%signature x y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall x0 y0 : itree ∅ₑ (fun _ : T1 => X) T1_0,
it_eq (fun _ : T1 => RX) x0 y0 ->
it_eq_t E RY R i (subst_delay x x0)
  (subst_delay y y0)
r1, r2: (fun _ : T1 => X) T1_0
r_rel: (fun _ : T1 => RX) T1_0 r1 r2
it_eqF E RY (it_eq_t E RY R) i 
  (_observe (x r1)) (_observe (y r2)) eapply it_eqF_mon; [ apply gfp_t | ].I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
x, y: X -> itree E Y i
Hf: (RX ==> it_eq RY (i:=i))%signature x y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall x0 y0 : itree ∅ₑ (fun _ : T1 => X) T1_0,
it_eq (fun _ : T1 => RX) x0 y0 ->
it_eq_t E RY R i (subst_delay x x0)
  (subst_delay y y0)
r1, r2: (fun _ : T1 => X) T1_0
r_rel: (fun _ : T1 => RX) T1_0 r1 r2
it_eqF E RY (gfp (it_eq_map E RY)) i 
  (_observe (x r1)) (_observe (y r2))
    specialize (Hf _ _ r_rel); apply it_eq_step in Hf; exact Hf.
  -I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
x, y: X -> itree E Y i
Hf: (RX ==> it_eq RY (i:=i))%signature x y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall x0 y0 : itree ∅ₑ (fun _ : T1 => X) T1_0,
it_eq (fun _ : T1 => RX) x0 y0 ->
it_eq_t E RY R i (subst_delay x x0)
  (subst_delay y y0)
t1, t2: itree ∅ₑ (fun _ : T1 => X) T1_0
t_rel: it_eq (fun _ : T1 => RX) t1 t2
it_eqF E RY (it_eq_t E RY R) i
  (TauF (subst_delay x t1)) 
  (TauF (subst_delay y t2)) econstructor; now apply CIH.
  -I: Type
E: event I I
X: Type
RX: relation X
Y: psh I
RY: relᵢ Y Y
i: I
x, y: X -> itree E Y i
Hf: (RX ==> it_eq RY (i:=i))%signature x y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall x0 y0 : itree ∅ₑ (fun _ : T1 => X) T1_0,
it_eq (fun _ : T1 => RX) x0 y0 ->
it_eq_t E RY R i (subst_delay x x0)
  (subst_delay y y0)
q: e_qry T1_0
k1, k2: forall x : e_rsp q,
itree ∅ₑ (fun _ : T1 => X) (e_nxt x)
k_rel: forall r : e_rsp q,
it_eq (fun _ : T1 => RX) (k1 r) (k2 r)
it_eqF E RY (it_eq_t E RY R) i
  match q return (itree' E Y i) with
  end match q return (itree' E Y i) with
      end destruct q.
Qed.