We collect in these file the main lemmas capturing the applicative, monadic, and iterative structure of itrees.
Section withE. Context {I} {E : event I I}.
fmap respects strong bisimilarity.
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)Proper (dpointwise_relation (fun i : I => RX i ==> RY i) ==> dpointwise_relation (fun i : I => it_eq RX (i:=i) ==> it_eq RY (i:=i))) fmapI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)Proper (dpointwise_relation (fun i : I => RX i ==> RY i) ==> dpointwise_relation (fun i : I => it_eq RX (i:=i) ==> it_eq RY (i:=i))) fmapI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f gdpointwise_relation (fun i : I => (it_eq RX (i:=i) ==> it_eq RY (i:=i))%signature) (fmap f) (fmap g)I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f gforall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> gfp (it_eq_map E RY) a (f <$> x) (g <$> y)I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
h: gfp (it_eq_map E RX) i x yit_eq_bt E RY R i (f <$> x) (g <$> y)I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
h: it_eq_map E RX (gfp (it_eq_map E RX)) i x yit_eq_bt E RY R i (f <$> x) (g <$> y)econstructor; now apply H1. Qed.I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f <$> x) (g <$> y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2it_eqF E RY (it_eq_t E RY R) i (RetF (f i r1)) (RetF (g i r2))
fmap respects weak bisimilarity.
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)Proper (dpointwise_relation (fun i : I => RX i ==> RY i) ==> dpointwise_relation (fun i : I => it_wbisim RX i ==> it_wbisim RY i)) fmapI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)Proper (dpointwise_relation (fun i : I => RX i ==> RY i) ==> dpointwise_relation (fun i : I => it_wbisim RX i ==> it_wbisim RY i)) fmapI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f gdpointwise_relation (fun i : I => (it_wbisim RX i ==> it_wbisim RY i)%signature) (fmap f) (fmap g)I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f gforall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> gfp (it_wbisim_map E RY) a (f <$> x) (g <$> y)I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
h: gfp (it_wbisim_map E RX) i x yit_wbisim_bt E RY R i (f <$> x) (g <$> y)I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
h: it_wbisim_map E RX (gfp (it_wbisim_map E RX)) i x yit_wbisim_bt E RY R i (f <$> x) (g <$> y)I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
h: it_wbisimF E RX (gfp (it_wbisim_map E RX)) i (_observe x) (_observe y)it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) endI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
x1, x2: itree' E X i
r1: it_eat i (_observe x) x1
r2: it_eat i (_observe y) x2
rr: it_eqF E RX (gfp (it_wbisim_map E RX)) i x1 x2it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) endI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) endI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) endI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) endI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) endI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3itree' E Y iI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3itree' E Y iI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end ?x1I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end ?x2I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2exact (RetF (f i r0)).I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3itree' E Y iexact (RetF (g i r3)).I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3itree' E Y iI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (RetF (f i r0))I: Type
E: event I I
X, Y: psh I
f: forall a : I, X a -> Y a
i: I
r0: X i
ot: itree' E X i
r1: it_eat i ot (RetF r0)it_eat i match ot with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (RetF (f i r0))exact (IHr1 Y f r0 eq_refl).I: Type
E: event I I
X: psh I
i: I
t1: itree E X i
r0: X i
r1: it_eat i (observe t1) (RetF r0)
IHr1: forall (Y : psh I) (f : forall a : I, X a -> Y a) (r1 : X i), RetF r0 = RetF r1 -> it_eat i match observe t1 with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (RetF (f i r1))
Y: psh I
f: forall a : I, X a -> Y ait_eat i (observe (f <$> t1)) (RetF (f i r0))I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (RetF (g i r3))I: Type
E: event I I
X, Y: psh I
g: forall a : I, X a -> Y a
i: I
r3: X i
ot: itree' E X i
r2: it_eat i ot (RetF r3)it_eat i match ot with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (RetF (g i r3))exact (IHr2 Y g r3 eq_refl).I: Type
E: event I I
X: psh I
i: I
t1: itree E X i
r3: X i
r2: it_eat i (observe t1) (RetF r3)
IHr2: forall (Y : psh I) (g : forall a : I, X a -> Y a) (r4 : X i), RetF r3 = RetF r4 -> it_eat i match observe t1 with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (RetF (g i r4))
Y: psh I
g: forall a : I, X a -> Y ait_eat i (observe (g <$> t1)) (RetF (g i r3))I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3it_eqF E RY (it_wbisim_t E RY R) i (RetF (f i r0)) (RetF (g i r3))now apply H1.I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3RY i (f i r0) (g i r3)I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) endI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2itree' E Y iI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2itree' E Y iI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end ?x1I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end ?x2I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2exact (TauF (f <$> t1)).I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2itree' E Y iexact (TauF (g <$> t2)).I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2itree' E Y iI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (TauF (f <$> t1))I: Type
E: event I I
X, Y: psh I
f: forall a : I, X a -> Y a
i: I
t1: itree E X i
ot: itree' E X i
r1: it_eat i ot (TauF t1)it_eat i match ot with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (TauF (f <$> t1))exact (IHr1 Y f t1 eq_refl).I: Type
E: event I I
X: psh I
i: I
t0, t1: itree E X i
r1: it_eat i (observe t0) (TauF t1)
IHr1: forall (Y : psh I) (f : forall a : I, X a -> Y a) (t2 : itree E X i), TauF t1 = TauF t2 -> it_eat i match observe t0 with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (TauF (f <$> t2))
Y: psh I
f: forall a : I, X a -> Y ait_eat i (observe (f <$> t0)) (TauF (f <$> t1))I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (TauF (g <$> t2))I: Type
E: event I I
X, Y: psh I
g: forall a : I, X a -> Y a
i: I
t2: itree E X i
ot: itree' E X i
r2: it_eat i ot (TauF t2)it_eat i match ot with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (TauF (g <$> t2))exact (IHr2 Y g t2 eq_refl).I: Type
E: event I I
X: psh I
i: I
t1, t2: itree E X i
r2: it_eat i (observe t1) (TauF t2)
IHr2: forall (Y : psh I) (g : forall a : I, X a -> Y a) (t3 : itree E X i), TauF t2 = TauF t3 -> it_eat i match observe t1 with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (TauF (g <$> t3))
Y: psh I
g: forall a : I, X a -> Y ait_eat i (observe (g <$> t1)) (TauF (g <$> t2))I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2it_eqF E RY (it_wbisim_t E RY R) i (TauF (f <$> t1)) (TauF (g <$> t2))now apply CIH.I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2it_wbisim_t E RY R i (f <$> t1) (g <$> t2)I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) endI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)itree' E Y iI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)itree' E Y iI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end ?x1I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end ?x2I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2exact (VisF q (fun r => f <$> k1 r)).I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)itree' E Y iexact (VisF q (fun r => g <$> k2 r)).I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)itree' E Y iI: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (VisF q (fun r : e_rsp q => f <$> k1 r))I: Type
E: event I I
X, Y: psh I
f: forall a : I, X a -> Y a
i: I
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
ot: itree' E X i
r1: it_eat i ot (VisF q k1)it_eat i match ot with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (VisF q (fun r : e_rsp q => f <$> k1 r))exact (IHr1 Y f q k1 eq_refl).I: Type
E: event I I
X: psh I
i: I
t1: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (observe t1) (VisF q k1)
IHr1: forall (Y : psh I) (f : forall a : I, X a -> Y a) (q0 : e_qry i) (k2 : forall x : e_rsp q0, itree E X (e_nxt x)), VisF q k1 = VisF q0 k2 -> it_eat i match observe t1 with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (VisF q0 (fun r : e_rsp q0 => f <$> k2 r))
Y: psh I
f: forall a : I, X a -> Y ait_eat i (observe (f <$> t1)) (VisF q (fun r : e_rsp q => f <$> k1 r))I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (VisF q (fun r : e_rsp q => g <$> k2 r))I: Type
E: event I I
X, Y: psh I
g: forall a : I, X a -> Y a
i: I
q: e_qry i
k2: forall x : e_rsp q, itree E X (e_nxt x)
ot: itree' E X i
r2: it_eat i ot (VisF q k2)it_eat i match ot with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (VisF q (fun r : e_rsp q => g <$> k2 r))exact (IHr2 Y g q k2 eq_refl).I: Type
E: event I I
X: psh I
i: I
t1: itree E X i
q: e_qry i
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (observe t1) (VisF q k2)
IHr2: forall (Y : psh I) (g : forall a : I, X a -> Y a) (q0 : e_qry i) (k3 : forall x : e_rsp q0, itree E X (e_nxt x)), VisF q k2 = VisF q0 k3 -> it_eat i match observe t1 with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (VisF q0 (fun r : e_rsp q0 => g <$> k3 r))
Y: psh I
g: forall a : I, X a -> Y ait_eat i (observe (g <$> t1)) (VisF q (fun r : e_rsp q => g <$> k2 r))I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)it_eqF E RY (it_wbisim_t E RY R) i (VisF q (fun r : e_rsp q => f <$> k1 r)) (VisF q (fun r : e_rsp q => g <$> k2 r))intro r; now apply CIH. Qed.I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)forall r : e_rsp q, it_wbisim_t E RY R (e_nxt r) (f <$> k1 r) (g <$> k2 r)
subst respects weak bisimilarity.
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y YProper (dpointwise_relation (fun i : I => RX i ==> it_eq RY (i:=i)) ==> dpointwise_relation (fun i : I => it_eq RX (i:=i) ==> it_eq RY (i:=i))) substI: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y YProper (dpointwise_relation (fun i : I => RX i ==> it_eq RY (i:=i)) ==> dpointwise_relation (fun i : I => it_eq RX (i:=i) ==> it_eq RY (i:=i))) substI: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Yforall x y : forall a : I, X a -> itree E Y a, (forall (a : I) (x0 y0 : X a), RX a x0 y0 -> gfp (it_eq_map E RY) a (x a x0) (y a y0)) -> forall (a : I) (x0 y0 : itree E X a), gfp (it_eq_map E RX) a x0 y0 -> gfp (it_eq_map E RY) a (x =<< x0) (y =<< y0)I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x, y: itree E X i
h2: gfp (it_eq_map E RX) i x yit_eq_bt E RY R i (f =<< x) (g =<< y)I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x, y: itree E X i
h2: it_eq_map E RX (gfp (it_eq_map E RX)) i x yit_eq_bt E RY R i (f =<< x) (g =<< y)I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2it_eqF E RY (it_eq_t E RY R) i (_observe (f i r1)) (_observe (g i r2))I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
h3:= h1 i r1 r2 r_rel: gfp (it_eq_map E RY) i (f i r1) (g i r2)it_eqF E RY (it_eq_t E RY R) i (_observe (f i r1)) (_observe (g i r2))I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
h3: it_eq_map E RY (gfp (it_eq_map E RY)) i (f i r1) (g i r2)it_eqF E RY (it_eq_t E RY R) i (_observe (f i r1)) (_observe (g i r2))I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
h3: it_eqF E RY (gfp (it_eq_map E RY)) i (_observe (f i r1)) (_observe (g i r2))it_eqF E RY (it_eq_t E RY R) i (_observe (f i r1)) (_observe (g i r2))I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
t1, t2: itree E Y i
t_rel: gfp (it_eq_map E RY) i t1 t2it_eq_t E RY R i t1 t2I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
q: e_qry i
k1, k2: forall x : e_rsp q, itree E Y (e_nxt x)
k_rel: forall r : e_rsp q, gfp (it_eq_map E RY) (e_nxt r) (k1 r) (k2 r)forall r : e_rsp q, it_eq_t E RY R (e_nxt r) (k1 r) (k2 r)all: now apply (gfp_t (it_eq_map E RY)). Qed.I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
t1, t2: itree E Y i
t_rel: gfp (it_eq_map E RY) i t1 t2it_eq_t E RY R i t1 t2I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
q: e_qry i
k1, k2: forall x : e_rsp q, itree E Y (e_nxt x)
k_rel: forall r : e_rsp q, gfp (it_eq_map E RY) (e_nxt r) (k1 r) (k2 r)
r: e_rsp qit_eq_t E RY R (e_nxt r) (k1 r) (k2 r)
A slight generalization of the monad law t ≊ t >>= η.
I: Type
E: event I I
X, Y: psh I
RX: relᵢ Y Y
H: Reflexiveᵢ RX
f: X ⇒ᵢ Y
i: I
t: itree E X iit_eq RX (f <$> t) (t >>= (fun (i : I) (x : X i) => Ret' (f i x)))I: Type
E: event I I
X, Y: psh I
RX: relᵢ Y Y
H: Reflexiveᵢ RX
f: X ⇒ᵢ Y
i: I
t: itree E X iit_eq RX (f <$> t) (t >>= (fun (i : I) (x : X i) => Ret' (f i x)))cbn; destruct (_observe t); auto. Qed.I: Type
E: event I I
X, Y: psh I
RX: relᵢ Y Y
H: Reflexiveᵢ RX
f: X ⇒ᵢ Y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E X i), it_eq_t E RX R i (f <$> t0) (t0 >>= (fun (i0 : I) (x : X i0) => Ret' (f i0 x)))
i: I
t: itree E X iit_eq_bt E RX R i (f <$> t) (t >>= (fun (i : I) (x : X i) => Ret' (f i x)))I: Type
E: event I I
X, Y: psh I
f: X ⇒ᵢ itree E Y
i: IProper (it_eat' i ==> it_eat' i) (subst f i)I: Type
E: event I I
X, Y: psh I
f: X ⇒ᵢ itree E Y
i: IProper (it_eat' i ==> it_eat' i) (subst f i)I: Type
E: event I I
X, Y: psh I
f: X ⇒ᵢ itree E Y
i: I
x, y: itree E X i
H: it_eat i (_observe x) (_observe y)it_eat i match _observe x with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) end match _observe y with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) endI: Type
E: event I I
X, Y: psh I
f: X ⇒ᵢ itree E Y
i: I
x, y: itree E X i
_x: itree' E X i
H: it_eat i _x (_observe y)it_eat i match _x with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) end match _observe y with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) enddependent induction H; now econstructor. Qed.I: Type
E: event I I
X, Y: psh I
f: X ⇒ᵢ itree E Y
i: I
x, y: itree E X i
_x, _y: itree' E X i
H: it_eat i _x _yit_eat i match _x with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) end match _y with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) end
Composition law of bind.
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ itree E Z
i: I
x: itree E X iit_eq RZ ((x >>= f) >>= g) (x >>= (f >=> g))I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ itree E Z
i: I
x: itree E X iit_eq RZ ((x >>= f) >>= g) (x >>= (f >=> g))I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ itree E Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i ((x >>= f) >>= g) (x >>= (f >=> g))
i: I
x: itree E X iit_eq_bt E RZ R i ((x >>= f) >>= g) (x >>= (f >=> g))I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ itree E Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i ((x >>= f) >>= g) (x >>= (f >=> g))
i: I
x: itree E X i
r: X iit_eqF E RZ (it_eq_t E RZ R) i match _observe (f i r) with | RetF r => _observe (g i r) | TauF t => TauF (g =<< t) | VisF e k => VisF e (fun r : e_rsp e => g =<< k r) end match _observe (f i r) with | RetF r => _observe (g i r) | TauF t => TauF (g =<< t) | VisF e k => VisF e (fun r : e_rsp e => g =<< k r) enddestruct ((g i r0).(_observe)); eauto. Qed.I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ itree E Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i ((x >>= f) >>= g) (x >>= (f >=> g))
i: I
x: itree E X i
r: X i
r0: Y iit_eqF E RZ (it_eq_t E RZ R) i (_observe (g i r0)) (_observe (g i r0))
Composition law of fmap.
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ Z
i: I
x: itree E X iit_eq RZ (g <$> (f <$> x)) ((fun i : I => g i ∘ f i) <$> x)I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ Z
i: I
x: itree E X iit_eq RZ (g <$> (f <$> x)) ((fun i : I => g i ∘ f i) <$> x)cbn; destruct (x.(_observe)); eauto. Qed.I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i (g <$> (f <$> x)) ((fun i0 : I => g i0 ∘ f i0) <$> x)
i: I
x: itree E X iit_eq_bt E RZ R i (g <$> (f <$> x)) ((fun i : I => g i ∘ f i) <$> x)
bind and fmap interaction.
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ itree E Z
i: I
x: itree E X iit_eq RZ ((f <$> x) >>= g) (x >>= (fun i : I => g i ∘ f i))I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ itree E Z
i: I
x: itree E X iit_eq RZ ((f <$> x) >>= g) (x >>= (fun i : I => g i ∘ f i))I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ itree E Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i ((f <$> x) >>= g) (x >>= (fun i0 : I => g i0 ∘ f i0))
i: I
x: itree E X iit_eq_bt E RZ R i ((f <$> x) >>= g) (x >>= (fun i : I => g i ∘ f i))destruct ((g i (f i r)).(_observe)); eauto. Qed.I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ itree E Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i ((f <$> x) >>= g) (x >>= (fun i0 : I => g i0 ∘ f i0))
i: I
x: itree E X i
r: X iit_eqF E RZ (it_eq_t E RZ R) i (_observe (g i (f i r))) (_observe (g i (f i r)))I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ Z
i: I
x: itree E X iit_eq RZ (g <$> (x >>= f)) (x >>= (fun i : I => fmap g i ∘ f i))I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ Z
i: I
x: itree E X iit_eq RZ (g <$> (x >>= f)) (x >>= (fun i : I => fmap g i ∘ f i))I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i (g <$> (x >>= f)) (x >>= (fun i0 : I => fmap g i0 ∘ f i0))
i: I
x: itree E X iit_eq_bt E RZ R i (g <$> (x >>= f)) (x >>= (fun i : I => fmap g i ∘ f i))destruct ((f i r).(_observe)); eauto. Qed.I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i (g <$> (x >>= f)) (x >>= (fun i0 : I => fmap g i0 ∘ f i0))
i: I
x: itree E X i
r: X iit_eqF E RZ (it_eq_t E RZ R) i match _observe (f i r) with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end match _observe (f i r) with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end
Rewording composition law of bind.
I: Type
E: event I I
X, Y, Z: psh I
f: Y ⇒ᵢ itree E Z
g: X ⇒ᵢ itree E Y
i: I
x: itree E X i((x >>= g) >>= f) ≊ (x >>= (g >=> f))apply bind_bind_com. Qed.I: Type
E: event I I
X, Y, Z: psh I
f: Y ⇒ᵢ itree E Z
g: X ⇒ᵢ itree E Y
i: I
x: itree E X i((x >>= g) >>= f) ≊ (x >>= (g >=> f))
Proof of the up-to bind principle: we may close bisimulation candidates by prefixing related elements by bisimilar computations.
Variant bindR {X1 X2 Y1 Y2} (RX : relᵢ X1 X2) (R : relᵢ (itree E X1) (itree E X2)) (S : relᵢ (itree E Y1) (itree E Y2)) : relᵢ (itree E Y1) (itree E Y2) := | BindR {i t1 t2 k1 k2} (u : R i t1 t2) (v : forall i x1 x2, RX i x1 x2 -> S i (k1 i x1) (k2 i x2)) : bindR RX R S i (t1 >>= k1) (t2 >>= k2). Arguments BindR {X1 X2 Y1 Y2 RX R S i t1 t2 k1 k2}. Hint Constructors bindR : core.
Up-to bind is valid for strong bisimilarity.
Program Definition bindR_eq_map {X1 X2 Y1 Y2} (RX : relᵢ X1 X2) : mon (relᵢ (itree E Y1) (itree E Y2)) := {| body S := bindR RX (@it_eq _ E _ _ RX) S ; Hbody _ _ H _ _ _ '(BindR u v) := BindR u (fun i _ _ r => H _ _ _ (v i _ _ r)) |}.I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2bindR_eq_map RX <= it_eq_t E RYI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2bindR_eq_map RX <= it_eq_t E RYI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_eq RX t1 t2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eq_map E RY R i (k1 i x1) (k2 i x2)bT (it_eq_map E RY) (bindR_eq_map RX) R i0 (t1 >>= k1) (t2 >>= k2)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_eq_map E RX (gfp (it_eq_map E RX)) i0 t1 t2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eq_map E RY R i (k1 i x1) (k2 i x2)bT (it_eq_map E RY) (bindR_eq_map RX) R i0 (t1 >>= k1) (t2 >>= k2)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_eqF E RX (gfp (it_eq_map E RX)) i0 (_observe t1) (_observe t2)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r1: X1 i0
r2: X2 i0
r_rel: RX i0 r1 r2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (_observe (k1 i0 r1)) (_observe (k2 i0 r2))I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
t3: itree E X2 i0
t_rel: gfp (it_eq_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (TauF (k1 =<< t0)) (TauF (k2 =<< t3))I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
k_rel: forall r : e_rsp q, gfp (it_eq_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (VisF q (fun r : e_rsp q => k1 =<< k0 r)) (VisF q (fun r : e_rsp q => k2 =<< k3 r))refine (it_eqF_mon _ _ (id_T _ _ R) _ _ _ (v i0 _ _ r_rel)).I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r1: X1 i0
r2: X2 i0
r_rel: RX i0 r1 r2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (_observe (k1 i0 r1)) (_observe (k2 i0 r2))I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
t3: itree E X2 i0
t_rel: gfp (it_eq_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (TauF (k1 =<< t0)) (TauF (k2 =<< t3))refine (BindR t_rel (fun i _ _ r => b_T (it_eq_map E RY) _ _ _ _ _ (v i _ _ r))).I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
t3: itree E X2 i0
t_rel: gfp (it_eq_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))(bindR_eq_map RX ° it_eq_T E RY (bindR_eq_map RX)) R i0 (k1 =<< t0) (k2 =<< t3)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
k_rel: forall r : e_rsp q, gfp (it_eq_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (VisF q (fun r : e_rsp q => k1 =<< k0 r)) (VisF q (fun r : e_rsp q => k2 =<< k3 r))refine (BindR (k_rel r) (fun i _ _ r => b_T (it_eq_map E RY) _ _ _ _ _ (v i _ _ r))). Qed.I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
k_rel: forall r : e_rsp q, gfp (it_eq_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
r: e_rsp q(bindR_eq_map RX ° it_eq_T E RY (bindR_eq_map RX)) R (e_nxt r) (k1 =<< k0 r) (k2 =<< k3 r)
Up-to bind is valid for weak bisimilarity.
Program Definition bindR_w_map {X1 X2 Y1 Y2} (RX : relᵢ X1 X2) : mon (relᵢ (itree E Y1) (itree E Y2)) := {| body S := bindR RX (@it_wbisim _ E _ _ RX) S ; Hbody _ _ H _ _ _ '(BindR u v) := BindR u (fun i _ _ r => H _ _ _ (v i _ _ r)) |}.I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2bindR_w_map RX <= it_wbisim_t E RYI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2bindR_w_map RX <= it_wbisim_t E RYI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_wbisim RX i0 t1 t2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisim_map E RY R i (k1 i x1) (k2 i x2)bT (it_wbisim_map E RY) (bindR_w_map RX) R i0 (t1 >>= k1) (t2 >>= k2)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_wbisim_map E RX (gfp (it_wbisim_map E RX)) i0 t1 t2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisim_map E RY R i (k1 i x1) (k2 i x2)bT (it_wbisim_map E RY) (bindR_w_map RX) R i0 (t1 >>= k1) (t2 >>= k2)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_wbisimF E RX (gfp (it_wbisim_map E RX)) i0 (_observe t1) (_observe t2)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2it_eat i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end ?x1I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 ?x1 ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 x1 ?x2now apply (it_eqF_mon _ _ (id_T _ _ R)).I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 x1 x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eat i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end ?x1I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 ?x1 ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 (_observe (k1 =<< Tau' t0)) ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 (_observe (k1 =<< Tau' t0)) (_observe (k2 =<< Tau' t3))I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_wbisim_T E RY (bindR_w_map RX) R i0 (k1 =<< t0) (k2 =<< t3)econstructor; [ apply t_rel | intros; now apply (b_T (it_wbisim_map E RY)), v ].I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))(bindR_w_map RX ° it_wbisim_T E RY (bindR_w_map RX)) R i0 (k1 =<< t0) (k2 =<< t3)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eat i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end ?x1I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 ?x1 ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 (_observe (k1 =<< Vis' q k0)) ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 (_observe (k1 =<< Vis' q k0)) (_observe (k2 =<< Vis' q k3))I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
r: e_rsp qit_wbisim_T E RY (bindR_w_map RX) R (e_nxt r) (k1 =<< k0 r) (k2 =<< k3 r)econstructor; [ apply k_rel | intros; now apply (b_T (it_wbisim_map E RY)), v ]. Qed.I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
r: e_rsp q(bindR_w_map RX ° it_wbisim_T E RY (bindR_w_map RX)) R (e_nxt r) (k1 =<< k0 r) (k2 =<< k3 r)
Bisimilar equations have bisimilar iteration (weakly and strongly).
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq RY (iter f i a) (iter g i b)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq RY (iter f i a) (iter g i b)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a bit_eq_bt E RY R i (iter f i a) (iter g i b)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
h1:= H i a b r: it_eq (sumᵣ RX RY) (f i a) (g i b)it_eq_bt E RY R i (iter f i a) (iter g i b)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
h1: it_eqF E (sumᵣ RX RY) (it_eq (sumᵣ RX RY)) i (_observe (f i a)) (_observe (g i b))it_eqF E RY (it_eq_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
r1: (X1 +ᵢ Y1) i
r2: (X2 +ᵢ Y2) i
r_rel: sumᵣ RX RY i r1 r2it_eqF E RY (it_eq_t E RY R) i match r1 with | inl x => TauF (iter f i x) | inr y => RetF y end match r2 with | inl x => TauF (iter g i x) | inr y => RetF y endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
t2: itree E (X2 +ᵢ Y2) i
t_rel: it_eq (sumᵣ RX RY) t1 t2it_eqF E RY (it_eq_t E RY R) i (TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1)) (TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2))I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
k_rel: forall r : e_rsp q, it_eq (sumᵣ RX RY) (k1 r) (k2 r)it_eqF E RY (it_eq_t E RY R) i (VisF q (fun r : e_rsp q => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r)) (VisF q (fun r : e_rsp q => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r))destruct r_rel; eauto.I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
r1: (X1 +ᵢ Y1) i
r2: (X2 +ᵢ Y2) i
r_rel: sumᵣ RX RY i r1 r2it_eqF E RY (it_eq_t E RY R) i match r1 with | inl x => TauF (iter f i x) | inr y => RetF y end match r2 with | inl x => TauF (iter g i x) | inr y => RetF y endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
t2: itree E (X2 +ᵢ Y2) i
t_rel: it_eq (sumᵣ RX RY) t1 t2it_eqF E RY (it_eq_t E RY R) i (TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1)) (TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2))I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
t2: itree E (X2 +ᵢ Y2) i
t_rel: it_eq (sumᵣ RX RY) t1 t2it_eq_t E RY R i ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
t2: itree E (X2 +ᵢ Y2) i
t_rel: it_eq (sumᵣ RX RY) t1 t2it_eq_t E RY (it_eq_t E RY R) i ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2)intros ? ? ? []; apply (tt_t (it_eq_map E RY)), (b_t (it_eq_map E RY)); cbn; eauto.I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
t2: itree E (X2 +ᵢ Y2) i
t_rel: it_eq (sumᵣ RX RY) t1 t2forall (i : I) (x1 : (X1 +ᵢ Y1) i) (x2 : (X2 +ᵢ Y2) i), sumᵣ RX RY i x1 x2 -> it_eq_t E RY R i {| _observe := match x1 with | inl x => TauF (iter f i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter g i x) | inr y => RetF y end |}I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
k_rel: forall r : e_rsp q, it_eq (sumᵣ RX RY) (k1 r) (k2 r)it_eqF E RY (it_eq_t E RY R) i (VisF q (fun r : e_rsp q => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r)) (VisF q (fun r : e_rsp q => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r))I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
k_rel: forall r : e_rsp q, it_eq (sumᵣ RX RY) (k1 r) (k2 r)
r0: e_rsp qit_eq_t E RY R (e_nxt r0) ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r0) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r0)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
k_rel: forall r : e_rsp q, it_eq (sumᵣ RX RY) (k1 r) (k2 r)
r0: e_rsp qit_eq_t E RY (it_eq_t E RY R) (e_nxt r0) ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r0) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r0)intros ? ? ? []; apply (bt_t (it_eq_map E RY)); cbn; eauto. Qed. #[global] Instance iter_proper_strong {X Y} {RX : relᵢ X X} {RY : relᵢ Y Y} : Proper (dpointwise_relation (fun i => RX i ==> it_eq (sumᵣ RX RY) (i:=i)) ==> dpointwise_relation (fun i => RX i ==> it_eq RY (i:=i))) (@iter I E X Y) := iter_cong_strong.I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
k_rel: forall r : e_rsp q, it_eq (sumᵣ RX RY) (k1 r) (k2 r)
r0: e_rsp qforall (i : I) (x1 : (X1 +ᵢ Y1) i) (x2 : (X2 +ᵢ Y2) i), sumᵣ RX RY i x1 x2 -> it_eq_t E RY R i {| _observe := match x1 with | inl x => TauF (iter f i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter g i x) | inr y => RetF y end |}I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim RY i (iter f i a) (iter g i b)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim RY i (iter f i a) (iter g i b)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a bit_wbisim_bt E RY R i (iter f i a) (iter g i b)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
H1:= H i a b r: it_wbisim (sumᵣ RX RY) i (f i a) (g i b)it_wbisim_bt E RY R i (iter f i a) (iter g i b)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
H1: it_wbisim_map E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i (f i a) (g i b)it_wbisim_bt E RY R i (iter f i a) (iter g i b)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
H1: it_wbisimF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i (_observe (f i a)) (_observe (g i b))it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
r0: (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (RetF r0)
r3: (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (RetF r3)
r_rel: sumᵣ RX RY i r0 r3it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
r0: (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (RetF r0)
r3: (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (RetF r3)
r_rel: sumᵣ RX RY i r0 r3it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
H2:= H i x1 x2 H0: it_wbisim (sumᵣ RX RY) i (f i x1) (g i x2)it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
H2: it_wbisim_map E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i (f i x1) (g i x2)it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3it_eat i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end ?x1I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Ret' (inl x1))) ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Ret' (inl x1))) (_observe ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< Ret' (inl x2)))now apply CIH.I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3it_wbisim_t E RY R i (iter f i x1) (iter g i x2)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2it_eat i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end ?x1I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Ret' (inr y1))) ?x2now cbn; econstructor.I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Ret' (inr y1))) (_observe ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< Ret' (inr y2)))I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2it_eat i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end ?x1I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Tau' t1)) ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Tau' t1)) (_observe ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< Tau' t2))I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2it_wbisim_t E RY R i ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2it_wbisim_t E RY (it_wbisim_t E RY R) i ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2)intros ? ? ? []; apply (tt_t (it_wbisim_map E RY)), (b_t (it_wbisim_map E RY)); cbn; eauto.I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2forall (i : I) (x1 : (X1 +ᵢ Y1) i) (x2 : (X2 +ᵢ Y2) i), sumᵣ RX RY i x1 x2 -> it_wbisim_t E RY R i {| _observe := match x1 with | inl x => TauF (iter f i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter g i x) | inr y => RetF y end |}I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) endI: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)it_eat i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end ?x1I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Vis' q k1)) ?x2I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Vis' q k1)) (_observe ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< Vis' q k2))I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)
r0: e_rsp qit_wbisim_t E RY R (e_nxt r0) ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r0) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r0)I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)
r0: e_rsp qit_wbisim_t E RY (it_wbisim_t E RY R) (e_nxt r0) ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r0) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r0)intros ? ? ? []; apply (tt_t (it_wbisim_map E RY)), (b_t (it_wbisim_map E RY)); cbn; eauto. Qed. #[global] Instance iter_weq {X Y} {RX : relᵢ X X} {RY : relᵢ Y Y} : Proper (dpointwise_relation (fun i => RX i ==> it_wbisim (sumᵣ RX RY) i) ==> dpointwise_relation (fun i => RX i ==> it_wbisim RY i)) (@iter I E X Y) := iter_cong_weak.I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)
r0: e_rsp qforall (i : I) (x1 : (X1 +ᵢ Y1) i) (x2 : (X2 +ᵢ Y2) i), sumᵣ RX RY i x1 x2 -> it_wbisim_t E RY R i {| _observe := match x1 with | inl x => TauF (iter f i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter g i x) | inr y => RetF y end |}
Iteration is a strong fixed point of the folowing guarded equation.
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Reflexiveᵢ0: Reflexiveᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
i: I
x: X iit_eq RY (iter f i x) (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}))I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Reflexiveᵢ0: Reflexiveᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
i: I
x: X iit_eq RY (iter f i x) (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}))I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Reflexiveᵢ0: Reflexiveᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
i: I
x: X iit_eq_map E RY (gfp (it_eq_map E RY)) i (iter f i x) (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}))destruct r; eauto. Qed.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Reflexiveᵢ0: Reflexiveᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
i: I
x: X i
r: (X +ᵢ Y) iit_eqF E RY (gfp (it_eq_map E RY)) i match r with | inl x => TauF (iter f i x) | inr y => RetF y end match r with | inl x => TauF (iter f i x) | inr y => RetF y end
Iteration is the unique such fixed point w.r.t. strong bisimilarity. Note that this is again not w.r.t. the initial equation but the alternate one which is trivially guarded. See example 6.14 in the paper.
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))forall (i : I) (x : X i), it_eq RY (g i x) (iter f i x)I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))forall (i : I) (x : X i), it_eq RY (g i x) (iter f i x)I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X iit_eq_bt E RY R i (g i x) (iter f i x)I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i(it_eq_t E RY ° it_eq_bt E RY) R i (g i x) (iter f i x)I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i(it_eq_t E RY ° it_eq_bt E RY) R i (g i x) ?yI: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i(it_eq_t E RY ° it_eq_bt E RY) R i ?y (iter f i x)I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i(it_eq_t E RY ° it_eq_bt E RY) R i (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (g i x) | inr y => RetF y end |})) (iter f i x)I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i(it_eq_t E RY ° it_eq_bt E RY) R i ?y (iter f i x)I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i(it_eq_t E RY ° it_eq_bt E RY) R i (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (g i x) | inr y => RetF y end |})) ?yI: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i(it_eq_t E RY ° it_eq_bt E RY) R i (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (g i x) | inr y => RetF y end |})) (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}))I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X ibindR_eq_map (eqᵢ (X +ᵢ Y)) (it_eq_bt E RY R) i (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (g i x) | inr y => RetF y end |})) (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}))I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X if i x ≊ f i xI: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X iforall (i : I) (x1 x2 : (X +ᵢ Y) i), eqᵢ (X +ᵢ Y) i x1 x2 -> it_eq_bt E RY R i {| _observe := match x1 with | inl x => TauF (g i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter f i x) | inr y => RetF y end |}I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X iforall (i : I) (x1 x2 : (X +ᵢ Y) i), eqᵢ (X +ᵢ Y) i x1 x2 -> it_eq_bt E RY R i {| _observe := match x1 with | inl x => TauF (g i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter f i x) | inr y => RetF y end |}I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i
i0: I
x0: X i0it_eq_t E RY R i0 (g i0 x0) (iter f i0 x0)I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i
i0: I
y: Y i0RY i0 y yreflexivity. Qed. End withE.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i
i0: I
y: Y i0RY i0 y y
Misc. utilities.
Variant is_tau' {I} {E : event I I} {X i} : itree' E X i -> Prop := | IsTau {t : itree E X i} : is_tau' (TauF t) . Definition is_tau {I} {E : event I I} {X i} (t : itree E X i) : Prop := is_tau' t.(_observe). Variant is_ret' {I} {E : event I I} {X i} : itree' E X i -> Prop := | IsRet {x : X i} : is_ret' (RetF x) . Definition is_ret {I} {E : event I I} {X i} (t : itree E X i) : Prop := is_ret' t.(_observe).I: Type
E: event I I
X: psh I
i: I
t: itree E X iis_ret t -> X iI: Type
E: event I I
X: psh I
i: I
t: itree E X iis_ret t -> X iI: Type
E: event I I
X: psh I
i: I
t: itree E X iis_ret' (_observe t) -> X iexact r. Defined.I: Type
E: event I I
X: psh I
i: I
t: itree E X i
r: X i
p: is_ret' (RetF r)X i