diff --git a/theories/Core/CTreeDefinitions.v b/theories/Core/CTreeDefinitions.v index f1fb5f4..39b4e79 100644 --- a/theories/Core/CTreeDefinitions.v +++ b/theories/Core/CTreeDefinitions.v @@ -25,8 +25,9 @@ br. From ITree Require Import Basics.Basics Core.Subevent Indexed.Sum. -From CTree Require Import - Core.Utils Core.Index. +From CTree Require Export + Core.Utils. +From CTree Require Import Core.Index. From ExtLib Require Import Structures.Functor diff --git a/theories/Core/Utils.v b/theories/Core/Utils.v index 99a079e..a114da7 100644 --- a/theories/Core/Utils.v +++ b/theories/Core/Utils.v @@ -1,4 +1,5 @@ -#[global] Set Warnings "-intuition-auto-with-star". +#[export] Set Warnings "-intuition-auto-with-star". +#[export] Set Warnings "-warn-library-file-stdlib-vector". From Stdlib Require Import Fin. From Stdlib Require Export Program.Equality. @@ -20,6 +21,7 @@ Polymorphic Class MonadStuck (M : Type -> Type) : Type := mstuck : forall X, M X. Notation rel X Y := (X -> Y -> Prop). +Notation rel1 E F := (forall X Y, E X -> E Y -> Prop). Ltac invert := match goal with @@ -100,7 +102,7 @@ Ltac do_det := clear RWTdet H' end. -#[global] Notation inhabited X := { x: X | True}. +(* #[global] Notation inhabited X := { x: X | True}. *) Definition sum_rel {A1 A2 B1 B2} Ra Rb : rel (A1 + B1) (A2 + B2) := fun ab ab' => @@ -109,3 +111,18 @@ Definition sum_rel {A1 A2 B1 B2} Ra Rb : rel (A1 + B1) (A2 + B2) := | inr b, inr b' => Rb b b' | _, _ => False end. + +Ltac ex := eexists. +Ltac ex2 := do 2 eexists. +Ltac ex3 := do 3 eexists. +Ltac split3 := split; [| split]. +Ltac edestruct3 H := edestruct H as (? & ? & ?). +Ltac edestruct4 H := edestruct H as (? & ? & ? & ?). +Ltac edestruct5 H := edestruct H as (? & ? & ? & ? & ?). + +(* Simple inhabited class in the sytle of stdpp. + Long term to do: use stdpp + *) +Class Inhabited (A : Type) : Type := populate { inhabitant : A }. +Global Hint Mode Inhabited ! : typeclass_instances. +Global Arguments populate {_} _ : assert. diff --git a/theories/Eq/CSSim.v b/theories/Eq/CSSim.v index c563bc7..b17632a 100644 --- a/theories/Eq/CSSim.v +++ b/theories/Eq/CSSim.v @@ -25,18 +25,16 @@ Import CoindNotations. Import CTree. Set Implicit Arguments. -(* TODO: Decide where to set this *) -Arguments trans : simpl never. - Section CompleteStrongSim. (*| Complete strong simulation [css]. |*) + Program Definition css {E F C D : Type -> Type} {X Y : Type} - (L : rel (@label E) (@label F)) : mon (ctree E C X -> ctree F D Y -> Prop) := + (L : lrel E F X Y) : mon (@S E C X -> @S F D Y -> Prop) := {| body R t u := - ss L R t u /\ (forall l u', trans l u u' -> exists l' t', trans l' t t') + ss L R t u /\ (not_stuck u -> not_stuck t) |}. Next Obligation. split; eauto. intros. @@ -51,11 +49,15 @@ Definition cssim {E F C D X Y} L := Module CSSimNotations. (*| css (complete simulation) notation |*) - Notation "t (⪅ L ) u" := (cssim L t u) (at level 70). - Notation "t ⪅ u" := (cssim eq t u) (at level 70). - Notation "t [⪅ L ] u" := (css L _ t u) (at level 79). - Notation "t [⪅] u" := (css eq _ t u) (at level 79). - + + Infix "⪅" := (cssim Leq) (at level 70). + Notation "t (⪅ [ Q ] ) u" := (cssim (Lvrel Q) t u) (at level 79). + Notation "t (⪅ Q ) u" := (cssim Q t u) (at level 79). + + Notation "t '[⪅]' u" := (css Leq (` _) t u) (at level 90, only printing). + Notation "t '[⪅' [ R ] ']' u" := (css (Lvrel R) (` _) t u) (at level 90, only printing). + Notation "t '[⪅' R ']' u" := (css R (` _) t u) (at level 90, only printing). + End CSSimNotations. Import CSSimNotations. @@ -95,51 +97,72 @@ Ltac __step_in_cssim H := Import CTreeNotations. Import EquNotations. +Ltac __play_cssim := (try step); cbn; split; [intros ? ? ?TR | etrans]. + +Ltac __play_cssim_in H := + (try step in H); + cbn in H; edestruct H as [(? & ? & ?TR & ?EQ & ?HL) ?PROG]; + clear H; [etrans |]; fold_cssim. + +Ltac __eplay_cssim := + match goal with + | h : cssim ?L ?u ?v |- _ => __play_cssim_in h + | h : body (css ?L) ?R ?u ?v |- _ => __play_cssim_in h + end. + +Ltac __answer_cssim := ex2; split3; etrans. + +#[local] Tactic Notation "play" := __play_cssim. +#[local] Tactic Notation "play" "in" ident(H) := __play_cssim_in H. +#[local] Tactic Notation "eplay" := __eplay_cssim. +#[local] Tactic Notation "answer" := __answer_cssim. + Section cssim_homogenous_theory. Context {E B : Type -> Type} {X : Type} - {L: relation (@label E)}. + {L: lrel E E X X}. - Notation css := (@css E E B B X X). - Notation cssim := (@cssim E E B B X X). - - Lemma cssim_subrelation : forall (t t' : ctree E B X) L', - subrelation L L' -> cssim L t t' -> cssim L' t t'. - Proof. - intros. revert t t' H0. coinduction R CH. - intros. step in H0. simpl; split; intros; cbn in H0; destruct H0 as [H0' H0'']. - - cbn in H0'; apply H0' in H1 as (? & ? & ? & ? & ?); - apply H in H2. exists x, x0. auto. - - apply H0'' in H1 as (? & ? & ?). - do 2 eexists; apply H0. - Qed. + Notation css := (@css E E B B X X). + Notation cssim := (@cssim E E B B X X). (*| Various results on reflexivity and transitivity. |*) - #[global] Instance refl_csst {LR: Reflexive L} {C: Chain (css L)}: Reflexive `C. + #[global] Instance reflexive_css {R} + (LR: Reflexive L) + (RR: Reflexive R): Reflexive (css L R). Proof. - apply Reflexive_chain; cbn; eauto 9. + cbn; eauto 10. Qed. - #[global] Instance square_csst {LT: Transitive L} {C: Chain (css L)}: Transitive `C. + #[global] Instance reflexive_chain {LR: Reflexive L} {C: Chain (css L)}: Reflexive `C. Proof. - apply Transitive_chain. - cbn. intros ????? [xy xy'] [yz yz']. - split. - - intros ?? xx'. - destruct (xy _ _ xx') as (l' & y' & yy' & ? & ?). - destruct (yz _ _ yy') as (l'' & z' & zz' & ? & ?). - eauto 8. - - intros ?? xx'. - destruct (yz' _ _ xx') as (l'' & z' & zz'). - destruct (xy' _ _ zz') as (l' & y' & yy'). - eauto 8. + apply Reflexive_chain; typeclasses eauto. + Qed. + + #[global] Instance transitive_css {R} + (LT: Transitive L) + (RT: Transitive R): Transitive (css L R). + Proof. + intros x y z SS1 SS2. + play. + - play in SS1. + play in SS2. + answer. + - intros ns. + now apply SS2,SS1 in ns. + Qed. + + #[global] Instance transitive_chain {LT: Transitive L} {C: Chain (css L)}: Transitive `C. + Proof. + apply Transitive_chain; typeclasses eauto. Qed. - (*| PreOrder |*) - #[global] Instance PreOrder_csst {LPO: PreOrder L} {C: Chain (css L)}: PreOrder `C. - Proof. split; typeclasses eauto. Qed. + #[global] Instance css_ss_subrelation R : subrelation (css L R) (ss L R). + Proof. + red. + intros ?? [? ?]; auto. + Qed. #[global] Instance cssim_ssim_subrelation : subrelation (cssim L) (ssim L). Proof. @@ -154,18 +177,33 @@ End cssim_homogenous_theory. Section cssim_heterogenous_theory. Arguments label: clear implicits. - Context {E F C D: Type -> Type} {X Y: Type} - {L: rel (@label E) (@label F)}. + Context {E F C D: Type -> Type} {X Y: Type}. Notation css := (@css E F C D X Y). Notation cssim := (@cssim E F C D X Y). + Lemma cssim_mono : + Proper (sub_lrel ==> leq) cssim. + Proof. + cbn; intros * SUB. + coinduction R cih. + intros u v CSS. + remember CSS as TMP; clear HeqTMP; + step in TMP; destruct TMP as [HSS HPROG]. + split; auto. + intros l u' TR. + eplay. + ex2; split3; etrans. + eapply sub_lrel_subrel; eauto. + Qed. + + Context {L: lrel E F X Y}. (*| Strong simulation up-to [equ] is valid ---------------------------------------- |*) - Lemma equ_clos_csst {c: Chain (css L)}: + Lemma equ_clos_chain {c: Chain (css L)}: forall x y, equ_clos `c x y -> `c x y. Proof. apply tower. @@ -174,75 +212,80 @@ Section cssim_heterogenous_theory. econstructor; eauto. apply leq_infx in H. now apply H. - - intros a b ?? [x' y' x'' y'' EQ' [SIM COMP]]. - split; intros ?? tr. - + rewrite EQ' in tr. + - intros a b ?? [x' y' x'' y'' EQ' [SIM LIVE]]. + split. + + intros ?? tr. + rewrite EQ' in tr. edestruct SIM as (l' & ? & ? & ? & ?); eauto. exists l',x0; intuition. rewrite <- Equu; auto. - + rewrite <- Equu in tr. - edestruct COMP as (l' & ? & ?); eauto. + + intros ns. + rewrite <- Equu in ns. + edestruct LIVE as (l' & ? & ?); eauto. setoid_rewrite EQ'. eauto. Qed. - #[global] Instance equ_clos_csst_goal {c: Chain (css L)} : - Proper (equ eq ==> equ eq ==> flip impl) `c. - Proof. - cbn; intros ? ? eq1 ? ? eq2 H. - apply equ_clos_csst; econstructor; [eauto | | symmetry; eauto]; assumption. - Qed. - - #[global] Instance equ_clos_csst_ctx {c: Chain (css L)} : - Proper (equ eq ==> equ eq ==> impl) `c. - Proof. - cbn; intros ? ? eq1 ? ? eq2 H. - apply equ_clos_csst; econstructor; [symmetry; eauto | | eauto]; assumption. - Qed. - - #[global] Instance equ_css_closed_goal {r} : Proper (equ eq ==> equ eq ==> flip impl) (css L r). - Proof. - intros t t' tt' u u' uu'; cbn; intros [H H0]; split; intros l t0 TR. - - rewrite tt' in TR. destruct (H _ _ TR) as (? & ? & ? & ? & ?). - exists x, x0; auto; rewrite uu'; auto. - - rewrite uu' in TR. destruct (H0 _ _ TR) as (? & ? & ?). - exists x, x0; eauto; rewrite tt'; auto. - Qed. - - #[global] Instance equ_css_closed_ctx {r} : Proper (equ eq ==> equ eq ==> impl) (css L r). - Proof. - intros t t' tt' u u' uu'; cbn; intros [H H0]; split; intros l t0 TR. - - rewrite <- tt' in TR. destruct (H _ _ TR) as (? & ? & ? & ? & ?). - exists x, x0; auto; rewrite <- uu'; auto. - - rewrite <- uu' in TR. destruct (H0 _ _ TR) as (? & ? & ?). - exists x, x0; auto; rewrite <- tt'; auto. - Qed. - - Lemma is_stuck_css : forall (t: ctree E C X) (u: ctree F D Y) R, - css L R t u -> is_stuck t <-> is_stuck u. - Proof. - split; intros; intros ? ? ?. - - apply H in H1 as (? & ? & ?). now apply H0 in H1. - - apply H in H1 as (? & ? & ? & ? & ?). now apply H0 in H1. - Qed. - - Lemma is_stuck_cssim : forall (t: ctree E C X) (u: ctree F D Y), - t (⪅ L) u -> is_stuck t <-> is_stuck u. + #[global] Instance seq_chain_goal {c: Chain (css L)} : + Proper (Seq ==> Seq ==> flip impl) `c. Proof. - intros. step in H. eapply is_stuck_css; eauto. + apply tower. + - intros ? INC t t' HP' ? ? HP'' ?? HP'''. + red. + eapply INC; eauto. + apply leq_infx in HP'''. + now apply HP'''. + - intros ? INC t t' EQt u u' EQu [HS PROG]. + split. + now rewrite EQu, EQt. + intros ns. + rewrite EQu in ns. + edestruct PROG as (? & ? & ?); eauto. + ex2; rewrite EQt; eauto. Qed. - Lemma css_is_stuck : forall (t : ctree E C X) (u: ctree F D Y) R, - is_stuck t -> is_stuck u -> css L R t u. + #[global] Instance seq_css_goal {r} : + Proper (Seq ==> Seq ==> flip impl) (css L r). Proof. - split; intros. - - cbn. intros. now apply H in H1. - - now apply H0 in H1. + intros t t' tt' u u' uu'; cbn; intros [H1 H2]. + split; intros; auto. + - edestruct5 H1. + rewrite <- tt'; eauto. + ex2; split3; eauto. + now rewrite uu'. + - edestruct3 H2. + rewrite <- uu'; eauto. + ex2; rewrite tt'; eauto. Qed. - Lemma cssim_is_stuck : forall (t : ctree E C X) (u: ctree F D Y), - is_stuck t -> is_stuck u -> t (⪅ L) u. + #[global] Instance seq_chain_ctx {c: Chain (css L)} : + Proper (Seq ==> Seq ==> impl) `c. Proof. - intros. step. now apply css_is_stuck. + apply tower. + - intros ? INC t t' HP' ? ? HP'' ?? HP'''. + red. + eapply INC; eauto. + apply leq_infx in HP'''. + now apply HP'''. + - intros ? INC t t' EQt u u' EQu [HS PROG]; split. + now rewrite <- EQt, <- EQu. + intros ns. + rewrite <- EQu in ns. + edestruct PROG as (? & ? & ?); eauto. + ex2; rewrite <- EQt; eauto. + Qed. + + #[global] Instance seq_css_ctx {r} : + Proper (Seq ==> Seq ==> impl) (css L r). + Proof. + intros t t' tt' u u' uu'; cbn; intros [H1 H2]. + split; intros; auto. + - edestruct5 H1. + rewrite tt'; eauto. + ex2; split3; eauto. + now rewrite <- uu'. + - edestruct3 H2. + rewrite uu'; eauto. + ex2; rewrite <- tt'; eauto. Qed. Lemma cssim_ssim_subrelation_gen : forall x y, cssim L x y -> ssim L x y. @@ -255,6 +298,12 @@ Section cssim_heterogenous_theory. End cssim_heterogenous_theory. +#[global] Instance weq_ssim : forall {E F C D X Y}, + Proper (lequiv ==> weq) (@ssim E F C D X Y). +Proof. + cbn -[ss weq]. intros. apply gfp_weq. now apply lequiv_ss. +Qed. + (*| Up-to [bind] context simulations ---------------------------------- @@ -267,861 +316,752 @@ Section bind. Arguments label: clear implicits. Obligation Tactic := idtac. - Context {E F C D: Type -> Type} {X X' Y Y': Type} - (L : hrel (@label E) (@label F)) (R0 : rel X Y). - (*| Specialization of [bind_ctx] to a function acting with [cssim] on the bound value, and with the argument (pointwise) on the continuation. |*) Lemma bind_chain_gen - (RR : rel (label E) (label F)) - (ISVR : is_update_val_rel L R0 RR) - (HL: Respects_val RR) + {E F C D: Type -> Type} {X X' Y Y': Type} + (L : lrel E F X' Y') + (SS: rel X Y) {R : Chain (@css E F C D X' Y' L)} : - forall (t : ctree E C X) (t' : ctree F D Y) (k : X -> ctree E C X') (k' : Y -> ctree F D Y'), - cssim RR t t' -> - (forall x x', R0 x x' -> (elem R (k x) (k' x') /\ exists l t', trans l (k x) t')) -> - elem R (bind t k) (bind t' k'). + forall (t : ctree E C X) (t' : ctree F D Y) + (k : X -> ctree E C X') (k' : Y -> ctree F D Y'), + cssim (upd_rel L SS) t t' -> + (forall x y, SS x y -> ` R (k x) (k' y) /\ not_stuck (k x)) -> + ` R (bind t k) (bind t' k'). Proof. apply tower. + - intros ? INC ? ? ? ? tt' kk' ? ?. apply INC. apply H. apply tt'. intros x x' xx'. split. apply leq_infx in H. apply H. now apply kk'. edestruct kk'; eauto. + - intros ? ? ? ? ? ? tt' kk'. step in tt'. destruct tt' as [tt tt']. split. + + cbn; intros * STEP. - apply trans_bind_inv in STEP as [(?H & ?t' & STEP & EQ) | (v & STEPres & STEP)]. - * apply tt in STEP as (? & ? & ? & ? & ?). - do 2 eexists; split; [| split]. - apply trans_bind_l; eauto. - ++ intro Hl. destruct Hl. - apply ISVR in H3; etrans. - inversion H3; subst. apply H0. constructor. apply H5. constructor. - ++ rewrite EQ. - apply H. - apply H2. - intros * HR. - split. - now apply (b_chain x), kk'. - apply (kk' _ _ HR). - ++ apply ISVR in H3; etrans. - destruct H3. exfalso. apply H0. constructor. eauto. - * apply tt in STEPres as (u' & ? & STEPres & EQ' & ?). - apply ISVR in H0; etrans. - dependent destruction H0. - 2 : exfalso; apply H0; constructor. - pose proof (trans_val_inv STEPres) as EQ. - rewrite EQ in STEPres. - specialize (kk' v v2 H0). - apply kk' in STEP as (u'' & ? & STEP & EQ'' & ?); cbn in *. - do 2 eexists; split. + apply trans_bind_inv in STEP as [(?H & ?t' & STEP & EQ) | [(Z & e & EQl & g & STEP & SEQ) | (v & STEPres & STEP)]]. + + * subst l. + apply tt in STEP as (? & ? & STEP' & HSIM & HRL). + invL. + refine_trans. + ex2; split3. + ++ apply trans_bind_l_τ; eauto. + ++ rewrite EQ; apply H; auto. + intros. + edestruct4 kk'; eauto. + split; eauto. + step; auto. + ++ etrans. + + * subst l. + apply tt in STEP as (? & ? & STEP' & HSIM & HRL). + invL. + refine_trans. + exists (ask f); ex; split3; etrans. + rewrite SEQ. + step. + split. + { intros ?? TR. + pose proof trans_passive_inv' TR as (a & EQ & ->). + rewrite EQ in TR. + assert (TR': trans (rcv e a) (β e g) (g a)) by etrans. + step in HSIM; apply HSIM in TR' as (l' & u' & TR' & HSIM' & HRL'). + pose proof trans_passive_inv' TR' as (b & EQ' & ->). + exists (rcv f b); ex; split; eauto; split; cycle 1. + { invL; etrans. } + rewrite EQ. + apply H. + rewrite EQ' in HSIM'; auto. + intros. + edestruct4 kk'; eauto. + split; eauto. + now step. + } + { + step in HSIM. + destruct HSIM as [HSIM' PROD]. + intros (? & ? & TR). + pose proof trans_passive_inv' TR as (y & EQ & EQ'). + destruct PROD as (?l' & ?t' & ?TR'). + exists (rcv f y); eauto. + pose proof trans_passive_inv' TR' as (z & EQz & EQz'). + exists (rcv e z). + etrans. + } + + * apply tt in STEPres as (? & ? & STEP' & HSIM & HRL). + invL. + destruct (kk' v y) as [HSIM' HBACK']; [etrans |]. + apply HSIM' in STEP as (l' & u' & STEP'' & HSIM'' & HRL'). + exists l'; eexists; split; eauto. eapply trans_bind_r; eauto. - split; auto. - + cbn; intros * STEP. + erewrite <- trans_val_inv'; eauto. + + + intros (? & ? & STEP). apply trans_bind_inv_l in STEP as (l' & t2' & STEP). - apply tt' in STEP as (l'' & t1' & TR1). + destruct tt' as (l'' & ? & STEP'); eauto. destruct l''. - do 2 eexists; apply trans_bind_l; eauto; intros abs; inv abs. - do 2 eexists; apply trans_bind_l; eauto; intros abs; inv abs. - apply trans_val_invT in TR1 as ?. subst X0. - apply trans_val_inv in TR1 as ?. rewrite H0 in TR1. - pose proof TR1 as tmp. + refine_trans; ex2; apply trans_bind_l_τ; etrans. + refine_trans; ex2; eapply trans_bind_l_ask; etrans. + exfalso; eapply trans_rcv_active_inv; eauto. + + apply trans_val_invT in STEP' as ?. subst X0. + apply trans_val_inv' in STEP' as ?. rewrite H0 in STEP'. + pose proof STEP' as tmp. apply tt in tmp as (? & ? & TR & ? & ?). - assert (is_val x0) by (eapply HL; eauto; constructor). - inv H3; pose proof trans_val_invT TR; subst X0. - specialize (kk' v x2). - destruct kk'. - apply ISVR in H2; etrans. - dependent destruction H2; auto. exfalso; apply H2; constructor. - edestruct H4 as (? & ? & ?); eauto. - eapply trans_bind_r in H5; eauto. - Qed. + invL. + specialize (kk' v y). + destruct kk' as [HSIM' (l'' & ? & TR')]; auto. + ex2. + eapply trans_bind_r; etrans. -End bind. + Qed. (*| -Specializing the congruence principle for [⪅] +Specialization: equality on external calls, equality everywhere |*) -Lemma cssim_clo_bind_gen {E F C D: Type -> Type} {X Y X' Y': Type} {L : rel (@label E) (@label F)} - (R0 : rel X Y) L0 - (HL : is_update_val_rel L R0 L0) - (HLV : Respects_val L0) - (t1 : ctree E C X) (t2: ctree F D Y) - (k1 : X -> ctree E C X') (k2 : Y -> ctree F D Y'): - cssim L0 t1 t2 -> - (forall x y, R0 x y -> cssim L (k1 x) (k2 y)) -> - (forall x, exists l t', trans l (k1 x) t') -> - cssim L (t1 >>= k1) (t2 >>= k2). -Proof. - intros. - eapply bind_chain_gen; eauto. - split; eauto. - now apply H0. -Qed. - -Lemma cssim_clo_bind {E F C D: Type -> Type} {X Y X' Y': Type} {L : rel (@label E) (@label F)} - (R0 : rel X Y) - (t1 : ctree E C X) (t2: ctree F D Y) - (k1 : X -> ctree E C X') (k2 : Y -> ctree F D Y'): - Respects_val L -> - t1 (⪅update_val_rel L R0) t2 -> - (forall x y, R0 x y -> k1 x (⪅L) k2 y) -> - (forall x, exists l t', trans l (k1 x) t') -> - t1 >>= k1 (⪅L) t2 >>= k2. -Proof. - intros. - eapply bind_chain_gen. - 3:eauto. - eauto using update_val_rel_correct. - eauto using Respects_val_update_val_rel. - split; eauto. - now apply H1. -Qed. - -Lemma cssim_clo_bind_eq {E C D: Type -> Type} {X X': Type} - (t1 : ctree E C X) (t2: ctree E D X) - (k1 : X -> ctree E C X') (k2 : X -> ctree E D X'): - t1 ⪅ t2 -> - (forall x, k1 x ⪅ k2 x) -> - (forall x, exists l t', trans l (k1 x) t') -> - t1 >>= k1 ⪅ t2 >>= k2. -Proof. - intros. - eapply bind_chain_gen; eauto. - - apply update_val_rel_eq. - - apply Respects_val_eq. - - split; subst; auto. - apply H0. -Qed. - -Ltac __play_cssim := step; cbn; split; [intros ? ? ?TR | etrans]. - -Ltac __play_cssim_in H := - step in H; - cbn in H; edestruct H as [(? & ? & ?TR & ?EQ & ?HL) ?PROG]; - clear H; [etrans |]. - -Ltac __eplay_cssim := - match goal with - | h : @cssim ?E ?F ?C ?D ?X ?Y _ _ ?L |- _ => - __play_cssim_in h - end. - -#[local] Tactic Notation "play" := __play_cssim. -#[local] Tactic Notation "play" "in" ident(H) := __play_cssim_in H. -#[local] Tactic Notation "eplay" := __eplay_cssim. - -Section Proof_Rules. - Arguments label: clear implicits. - Context {E C : Type -> Type} {X: Type}. - - Lemma step_css_ret_gen {Y F D}(x : X) (y : Y) (R L : rel _ _) : - R Stuck Stuck -> - (Proper (equ eq ==> equ eq ==> impl) R) -> - L (val x) (val y) -> - css L R (Ret x : ctree E C X) (Ret y : ctree F D Y). + Lemma bind_chain E C D X Y X' Y' + (RR : rel X' Y') (SS : rel X Y) + {R : Chain (@css E E C D X' Y' (Lvrel RR))} : + forall (t1 : ctree E C X) (t2: ctree E D Y) + (k1 : X -> ctree E C X') (k2 : Y -> ctree E D Y'), + t1 (⪅[SS]) t2 -> + (forall x y, SS x y -> `R (k1 x) (k2 y) /\ not_stuck (k1 x)) -> + `R (t1 >>= k1) (t2 >>= k2). Proof. - intros Rstuck PROP Lval. - split. - cbn; intros ? ? TR; inv_trans; subst; - cbn; eexists; eexists; intuition; etrans; - now rewrite EQ. - intros; do 2 eexists; etrans. + intros. + eapply bind_chain_gen; eauto. Qed. - Lemma step_css_ret {Y F D} (x : X) (y : Y) (L : rel _ _) - {R : Chain (@css E F C D X Y L)} : - L (val x) (val y) -> - css L `R (Ret x : ctree E C X) (Ret y : ctree F D Y). + Lemma bind_chain_eq E C X X' + {R : Chain (@css E E C C X' X' Leq)} : + forall (t1 t2 : ctree E C X) + (k1 k2 : X -> ctree E C X'), + t1 ⪅ t2 -> + (forall x, `R (k1 x) (k2 x) /\ not_stuck (k1 x)) -> + `R (t1 >>= k1) (t2 >>= k2). Proof. intros. - apply step_css_ret_gen. - - apply (b_chain R). - split. - apply is_stuck_ss; apply Stuck_is_stuck. - intros * abs; apply trans_stuck_inv in abs; easy. - - typeclasses eauto. - - apply H. + eapply bind_chain_gen; eauto. + intros ??<-; auto. Qed. - Lemma step_css_ret_l_gen {Y F D} (x : X) (y : Y) (u u' : ctree F D Y) (L R : rel _ _) : - R Stuck Stuck -> - (Proper (equ eq ==> equ eq ==> impl) R) -> - L (val x) (val y) -> - trans (val y) u u' -> - css L R (Ret x : ctree E C X) u. +(*| +Specializations to the gfp +|*) + Lemma cssim_bind_gen E F C D X Y X' Y' + L (SS : rel X Y) + (t1 : ctree E C X) (t2: ctree F D Y) + (k1 : X -> ctree E C X') (k2 : Y -> ctree F D Y'): + t1 (⪅ upd_rel L SS) t2 -> + (forall x y, SS x y -> k1 x (⪅ L) k2 y /\ not_stuck (k1 x)) -> + t1 >>= k1 (⪅ L) t2 >>= k2. Proof. intros. - apply trans_val_inv in H2 as ?. - split. - - cbn. intros. - inv_trans. - subst; setoid_rewrite EQ. - etrans. - - intros. - do 2 eexists. - etrans. + eapply bind_chain_gen; eauto. Qed. - Lemma step_css_ret_l {Y F D} (x : X) (y : Y) (u u' : ctree F D Y) (L : rel _ _) - {R : Chain (@css E F C D X Y L)} : - L (val x) (val y) -> - trans (val y) u u' -> - css L ` R (Ret x : ctree E C X) u. + Lemma cssim_bind E C D X Y X' Y' + (RR : rel X' Y') (SS : rel X Y) + (t1 : ctree E C X) (t2: ctree E D Y) + (k1 : X -> ctree E C X') (k2 : Y -> ctree E D Y'): + t1 (⪅ [SS]) t2 -> + (forall x y, SS x y -> k1 x (⪅ [RR]) k2 y /\ not_stuck (k1 x)) -> + t1 >>= k1 (⪅ [RR]) t2 >>= k2. Proof. intros. - eapply step_css_ret_l_gen; eauto. - - apply (b_chain R). - split. - apply is_stuck_ss; apply Stuck_is_stuck. - intros * abs; apply trans_stuck_inv in abs; easy. - - typeclasses eauto. + eapply bind_chain_gen; eauto. Qed. - Lemma cssim_ret {Y F D} (x : X) (y : Y) (L : rel _ _) : - L (val x) (val y) -> - cssim L (Ret x : ctree E C X) (Ret y : ctree F D Y). + Lemma cssim_bind_eq {E C D: Type -> Type} {X X': Type} + (t1 : ctree E C X) (t2: ctree E D X) + (k1 : X -> ctree E C X') (k2 : X -> ctree E D X'): + t1 ⪅ t2 -> + (forall x, k1 x ⪅ k2 x /\ not_stuck (k1 x)) -> + t1 >>= k1 ⪅ t2 >>= k2. Proof. - intros. step. now apply step_css_ret. + intros. + eapply cssim_bind; eauto. + intros ?? ->; auto. Qed. +End bind. + (*| - The vis nodes are deterministic from the perspective of the labeled - transition system, stepping is hence symmetric and we can just recover - the itree-style rule. +And in particular, we can justify rewriting [⪅] to the left of a [bind]. + +NOTE: we shouldn't have to impose [eq] to the right. +|*) +#[global] Instance cssim_bind_chain {E C X Y} + {R : Chain (@css E E C C Y Y Leq)} : + Proper ((fun t u => cssim Leq (α t) (α u)) ==> + (pointwise_relation _ (fun t u => ` R (α t) (α u) /\ not_stuck t)) ==> `R) (@bind E C X Y). +Proof. + repeat intro; eapply bind_chain_gen; eauto. + intros ?? <-; auto. +Qed. + +Section Proof_Rules. + + Context {E F C D: Type -> Type} {X Y : Type}. + +(*| +Stuck ctrees can be simulated by anything. |*) - Lemma step_css_vis_gen {Y Z Z' F D} (e : E Z) (f: F Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (R L: rel _ _) : - inhabited Z -> - (Proper (equ eq ==> equ eq ==> impl) R) -> - (forall x, exists y, R (k x) (k' y) /\ L (obs e x) (obs f y)) -> - css L R (Vis e k) (Vis f k'). + + Lemma css_is_stuck L R : forall (t: @S E C X) (u: @S F D Y), + css L R t u -> is_stuck t <-> is_stuck u. Proof. - intros. - split. - - apply step_ss_vis_gen; auto. - - intros * tr; inv_trans; subst. - do 2 eexists. etrans. - Unshelve. - apply X0. + intros * [SIM LIVE]; split; intros IS ? ? TR. + - destruct LIVE as (? & ? & ?); eauto. now apply IS in H. + - apply SIM in TR as (? & ? & ? & ? & ?). now apply IS in H. Qed. - Lemma step_css_vis {Y Z Z' F D} (e : E Z) (f: F Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (L : rel _ _) - {R : Chain (@css E F C D X Y L)} : - inhabited Z -> - (forall x, exists y, ` R (k x) (k' y) /\ L (obs e x) (obs f y)) -> - css L ` R (Vis e k) (Vis f k'). + Lemma cssim_is_stuck L : forall (t: @S E C X) (u: @S F D Y), + t (⪅ L) u -> is_stuck t <-> is_stuck u. Proof. - intros * INH EQ. - apply step_css_vis_gen; auto. - typeclasses eauto. + intros. step in H. eapply css_is_stuck; eauto. Qed. - Lemma cssim_vis {Y Z Z' F D} (e : E Z) (f: F Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (L : rel _ _) : - inhabited Z -> - (forall x, exists y, cssim L (k x) (k' y) /\ L (obs e x) (obs f y)) -> - cssim L (Vis e k) (Vis f k'). + Lemma css_is_stuck' L R : forall (t : @S E C X) (u: @S F D Y), + is_stuck t -> is_stuck u -> css L R t u. Proof. - intros. step. apply step_css_vis; auto. + split; intros. + - cbn. intros. now apply H in H1. + - edestruct3 H1. now apply H0 in H2. Qed. - Lemma step_css_vis_id_gen {Y Z F D} (e : E Z) (f: F Z) - (k : Z -> ctree E C X) (k' : Z -> ctree F D Y) (R L: rel _ _) : - (Proper (equ eq ==> equ eq ==> impl) R) -> - (forall x, R (k x) (k' x) /\ L (obs e x) (obs f x)) -> - css L R (Vis e k) (Vis f k'). + Lemma cssim_is_stuck' L : forall (t : @S E C X) (u: @S F D Y), + is_stuck t -> is_stuck u -> t (⪅ L) u. Proof. - intros. - split. - - apply step_ss_vis_id_gen; auto. - - intros * tr; inv_trans; subst. - do 2 eexists. etrans. - Unshelve. apply x. + intros. step. now apply css_is_stuck'. Qed. - - Lemma step_css_vis_id {Y Z F D} (e : E Z) (f: F Z) - (k : Z -> ctree E C X) (k' : Z -> ctree F D Y) (L : rel _ _) + +(*| +Ret nodes +|*) + Lemma css_ret (x : X) (y : Y) L {R : Chain (@css E F C D X Y L)} : - (forall x, ` R (k x) (k' x) /\ L (obs e x) (obs f x)) -> - css L ` R (Vis e k) (Vis f k'). + RR L x y -> + css L `R (Ret x : ctree E C X) (Ret y : ctree F D Y). Proof. - intros * EQ. - apply step_css_vis_id_gen; auto. - typeclasses eauto. + intros HR; split. + - apply ss_ret_gen; auto. + step; eapply css_is_stuck'; apply stuck_is_stuck. + typeclasses eauto. + - eauto. Qed. - - Lemma cssim_vis_id {Y Z F D} (e : E Z) (f: F Z) - (k : Z -> ctree E C X) (k' : Z -> ctree F D Y) (L : rel _ _) : - (forall x, cssim L (k x) (k' x) /\ L (obs e x) (obs f x)) -> - cssim L (Vis e k) (Vis f k'). + + Lemma cssim_ret (x : X) (y : Y) L : + RR L x y -> + cssim L (Ret x : ctree E C X) (Ret y : ctree F D Y). Proof. - intros. step. now apply step_css_vis_id. + intros. + step. now apply css_ret. Qed. + (*| - Same goes for visible tau nodes. + The vis nodes are deterministic from the perspective of the labeled + transition system, stepping is hence symmetric and we can just recover + the itree-style rule. |*) - Lemma step_css_step_gen {Y F D} - (t : ctree E C X) (t': ctree F D Y) (R L: rel _ _): - (Proper (equ eq ==> equ eq ==> impl) R) -> - L τ τ -> - (R t t') -> - css L R (Step t) (Step t'). - Proof. - intros PR ? EQs. + Lemma css_vis {Z Z'} `{Inhabited Z} (e : E Z) (f: F Z') + (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) L + {R : Chain (@css E F C D X Y L)} + (HRask : Rask L e f) + (HRrcv : forall x, exists y, `R (k x) (k' y) /\ Rrcv L e f x y) : + css L ` R (Vis e k) (Vis f k'). + Proof. split. - - apply step_ss_step_gen; auto. - - intros * TR; inv_trans; subst; etrans. + - intros ?? TR; inv_trans. + ex2; intuition. + rewrite EQ. + step. + split. + + intros l u TR. + inv_trans; subst. + destruct (HRrcv x) as (y & ? & ?). + ex2; intuition. + rewrite EQ0; eauto. + etrans. + + unshelve eauto. + exact inhabitant. + - eauto. + Qed. + + Lemma cssim_vis {Z Z'} `{Inhabited Z} (e : E Z) (f: F Z') + (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) L + (HRask : Rask L e f) + (HRrcv : forall x, exists y, cssim L (k x) (k' y) /\ Rrcv L e f x y) : + cssim L (Vis e k) (Vis f k'). + Proof. + intros. step. apply css_vis; auto. Qed. - Lemma step_css_step {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L : rel _ _) - {R : Chain (@css E F C D X Y L)} : - (` R t t') -> - L τ τ -> - css L ` R (Step t) (Step t'). + (* Useful special case: over the same type return type, + we usually pick the identity *) + Lemma css_vis_id {Z} `{Inhabited Z} (e : E Z) (f: F Z) + (k : Z -> ctree E C X) (k' : Z -> ctree F D Y) L + {R : Chain (@css E F C D X Y L)} + (HRask : Rask L e f) + (HRrcv : forall z, ` R (k z) (k' z) /\ Rrcv L e f z z) : + css L ` R (Vis e k) (Vis f k'). Proof. - intros. - apply step_css_step_gen; auto. - typeclasses eauto. + eapply css_vis; eauto. Qed. - - Lemma cssim_step {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L : rel _ _) : - (cssim L t t') -> - L τ τ -> - cssim L (Step t) (Step t'). + + Lemma cssim_vis_id {Z} `{Inhabited Z} (e : E Z) (f : F Z) + (k : Z -> ctree E C X) (k' : Z -> ctree F D Y) L + (HRask : Rask L e f) + (HRrcv : forall x, cssim L (k x) (k' x) /\ Rrcv L e f x x) : + cssim L (Vis e k) (Vis f k'). Proof. - intros. - step. apply step_css_step; auto. + intros. step. now apply css_vis_id. Qed. + (*| - For invisible nodes, the situation is different: we may kill them, but that execution - cannot act as going under the guard. +Invisible nodes |*) - Lemma step_css_br_l_gen {Y F D Z} (c : C Z) - (k : Z -> ctree E C X) (t': ctree F D Y) (R L: rel _ _): - inhabited Z -> + (* Here we need a stronger lemma quantifying over arbitrary relations [R] and not just elements of the Chain in order to lift things to cssim as we don't unlock cssim in the structural subterm *) + Lemma css_br_l_gen {Z} `{Inhabited Z} (c : C Z) + (k : Z -> ctree E C X) (t': ctree F D Y) R L: (forall x, css L R (k x) t') -> css L R (Br c k) t'. Proof. - intros [? _] EQs. + intros EQs. split. - - apply step_ss_br_l_gen; auto. apply EQs. - - intros * TR. - unshelve edestruct EQs as [_ ?]; eauto. - apply H in TR. - destruct TR as (? & ? & ?). - etrans. + - apply ss_br_l_gen; intros z; destruct (EQs z); auto. + - intros NS. + destruct (EQs inhabitant) as [_ PROG]. + edestruct3 PROG; auto. + eauto. Qed. - Lemma step_css_br_l {Y F D Z} (c : C Z) - (k : Z -> ctree E C X) (t: ctree F D Y) (L: rel _ _) + Lemma css_br_l {Z} `{Inhabited Z} (c : C Z) + (k : Z -> ctree E C X) (t: ctree F D Y) L {R : Chain (@css E F C D X Y L)} : - inhabited Z -> - (forall x, css L (elem R) (k x) t) -> - css L ` R (Br c k) t. + (forall x, css L `R (k x) t) -> + css L `R (Br c k) t. Proof. - intros [? _] EQs. - split. - - apply step_ss_br_l_gen; auto. apply EQs. - - intros * TR. - unshelve edestruct EQs as [_ ?]; eauto. - apply H in TR. - destruct TR as (? & ? & ?). - etrans. + intros; now apply css_br_l_gen. Qed. - Lemma cssim_br_l {Y F D Z} (c : C Z) - (k : Z -> ctree E C X) (t: ctree F D Y) (L: rel _ _): - inhabited Z -> + Lemma cssim_br_l {Z} `{Inhabited Z} (c : C Z) + (k : Z -> ctree E C X) (t: ctree F D Y) L : (forall x, cssim L (k x) t) -> cssim L (Br c k) t. Proof. - intros. step. apply step_css_br_l_gen; auto. intros. - specialize (H x). step in H. apply H. + intros SIM; step; eapply css_br_l. + now intros z; specialize (SIM z); step in SIM. Qed. - (* This does not hold without assuming explicit progress on the left side. - Indeed, if [k x] is stuck, [t] would be stuck as well. - But then [Br c k] could be able to step, contradicting the completeness. - *) - Lemma step_css_br_r_gen {Y F D Z} (c : D Z) - (t : ctree E C X) (k : Z -> ctree F D Y) (R L: rel _ _) z : - (exists l t', trans l t t') -> - css L R t (k z) -> + Lemma css_br_r_gen {Z} (c : D Z) x + (k : Z -> ctree F D Y) (t: ctree E C X) R L: + (not_stuck t \/ not_stuck (k x)) -> + css L R t (k x) -> css L R t (Br c k). Proof. - intros TR [SIM COMP]. - split. - - eapply step_ss_br_r_gen; eauto. - - intros; auto. + cbn. intros NS [SIM PROG]; split. + - intros; edestruct5 SIM; eauto 10. + - destruct NS; auto. Qed. - Lemma step_css_br_r {Y F D Z} (c : D Z) x - (k : Z -> ctree F D Y) (t: ctree E C X) (L: rel _ _) - {R : Chain (@css E F C D X Y L)} : - (exists l t', trans l t t') -> - css L (elem R) t (k x) -> - css L ` R t (Br c k). + Lemma css_br_r {Z} (c : D Z) x + (k : Z -> ctree F D Y) (t: ctree E C X) L + {R : Chain (@css E F C D X Y L)} : + (not_stuck t \/ not_stuck (k x)) -> + css L `R t (k x) -> + css L `R t (Br c k). Proof. - intros TR SIM. - split. - - eapply step_ss_br_r_gen; apply SIM. - - auto. + apply css_br_r_gen. Qed. - Lemma cssim_br_r {Y F D Z} (c : D Z) x - (k : Z -> ctree F D Y) (t: ctree E C X) (L: rel _ _): - (exists l t', trans l t t') -> + Lemma cssim_br_r {Z} (c : D Z) x + (k : Z -> ctree F D Y) (t: ctree E C X) L : + (not_stuck t \/ not_stuck (k x)) -> cssim L t (k x) -> cssim L t (Br c k). Proof. - intros. step. - apply (@step_css_br_r_gen Y F D Z c t k (cssim L) L x); auto. - step in H0; auto. + intros. step. apply css_br_r_gen with (x := x); auto. + now step in H0. Qed. - Lemma step_css_br_gen {Y F D n m} (a: C n) (b: D m) - (k : n -> ctree E C X) (k' : m -> ctree F D Y) (R L : rel _ _) : - (exists x l t', trans l (k x) t') -> + Lemma css_br_gen {A B} (c: C A) (d: D B) + (k : A -> ctree E C X) (k' : B -> ctree F D Y) R L : + (exists x, not_stuck (k x)) -> (forall x, exists y, css L R (k x) (k' y)) -> - css L R (Br a k) (Br b k'). + css L R (Br c k) (Br d k'). Proof. - intros [? PROG] EQs. + intros [a NS] EQs. split. - - apply step_ss_br_gen; auto. intros y. destruct (EQs y). - exists x0; apply H. - - intros * TR. - destruct PROG as (? & ? & TR'). - do 2 eexists; econstructor; apply TR'. - Qed. - - Lemma step_css_br {Y F D n m} (cn: C n) (cm: D m) - (k : n -> ctree E C X) (k' : m -> ctree F D Y) (L : rel _ _) + - apply ss_br_l_gen. + intros x. + destruct (EQs x) as [x' ?]. + destruct H. + eapply ss_br_r_gen; eauto. + - intros NS'. + destruct NS as (? & ? & TR'). + ex2; eauto. + Qed. + + Lemma css_br {A B} (c: C A) (d: D B) + (k : A -> ctree E C X) (k' : B -> ctree F D Y) L {R : Chain (@css E F C D X Y L)} : - (exists x l t', trans l (k x) t') -> - (forall x, exists y, css L (elem R) (k x) (k' y)) -> - css L `R (Br cn k) (Br cm k'). + (exists x, not_stuck (k x)) -> + (forall x, exists y, css L `R (k x) (k' y)) -> + css L `R (Br c k) (Br d k'). Proof. - intros. - apply step_css_br_gen; auto. + apply css_br_gen. Qed. - Lemma cssim_br {Y F D n m} (cn: C n) (cm: D m) - (k : n -> ctree E C X) (k' : m -> ctree F D Y) (L : rel _ _) : - (exists x l t', trans l (k x) t') -> + Lemma cssim_br {A B} (c: C A) (d: D B) + (k : A -> ctree E C X) (k' : B -> ctree F D Y) L : + (exists x, not_stuck (k x)) -> (forall x, exists y, cssim L (k x) (k' y)) -> - cssim L (Br cn k) (Br cm k'). - Proof. - intros. step. apply step_css_br; auto. - intros. destruct (H0 x). step in H1. exists x0. apply H1. - Qed. - - Lemma step_css_br_id_gen {Y F D Z} (c: C Z) (d: D Z) - (k : Z -> ctree E C X) (k' : Z -> ctree F D Y) - (R L : rel _ _) : - (forall x, css L R (k x) (k' x)) -> - css L R (Br c k) (Br d k'). + cssim L (Br c k) (Br d k'). Proof. - intros EQs. - split. - - apply step_ss_br_id_gen; auto. intros y. destruct (EQs y). - apply H. - - intros * TR. - apply trans_br_inv in TR as [x TR]. - apply EQs in TR as (l' & t & TR). - do 2 eexists; econstructor; apply TR. + intros NS SIM. step. apply css_br_gen; auto. + intros. destruct (SIM x). step in H. eauto. Qed. - Lemma step_css_br_id {Y F D n} (c: C n) (d: D n) - (k : n -> ctree E C X) (k': n -> ctree F D Y) (L: rel _ _) + Lemma css_br_id {A} (c: C A) (d: D A) + (k : A -> ctree E C X) (k': A -> ctree F D Y) L {R : Chain (@css E F C D X Y L)} : - (forall x, css L (elem R) (k x) (k' x)) -> - css L ` R (Br c k) (Br d k'). + (exists x, not_stuck (k x)) -> + (forall x, css L `R (k x) (k' x)) -> + css L `R (Br c k) (Br d k'). Proof. - intros. - apply step_css_br_id_gen; eauto. + intros; apply css_br; eauto. Qed. - Lemma cssim_br_id {Y F D n} (c: C n) (d: D n) - (k : n -> ctree E C X) (k': n -> ctree F D Y) (L: rel _ _) : + Lemma cssim_br_id {A} (c: C A) (d: D A) + (k : A -> ctree E C X) (k': A -> ctree F D Y) L : + (exists x, not_stuck (k x)) -> (forall x, cssim L (k x) (k' x)) -> cssim L (Br c k) (Br d k'). Proof. - intros. step. apply step_css_br_id; eauto. - intros. apply (gfp_pfp (css L)). apply H. + intros. apply cssim_br; eauto. Qed. - Lemma step_css_guard_gen {Y F D} - (t: ctree E C X) (t': ctree F D Y) (R L: rel _ _): + Lemma css_guard_l_gen + (t: ctree E C X) (t': ctree F D Y) R L: css L R t t' -> - css L R (Guard t) (Guard t'). + css L R (Guard t) t'. Proof. - intros EQ. - split. - - apply step_ss_guard_gen; apply EQ. - - intros. - inv_trans. - apply EQ in H as (? & ? & ?). - etrans. + intros [SIM PROG]; split. + - apply ss_guard_l_gen; auto. + - intros NS; edestruct3 PROG; auto. + eauto. Qed. - Lemma step_css_guard_l {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _) + Lemma css_guard_l + (t: ctree E C X) (t': ctree F D Y) L {R : Chain (@css E F C D X Y L)} : css L `R t t' -> css L `R (Guard t) t'. Proof. - intros EQ. - split. - - intros ? ? TR; inv_trans; subst. - apply EQ in TR as (? & ? & TR' & ?). - eauto. - - intros. - apply EQ in H as (? & ? & ?). - etrans. + intros; now apply css_guard_l_gen. Qed. - Lemma step_css_guard_r {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _) - {R : Chain (@css E F C D X Y L)} : - css L `R t t' -> - css L `R t (Guard t'). + Lemma cssim_guard_l + (t: ctree E C X) (t': ctree F D Y) L: + cssim L t t' -> + cssim L (Guard t) t'. Proof. - intros EQ. - split. - - intros ? ? TR; inv_trans; subst. - apply EQ in TR as (? & ? & TR' & ?). - do 2 eexists; split; eauto. - etrans. - - intros. - inv_trans. - apply EQ in H as (? & ? & ?). - etrans. + intros; step; apply css_guard_l; step in H; auto. Qed. - Lemma step_css_guard {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _) - {R : Chain (@css E F C D X Y L)} : - css L `R t t' -> - css L `R (Guard t) (Guard t'). + Lemma css_guard_r_gen + (t: ctree E C X) (t': ctree F D Y) R L : + css L R t t' -> + css L R t (Guard t'). Proof. - intros. - now apply step_css_guard_gen. + intros [SIM PROG]; split. + - apply ss_guard_r_gen; auto. + - intros (? & ? & TR); inv_trans; destruct PROG; eauto. Qed. - Lemma cssim_guard_l {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _): - cssim L t t' -> - cssim L (Guard t) t'. + Lemma css_guard_r + (t: ctree E C X) (t': ctree F D Y) L + {R : Chain (@css E F C D X Y L)} : + css L `R t t' -> + css L `R t (Guard t'). Proof. - intros; step; apply step_css_guard_l; step in H; auto. + now apply css_guard_r_gen. Qed. - Lemma cssim_guard_r {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _): + Lemma cssim_guard_r + (t: ctree E C X) (t': ctree F D Y) L : cssim L t t' -> cssim L t (Guard t'). Proof. - intros; step; apply step_css_guard_r; step in H; auto. + intros; step; apply css_guard_r; step in H; auto. Qed. - Lemma cssim_guard {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _): + Lemma cssim_guard + (t: ctree E C X) (t': ctree F D Y) L : cssim L t t' -> cssim L (Guard t) (Guard t'). Proof. - intros; step; apply step_css_guard; step in H; auto. + intros. + now apply cssim_guard_l, cssim_guard_r. Qed. (*| - When matching visible brs one against another, in general we need to explain how - we map the branches from the left to the branches to the right. - A useful special case is the one where the arity coincide and we simply use the identity - in both directions. We can in this case have [n] rather than [2n] obligations. +Internal transitions |*) - Lemma step_css_brS_gen {Z Z' Y F D} (c : C Z) (d : D Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (R L: rel _ _) : - inhabited Z -> - (Proper (equ eq ==> equ eq ==> impl) R) -> - (forall x, exists y, R (k x) (k' y)) -> - L τ τ -> - css L R (BrS c k) (BrS d k'). - Proof. - intros INH HP REL HL. - eapply step_css_br_gen. - destruct INH as [z _]. - exists z; etrans. - intros. - specialize (REL x) as [y ?]. - exists y. - eapply step_css_step_gen; auto. + Lemma css_step + (t: ctree E C X) (t': ctree F D Y) L + {R : Chain (@css E F C D X Y L)} : + ` R t t' -> + css L ` R (Step t) (Step t'). + Proof. + intros HR; split. + - apply ss_step_gen; auto. + typeclasses eauto. + - eauto. + Qed. + + Lemma cssim_step + (t: ctree E C X) (t': ctree F D Y) L : + cssim L t t' -> + cssim L (Step t) (Step t'). + Proof. + now intros; step; apply css_step. Qed. - Lemma step_css_brS {Z Z' Y F D} (c : C Z) (c' : D Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (L: rel _ _) + Lemma css_brS {Z Z'} `{Inhabited Z} (c : C Z) (c' : D Z') + (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) L {R : Chain (@css E F C D X Y L)} : - inhabited Z -> - (forall x, exists y, `R (k x) (k' y)) -> - L τ τ -> - css L `R (BrS c k) (BrS c' k'). - Proof. - intros INH REL HL. - destruct INH as [z _]. - eapply step_css_br. - exists z; etrans. - intros x; specialize (REL x) as [y ?]. + (forall x, exists y, ` R (k x) (k' y)) -> + css L ` R (BrS c k) (BrS c' k'). + Proof. + intros * SIM. + eapply css_br. + exists inhabitant; eauto. + intros x; specialize (SIM x) as [y ?]. exists y. - eapply step_css_step; auto. + eapply css_step; auto. Qed. - Lemma cssim_brS {Z Z' Y F D} (c : C Z) (c' : D Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (L: rel _ _) : - inhabited Z -> + Lemma cssim_brS {Z Z'} `{Inhabited Z} (c : C Z) (c' : D Z') + (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) L : (forall x, exists y, cssim L (k x) (k' y)) -> - L τ τ -> cssim L (BrS c k) (BrS c' k'). Proof. - intros INH REL HL. - destruct INH as [z _]. - apply cssim_br. - exists z; etrans. - intros x; specialize (REL x) as [y ?]; exists y. - apply cssim_step; auto. - Qed. - - Lemma step_css_brS_id_gen {Z Y D F} (c : C Z) (d: D Z) - (k: Z -> ctree E C X) (k': Z -> ctree F D Y) (R L : rel _ _) : - (Proper (equ eq ==> equ eq ==> impl) R) -> - (forall x, R (k x) (k' x)) -> - L τ τ -> - css L R (BrS c k) (BrS d k'). - Proof. - intros HP REL HL. - split; [apply step_ss_brS_id_gen; auto |]. - intros. inv_trans. etrans. - Unshelve. apply x0. + now intros; step; apply css_brS. Qed. - Lemma step_css_brS_id {Z Y D F} (c : C Z) (d : D Z) - (k: Z -> ctree E C X) (k': Z -> ctree F D Y) (L : rel _ _) + Lemma css_brS_id {Z} `{Inhabited Z} (c : C Z) (d : D Z) + (k: Z -> ctree E C X) (k': Z -> ctree F D Y) L {R : Chain (@css E F C D X Y L)} : (forall x, `R (k x) (k' x)) -> - L τ τ -> - css L `R (BrS c k) (BrS d k'). + css L ` R (BrS c k) (BrS d k'). Proof. - intros REL HL. - apply step_css_brS_id_gen; auto. - typeclasses eauto. + intros; apply css_brS; eauto. Qed. - Lemma cssim_brS_id {Z Y D F} (c : C Z) (d : D Z) - (k: Z -> ctree E C X) (k': Z -> ctree F D Y) (L : rel _ _) : + Lemma cssim_brS_id {Z} `{Inhabited Z} (c : C Z) (d : D Z) + (k: Z -> ctree E C X) (k': Z -> ctree F D Y) L : (forall x, cssim L (k x) (k' x)) -> - L τ τ -> cssim L (BrS c k) (BrS d k'). Proof. - intros. step. apply step_css_brS_id; auto. + intros; apply cssim_brS; eauto. Qed. -End Proof_Rules. - -Section WithParams. - - Context {E F C D : Type -> Type}. - Context (L : rel (@label E) (@label F)). - (*| -Note that with visible schedules, nary-spins are equivalent only -if neither are empty, or if both are empty: they match each other's -tau challenge infinitely often. -With invisible schedules, they are always equivalent: neither of them -produce any challenge for the other. + Note that with visible schedules, an nary-spins refines another only + if it is empty, or if neither are empty. |*) - Lemma spinS_gen_nonempty : forall {Z Z' X Y} (c: C X) (c': D Y) (x: X) (y: Y) (L : rel _ _), - L τ τ -> - cssim L (@spinS_gen E C Z X c) (@spinS_gen F D Z' Y c'). + Lemma cssim_spinS_nonempty : + forall {Z Z'} L (x: Z) (y: Z') (c: C Z) (c': D Z'), + @cssim E F C D X Y L (spinS_gen c) (spinS_gen c'). Proof. - intros. - red. coinduction R CH. - simpl; split; intros l t' TR; rewrite ctree_eta in TR; cbn in TR; - apply trans_brS_inv in TR as (_ & EQ & ->); - do 2 eexists; - rewrite ctree_eta; cbn; intuition. - - econstructor; auto. - constructor; eauto. - - rewrite EQ; eauto. - - eapply H. - - econstructor; auto. - constructor; eauto. + intros until L; intros x y. + coinduction S CIH. + split. + - intros * ?? TR. + rewrite ctree_eta in TR; cbn in TR. + inv_trans. + ex2; split3; subst; etrans. + rewrite ctree_eta; cbn; etrans. + now rewrite EQ. + - intros. + rewrite ctree_eta; cbn. + eauto. Qed. (*| Inversion principles -------------------- +TODO: these principles are mirrored on ssim directly. We should be able to derive additional liveness information from them in some cases. |*) - Lemma cssim_ret_inv X Y (r1 : X) (r2 : Y) : - (Ret r1 : ctree E C X) (⪅L) (Ret r2 : ctree F D Y) -> + + Lemma cssim_stuck_inv L (t : ctree E C X) (u : ctree F D Y) + (CSS :@cssim E F C D X Y L t u) : + is_stuck t <-> is_stuck u. + Proof. + split. + - intros IS l u' TR. + step in CSS. + destruct CSS as [SS PROG]. + eapply not_stuck_is_stuck. + apply PROG. + eauto. + auto. + - intros IS l t' TR. + step in CSS. + apply CSS in TR. + edestruct5 TR. + eapply IS; eauto. + Qed. + + Lemma cssim_ret_l_inv L : + forall r (u : ctree F D Y) + (CSS : @cssim E F C D X Y L (Ret r) u), + exists r' u', trans (val r') u u' /\ RR L r r'. + Proof. + intros. step in CSS. + destruct CSS as [SIM PROG]. + edestruct5 SIM; etrans. + invL. + ex2; split; etrans. + Qed. + + Lemma cssim_ret_inv L (r1 : X) (r2 : Y) + (CSS : @cssim E F C D X Y L (Ret r1) (Ret r2)) : L (val r1) (val r2). Proof. - intros. eplay. - inv_trans. - now subst. + now inv_trans. Qed. - Lemma css_ret_l_inv {X Y R} : - forall r (u : ctree F D Y), - css L R (Ret r : ctree E C X) u -> - exists l' u', trans l' u u' /\ R Stuck u' /\ L (val r) l'. + Lemma cssim_vis_inv {X1 X2} L + (e : E X1) (f : F X2) + (k1 : X1 -> ctree E C X) (k2 : X2 -> ctree F D Y) + (CSS : cssim L (Vis e k1) (Vis f k2)) : + Rask L e f /\ + (forall x, exists y, Rrcv L e f x y /\ cssim L (k1 x) (k2 y)). Proof. - intros. apply H; etrans. - Qed. - - Lemma cssim_ret_l_inv {X Y} : - forall r (u : ctree F D Y), - cssim L (Ret r : ctree E C X) u -> - exists l' u', trans l' u u' /\ L (val r) l'. + eplay; inv_trans; invL. + split; auto. + intros x. + unshelve eplay. exact x. + invL. + inv_trans. + exists x1; split; eauto. + dependent induction EQl; eauto. + Qed. + + Lemma cssim_vis_l_inv {Z L} : + forall (e : E Z) (k : Z -> ctree E C X) u, + @cssim E F C D X Y L (Vis e k) u -> + exists Z' (f : F Z') k', + trans (ask f) u (β f k') /\ + Rask L e f /\ + forall x, exists y, cssim L (k x) (k' y) /\ Rrcv L e f x y. Proof. - intros. step in H. - apply css_ret_l_inv in H as (? & ? & ? & ? & ?). etrans. + intros. + eplay; invL; refine_trans. + ex3; split3; etrans. + intros z. + unshelve eplay; [eassumption |]; inv_trans; invL. + ex; split; etrans. Qed. - Lemma cssim_vis_inv_type {X Y X1 X2} - (e1 : E X1) (e2 : E X2) (k1 : X1 -> ctree E C X) (k2 : X2 -> ctree E D Y) (x1 : X1): - cssim eq (Vis e1 k1) (Vis e2 k2) -> - X1 = X2. + Lemma cssim_guard_l_inv L (t1 : ctree E C X) (t2 : ctree F D Y) : + cssim L (Guard t1) t2 -> + cssim L t1 t2. Proof. - intros. - step in H; cbn in H; destruct H as [SIM COMP]. - edestruct SIM as (? & ? & ? & ? & ?). - etrans. - inv_trans; subst; auto. - eapply obs_eq_invT; eauto. - Unshelve. - exact x1. + intros CSS; play. + - eplay. + ex2; split3; etrans. + - intros NS. + step in CSS; destruct CSS as [_ PROG]; edestruct3 PROG; eauto. + inv_trans; eauto. Qed. - Lemma cssbt_vis_inv {X Y X1 X2} - (e1 : E X1) (e2 : F X2) (k1 : X1 -> ctree E C X) (k2 : X2 -> ctree F D Y) (x : X1) - {R : Chain (@css E F C D X Y L)} : - css L (elem R) (Vis e1 k1) (Vis e2 k2) -> - (exists y, L (obs e1 x) (obs e2 y)) /\ (forall x, exists y, ` R (k1 x) (k2 y)). + Lemma cssim_guard_r_inv L (t1 : ctree E C X) (t2 : ctree F D Y) : + cssim L t1 (Guard t2) -> + cssim L t1 t2. Proof. - intros. - destruct H as [SIM COMP]. - split; intros; edestruct SIM as (? & ? & ? & ? & ?); - etrans; subst; - inv_trans; subst; eexists; auto. - - now eapply H1. - - now apply H0. + intros CSS; play. + - eplay; inv_trans. + ex2; split3; etrans. + - intros (? & ? & ?). + step in CSS; destruct CSS as [_ PROG]; edestruct3 PROG; eauto. Qed. - Lemma ssim_vis_inv {X Y X1 X2} - (e1 : E X1) (e2 : F X2) (k1 : X1 -> ctree E C X) (k2 : X2 -> ctree F D Y) (x : X1): - cssim L (Vis e1 k1) (Vis e2 k2) -> - (exists y, L (obs e1 x) (obs e2 y)) /\ (forall x, exists y, cssim L (k1 x) (k2 y)). + Lemma cssim_guard_inv L (t1 : ctree E C X) (t2 : ctree F D Y) : + cssim L (Guard t1) (Guard t2) -> + cssim L t1 t2. Proof. intros. - split. - - eplay. - inv_trans; subst; exists x2; eauto. - - intros y. - step in H. - cbn in H. - edestruct H as [(l' & u' & TR & IN & HL) ?]. - apply trans_vis with (x := y). - inv_trans. - eexists. - apply IN. + now apply cssim_guard_r_inv, cssim_guard_l_inv. Qed. - Lemma css_vis_l_inv {X Y Z R} : - forall (e : E Z) (k : Z -> ctree E C X) (u : ctree F D Y) x, - css L R (Vis e k) u -> - exists l' u', trans l' u u' /\ R (k x) u' /\ L (obs e x) l'. + Lemma cssim_br_l_inv L Z + (c: C Z) (t : ctree F D Y) (k : Z -> ctree E C X): + cssim L (Br c k) t -> + forall x, not_stuck (k x) -> cssim L (k x) t. Proof. - intros. apply H; etrans. + intros CSS ? NS; play. + eplay; eauto. Qed. - Lemma cssim_vis_l_inv {X Y Z} : - forall (e : E Z) (k : Z -> ctree E C X) (u : ctree F D Y) x, - cssim L (Vis e k) u -> - exists l' u', trans l' u u' /\ cssim L (k x) u' /\ L (obs e x) l'. + Lemma cssim_br_r_inv L Z + (d: D Z) (t : ctree E C X) (k : Z -> ctree F D Y): + cssim L t (Br d k) -> + forall l t', trans l t t' -> + exists x l' u', trans l' (k x) u' /\ + cssim L t' u' /\ + L l l'. Proof. - intros. step in H. - now simple apply css_vis_l_inv with (x := x) in H. + intros CSS * TR. + eplay; inv_trans. + ex3; split3; eauto. Qed. - Lemma cssim_brS_inv {X Y} - n m (cn: C n) (cm: D m) (k1 : n -> ctree E C X) (k2 : m -> ctree F D Y) : - cssim L (BrS cn k1) (BrS cm k2) -> - (forall i1, exists i2, cssim L (k1 i1) (k2 i2)). + Lemma cssim_step_inv L (t1 : ctree E C X) (t2 : ctree F D Y) : + cssim L (Step t1) (Step t2) -> + cssim L t1 t2. Proof. - intros EQ i1. - eplay. - subst; inv_trans. - eexists; eauto. + intros; eplay; inv_trans; etrans. Qed. - Lemma css_brS_l_inv {X Y Z R} : - forall (c : C Z) (k : Z -> ctree E C X) (u : ctree F D Y) x, - css L R (BrS c k) u -> - exists l' u', trans l' u u' /\ R (k x) u' /\ L τ l'. + Lemma cssim_step_l_inv L (t1 : ctree E C X) (t2 : ctree F D Y) : + cssim L (Step t1) t2 -> + exists t2', trans τ t2 t2' /\ cssim L t1 t2'. Proof. - intros. apply H; etrans. + intros; eplay; invL; refine_trans. + ex; split; etrans. Qed. - Lemma cssim_brS_l_inv {X Y Z} : - forall (c : C Z) (k : Z -> ctree E C X) (u : ctree F D Y) x, - cssim L (BrS c k) u -> - exists l' u', trans l' u u' /\ cssim L (k x) u' /\ L τ l'. + Lemma cssim_brS_inv L + A B (c: C A) (d: D B) (k1 : A -> ctree E C X) (k2 : B -> ctree F D Y) : + cssim L (BrS c k1) (BrS d k2) -> + forall i1, exists i2, cssim L (k1 i1) (k2 i2). Proof. - intros. step in H. - now simple apply css_brS_l_inv with (x := x) in H. + intros EQ i1. + eplay; invL; inv_trans; eauto. Qed. - Lemma css_br_l_inv {X Y} - n (c: C n) (t : ctree F D Y) (k : n -> ctree E C X) R: - css L R (Br c k) t -> - forall x, - (exists l' t', trans l' (k x) t') -> - css L R (k x) t. + Lemma cssim_brS_l_inv L + A (c: C A) (k1 : A -> ctree E C X) (t2 : ctree F D Y) : + cssim L (BrS c k1) t2 -> + forall i, exists t2', trans τ t2 t2' /\ cssim L (k1 i) t2'. Proof. - cbn. intros [? ?] * PROG; split; intros * TR. - - eapply trans_br in TR; [| reflexivity]. - apply H in TR as (? & ? & ? & ? & ?); subst. - eauto. - - apply PROG. - Qed. - - Lemma cssim_br_l_inv {X Y} - n (c: C n) (t : ctree F D Y) (k : n -> ctree E C X): - cssim L (Br c k) t -> - forall x, - (exists l' t', trans l' (k x) t') -> - cssim L (k x) t. - Proof. - intros. step. step in H. eapply css_br_l_inv; eauto. + intros EQ i1. + eplay; invL; inv_trans; eauto. Qed. - (* This one isn't very convenient... *) - Lemma cssim_br_r_inv {X Y} - n (c: D n) (t : ctree E C X) (k : n -> ctree F D Y): - cssim L t (Br c k) -> - forall l t', trans l t t' -> - exists l' x t'' , trans l' (k x) t'' /\ L l l' /\ (cssim L t' t''). - Proof. - cbn. intros. step in H. apply H in H0 as (? & ? & ? & ? & ?); subst. inv_trans. - do 3 eexists; eauto. - Qed. +End Proof_Rules. -End WithParams. diff --git a/theories/Eq/SBisim.v b/theories/Eq/SBisim.v index 9665d34..640e953 100644 --- a/theories/Eq/SBisim.v +++ b/theories/Eq/SBisim.v @@ -70,9 +70,6 @@ Import CTree. Import CTreeNotations. Import EquNotations. -(* TODO: Decide where to set this *) -Arguments trans : simpl never. - (*| Strong Bisimulation ------------------- @@ -83,33 +80,29 @@ Relation relaxing [equ] to become insensitive to: Section StrongBisim. Context {E F C D : Type -> Type} {X Y : Type}. - Notation S := (ctree E C X). - Notation S' := (ctree F D Y). (*| In the heterogeneous case, the relation is not symmetric. |*) - Program Definition sb L : mon (S -> S' -> Prop) := - {| body R t u := ss L R t u /\ ss (flip L) (flip R) u t |}. + Program Definition sb L : mon (@S E C X -> @S F D Y -> Prop) := + {| body R t u := ss L R t u /\ ss (flipL L) (flip R) u t |}. Next Obligation. split; intros; [edestruct H0 as (? & ? & ?) | edestruct H1 as (? & ? & ?)]; eauto; eexists; eexists; intuition; eauto. Qed. - #[global] Instance Lequiv_sb_goal : - Proper (Lequiv X Y ==> leq) sb. - Proof. - cbn -[sb]. split. - - destruct H0 as [? _]. eapply Lequiv_ss_goal. apply H. apply H0. - - destruct H0 as [_ ?]. eapply Lequiv_ss_goal with (x := flip x). - red. cbn. intros. now apply H. apply H0. - Qed. - - #[global] Instance weq_sb : - Proper (weq ==> weq) sb. + #[global] Instance lequiv_sb : + Proper (lequiv ==> weq) sb. Proof. - cbn -[weq]. split; intro. - - eapply Lequiv_sb_goal. apply weq_Lequiv. apply H. auto. - - eapply Lequiv_sb_goal. apply weq_Lequiv. symmetry. apply H. auto. + cbn -[sb]. intros * EQ *; split. + - intros [For Bac]; split. + eapply lequiv_ss in EQ. + now apply EQ in For. + eapply lequiv_ss; [| eauto]. + now apply lequiv_flipL. + - intros [For Bac]; split. + eapply lequiv_ss; eauto. + eapply lequiv_ss; [| eauto]. + now apply lequiv_flipL. Qed. End StrongBisim. @@ -117,51 +110,47 @@ End StrongBisim. Definition sbisim {E F C D X Y} L := (gfp (@sb E F C D X Y L) : hrel _ _). -#[global] Instance Lequiv_sbisim : forall {E F C D X Y}, - Proper (Lequiv X Y ==> leq) (@sbisim E F C D X Y). -Proof. - cbn. intros. - - unfold sbisim. - epose proof (gfp_leq (x := sb x) (y := sb y)). lapply H1. - + intro. red in H2. cbn in H2. apply H2. apply H0. - + now rewrite H. -Qed. - -#[global] Instance weq_sbisim : forall {E F C D X Y}, - Proper (weq ==> weq) (@sbisim E F C D X Y). -Proof. - cbn -[ss weq]. intros. apply gfp_weq. now apply weq_sb. -Qed. - -(* This instance allows to use the symmetric tactic from coq-coinduction - for homogeneous bisimulations *) -#[global] Instance sbisim_sym {E C X L} : - Symmetric L -> - Symmetrical converse (@sb E E C C X X L) (@ss E E C C X X L). -Proof. - intros SYM. split; intro. - - destruct H. split. - + apply H. - + cbn. intros. apply H0 in H1 as (? & ? & ? & ? & ?). apply SYM in H3. eauto. - - destruct H. split. - + apply H. - + cbn. intros. apply H0 in H1 as (? & ? & ? & ? & ?). apply SYM in H3. eauto. -Qed. - Module SBisimNotations. (*| sb (bisimulation) notation |*) Notation "t ~ u" := (sbisim eq t u) (at level 70). + Notation "t (~ [ Q ] ) u" := (sbisim (Lvrel Q) t u) (at level 79). Notation "t (~ L ) u" := (sbisim L t u) (at level 70). Notation "t {{ ~ L }} u" := (sb L _ t u) (at level 79). + Notation "t '{{~' [ R ] '}}' u" := (sb (Lvrel R) (` _) t u) (at level 90, only printing). Notation "t {{~}} u" := (sb eq _ t u) (at level 79). End SBisimNotations. Import SBisimNotations. +(* This instance allows to use the symmetric tactic from coq-coinduction + for homogeneous bisimulations *) +#[global] Instance sbisim_sym {E C X L} : + Symmetric L -> + Symmetrical converse (@sb E E C C X X (Lvrel L)) (@ss E E C C X X (Lvrel L)). +Proof. + intros SYM. intros RR u v. split; intros HSIM. + - destruct HSIM as [F B]. split. + + apply F. + + cbn. intros l v' TR. + apply B in TR as (l' & u' & TR & HR & HR'). + ex2; split3; eauto. + symmetry. + pose proof flipL_flip (Lvrel L) l l' as G. + now apply G. + - destruct HSIM as [F B]. split. + + apply F. + + intros l v' TR. + apply B in TR as (l' & u' & TR & HR & HR'). + ex2; split3; eauto. + pose proof flipL_flip (Lvrel L) l l' as G. + apply G. + now symmetry. +Qed. + Ltac fold_sbisim := repeat match goal with @@ -192,6 +181,174 @@ Tactic Notation "__coinduction_sbisim" simple_intropattern(r) simple_intropatter #[local] Tactic Notation "coinduction" simple_intropattern(r) simple_intropattern(cih) := __coinduction_sbisim r cih || __coinduction_cssim r cih || __coinduction_ssim r cih || coinduction r cih. +Ltac __play_sbisim := (try step); split; cbn; intros ? ? ?TR. + +Ltac __playL_sbisim H := + (try step in H); + let Hf := fresh "Hf" in + destruct H as [Hf _]; + cbn in Hf; edestruct Hf as (? & ? & ?TR & ?EQ & ?); + clear Hf; subst; [etrans |]. + +Ltac __eplayL_sbisim := + match goal with + | h : @sbisim ?E _ ?C _ ?X _ ?RR _ _ |- _ => + __playL_sbisim h + | h : body (sb ?L) ?R _ _ |- _ => + __playL_sbisim h + end. + +Ltac __playR_sbisim H := + try (step in H); + let Hb := fresh "Hb" in + destruct H as [_ Hb]; + cbn in Hb; edestruct Hb as (? & ? & ?TR & ?EQ & ?); + clear Hb; subst; [etrans |]. + +Ltac __eplayR_sbisim := + match goal with + | h : @sbisim ?E _ ?C _ ?X _ ?RR _ _ |- _ => + __playR_sbisim h + | h : body (sb ?L) ?R _ _ |- _ => + __playR_sbisim h + end. + +Ltac __answer_sbisim := ex2; split3; etrans. + +#[local] Tactic Notation "play" := __play_sbisim. +#[local] Tactic Notation "playL" "in" ident(H) := __playL_sbisim H. +#[local] Tactic Notation "playR" "in" ident(H) := __playR_sbisim H. +#[local] Tactic Notation "play" "in" ident(H) := first [playL in H; [] | playR in H; []]. +#[local] Tactic Notation "eplayL" := __eplayL_sbisim. +#[local] Tactic Notation "eplayR" := __eplayR_sbisim. +#[local] Tactic Notation "eplay" := first [eplayL; [] | eplayR; []]. +#[local] Tactic Notation "answer" := __answer_sbisim. + +Section sbisim_homogenous_theory. + Context {E B: Type -> Type} {X: Type} {L: lrel E E X X}. + + Notation sb := (@sb E E B B X X). + + #[global] Instance reflexive_sb {R} + (LR: Reflexive L) + (RR: Reflexive R): Reflexive (sb L R). + Proof. + split. reflexivity. + cbn; eauto 10. + Qed. + + #[global] Instance reflexive_chain {LR: Reflexive L} {C: Chain (sb L)}: Reflexive `C. + Proof. + apply Reflexive_chain; typeclasses eauto. + Qed. + + #[global] Instance symmetric_sb {R} + (LS : Symmetric L) + (RS : Symmetric R) : + Symmetric (sb L R). + Proof. + intros u v SB. + play; eplay. + answer; now apply flipL_flip. + answer; now apply flipL_flip. + Qed. + + #[global] Instance symmetric_chain {LR: Symmetric L} {C: Chain (sb L)}: Symmetric `C. + Proof. + apply Symmetric_chain; typeclasses eauto. + Qed. + + #[global] Instance transitive_sb {R} + (LT: Transitive L) + (RT: Transitive R): Transitive (sb L R). + Proof. + intros x y z SS1 SS2. + play. + - play in SS1; play in SS2; answer. + - play in SS2; play in SS1; answer. + apply (flipL_flip L) in H,H0; apply flipL_flip; cbn in *; eauto. + Qed. + + #[global] Instance transitive_chain {LT: Transitive L} {C: Chain (sb L)}: Transitive `C. + Proof. + apply Transitive_chain; typeclasses eauto. + Qed. + + (*| Equivalence |*) + #[global] Instance equivalence_sb {R} + (LE : Equivalence L) + (RE : Equivalence R) : Equivalence (sb L R). + Proof. split; typeclasses eauto. Qed. + + #[global] Instance equivalence_chain {LE: Equivalence L} {C: Chain (sb L)}: Equivalence `C. + Proof. split; typeclasses eauto. Qed. + +End sbisim_homogenous_theory. + +(* Section Homogeneous. *) + +(* Context {E C: Type -> Type} {X: Type} *) +(* {L: rel (@label E) (@label E)}. *) +(* Notation ss := (@ss E E C C X X). *) +(* Notation ssim := (@ssim E E C C X X). *) + +(* #[global] Instance sbisim_clos_ssim_goal `{Symmetric _ L} `{Transitive _ L} : *) +(* Proper (sbisim L ==> sbisim L ==> flip impl) (ssim L). *) +(* Proof. *) +(* repeat intro. *) +(* transitivity y0. transitivity y. *) +(* - now apply sbisim_ssim_subrelation in H1. *) +(* - now exact H3. *) +(* - symmetry in H2; now apply sbisim_ssim_subrelation in H2. *) +(* Qed. *) + +(* #[global] Instance sbisim_clos_ssim_ctx `{Equivalence _ L}: *) +(* Proper (sbisim L ==> sbisim L ==> impl) (ssim L). *) +(* Proof. *) +(* repeat intro. symmetry in H0, H1. eapply sbisim_clos_ssim_goal; eauto. *) +(* Qed. *) + +(* End Homogeneous. *) + +Section VRel. + Context {E B: Type -> Type} {X Y: Type} {RR: rel X Y}. +(*| +Hence [equ eq] is a included in [sbisim] +|*) + +(* TODO: Generalize SEQ to take a relation on values as argument *) +Lemma foo u v : + SeqR RR u v -> + @sbisim E E B B X Y (Lvrel RR) u v. +Proof. + intros SEQ. + dependent induction SEQ. + - rewrite EQ. + +#[global] Instance equ_sbisim_subrelation {X Y} (RR : rel X Y) : subrelation (SeqR RR) (sbisim (Lvrel RR)). + Proof. + red; intros. + rewrite H; reflexivity. + Qed. + + #[global] Instance is_stuck_sbisim : Proper (sbisim L ==> flip impl) is_stuck. + Proof. + cbn. intros ???????. + step in H. destruct H as [? _]. + apply H in H1 as (? & ? & ? & ? & ?). now apply H0 in H1. + Qed. + + #[global] Instance sbisim_cssim_subrelation : subrelation (sbisim L) (cssim L). + Proof. + red; apply sbisim_cssim_subrelation_gen. + Qed. + + #[global] Instance sbisim_ssim_subrelation : subrelation (sbisim L) (ssim L). + Proof. + red; apply sbisim_ssim_subrelation_gen. + Qed. + + (*| This section should describe lemmas proved for the heterogenous version of `css`, parametric on @@ -339,82 +496,6 @@ stuck ctrees can be simulated by anything. End sbisim_heterogenous_theory. -Section sbisim_homogenous_theory. - Context {E B: Type -> Type} {X: Type} (L: relation (@label E)). - - Notation sb := (@sb E E B B X X). - Notation sbisim := (@sbisim E E B B X X). - - #[global] Instance refl_sb {LR: Reflexive L} {C: Chain (sb L)}: Reflexive `C. - Proof. - apply Reflexive_chain. - cbn; intros; split; intros * TR; do 2 eexists; eauto. - Qed. - - #[global] Instance sb_sym {R} : - Symmetric L -> - Symmetric R -> - Symmetric (sb L R). - Proof. - intros SYM SYM'. split; cbn; intros. - - destruct H as [_ ?]. cbn in H. - apply H in H0 as (? & ? & ? & ? & ?). eauto 7. - - destruct H as [? _]. cbn in H. - apply H in H0 as (? & ? & ? & ? & ?). eauto 7. - Qed. - - #[global] Instance sym_sb {LT: Symmetric L} {C: Chain (sb L)}: Symmetric `C. - Proof. - apply Symmetric_chain. - cbn; intros * HS * [fwd bwd]; split; intros ?? TR. - - destruct (bwd _ _ TR) as (l' & y' & yy' & ? & ?); eauto 8. - - destruct (fwd _ _ TR) as (l' & y' & yy' & ? & ?); eauto 8. - Qed. - - #[global] Instance square_sb {LT: Transitive L} {C: Chain (sb L)}: Transitive `C. - Proof. - apply Transitive_chain. - cbn. intros ????? [xy xy'] [yz yz']; split; intros ?? xx'. - - destruct (xy _ _ xx') as (l' & y' & yy' & ? & ?). - destruct (yz _ _ yy') as (l'' & z' & zz' & ? & ?). - eauto 8. - - destruct (yz' _ _ xx') as (l' & y' & yy' & ? & ?). - destruct (xy' _ _ yy') as (l'' & z' & zz' & ? & ?). - eauto 8. - Qed. - -(*| PreOrder |*) - #[global] Instance Equivalence_sb {LPO: Equivalence L} {C: Chain (sb L)}: Equivalence `C. - Proof. split; typeclasses eauto. Qed. - -(*| -Hence [equ eq] is a included in [sbisim] -|*) - #[global] Instance equ_sbisim_subrelation `{EqL: Equivalence _ L} : subrelation (equ eq) (sbisim L). - Proof. - red; intros. - rewrite H; reflexivity. - Qed. - - #[global] Instance is_stuck_sbisim : Proper (sbisim L ==> flip impl) is_stuck. - Proof. - cbn. intros ???????. - step in H. destruct H as [? _]. - apply H in H1 as (? & ? & ? & ? & ?). now apply H0 in H1. - Qed. - - #[global] Instance sbisim_cssim_subrelation : subrelation (sbisim L) (cssim L). - Proof. - red; apply sbisim_cssim_subrelation_gen. - Qed. - - #[global] Instance sbisim_ssim_subrelation : subrelation (sbisim L) (ssim L). - Proof. - red; apply sbisim_ssim_subrelation_gen. - Qed. - -End sbisim_homogenous_theory. - (*| Up-to [bind] context bisimulations ---------------------------------- @@ -642,40 +723,6 @@ Proof. intros. eapply vis_chain_gen with (left := fun x => x) (right := fun x => x); auto. Qed. -Ltac __play_sbisim := step; split; cbn; intros ? ? ?TR. - -Ltac __playL_sbisim H := - step in H; - let Hf := fresh "Hf" in - destruct H as [Hf _]; - cbn in Hf; edestruct Hf as (? & ? & ?TR & ?EQ & ?); - clear Hf; subst; [etrans |]. - -Ltac __eplayL_sbisim := - match goal with - | h : @sbisim ?E _ ?C _ ?X _ ?RR _ _ |- _ => - __playL_sbisim h - end. - -Ltac __playR_sbisim H := - step in H; - let Hb := fresh "Hb" in - destruct H as [_ Hb]; - cbn in Hb; edestruct Hb as (? & ? & ?TR & ?EQ & ?); - clear Hb; subst; [etrans |]. - -Ltac __eplayR_sbisim := - match goal with - | h : @sbisim ?E _ ?C _ ?X _ ?RR _ _ |- _ => - __playR_sbisim h - end. - -#[local] Tactic Notation "play" := __play_sbisim. -#[local] Tactic Notation "playL" "in" ident(H) := __playL_sbisim H. -#[local] Tactic Notation "playR" "in" ident(H) := __playR_sbisim H. -#[local] Tactic Notation "eplayL" := __eplayL_sbisim. -#[local] Tactic Notation "eplayR" := __eplayR_sbisim. - (*| Proof rules for [~] @@ -1614,31 +1661,6 @@ Section StrongSimulations. End Heterogeneous. - Section Homogeneous. - - Context {E C: Type -> Type} {X: Type} - {L: rel (@label E) (@label E)}. - Notation ss := (@ss E E C C X X). - Notation ssim := (@ssim E E C C X X). - - #[global] Instance sbisim_clos_ssim_goal `{Symmetric _ L} `{Transitive _ L} : - Proper (sbisim L ==> sbisim L ==> flip impl) (ssim L). - Proof. - repeat intro. - transitivity y0. transitivity y. - - now apply sbisim_ssim_subrelation in H1. - - now exact H3. - - symmetry in H2; now apply sbisim_ssim_subrelation in H2. - Qed. - - #[global] Instance sbisim_clos_ssim_ctx `{Equivalence _ L}: - Proper (sbisim L ==> sbisim L ==> impl) (ssim L). - Proof. - repeat intro. symmetry in H0, H1. eapply sbisim_clos_ssim_goal; eauto. - Qed. - - End Homogeneous. - Section two_ss_is_not_sb. Lemma split_sb_eq : forall {E C X} RR diff --git a/theories/Eq/SSim.v b/theories/Eq/SSim.v index 289a129..52226bc 100644 --- a/theories/Eq/SSim.v +++ b/theories/Eq/SSim.v @@ -24,9 +24,6 @@ Import CoindNotations. Import CTree. Set Implicit Arguments. -(* TODO: Decide where to set this *) -Arguments trans : simpl never. - Section StrongSim. (*| The function defining strong simulations: [trans] plays must be answered @@ -37,23 +34,25 @@ Pous'16 in order to be able to exploit symmetry arguments in proofs (see [square_st] for an illustration). |*) Program Definition ss {E F C D : Type -> Type} {X Y : Type} - (L : rel (@label E) (@label F)) : - mon (ctree E C X -> ctree F D Y -> Prop) := - {| body R t u := - forall l t', trans l t t' -> exists l' u', trans l' u u' /\ R t' u' /\ L l l' + (L : lrel E F X Y) : + mon (@S E C X -> @S F D Y -> Prop) := + {| body R t u := forall l t', trans l t t' -> + exists l' u', trans l' u u' /\ R t' u' /\ L l l' |}. Next Obligation. - edestruct H0 as (u' & l' & ?); eauto. - eexists; eexists; intuition; eauto. + edestruct3 H0; eauto. + ex2; intuition; eauto. Qed. - #[global] Instance weq_ss : forall {E F C D X Y}, Proper (weq ==> weq) (@ss E F C D X Y). + #[global] Instance lequiv_ss : forall {E F C D X Y}, Proper (lequiv ==> weq) (@ss E F C D X Y). Proof. - cbn. intros. split. - - intros. apply H0 in H1 as (? & ? & ? & ? & ?). - exists x0, x1. intuition. now apply H. - - intros. apply H0 in H1 as (? & ? & ? & ? & ?). - exists x0, x1. intuition. now apply H. + cbn. intros * EQ *. split. + - intros. apply H in H0 as (? & ? & ? & ? & ?). + ex2; split3; eauto. + now rewrite <- EQ. + - intros. apply H in H0 as (? & ? & ? & ? & ?). + ex2; split3; eauto. + now rewrite EQ. Qed. End StrongSim. @@ -61,13 +60,17 @@ End StrongSim. Definition ssim {E F C D X Y} L := (gfp (@ss E F C D X Y L): hrel _ _). +(* TODO : TESTER LVREL COERCION *) Module SSimNotations. - Infix "≲" := (ssim eq) (at level 70). + Infix "≲" := (ssim Leq) (at level 70). + Notation "t (≲ [ Q ] ) u" := (ssim (Lvrel Q) t u) (at level 79). Notation "t (≲ Q ) u" := (ssim Q t u) (at level 79). - Notation "t '[≲' R ']' u" := (ss R (` _) t u) (at level 90, only printing). - Notation "t '[≲]' u" := (ss eq (` _) t u) (at level 90, only printing). + Notation "t '[≲]' u" := (ss Leq (` _) t u) (at level 90, only printing). + Notation "t '[≲' [ R ] ']' u" := (ss (Lvrel R) (` _) t u) (at level 90, only printing). + Notation "t '[≲' R ']' u" := (ss R (` _) t u) (at level 90, only printing). + End SSimNotations. Import SSimNotations. @@ -106,51 +109,97 @@ Tactic Notation "__coinduction_ssim" simple_intropattern(r) simple_intropattern( first [unfold ssim at 4 | unfold ssim at 3 | unfold ssim at 2 | unfold ssim at 1]; coinduction r cih. #[local] Tactic Notation "coinduction" simple_intropattern(r) simple_intropattern(cih) := __coinduction_ssim r cih || coinduction r cih. +Ltac __play_ssim := (try step); cbn; intros ? ? ?TR. + +Ltac __play_ssim_in H := + (try step in H); + cbn in H; edestruct H as (? & ? & ?TR & ?SS & ?HL); + clear H; [etrans |]; fold_ssim. + +Ltac __eplay_ssim := + match goal with + | h : ssim ?L ?u ?v |- _ => __play_ssim_in h + | h : body (ss ?L) ?R ?u ?v |- _ => __play_ssim_in h + end. + +Ltac __answer_ssim := ex2; split3; etrans. + +#[local] Tactic Notation "play" := __play_ssim. +#[local] Tactic Notation "play" "in" ident(H) := __play_ssim_in H. +#[local] Tactic Notation "eplay" := __eplay_ssim. +#[local] Tactic Notation "answer" := __answer_ssim. + Section ssim_homogenous_theory. Context {E B: Type -> Type} {X: Type} - {L: relation (@label E)}. + {L: lrel E E X X}. Notation ss := (@ss E E B B X X). - #[global] Instance refl_sst {LR: Reflexive L} {C: Chain (ss L)}: Reflexive `C. + #[global] Instance reflexive_ss {R} + (LR: Reflexive L) + (RR: Reflexive R): Reflexive (ss L R). + Proof. + cbn; eauto 10. + Qed. + + #[global] Instance reflexive_chain {LR: Reflexive L} {C: Chain (ss L)}: Reflexive `C. + Proof. + apply Reflexive_chain; typeclasses eauto. + Qed. + + #[global] Instance transitive_ss {R} + (LT: Transitive L) + (RT: Transitive R): Transitive (ss L R). Proof. - apply Reflexive_chain. - cbn; eauto. + intros x y z SS1 SS2. + play. + play in SS1. + play in SS2. + answer. Qed. - #[global] Instance square_sst {LT: Transitive L} {C: Chain (ss L)}: Transitive `C. + #[global] Instance transitive_chain {LT: Transitive L} {C: Chain (ss L)}: Transitive `C. Proof. apply Transitive_chain. - cbn. intros ????? xy yz. - intros ?? xx'. - destruct (xy _ _ xx') as (l' & y' & yy' & ? & ?). - destruct (yz _ _ yy') as (l'' & z' & zz' & ? & ?). - eauto 8. + typeclasses eauto. Qed. (*| PreOrder |*) - #[global] Instance PreOrder_sst {LPO: PreOrder L} {C: Chain (ss L)}: PreOrder `C. + #[global] Instance PreOrder_chain {LPO: PreOrder L} {C: Chain (ss L)}: PreOrder `C. Proof. split; typeclasses eauto. Qed. End ssim_homogenous_theory. - + (*| Parametric theory of [ss] with heterogenous [L] |*) Section ssim_heterogenous_theory. Arguments label: clear implicits. - Context {E F C D: Type -> Type} {X Y: Type} - {L: rel (@label E) (@label F)}. + Context {E F C D: Type -> Type} {X Y: Type}. Notation ss := (@ss E F C D X Y). Notation ssim := (@ssim E F C D X Y). + Lemma ssim_mono : + Proper (sub_lrel ==> leq) ssim. + Proof. + cbn; intros * SUB. + coinduction R cih. + intros u v HSS l u' TR. + eplay. + answer. + eapply sub_lrel_subrel; eauto. + Qed. + + Context {L: lrel E F X Y}. + (*| Strong simulation up-to [equ] is valid ---------------------------------------- |*) - Lemma equ_clos_sst {c: Chain (ss L)}: + (* Can this be rewritten with a simpler proper? *) + Lemma equ_clos_chain {c: Chain (ss L)}: forall x y, equ_clos `c x y -> `c x y. Proof. apply tower. @@ -166,116 +215,90 @@ Section ssim_heterogenous_theory. rewrite <- Equu; auto. Qed. - #[global] Instance equ_clos_sst_goal {c: Chain (ss L)} : - Proper (equ eq ==> equ eq ==> flip impl) `c. + #[global] Instance seq_chain_goal {c: Chain (ss L)} : + Proper (Seq ==> Seq ==> flip impl) (`c). Proof. - cbn; intros ? ? eq1 ? ? eq2 H. - apply equ_clos_sst; econstructor; [eauto | | symmetry; eauto]; assumption. - Qed. - - #[global] Instance equ_clos_sst_ctx {c: Chain (ss L)} : - Proper (equ eq ==> equ eq ==> impl) `c. + apply tower. + - intros ? INC t t' HP' ? ? HP'' ?? HP'''. + red. + eapply INC; eauto. + apply leq_infx in HP'''. + now apply HP'''. + - intros ? INC t t' EQt u u' EQu HS l v TR. + rewrite EQt in TR. + apply HS in TR as (l' & v' & ? & ? & ?). + exists l',v'; split; auto. + now rewrite EQu. + Qed. + + #[global] Instance equ_chain_goal {c: Chain (ss L)} : + Proper (equ eq ==> equ eq ==> flip impl) `c. Proof. cbn; intros ? ? eq1 ? ? eq2 H. - apply equ_clos_sst; econstructor; [symmetry; eauto | | eauto]; assumption. + apply equ_clos_chain; econstructor; [eauto | | symmetry; eauto]; assumption. Qed. - #[global] Instance equ_ss_closed_goal {r} : - Proper (equ eq ==> equ eq ==> flip impl) (ss L r). + #[global] Instance seq_ss_goal {r} : + Proper (Seq ==> Seq ==> flip impl) (ss L r). Proof. intros t t' tt' u u' uu'; cbn; intros. rewrite tt' in H0. apply H in H0 as (l' & ? & ? & ? & ?). - do 2 eexists; eauto. rewrite uu'. eauto. + ex2; eauto. rewrite uu'. eauto. Qed. - #[global] Instance equ_ss_closed_ctx {r} : - Proper (equ eq ==> equ eq ==> impl) (ss L r). + #[global] Instance equ_ss_goal {r} : + Proper (equ eq ==> equ eq ==> flip impl) (ss L r). Proof. intros t t' tt' u u' uu'; cbn; intros. - rewrite <- tt' in H0. apply H in H0 as (l' & ? & ? & ? & ?). - do 2 eexists; eauto. rewrite <- uu'. eauto. - Qed. - -(*| - stuck ctrees can be simulated by anything. -|*) - Lemma is_stuck_ss (R : rel _ _) (t : ctree E C X) (t': ctree F D Y): - is_stuck t -> ss L R t t'. - Proof. - repeat intro. now apply H in H0. - Qed. - - Lemma is_stuck_ssim (t: ctree E C X) (t': ctree F D Y): - is_stuck t -> ssim L t t'. - Proof. - intros. step. now apply is_stuck_ss. + rewrite tt' in H0. apply H in H0 as (l' & ? & ? & ? & ?). + ex2; eauto. rewrite uu'. eauto. Qed. - Lemma Stuck_ss (R : rel _ _) (t : ctree F D Y) : ss L R Stuck t. + #[global] Instance seq_chain_ctx {c: Chain (ss L)} : + Proper (Seq ==> Seq ==> impl) `c. Proof. - repeat intro. now apply Stuck_is_stuck in H. - Qed. - - Lemma Stuck_ssim (t : ctree F D Y) : ssim L Stuck t. + apply tower. + - intros ? INC t t' HP' ? ? HP'' ?? HP'''. + red. + eapply INC; eauto. + apply leq_infx in HP'''. + now apply HP'''. + - intros ? INC t t' EQt u u' EQu HS l v TR. + rewrite <- EQt in TR. + apply HS in TR as (l' & v' & ? & ? & ?). + exists l',v'; split; auto. + now rewrite <- EQu. + Qed. + + #[global] Instance equ_chain_ctx {c: Chain (ss L)} : + Proper (equ eq ==> equ eq ==> impl) `c. Proof. - intros. step. apply Stuck_ss. + cbn; intros ? ? eq1 ? ? eq2 H. + apply equ_clos_chain; econstructor; [symmetry; eauto | | eauto]; assumption. Qed. - Lemma spin_ss (R : rel _ _) (t : ctree F D Y): ss L R spin t. + #[global] Instance seq_ss_ctx {r} : + Proper (Seq ==> Seq ==> impl) (ss L r). Proof. - repeat intro. now apply spin_is_stuck in H. + intros t t' tt' u u' uu'; cbn; intros. + rewrite <- tt' in H0. apply H in H0 as (l' & ? & ? & ? & ?). + ex2; eauto. rewrite <- uu'. eauto. Qed. - Lemma spin_ssim : forall (t' : ctree F D Y), - ssim L spin t'. + #[global] Instance equ_ss_ctx {r} : + Proper (equ eq ==> equ eq ==> impl) (ss L r). Proof. - intros. step. apply spin_ss. + intros t t' tt' u u' uu'; cbn; intros. + rewrite <- tt' in H0. apply H in H0 as (l' & ? & ? & ? & ?). + ex2; eauto. rewrite <- uu'. eauto. Qed. End ssim_heterogenous_theory. -Definition Lequiv {E F} X Y (L L' : rel (@label E) (@label F)) := - forall l l', wf_val X l -> wf_val Y l' -> - L l l' <-> L' l l'. - -#[global] Instance weq_Lequiv : forall {E F} X Y, - subrelation weq (@Lequiv E F X Y). -Proof. - red. red. intros. apply H. -Qed. - -#[global] Instance Equivalence_Lequiv : forall {E F} X Y, - Equivalence (@Lequiv E F X Y). -Proof. - split; cbn; intros. - - now apply weq_Lequiv. - - red. intros. red in H. rewrite H; auto. - - red. intros. - etransitivity. apply H; auto. apply H0; auto. -Qed. - -#[global] Instance Lequiv_ss_goal : forall {E F C D X Y}, - Proper (Lequiv X Y ==> leq) (@ss E F C D X Y). -Proof. - cbn. intros. - apply H0 in H1 as ?. destruct H2 as (? & ? & ? & ? & ?). - exists x0, x1. split; auto. split; auto. apply H; etrans. -Qed. - -#[global] Instance Lequiv_ssim : forall {E F C D X Y}, - Proper (Lequiv X Y ==> leq) (@ssim E F C D X Y). -Proof. - cbn. intros. - - unfold ssim. - epose proof (gfp_leq (x := ss x) (y := ss y)). lapply H1. - + intro. red in H2. cbn in H2. apply H2. unfold ssim in H0. apply H0. - + now rewrite H. -Qed. - #[global] Instance weq_ssim : forall {E F C D X Y}, - Proper (weq ==> weq) (@ssim E F C D X Y). + Proper (lequiv ==> weq) (@ssim E F C D X Y). Proof. - cbn -[ss weq]. intros. apply gfp_weq. now apply weq_ss. + cbn -[ss weq]. intros. apply gfp_weq. now apply lequiv_ss. Qed. (*| @@ -285,254 +308,146 @@ We have proved in the module [Equ] that up-to bind context is a valid enhancement to prove [equ]. We now prove the same result, but for strong simulation. |*) - + Section bind. Arguments label: clear implicits. Obligation Tactic := idtac. - Context {E F C D: Type -> Type} {X X' Y Y': Type} - (L : hrel (@label E) (@label F)) (R0 : rel X Y). - - (* Mix of R0 for val and L for tau/obs. *) - Variant update_val_rel : @label E -> @label F -> Prop := - | update_Val (v1 : X) (v2 : Y) : R0 v1 v2 -> update_val_rel (val v1) (val v2) - | update_NonVal l1 l2 : ~is_val l1 -> ~is_val l2 -> L l1 l2 -> update_val_rel l1 l2 - . - - Lemma update_val_rel_val : forall (v1 : X) (v2 : Y), - update_val_rel (val v1) (val v2) -> - R0 v1 v2. - Proof. - intros. remember (val v1) as l1. remember (val v2) as l2. - destruct H. - - apply val_eq_inv in Heql1, Heql2. now subst. - - subst. exfalso. now apply H. - Qed. - - Lemma update_val_rel_val_l : forall (v1 : X) l2, - update_val_rel (val v1) l2 -> - exists v2 : Y, l2 = val v2 /\ R0 v1 v2. - Proof. - intros. remember (val v1) as l1. destruct H. - - apply val_eq_inv in Heql1. subst. eauto. - - subst. exfalso. apply H. constructor. - Qed. - - Lemma update_val_rel_val_r : forall l1 (v2 : Y), - update_val_rel l1 (val v2) -> - exists v1 : X, l1 = val v1 /\ R0 v1 v2. - Proof. - intros. remember (val v2) as l2. destruct H. - - apply val_eq_inv in Heql2. subst. eauto. - - subst. exfalso. apply H0. constructor. - Qed. - - Lemma update_val_rel_nonval_l : forall l1 l2, - update_val_rel l1 l2 -> - ~is_val l1 -> - ~is_val l2 /\ L l1 l2. - Proof. - intros. destruct H. - - exfalso. apply H0. constructor. - - auto. - Qed. - - Lemma update_val_rel_nonval_r : forall l1 l2, - update_val_rel l1 l2 -> - ~is_val l2 -> - ~is_val l1 /\ L l1 l2. - Proof. - intros. destruct H. - - exfalso. apply H0. constructor. - - auto. - Qed. - - #[global] Instance Respects_val_update_val_rel : - Respects_val update_val_rel. - Proof. - constructor. intros. destruct H. - - split; etrans. - - tauto. - Qed. - - Definition is_update_val_rel (L0 : rel (@label E) (@label F)) : Prop := - Lequiv X Y update_val_rel L0. - - Lemma update_val_rel_correct : is_update_val_rel update_val_rel. - Proof. - red. red. reflexivity. - Qed. - (*| Specialization of [bind_ctx] to a function acting with [ssim] on the bound value, and with the argument (pointwise) on the continuation. |*) Lemma bind_chain_gen - (RR : rel (label E) (label F)) - (ISVR : is_update_val_rel RR) + {E F C D: Type -> Type} {X X' Y Y': Type} + (L : lrel E F X' Y') + (SS: rel X Y) {R : Chain (@ss E F C D X' Y' L)} : - forall (t : ctree E C X) (t' : ctree F D Y) (k : X -> ctree E C X') (k' : Y -> ctree F D Y'), - ssim RR t t' -> - (forall x x', R0 x x' -> elem R (k x) (k' x')) -> - elem R (bind t k) (bind t' k'). + forall (t : ctree E C X) (t' : ctree F D Y) + (k : X -> ctree E C X') (k' : Y -> ctree F D Y'), + ssim (upd_rel L SS) t t' -> + (forall x y, SS x y -> ` R (k x) (k' y)) -> + ` R (bind t k) (bind t' k'). Proof. apply tower. - intros ? INC ? ? ? ? tt' kk' ? ?. apply INC. apply H. apply tt'. intros x x' xx'. apply leq_infx in H. apply H. now apply kk'. - - intros ? ? ? ? ? ? tt' kk'. + - clear R. + intros R ? ? ? ? ? tt' kk'. step in tt'. cbn; intros * STEP. - apply trans_bind_inv in STEP as [(?H & ?t' & STEP & EQ) | (v & STEPres & STEP)]. - + apply tt' in STEP as (? & ? & ? & ? & ?). - do 2 eexists; split; [| split]. - apply trans_bind_l; eauto. - * intro Hl. destruct Hl. - apply ISVR in H3; etrans. - inversion H3; subst. apply H0. constructor. apply H5. constructor. + apply trans_bind_inv in STEP as [(?H & ?t' & STEP & EQ) | [(Z & e & EQl & g & STEP & SEQ) | (v & STEPres & STEP)]]. + + subst l. + apply tt' in STEP as (? & ? & STEP' & HSIM & HRL). + inv HRL. + refine_trans. + ex2; split3. + apply trans_bind_l_τ; eauto. * rewrite EQ. + apply H; auto. + intros. + now step; apply kk'. + * etrans. + + subst l. + apply tt' in STEP as (? & ? & STEP' & HSIM & HRL). + invL. + refine_trans. + exists (ask f); ex; split3. + eapply trans_bind_l_ask; eauto. + * rewrite SEQ. + step. + intros ? ? STEP''. + pose proof trans_passive_inv' STEP'' as (a & EQ & ->). + rewrite EQ in STEP''. + assert (TR: trans (rcv e a) (β e g) (g a)) by etrans. + step in HSIM; apply HSIM in TR as (l' & u' & TR' & HSIM' & HRL'). + pose proof trans_passive_inv' TR' as (b & EQ' & ->). + exists (rcv f b); ex; split; eauto; split; cycle 1. + { invL; etrans. } + rewrite EQ. apply H. - apply H2. - intros * HR. - now apply (b_chain x), kk'. - * apply ISVR in H3; etrans. - destruct H3. exfalso. apply H0. constructor. eauto. - + apply tt' in STEPres as (u' & ? & STEPres & EQ' & ?). - apply ISVR in H0; etrans. - dependent destruction H0. - 2 : exfalso; apply H0; constructor. - pose proof (trans_val_inv STEPres) as EQ. - rewrite EQ in STEPres. - specialize (kk' v v2 H0). - apply kk' in STEP as (u'' & ? & STEP & EQ'' & ?); cbn in *. - do 2 eexists; split. + rewrite EQ' in HSIM'; auto. + intros. + now step; apply kk'. + * etrans. + + apply tt' in STEPres as (? & ? & STEP' & HSIM & HRL). + invL. + apply (kk' v y) in STEP as (l' & u' & STEP'' & HSIM'' & HRL'). + exists l'; eexists; split; eauto. + 2:etrans. eapply trans_bind_r; eauto. - split; auto. + erewrite <- trans_val_inv'; eauto. Qed. -End bind. - -Theorem update_val_rel_eq {E X} : Lequiv X X (@update_val_rel E E X X eq eq) eq. -Proof. - split; intro. - - inv H1; reflexivity. - - subst. destruct l'. - + constructor; auto. - all: intro; inv H1. - + constructor; auto. - all: intro; inv H1. - + red in H. specialize (H X0 v eq_refl). subst. - constructor. reflexivity. -Qed. - -#[global] Instance update_val_rel_Lequiv {E F X Y X' Y'} : - Proper (Lequiv X' Y' ==> weq ==> Lequiv X Y) (@update_val_rel E F X Y). -Proof. - cbn. red. intros. - red in H. split; intro. - - inv H3. - + left. apply H0. auto. - + right; auto. - apply H; auto; now apply wf_val_nonval. - - inv H3. - + left. apply H0. auto. - + right; auto. - apply H; auto; now apply wf_val_nonval. -Qed. - -#[global] Instance is_update_val_rel_Lequiv {E F X Y X' Y'} : - Proper (Lequiv X' Y' ==> weq ==> Lequiv X Y ==> flip impl) (@is_update_val_rel E F X Y). -Proof. - cbn -[weq]. red. intros. red in H2. subst. now rewrite H, H0, H1. -Qed. - -Theorem update_val_rel_update_val_rel {E F X0 X1 Y0 Y1} - (L : rel (@label E) (@label F)) (R0 : rel X0 Y0) (R1 : rel X1 Y1) : - update_val_rel (update_val_rel L R0) R1 == update_val_rel L R1. -Proof. - split; intro. - - destruct H. - + now constructor. - + destruct H1. { exfalso. now apply H. } - constructor; auto. - - destruct H. - + now constructor. - + constructor; auto. - constructor; auto. -Qed. - -Theorem is_update_val_rel_update_val_rel_eq {E X Y Z} : - forall (R : rel X Y), - @Lequiv E E Z Z (@update_val_rel E E Z Z (update_val_rel eq R) eq) eq. -Proof. - intros. rewrite update_val_rel_update_val_rel. - now rewrite update_val_rel_eq. -Qed. - -#[global] Instance Symmetric_update_val_rel {E X} L R0 : - Symmetric L -> - Symmetric R0 -> - Symmetric (@update_val_rel E E X X L R0). -Proof. - cbn. intros. destruct H1; constructor; auto. -Qed. - -#[global] Instance Transitive_update_val_rel : - forall {E X} (L : relation (@label E)) (R0 : relation X), - Transitive L -> - Transitive R0 -> - Transitive (update_val_rel L R0). -Proof. - red. intros. destruct y. - - inv H1. inv H2. constructor; auto. etransitivity; eassumption. - - inv H1. inv H2. constructor; auto. etransitivity; eassumption. - - inv H1; [| exfalso; etrans]. - inv H2; [| exfalso; etrans]. - invert. constructor. eauto. -Qed. +(*| +Specialization: equality on external calls, equality everywhere +|*) + Lemma bind_chain E C D X Y X' Y' + (RR : rel X' Y') (SS : rel X Y) + {R : Chain (@ss E E C D X' Y' (Lvrel RR))} : + forall (t1 : ctree E C X) (t2: ctree E D Y) + (k1 : X -> ctree E C X') (k2 : Y -> ctree E D Y'), + t1 (≲[SS]) t2 -> + (forall x y, SS x y -> `R (k1 x) (k2 y)) -> + `R (t1 >>= k1) (t2 >>= k2). + Proof. + intros. + eapply bind_chain_gen; eauto. + Qed. -Definition lift_val_rel {E X Y} := @update_val_rel E E X Y eq. + Lemma bind_chain_eq E C X X' + {R : Chain (@ss E E C C X' X' Leq)} : + forall (t1 t2 : ctree E C X) + (k1 k2 : X -> ctree E C X'), + t1 ≲ t2 -> + (forall x, `R (k1 x) (k2 x)) -> + `R (t1 >>= k1) (t2 >>= k2). + Proof. + intros. + eapply bind_chain_gen; eauto. + intros ??<-; auto. + Qed. (*| -Specializing the congruence principle for [≲] +Specializations to the gfp |*) -Lemma ssim_clo_bind_gen {E F C D: Type -> Type} {X Y X' Y': Type} {L : rel (@label E) (@label F)} - (R0 : rel X Y) L0 - (HL0 : is_update_val_rel L R0 L0) - (t1 : ctree E C X) (t2: ctree F D Y) - (k1 : X -> ctree E C X') (k2 : Y -> ctree F D Y'): - ssim L0 t1 t2 -> - (forall x y, R0 x y -> ssim L (k1 x) (k2 y)) -> - ssim L (t1 >>= k1) (t2 >>= k2). -Proof. - intros. - eapply bind_chain_gen; eauto. -Qed. + Lemma ssim_bind_gen E F C D X Y X' Y' + L (SS : rel X Y) + (t1 : ctree E C X) (t2: ctree F D Y) + (k1 : X -> ctree E C X') (k2 : Y -> ctree F D Y'): + t1 (≲ upd_rel L SS) t2 -> + (forall x y, SS x y -> k1 x (≲ L) k2 y) -> + t1 >>= k1 (≲ L) t2 >>= k2. + Proof. + intros. + eapply bind_chain_gen; eauto. + Qed. -Lemma ssim_clo_bind {E F C D: Type -> Type} {X Y X' Y': Type} {L : rel (@label E) (@label F)} - (R0 : rel X Y) - (t1 : ctree E C X) (t2: ctree F D Y) - (k1 : X -> ctree E C X') (k2 : Y -> ctree F D Y'): - t1 (≲update_val_rel L R0) t2 -> - (forall x y, R0 x y -> k1 x (≲L) k2 y) -> - t1 >>= k1 (≲L) t2 >>= k2. -Proof. - intros. - eapply bind_chain_gen; eauto using update_val_rel_correct. -Qed. + Lemma ssim_bind E C D X Y X' Y' + (RR : rel X' Y') (SS : rel X Y) + (t1 : ctree E C X) (t2: ctree E D Y) + (k1 : X -> ctree E C X') (k2 : Y -> ctree E D Y'): + t1 (≲ [SS]) t2 -> + (forall x y, SS x y -> k1 x (≲ [RR]) k2 y) -> + t1 >>= k1 (≲ [RR]) t2 >>= k2. + Proof. + intros. + eapply bind_chain_gen; eauto. + Qed. -Lemma ssim_clo_bind_eq {E C D: Type -> Type} {X X': Type} - (t1 : ctree E C X) (t2: ctree E D X) - (k1 : X -> ctree E C X') (k2 : X -> ctree E D X'): - t1 ≲ t2 -> - (forall x, k1 x ≲ k2 x) -> - t1 >>= k1 ≲ t2 >>= k2. -Proof. - intros. - eapply bind_chain_gen; eauto. - - apply update_val_rel_eq. - - intros; subst. apply H0. -Qed. + Lemma ssim_bind_eq {E C D: Type -> Type} {X X': Type} + (t1 : ctree E C X) (t2: ctree E D X) + (k1 : X -> ctree E C X') (k2 : X -> ctree E D X'): + t1 ≲ t2 -> + (forall x, k1 x ≲ k2 x) -> + t1 >>= k1 ≲ t2 >>= k2. + Proof. + intros. + eapply ssim_bind; eauto. + intros ?? ->; auto. + Qed. + +End bind. (*| And in particular, we can justify rewriting [≲] to the left of a [bind]. @@ -540,245 +455,197 @@ And in particular, we can justify rewriting [≲] to the left of a [bind]. NOTE: we shouldn't have to impose [eq] to the right. |*) #[global] Instance ssim_bind_chain {E C X Y} - {R : Chain (@ss E E C C Y Y eq)} : - Proper (ssim eq ==> - (pointwise_relation _ (elem R)) ==> - (elem R)) (@bind E C X Y). + {R : Chain (@ss E E C C Y Y Leq)} : + Proper ((fun t u => ssim Leq (α t) (α u)) ==> + (pointwise_relation _ (fun t u => ` R (α t) (α u))) ==> ` R) (@bind E C X Y). Proof. repeat intro; eapply bind_chain_gen; eauto. - - apply update_val_rel_eq. - - intros. now subst. -Qed. - -#[global] Instance bind_ssim_cong_gen {E C X X'} : - Proper (ssim eq ==> pointwise_relation X (ssim eq) ==> ssim eq) (@CTree.bind E C X X'). -Proof. - cbn. intros. now apply ssim_clo_bind_eq. + intros ?? <-; auto. Qed. -Ltac __play_ssim := step; cbn; intros ? ? ?TR. - -Ltac __play_ssim_in H := - step in H; - cbn in H; edestruct H as (? & ? & ?TR & ?EQ & ?HL); - clear H; [etrans |]. +(* #[global] Instance bind_ssim_cong_gen {E C X X'} : *) +(* Proper (ssim eq ==> pointwise_relation X (ssim eq) ==> ssim eq) (@CTree.bind E C X X'). *) +(* Proof. *) +(* cbn. intros. now apply ssim_clo_bind_eq. *) +(* Qed. *) -Ltac __eplay_ssim := - match goal with - | h : @ssim ?E ?F ?C ?D ?X ?Y _ _ ?L |- _ => - __play_ssim_in h - end. - -#[local] Tactic Notation "play" := __play_ssim. -#[local] Tactic Notation "play" "in" ident(H) := __play_ssim_in H. -#[local] Tactic Notation "eplay" := __eplay_ssim. +(* Notation ssim_ L t u := (ssim L (α t) (α u)). *) +(* Notation ss_ L t u := (ss L _ (α t) (α u)). *) Section Proof_Rules. - Arguments label: clear implicits. - Context {E C: Type -> Type} - {X : Type}. + Context {E F C D: Type -> Type} {X Y : Type}. - Lemma step_ss_ret_gen {Y F D}(x : X) (y : Y) (R L : rel _ _) : - R Stuck Stuck -> - (Proper (equ eq ==> equ eq ==> impl) R) -> - L (val x) (val y) -> - ss L R (Ret x : ctree E C X) (Ret y : ctree F D Y). +(*| +Stuck ctrees can be simulated by anything. +|*) + Lemma ss_is_stuck L R (t : ctree E C X) (t': ctree F D Y): + is_stuck t -> + ss L R t t'. Proof. - intros Rstuck PROP Lval. - cbn; intros ? ? TR; inv_trans; subst; - cbn; eexists; eexists; intuition; etrans; - now rewrite EQ. + repeat intro. now apply H in H0. Qed. - Lemma step_ss_ret {Y F D} (x : X) (y : Y) (L : rel _ _) - {R : Chain (@ss E F C D X Y L)} : - L (val x) (val y) -> - ss L `R (Ret x : ctree E C X) (Ret y : ctree F D Y). + Lemma ssim_is_stuck L (t: ctree E C X) (t': ctree F D Y): + is_stuck t -> + ssim L t t'. Proof. - intros. - apply step_ss_ret_gen. - - apply (b_chain R). - apply is_stuck_ss; apply Stuck_is_stuck. - - typeclasses eauto. - - apply H. - Qed. - - Lemma step_ss_ret_l_gen {Y F D} (x : X) (y : Y) (u u' : ctree F D Y) (L R : rel _ _) : - R Stuck Stuck -> - (Proper (equ eq ==> equ eq ==> impl) R) -> - L (val x) (val y) -> - trans (val y) u u' -> - ss L R (Ret x : ctree E C X) u. - Proof. - intros. cbn. intros. - apply trans_val_inv in H2 as ?. - inv_trans. subst. setoid_rewrite EQ. - etrans. + intros. step. now apply ss_is_stuck. Qed. - Lemma step_ss_ret_l {Y F D} (x : X) (y : Y) (u u' : ctree F D Y) (L : rel _ _) - {R : Chain (@ss E F C D X Y L)} : - L (val x) (val y) -> - trans (val y) u u' -> - ss L ` R (Ret x : ctree E C X) u. + Lemma ss_stuck L R (t : ctree F D Y) : + @ss E F C D X Y L R Stuck t. Proof. - intros. - eapply step_ss_ret_l_gen; eauto. - - apply (b_chain R). - apply is_stuck_ss; apply Stuck_is_stuck. - - typeclasses eauto. + repeat intro. now apply stuck_is_stuck in H. Qed. - Lemma ssim_ret {Y F D} (x : X) (y : Y) (L : rel _ _) : - L (val x) (val y) -> - ssim L (Ret x : ctree E C X) (Ret y : ctree F D Y). + Lemma ssim_stuck L (t : ctree F D Y) : + @ssim E F C D X Y L Stuck t. Proof. - intros. step. now apply step_ss_ret. + intros. step. apply ss_stuck. Qed. -(*| - The vis nodes are deterministic from the perspective of the labeled - transition system, stepping is hence symmetric and we can just recover - the itree-style rule. -|*) - Lemma step_ss_vis_gen {Y Z Z' F D} (e : E Z) (f: F Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (R L: rel _ _) : - (Proper (equ eq ==> equ eq ==> impl) R) -> - (forall x, exists y, R (k x) (k' y) /\ L (obs e x) (obs f y)) -> - ss L R (Vis e k) (Vis f k'). + Lemma ss_spin L R (t : ctree F D Y) : + @ss E F C D X Y L R spin t. Proof. - intros. - cbn; intros ? ? TR; inv_trans; subst; - destruct (H0 x) as (x' & RR & LL); - cbn; eexists; eexists; intuition. - - rewrite EQ; eauto. - - assumption. + repeat intro. now apply spin_is_stuck in H. Qed. - Lemma step_ss_vis {Y Z Z' F D} (e : E Z) (f: F Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (L : rel _ _) - {R : Chain (@ss E F C D X Y L)} : - (forall x, exists y, ` R (k x) (k' y) /\ L (obs e x) (obs f y)) -> - ss L ` R (Vis e k) (Vis f k'). + Lemma ssim_spin L (t' : ctree F D Y) : + @ssim E F C D X Y L spin t'. Proof. - intros * EQ. - apply step_ss_vis_gen; auto. - typeclasses eauto. + intros. step. apply ss_spin. Qed. - Lemma ssim_vis {Y Z Z' F D} (e : E Z) (f: F Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (L : rel _ _) : - (forall x, exists y, ssim L (k x) (k' y) /\ L (obs e x) (obs f y)) -> - ssim L (Vis e k) (Vis f k'). - Proof. - intros. step. apply step_ss_vis; auto. - Qed. +(*| +Ret nodes - Lemma step_ss_vis_id_gen {Y Z F D} (e : E Z) (f: F Z) - (k : Z -> ctree E C X) (k' : Z -> ctree F D Y) (R L: rel _ _) : - (Proper (equ eq ==> equ eq ==> impl) R) -> - (forall x, R (k x) (k' x) /\ L (obs e x) (obs f x)) -> - ss L R (Vis e k) (Vis f k'). +Note: the general formulation (over any well-behaved realtion rather than elements of the chain) is necessary for br nodes, but also useful to reuse in [css] (where the relation will be an element of the css chain). +|*) + Lemma ss_ret_gen (x : X) (y : Y) L R : + R (α Stuck) (α Stuck) -> + (Proper (Seq ==> Seq ==> impl) R) -> + RR L x y -> + ss L R (Ret x : ctree E C X) (Ret y : ctree F D Y). Proof. - intros. apply step_ss_vis_gen. { typeclasses eauto. } - eauto. + intros HS HP HR l u TR. + inv_trans. subst. + ex2; intuition. + now rewrite EQ. Qed. - - Lemma step_ss_vis_id {Y Z F D} (e : E Z) (f: F Z) - (k : Z -> ctree E C X) (k' : Z -> ctree F D Y) (L : rel _ _) + + Lemma ss_ret (x : X) (y : Y) L {R : Chain (@ss E F C D X Y L)} : - (forall x, ` R (k x) (k' x) /\ L (obs e x) (obs f x)) -> - ss L ` R (Vis e k) (Vis f k'). + RR L x y -> + ss L `R (Ret x : ctree E C X) (Ret y : ctree F D Y). Proof. - intros * EQ. - apply step_ss_vis_id_gen; auto. + apply ss_ret_gen. + step; apply ss_stuck. typeclasses eauto. Qed. - - Lemma ssim_vis_id {Y Z F D} (e : E Z) (f: F Z) - (k : Z -> ctree E C X) (k' : Z -> ctree F D Y) (L : rel _ _) : - (forall x, ssim L (k x) (k' x) /\ L (obs e x) (obs f x)) -> - ssim L (Vis e k) (Vis f k'). + + Lemma ssim_ret (x : X) (y : Y) L : + RR L x y -> + ssim L (Ret x : ctree E C X) (Ret y : ctree F D Y). Proof. - intros. step. now apply step_ss_vis_id. + intros. + step. now apply ss_ret. Qed. - + (*| - Same goes for visible tau nodes. + The vis nodes are deterministic from the perspective of the labeled + transition system, stepping is hence symmetric and we can just recover + the itree-style rule. |*) - Lemma step_ss_step_gen {Y F D} - (t : ctree E C X) (t': ctree F D Y) (R L: rel _ _): - (Proper (equ eq ==> equ eq ==> impl) R) -> - L τ τ -> - (R t t') -> - ss L R (Step t) (Step t'). + (* TODO: specialization to Lvrel *) + + Lemma ss_vis {Z Z'} (e : E Z) (f: F Z') + (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) L + {R : Chain (@ss E F C D X Y L)} + (HRask : Rask L e f) + (HRrcv : forall x, exists y, `R (k x) (k' y) /\ Rrcv L e f x y) : + ss L ` R (Vis e k) (Vis f k'). Proof. - intros PR ? EQs. - intros ? ? TR; inv_trans; subst. - cbn; do 2 eexists; split; [etrans | split; [rewrite EQ; eauto|assumption]]. + intros ?? TR; inv_trans. + subst. + ex2; intuition. + rewrite EQ. + step. + intros l u TR. + inv_trans; subst. + destruct (HRrcv x) as (y & ? & ?). + ex2; intuition. + rewrite EQ0; eauto. + etrans. Qed. - Lemma step_ss_step {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L : rel _ _) - {R : Chain (@ss E F C D X Y L)} : - (` R t t') -> - L τ τ -> - ss L ` R (Step t) (Step t'). + Lemma ssim_vis {Z Z'} (e : E Z) (f: F Z') + (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) L + (HRask : Rask L e f) + (HRrcv : forall x, exists y, ssim L (k x) (k' y) /\ Rrcv L e f x y) : + ssim L (Vis e k) (Vis f k'). Proof. - intros. - apply step_ss_step_gen; auto. - typeclasses eauto. + intros. step. apply ss_vis; auto. Qed. - Lemma step_ssim_step {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L : rel _ _) : - (ssim L t t') -> - L τ τ -> - ssim L (Step t) (Step t'). + (* Useful special case: over the same type return type, + we usually pick the identity *) + Lemma ss_vis_id {Z} (e : E Z) (f: F Z) + (k : Z -> ctree E C X) (k' : Z -> ctree F D Y) L + {R : Chain (@ss E F C D X Y L)} + (HRask : Rask L e f) + (HRrcv : forall z, ` R (k z) (k' z) /\ Rrcv L e f z z) : + ss L ` R (Vis e k) (Vis f k'). Proof. - intros. - step. apply step_ss_step; auto. + eapply ss_vis; eauto. + Qed. + + Lemma ssim_vis_id {Z} (e : E Z) (f : F Z) + (k : Z -> ctree E C X) (k' : Z -> ctree F D Y) L + (HRask : Rask L e f) + (HRrcv : forall x, ssim L (k x) (k' x) /\ Rrcv L e f x x) : + ssim L (Vis e k) (Vis f k'). + Proof. + intros. step. now apply ss_vis_id. Qed. (*| - For invisible nodes, the situation is different: we may kill them, but that execution - cannot act as going under the guard. +Invisible nodes |*) - Lemma step_ss_br_l_gen {Y F D Z} (c : C Z) - (k : Z -> ctree E C X) (t': ctree F D Y) (R L: rel _ _): + (* Here we need a stronger lemma quantifying over arbitrary relations [R] and not just elements of the Chain in order to lift things to ssim as we don't unlock ssim in the structural subterm *) + Lemma ss_br_l_gen {Z} (c : C Z) + (k : Z -> ctree E C X) (t': ctree F D Y) R L: (forall x, ss L R (k x) t') -> ss L R (Br c k) t'. Proof. intros EQs. intros ? ? TR; inv_trans; subst. - apply EQs in TR; destruct TR as (u' & TR' & EQ'). - eauto. + edestruct3 EQs; eauto. Qed. - Lemma step_ss_br_l {Y F D Z} (c : C Z) - (k : Z -> ctree E C X) (t: ctree F D Y) (L: rel _ _) - {R : Chain (@ss E F C D X Y L)} : + Lemma ss_br_l {Z} (c : C Z) + (k : Z -> ctree E C X) (t: ctree F D Y) L + {R : Chain (@ss E F C D X Y L)} : (forall x, ss L `R (k x) t) -> ss L `R (Br c k) t. Proof. intros. - intros ? ? TR; inv_trans; subst. - apply H in TR as (? & ? & ?). - eauto. + intros ? ? TR. + inv_trans; subst. + edestruct3 H; eauto. Qed. - Lemma ssim_br_l {Y F D Z} (c : C Z) - (k : Z -> ctree E C X) (t: ctree F D Y) (L: rel _ _): + Lemma ssim_br_l {Z} (c : C Z) + (k : Z -> ctree E C X) (t: ctree F D Y) L : (forall x, ssim L (k x) t) -> ssim L (Br c k) t. Proof. - intros. step. apply step_ss_br_l_gen. intros. + intros. step. apply ss_br_l_gen. intros. specialize (H x). step in H. apply H. Qed. - Lemma step_ss_br_r_gen {Y F D Z} (c : D Z) x - (k : Z -> ctree F D Y) (t: ctree E C X) (R L: rel _ _): + Lemma ss_br_r_gen {Z} (c : D Z) x + (k : Z -> ctree F D Y) (t: ctree E C X) R L: ss L R t (k x) -> ss L R t (Br c k). Proof. @@ -787,493 +654,404 @@ Section Proof_Rules. exists x0; etrans. Qed. - Lemma step_ss_br_r {Y F D Z} (c : D Z) x - (k : Z -> ctree F D Y) (t: ctree E C X) (L: rel _ _) + Lemma ss_br_r {Z} (c : D Z) x + (k : Z -> ctree F D Y) (t: ctree E C X) L {R : Chain (@ss E F C D X Y L)} : ss L `R t (k x) -> ss L `R t (Br c k). Proof. - apply step_ss_br_r_gen. + apply ss_br_r_gen. Qed. - Lemma ssim_br_r {Y F D Z} (c : D Z) x - (k : Z -> ctree F D Y) (t: ctree E C X) (L: rel _ _): + Lemma ssim_br_r {Z} (c : D Z) x + (k : Z -> ctree F D Y) (t: ctree E C X) L : ssim L t (k x) -> ssim L t (Br c k). Proof. - intros. step. apply step_ss_br_r_gen with (x := x). now step in H. + intros. step. apply ss_br_r_gen with (x := x). now step in H. Qed. - Lemma step_ss_br_gen {Y F D n m} (a: C n) (b: D m) - (k : n -> ctree E C X) (k' : m -> ctree F D Y) (R L : rel _ _) : + Lemma ss_br_gen {A B} (c: C A) (d: D B) + (k : A -> ctree E C X) (k' : B -> ctree F D Y) R L : (forall x, exists y, ss L R (k x) (k' y)) -> - ss L R (Br a k) (Br b k'). + ss L R (Br c k) (Br d k'). Proof. intros EQs. - apply step_ss_br_l_gen. + apply ss_br_l_gen. intros. destruct (EQs x) as [x' ?]. - now apply step_ss_br_r_gen with (x:=x'). + now apply ss_br_r_gen with (x:=x'). Qed. - Lemma step_ss_br {Y F D n m} (cn: C n) (cm: D m) - (k : n -> ctree E C X) (k' : m -> ctree F D Y) (L : rel _ _) + Lemma ss_br {A B} (c: C A) (d: D B) + (k : A -> ctree E C X) (k' : B -> ctree F D Y) L {R : Chain (@ss E F C D X Y L)} : (forall x, exists y, ss L `R (k x) (k' y)) -> - ss L `R (Br cn k) (Br cm k'). + ss L `R (Br c k) (Br d k'). Proof. - apply step_ss_br_gen. + apply ss_br_gen. Qed. - Lemma ssim_br {Y F D n m} (cn: C n) (cm: D m) - (k : n -> ctree E C X) (k' : m -> ctree F D Y) (L : rel _ _) : + Lemma ssim_br {A B} (c: C A) (d: D B) + (k : A -> ctree E C X) (k' : B -> ctree F D Y) L : (forall x, exists y, ssim L (k x) (k' y)) -> - ssim L (Br cn k) (Br cm k'). + ssim L (Br c k) (Br d k'). Proof. - intros. step. apply step_ss_br_gen. + intros. step. apply ss_br_gen. intros. destruct (H x). step in H0. exists x0. apply H0. Qed. - Lemma step_ss_br_id_gen {Y F D n} (c: C n) (d: D n) - (k : n -> ctree E C X) (k' : n -> ctree F D Y) - (R L : rel _ _) : - (forall x, ss L R (k x) (k' x)) -> - ss L R (Br c k) (Br d k'). - Proof. - intros; apply step_ss_br_gen. - eauto. - Qed. - - Lemma step_ss_br_id {Y F D n} (c: C n) (d: D n) - (k : n -> ctree E C X) (k': n -> ctree F D Y) (L: rel _ _) + Lemma ss_br_id {A} (c: C A) (d: D A) + (k : A -> ctree E C X) (k': A -> ctree F D Y) L {R : Chain (@ss E F C D X Y L)} : (forall x, ss L `R (k x) (k' x)) -> ss L `R (Br c k) (Br d k'). Proof. - intros; apply step_ss_br; eauto. + intros; apply ss_br; eauto. Qed. - Lemma ssim_br_id {Y F D n} (c: C n) (d: D n) - (k : n -> ctree E C X) (k': n -> ctree F D Y) (L: rel _ _) : + Lemma ssim_br_id {A} (c: C A) (d: D A) + (k : A -> ctree E C X) (k': A -> ctree F D Y) L : (forall x, ssim L (k x) (k' x)) -> ssim L (Br c k) (Br d k'). Proof. intros. apply ssim_br. eauto. Qed. - Lemma step_ss_guard_gen {Y F D} - (t: ctree E C X) (t': ctree F D Y) (R L: rel _ _): - ss L R t t' -> - ss L R (Guard t) (Guard t'). - Proof. - intros EQ. - intros ? ? TR; inv_trans; subst. - apply EQ in TR; destruct TR as (u' & ? & TR' & ? & EQ'). - do 2 eexists; split. - constructor. apply TR'. - eauto. - Qed. - - Lemma step_ss_guard_l_gen {Y F D} - (t: ctree E C X) (t': ctree F D Y) (R L: rel _ _): + Lemma ss_guard_l_gen + (t: ctree E C X) (t': ctree F D Y) R L: ss L R t t' -> ss L R (Guard t) t'. Proof. intros EQ. intros ? ? TR; inv_trans; subst. - apply EQ in TR; destruct TR as (u' & ? & TR' & ? & EQ'). - eauto. - Qed. - - Lemma step_ss_guard_r_gen {Y F D} - (t: ctree E C X) (t': ctree F D Y) (R L: rel _ _): - ss L R t t' -> - ss L R t (Guard t'). - Proof. - intros EQ. - intros ? ? TR; inv_trans; subst. - apply EQ in TR; destruct TR as (u' & ? & TR' & ? & EQ'). - do 2 eexists; split. - constructor. apply TR'. - eauto. + apply EQ in TR; edestruct5 TR; eauto. Qed. - Lemma step_ss_guard_l {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _) + Lemma ss_guard_l + (t: ctree E C X) (t': ctree F D Y) L {R : Chain (@ss E F C D X Y L)} : ss L `R t t' -> ss L `R (Guard t) t'. Proof. - intros. - intros ? ? TR; inv_trans; subst. - apply H in TR as (? & ? & TR' & ?). - eauto. + intros; now apply ss_guard_l_gen. Qed. - Lemma step_ss_guard_r {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _) - {R : Chain (@ss E F C D X Y L)} : - ss L `R t t' -> - ss L `R t (Guard t'). + Lemma ssim_guard_l + (t: ctree E C X) (t': ctree F D Y) L: + ssim L t t' -> + ssim L (Guard t) t'. Proof. - intros. - intros ? ? TR; inv_trans; subst. - apply H in TR as (? & ? & TR' & ?). - do 2 eexists; split; [constructor; apply TR' |]; eauto. + intros; step; apply ss_guard_l; step in H; auto. Qed. - Lemma step_ss_guard {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _) - {R : Chain (@ss E F C D X Y L)} : - ss L `R t t' -> - ss L `R (Guard t) (Guard t'). + Lemma ss_guard_r_gen + (t: ctree E C X) (t': ctree F D Y) R L : + ss L R t t' -> + ss L R t (Guard t'). Proof. - intros. + intros EQ. intros ? ? TR; inv_trans; subst. - apply H in TR as (? & ? & TR' & ?). - do 2 eexists; split; [constructor; apply TR' |]; eauto. + apply EQ in TR; edestruct5 TR; eauto 7. Qed. - Lemma ssim_guard_l {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _): - ssim L t t' -> - ssim L (Guard t) t'. + Lemma ss_guard_r + (t: ctree E C X) (t': ctree F D Y) L + {R : Chain (@ss E F C D X Y L)} : + ss L `R t t' -> + ss L `R t (Guard t'). Proof. - intros; step; apply step_ss_guard_l; step in H; auto. + now apply ss_guard_r_gen. Qed. - Lemma ssim_guard_r {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _): + Lemma ssim_guard_r + (t: ctree E C X) (t': ctree F D Y) L : ssim L t t' -> ssim L t (Guard t'). Proof. - intros; step; apply step_ss_guard_r; step in H; auto. + intros; step; apply ss_guard_r; step in H; auto. Qed. - Lemma ssim_guard {Y F D} - (t: ctree E C X) (t': ctree F D Y) (L: rel _ _): + Lemma ssim_guard + (t: ctree E C X) (t': ctree F D Y) L : ssim L t t' -> ssim L (Guard t) (Guard t'). Proof. - intros; step; apply step_ss_guard; step in H; auto. + intros. + now apply ssim_guard_l, ssim_guard_r. Qed. (*| - When matching visible brs one against another, in general we need to explain how - we map the branches from the left to the branches to the right. - A useful special case is the one where the arity coincide and we simply use the identity - in both directions. We can in this case have [n] rather than [2n] obligations. +Internal transitions |*) - Lemma step_ss_brS_gen {Z Z' Y F D} (c : C Z) (d : D Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (R L: rel _ _) : - (Proper (equ eq ==> equ eq ==> impl) R) -> - (forall x, exists y, R (k x) (k' y)) -> - L τ τ -> - ss L R (BrS c k) (BrS d k'). + Lemma ss_step_gen + (t: ctree E C X) (t': ctree F D Y) L R : + (Proper (Seq ==> Seq ==> impl) R) -> + R (α t) (α t') -> + ss L R (Step t) (Step t'). Proof. - intros. - eapply step_ss_br_gen. - intros. - specialize (H0 x) as [y ?]. - exists y. - eapply step_ss_step_gen; auto. + intros HP HR ???; inv_trans; subst. + ex2; intuition. + now rewrite EQ. Qed. - Lemma step_ss_brS {Z Z' Y F D} (c : C Z) (c' : D Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (L: rel _ _) - {R : Chain (@ss E F C D X Y L)} : - (forall x, exists y, (elem R) (k x) (k' y)) -> - L τ τ -> + Lemma ss_step + (t: ctree E C X) (t': ctree F D Y) L + {R : Chain (@ss E F C D X Y L)} : + ` R t t' -> + ss L ` R (Step t) (Step t'). + Proof. + apply ss_step_gen. + typeclasses eauto. + Qed. + + Lemma ssim_step + (t: ctree E C X) (t': ctree F D Y) L : + ssim L t t' -> + ssim L (Step t) (Step t'). + Proof. + now intros; step; apply ss_step. + Qed. + + Lemma ss_brS {Z Z'} (c : C Z) (c' : D Z') + (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) L + {R : Chain (@ss E F C D X Y L)} : + (forall x, exists y, ` R (k x) (k' y)) -> ss L ` R (BrS c k) (BrS c' k'). Proof. intros. - eapply step_ss_br. + eapply ss_br. intros x; specialize (H x) as [y ?]. exists y. - eapply step_ss_step; auto. + eapply ss_step; auto. Qed. - Lemma ssim_brS {Z Z' Y F D} (c : C Z) (c' : D Z') - (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (L: rel _ _) : + Lemma ssim_brS {Z Z'} (c : C Z) (c' : D Z') + (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) L : (forall x, exists y, ssim L (k x) (k' y)) -> - L τ τ -> ssim L (BrS c k) (BrS c' k'). Proof. - intros. - apply ssim_br. - intros x; specialize (H x) as [y ?]; exists y. - apply step_ssim_step; auto. - Qed. - - Lemma step_ss_brS_id_gen {Z Y D F} (c : C Z) (d: D Z) - (k: Z -> ctree E C X) (k': Z -> ctree F D Y) (R L : rel _ _) : - (Proper (equ eq ==> equ eq ==> impl) R) -> - (forall x, R (k x) (k' x)) -> - L τ τ -> - ss L R (BrS c k) (BrS d k'). - Proof. - intros; apply step_ss_brS_gen; eauto. + now intros; step; apply ss_brS. Qed. - Lemma step_ss_brS_id {Z Y D F} (c : C Z) (d : D Z) - (k: Z -> ctree E C X) (k': Z -> ctree F D Y) (L : rel _ _) - {R : Chain (@ss E F C D X Y L)} : + Lemma ss_brS_id {Z} (c : C Z) (d : D Z) + (k: Z -> ctree E C X) (k': Z -> ctree F D Y) L + {R : Chain (@ss E F C D X Y L)} : (forall x, `R (k x) (k' x)) -> - L τ τ -> ss L ` R (BrS c k) (BrS d k'). Proof. - intros. - apply step_ss_brS; eauto. + intros; apply ss_brS; eauto. Qed. - Lemma ssim_brS_id {Z Y D F} (c : C Z) (d : D Z) - (k: Z -> ctree E C X) (k': Z -> ctree F D Y) (L : rel _ _) : + Lemma ssim_brS_id {Z} (c : C Z) (d : D Z) + (k: Z -> ctree E C X) (k': Z -> ctree F D Y) L : (forall x, ssim L (k x) (k' x)) -> - L τ τ -> ssim L (BrS c k) (BrS d k'). Proof. - intros. - apply ssim_brS; eauto. + intros; apply ssim_brS; eauto. Qed. (*| - Note that with visible schedules, nary-spins are equivalent only - if neither are empty, or if both are empty: they match each other's - τ challenge infinitely often. - With invisible schedules, they are always equivalent: neither of them - produce any challenge for the other. + Note that with visible schedules, an nary-spins refines another only + if it is empty, or if neither are empty. |*) - Lemma spinS_gen_nonempty : forall {Z X Y D F} {L: rel (label E) (label F)} - (x: X) (y: Y) - (c: C X) (c': D Y), - L τ τ -> - ssim L (@spinS_gen E C Z X c) (@spinS_gen F D Z Y c'). + Lemma ssim_spinS_nonempty : + forall {Z Z'} L (x: Z) (y: Z') (c: C Z) (c': D Z'), + @ssim E F C D X Y L (spinS_gen c) (spinS_gen c'). Proof. intros until L; intros x y. - coinduction S CIH; simpl. intros ? ? ? ? ? TR; - rewrite ctree_eta in TR; cbn in TR. - apply trans_brS_inv in TR as (_ & EQ & ->). - eexists; eexists. - rewrite ctree_eta; cbn. - split; [econstructor|]. - + exact y. - + constructor. reflexivity. - + rewrite EQ; eauto. + coinduction S CIH. + intros * ?? TR. + rewrite ctree_eta in TR; cbn in TR. + inv_trans. + ex2; split3; subst; etrans. + rewrite ctree_eta; cbn; etrans. + now rewrite EQ. Qed. + Lemma ssim_spinS_empty : + forall Z L (c: C False) (c': D Z), + @ssim E F C D X Y L (spinS_gen c) (spinS_gen c'). + Proof. + intros. + eapply ssim_is_stuck. + intros ?? TR. + rewrite ctree_eta in TR; cbn in TR. + now inv_trans. + Qed. + + (* Seems useless, but used in a fold lemma. To double check *) + (* Lemma step_ss_ret_l_gen {Y F D} (x : X) (y : Y) (u u' : ctree F D Y) (L R : rel _ _) : *) + (* R Stuck Stuck -> *) + (* (Proper (equ eq ==> equ eq ==> impl) R) -> *) + (* L (val x) (val y) -> *) + (* trans (val y) u u' -> *) + (* ss L R (Ret x : ctree E C X) u. *) + (* Proof. *) + (* intros. cbn. intros. *) + (* apply trans_val_inv in H2 as ?. *) + (* inv_trans. subst. setoid_rewrite EQ. *) + (* etrans. *) + (* Qed. *) + + (* Lemma step_ss_ret_l {Y F D} (x : X) (y : Y) (u u' : ctree F D Y) (L : rel _ _) *) + (* {R : Chain (@ss E F C D X Y L)} : *) + (* L (val x) (val y) -> *) + (* trans (val y) u u' -> *) + (* ss L ` R (Ret x : ctree E C X) u. *) + (* Proof. *) + (* intros. *) + (* eapply step_ss_ret_l_gen; eauto. *) + (* - apply (b_chain R). *) + (* apply is_stuck_ss; apply stuck_is_stuck. *) + (* - typeclasses eauto. *) + (* Qed. *) + (*| Inversion principles -------------------- +Question: are the principles useful over [ss] as well? |*) - Lemma ssim_ret_inv {F D Y} {L: rel (label E) (label F)} (r1 : X) (r2 : Y) : - ssim L (Ret r1 : ctree E C X) (Ret r2 : ctree F D Y) -> + + Lemma ssim_stuck_inv L (t : ctree E C X) (u : ctree F D Y) + (IS : is_stuck u) + (SS :@ssim E F C D X Y L t u) : + is_stuck t. + Proof. + intros l t' TR. + step in SS. + apply SS in TR. + edestruct5 TR. + eapply IS; eauto. + Qed. + + Lemma ssim_ret_l_inv L : + forall r (u : ctree F D Y) + (SS : @ssim E F C D X Y L (Ret r) u), + exists r' u', trans (val r') u u' /\ RR L r r'. + Proof. + intros. step in SS. + edestruct5 SS; etrans. + invL. + ex2; split; etrans. + Qed. + + Lemma ssim_ret_inv L (r1 : X) (r2 : Y) + (SS : @ssim E F C D X Y L (Ret r1) (Ret r2)) : L (val r1) (val r2). Proof. - intro. eplay. - inv_trans; subst; assumption. - Qed. - - Lemma ss_ret_l_inv {F D Y L R} : - forall r (u : ctree F D Y), - ss L R (Ret r : ctree E C X) u -> - exists l' u', trans l' u u' /\ R Stuck u' /\ L (val r) l'. - Proof. - intros. apply H; etrans. + now inv_trans. Qed. - Lemma ssim_ret_l_inv {F D Y L} : - forall r (u : ctree F D Y), - ssim L (Ret r : ctree E C X) u -> - exists l' u', trans l' u u' /\ L (val r) l'. + Lemma ssim_vis_inv {X1 X2} L + (e : E X1) (f : F X2) + (k1 : X1 -> ctree E C X) (k2 : X2 -> ctree F D Y) + (SS : ssim L (Vis e k1) (Vis f k2)) : + Rask L e f /\ + (forall x, exists y, Rrcv L e f x y /\ ssim L (k1 x) (k2 y)). Proof. - intros. step in H. - apply ss_ret_l_inv in H as (? & ? & ? & ? & ?). etrans. + eplay; inv_trans; invL. + split; auto. + intros x. + unshelve eplay; [exact x |]. + invL. + inv_trans. + dependent destruction EQl. + ex; split; eauto. Qed. - Lemma ssim_vis_inv_type {D Y X1 X2} - (e1 : E X1) (e2 : E X2) (k1 : X1 -> ctree E C X) (k2 : X2 -> ctree E D Y) (x1 : X1): - ssim eq (Vis e1 k1) (Vis e2 k2) -> - X1 = X2. + Lemma ssim_vis_l_inv {Z L} : + forall (e : E Z) (k : Z -> ctree E C X) u, + @ssim E F C D X Y L (Vis e k) u -> + exists Z' (f : F Z') k', + trans (ask f) u (β f k') /\ + Rask L e f /\ + forall x, exists y, ssim L (k x) (k' y) /\ Rrcv L e f x y. Proof. intros. - step in H; cbn in H. - edestruct H as (? & ? & ? & ? & ?). - etrans. - inv_trans; subst; auto. - eapply obs_eq_invT; eauto. - Unshelve. - exact x1. + eplay; invL; refine_trans. + ex3; split3; etrans. + intros z. + unshelve eplay; [eassumption |]; inv_trans; invL. + ex; split; etrans. Qed. - Lemma ssbt_vis_inv {F D Y X1 X2} {L: rel (label E) (label F)} - (e1 : E X1) (e2 : F X2) (k1 : X1 -> ctree E C X) (k2 : X2 -> ctree F D Y) (x : X1) - {R : Chain (@ss E F C D X Y L)} : - ss L (elem R) (Vis e1 k1) (Vis e2 k2) -> - (exists y, L (obs e1 x) (obs e2 y)) /\ (forall x, exists y, ` R (k1 x) (k2 y)). + Lemma ssim_guard_l_inv L (t1 : ctree E C X) (t2 : ctree F D Y) : + ssim L (Guard t1) t2 -> + ssim L t1 t2. Proof. - intros. - split; intros; edestruct H as (? & ? & ? & ? & ?); - etrans; subst; - inv_trans; subst; eexists; auto. - - now eapply H2. - - now apply H1. + intros SS; play; eplay. + ex2; split3; etrans. Qed. - Lemma ssim_vis_inv {F D Y X1 X2} {L: rel (label E) (label F)} - (e1 : E X1) (e2 : F X2) (k1 : X1 -> ctree E C X) (k2 : X2 -> ctree F D Y) (x : X1): - ssim L (Vis e1 k1) (Vis e2 k2) -> - (exists y, L (obs e1 x) (obs e2 y)) /\ (forall x, exists y, ssim L (k1 x) (k2 y)). + Lemma ssim_guard_r_inv L (t1 : ctree E C X) (t2 : ctree F D Y) : + ssim L t1 (Guard t2) -> + ssim L t1 t2. Proof. - intros. - split. - - eplay. - inv_trans; subst; exists x2; eauto. - - intros y. - step in H. - cbn in H. - edestruct H as (l' & u' & TR & IN & HL). - apply trans_vis with (x := y). - inv_trans. - eexists. - apply IN. + intros SS; play; eplay; inv_trans. + ex2; split3; etrans. Qed. - Lemma ss_vis_l_inv {F D Y Z L R} : - forall (e : E Z) (k : Z -> ctree E C X) (u : ctree F D Y) x, - ss L R (Vis e k) u -> - exists l' u', trans l' u u' /\ R (k x) u' /\ L (obs e x) l'. + Lemma ssim_guard_inv L (t1 : ctree E C X) (t2 : ctree F D Y) : + ssim L (Guard t1) (Guard t2) -> + ssim L t1 t2. Proof. - intros. apply H; etrans. + intros. + now apply ssim_guard_r_inv, ssim_guard_l_inv. Qed. - Lemma ssim_vis_l_inv {F D Y Z L} : - forall (e : E Z) (k : Z -> ctree E C X) (u : ctree F D Y) x, - ssim L (Vis e k) u -> - exists l' u', trans l' u u' /\ ssim L (k x) u' /\ L (obs e x) l'. + Lemma ssim_br_l_inv L Z + (c: C Z) (t : ctree F D Y) (k : Z -> ctree E C X): + ssim L (Br c k) t -> + forall x, ssim L (k x) t. Proof. - intros. step in H. - now simple apply ss_vis_l_inv with (x := x) in H. + intros; play; eplay; eauto. Qed. - Lemma ss_step_inv {F D Y} {L: rel (label E) (label F)} {R : Chain (@ss E F C D X Y L)} - (t1 : ctree E C X) (t2 : ctree F D Y) : - ss L (elem R) (Step t1) (Step t2) -> - (elem R t1 t2). + Lemma ssim_br_r_inv L Z + (d: D Z) (t : ctree E C X) (k : Z -> ctree F D Y): + ssim L t (Br d k) -> + forall l t', trans l t t' -> + exists x l' u', trans l' (k x) u' /\ + ssim L t' u' /\ + L l l'. Proof. - intros EQ. - edestruct EQ as (l & t & TR & REL & HL); etrans. - now inv_trans. + intros SS * TR. + eplay; inv_trans. + ex3; split3; eauto. Qed. - Lemma ssim_step_inv {F D Y} {L: rel (label E) (label F)} - (t1 : ctree E C X) (t2 : ctree F D Y) : + Lemma ssim_step_inv L (t1 : ctree E C X) (t2 : ctree F D Y) : ssim L (Step t1) (Step t2) -> ssim L t1 t2. Proof. - intros EQ. step in EQ. now apply ss_step_inv. + intros; eplay; inv_trans; etrans. Qed. - Lemma ss_step_l_inv {F D Y L R} : - forall (t : ctree E C X) (u : ctree F D Y), - ss L R (Step t) u -> - exists l' u', trans l' u u' /\ R t u' /\ L τ l'. + Lemma ssim_step_l_inv L (t1 : ctree E C X) (t2 : ctree F D Y) : + ssim L (Step t1) t2 -> + exists t2', trans τ t2 t2' /\ ssim L t1 t2'. Proof. - etrans. + intros; eplay; invL; refine_trans. + ex; split; etrans. Qed. - Lemma ssim_step_l_inv {F D Y L} : - forall (t : ctree E C X) (u : ctree F D Y), - Step t (≲L) u -> - exists l' u', trans l' u u' /\ t (≲L) u' /\ L τ l'. - Proof. - intros. step in H. etrans. - Qed. - - Lemma ssbt_brS_inv {F D Y} {L: rel (label E) (label F)} {R : Chain (@ss E F C D X Y L)} - n m (cn: C n) (cm: D m) (k1 : n -> ctree E C X) (k2 : m -> ctree F D Y) : - ss L (elem R) (BrS cn k1) (BrS cm k2) -> - (forall i1, exists i2, elem R (k1 i1) (k2 i2)). + Lemma ssim_brS_inv L + A B (c: C A) (d: D B) (k1 : A -> ctree E C X) (k2 : B -> ctree F D Y) : + ssim L (BrS c k1) (BrS d k2) -> + forall i1, exists i2, ssim L (k1 i1) (k2 i2). Proof. intros EQ i1. - edestruct EQ as (l & t & TR & REL & HL); etrans. - inv_trans. subst. eauto. + eplay; invL; inv_trans; eauto. Qed. - Lemma ssim_brS_inv {F D Y} {L: rel (label E) (label F)} - n m (cn: C n) (cm: D m) (k1 : n -> ctree E C X) (k2 : m -> ctree F D Y) : - ssim L (BrS cn k1) (BrS cm k2) -> - (forall i1, exists i2, ssim L (k1 i1) (k2 i2)). + Lemma ssim_brS_l_inv L + A (c: C A) (k1 : A -> ctree E C X) (t2 : ctree F D Y) : + ssim L (BrS c k1) t2 -> + forall i, exists t2', trans τ t2 t2' /\ ssim L (k1 i) t2'. Proof. intros EQ i1. - eplay. - subst; inv_trans. - eexists; eauto. - Qed. - - Lemma ss_brS_l_inv {F D Y Z L R} : - forall (c : C Z) (k : Z -> ctree E C X) (u : ctree F D Y) x, - ss L R (BrS c k) u -> - exists l' u', trans l' u u' /\ R (k x) u' /\ L τ l'. - Proof. - intros. apply H; etrans. - Qed. - - Lemma ssim_brS_l_inv {F D Y Z L} : - forall (c : C Z) (k : Z -> ctree E C X) (u : ctree F D Y) x, - ssim L (BrS c k) u -> - exists l' u', trans l' u u' /\ ssim L (k x) u' /\ L τ l'. - Proof. - intros. step in H. - now simple apply ss_brS_l_inv with (x := x) in H. - Qed. - - Lemma ss_br_l_inv {F D Y} {L: rel (label E) (label F)} - n (c: C n) (t : ctree F D Y) (k : n -> ctree E C X) R: - ss L R (Br c k) t -> - forall x, ss L R (k x) t. - Proof. - cbn. intros. - eapply trans_br in H0; [| reflexivity]. - apply H in H0 as (? & ? & ? & ? & ?); subst. - eauto. - Qed. - - Lemma ssim_br_l_inv {F D Y} {L: rel (label E) (label F)} - n (c: C n) (t : ctree F D Y) (k : n -> ctree E C X): - ssim L (Br c k) t -> - forall x, ssim L (k x) t. - Proof. - intros. step. step in H. eapply ss_br_l_inv. apply H. - Qed. - - Lemma ss_guard_l_inv {F D Y} {L: rel (label E) (label F)} - (t : ctree E C X) (u : ctree F D Y) R: - ss L R (Guard t) u -> - ss L R t u. - Proof. - cbn. intros. - eapply trans_guard in H0. - apply H in H0 as (? & ? & ? & ? & ?); subst. - eauto. - Qed. - - Lemma ssim_guard_l_inv {F D Y} {L: rel (label E) (label F)} - (t : ctree E C X) (u : ctree F D Y): - ssim L (Guard t) u -> - ssim L t u. - Proof. - intros. step. step in H. eapply ss_guard_l_inv. apply H. - Qed. - - (* This one isn't very convenient... *) - Lemma ssim_br_r_inv {F D Y} {L: rel (label E) (label F)} - n (c: D n) (t : ctree E C X) (k : n -> ctree F D Y): - ssim L t (Br c k) -> - forall l t', trans l t t' -> - exists l' x t'' , trans l' (k x) t'' /\ L l l' /\ (ssim L t' t''). - Proof. - cbn. intros. step in H. apply H in H0 as (? & ? & ? & ? & ?); subst. inv_trans. - do 3 eexists; eauto. + eplay; invL; inv_trans; eauto. Qed. End Proof_Rules. diff --git a/theories/Eq/Trans.v b/theories/Eq/Trans.v index 910860e..f689db1 100644 --- a/theories/Eq/Trans.v +++ b/theories/Eq/Trans.v @@ -69,17 +69,41 @@ Set Primitive Projections. .. coq:: |*) -Section Trans. +Variant S E B R := + | Active (t : ctree E B R) + | Passive {X} (e : E X) (k : X -> ctree E B R). - Context {E B : Type -> Type} {R : Type}. +Variant SeqR {E B X Y} (RR : hrel X Y) : S E B X -> S E B Y -> Prop := + | ActAct t u (EQ: equ RR t u) : SeqR RR (Active t) (Active u) + | PasPas {A} e (k g : A -> _) (EQ: forall a, equ RR (k a) (g a)) : SeqR RR (Passive e k) (Passive e g) +. +Hint Constructors SeqR : core. +Definition Seq {E B X} := (@SeqR E B X X eq). +Hint Unfold Seq : core. - Notation S' := (ctree' E B R). - Notation S := (ctree E B R). +#[global] Instance SeqR_equiv {E B R} {RR : rel R R} {RE: Equivalence RR}: Equivalence (@SeqR E B R R RR). +Proof. + constructor. + - intros []; auto. + - intros ? ? []; constructor; intros; now symmetry. + - intros ? ? ? EQ1 EQ2. + inv EQ1. + inv EQ2; constructor; intros; etransitivity; eauto. + dependent induction EQ2; constructor; intros; etransitivity; eauto. +Qed. +Arguments Active {E B R}. +Arguments Passive {E B R X} e k. + +Section Trans. + Context {E B : Type -> Type} {R : Type}. + Notation S := (S E B R). + Notation Seq := (@Seq E B R). + Definition SS : EqType := - {| type_of := S ; Eq := equ eq |}. + {| type_of := S ; Eq := Seq |}. - (*| +(*| The domain of labels of the LTS. Note that it could be typed more strongly: [val] labels can only be of type [R]. However typing it statically makes lemmas about @@ -88,7 +112,8 @@ least annoying solution. |*) Variant label : Type := | τ - | obs {X : Type} (e : E X) (v : X) + | ask {X : Type} (e : E X) + | rcv {X : Type} (e : E X) (v : X) (* Note: I think we need to remember which request led to the response for the bisimilarity to be right, but I am not 100% sure, [e] might be spurious *) | val {X : Type} (v : X). Variant is_val : label -> Prop := @@ -99,12 +124,17 @@ least annoying solution. intro H. inversion H. Qed. - Lemma is_val_obs {X} (e : E X) x : ~ is_val (obs e x). + Lemma is_val_ask {X} (e : E X) : ~ is_val (ask e). Proof. intro H. inversion H. Qed. - (*| + Lemma is_val_rcv {X} (e : E X) (x : X) : ~ is_val (rcv e x). + Proof. + intro H. inversion H. + Qed. + +(*| The transition relation over [ctree]s. It can either: - recursively crawl through invisible [br] node; @@ -113,133 +143,133 @@ It can either: - stop at a sink (implemented as a [Stuck] node) by stepping from a [ret v] node, labelling the transition by the returned value. |*) - Inductive trans_ : label -> hrel S' S' := + Inductive transR : label -> hrel S S := - | Transbr {X} (c : B X) x k l t : - trans_ l (observe (k x)) t -> - trans_ l (BrF c k) t + | Transbr {X} (c : B X) x k l t t' u : + t ≅ Br c k -> + t' ≅ k x -> + transR l (Active t') u -> + transR l (Active t) u - | Transguard t t' l : - trans_ l (observe t) t' -> - trans_ l (GuardF t) t' + | Transguard t t' u l : + t ≅ Guard t' -> + transR l (Active t') u -> + transR l (Active t) u - | Transtau t u : - u ≅ t -> - trans_ τ (StepF t) (observe u) + | Transstep t t' u : + t ≅ Step t' -> + u ≅ t' -> + transR τ (Active t) (Active u) - | Transobs {X} (e : E X) k x t : - k x ≅ t -> - trans_ (obs e x) (VisF e k) (observe t) - - | Transval r : - trans_ (val r) (RetF r) StuckF. - Hint Constructors trans_ : core. - - Definition transR l : hrel S S := - fun u v => trans_ l (observe u) (observe v). - - Ltac FtoObs := - match goal with - |- trans_ _ _ ?t => - change t with (observe {| _observe := t |}) - end. - - #[local] Instance trans_equ_aux1 l t : - Proper (going (equ eq) ==> flip impl) (trans_ l t). - Proof. - intros u u' equ; intros TR. - inv equ; rename H into equ. - step in equ. - revert u equ. - dependent induction TR; intros; subst; eauto. - + inv equ. - * rewrite H2; eauto. - * FtoObs. - constructor. - rewrite <- H. - apply observing_sub_equ; eauto. - * FtoObs. - constructor. - rewrite <- H, REL. - apply observing_sub_equ; eauto. - * FtoObs. - constructor. - rewrite <- H, REL. - apply observing_sub_equ; eauto. - * FtoObs. - constructor. - rewrite <- H. - step; rewrite <- H2; constructor; intros. - auto. - * FtoObs. - constructor. - rewrite <- H. - step; rewrite <- H2; constructor; intros. - auto. - + FtoObs. - econstructor. - rewrite H; symmetry; step; auto. - + inv equ. eauto. - Qed. - - #[local] Instance trans_equ_aux2 l : - Proper (going (equ eq) ==> going (equ eq) ==> impl) (trans_ l). - Proof. - intros t t' eqt u u' equ TR. - rewrite <- equ; clear u' equ. - inv eqt; rename H into eqt. - revert t' eqt. - dependent induction TR; intros; auto. - + step in eqt; dependent induction eqt. - econstructor. - apply IHTR. - rewrite REL; reflexivity. - + step in eqt; dependent induction eqt. - econstructor. - apply IHTR. rewrite REL; reflexivity. - + step in eqt; dependent induction eqt. - econstructor. rewrite H,REL; auto. - + step in eqt; dependent induction eqt. - econstructor. - rewrite <- REL; eauto. - + step in eqt; dependent induction eqt. - econstructor. - Qed. - - #[global] Instance trans_equ_ l : - Proper (going (equ eq) ==> going (equ eq) ==> iff) (trans_ l). - Proof. - intros ? ? eqt ? ? equ; split; intros TR. - - eapply trans_equ_aux2; eauto. - - symmetry in equ; symmetry in eqt; eapply trans_equ_aux2; eauto. - Qed. + | Transask {X} (e : E X) t k : + t ≅ Vis e k -> + transR (ask e) (Active t) (Passive e k) + | Transrcv {X} (e : E X) (x : X) k t : + k x ≅ t -> + transR (rcv e x) (Passive e k) (Active t) + + | Transval r t u : + t ≅ Ret r -> + u ≅ Stuck -> + transR (val r) (Active t) (Active u). + Hint Constructors transR : core. + + #[global] Instance equ_Seq_active : Proper (equ eq ==> Seq) Active. + Proof. + now intros ?? EQ; constructor. + Qed. + + #[global] Instance equ_Seq_passive {X} (e : E X) : Proper (pointwise_relation X (equ eq) ==> Seq) (Passive e). + Proof. + now intros ?? EQ; constructor. + Qed. + + #[global] Instance transR_equ_ l : + Proper (Seq ==> Seq ==> iff) (transR l). + Proof. + intros ?? EQ1 ?? EQ2; split; intros TR. + - revert y y0 EQ1 EQ2; dependent induction TR; intros y y0 EQ1 EQ2. + + inv EQ1. + econstructor 1. + rewrite <- EQ, H; reflexivity. + apply H0. + apply IHTR; auto. + + inv EQ1. + econstructor 2. + rewrite <- EQ, H; reflexivity. + apply IHTR; auto. + + inv EQ1; inv EQ2. + econstructor 3. + rewrite <- EQ , H; reflexivity. + rewrite <- EQ0, H0; reflexivity. + + inv EQ1. dependent induction EQ2. + econstructor 4. + rewrite <- EQ0,H. + step; constructor. + apply EQ. + + dependent induction EQ1; inv EQ2. + econstructor 5. + specialize (EQ x); rewrite <- EQ, H; auto. + + inv EQ1; inv EQ2. + econstructor 6. + rewrite <- EQ, H; reflexivity. + rewrite <- EQ0, H0; reflexivity. + - revert x x0 EQ1 EQ2; dependent induction TR; intros y y0 EQ1 EQ2. + + inv EQ1. + econstructor 1. + rewrite EQ, H; reflexivity. + apply H0. + apply IHTR; auto. + + inv EQ1. + econstructor 2. + rewrite EQ, H; reflexivity. + apply IHTR; auto. + + inv EQ1; inv EQ2. + econstructor 3. + rewrite EQ , H; reflexivity. + rewrite EQ0, H0; reflexivity. + + inv EQ1. dependent induction EQ2. + econstructor 4. + rewrite EQ0,H. + step; constructor. + intros ?; symmetry; apply EQ. + + dependent induction EQ1; inv EQ2. + econstructor 5. + specialize (EQ x); rewrite EQ, H, EQ0; auto. + + inv EQ1; inv EQ2. + econstructor 6. + rewrite EQ, H; reflexivity. + rewrite EQ0, H0; reflexivity. + Qed. + (*| -[equ] is congruent for [trans], we can hence build a [srel] and build our +[equ] is congruent for [transR], we can hence build a [srel] and build our relations in this model to still exploit the automation from the [RelationAlgebra] library. |*) - #[global] Instance trans_equ l : - Proper (equ eq ==> equ eq ==> iff) (transR l). - Proof. - intros ? ? eqt ? ? equ; unfold transR. - rewrite eqt, equ; reflexivity. + #[global] Instance transR_equ l : + Proper (Seq ==> Seq ==> iff) (transR l). + Proof. + intros ? ? eqt ? ? equ. + inv eqt; inv equ. + now rewrite EQ,EQ0. + rewrite EQ. + all: try now rewrite EQ, EQ0. + assert (H: Seq (Passive e k) (Passive e g)) + by (apply equ_Seq_passive; red; apply EQ0); now rewrite H. + rewrite EQ0. + assert (H: Seq (Passive e k) (Passive e g)) + by (apply equ_Seq_passive; red; apply EQ); now rewrite H. + assert (H1: Seq (Passive e k) (Passive e g)) + by (apply equ_Seq_passive; red; apply EQ); + assert (H2: Seq (Passive e0 k0) (Passive e0 g0)) + by (apply equ_Seq_passive; red; apply EQ0); + now rewrite H1,H2. Qed. Definition trans l : srel SS SS := {| hrel_of := transR l : hrel SS SS |}. - Lemma trans__trans : forall l t u, - trans_ l (observe t) (observe u) = trans l t u. - Proof. - reflexivity. - Qed. - - Lemma transR_trans : forall l (t t' : S), - transR l t t' = trans l t t'. - Proof. - reflexivity. - Qed. - (*| Extension of [trans] with its reflexive closure, labelled by [τ]. |*) @@ -372,33 +402,44 @@ Elimination rules for [trans] eexists; apply wtrans_τ; eassumption. Qed. - End Trans. -Class Respects_val {E F} (L : rel (@label E) (@label F)) := - { respects_val: - forall l l', - L l l' -> - is_val l <-> is_val l' }. - -Class Respects_τ {E F} (L : rel (@label E) (@label F)) := - { respects_τ: forall l l', - L l l' -> - l = τ <-> l' = τ }. - -Definition eq_obs {E} (L : relation (@label E)) : Prop := - forall X X' e e' (x : X) (x' : X'), - L (obs e x) (obs e' x') -> - obs e x = obs e' x'. - -#[global] Instance Respects_val_eq A: @Respects_val A A eq. -split; intros; subst; reflexivity. -Defined. - -#[global] Instance Respects_τ_eq A: @Respects_τ A A eq. -split; intros; subst; reflexivity. -Defined. - +Arguments label : clear implicits. +#[global] Infix "⩸" := Seq (at level 10). +#[global] Hint Constructors transR : core. + +Ltac rem_weak_ t s := + let tmp := fresh in + let name := fresh "EQ" in + remember t as s eqn:tmp; + assert (EQ: Seq s t) by (now subst); + clear tmp. + +Tactic Notation "rem_weak" constr(t) "as" ident(s) := rem_weak_ t s. + +(* Class Respects_val {E F} (L : rel (@label E) (@label F)) := *) +(* { respects_val: *) +(* forall l l', *) +(* L l l' -> *) +(* is_val l <-> is_val l' }. *) + +(* Class Respects_τ {E F} (L : rel (@label E) (@label F)) := *) +(* { respects_τ: forall l l', *) +(* L l l' -> *) +(* l = τ <-> l' = τ }. *) + +(* #[global] Instance Respects_val_eq A: @Respects_val A A eq. *) +(* split; intros; subst; reflexivity. *) +(* Defined. *) + +(* #[global] Instance Respects_τ_eq A: @Respects_τ A A eq. *) +(* split; intros; subst; reflexivity. *) +(* Defined. *) + +Coercion Active : ctree >-> S. +Notation "'α' t" := (Active t) (at level 100). +(* Out of curiosity: do coercion for β in rocq-elpi *) +Notation "'β' e" := (Passive e) (at level 0). (*| Backward reasoning for [trans] ------------------------------ @@ -412,59 +453,64 @@ Section backward. (*| Structural rules + +We essentially lift the constructors to the [trans] bundling, and +eliminate on the way the noise from closing up everything to [equ eq]. |*) Lemma trans_ret : forall (x : X), trans (E := E) (B := B) (val x) (Ret x) Stuck. Proof. - intros; constructor. + intros; constructor; auto. Qed. - Lemma trans_vis : forall {Y} (e : E Y) x (k : Y -> ctree E B X), - trans (obs e x) (Vis e k) (k x). + Lemma trans_ask : forall {Y} (e : E Y) (k : Y -> ctree E B X), + trans (ask e) (Vis e k) (β e k). Proof. intros; constructor; auto. Qed. - Lemma trans_br : forall {Y} l (t t' : ctree E B X) (c : B Y) k x, - trans l t t' -> - k x ≅ t -> - trans l (Br c k) t'. + Lemma trans_rcv : forall {Y} (e : E Y) (k : Y -> ctree E B X) y, + trans (rcv e y) (β e k) (k y). Proof. - intros * TR Eq. - apply Transbr with x. - rewrite Eq; auto. + intros; constructor; auto. Qed. - Lemma trans_brS : forall {Y} (c : B Y) (k : _ -> ctree E B X) x, - trans τ (BrS c k) (k x). + Lemma trans_br : forall {Y} l (c : B Y) (k : Y -> ctree E B X) u y, + trans l (k y) u -> + trans l (Br c k) u. Proof. - intros. - apply Transbr with x, Transtau. - reflexivity. + intros * TR. + eapply Transbr; [reflexivity| reflexivity |]. + apply TR. Qed. -(*| -Ad-hoc rules for pre-defined finite branching -|*) - - Variable (l : @label E) (t t' : ctree E B X). + Lemma trans_step : forall (t : ctree E B X), + trans τ (Step t) t. + Proof. + intros. + eapply Transstep; reflexivity. + Qed. - Lemma trans_step : - trans τ (Step t) t. + Lemma trans_guard : forall l (t : ctree E B X) u, + trans l t u -> + trans l (Guard t) u. Proof. - now econstructor. + intros * TR. + eapply Transguard; [reflexivity | auto]. Qed. - Lemma trans_guard : - trans l t t' -> - trans l (Guard t) t'. + Lemma trans_brS : forall {Y} (c : B Y) (k : _ -> ctree E B X) x, + trans τ (BrS c k) (k x). Proof. - now econstructor. + intros. + apply trans_br with x, trans_step. Qed. End backward. +#[global] Hint Resolve trans_br trans_guard trans_brS trans_step trans_ask trans_rcv trans_ret : core. + Section BackwardBounded. Context {E B : Type -> Type} {X : Type}. @@ -477,61 +523,48 @@ Section BackwardBounded. trans τ (brS2 t u) t. Proof. intros. - unfold brS2. - apply Transbr with true. - now constructor. + apply trans_br with true, trans_step. Qed. Lemma trans_brS22 : trans τ (brS2 t u) u. Proof. intros. - unfold brS2. - apply Transbr with false. - now constructor. + apply trans_br with false, trans_step. Qed. - Lemma trans_br21 : - trans l t t' -> - trans l (br2 t u) t'. + Lemma trans_br21 x : + trans l t x -> + trans l (br2 t u) x. Proof. intros * TR. - eapply trans_br with (x := true); eauto. + now apply trans_br with true. Qed. - Lemma trans_br22 : - trans l u u' -> - trans l (br2 t u) u'. + Lemma trans_br22 x : + trans l u x -> + trans l (br2 t u) x. Proof. intros * TR. - eapply trans_br with (x := false); eauto. + now apply trans_br with false. Qed. Lemma trans_brS31 : trans τ (brS3 t u v) t. Proof. - intros. - unfold brS3. - apply Transbr with t31. - now constructor. + now apply trans_br with t31. Qed. Lemma trans_brS32 : trans τ (brS3 t u v) u. Proof. - intros. - unfold brS3. - apply Transbr with t32. - now constructor. + now apply trans_br with t32. Qed. Lemma trans_brS33 : trans τ (brS3 t u v) v. Proof. - intros. - unfold brS3. - apply Transbr with t33. - now constructor. + now apply trans_br with t33. Qed. Lemma trans_br31 : @@ -539,7 +572,7 @@ Section BackwardBounded. trans l (br3 t u v) t'. Proof. intros * TR. - eapply trans_br with (x := t31); eauto. + now apply trans_br with t31. Qed. Lemma trans_br32 : @@ -547,7 +580,7 @@ Section BackwardBounded. trans l (br3 t u v) u'. Proof. intros * TR. - eapply trans_br with (x := t32); eauto. + now apply trans_br with t32. Qed. Lemma trans_br33 : @@ -555,43 +588,31 @@ Section BackwardBounded. trans l (br3 t u v) v'. Proof. intros * TR. - eapply trans_br with (x := t33); eauto. + now apply trans_br with t33. Qed. Lemma trans_brS41 : trans τ (brS4 t u v w) t. Proof. - intros. - unfold brS4. - apply Transbr with t41. - now constructor. + eapply trans_br with t41; eauto. Qed. Lemma trans_brS42 : trans τ (brS4 t u v w) u. Proof. - intros. - unfold brS4. - apply Transbr with t42. - now constructor. + eapply trans_br with t42; eauto. Qed. Lemma trans_brS43 : trans τ (brS4 t u v w) v. Proof. - intros. - unfold brS4. - apply Transbr with t43. - now constructor. + eapply trans_br with t43; eauto. Qed. Lemma trans_brS44 : trans τ (brS4 t u v w) w. Proof. - intros. - unfold brS4. - apply Transbr with t44. - now constructor. + eapply trans_br with t44; eauto. Qed. Lemma trans_br41 : @@ -599,7 +620,7 @@ Section BackwardBounded. trans l (br4 t u v w) t'. Proof. intros * TR. - eapply trans_br with (x := t41); eauto. + eapply trans_br with t41; eauto. Qed. Lemma trans_br42 : @@ -607,7 +628,7 @@ Section BackwardBounded. trans l (br4 t u v w) u'. Proof. intros * TR. - eapply trans_br with (x := t42); eauto. + eapply trans_br with t42; eauto. Qed. Lemma trans_br43 : @@ -615,7 +636,7 @@ Section BackwardBounded. trans l (br4 t u v w) v'. Proof. intros * TR. - eapply trans_br with (x := t43); eauto. + eapply trans_br with t43; eauto. Qed. Lemma trans_br44 : @@ -623,7 +644,7 @@ Section BackwardBounded. trans l (br4 t u v w) w'. Proof. intros * TR. - eapply trans_br with (x := t44); eauto. + eapply trans_br with t44; eauto. Qed. End BackwardBounded. @@ -651,13 +672,23 @@ Inverting equalities between labels now dependent induction EQ. Qed. - Lemma obs_eq_invT : forall X Y e1 e2 v1 v2, @obs E X e1 v1 = @obs E Y e2 v2 -> X = Y. - clear B. intros * EQ. + Lemma ask_invT : forall E X Y e1 e2, @ask E X e1 = @ask E Y e2 -> X = Y. + intros * EQ. now dependent induction EQ. Qed. - Lemma obs_eq_inv : forall X e1 e2 v1 v2, @obs E X e1 v1 = @obs E X e2 v2 -> e1 = e2 /\ v1 = v2. - clear B. intros * EQ. + Lemma ask_inv : forall E X e1 e2, @ask E X e1 = @ask E X e2 -> e1 = e2. + intros * EQ. + now dependent induction EQ. + Qed. + + Lemma rcv_invT : forall E X Y e1 e2 v1 v2, @rcv E X e1 v1 = @rcv E Y e2 v2 -> X = Y. + intros * EQ. + now dependent induction EQ. + Qed. + + Lemma rcv_inv : forall E X e1 e2 v1 v2, @rcv E X e1 v1 = @rcv E X e2 v2 -> e1 = e2 /\ v1 = v2. + intros * EQ. now dependent induction EQ. Qed. @@ -665,38 +696,77 @@ Inverting equalities between labels Structural rules |*) - Lemma trans_ret_inv : forall x l (t : ctree E B X), - trans l (Ret x) t -> - t ≅ Stuck /\ l = val x. + (* In the primed versions, [u] is left as an arbitrary S. + In the main version, we can only invert if we already know + that the resulting state is an active one. + (it is of course always one) + *) + Lemma trans_ret_inv' : forall x l u, + trans l (Ret x : ctree E B X) u -> + Seq u (α Stuck) /\ l = val x. + Proof. + intros * TR; inv TR; inv_equ. + intuition. + Qed. + + Lemma trans_ret_inv : forall x l (u : ctree E B X), + trans l (Ret x) u -> + u ≅ Stuck /\ l = val x. Proof. - intros * TR; inv TR; intuition. - rewrite ctree_eta, <- H2; auto. + intros * TR; inv TR; inv_equ. + intuition. + Qed. + + Lemma trans_vis_inv' : forall {Y} (e : E Y) (k : _ -> ctree E B X) l u, + trans l (Vis e k) u -> + Seq u (β e k) /\ l = ask e. + Proof. + intros * TR. + inv TR; inv_equ. + split; auto. + constructor; intros ?; symmetry; eauto. Qed. Lemma trans_vis_inv : forall {Y} (e : E Y) k l (u : ctree E B X), trans l (Vis e k) u -> - exists x, u ≅ k x /\ l = obs e x. + False. + Proof. + intros * TR. + inv TR; inv_equ. + Qed. + + Lemma trans_passive_inv' : forall {Y} (e : E Y) (k : Y -> ctree E B X) l u, + trans l (β e k) u -> + exists x, Seq u (α k x) /\ l = rcv e x. + Proof. + intros * TR. + cbn in TR; dependent induction TR. + eexists; split; eauto. + constructor; symmetry; eauto. + Qed. + + Lemma trans_passive_inv : forall {Y} (e : E Y) (k : Y -> ctree E B X) l (u : ctree E B X), + trans l (β e k) u -> + exists x, u ≅ (k x) /\ l = rcv e x. Proof. intros * TR. - inv TR. - dependent induction H3; eexists; split; eauto. - rewrite ctree_eta, <- H4, <- ctree_eta; symmetry; auto. + apply trans_passive_inv' in TR as (? & ? & ?). + inv H; eauto. Qed. - Lemma trans_br_inv : forall {Y} l (c : B Y) k (u : ctree E B X), + Lemma trans_br_inv : forall {Y} l (c : B Y) (k : _ -> ctree E B X) u, trans l (Br c k) u -> exists n, trans l (k n) u. Proof. intros * TR. cbn in *. - unfold transR in *. - cbn in TR |- *. match goal with - | h: trans_ _ ?x ?y |- _ => + | h: transR _ ?x ?y |- _ => remember x as ox; remember y as oy end. revert c k u Heqox Heqoy. - induction TR; intros; inv Heqox; eauto. + inv TR; intros; subst; inv Heqox; inv_equ. + exists x; now rewrite H0, <- (EQ x) in H1. Qed. Lemma trans_guard_inv : forall l (t : ctree E B X) u, @@ -704,16 +774,36 @@ Structural rules trans l t u. Proof. intros * TR. - now inv TR. + inv TR; inv_equ. + now rewrite H0. Qed. - Lemma trans_step_inv : forall l (t : ctree E B X) u, + Lemma trans_step_inv' : forall l (t : ctree E B X) u, + trans l (Step t) u -> + Seq u t /\ l = τ. + Proof. + intros * TR. + inv TR; inv_equ; split; auto. + now rewrite H0,H2. + Qed. + + Lemma trans_step_inv : forall l (t u : ctree E B X), trans l (Step t) u -> u ≅ t /\ l = τ. Proof. intros * TR. - inv TR; split; auto. - rewrite <- H2. apply observe_equ_eq; auto. + apply trans_step_inv' in TR as [? ?]; split; auto. + now inv H. + Qed. + + Lemma trans_brS_inv' : forall {Y} l (c : B Y) (k : _ -> ctree E B X) u, + trans l (BrS c k) u -> + exists n, Seq u (α (k n)) /\ l = τ. + Proof. + intros * TR. + eapply trans_br_inv in TR as [n ?]. + apply trans_step_inv' in H as [? ?]. + eauto. Qed. Lemma trans_brS_inv : forall {Y} l (c : B Y) k (u : ctree E B X), @@ -721,18 +811,15 @@ Structural rules exists n, u ≅ k n /\ l = τ. Proof. intros * TR. - apply trans_br_inv in TR as [n ?]. - inv H. - exists n; split; auto. - rewrite <- H3. apply observe_equ_eq; auto. + apply trans_brS_inv' in TR as (? & H & ?); inv H; eauto. Qed. - Lemma trans_stuck_inv : forall l (u : ctree E B X), - trans l Stuck u -> + Lemma trans_stuck_inv : forall l u, + trans l (Stuck : ctree E B X) u -> False. Proof. intros * TR. - inv TR. + cbn in TR; dependent induction TR; inv_equ. Qed. (*| @@ -798,14 +885,16 @@ I'll skip them for now and introduce them if they turn out to be useful. |*) - Lemma trans__val_inv {Y} : - forall (T U : ctree' E B X) (x : Y), - trans_ (val x) T U -> - go U ≅ Stuck. + Lemma trans_val_inv' {Y} : + forall t u (x : Y), + trans (val x) t u -> + Seq u (α (Stuck : ctree E B X)). Proof. intros * TR. remember (val x) as ox. - rewrite ctree_eta; induction TR; intros; auto; try now inv Heqox. + revert x Heqox. + cbn in TR; induction TR; intros ? Heqox; try now inv Heqox. + all: eauto. Qed. Lemma trans_val_inv {Y} : @@ -813,8 +902,7 @@ useful. trans (val x) t u -> u ≅ Stuck. Proof. - intros * TR. cbn in TR. red in TR. - apply trans__val_inv in TR. rewrite ctree_eta. apply TR. + now intros * TR; apply trans_val_inv' in TR; inv TR. Qed. Lemma wtrans_val_inv : forall (x : X), @@ -825,7 +913,7 @@ useful. destruct TR as [t2 [t1 step1 step2] step3]. exists t1; split. apply wtrans_τ; auto. - erewrite <- trans_val_inv; eauto. + erewrite <- trans_val_inv'; eauto. Qed. End forward. @@ -835,11 +923,31 @@ End forward. --------------- |*) +Lemma etrans_case' {E B X} : forall l t u, + etrans l t u -> + (trans l t u \/ (l = τ /\ @Seq E B X t u)). +Proof. + intros [] * TR; cbn in *; intuition. +Qed. + Lemma etrans_case {E B X} : forall l (t u : ctree E B X), etrans l t u -> (trans l t u \/ (l = τ /\ t ≅ u)). Proof. intros [] * TR; cbn in *; intuition. + inv H; intuition. +Qed. + +Lemma etrans_ret_inv' {E B X} : forall x l t, + etrans l (Ret x) t -> + (l = τ /\ @Seq E B X t (α Ret x)) \/ (l = val x /\ Seq t (α Stuck)). +Proof. + intros ? [] ? step; cbn in step. + - intuition; try (eapply trans_ret in step; now apply step). + apply trans_ret_inv' in H; intuition. + - eapply trans_ret_inv' in step; intuition. + - eapply trans_ret_inv' in step; intuition. + - eapply trans_ret_inv' in step; intuition. Qed. Lemma etrans_ret_inv {E B X} : forall x l (t : ctree E B X), @@ -848,11 +956,56 @@ Lemma etrans_ret_inv {E B X} : forall x l (t : ctree E B X), Proof. intros ? [] ? step; cbn in step. - intuition; try (eapply trans_ret in step; now apply step). - inv H. + apply trans_ret_inv in H; intuition. + inv H; intuition. + - eapply trans_ret_inv in step; intuition. - eapply trans_ret_inv in step; intuition. - eapply trans_ret_inv in step; intuition. Qed. +Lemma passive_τ_trans {E B X Y} e (g : X -> ctree E B Y) u : + trans τ (β e g) u -> + False. +Proof. + intros TR; cbn in TR; dependent induction TR. +Qed. + +Lemma passive_τ_etrans {E B X Y} e (g : X -> ctree E B Y) u : + etrans τ (β e g) u -> + Seq u (β e g). +Proof. + intros [TR | EQ]. + - cbn in TR; dependent induction TR. + - symmetry; apply EQ. +Qed. + +Lemma passive_τ_wtrans {E B X Y} e (g : X -> ctree E B Y) u : + wtrans τ (β e g) u -> + Seq u (β e g). +Proof. + intros [? [? [n TR1] TR2] [m TR3]]. + destruct n. + - cbn in TR1. rewrite <- TR1 in TR2. + apply passive_τ_etrans in TR2. + destruct m. + * cbn in TR3. + now rewrite <- TR3, TR2. + * destruct TR3 as [? TR _]. + rewrite TR2 in TR. + exfalso; eapply passive_τ_trans; eauto. + - destruct TR1 as [? TR _]. + exfalso; eapply passive_τ_trans; eauto. +Qed. + +Lemma transs_τ_passive {E B X Y} e (g : X -> ctree E B Y) u : + (trans τ)^* (β e g) u -> + Seq u (β e g). +Proof. + intros TR. + eapply passive_τ_wtrans. + now apply wtrans_τ. +Qed. + (*| Stuck processes --------------- @@ -864,19 +1017,28 @@ is not. Section stuck. Context {E B : Type -> Type} {X : Type}. - Variable (l : @label E) (t u : ctree E B X). - Definition is_stuck : ctree E B X -> Prop := + Definition is_stuck : @S E B X -> Prop := fun t => forall l u, ~ (trans l t u). - #[global] Instance is_stuck_equ : Proper (equ eq ==> iff) is_stuck. + #[global] Instance Seq_is_stuck : Proper (Seq ==> iff) is_stuck. Proof. intros ? ? EQ; split; intros ST; red; intros * ABS. rewrite <- EQ in ABS; eapply ST; eauto. rewrite EQ in ABS; eapply ST; eauto. Qed. - Lemma etrans_is_stuck_inv (v v' : ctree E B X) : + Lemma etrans_is_stuck_inv' v v' l : + is_stuck v -> + etrans l v v' -> + l = τ /\ Seq v v'. + Proof. + intros * ST TR. + edestruct @etrans_case'; eauto. + apply ST in H; tauto. + Qed. + + Lemma etrans_is_stuck_inv (v v' : ctree E B X) l : is_stuck v -> etrans l v v' -> (l = τ /\ v ≅ v'). @@ -886,32 +1048,52 @@ Section stuck. apply ST in H; tauto. Qed. - Lemma transs_is_stuck_inv (v v' : ctree E B X) : + Lemma transs_is_stuck_inv' v v' : is_stuck v -> (trans τ)^* v v' -> - v ≅ v'. + Seq v v'. Proof. intros * ST TR. - destruct TR as [[] TR]; intuition. + destruct TR as [[] TR]. + inv TR; eauto. destruct TR. apply ST in H; tauto. Qed. + + Lemma transs_is_stuck_inv (v v' : ctree E B X) : + is_stuck v -> + (trans τ)^* v v' -> + v ≅ v'. + Proof. + intros * ST TR. + eapply transs_is_stuck_inv' in TR; eauto. + now inv TR. + Qed. - Lemma wtrans_is_stuck_inv : + Lemma wtrans_is_stuck_inv t u l : is_stuck t -> wtrans l t u -> - (l = τ /\ t ≅ u). + (l = τ /\ Seq t u). Proof. intros * ST TR. destruct TR as [? [? ?] ?]. - apply transs_is_stuck_inv in H; auto. - rewrite H in ST; apply etrans_is_stuck_inv in H0 as [-> ?]; auto. - rewrite H0 in ST; apply transs_is_stuck_inv in H1; auto. - intuition. - rewrite H, H0; auto. - Qed. - - Lemma Stuck_is_stuck : + apply transs_is_stuck_inv' in H; auto. + rewrite H in ST. + inv H. + - apply etrans_is_stuck_inv' in H0 as [-> ?]; auto. + inv H. + rewrite EQ0 in ST; apply transs_is_stuck_inv' in H1; auto. + intuition. + rewrite EQ, EQ0; auto. + - pose proof etrans_is_stuck_inv' _ _ ST H0 as [-> ?]; auto. + split; auto. + rewrite <-H in H1. + apply transs_τ_passive in H1. + rewrite H1. auto. + Qed. + + (* Constructions *) + Lemma stuck_is_stuck : is_stuck Stuck. Proof. repeat intro; eapply trans_stuck_inv; eauto. @@ -920,51 +1102,51 @@ Section stuck. Lemma br_void_is_stuck (c : B void) (k : void -> _) : is_stuck (Br c k). Proof. - red. intros. intro. inv H; destruct x. + red. intros * ?. + apply trans_br_inv in H as [[] ?]. Qed. Lemma br_fin0_is_stuck (c : B (fin 0)) (k : fin 0 -> _) : is_stuck (Br c k). Proof. - red. intros. intro. inv H; now apply case0. + red. intros * ?. + apply trans_br_inv in H as [? ?]. + now apply case0. Qed. - Lemma spinD_gen_is_stuck {Y} (x : B Y) : + Lemma spin_gen_is_stuck {Y} (x : B Y) : is_stuck (spin_gen x). Proof. red; intros * abs. - remember (spin_gen x) as v. - assert (EQ: v ≅ spin_gen x) by (subst; reflexivity); clear Heqv; revert EQ; rewrite ctree_eta. - induction abs; auto; try now (rewrite ctree_eta; intros abs; step in abs; inv abs). - - intros EQ; apply IHabs. - rewrite <- ctree_eta. - rewrite ctree_eta in EQ. - step in EQ; cbn in *. - dependent induction EQ; auto. - - intros EQ; apply IHabs. - rewrite <- ctree_eta. - rewrite ctree_eta in EQ. - step in EQ; cbn in *. - dependent induction EQ; auto. + rem_weak (α (@spin_gen E B X _ x)) as v. + revert EQ. + cbn in abs; induction abs. + 3-6: intros EQ; inv EQ; rewrite EQ0 in H; step in H; inv H. + - intros EQ; inv EQ. + apply IHabs; constructor. + rewrite H0. + rewrite EQ0 in H; step in H; dependent induction H. + symmetry; apply REL. + - intros EQ; inv EQ. + apply IHabs; constructor. + rewrite EQ0 in H; step in H; dependent induction H. Qed. Lemma spin_is_stuck : is_stuck spin. Proof. red; intros * abs. - remember spin as v. - assert (EQ: v ≅ spin) by (subst; reflexivity); clear Heqv; revert EQ; rewrite ctree_eta. - induction abs; auto; try now (rewrite unfold_spin; intros abs; step in abs; inv abs). - - intros EQ; apply IHabs. - rewrite <- ctree_eta. - rewrite unfold_spin in EQ. - step in EQ. - dependent induction EQ; auto. - - intros EQ; apply IHabs. - rewrite <- ctree_eta. - rewrite unfold_spin in EQ. - step in EQ. - dependent induction EQ; auto. + rem_weak (α @spin E B X) as v; revert EQ. + cbn in abs; induction abs. + 3-6: intros EQ; inv EQ; rewrite EQ0 in H; step in H; inv H. + - intros EQ; inv EQ. + apply IHabs; constructor. + rewrite H0. + rewrite EQ0 in H; step in H; dependent induction H. + - intros EQ; inv EQ. + apply IHabs; constructor. + rewrite EQ0 in H; step in H; dependent induction H. + now rewrite <- REL. Qed. Lemma spinS_is_not_stuck : @@ -973,11 +1155,95 @@ Section stuck. red; intros * abs. apply (abs τ spinS). rewrite ctree_eta at 1; cbn. - constructor; auto. + apply trans_step. + Qed. + + Lemma vis_is_not_stuck {Y} (e : E Y) (k : Y -> _) : + ~ is_stuck (Vis e k). + Proof. + red; intros * abs. + eapply (abs (ask e)). + apply trans_ask. + Qed. + + Lemma passive_is_not_stuck {Y} `{Inhabited Y} (e : E Y) (k : Y -> _) : + ~ is_stuck (β e k). + Proof. + red; intros * abs. + eapply (abs (rcv e inhabitant)). + apply trans_rcv. + Qed. + + Lemma passive_void_is_stuck (e : E void) (k : void -> _) : + is_stuck (β e k). + Proof. + red; intros * abs. + apply trans_passive_inv' in abs as ([] & _ & _). Qed. End stuck. +Section not_stuck. + + Context {E B : Type -> Type} {X : Type}. + + Definition not_stuck t := + exists l' t', @trans E B X l' t t'. + + #[global] Instance seq_not_stuck : Proper (Seq ==> iff) not_stuck. + Proof. + intros ? ? EQ; split; intros (l' & t' & TR). + rewrite EQ in TR; red; eauto. + rewrite <- EQ in TR; red; eauto. + Qed. + + (* Converse is classically true *) + Lemma not_stuck_is_stuck : + forall t, not_stuck t -> ~ is_stuck t. + Proof. + intros t (l' & t' & NS) IS; eapply IS; eauto. + Qed. + + Lemma ret_not_stuck x: + not_stuck (Ret x). + Proof. + red; eauto. + Qed. + + Lemma vis_not_stuck {Y} (e : E Y) k: + not_stuck (Vis e k). + Proof. + red; eauto. + Qed. + + Lemma passive_not_stuck {Y} `{Inhabited Y} (e : E Y) k: + not_stuck (β e k). + Proof. + red; eauto. + Unshelve. + exact inhabitant. + Qed. + + Lemma br_not_stuck {Y} (b : B Y) (k : Y -> ctree _ _ _): + (exists x, not_stuck (k x)) -> + not_stuck (Br b k). + Proof. + intros (y & l' & t' & TR). + red; eauto. + Qed. + + Lemma brS_not_stuck {Y} (b : B Y) (k : Y -> ctree _ _ _): + (exists x, not_stuck (k x)) -> + not_stuck (BrS b k). + Proof. + intros (y & l' & t' & TR). + red; eauto. + Unshelve. exact y. + Qed. + +End not_stuck. +#[global] Hint Unfold not_stuck : core. + (*| wtrans theory --------------- @@ -993,7 +1259,16 @@ Section wtrans. Proof. intros * TR. eapply wcons; eauto. - apply trans_step. + Qed. + + Lemma trans_τ_str_ret_inv' : forall x t, + (trans τ)^* (Ret x) t -> + @Seq E B X t (α Ret x). + Proof. + intros * [[|] step]. + - cbn in *; now symmetry. + - destruct step. + apply trans_ret_inv' in H; intuition congruence. Qed. Lemma trans_τ_str_ret_inv : forall x (t : ctree E B X), @@ -1001,9 +1276,9 @@ Section wtrans. t ≅ Ret x. Proof. intros * [[|] step]. - - cbn in *; symmetry; eauto. + - inv step; now symmetry. - destruct step. - apply trans_ret_inv in H; intuition congruence. + apply trans_ret_inv' in H; intuition congruence. Qed. Lemma wtrans_ret_inv : forall x l (t : ctree E B X), @@ -1012,28 +1287,30 @@ Section wtrans. Proof. intros * step. destruct step as [? [? step1 step2] step3]. - apply trans_τ_str_ret_inv in step1. + apply trans_τ_str_ret_inv' in step1. rewrite step1 in step2; clear step1. - apply etrans_ret_inv in step2 as [[-> EQ] |[-> EQ]]. + apply etrans_ret_inv' in step2 as [[-> EQ] |[-> EQ]]. rewrite EQ in step3; apply trans_τ_str_ret_inv in step3; auto. rewrite EQ in step3. - apply transs_is_stuck_inv in step3; [| apply Stuck_is_stuck]. + apply transs_is_stuck_inv in step3; [| apply stuck_is_stuck]. intuition. Qed. - Lemma wtrans_val_inv' : forall (x : X) (t v : ctree E B X), - wtrans (val x) t v -> - exists u, wtrans τ t u /\ trans (val x) u v /\ v ≅ Stuck. + Lemma wtrans_val_inv' : forall (x : X) t u, + wtrans (val x) t u -> + exists t', @wtrans E B X τ t t' /\ @trans E B X (val x) t' u /\ Seq u Stuck. Proof. intros * TR. destruct TR as [t2 [t1 step1 step2] step3]. - pose proof trans_val_inv step2 as EQ. - rewrite EQ in step3, step2. - apply transs_is_stuck_inv in step3; auto using Stuck_is_stuck. - exists t1; repeat split. - apply wtrans_τ, step1. - rewrite <- step3; auto. - symmetry; auto. + exists t1; split. + apply wtrans_τ; auto. + clear step1. + pose proof trans_val_inv' step2. + rewrite H in step3. + apply transs_is_stuck_inv' in step3; auto using stuck_is_stuck. + split; [| rewrite <- step3; auto]. + rewrite H in step2. rewrite <- step3. + auto. Qed. End wtrans. @@ -1045,159 +1322,176 @@ trans l (t >>= k) u -> (trans l t t' /\ u ≅ t' >>= k) \/ (trans (ret x) t stuc l <> val x -> trans l t u -> trans l (t >>= k) (u >>= k) trans (val x) t stuck -> trans l (k x) u -> trans l (bind t k) u. |*) -Lemma trans_bind_inv_aux {E B X Y} l T U : - trans_ l T U -> - forall (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B Y), - go T ≅ t >>= k -> - go U ≅ u -> - (~ (is_val l) /\ exists t', trans l t t' /\ u ≅ t' >>= k) \/ - (exists (x : X), trans (val x) t Stuck /\ trans l (k x) u). -Proof. - intros TR; induction TR; intros. - - - rewrite unfold_bind in H; setoid_rewrite (ctree_eta t0). - desobs t0. - + right. - exists r; split. - constructor. - rewrite <- H. - apply (Transbr _ x); auto. - rewrite <- H0; auto. - + step in H; inv H. - + step in H; dependent induction H. - + step in H; dependent induction H. - + step in H; dependent induction H. - + step in H; dependent induction H. - specialize (IHTR (k1 x) k0 u). - destruct IHTR as [(? & ? & ? & ?) | (? & ? & ?)]; auto. - rewrite <- ctree_eta, REL; reflexivity. - left; split; eauto. - exists x0; split; auto. - apply (Transbr _ x); auto. - right. - exists x0; split; auto. - apply (Transbr _ x); auto. - - - symmetry in H; apply guard_equ_bind in H. - destruct H as [(? & EQ & EQ') | (? & EQ & EQ')]. - + right. - exists x; split; [rewrite EQ; constructor |]. - rewrite EQ'; auto. - rewrite <- H0; constructor; auto. - + destruct (IHTR x k u). - rewrite EQ', <- ctree_eta; auto. - auto. - destruct H as (?& (? & ? & ?)); left; split; eauto. - eexists; split. - rewrite EQ; constructor; apply H1. - auto. - destruct H as (? & ? & ?). - right; eexists; split; eauto. - rewrite EQ; constructor. - apply H. - - symmetry in H0; apply step_equ_bind in H0. - destruct H0 as [(? & EQ & EQ') | (? & EQ & EQ')]. - + right. - exists x; split; [rewrite EQ; constructor |]. - rewrite EQ'; constructor. - rewrite <- ctree_eta in H1; rewrite <- H1; auto. - + left; split; [apply is_val_τ |]. - eexists; split; [rewrite EQ; constructor; reflexivity |]. - rewrite <- H1, <- ctree_eta, H, <-EQ'; auto. - - symmetry in H0; apply vis_equ_bind in H0. - destruct H0 as [(? & EQ & EQ') | (? & EQ & EQ')]. - + right. - exists x0; split; [rewrite EQ; constructor |]. - rewrite EQ'; constructor. - rewrite <- ctree_eta in H1; rewrite <- H1; auto. - + left; split; [apply is_val_obs |]. - eexists; split; [rewrite EQ; constructor; reflexivity |]. - rewrite <- H1, <- ctree_eta, <- H, <-EQ'; auto. - - symmetry in H; apply ret_equ_bind in H. - destruct H as (? & EQ & EQ'). - right. - exists x; split; [rewrite EQ; constructor |]. - rewrite EQ', <- H0; econstructor. -Qed. -Lemma trans_bind_inv {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B Y) l : +Lemma trans_bind_inv {E B X Y} + (t : ctree E B X) (k : X -> ctree E B Y) u l : trans l (t >>= k) u -> - (~ (is_val l) /\ exists t', trans l t t' /\ u ≅ t' >>= k) \/ - (exists (x : X), trans (val x) t Stuck /\ trans l (k x) u). + (l = τ /\ exists t', trans l t (α t') /\ Seq u (α t' >>= k)) \/ + (exists Z (e : E Z), l = ask e /\ + exists (g : Z -> ctree E B X), trans l t (β e g) /\ Seq u (β e (fun x => g x >>= k))) \/ + (exists (x : X), trans (val x) t Stuck /\ trans l (k x) u). Proof. intros TR. - eapply trans_bind_inv_aux. - apply TR. - rewrite <- ctree_eta; reflexivity. - rewrite <- ctree_eta; reflexivity. + rem_weak (α x <- t ;; k x) as ob. + revert t EQ. + induction TR. + - intros ? EQ. + inv EQ. + rewrite EQ0 in H. + apply br_equ_bind in H as [(r & EQ1 & EQ2) | (v & EQ1 & EQ2)]. + + right; right. + exists r; split. + rewrite EQ1; auto. + rewrite EQ2. + apply trans_br with x. + rewrite <- H0; auto. + + edestruct IHTR as [H | [H | H]]; [rewrite H0, EQ2; reflexivity |..]; clear IHTR. + * destruct H as (-> & u' & EQ1' & EQ2'). + left. split; auto. + eexists; split; [| eassumption]; rewrite EQ1; eauto. + * destruct H as (Z & e & -> & g & TR' & EQ). + right; left. + exists Z,e; split; auto; exists g; split; auto. + rewrite EQ1; eauto. + * destruct H as (y & TR' & TR''). + right; right. + exists y; split; auto. + rewrite EQ1; eauto. + + - intros ? EQ. + inv EQ. + rewrite EQ0 in H. + apply guard_equ_bind in H as [(r & EQ1 & EQ2) | (v & EQ1 & EQ2)]. + + right; right. + exists r; split. + rewrite EQ1; auto. + rewrite EQ2; auto. + + edestruct IHTR as [H | [H | H]]; [rewrite <- EQ2; reflexivity | ..]; clear IHTR. + * destruct H as (-> & u' & EQ1' & EQ2'). + left. split; auto. + eexists; split; [| eassumption]; rewrite EQ1; auto. + * destruct H as (Z & e & -> & g & TR' & EQ). + right; left. + exists Z,e; split; auto; exists g; split; auto. + rewrite EQ1; auto. + * destruct H as (x & TR' & TR''). + right; right. + exists x; split; auto. + rewrite EQ1; auto. + + - intros ? EQ. + inv EQ. + rewrite EQ0 in H. + apply step_equ_bind in H as [(r & EQ1 & EQ2) | (v & EQ1 & EQ2)]. + + right; right. + exists r; split. + rewrite EQ1; auto. + rewrite EQ2, H0; auto. + + left. + split; auto. + exists v; split. + rewrite EQ1; auto. + rewrite H0, <- EQ2; auto. + + - intros ? EQ. + inv EQ. + rewrite EQ0 in H. + apply vis_equ_bind in H as [(r & EQ1 & EQ2) | (v & EQ1 & EQ2)]. + + right; right. + exists r; split. + rewrite EQ1; auto. + rewrite EQ2; auto. + + right; left. + exists X0, e; split; auto. + exists v; split. + rewrite EQ1; auto. + constructor. + intros ?. + rewrite EQ2; auto. + + - intros ? EQ. + inv EQ. + + - intros ? EQ. + inv EQ. + rewrite EQ0 in H. + apply ret_equ_bind in H as (r' & EQ1 & EQ2). + right; right. + exists r'; split. + rewrite EQ1; auto. + rewrite EQ2, H0; auto. Qed. - -Lemma trans_bind_inv_l {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B Y) l : + +Lemma trans_bind_inv_l {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) u l : trans l (t >>= k) u -> exists l' t', trans l' t t'. Proof. intros TR. apply trans_bind_inv in TR. - destruct TR as [(? & ? & ? & ?) | (? & ? & ?)]; eauto. + destruct TR as [(? & ? & ? & ?) | [(? & ? & ? & ? & ? & ?) | (? & ? & ?)]]; eauto. Qed. -Lemma trans_bind_l {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B X) l : - ~ (@is_val E l) -> - trans l t u -> - trans l (t >>= k) (u >>= k). +Lemma trans_bind_l_τ {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B X) : + trans τ t u -> + trans τ (t >>= k) (u >>= k). Proof. - cbn; unfold transR; intros NOV TR. + cbn; intros TR. dependent induction TR; cbn in *. - - rewrite unfold_bind, <- x. - cbn. - econstructor. - now apply IHTR. - - rewrite unfold_bind, <- x; cbn. - constructor. + - rewrite H, bind_br. + apply trans_br with x. + specialize (IHTR t' k u eq_refl eq_refl eq_refl). + now rewrite H0 in IHTR. + - rewrite H, bind_guard. + apply trans_guard. apply IHTR; auto. - - rewrite unfold_bind. - rewrite <- x0; cbn. - econstructor. - now rewrite <- H, (ctree_eta u0), x, <- ctree_eta. - - rewrite unfold_bind. - rewrite <- x1; cbn. - econstructor. - rewrite H. - rewrite (ctree_eta t0),x,<- ctree_eta. - reflexivity. - - exfalso; eapply NOV; constructor. + - rewrite H, bind_step. + rewrite H0; apply trans_step. Qed. -Lemma trans_bind_r {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B Y) x l : +Lemma trans_bind_l_ask {E B X Y Z} (t : ctree E B X) (k : X -> ctree E B Y) (e : E Z) (g : Z -> ctree E B X) : + trans (ask e) t (β e g) -> + trans (ask e) (t >>= k) (β e (fun x => g x >>= k)). +Proof. + cbn; intros TR. + dependent induction TR; cbn in *. + - rewrite H, bind_br. + apply trans_br with x. + specialize (IHTR Z t' k e g eq_refl eq_refl eq_refl). + now rewrite H0 in IHTR. + - rewrite H, bind_guard. + apply trans_guard. + apply IHTR; auto. + - rewrite H, bind_vis. + apply trans_ask. +Qed. + +Lemma trans_bind_r {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) u x l : trans (val x) t Stuck -> trans l (k x) u -> trans l (t >>= k) u. Proof. - cbn; unfold transR; intros TR1. - genobs t ot. - remember (observe Stuck) as oc. - remember (val x) as v. - revert t x Heqot Heqoc Heqv. - induction TR1; intros; try (inv Heqv; fail). - - subst. - rewrite (ctree_eta t0), <- Heqot; cbn; econstructor. - eapply IHTR1; eauto. - - rewrite (ctree_eta t0), <- Heqot; cbn; econstructor. + cbn; intros TR1. + dependent induction TR1; cbn in *. + - intros TR2; rewrite H, bind_br. + apply trans_br with x0. + rewrite <- H0; eapply IHTR1; eauto. + - intros TR2; rewrite H, bind_guard. + apply trans_guard. eapply IHTR1; eauto. - - dependent induction Heqv. - rewrite (ctree_eta t), <- Heqot, unfold_bind; cbn; auto. + - intros TR2; rewrite H, bind_ret_l; auto. Qed. -Lemma is_stuck_bind : forall {E B X Y} - (t : ctree E B X) (k : X -> ctree E B Y), +Lemma is_stuck_bind : forall {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y), is_stuck t -> is_stuck (bind t k). Proof. repeat intro. - apply trans_bind_inv in H0 as []. - - destruct H0 as (? & ? & ? & ?). - now apply H in H1. - - destruct H0 as (? & ? & ?). - now apply H in H0. + apply trans_bind_inv in H0 as [|[]]. + - destruct H0 as (? & ? & TR & ?). + now apply H in TR. + - destruct H0 as (? & ? & ? & ? & TR & ?). + now apply H in TR. + - destruct H0 as (? & TR & ?). + now apply H in TR. Qed. (*| @@ -1205,26 +1499,29 @@ Forward and backward rules for [wtrans] w.r.t. [bind] ----------------------------------------------------- |*) -Lemma etrans_bind_inv {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B Y) l : +Lemma etrans_bind_inv {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) u l : etrans l (t >>= k) u -> - (~ (is_val l) /\ exists t', etrans l t t' /\ u ≅ t' >>= k) \/ - (exists (x : X), trans (val x) t Stuck /\ etrans l (k x) u). + (l = τ /\ exists t', etrans l t (α t') /\ Seq u (t' >>= k)) \/ + (exists Z (e : E Z), l = ask e /\ + exists (g : Z -> ctree E B X), trans l t (β e g) /\ Seq u (β e (fun x => g x >>= k))) \/ + (exists (x : X), trans (val x) t Stuck /\ etrans l (k x) u). Proof. intros TR. - apply @etrans_case in TR as [ | (-> & ?)]. - - apply trans_bind_inv in H as [[? (? & ? & ?)]|( ? & ? & ?)]; eauto. - left; split; eauto. - eexists; split; eauto; apply trans_etrans; auto. - right; eexists; split; eauto; apply trans_etrans; auto. - - left; split. - intros abs; inv abs. + apply @etrans_case' in TR as [ | (-> & ?)]. + - apply trans_bind_inv in H as [[? (? & ? & ?)]|[( ? & ? & ? & ? & ? & ?)|( ? & ? & ?)]]; eauto. + + subst; left; split; eauto using is_val_τ. + eexists; split; eauto; apply trans_etrans; auto. + + subst; right; left. + eexists; eexists; split; eauto. + + right; right; eexists; split; eauto. now apply trans_etrans. + - inv H; left; split; auto. exists t; split; auto using enil; symmetry; auto. Qed. -Lemma transs_bind_inv {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B Y) : +Lemma transs_bind_inv {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) u : (trans τ)^* (t >>= k) u -> - (exists t', (trans τ)^* t t' /\ u ≅ t' >>= k) \/ - (exists (x : X), wtrans (val x) t Stuck /\ (trans τ)^* (k x) u). + (exists t', (trans τ)^* t (α t') /\ Seq u (t' >>= k)) \/ + (exists (x : X), wtrans (val x) t Stuck /\ (trans τ)^* (k x) u). Proof. intros [n TR]. revert t k u TR. @@ -1234,7 +1531,7 @@ Proof. exists 0%nat; reflexivity. symmetry; auto. - destruct TR as [t1 TR1 TR2]. - apply trans_bind_inv in TR1 as [(_ & t2 & TR1 & EQ) | (x & TR1 & TR1')]. + apply trans_bind_inv in TR1 as [(_ & t2 & TR1 & EQ) | [(x & TR1 & abs & ?) | (x & TR1 & TR1')]]. + rewrite EQ in TR2; clear t1 EQ. apply IH in TR2 as [(t3 & TR2 & EQ')| (x & TR2 & TR3)]. * left; eexists; split; eauto. @@ -1242,12 +1539,14 @@ Proof. apply wtrans_τ; auto. * right; exists x; split; eauto. eapply wcons; eauto. + + inv abs. + right. exists x; split. apply trans_wtrans; auto. - exists (S n), t1; auto. + exists (Datatypes.S n), t1; auto. Qed. + (*| Things are a bit ugly with [wtrans], we end up with three cases: - the reduction entirely takes place in the prefix @@ -1259,50 +1558,127 @@ in the prefix. This is a bit more annoying to express: we cannot necessarily just before the [Ret] some invisible br nodes. We therefore have to introduce the last visible state reached by [wtrans] and add a [trans (val _)] afterward. |*) -Lemma wtrans_bind_inv {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B Y) l : +Lemma wtrans_bind_inv {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) u l : wtrans l (t >>= k) u -> - (~ (is_val l) /\ exists t', wtrans l t t' /\ u ≅ t' >>= k) \/ - (exists (x : X), wtrans (val x) t Stuck /\ wtrans l (k x) u) \/ - (exists (x : X) s, wtrans l t s /\ trans (val x) s Stuck /\ wtrans τ (k x) u). + (l = τ /\ exists t', wtrans l t (α t') /\ Seq u (t' >>= k)) \/ + (exists Y (e : E Y), l = ask e /\ exists g, wtrans l t (β e g) /\ Seq u (β e (fun x => g x >>= k))) \/ + (exists (x : X), wtrans (val x) t Stuck /\ wtrans l (k x) u) \/ + (exists (x : X) s, wtrans l t s /\ trans (val x) s Stuck /\ wtrans τ (k x) u). Proof. intros TR. destruct TR as [t2 [t1 step1 step2] step3]. apply transs_bind_inv in step1 as [(u1 & TR1 & EQ1)| (x & TR1 & TR1')]. - - rewrite EQ1 in step2; clear t1 EQ1. - apply etrans_bind_inv in step2 as [(H & u2 & TR2 & EQ2)| (x & TR2 & TR2')]. - + rewrite EQ2 in step3; clear t2 EQ2. + - rewrite EQ1 in step2. + apply etrans_bind_inv in step2 as [(H & u2 & TR2 & EQ2)| [(Z & e & EQ & g & TR2 & EQ2) | (x & TR2 & TR2')]]. + + rewrite EQ2 in step3. + subst. apply transs_bind_inv in step3 as [(u3 & TR3 & EQ3)| (x & TR3 & TR3')]. * left; split; auto. - eexists; split; eauto. - exists u2; auto; exists u1; auto. - * right; right. + eexists; split. 2:apply EQ3. + exists (α u2); [exists (α u1) |]; auto. + * right; right; right. apply wtrans_val_inv in TR3 as (u3 & TR2' & TR2''). exists x, u3. split; [|split]; auto. 2:apply wtrans_τ; auto. - exists u2; [exists u1; assumption | ]. + exists (α u2); [exists (α u1) |]; auto. apply wtrans_τ; apply wtrans_τ in TR1. eapply wconss; eauto. - + right; left. + + destruct t2 as [? | h]; [inv EQ2 |]. + dependent induction EQ2. + assert (Seq u (β (e) k0)). + { apply passive_τ_wtrans, wtrans_τ; auto. } + right; left. + exists Z, e; split; auto. + eexists; split. + 2:rewrite H; constructor; intros x; rewrite (EQ x); reflexivity. + exists (β (e) g); [exists (α u1) |]; auto. + apply wtrans_τ; apply wnil. + + right; right; left. exists x; split. eexists; [eexists |]; eauto; apply wtrans_τ, wnil. eexists; [eexists |]; eauto; apply wtrans_τ, wnil. - - right; left. + - right; right; left. exists x; split; eauto. eexists; [eexists |]; eauto. Qed. -Lemma etrans_bind_l {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B X) l : - ~ is_val l -> - etrans l t u -> - etrans l (t >>= k) (u >>= k). +Lemma etrans_bind_l_τ {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B X) : + etrans τ t u -> + etrans τ (t >>= k) (u >>= k). +Proof. + cbn. + intros [|]. + left; apply trans_bind_l_τ; auto. + inv H; rewrite EQ; auto. +Qed. + +Lemma etrans_bind_l_ask {E B X Y Z} (t : ctree E B X) (k : X -> ctree E B Y) (e : E Z) (g : Z -> ctree E B X) : + etrans (ask e) t (β e g) -> + etrans (ask e) (t >>= k) (β e (fun x => g x >>= k)). Proof. - destruct l; cbn; try apply trans_bind_l; auto. - intros NOV [|]. - left; apply trans_bind_l; auto. - right; rewrite H; auto. + cbn; intros TR. + apply trans_bind_l_ask; auto. Qed. +Lemma trans_τ_inv {E B X} t u : + @trans E B X τ t u -> + exists u', Seq u (α u'). +Proof. + intros TR; cbn in TR; dependent induction TR. + - edestruct IHTR; auto. + inv H1; eauto. + - edestruct IHTR; eauto. + - eauto. +Qed. + +Lemma etrans_τ_inv {E B X} (t : ctree E B X) u : + etrans τ (α t) u -> + exists u', Seq u (α u'). +Proof. + intros [TR | TR]. + - eapply trans_τ_inv; eauto. + - cbn in *; exists t; rewrite TR; auto. +Qed. + +Lemma trans_ask_inv {E B X Y} t (e : E Y) u : + @trans E B X (ask e) t u -> + exists g, Seq u (β e g). +Proof. + intros TR; cbn in TR; dependent induction TR. + - edestruct IHTR; auto. + dependent induction H1; eauto. + - edestruct IHTR; eauto. + - eauto. +Qed. + +Lemma etrans_ask_inv {E B X Y} (t : ctree E B X) (e : E Y) u : + etrans (ask e) (α t) u -> + exists g, Seq u (β e g). +Proof. + intros TR; eapply trans_ask_inv; eauto. +Qed. + +Lemma transs_τ_active {E B X} (t : ctree E B X) u : + (trans τ)^* (α t) u -> + exists u', Seq u (α u'). +Proof. + intros [n TR]. revert t TR. + induction n as [| n IH]; intros t TR. + - cbn in TR; exists t; symmetry; eauto. + - destruct TR as [? TR TRs]. + eapply trans_τ_inv in TR as [u' EQ]. + rewrite EQ in TRs. + edestruct IH; eauto. +Qed. + +Lemma wtrans_τ_active {E B X} (t : ctree E B X) u : + wtrans τ (α t) u -> + exists u', Seq u (α u'). +Proof. + intros TR; apply wtrans_τ in TR; eapply transs_τ_active; eauto. +Qed. + Lemma transs_bind_l {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B X) : (trans τ)^* t u -> (trans τ)^* (t >>= k) (u >>= k). @@ -1310,29 +1686,58 @@ Proof. intros [n TR]. revert t u TR. induction n as [| n IH]. - - cbn; intros; exists 0%nat; cbn; rewrite TR; reflexivity. + - cbn; intros; exists 0%nat; cbn; inv TR; rewrite EQ; auto. - intros t u [v TR1 TR2]. + pose proof trans_τ_inv TR1 as (v' & EQv). + rewrite EQv in TR1,TR2. apply IH in TR2. eapply wtrans_τ, wcons. - apply trans_bind_l; eauto; intros abs; inv abs. - apply wtrans_τ; eauto. + 2:apply wtrans_τ; eauto. + apply trans_bind_l_τ; eauto. Qed. -Lemma wtrans_bind_l {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B X) l : - ~ (@is_val E l) -> - wtrans l t u -> - wtrans l (t >>= k) (u >>= k). +Lemma wtrans_bind_l_τ {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B X) : + wtrans τ t u -> + wtrans τ (t >>= k) (u >>= k). Proof. - intros NOV [t2 [t1 TR1 TR2] TR3]. + intros [t2 [t1 TR1 TR2] TR3]. + pose proof transs_τ_active TR1 as (x & EQx). + rewrite EQx in TR1,TR2. + pose proof etrans_τ_inv TR2 as (y & EQy). + rewrite EQy in TR2,TR3. + pose proof transs_τ_active TR3 as (z & EQz). eexists; [eexists |]. apply transs_bind_l; eauto. - apply etrans_bind_l; eauto. + apply etrans_bind_l_τ; eauto. apply transs_bind_l; eauto. Qed. -Lemma wtrans_case {E B X} (t u : ctree E B X) l: +Lemma wtrans_bind_l_ask {E B X Y Z} (t : ctree E B X) (k : X -> ctree E B Y) (e : E Z) (g : Z -> ctree E B X) : + wtrans (ask e) t (β e g) -> + wtrans (ask e) (t >>= k) (β e (fun x => g x >>= k)). +Proof. + intros [t2 [t1 TR1 TR2] TR3]. + pose proof transs_τ_active TR1 as (x & EQx). + rewrite EQx in TR1,TR2. + pose proof etrans_ask_inv TR2 as (y & EQy). + rewrite EQy in TR2,TR3. + pose proof transs_τ_passive TR3 as EQz. + eexists; [eexists |]. + apply transs_bind_l; eauto. + apply etrans_bind_l_ask; eauto. + apply wtrans_τ. + assert (Seq (β (e) (fun x0 : Z => x <- y x0;; k x)) (β (e) (fun x0 : Z => x <- g x0;; k x))). + { dependent induction EQz. + constructor; intros a. + now rewrite <- (EQ a). } + rewrite H. apply wnil. +Qed. + +Lemma wtrans_case_active {E B X} (t u : ctree E B X) l: wtrans l t u -> - t ≅ u \/ (exists v, trans l t v /\ wtrans τ v u) \/ (exists v, trans τ t v /\ wtrans l v u). + (l = τ /\ t ≅ u) \/ + (exists v, trans l t v /\ wtrans τ v u) \/ + (exists v, trans τ t v /\ wtrans l v u). Proof. intros [t2 [t1 [n TR1] TR2] TR3]. destruct n as [| n]. @@ -1343,6 +1748,7 @@ Proof. cbn in H; rewrite <- H in TR3. apply wtrans_τ in TR3. destruct TR3 as [[| n] ?]; eauto. + cbn in H0; inv H0; eauto. destruct H0 as [? ? ?]; right; left; eexists; split; eauto. apply wtrans_τ; exists n; auto. - destruct TR1 as [? ? ?]. @@ -1352,44 +1758,95 @@ Proof. exists n; eauto. Qed. -Lemma wtrans_case' {E B X} (t u : ctree E B X) l: - wtrans l t u -> - match l with - | τ => (t ≅ u \/ exists v, trans τ t v /\ wtrans τ v u) - | _ => (exists v, trans l t v /\ wtrans τ v u) \/ - (exists v, trans τ t v /\ wtrans l v u) - end. +Lemma trans_rcv_inv {E B X Y} (e : E Y) (y : Y) u v : + trans (rcv e y) u v -> + exists (g : Y -> ctree E B X), Seq u (β e g) /\ Seq v (α g y). Proof. - intros [t2 [t1 [n TR1] TR2] TR3]. - destruct n as [| n]. - - apply wtrans_τ in TR3. - cbn in TR1; rewrite <- TR1 in TR2. - destruct l; eauto. - destruct TR2; eauto. - cbn in H; rewrite <- H in TR3. - apply wtrans_τ in TR3. - destruct TR3 as [[| n] ?]; eauto. - destruct H0 as [? ? ?]; right; eexists; split; eauto. - apply wtrans_τ; exists n; auto. - - destruct TR1 as [? ? ?]. - destruct l; right. - all:eexists; split; eauto. - all:exists t2; [exists t1|]; eauto. - all:exists n; eauto. + intros TR. + remember (rcv e y). + revert e y Heql. + induction TR; intros * EQl; subst; auto; inv_equ. + - edestruct IHTR as (g & abs & ?); [reflexivity |]. + inv abs. + - edestruct IHTR as (g & abs & ?); [reflexivity |]. + inv abs. + - inv EQl. + - dependent induction EQl. + exists k; split; auto. + now rewrite <- H. + - inv EQl. +Qed. + +Lemma trans_rcv_active_inv {E B X Y} (e : E Y) (y : Y) (u : ctree E B X) v : + trans (rcv e y) (α u) v -> + False. +Proof. + intros TR; pose proof trans_rcv_inv TR as (? & abs & ?); inv abs. Qed. -Lemma wtrans_Stuck_inv {E B R} : +Lemma wtrans_stuck {E B X} l t : + wtrans l (Stuck : ctree E B X) t -> + l = τ /\ Seq t (Stuck : ctree E B X). +Proof. + intros WTR. + destruct l. + 1: split; auto. + 2-4:exfalso. + apply wtrans_τ in WTR as [[|n] WTR]. + now symmetry. + exfalso; destruct WTR as [? TR WTR]. + eapply trans_stuck_inv; eauto. + all: destruct WTR as [t2 [t1 TR1 TR2] TR3]. + all: destruct TR1 as [[|n] TR1]. + all: cbn in TR1; try (rewrite <- TR1 in TR2; eapply trans_stuck_inv; now eauto). + all: destruct TR1 as [? TR WTR]; eapply trans_stuck_inv; now apply TR. +Qed. + +Lemma wtrans_stuck' {E B R} : forall (t : ctree E B R) l, wtrans l Stuck t -> match l with | τ => t ≅ Stuck | _ => False end. Proof. intros * TR. - apply wtrans_case' in TR. - destruct l; break; cbn in *. - symmetry; auto. - all: exfalso; eapply Stuck_is_stuck; now apply H. + pose proof wtrans_stuck TR as [-> EQ]. + now inv EQ. Qed. +Lemma wtrans_case_passive {E B X Y} (t : ctree E B X) (e : E Y) (g : Y -> ctree E B X) l: + wtrans l t (β e g) -> + (l = ask e /\ exists v h, wtrans τ t (α v) /\ trans (ask e) v (β e h) /\ Seq (β e h) (β e g)). +Proof. + intros [t2 [t1 TR1 TR2] TR3]. + apply wtrans_τ in TR1. + pose proof wtrans_τ_active TR1 as [? EQ1]. + rewrite EQ1 in *. + destruct l. + - pose proof etrans_τ_inv TR2 as [? EQ2]. + rewrite EQ2 in *. + apply wtrans_τ in TR3. + pose proof wtrans_τ_active TR3 as [? EQ3]. + inv EQ3. + - cbn in TR2. + pose proof trans_ask_inv TR2 as [h EQ]. + rewrite EQ in *; clear t2 EQ. + clear t1 EQ1. + apply wtrans_τ in TR3. + pose proof passive_τ_wtrans TR3 as EQ. + dependent induction EQ. + split; auto. + exists x, h; split; auto. + split; auto. + now constructor. + - exfalso. + eapply trans_rcv_active_inv; eauto. + - exfalso. + apply trans_val_inv' in TR2. + rewrite TR2 in TR3. + apply wtrans_τ in TR3. + apply wtrans_stuck in TR3 as [_ EQ]. + inv EQ. +Qed. + Lemma pwtrans_case {E B X} (t u : ctree E B X) l: pwtrans l t u -> (exists v, trans l t v /\ wtrans τ v u) \/ (exists v, trans τ t v /\ wtrans l v u). @@ -1412,52 +1869,118 @@ It's a bit annoying that we need two cases in this lemma, but if by taking the [Ret] in the prefix, but we cannot process it to reach [u] in the bound computation. |*) -Lemma wtrans_bind_r {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B Y) x l : + +Lemma wtrans_bind_r_τ {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B Y) x : wtrans (val x) t Stuck -> - wtrans l (k x) u -> - (u ≅ k x \/ wtrans l (t >>= k) u). + wtrans τ (k x) u -> + (u ≅ k x \/ wtrans τ (t >>= k) u). Proof. intros TR1 TR2. apply wtrans_val_inv in TR1 as (t' & TR1 & TR1'). - eapply wtrans_bind_l in TR1; [| intros abs; inv abs]. - apply wtrans_case in TR2 as [? | [|]]. + pose proof wtrans_τ_active TR1 as (a & EQa). + rewrite EQa in TR1. + eapply wtrans_bind_l_τ in TR1. + apply wtrans_case_active in TR2 as [[? ?] | [|(v & TR & WTR)]]. - left; symmetry; assumption. - - right;eapply wconss; [apply TR1 | clear t TR1]. - destruct H as (? & ? & ?). - eapply trans_bind_r in TR1'; eauto. - eapply wsnocs; eauto. - apply trans_wtrans; auto. - - right;eapply wconss; [apply TR1 | clear t TR1]. + - right; eapply wconss; [apply TR1 | clear t TR1]. destruct H as (? & ? & ?). + rewrite EQa in TR1'; clear t' EQa. + pose proof trans_τ_inv H as [? EQ]. + rewrite EQ in H,H0. + eapply trans_bind_r in H; [| eauto]. + eapply wcons; eauto. + - right; eapply wconss; [apply TR1 | clear t TR1]. + rewrite EQa in TR1'. + pose proof trans_τ_inv TR as [? EQ]. + rewrite EQ in TR,WTR. eapply trans_bind_r in TR1'; eauto. eapply wconss; [|eauto]. apply trans_wtrans; auto. Qed. -Lemma wtrans_bind_r' {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B Y) x l : +Lemma wtrans_bind_r_val {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) x (y : Y) : wtrans (val x) t Stuck -> - pwtrans l (k x) u -> - (wtrans l (t >>= k) u). + wtrans (val y) (k x) Stuck -> + wtrans (val y) (t >>= k) Stuck. Proof. intros TR1 TR2. apply wtrans_val_inv in TR1 as (t' & TR1 & TR1'). - eapply wtrans_bind_l in TR1; [| intros abs; inv abs]. - apply pwtrans_case in TR2 as [? | ]. - - eapply wconss; [apply TR1 | clear t TR1]. - destruct H as (? & ? & ?). - eapply trans_bind_r in TR1'; eauto. - eapply wsnocs; eauto. - apply trans_wtrans; auto. - - eapply wconss; [apply TR1 | clear t TR1]. - destruct H as (? & ? & ?). + pose proof wtrans_τ_active TR1 as (a & EQa). + rewrite EQa in TR1, TR1'; clear t' EQa. + eapply wconss. + eapply wtrans_bind_l_τ, TR1. + clear t TR1. + apply wtrans_case_active in TR2 as [[abs ?] | [(v & TR & WTR)|(v & TR & WTR)]]. + - inv abs. + - eapply wsnocs; eauto. + apply trans_wtrans. + pose proof trans_val_inv' TR as EQ; rewrite EQ in TR |-*. + eapply trans_bind_r; eauto. + - pose proof trans_τ_inv TR as [? EQ]. + rewrite EQ in TR,WTR. eapply trans_bind_r in TR1'; eauto. eapply wconss; [|eauto]. apply trans_wtrans; auto. Qed. +Lemma wtrans_bind_r_ask {E B X Y Z} (t : ctree E B X) (k : X -> ctree E B Y) (e : E Z) (u : Z -> ctree E B Y) x : + wtrans (val x) t Stuck -> + wtrans (ask e) (k x) (β e u) -> + wtrans (ask e) (t >>= k) (β e u). +Proof. + intros TR1 TR2. + apply wtrans_val_inv in TR1 as (t' & TR1 & TR1'). + apply wtrans_case_passive in TR2 as (_ & v & h & WTR & TR & EQ). + rewrite <- EQ. + clear u EQ. + pose proof wtrans_τ_active TR1 as [? EQ]. + rewrite EQ in *; clear t' EQ. + eapply wconss. + eapply wtrans_bind_l_τ, TR1. + clear t TR1. + apply wtrans_case_active in WTR as [[_ EQ] | [(?v & TRv & WTRv) | (?v & TRv & WTRv)]]. + - rewrite <- EQ in *. + clear v EQ. + apply trans_wtrans. + eapply trans_bind_r; eauto. + - pose proof trans_τ_inv TRv as [? EQ]. + rewrite EQ in *; clear v0 EQ. + eapply wcons. + eapply trans_bind_r; eauto. + eapply wconss; eauto. + now apply trans_wtrans. + - pose proof trans_τ_inv TRv as [? EQ]. + rewrite EQ in *; clear v0 EQ. + eapply wcons. + eapply trans_bind_r; eauto. + eapply wconss; eauto. + now apply trans_wtrans. +Qed. + +(* Lemma wtrans_bind_r' {E B X Y} (t : ctree E B X) (k : X -> ctree E B Y) (u : ctree E B Y) x l : *) +(* wtrans (val x) t Stuck -> *) +(* pwtrans l (k x) u -> *) +(* (wtrans l (t >>= k) u). *) +(* Proof. *) +(* intros TR1 TR2. *) +(* apply wtrans_val_inv in TR1 as (t' & TR1 & TR1'). *) +(* eapply wtrans_bind_l in TR1; [| intros abs; inv abs]. *) +(* apply pwtrans_case in TR2 as [? | ]. *) +(* - eapply wconss; [apply TR1 | clear t TR1]. *) +(* destruct H as (? & ? & ?). *) +(* eapply trans_bind_r in TR1'; eauto. *) +(* eapply wsnocs; eauto. *) +(* apply trans_wtrans; auto. *) +(* - eapply wconss; [apply TR1 | clear t TR1]. *) +(* destruct H as (? & ? & ?). *) +(* eapply trans_bind_r in TR1'; eauto. *) +(* eapply wconss; [|eauto]. *) +(* apply trans_wtrans; auto. *) +(* Qed. *) + Lemma trans_val_invT {E B R R'} : - forall (t u : ctree E B R) (v : R'), - trans (val v) t u -> + forall t u (v : R'), + @trans E B R (val v) t u -> R = R'. Proof. intros * TR. @@ -1465,37 +1988,37 @@ Proof. induction TR; intros; auto; try now inv Heqov. Qed. -Lemma wtrans_bind_lr {E B X Y} (t u : ctree E B X) (k : X -> ctree E B Y) (v : ctree E B Y) x l : - pwtrans l t u -> - wtrans (val x) u Stuck -> - pwtrans τ (k x) v -> - (wtrans l (t >>= k) v). -Proof. - intros [t2 [t1 TR1 TR1'] TR1''] TR2 TR3. - exists (x <- t2;; k x). - - assert (~ is_val l). - { - destruct l; try now intros abs; inv abs. - exfalso. - pose proof (trans_val_invT TR1'); subst. - apply trans_val_inv in TR1'. - rewrite TR1' in TR1''. - apply transs_is_stuck_inv in TR1''; [| apply Stuck_is_stuck]. - rewrite <- TR1'' in TR2. - apply wtrans_is_stuck_inv in TR2; [| apply Stuck_is_stuck]. - destruct TR2 as [abs _]; inv abs. - } - eexists. - 2:apply trans_etrans, trans_bind_l; eauto. - apply wtrans_τ; eapply wtrans_bind_l; [intros abs; inv abs| apply wtrans_τ; auto]. - - apply wtrans_τ. - eapply wconss. - eapply wtrans_bind_l; [intros abs; inv abs| apply wtrans_τ; eauto]. - eapply wtrans_bind_r'; eauto. -Qed. - -Lemma trans_trigger : forall {E B X Y} (e : E X) x (k : X -> ctree E B Y), - trans (obs e x) (trigger e >>= k) (k x). +(* Lemma wtrans_bind_lr {E B X Y} (t u : ctree E B X) (k : X -> ctree E B Y) (v : ctree E B Y) x l : *) +(* pwtrans l t u -> *) +(* wtrans (val x) u Stuck -> *) +(* pwtrans τ (k x) v -> *) +(* (wtrans l (t >>= k) v). *) +(* Proof. *) +(* intros [t2 [t1 TR1 TR1'] TR1''] TR2 TR3. *) +(* exists (x <- t2;; k x). *) +(* - assert (~ is_val l). *) +(* { *) +(* destruct l; try now intros abs; inv abs. *) +(* exfalso. *) +(* pose proof (trans_val_invT TR1'); subst. *) +(* apply trans_val_inv in TR1'. *) +(* rewrite TR1' in TR1''. *) +(* apply transs_is_stuck_inv in TR1''; [| apply stuck_is_stuck]. *) +(* rewrite <- TR1'' in TR2. *) +(* apply wtrans_is_stuck_inv in TR2; [| apply stuck_is_stuck]. *) +(* destruct TR2 as [abs _]; inv abs. *) +(* } *) +(* eexists. *) +(* 2:apply trans_etrans, trans_bind_l; eauto. *) +(* apply wtrans_τ; eapply wtrans_bind_l; [intros abs; inv abs| apply wtrans_τ; auto]. *) +(* - apply wtrans_τ. *) +(* eapply wconss. *) +(* eapply wtrans_bind_l; [intros abs; inv abs| apply wtrans_τ; eauto]. *) +(* eapply wtrans_bind_r'; eauto. *) +(* Qed. *) + +Lemma trans_trigger : forall {E B X Y} (e : E X) (k : X -> ctree E B Y), + trans (ask e) (trigger e >>= k) (β e k). Proof. intros. unfold CTree.trigger. @@ -1504,8 +2027,8 @@ Proof. constructor; auto. Qed. -Lemma trans_trigger' : forall {E B X Y} (e : E X) x (t : ctree E B Y), - trans (obs e x) (trigger e;; t) t. +Lemma trans_trigger' : forall {E B X Y} (e : E X) (t : ctree E B Y), + trans (ask e) (trigger e;; t) (β e (fun _ => t)). Proof. intros. unfold CTree.trigger. @@ -1516,241 +2039,219 @@ Qed. Lemma trans_trigger_inv : forall {E B X Y} (e : E X) (k : X -> ctree E B Y) l u, trans l (trigger e >>= k) u -> - exists x, u ≅ k x /\ l = obs e x. + Seq u (β e k) /\ l = ask e. Proof. intros * TR. unfold trigger in TR. - apply trans_bind_inv in TR. - destruct TR as [(? & ? & TR & ?) |(? & TR & ?)]. - - apply trans_vis_inv in TR. - destruct TR as (? & ? & ->); eexists; split; eauto. - rewrite H0, H1, bind_ret_l; reflexivity. - - apply trans_vis_inv in TR. - destruct TR as (? & ? & abs); inv abs. + rewrite bind_vis in TR. + apply trans_vis_inv' in TR as [EQ ->]. + setoid_rewrite bind_ret_l in EQ. + split; auto. Qed. Lemma trans_branch : forall {E B : Type -> Type} {X : Type} {Y : Type} - [l : label] [t t' : ctree E B X] (c : B Y) (k : Y -> ctree E B X) (x : Y), - trans l t t' -> k x ≅ t -> trans l (branch c >>= k) t'. + [l : label E] [t t' : ctree E B X] (c : B Y) (k : Y -> ctree E B X) (x : Y), + trans l (k x) t' -> + trans l (branch c >>= k) t'. Proof. intros. - setoid_rewrite bind_branch. + rewrite bind_branch. eapply trans_br; eauto. Qed. -(*| -[wf_val] states that a [label] is well-formed: -if it is a [val] it should be of the right type. -|*) -Definition wf_val {E} X l := forall Y (v : Y), l = @val E Y v -> X = Y. +(* (*| *) +(* [wf_val] states that a [label] is well-formed: *) +(* if it is a [val] it should be of the right type. *) +(* |*) *) +(* Definition wf_val {E} X l := forall Y (v : Y), l = @val E Y v -> X = Y. *) + +(* Lemma wf_val_val {E} X (v : X) : wf_val X (@val E X v). *) +(* Proof. *) +(* red. intros. apply val_eq_invT in H. assumption. *) +(* Qed. *) + +(* Lemma wf_val_nonval {E} X (l : @label E) : ~is_val l -> wf_val X l. *) +(* Proof. *) +(* red. intros. subst. exfalso. apply H. constructor. *) +(* Qed. *) + +(* Lemma wf_val_trans {E B X} (l : @label E) t t' : *) +(* @trans E B X l t t' -> wf_val X l. *) +(* Proof. *) +(* red. intros. subst. *) +(* now apply trans_val_invT in H. *) +(* Qed. *) + +(* Lemma wf_val_is_val_inv : forall {E} X (l : @label E), *) +(* is_val l -> *) +(* wf_val (E := E) X l -> *) +(* exists (x : X), l = val x. *) +(* Proof. *) +(* intros. *) +(* destruct H. red in H0. *) +(* specialize (H0 X0 x eq_refl). subst. eauto. *) +(* Qed. *) + +(* (*| If the LTS has events of type [L +' R] then *) +(* it is possible to step it as either an [L] LTS *) +(* or [R] LTS ignoring the other. *) +(* *) *) +(* Section Coproduct. *) +(* Arguments label: clear implicits. *) +(* Context {L R C: Type -> Type} {X: Type}. *) +(* Notation S := (ctree (L +' R) C X). *) +(* Notation S' := (ctree' (L +' R) C X). *) +(* Notation SP := (SS -> label (L +' R) -> Prop). *) + +(* (* Skip an [R] event *) *) +(* Inductive srtrans_: rel S' S' := *) +(* | IgnoreR {X} (e : R X) k x t : *) +(* srtrans_ (observe (k x)) t -> *) +(* srtrans_ (VisF (inr1 e) k) t. *) + +(* (* Skip an [L] event *) *) +(* Inductive sltrans_: rel S' S' := *) +(* | IgnoreL {X} (e : L X) k x t : *) +(* sltrans_ (observe (k x)) t -> *) +(* sltrans_ (VisF (inl1 e) k) t. *) + +(* Hint Constructors srtrans_ sltrans_: core. *) + +(* (* Make those relations that respect equality [srel] *) *) +(* Program Definition srtrans : srel SS SS := *) +(* {| hrel_of := (fun (u v: SS) => srtrans_ (observe u) (observe v)) |}. *) +(* Next Obligation. split; induction 1; auto. Defined. *) + +(* Program Definition sltrans : srel SS SS := *) +(* {| hrel_of := (fun (u v: SS) => sltrans_ (observe u) (observe v)) |}. *) +(* Next Obligation. split; induction 1; auto. Defined. *) + +(* (*| Obs transition on the left, ignores right transitions and [τ] |*) *) +(* Definition ltrans {X}(l: L X)(x: X): srel SS SS := *) +(* (trans τ ⊔ srtrans)^* ⋅ trans (obs (inl1 l) x) ⋅ (trans τ ⊔ srtrans)^*. *) + +(* (*| Obs transition on the right, ignores left transitions and [τ] |*) *) +(* Definition rtrans {X}(r: R X)(x: X): srel SS SS := *) +(* (trans τ ⊔ sltrans)^* ⋅ trans (obs (inr1 r) x) ⋅ (trans τ ⊔ sltrans)^*. *) + +(* End Coproduct. *) + +#[global] Notation htrans l u v := (hrel_of (trans l) u v) (only parsing). -Lemma wf_val_val {E} X (v : X) : wf_val X (@val E X v). -Proof. - red. intros. apply val_eq_invT in H. assumption. -Qed. - -Lemma wf_val_nonval {E} X (l : @label E) : ~is_val l -> wf_val X l. -Proof. - red. intros. subst. exfalso. apply H. constructor. -Qed. - -Lemma wf_val_trans {E B X} (l : @label E) (t t' : ctree E B X) : - trans l t t' -> wf_val X l. -Proof. - red. intros. subst. - now apply trans_val_invT in H. -Qed. +(*| +[refine_transition H]: given a transition whose concrete label is known, +derive information on the active/passive status of its destination state. -Lemma wf_val_is_val_inv : forall {E} X (l : @label E), - is_val l -> - wf_val (E := E) X l -> - exists (x : X), l = val x. -Proof. - intros. - destruct H. red in H0. - specialize (H0 X0 x eq_refl). subst. eauto. -Qed. +Currently very partial +|*) +Ltac refine_trans_in h := + match type of h with + | htrans τ _ _ => + let u := fresh "u" in + let EQ := fresh "EQ" in + pose proof trans_τ_inv h as [u EQ]; + rewrite EQ in *; + match type of EQ with + | Seq ?a _ => try clear a EQ + end + | htrans (ask ?e) _ _ => + let u := fresh "u" in + let EQ := fresh "EQ" in + pose proof trans_ask_inv h as [u EQ]; + rewrite EQ in *; + match type of EQ with + | Seq ?a _ => try clear a EQ + end + end. -(*| If the LTS has events of type [L +' R] then - it is possible to step it as either an [L] LTS - or [R] LTS ignoring the other. -*) -Section Coproduct. - Arguments label: clear implicits. - Context {L R C: Type -> Type} {X: Type}. - Notation S := (ctree (L +' R) C X). - Notation S' := (ctree' (L +' R) C X). - Notation SP := (SS -> label (L +' R) -> Prop). - - (* Skip an [R] event *) - Inductive srtrans_: rel S' S' := - | IgnoreR {X} (e : R X) k x t : - srtrans_ (observe (k x)) t -> - srtrans_ (VisF (inr1 e) k) t. - - (* Skip an [L] event *) - Inductive sltrans_: rel S' S' := - | IgnoreL {X} (e : L X) k x t : - sltrans_ (observe (k x)) t -> - sltrans_ (VisF (inl1 e) k) t. - - Hint Constructors srtrans_ sltrans_: core. - - (* Make those relations that respect equality [srel] *) - Program Definition srtrans : srel SS SS := - {| hrel_of := (fun (u v: SS) => srtrans_ (observe u) (observe v)) |}. - Next Obligation. split; induction 1; auto. Defined. - - Program Definition sltrans : srel SS SS := - {| hrel_of := (fun (u v: SS) => sltrans_ (observe u) (observe v)) |}. - Next Obligation. split; induction 1; auto. Defined. - - (*| Obs transition on the left, ignores right transitions and [τ] |*) - Definition ltrans {X}(l: L X)(x: X): srel SS SS := - (trans τ ⊔ srtrans)^* ⋅ trans (obs (inl1 l) x) ⋅ (trans τ ⊔ srtrans)^*. - - (*| Obs transition on the right, ignores left transitions and [τ] |*) - Definition rtrans {X}(r: R X)(x: X): srel SS SS := - (trans τ ⊔ sltrans)^* ⋅ trans (obs (inr1 r) x) ⋅ (trans τ ⊔ sltrans)^*. - -End Coproduct. +Tactic Notation "refine_trans" := + match goal with + | h : htrans _ _ _ |- _ => refine_trans_in h + end. +Tactic Notation "refine_trans" "in" ident(h) := refine_trans_in h. (*| [inv_trans] is an helper tactic to automatically invert hypotheses involving [trans]. |*) -#[local] Notation trans' l t u := (hrel_of (trans l) t u). +Ltac inv_label_eq EQl := + match type of EQl with + | τ = τ => + clear EQl + | val _ = val _ => + apply val_eq_inv in EQl; try (inversion EQl; fail) + | ask _ = ask _ => + let EQt := fresh "EQt" in + let EQe := fresh "EQe" in + apply ask_invT in EQl as EQt; + symmetry in EQt; + (* subst_hyp_in EQt h; *) + apply ask_inv in EQl as EQe; + try (inversion EQe; fail) + | rcv _ _ = rcv _ _ => + let EQt := fresh "EQt" in + let EQt := fresh "EQv" in + let EQe := fresh "EQe" in + apply rcv_invT in EQl as EQt; + symmetry in EQt; + (* subst_hyp_in EQt h; *) + apply rcv_inv in EQl as [EQe EQv]; + try (inversion EQe; inversion EQv; fail) + | _ => subst; try now inv EQl + end. Ltac inv_trans_one := match goal with - (* Ret *) - | h : trans' _ (Ret ?x) _ |- _ => + | h : htrans _ (α Ret _) _ |- _ => let EQl := fresh "EQl" in - apply trans_ret_inv in h as [?EQ EQl]; - match type of EQl with - | val _ = val _ => apply val_eq_inv in EQl; try (inversion EQl; fail) - | τ = val _ => now inv EQl - | obs _ _ = val _ => now inv EQl - | _ => idtac - end - - (* Vis *) - | h : trans' _ (Vis ?e ?k) _ |- _ => - let EQl := fresh "EQl" in - apply trans_vis_inv in h as (?x & ?EQ & EQl); - match type of EQl with - | @obs _ ?X _ _ = obs _ _ => - let EQt := fresh "EQt" in - let EQe := fresh "EQe" in - let EQv := fresh "EQv" in - apply obs_eq_invT in EQl as EQt; - subst_hyp_in EQt h; - apply obs_eq_inv in EQl as [EQe EQv]; - try (inversion EQv; inversion EQe; fail) - | val _ = obs _ _ => now inv EQl - | τ = obs _ _ => now inv EQl - | _ => idtac - end + let EQ := fresh "EQ" in + (apply trans_ret_inv in h as [EQ EQl] || apply trans_ret_inv' in h as [EQ EQl]); + try rewrite EQ in *; + inv_label_eq EQl (* Step *) - | h : trans' _ (Step _) _ |- _ => + | h : htrans _ (α Step _) _ |- _ => let EQl := fresh "EQl" in - apply trans_step_inv in h as (?EQ & EQl); - match type of EQl with - | τ = τ => clear EQl - | val _ = τ => now inv EQl - | obs _ _ = τ => now inv EQl - | _ => idtac - end - - (* BrS *) - | h : trans' _ (BrS ?n ?k) _ |- _ => - let x := fresh "x" in - let EQl := fresh "EQl" in - apply trans_brS_inv in h as (x & ?EQ & EQl); - match type of EQl with - | τ = τ => clear EQl - | val _ = τ => now inv EQl - | obs _ _ = τ => now inv EQl - | _ => idtac - end - - (* brS2 *) - | h : trans' _ (brS2 _ _) _ |- _ => - let EQl := fresh "EQl" in - apply trans_brS2_inv in h as (EQl & [?EQ | ?EQ]); - match type of EQl with - | τ = τ => clear EQl - | val _ = τ => now inv EQl - | obs _ _ = τ => now inv EQl - | _ => idtac - end - - (* brS3 *) - | h : trans' _ (brS3 _ _ _) _ |- _ => - let EQl := fresh "EQl" in - apply trans_brS3_inv in h as (EQl & [?EQ | [?EQ | ?EQ]]); - match type of EQl with - | τ = τ => clear EQl - | val _ = τ => now inv EQl - | obs _ _ = τ => now inv EQl - | _ => idtac - end - - (* brS4 *) - | h : trans' _ (brS4 _ _ _ _) _ |- _ => - let EQl := fresh "EQl" in - apply trans_brS4_inv in h as (EQl & [?EQ | [?EQ | [?EQ | ?EQ]]]); - match type of EQl with - | τ = τ => clear EQl - | val _ = τ => now inv EQl - | obs _ _ = τ => now inv EQl - | _ => idtac - end + let EQ := fresh "EQ" in + apply trans_step_inv' in h as (EQ & EQl); + try rewrite EQ in *; + inv_label_eq EQl + + (* Br *) + | h : htrans _ (α Br _ _) _ |- _ => + let TR := fresh "TR" in + apply trans_br_inv in h as (?n & TR) (* Guard *) - | h : trans' _ (Guard _) _ |- _ => + | h : htrans _ (α Guard _) _ |- _ => apply trans_guard_inv in h + + (* Vis *) + | h : htrans _ (α (Vis ?e ?k)) _ |- _ => + let EQl := fresh "EQl" in + let EQ := fresh "EQ" in + apply trans_vis_inv' in h as (EQ & EQl); + try rewrite EQ in *; + inv_label_eq EQl + + (* Passive *) + | h : htrans _ (β ?e ?k) _ |- _ => + let EQl := fresh "EQl" in + let EQ := fresh "EQ" in + apply trans_passive_inv' in h as (?x & EQ & EQl); + try rewrite EQ in *; + inv_label_eq EQl - (* Br *) - | h : trans' _ (Br ?n ?k) _ |- _ => - let x := fresh "x" in - apply trans_br_inv in h as (x & ?TR) - - (* br2 *) - | h : trans' _ (br2 _ _) _ |- _ => - apply trans_br2_inv in h as [?TR | ?TR] - - (* br3 *) - | h : trans' _ (br3 _ _ _) _ |- _ => - apply trans_br3_inv in h as [?TR | [?TR | ?TR]] - - (* br4 *) - | h : trans' _ (br4 _ _ _ _) _ |- _ => - apply trans_br4_inv in h as [?TR | [?TR | [?TR | ?TR]]] - - (* Stuck *) - | h : trans' _ Stuck _ |- _ => - exfalso; eapply Stuck_is_stuck; now apply h - (* (* stuckS *) *) - (* | h : trans' _ stuckS _ |- _ => *) - (* exfalso; eapply stuckS_is_stuck; now apply h *) - - (* trigger *) - | h : trans' _ (CTree.bind (CTree.trigger ?e) ?t) _ |- _ => - apply trans_trigger_inv in h as (?x & ?EQ & ?EQl) - - end; try subs -. + end. Ltac inv_trans := repeat inv_trans_one. - + Create HintDb trans. #[global] Hint Resolve - trans_ret trans_vis trans_brS trans_br + trans_ret trans_ask trans_brS trans_br trans_guard trans_br21 trans_br22 trans_br31 trans_br32 trans_br33 @@ -1759,12 +2260,231 @@ Create HintDb trans. trans_brS21 trans_brS22 trans_brS31 trans_brS32 trans_brS33 trans_brS41 trans_brS42 trans_brS43 trans_brS44 - trans_trigger trans_bind_l trans_bind_r + trans_trigger trans_bind_l_τ trans_bind_l_ask trans_bind_r : trans. #[global] Hint Constructors is_val : trans. #[global] Hint Resolve - is_val_τ is_val_obs - wf_val_val wf_val_nonval wf_val_trans : trans. + is_val_τ + is_val_ask + is_val_rcv : trans. Ltac etrans := eauto with trans. +#[global] Arguments trans : simpl never. + + +(*| +Structured relations on labels +|*) + +Section build_rel. + + Context {E F : Type -> Type} {X Y : Type}. + + Record lrel := + { + RR: rel X Y ; + Rask: forall [X Y], E X -> F Y -> Prop ; + Rrcv: forall [X Y] (e : E X) (f : F Y), X -> Y -> Prop ; + }. + + Variant build_rel {RL : lrel} : hrel (label E) (label F) := + | rel_τ : build_rel τ τ + | rel_ask {X Y} {e : E X} {f : F Y} + (HR : Rask RL e f) : + build_rel (ask e) (ask f) + | rel_rcv {X Y} {e : E X} {f : F Y} x y + (HR : Rrcv RL e f x y) : + build_rel (rcv e x) (rcv f y) + | rel_ret {x : X} {y : Y}: + RR RL x y -> build_rel (val x) (val y). + Arguments build_rel : clear implicits. + + Lemma build_rel_val RL x y : + build_rel RL (val x) (val y) -> RR RL x y. + Proof. + now intros H; dependent induction H. + Qed. + + Lemma build_rel_ask RL A B (e : E A) (f : F B) : + build_rel RL (ask e) (ask f) -> Rask RL e f. + Proof. + now intros H; dependent induction H. + Qed. + + Lemma build_rel_rcv RL A B (e : E A) (f : F B) a b : + build_rel RL (rcv e a) (rcv f b) -> Rrcv RL e f a b. + Proof. + now intros H; dependent induction H. + Qed. + + Lemma build_rel_τ RL : + build_rel RL τ τ. + Proof. + constructor. + Qed. + +End build_rel. + +Arguments lrel : clear implicits. +Arguments build_rel {E F X Y} RL. +#[global] Hint Constructors build_rel : trans. +Coercion build_rel : lrel >-> hrel. + +Definition upd_rel {E F X Y X' Y'} + (RL : lrel E F X Y) + (SS : rel X' Y') : lrel E F X' Y' := + {| + RR := SS ; + Rask := Rask RL ; + Rrcv := Rrcv RL + |}. + +Variant eq1 {E} : forall [X Y : Type], rel (E X) (E Y) := + | Eq1 X (e : E X) : eq1 e e. +Variant eq2 {E} : forall [X Y : Type], E X -> E Y -> rel X Y := + | Eq2 X (e : E X) x : eq2 e e x x. +Hint Resolve Eq1 : trans. +Hint Resolve Eq2 : trans. + +Definition Leq {E} {X : Type} : lrel E E X X := + {| + RR := eq ; + Rask := eq1 ; + Rrcv := eq2 + |}. + +Definition Lvrel {E X Y} (RR : rel X Y) : lrel E E X Y := + {| + RR := RR ; + Rask := eq1 ; + Rrcv := eq2 + |}. + +Ltac invL := + match goal with + h: build_rel _ _ _ |- _ => dependent induction h + | h: upd_rel _ _ _ _ |- _ => dependent induction h + end. + +Definition lequiv {E F X Y} : rel (lrel E F X Y) (lrel E F X Y) := + fun L1 L2 => RR L1 == RR L2 /\ Rask L1 == Rask L2 /\ Rrcv L1 == Rrcv L2. + +#[global] Instance lequiv_equivalence {E F X Y} : Equivalence (@lequiv E F X Y). +Proof. + constructor. + - split3; auto. + - intros ?? [? []]; split3; symmetry; auto. + - intros ??? [? []] [? []]; split3; etransitivity; eauto. +Qed. + +#[global] Instance lequiv_build_rel {E F X Y} : Proper (lequiv ==> weq) (@build_rel E F X Y). +Proof. + cbn; intros L1 L2 [EQ1 [EQ2 EQ3]] l1 l2; split; intros H. + - inv H; etrans. + constructor; now apply EQ2. + constructor; now apply EQ3. + constructor; now apply EQ1. + - inv H; etrans. + constructor; now apply EQ2. + constructor; now apply EQ3. + constructor; now apply EQ1. +Qed. + +#[global] Instance lequiv_build_rel' {E F X Y} : Proper (lequiv ==> eq ==> eq ==> iff) (@build_rel E F X Y). +Proof. + now cbn; intros; subst; eapply lequiv_build_rel. +Qed. + +Definition sub_lrel {E F X Y} (L L' : lrel E F X Y) : Prop := + RR L <= RR L' /\ Rask L <= Rask L' /\ Rrcv L <= Rrcv L'. + +Lemma sub_lrel_subrel {E F X Y} : + Proper (sub_lrel ==> leq) (@build_rel E F X Y). +Proof. + intros L L' (SUB1 & SUB2 & SUB3) ?? HL. + inv HL; etrans. + now constructor; apply SUB2. + now constructor; apply SUB3. + now constructor; apply SUB1. +Qed. + +Definition flipL {E F X Y} (L : lrel E F X Y) : lrel F E Y X := + {| RR := flip (RR L) ; + Rask := fun X Y => flip (@Rask _ _ _ _ L Y X) ; + Rrcv := fun X Y f e => flip (Rrcv L e f) |}. + +Lemma flipL_flip {E F X Y} (L : lrel E F X Y) : + build_rel (flipL L) == flip (build_rel L). +Proof. + intros f e; split; cbn; intros []; constructor; auto. +Qed. + +Lemma lequiv_flipL {E F X Y} (L L' : lrel E F X Y): + lequiv L L' -> + lequiv (flipL L) (flipL L'). +Proof. + intros (EQV & EQA & EQR). + split3. + cbn; intros; apply EQV. + cbn; intros; apply EQA. + cbn; intros; apply EQR. +Qed. + +Lemma equiv_flipL {E F X Y} (L L' : lrel E F X Y): + build_rel L == build_rel L' -> + build_rel (flipL L) == build_rel (flipL L'). +Proof. + intros EQ e f; specialize (EQ f e); cbn in *. + split. + - destruct EQ as [EQ _]. + intros FL; dependent induction FL; constructor. + cbn in *. + assert (HL: L (ask f) (ask e)) by (now constructor); apply EQ in HL; dependent induction HL; auto. + assert (HL: L (rcv f y) (rcv e x)) by (now constructor); apply EQ in HL; dependent induction HL; auto. + assert (HL: L (val y) (val x)) by (now constructor); apply EQ in HL; dependent induction HL; auto. + - destruct EQ as [_ EQ]. + intros FL; dependent induction FL; constructor. + cbn in *. + assert (HL: L' (ask f) (ask e)) by (now constructor); apply EQ in HL; dependent induction HL; auto. + assert (HL: L' (rcv f y) (rcv e x)) by (now constructor); apply EQ in HL; dependent induction HL; auto. + assert (HL: L' (val y) (val x)) by (now constructor); apply EQ in HL; dependent induction HL; auto. +Qed. + +#[global] Instance flipL_reflexive {E X} (L : lrel E E X X) {LR: Reflexive L} : Reflexive (flipL L). +Proof. + intros ?. + now apply flipL_flip. +Qed. + +#[global] Instance flipL_symmetric {E X} (L : lrel E E X X) {LR: Symmetric L} : Symmetric (flipL L). +Proof. + intros l l' HL. + apply flipL_flip. + apply (flipL_flip L) in HL. + now apply LR. +Qed. + +#[global] Instance flipL_transitive {E X} (L : lrel E E X X) {LR: Transitive L} : Transitive (flipL L). +Proof. + intros l1 l2 l3 HL1 HL2. + apply flipL_flip. + apply (flipL_flip L) in HL1,HL2. + etransitivity; eauto. +Qed. + +#[global] Instance flipL_equivalence {E X} (L : lrel E E X X) {LR: Equivalence L} : Equivalence (flipL L). +Proof. + split; typeclasses eauto. +Qed. + +#[global] Instance build_rel_symmetric {E X L} `{Symmetric X L} : Symmetric (@build_rel E E X X (Lvrel L)). +Proof. + intros l l' HL. + unfold Lvrel in *. + dependent induction HL; constructor; cbn in *. + dependent induction HR; constructor. + dependent induction HR; constructor. + now apply H. +Qed. +