Library HoweSound
Require Export Howe.
Notation refl0 Rel := (∀ P, is_proc P → Rel P P).
Notation pseudo_sim :=
(∀ {V W:Set} Rel (P1 Q1:proc V)(P2 Q2:proc W) a F1 C1 (f:V → proc0)(g: W → proc0),
simulation Rel → refl0 Rel → rename_compatible Rel → (Rincl sc0 Rel) → trans Rel
→ howe Rel P2 Q2 → howe Rel P1 Q1
→ (∀ v, is_proc (f v)) → (∀ v, is_proc (g v))
→ lts (bind f P1) (inp a) (ag_abs F1) → lts (bind g P2) (out a) (ag_conc C1)
→ ∃ F2 C2 P'2 Q'2, lts (bind f Q1) (inp a) (ag_abs F2) ∧
lts (bind g Q2) (out a) (ag_conc C2) ∧
sc0 P'2 (appr F1 C1) ∧
sc0 Q'2 (appr F2 C2) ∧
howe Rel P'2 Q'2).
Notation refl0 Rel := (∀ P, is_proc P → Rel P P).
Notation pseudo_sim :=
(∀ {V W:Set} Rel (P1 Q1:proc V)(P2 Q2:proc W) a F1 C1 (f:V → proc0)(g: W → proc0),
simulation Rel → refl0 Rel → rename_compatible Rel → (Rincl sc0 Rel) → trans Rel
→ howe Rel P2 Q2 → howe Rel P1 Q1
→ (∀ v, is_proc (f v)) → (∀ v, is_proc (g v))
→ lts (bind f P1) (inp a) (ag_abs F1) → lts (bind g P2) (out a) (ag_conc C1)
→ ∃ F2 C2 P'2 Q'2, lts (bind f Q1) (inp a) (ag_abs F2) ∧
lts (bind g Q2) (out a) (ag_conc C2) ∧
sc0 P'2 (appr F1 C1) ∧
sc0 Q'2 (appr F2 C2) ∧
howe Rel P'2 Q'2).
Lemma pseudo_inp_first {V:Set}:
∀ Rel (P1 Q1:proc V)(P2 Q2:proc0) a F1 (f:V → proc0),
simulation Rel → refl0 Rel → rename_compatible Rel
→ (∀ P Q, Rel (P // PO) (Q // PO) → Rel P Q)
→ howe Rel P1 Q1 → howe Rel P2 Q2 → (∀ v, is_proc (f v))
→ lts (bind f P1) (inp a) (ag_abs F1)
→ ∃ F2, lts (bind f Q1) (inp a) (ag_abs F2) ∧
howe Rel (asubst F1 P2) (asubst F2 Q2).
Proof.
introv Hsim Hrefl Hrename HpO Hp1q1. gen a f F1 P2 Q2.
induction Hp1q1; introv Hp2q2 Hf HltsP1; try solve [inverts HltsP1].
- forwards*: IHHp1q1 Hp2q2 HltsP1. destruct H1 as [F2 [Hltsf2 Hhowe]].
forwards*: H0 f. destruct Hsim as [Hisproc Hsim].
assert (is_agent (conc_def 0 Q2 PO)).
intros_all. assert (is_proc Q2) by auto with howe.
apply is_proc_bn in H3. rewrite H3 in H2. autofs.
assert (Hwf:conc_wf (conc_def 0 Q2 PO)).
intros_all. omega.
forwards_test Rel.
destruct F2 as [R']; destruct F'0 as [Q'1]; subst. simpl in H7.
apply HpO in H7. repeat (rewrite mapN_id' in H7).
∃ (abs_def Q'1); intuition. simpl.
apply howe_comp with (subst R' Q2); eauto with howe hopi.
apply× oe_proc0.
- simpl in ×. ∃ F1; intuition. destruct F1 as [P']; simpl.
apply howe_subst; auto with howe. apply howe_refl.
forwards: lts_is_proc HltsP1; auto with howe.
- inverts HltsP1.
+ forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
forwards*: IHHp1q1_1 Hp2q2 H2. destruct H as [F'2 [Hltsf'2 Hhowe]].
∃ (abs_parl F'2 (bind f Q')). split.
eapply lts_parl'; eauto.
inverts H3. destruct F'1 as [P'1]. destruct F'2 as [Q'1]. simpl.
simpl in Hhowe. apply howe_par; auto with howe.
+ forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
forwards*: IHHp1q1_2 Hp2q2 H2. destruct H as [F'2 [Hltsf'2 Hhowe]].
∃ (abs_parr (bind f Q) F'2 ). split.
eapply lts_parr'; eauto.
inverts H3. destruct F'1 as [P'1]. destruct F'2 as [Q'1]. simpl.
simpl in Hhowe. apply howe_par; auto with howe.
- inverts HltsP1. ∃ (abs_def (bind (liftV f) Q)). split.
simpl. auto with hopi.
simpl. apply howe_subst; auto with howe. apply× @howe_bind.
intros [ |]; simpl; auto with howe.
- simpl in ×. inverts HltsP1.
pick_fresh_fset_V V
(fn (bind (fun x ⇒ mapN (fun x0 ⇒ S x0) (f x)) Q) \u
fn P2 \u fn Q2) x.
forwards: H4 x; auto.
forwards: lts_inp_abs H1. destruct H3 as [Fx].
rewrite H3 in H1.
assert (∀ y, is_proc (mapN (fun x1 ⇒ S x1) (f y)))
by auto with hopi.
rewrite× <- @bind_open in H1.
forwards*: H0 Hp2q2 H1.
destruct H6 as [F'x [ HltsF'x HhoweF'x]]. destruct F'x as [P'x].
∃ (abs_def (nu (close 0 x P'x))). split.
apply (lts_new' L) with (abs_def (close 0 x P'x)); auto.
intros. rewrite× @bind_open in HltsF'x.
forwards: lts_open HltsF'x; eauto.
rewrite× <- @bind_open. apply× @is_proc_bind.
forwards*: @howe_implies_proc (H x). intuition.
destruct H8 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
inverts Ha'. destruct A' as [ |[Q''] |[] ]; inverts H9. simpl in HxA'.
rewrite× @close_open. rewrite× subst_lab_id in HltsA'. simpl; autofs.
destruct A as [ | [] | [] ]; inverts H3. inverts H2; simpl in ×.
apply (howe_nu (L \u fn (subst p P2) \u fn (subst (close 0 x P'x) Q2))).
intros. do 2 (rewrite <- bind_open; auto with hopi).
asserts_rewrite ((fun x1 : incV Empty_set ⇒ mapN (fun x2 : nat ⇒ S x2) (subst_func P2 x1))
= subst_func P2).
extens. intros [ |]; simpl; auto. rewrite is_proc_mapN; auto with howe.
asserts_rewrite ((fun x1 : incV Empty_set ⇒ mapN (fun x2 : nat ⇒ S x2) (subst_func Q2 x1))
= subst_func Q2).
extens. intros [ |]; simpl; auto. rewrite is_proc_mapN; auto with howe.
asserts_rewrite (P'x= (open 0 x (close 0 x P'x))) in HhoweF'x.
rewrite× @open_close. forwards*: lts_is_proc HltsF'x.
forwards: @howe_implies_proc (H x); intuition.
do 2 (rewrite bind_open in HhoweF'x; auto with hopi).
forwards: @howe_rename HhoweF'x x0; auto.
autofnF.
rewrite <- bind_open; auto with hopi howe.
forwards: lts_is_proc (H4 x); auto with hopi howe.
rewrite <- bind_open; auto with hopi howe.
forwards: @howe_implies_proc (H x); intuition.
rewrite <- bind_open; auto with hopi howe.
forwards*: @howe_implies_proc (H x); destruct_hyps.
apply is_proc_bind; auto with hopi.
do 2 (rewrite <- bind_open in H3; auto with hopi).
Qed.
Lemma pseudo_inp_conc {V:Set}: ∀ Rel (P1 Q1:proc V) a F1 C (f:V → proc0),
simulation Rel → refl0 Rel → rename_compatible Rel
→ (∀ P Q, Rel (P // PO) (Q // PO) → Rel P Q)
→ howe Rel P1 Q1 → is_agent (ag_conc C) → (∀ v, is_proc (f v))
→ lts (bind f P1) (inp a) (ag_abs F1)
→ ∃ F2, lts (bind f Q1) (inp a) (ag_abs F2) ∧ howe Rel (appr F1 C) (appr F2 C).
Proof.
intros. destruct C. pick_freshes_fset_V V (fn p \u fn p0 \u fn (bind f Q1)) n l.
forwards: @pseudo_inp_first (open_list l p) (open_list l p) H2 H5; auto with hopi howe.
apply howe_refl. apply is_proc_open_list. forwards: fresh_length Fr.
simpl in H3. rewrite <- H6. intros. forwards: H3 k; autofs.
destruct H6 as [F2 [HltsF2 Hhowe]]. repeat (rewrite bind_proc0 in Hhowe).
∃ F2; intuition. destruct F1 as [P'1]; destruct F2 as [P'2]; simpl in ×.
assert (is_proc P'1). forwards: lts_is_proc H5; auto with howe.
assert (is_proc P'2). forwards: lts_is_proc HltsF2; auto with howe.
repeat (rewrite is_proc_mapN); auto. forwards: fresh_length Fr.
subst. apply× @howe_open_list.
simpl. apply fresh_union_l; auto. apply fresh_sub with (fn P'1 \u fn p).
auto. apply fn_subst.
simpl. apply fresh_union_l; auto. apply fresh_sub with (fn (bind f Q1) \u fn p).
auto. forwards: @fn_subst P'2 p. forwards: lts_fn HltsF2. simpl in H9.
assert (fn P'2 \u fn p \c fn (bind f Q1) \u fn p) by autofs. autofs.
intros. simpl in H8. autofs. apply bn_subst in H9.
rewrite× @is_proc_bn in H9. rewrite union_empty_l in H9.
forwards: H3 k; autofs; try omega. forwards: H3 k; autofs; try omega.
intros. simpl in H8. autofs. apply bn_subst in H9.
rewrite is_proc_bn in H9; auto. rewrite union_empty_l in H9.
forwards: H3 k; autofs; try omega. forwards: H3 k; autofs; try omega.
repeat (rewrite open_list_par). repeat (rewrite open_list_subst).
rewrite× (open_list_id P'1). rewrite× (open_list_id P'2).
apply howe_par; auto with howe. apply howe_refl. apply is_proc_open_list.
intros. forwards: H3 k; autofs; try omega.
Qed.
Lemma pseudo_sim_out : pseudo_sim.
Proof.
introv Hsim Hrefl Hrename Hsc0 Htrans Hp2q2.
assert (∀ P Q : proc0, Rel (P // PO) (Q // PO) → Rel P Q) as HpO.
intros. apply Htrans with (P//PO). apply Hsc0.
destruct Hsim. apply sc0_def; auto with bisim sc.
apply is_proc_sc with (P//PO); auto with bisim sc.
apply Htrans with (Q//PO); auto. apply Hsc0.
destruct Hsim. apply sc0_def; auto with bisim sc.
apply is_proc_sc with (Q//PO); auto with bisim sc.
gen a f g F1 C1 P1 Q1.
induction Hp2q2; introv Hp1q1 Hf Hg HltsP1 HltsP2; try solve [inverts HltsP2].
- forwards*: IHHp2q2 a F1 C1 P1 Q1.
destruct H1 as [F2 [C2 [ P'2 [R' [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]].
forwards*: H0 g. destruct Hsim as [Hisproc Hsim].
assert (is_agent F2) by auto with howe hopi.
forwards_test Rel.
∃ F2 C'0 P'2 (appr F2 C'0); intuition.
apply howe_comp with R'; auto with hopi howe.
apply oe_trans with (appr F2 C2); auto.
apply× oe_sc0. apply× oe_proc0.
- forwards: @pseudo_inp_conc P1 Q1 F1 C1; eauto with hopi.
destruct H as [F2 []]. ∃ F2 C1 (appr F1 C1) (appr F2 C1); intuition.
- inverts HltsP2.
+ forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
forwards*: IHHp2q2_1 Hp1q1 HltsP1 H2.
destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
inverts Hp'2. inverts Hq'2.
∃ F'2 (conc_parl C'2 (bind g Q')) (P'2// bind g P') (Q'2//bind g Q').
splits; eauto with hopi howe.
eapply lts_parl'; eauto.
apply sc0_trans with (appr F1 C'1 // bind g P'); auto with sc hopi howe.
inverts H3. assert (struct_congr
(appr F1 C'1 // bind g P') (appr F1 (conc_parl C'1 (bind g P')))).
destruct F1, C'1; simpl. eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
apply sc0_trans with (appr F'2 C'2 // bind g Q'); auto with sc hopi howe.
assert (struct_congr
(appr F'2 C'2 // bind g Q') (appr F'2 (conc_parl C'2 (bind g Q')))).
destruct F'2, C'2; simpl. eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
+ forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
forwards*: IHHp2q2_2 Hp1q1 HltsP1 H2.
destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
inverts Hp'2. inverts Hq'2.
∃ F'2 (conc_parr (bind g Q) C'2) (bind g P // P'2) (bind g Q // Q'2).
splits; eauto with hopi howe.
eapply lts_parr'; eauto.
apply sc0_trans with (bind g P // appr F1 C'1); auto with sc hopi howe.
inverts H3. assert (struct_congr
(bind g P // appr F1 C'1) (appr F1 (conc_parr (bind g P) C'1))).
destruct F1, C'1; simpl. apply sc_trans with
(genNu n (shiftN n (bind g P) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
apply sc0_trans with (bind g Q // appr F'2 C'2); auto with sc hopi howe.
assert (struct_congr (bind g Q // appr F'2 C'2)
(appr F'2 (conc_parr (bind g Q) C'2))).
destruct F'2, C'2; simpl. apply sc_trans with
(genNu n (shiftN n (bind g Q) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
- inverts HltsP2. simpl.
forwards*: @pseudo_inp_first Rel P1 Q1 (bind g P)(bind g Q).
apply @howe_bind; auto with howe. apply HltsP1.
destruct H as [F2 [HltsQ1 HhoweF1F2]]. assert (∀ F, fshiftN 0 F = F).
destruct F; simpl; rewrite× @mapN_id'.
∃ F2 (conc_def 0 (bind g Q) (bind g Q'))
(appr F1 (conc_def 0 (bind g P) (bind g P')))
(appr F2 (conc_def 0 (bind g Q) (bind g Q'))); intuition auto with hopi howe;
simpl; repeat (rewrite H); auto with sc hopi howe.
- simpl in ×. inversion HltsP2; subst.
pick_fresh_fset_V V
(fn (bind (fun x ⇒ mapN (fun x0 ⇒ S x0) (g x)) Q) \u fn (bind f Q1)) x.
forwards*: H4 x. forwards: lts_out_conc H1. destruct H3 as [Cx].
rewrite H3 in H1.
assert (∀ y, is_proc (mapN (fun x1 ⇒ S x1) (g y))) by auto with hopi.
rewrite <- bind_open in H1; auto with hopi.
forwards: H0 Hp1q1 H1; auto with hopi.
apply HltsP1.
destruct H6 as [F'1 [ C'x [ P'x [Q'x [HltsF'x [HltsC'x [Hp'x [Hq'x HhoweF'x]]]]]]]].
destruct C'x as [n P1x P2x].
assert (lts (nu bind (fun x0 ⇒ mapN (fun x1 ⇒ S x1) (g x0)) Q) (out a)
(conc_new (conc_def n (close n x P1x) (close n x P2x)))).
apply (lts_new' L) with (conc_def n (close n x P1x) (close n x P2x)); auto.
intros. rewrite bind_open in HltsC'x; auto with hopi.
forwards: lts_open HltsC'x; eauto.
rewrite <- bind_open; auto with hopi. apply is_proc_bind; auto with hopi.
forwards: @howe_implies_proc (H x); auto. intuition.
destruct H8 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
inverts Ha'. destruct A' as [ | [] |[] ]; inverts H9. simpl in HxA'.
repeat (rewrite close_open; auto). rewrite subst_lab_id in HltsA'; auto. simpl; autofs.
∃ F'1 (conc_new (conc_def n (close n x P1x) (close n x P2x)))
(nu close 0 x P'x) (nu close 0 x Q'x). splits; auto.
assert (is_agent F1) by auto with howe hopi.
assert (is_agent C1).
forwards*: @lts_is_proc HltsP2.
apply (proc_nu L). intros. unfold open. rewrite× <- @bind_open.
apply× @is_proc_bind. forwards*: H x0. auto with howe. inverts Hp'x.
apply sc0_def; auto with hopi.
apply (proc_nu L). intros. auto with hopi.
destructA A; inverts H2. fold (conc_new (conc_def n0 p p0)).
apply sc_trans with (nu appr F1 (conc_def n0 p p0)); auto with sc.
apply sc_nu'. destruct F1 as [P12].
destruct Cx as [n1 px p0x]; inverts H3. simpl in ×.
asserts_rewrite (genNu n1 (subst ((shiftN n1) P12) p // p0)
= close 0 x (genNu n1 (subst ((shiftN n1) P12)(open n1 x p) //(open n1 x p0)))).
rewrite close_genNu. simpl. fequals.
rewrite close_subst. repeat (rewrite close_open); try solve [autofnF].
rewrite× @close_id. autofnF.
apply× @sc_close.
apply sc_symmetric. apply× sc_F_newC.
forwards*: H x. forwards*: lts_is_proc H1; auto with hopi howe.
simpl in H3. rewrite <- H3 in H12.
simpl in H12. intros. destruct (classic (k=n0)); try omega.
forwards: H12 k. autobnF. omega.
assert (is_agent F'1) by auto with howe hopi.
inverts Hq'x.
apply sc0_def; auto with hopi.
apply (proc_nu L). intros. auto with hopi.
apply× is_proc_app. forwards*: @lts_is_proc H6.
apply (proc_nu L). intros. rewrite× <- @bind_open.
apply× @is_proc_bind. forwards*: H x0. auto with howe.
apply sc_trans with (nu appr F'1 (conc_def n (close n x P1x)(close n x P2x))); auto with sc.
apply sc_nu'. destruct F'1 as [P12]. simpl in ×.
asserts_rewrite (genNu n (subst ((shiftN n) P12) (close n x P1x) // (close n x P2x))
= close 0 x (genNu n (subst ((shiftN n) P12) P1x // P2x))).
rewrite close_genNu. simpl. fequals.
rewrite close_subst. fequals. fequals. rewrite× @close_id.
rewrite× @is_proc_mapN. forwards*: lts_fn HltsF'x. simpl in H11. autofnF.
apply× @sc_close.
apply sc_symmetric. apply× sc_F_newC.
forwards*: lts_is_proc HltsC'x; auto with howe hopi.
apply× @is_proc_bind. forwards*: H x. auto with howe.
simpl in H11. intros. destruct (classic (k=n)); try omega.
forwards: H11 k. autobnF. omega.
apply (howe_nu (L \u fn (close 0 x P'x) \u fn (close 0 x Q'x))).
intros. unfold open.
eapply (howe_rename _ Hrename) with x; eauto;
try solve [rewrite open_close; auto with howe].
autofnF.
rewrite open_close; auto with howe. rewrite open_close; auto with howe.
Qed.
Lemma pseudo_out_first {V:Set}: ∀ Rel (P1 Q1:proc V)(P2 Q2:proc1) a C1
(f:V → proc0), simulation Rel → refl0 Rel →
rename_compatible Rel → (Rincl sc0 Rel) → trans Rel →
howe Rel P1 Q1 → howe Rel P2 Q2 →
(∀ v, is_proc (f v)) →
lts (bind f P1) (out a) (ag_conc C1) →
∃ C2 P'2 Q'2, lts (bind f Q1) (out a) (ag_conc C2) ∧
sc0 P'2 (appr (abs_def P2) C1) ∧
sc0 Q'2 (appr (abs_def Q2) C2) ∧ howe Rel P'2 Q'2.
Proof.
introv Hsim Hrefl Hrename Hsc0 Htrans Hp1q1. gen a f C1 P2 Q2.
induction Hp1q1; introv Hp2q2 Hf HltsP1; try solve [inverts HltsP1].
- forwards*: IHHp1q1 Hp2q2 HltsP1.
destruct H1 as [C2 [P'2 [Q'2 [Hltsc2 [Hp'2 [Hq'2 Hhowe]]]]]].
forwards: H0 f; auto. destruct Hsim as [Hisproc Hsim].
assert (is_agent (abs_def Q2)) by (simpl; auto with howe).
forwards_test Rel.
∃ C'0 P'2 (appr (abs_def Q2) C'0); intuition.
apply howe_comp with Q'2; auto with hopi howe.
apply oe_trans with (appr (abs_def Q2) C2); auto.
apply× oe_sc0. apply× oe_proc0.
- simpl in ×. assert (is_agent (ag_conc C1)) by auto with hopi.
assert (is_proc (appr (abs_def P2) C1)).
apply× is_proc_app. simpl; auto with hopi howe.
assert (is_proc (appr (abs_def Q2) C1)).
apply× is_proc_app. simpl; auto with hopi howe.
∃ C1 (appr (abs_def P2) C1)(appr (abs_def Q2) C1);
intuition auto with sc.
destruct C1 as [n P Q]; simpl.
pick_freshes_fset_V V (fn P \u fn Q \u fn P2 \u fn Q2) n l.
forwards: fresh_length Fr. subst.
forwards*: @howe_subst Rel (open_list l P) (open_list l P) P2 Q2.
apply× @howe_refl. apply× @is_proc_open_list. intros. forwards: H k; autofs.
repeat (rewrite is_proc_mapN); auto with howe. apply× @howe_open_list.
simpl. apply fresh_union_l; auto.
apply fresh_sub with (fn P2 \u fn P). auto. apply fn_subst.
simpl. apply fresh_union_l; auto.
apply fresh_sub with (fn Q2 \u fn P). auto. apply fn_subst.
intros. simpl in H3. autofs. apply bn_subst in H4.
rewrite @is_proc_bn in H4; auto with howe. rewrite union_empty_l in H4.
forwards: H k; autofs; try omega. forwards: H k; autofs; try omega.
intros. simpl in H3. autofs. apply bn_subst in H4.
rewrite @is_proc_bn in H4; auto with howe. rewrite union_empty_l in H4.
forwards: H k; autofs; try omega. forwards: H k; autofs; try omega.
repeat (rewrite open_list_par). repeat (rewrite open_list_subst).
rewrite (open_list_id P2); auto with howe.
rewrite (open_list_id Q2); auto with howe.
apply howe_par; auto with howe. apply howe_refl. apply is_proc_open_list.
intros. forwards: H k; autofs; try omega.
- inverts HltsP1.
+ forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
forwards*: IHHp1q1_1 Hp2q2 H2.
destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
inverts Hp'2. inverts Hq'2.
∃ (conc_parl C'2 (bind f Q')) (P'2// bind f P') (Q'2//bind f Q').
splits; eauto with hopi howe.
eapply lts_parl'; eauto.
apply sc0_trans with (appr (abs_def P2) C'1 // bind f P');
auto with sc hopi howe.
inverts H3. assert (struct_congr
(appr (abs_def P2) C'1 // bind f P')
(appr (abs_def P2) (conc_parl C'1 (bind f P')))).
destruct C'1; simpl. eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
apply sc0_trans with (appr (abs_def Q2) C'2 // bind f Q');
auto with sc hopi howe.
assert (struct_congr
(appr (abs_def Q2) C'2 // bind f Q')
(appr (abs_def Q2) (conc_parl C'2 (bind f Q')))).
destruct C'2; simpl. eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
+ forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
forwards*: IHHp1q1_2 Hp2q2 H2.
destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
inverts Hp'2. inverts Hq'2.
∃ (conc_parr (bind f Q) C'2) (bind f P // P'2) (bind f Q // Q'2).
splits; eauto with hopi howe.
eapply lts_parr'; eauto.
apply sc0_trans with (bind f P // appr (abs_def P2) C'1);
auto with sc hopi howe.
inverts H3. assert (struct_congr
(bind f P // appr (abs_def P2) C'1)
(appr (abs_def P2) (conc_parr (bind f P) C'1))).
destruct C'1; simpl. apply sc_trans with
(genNu n (shiftN n (bind f P) // (subst ((shiftN n) P2) p // p0))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
apply sc0_trans with (bind f Q // appr (abs_def Q2) C'2); auto with sc hopi howe.
assert (struct_congr (bind f Q // appr (abs_def Q2) C'2)
(appr (abs_def Q2) (conc_parr (bind f Q) C'2))).
destruct C'2; simpl. apply sc_trans with
(genNu n (shiftN n (bind f Q) // (subst ((shiftN n) Q2) p // p0))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
- inverts HltsP1. simpl.
assert (is_proc (subst (mapN (fun x ⇒ x) P2) (bind f P) // bind f P')).
rewrite is_proc_mapN; auto with howe. auto with hopi howe.
assert (is_proc (subst (mapN (fun x ⇒ x) Q2) (bind f Q) // bind f Q')).
rewrite is_proc_mapN; auto with howe. auto with hopi howe.
∃ (conc_def 0 (bind f Q) (bind f Q'))
(appr (abs_def P2) (conc_def 0 (bind f P) (bind f P')))
(appr (abs_def Q2) (conc_def 0 (bind f Q) (bind f Q')));
simpl; intuition auto with hopi sc.
repeat (rewrite is_proc_mapN; auto with howe).
- simpl in ×. inversion HltsP1; subst.
pick_fresh_fset_V V
(fn (bind (fun x ⇒ mapN (fun x0 ⇒ S x0) (f x)) Q) \u fn Q2 \u fn P2) x.
forwards*: H4 x. forwards: lts_out_conc H1. destruct H3 as [Cx].
rewrite H3 in H1.
assert (∀ y, is_proc (mapN (fun x1 ⇒ S x1) (f y))) by auto with hopi.
rewrite <- bind_open in H1; auto with hopi.
forwards: H0 Hp2q2 H1; auto with hopi.
destruct H6 as [ C'x [ P'x [Q'x [HltsC'x [Hp'x [Hq'x HhoweF'x]]]]]].
destruct C'x as [n P1x P2x].
assert (lts (nu bind (fun x0 ⇒ mapN (fun x1 ⇒ S x1) (f x0)) Q) (out a)
(conc_new (conc_def n (close n x P1x) (close n x P2x)))).
apply (lts_new' L) with (conc_def n (close n x P1x) (close n x P2x)); auto.
intros. rewrite bind_open in HltsC'x; auto with hopi.
forwards: lts_open HltsC'x; eauto with hopi.
rewrite <- bind_open; auto with hopi. apply is_proc_bind; auto with hopi.
forwards*: @howe_implies_proc (H x). intuition.
destruct H8 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
inverts Ha'. destruct A' as [ | [] |[] ]; inverts H9. simpl in HxA'.
repeat (rewrite× @close_open). rewrite× subst_lab_id in HltsA'. simpl; autofs.
∃ (conc_new (conc_def n (close n x P1x) (close n x P2x)))
(nu close 0 x P'x) (nu close 0 x Q'x). splits×.
assert (is_agent C1).
forwards*: @lts_is_proc HltsP1.
apply (proc_nu L). intros. rewrite× <- @bind_open.
apply× @is_proc_bind. forwards*: H x0. auto with howe.
inverts Hp'x. apply sc0_def; auto with hopi.
apply (proc_nu L). intros. auto with hopi.
apply× is_proc_app. simpl; auto with howe.
destruct A as [ | [] |[] ]; inverts H2. fold (conc_new (conc_def n0 p p0)).
apply sc_trans with (nu appr (abs_def P2)(conc_def n0 p p0)); auto with sc.
apply sc_nu'. destruct Cx as [n1 px p0x]; inverts H3. simpl in ×.
asserts_rewrite (genNu n1 (subst ((shiftN n1) P2) p // p0)
= close 0 x (genNu n1 (subst ((shiftN n1) P2)(open n1 x p) //(open n1 x p0)))).
rewrite close_genNu. simpl. fequals.
rewrite close_subst. repeat (rewrite close_open); try solve [autofnF].
rewrite× @close_id. autofnF.
apply× @sc_close.
apply sc_symmetric. apply× sc_F_newC.
simpl; auto with howe.
forwards*: H x. forwards*: lts_is_proc H1; auto with hopi howe.
simpl in H3. rewrite <- H3 in H11.
simpl in H11. intros. destruct (classic (k=n0)); try omega.
forwards: H11 k. autobnF. omega.
inverts Hq'x. apply sc0_def; auto with hopi.
apply (proc_nu L). intros. auto with hopi.
apply× is_proc_app. simpl; auto with howe. forwards*: @lts_is_proc H6.
apply (proc_nu L). intros. rewrite× <- @bind_open.
apply× @is_proc_bind. forwards*: H x0. auto with howe.
apply sc_trans with (nu appr (abs_def Q2)
(conc_def n (close n x P1x)(close n x P2x))); auto with sc.
apply sc_nu'. simpl in ×.
asserts_rewrite (genNu n (subst ((shiftN n) Q2) (close n x P1x) // (close n x P2x))
= close 0 x (genNu n (subst ((shiftN n) Q2) P1x // P2x))).
rewrite close_genNu. simpl. fequals.
rewrite close_subst. do 2 fequals. rewrite× @close_id.
rewrite× @is_proc_mapN. auto with howe.
apply× @sc_close.
apply sc_symmetric. apply× sc_F_newC.
simpl; auto with howe.
forwards*: lts_is_proc HltsC'x; auto with howe hopi.
apply× @is_proc_bind. forwards*: H x. auto with howe.
simpl in H10. intros. destruct (classic (k=n)); try omega.
forwards: H10 k. autobnF. omega.
apply (howe_nu (L \u fn (close 0 x P'x) \u fn (close 0 x Q'x))).
intros. eapply (howe_rename _ Hrename) with x; eauto;
try solve [rewrite open_close; auto with howe].
autofnF.
rewrite open_close; auto with howe. rewrite open_close; auto with howe.
Qed.
Lemma pseudo_sim_in : pseudo_sim.
Proof.
introv Hsim Hrefl Hrename Hsc0 Htrans Hp2q2 Hp1q1. gen a f g F1 C1 P2 Q2.
induction Hp1q1; introv Hp2q2 Hf Hg HltsP1 HltsP2; try solve [inverts HltsP1].
- forwards*: IHHp1q1 a F1 C1 P2 Q2.
destruct H1 as [F2 [C2 [ P'2 [R' [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]].
forwards*: H0 f. destruct Hsim as [Hisproc Hsim].
assert (is_agent C2) by auto with howe hopi.
assert (conc_wf C2). forwards*: lts_conc_wf HltsR.
forwards_test Rel.
∃ F'0 C2 P'2 (appr F'0 C2); intuition.
apply howe_comp with R'; auto with hopi howe.
apply oe_trans with (appr F2 C2); auto.
apply× oe_sc0. apply× oe_proc0.
- simpl in ×. destruct F1 as [P'1].
forwards: @pseudo_out_first P2 Q2 P'1 P'1 C1; eauto with howe hopi.
destruct H as [C2 [ P'2 [Q'2 [HltsC2 [Hp'2 [Hq'2 Hhowe]]]]]].
∃ (abs_def P'1) C2 P'2 Q'2; intuition.
- inverts HltsP1.
+ forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
forwards*: IHHp1q1_1 Hp2q2 H2 HltsP2.
destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
inverts Hp'2. inverts Hq'2.
∃ (abs_parl F'2 (bind f Q')) C'2 (P'2// bind f P') (Q'2//bind f Q').
splits; eauto with hopi howe.
eapply lts_parl'; eauto.
apply sc0_trans with (appr F'1 C1 // bind f P'); auto with sc hopi howe.
inverts H3. assert (struct_congr
(appr F'1 C1 // bind f P') (appr (abs_parl F'1 (bind f P')) C1)).
destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
apply sc_trans with
(genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f P'))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
apply sc0_trans with (appr F'2 C'2 // bind f Q'); auto with sc hopi howe.
assert (struct_congr
(appr F'2 C'2 // bind f Q') (appr (abs_parl F'2 (bind f Q')) C'2)).
destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
apply sc_trans with
(genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f Q'))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
+ forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
forwards*: IHHp1q1_2 Hp2q2 H2 HltsP2.
destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
inverts Hp'2. inverts Hq'2.
∃ (abs_parr (bind f Q) F'2) C'2 (bind f P // P'2) (bind f Q // Q'2).
splits; eauto with hopi howe.
eapply lts_parr'; eauto.
apply sc0_trans with (bind f P // appr F'1 C1); auto with sc hopi howe.
inverts H3. assert (struct_congr
(bind f P // appr F'1 C1) (appr (abs_parr (bind f P) F'1) C1)).
destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
apply sc_trans with
(genNu n (shiftN n (bind f P) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
apply sc0_trans with (bind f Q // appr F'2 C'2); auto with sc hopi howe.
assert (struct_congr (bind f Q // appr F'2 C'2)
(appr (abs_parr (bind f Q) F'2) C'2)).
destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
apply sc_trans with
(genNu n (shiftN n (bind f Q) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
- inverts HltsP1. simpl. forwards*: @pseudo_out_first Rel P2 Q2 (bind (liftV f) P)(bind (liftV f) Q).
apply× @howe_bind. intros [|]; simpl; auto with howe. apply HltsP2.
destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
∃ (abs_def (bind (liftV f) Q)) C'2 P'2 Q'2; intuition.
- simpl in ×. inversion HltsP1; subst.
pick_fresh_fset_V V
(fn (bind (fun x ⇒ mapN (fun x0 ⇒ S x0) (f x)) Q) \u fn (bind g Q2)) x.
forwards*: H4 x. forwards: lts_inp_abs H1. destruct H3 as [Fx].
rewrite H3 in H1.
assert (∀ y, is_proc (mapN (fun x1 ⇒ S x1) (f y))) by auto with hopi.
rewrite <- bind_open in H1; auto with hopi.
forwards: H0 Hp2q2 H1; auto with hopi.
apply HltsP2.
destruct H6 as [F'x [ C'1 [ P'x [Q'x [HltsF'x [HltsC'1 [Hp'x [Hq'x HhoweF'x]]]]]]]].
destruct F'x as [Pfx].
assert (lts (nu bind (fun x0 ⇒ mapN (fun x1 ⇒ S x1) (f x0)) Q) (inp a)
(abs_new (abs_def (close 0 x Pfx)))).
apply (lts_new' L) with (abs_def (close 0 x Pfx)); auto.
intros. rewrite× @bind_open in HltsF'x.
forwards: lts_open HltsF'x; eauto.
rewrite <- bind_open; auto. apply is_proc_bind; auto.
forwards: @howe_implies_proc (H x); auto. intuition.
destruct H8 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
inverts Ha'. destruct A' as [ |[Q''] |[] ]; inverts H9. simpl in HxA'.
rewrite× @close_open. rewrite× subst_lab_id in HltsA'. simpl; autofs.
∃ (abs_new (abs_def (close 0 x Pfx))) C'1
(nu close 0 x P'x) (nu close 0 x Q'x). splits; auto.
assert (is_agent C1) by auto with howe hopi.
assert (is_agent F1).
forwards*: @lts_is_proc HltsP1.
apply (proc_nu L). intros. rewrite× <- @bind_open.
apply× @is_proc_bind. forwards*: H x0. auto with howe.
inverts Hp'x. apply sc0_def; auto with hopi.
apply (proc_nu L); auto with hopi.
destructA A; inverts H2.
apply sc_trans with (nu appr (abs_def p) C1); auto with sc.
apply sc_nu'. destruct C1 as [n P22 P23].
destruct Fx as [px]; inverts H3. simpl in ×.
asserts_rewrite (genNu n (subst ((shiftN n) p) P22 // P23)
= close 0 x (genNu n (subst ((shiftN n)(open 0 x p)) P22 // P23))).
rewrite close_genNu. simpl. fequals.
rewrite close_subst. rewrite mapN_open; auto using shiftN_injective.
replace (n+0) with n by omega. rewrite close_open; try solve [autofnF].
repeat (rewrite× @close_id).
apply× @sc_close. apply sc_symmetric. apply× (sc_newF_C (abs_def p)).
assert (is_agent C'1) by auto with howe hopi.
inverts Hq'x. apply sc0_def; auto with hopi.
apply (proc_nu L); auto with hopi.
apply× is_proc_app. forwards*: @lts_is_proc H6.
apply (proc_nu L). intros. rewrite× <- @bind_open.
apply× @is_proc_bind. forwards*: H x0. auto with howe.
apply sc_trans with (nu appr (abs_def (close 0 x Pfx)) C'1); auto with sc.
apply sc_nu'. destruct C'1 as [n P22 P23]. simpl in ×.
asserts_rewrite (genNu n (subst ((shiftN n)(close 0 x Pfx)) P22 // P23)
= close 0 x (genNu n (subst ((shiftN n) Pfx) P22 // P23))).
rewrite close_genNu. simpl. fequals.
rewrite close_subst. forwards*: lts_fn HltsC'1. simpl in H11.
rewrite <- mapN_close. replace (n+0) with n by omega.
repeat fequals; rewrite× @close_id.
assert (fn P22 \c fn (bind g Q2)).
apply subset_trans with (fn P22 \u fn P23); auto. autofs.
autofnF.
assert (fn P23 \c fn (bind g Q2)).
apply subset_trans with (fn P22 \u fn P23); auto. autofs.
autofnF.
apply× @sc_close.
apply sc_symmetric. apply× (sc_newF_C (abs_def (close 0 x Pfx))).
apply (howe_nu (L \u fn (close 0 x P'x) \u fn (close 0 x Q'x))).
intros. eapply (howe_rename _ Hrename) with x; eauto;
try solve [rewrite open_close; auto with howe].
autofnF.
do 2 (rewrite open_close; auto with howe).
Qed.
Simultaneous proof
Lemma pseudo_sim_sim' :
(∀ {V W:Set} Rel (P1 Q1:proc V)(P2 Q2:proc W) a F1 C1 (f:V → proc0)(g: W → proc0) n1 n2,
simulation Rel → refl0 Rel → rename_compatible Rel → (Rincl sc0 Rel) → trans Rel
→ howe' Rel P2 Q2 n2 → howe' Rel P1 Q1 n1
→ (∀ v, is_proc (f v)) → (∀ v, is_proc (g v))
→ lts (bind f P1) (inp a) (ag_abs F1) → lts (bind g P2) (out a) (ag_conc C1)
→ ∃ F2 C2 P'2 Q'2 n3, lts (bind f Q1) (inp a) (ag_abs F2) ∧
lts (bind g Q2) (out a) (ag_conc C2) ∧
sc0 P'2 (appr F1 C1) ∧
sc0 Q'2 (appr F2 C2) ∧
howe' Rel P'2 Q'2 n3).
Proof.
introv Hsim Hrefl Hrename Hsc0 Htrans.
Require Import TLC.LibWf.
assert (wf (lexico2 lt lt)).
rewrite <- LibNat.lt_peano.
apply wf_lexico2; auto with wf.
remember (n2, n1) as p. gen V W.
gen n1 n2 a F1 C1.
induction_wf IH: H p. intros n1 n2 Hp. subst.
assert (∀ (V2 : Set) (a:var) (P1 Q1 : proc1) (n1 : nat) (P2 Q2 : proc V2),
howe' Rel P1 Q1 n1
→ howe' Rel P2 Q2 n2
→ ∀ (g : V2 → proc0) (C1 : conc),
(∀ v : V2, is_proc (g v))
→ lts (bind g P2) (out a) C1
→ ∃ (C2:conc) P'2 Q'2 x3,
lts (bind g Q2) (out a) C2
∧ sc0 P'2 (appr (abs_def P1) C1)
∧ sc0 Q'2 (appr (abs_def Q1) C2) ∧ howe' Rel P'2 Q'2 x3).
{ intros.
assert (howe' Rel (a? P1) (a? Q1)(S n0)) by auto with howe.
remember (pr_var (V:=Empty_set)) as f.
assert (∀ P, bind (liftV f) P = P).
intros; rewrite× @bind_return. intros [|]; simpl; auto.
intros. inverts e.
destruct H1; try solve [inverts H3].
- forwards*: IH (k, S n0) f H6 H4 H3; try solve [subst; simpl; eauto with hopi].
destruct_hyps. assert (is_agent x) by auto with hopi howe. simpl in H8.
inverts H8. specialize (H7 g H2). destruct Hsim as [ Hbla Hsim].
rewrite H5 in ×.
forwards_test Rel.
∃ C'0 x1 (appr (abs_def Q1) C'0)(S x3); intuition.
apply howe_comp' with x2; auto with hopi howe.
apply oe_trans with (appr (abs_def Q1) x0); auto.
apply× oe_sc0. apply× oe_proc0.
- simpl in ×. assert (is_agent (ag_conc C1)) by auto with hopi.
assert (is_proc (appr (abs_def P1) C1)).
apply× is_proc_app. simpl; auto with hopi howe.
assert (is_proc (appr (abs_def Q1) C1)).
apply× is_proc_app. simpl; auto with hopi howe.
assert (∃ n3, howe' Rel (appr (abs_def P1) C1) (appr (abs_def Q1) C1) n3).
destruct C1 as [n P Q]; simpl.
pick_freshes_fset_V V2 (fn P \u fn Q \u fn P1 \u fn Q1) n l.
forwards: fresh_length Fr. subst.
forwards*: @howe_subst Rel (open_list l P) (open_list l P) P1 Q1.
eapply @howe'_implies_howe; eauto.
apply× @howe_refl. apply× @is_proc_open_list.
intros. forwards: H1 k; autofs.
apply× @howe_implies_howe'.
repeat (rewrite is_proc_mapN); auto with howe. apply× @howe_open_list.
simpl. apply fresh_union_l; auto.
apply fresh_sub with (fn P1 \u fn P). auto. apply fn_subst.
simpl. apply fresh_union_l; auto.
apply fresh_sub with (fn Q1 \u fn P). auto. apply fn_subst.
intros. simpl in H9. autofs. apply bn_subst in H10.
rewrite @is_proc_bn in H10; auto with howe. rewrite union_empty_l in H10.
forwards: H1 k; autofs; try omega. forwards: H1 k; autofs; try omega.
intros. simpl in H9. autofs. apply bn_subst in H10.
rewrite @is_proc_bn in H10; auto with howe. rewrite union_empty_l in H10.
forwards: H1 k; autofs; try omega. forwards: H1 k; autofs; try omega.
repeat (rewrite open_list_par). repeat (rewrite open_list_subst).
rewrite (open_list_id P1); auto with howe.
rewrite (open_list_id Q1); auto with howe.
apply howe_par; auto with howe. apply howe_refl. apply is_proc_open_list.
intros. forwards: H1 k; autofs; try omega.
destruct H8. ∃ C1 (appr (abs_def P1) C1)(appr (abs_def Q1) C1) x0;
intuition auto with sc.
- inverts H3.
+ forwards: lts_out_conc H8. destruct H1 as [C'1].
rewrite_all H1 in *; clear H1. simpl in H9.
forwards*: IH f H1_ H4 H8; try solve [subst; simpl; eauto with hopi].
apply lexico2_1. omega.
destruct H1 as [ F2 [ C'2 [P'2 [Q'2 [ n3 [ HltsF2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
inverts Hp'2. inverts Hq'2. inverts HltsF2.
rewrite H5 in H3,H6, H11, H10.
assert (∃ n4, howe' Rel (P'2// bind g P') (Q'2//bind g Q') n4).
apply× @howe_implies_howe'. apply howe'_implies_howe in H1_0.
apply howe'_implies_howe in Hhowe. apply× @howe_par. apply× @howe_bind.
intros; auto with howe hopi.
destruct H12.
∃ (conc_parl C'2 (bind g Q')) (P'2// bind g P') (Q'2//bind g Q') x.
splits; eauto with hopi howe.
eapply lts_parl'; eauto.
apply sc0_trans with (appr (abs_def P1) C'1 // bind g P');
auto with sc hopi howe.
inverts H9. assert (struct_congr
(appr (abs_def P1) C'1 // bind g P')
(appr (abs_def P1) (conc_parl C'1 (bind g P')))).
destruct C'1; simpl. eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H9.
apply sc0_trans with (appr (abs_def Q1) C'2 // bind g Q');
auto with sc hopi howe.
assert (struct_congr
(appr (abs_def Q1) C'2 // bind g Q')
(appr (abs_def Q1) (conc_parl C'2 (bind g Q')))).
destruct C'2; simpl. eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H13.
+ forwards: lts_out_conc H8. destruct H1 as [C'1].
rewrite_all H1 in *; clear H1. simpl in H9.
forwards*: IH f H1_0 H4 H8; try solve [subst; simpl; eauto with hopi].
apply lexico2_1. omega.
destruct H1 as [ F2 [ C'2 [P'2 [Q'2 [ n3 [ HltsF2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
inverts Hp'2. inverts Hq'2. inverts HltsF2.
rewrite H5 in H3,H6, H11, H10.
assert (∃ n4, howe' Rel (bind g P // P'2) (bind g Q // Q'2) n4).
apply× @howe_implies_howe'. apply howe'_implies_howe in H1_.
apply howe'_implies_howe in Hhowe. apply× @howe_par. apply× @howe_bind.
intros; auto with howe hopi.
destruct H12.
∃ (conc_parr (bind g Q) C'2) (bind g P // P'2) (bind g Q // Q'2) x.
splits; eauto with hopi howe.
eapply lts_parr'; eauto.
apply sc0_trans with (bind g P // appr (abs_def P1) C'1);
auto with sc hopi howe.
inverts H9. assert (struct_congr
(bind g P // appr (abs_def P1) C'1)
(appr (abs_def P1) (conc_parr (bind g P) C'1))).
destruct C'1; simpl. apply sc_trans with
(genNu n (shiftN n (bind g P) // (subst ((shiftN n) P1) p // p0))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H9.
apply sc0_trans with (bind g Q // appr (abs_def Q1) C'2); auto with sc hopi howe.
assert (struct_congr (bind g Q // appr (abs_def Q1) C'2)
(appr (abs_def Q1) (conc_parr (bind g Q) C'2))).
destruct C'2; simpl. apply sc_trans with
(genNu n (shiftN n (bind g Q) // (subst ((shiftN n) Q1) p // p0))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H13.
- inverts H3. simpl.
assert (is_proc (subst (mapN (fun x ⇒ x) P1) (bind g P) // bind g P')).
rewrite is_proc_mapN; auto with howe. auto with hopi howe.
assert (is_proc (subst (mapN (fun x ⇒ x) Q1) (bind g Q) // bind g Q')).
rewrite is_proc_mapN; auto with howe. auto with hopi howe.
assert (∃ n, howe' Rel (appr (abs_def P1) (conc_def 0 (bind g P) (bind g P')))
(appr (abs_def Q1) (conc_def 0 (bind g Q) (bind g Q'))) n).
apply× @howe_implies_howe'. simpl. apply howe'_implies_howe in H1_.
apply howe'_implies_howe in H1_0. apply howe'_implies_howe in H0.
repeat (rewrite is_proc_mapN; auto with howe).
destruct H6.
∃ (conc_def 0 (bind g Q) (bind g Q'))
(appr (abs_def P1) (conc_def 0 (bind g P) (bind g P')))
(appr (abs_def Q1) (conc_def 0 (bind g Q) (bind g Q'))) x;
intuition auto with hopi sc.
- simpl in ×. inversion H3.
pick_fresh_fset_V V2
(fn (bind (fun x ⇒ mapN (fun x0 ⇒ S x0) (g x)) Q) \u fn Q1 \u fn P1) x.
forwards*: H9 x. forwards: lts_out_conc H10. destruct H11 as [Cx].
rewrite H11 in H10.
assert (∀ y, is_proc (mapN (fun x1 ⇒ S x1) (g y))) by auto with hopi.
rewrite <- bind_open in H10; auto with hopi. forwards*: H1 x.
forwards: IH f H13 H4 H10; try solve [subst; simpl; eauto with hopi].
apply lexico2_1. omega.
destruct H14 as [ F2 [ C'x [ P'x [Q'x [n3 [HltsF2 [HltsC'x [Hp'x [Hq'x HhoweF'x]]]]]]]]].
destruct C'x as [n P1x P2x].
assert (lts (nu bind (fun x0 ⇒ mapN (fun x1 ⇒ S x1) (g x0)) Q) (out a)
(conc_new (conc_def n (close n x P1x) (close n x P2x)))).
apply (lts_new' L) with (conc_def n (close n x P1x) (close n x P2x)); auto.
intros. rewrite bind_open in HltsC'x; auto with hopi.
forwards: lts_open HltsC'x; eauto with hopi.
rewrite <- bind_open; auto with hopi.
destruct H16 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
inverts Ha'. destructA A'; inverts H17. simpl in HxA'.
repeat (rewrite close_open; auto). rewrite subst_lab_id in HltsA'; auto. simpl; autofs.
assert (∃ n, howe' Rel (nu close 0 x P'x) (nu close 0 x Q'x) n).
apply× @howe_implies_howe'.
apply (howe_nu (L \u fn (close 0 x P'x) \u fn (close 0 x Q'x))).
intros. eapply (howe_rename _ Hrename) with x; eauto;
try solve [rewrite open_close; auto with howe].
autofnF.
rewrite open_close; auto with howe. rewrite open_close; auto with howe.
apply howe'_implies_howe in HhoweF'x; auto.
destruct H15. inverts HltsF2. rewrite H5 in Hq'x, Hp'x.
∃ (conc_new (conc_def n (close n x P1x) (close n x P2x)))
(nu close 0 x P'x) (nu close 0 x Q'x) x0. splits×.
assert (is_agent C1).
forwards*: @lts_is_proc H3.
apply (proc_nu L). intros. rewrite× <- @bind_open.
apply× @is_proc_bind. forwards*: H1 x1. auto with howe.
inverts Hp'x. apply sc0_def; auto with hopi.
apply (proc_nu L); auto with hopi.
apply× is_proc_app. simpl; auto with howe.
destruct A as [ | [] |[] ]; inverts H7. fold (conc_new (conc_def n2 p p0)).
inverts H11.
apply sc_trans with (nu appr (abs_def P1)(conc_def n2 p p0)); auto with sc.
apply sc_nu'. simpl.
asserts_rewrite (genNu n2 (subst ((shiftN n2) P1) p // p0)
= close 0 x (genNu n2 (subst ((shiftN n2) P1)(open n2 x p) //(open n2 x p0)))).
rewrite close_genNu. simpl. fequals.
rewrite close_subst. repeat (rewrite close_open); try solve [autofnF].
rewrite× @close_id. autofnF.
apply× @sc_close.
apply sc_symmetric. subst. apply× sc_F_newC.
simpl; auto with howe.
forwards*: H1 x. forwards*: lts_is_proc H10; auto with hopi howe.
intros. destruct (classic (k0=n2)); try omega.
forwards: H7 k0. autobnF. omega.
inverts Hq'x.
apply sc0_def; auto with hopi.
apply (proc_nu L); auto with hopi.
apply× is_proc_app. simpl; auto with howe. forwards*: @lts_is_proc H14.
apply (proc_nu L). intros. rewrite× <- @bind_open.
apply× @is_proc_bind. forwards*: H1 x1. auto with howe.
apply sc_trans with (nu appr (abs_def Q1)
(conc_def n (close n x P1x)(close n x P2x))); auto with sc.
apply sc_nu'. simpl in ×.
asserts_rewrite (genNu n (subst ((shiftN n) Q1) (close n x P1x) // (close n x P2x))
= close 0 x (genNu n (subst ((shiftN n) Q1) P1x // P2x))).
rewrite close_genNu. simpl. fequals.
rewrite close_subst. do 2 fequals. rewrite× @close_id.
rewrite× @is_proc_mapN. auto with howe.
apply× @sc_close.
apply sc_symmetric. apply× sc_F_newC.
simpl; auto with howe.
forwards*: lts_is_proc HltsC'x; auto with howe hopi.
intros. destruct (classic (k0=n)); try omega.
forwards: H19 k0. autobnF. omega.
}
intros. destruct H2; try solve [inverts H5].
+ forwards*: IH H1 H7; try solve [simpl; eauto with hopi].
destruct H9 as [F2 [C2 [ P'2 [R' [n3 [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]]].
forwards*: H8 f. destruct Hsim as [Hisproc Hsim].
assert (is_agent C2) by auto with howe hopi.
assert (conc_wf C2). forwards*: lts_conc_wf HltsR.
forwards_test Rel.
assert (∃ n, howe' Rel P'2 (appr F'0 C2) n).
apply× @howe_implies_howe'. apply howe'_implies_howe in HhoweP1R.
apply howe_comp with R'; auto with hopi howe.
apply oe_trans with (appr F2 C2); auto.
apply× oe_sc0. apply× oe_proc0.
destruct H17. ∃ F'0 C2 P'2 (appr F'0 C2) x; intuition.
+ simpl in ×. destruct F1 as [P1'].
assert (∃ n1, howe' Rel P1' P1' n1).
apply howe_implies_howe'; auto with howe hopi.
destruct H2. forwards*: H0 H2 H1 H6. destruct_hyps.
do 5 eexists; intuition (try eassumption).
+ inverts H5.
- forwards: lts_inp_abs H9. destruct H2 as [F'1]. subst. simpl in H10.
forwards*: IH H1 H2_; try solve [simpl; eauto with hopi].
apply lexico2_2; omega.
destruct H2 as [F'2 [ C'2 [P'2 [Q'2 [n3 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
inverts Hp'2. inverts Hq'2.
assert (∃ n4, howe' Rel (P'2 // bind f P') (Q'2 // bind f Q') n4).
apply× @howe_implies_howe'. apply howe'_implies_howe in H2_0.
apply howe'_implies_howe in Hhowe. auto with hopi howe.
destruct H13.
∃ (abs_parl F'2 (bind f Q')) C'2 (P'2// bind f P') (Q'2//bind f Q') x.
splits; eauto with hopi howe.
eapply lts_parl'; eauto.
apply sc0_trans with (appr F'1 C1 // bind f P'); auto with sc hopi howe.
inverts H10. assert (struct_congr
(appr F'1 C1 // bind f P') (appr (abs_parl F'1 (bind f P')) C1)).
destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
apply sc_trans with
(genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f P'))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H10.
apply sc0_trans with (appr F'2 C'2 // bind f Q'); auto with sc hopi howe.
assert (struct_congr
(appr F'2 C'2 // bind f Q') (appr (abs_parl F'2 (bind f Q')) C'2)).
destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
apply sc_trans with
(genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f Q'))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H14.
- forwards: lts_inp_abs H9. destruct H2 as [F'1]. subst. simpl in H10.
forwards*: IH H1 H2_0; try solve [simpl; eauto with hopi].
apply lexico2_2; omega.
destruct H2 as [F'2 [ C'2 [P'2 [Q'2 [n3 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
inverts Hp'2. inverts Hq'2.
assert (∃ n4, howe' Rel (bind f P // P'2) (bind f Q // Q'2) n4).
apply× @howe_implies_howe'. apply howe'_implies_howe in H2_.
apply howe'_implies_howe in Hhowe. auto with hopi howe.
destruct H13.
∃ (abs_parr (bind f Q) F'2) C'2 (bind f P // P'2) (bind f Q // Q'2) x.
splits; eauto with hopi howe.
eapply lts_parr'; eauto.
apply sc0_trans with (bind f P // appr F'1 C1); auto with sc hopi howe.
inverts H10. assert (struct_congr
(bind f P // appr F'1 C1) (appr (abs_parr (bind f P) F'1) C1)).
destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
apply sc_trans with
(genNu n (shiftN n (bind f P) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H10.
apply sc0_trans with (bind f Q // appr F'2 C'2); auto with sc hopi howe.
assert (struct_congr (bind f Q // appr F'2 C'2)
(appr (abs_parr (bind f Q) F'2) C'2)).
destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
apply sc_trans with
(genNu n (shiftN n (bind f Q) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H14.
+ inverts H5. assert (∃ n1, howe' Rel (bind (liftV f) P)(bind (liftV f) Q) n1).
apply× @howe_implies_howe'. apply× @howe_bind. apply× @howe'_implies_howe. eassumption.
intros [|]; simpl; auto with howe.
destruct H5. forwards*: H0 H5 H1 H6. destruct_hyps.
do 5 eexists; intuition (try eassumption).
simpl. auto with hopi.
+ simpl in ×. inversion H5; subst.
pick_fresh_fset_V V
(fn (bind (fun x ⇒ mapN (fun x0 ⇒ S x0) (f x)) Q) \u fn (bind g Q2)) x.
forwards*: H10 x. forwards: lts_inp_abs H7. destruct H9 as [Fx].
rewrite H9 in H7.
assert (∀ y, is_proc (mapN (fun x1 ⇒ S x1) (f y))) by auto with hopi.
rewrite <- bind_open in H7; auto with hopi.
forwards*: H2 x.
forwards: IH H1 H12 H7; try solve [simpl; eauto with hopi].
apply lexico2_2; omega.
destruct H13 as [F'x [ C'1 [ P'x [Q'x [n3 [HltsF'x [HltsC'1 [Hp'x [Hq'x HhoweF'x]]]]]]]]].
destruct F'x as [Pfx].
assert (lts (nu bind (fun x0 ⇒ mapN (fun x1 ⇒ S x1) (f x0)) Q) (inp a)
(abs_new (abs_def (close 0 x Pfx)))).
apply (lts_new' L) with (abs_def (close 0 x Pfx)); auto.
intros. rewrite bind_open in HltsF'x; auto.
forwards: lts_open HltsF'x; eauto.
rewrite <- bind_open; auto. apply× @is_proc_bind. intuition.
destruct H15 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
inverts Ha'. destruct A' as [ |[Q''] |[] ]; inverts H16. simpl in HxA'.
rewrite× @close_open. rewrite× subst_lab_id in HltsA'. simpl; autofs.
assert (∃ n, howe' Rel (nu close 0 x P'x) (nu close 0 x Q'x) n).
apply× @howe_implies_howe'.
apply (howe_nu (L \u fn (close 0 x P'x) \u fn (close 0 x Q'x))).
intros. eapply (howe_rename _ Hrename) with x; eauto;
try solve [rewrite open_close; auto with howe].
autofnF.
rewrite open_close; auto with howe. rewrite open_close; auto with howe.
apply howe'_implies_howe in HhoweF'x; auto.
destruct H14.
∃ (abs_new (abs_def (close 0 x Pfx))) C'1
(nu close 0 x P'x) (nu close 0 x Q'x) x0. splits; auto.
assert (is_agent C1) by auto with howe hopi.
assert (is_agent F1).
forwards*: @lts_is_proc H5.
apply (proc_nu L). intros. rewrite× <- @bind_open.
apply× @is_proc_bind. forwards*: H2 x1. auto with howe.
inverts Hp'x. apply sc0_def; auto with hopi.
apply (proc_nu L); auto with hopi.
destructA A; inverts H9.
apply sc_trans with (nu appr (abs_def p) C1); auto with sc.
apply sc_nu'. destruct C1 as [n P22 P23]. simpl in ×.
asserts_rewrite (genNu n (subst ((shiftN n) p) P22 // P23)
= close 0 x (genNu n (subst ((shiftN n)(open 0 x p)) P22 // P23))).
rewrite close_genNu. simpl. fequals.
rewrite close_subst. rewrite mapN_open; auto using shiftN_injective.
replace (n+0) with n by omega. rewrite close_open; try solve [autofnF].
repeat (rewrite× @close_id).
apply× @sc_close. apply sc_symmetric.
inverts H8. apply× (sc_newF_C (abs_def p)).
assert (is_agent C'1) by auto with howe hopi.
inverts Hq'x.
apply sc0_def; auto with hopi.
apply (proc_nu L); auto with hopi.
apply× is_proc_app. forwards*: @lts_is_proc H13.
apply (proc_nu L). intros. rewrite× <- @bind_open.
apply× @is_proc_bind. forwards*: H2 x1. auto with howe.
apply sc_trans with (nu appr (abs_def (close 0 x Pfx)) C'1); auto with sc.
apply sc_nu'. destruct C'1 as [n P22 P23]. simpl in ×.
asserts_rewrite (genNu n (subst ((shiftN n)(close 0 x Pfx)) P22 // P23)
= close 0 x (genNu n (subst ((shiftN n) Pfx) P22 // P23))).
rewrite close_genNu. simpl. fequals.
rewrite close_subst. forwards*: lts_fn HltsC'1. simpl in H19.
rewrite <- mapN_close. replace (n+0) with n by omega.
repeat fequals; rewrite× @close_id.
assert (fn P22 \c fn (bind g Q2)).
apply subset_trans with (fn P22 \u fn P23); auto. autofs.
autofnF.
assert (fn P23 \c fn (bind g Q2)).
apply subset_trans with (fn P22 \u fn P23); auto. autofs.
autofnF.
apply× @sc_close.
apply sc_symmetric. apply× (sc_newF_C (abs_def (close 0 x Pfx))).
Qed.
Lemma pseudo_sim_sim : pseudo_sim.
Proof.
intros. apply howe_implies_howe' in H3; auto.
apply howe_implies_howe' in H4; auto. destruct H3, H4.
forwards*: @pseudo_sim_sim' H2 H3; try eassumption. destruct_hyps.
apply howe'_implies_howe in H13. do 4 eexists; intuition eassumption.
Qed.
Notation lpseudo_sim := pseudo_sim_in .
Lemma pseudo_tau {V:Set}: ∀ Rel (P Q:proc V) P'
(f:V → proc0), simulation Rel → refl0 Rel → rename_compatible Rel →
(Rincl sc0 Rel) → trans Rel → howe Rel P Q → (∀ v, is_proc (f v)) →
lts (bind f P) tau (ag_proc P') →
∃ Q' P'' Q'', lts (bind f Q) tau (ag_proc Q') ∧
sc0 P' P'' ∧ sc0 Q' Q'' ∧ howe Rel P'' Q''.
Proof.
introv Hsim Hrefl Hrename Hincl Htrans Hp1q1. gen f P'.
induction Hp1q1; introv Hf HltsP1; try solve [inverts HltsP1].
- forwards*: IHHp1q1 P'.
destruct H1 as [R' [P'' [R'' [HltsR [Hp'p'' [Hr'r'' HhoweP1R]]]]]].
forwards: H0 f; auto. destruct Hsim as [Hisproc Hsim]. forwards_test Rel.
∃ Q'0 P'' Q'0; intuition.
apply howe_comp with R''; auto with hopi howe.
apply oe_trans with R'; auto. apply oe_sc0; auto with sc. apply× oe_proc0.
- ∃ P' P' P'; intuition.
- inversion HltsP1; subst.
+ forwards: lts_tau_proc H2. destruct H as [P'1]. subst. simpl in H3.
forwards: IHHp1q1_1 H2; auto.
destruct H as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
inverts Hp'1p''1. inverts Hq'1q''1.
∃ (Q'1 // (bind f Q')) (P''1 // (bind f P')) (Q''1 // (bind f Q')).
inverts H3. splits; auto with sc howe hopi.
eapply lts_parl'; eauto.
+ forwards: lts_tau_proc H2. destruct H as [P'1]. subst. simpl in H3.
forwards: IHHp1q1_2 H2; auto.
destruct H as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
inverts Hp'1p''1. inverts Hq'1q''1.
∃ ((bind f Q) // Q'1) ((bind f P) // P''1) ((bind f Q) // Q''1).
inverts H3. splits; auto with sc howe hopi.
eapply lts_parr'; eauto.
+ forwards: lpseudo_sim H3 H2; eauto.
destruct H as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
∃ (appl C2 F2) P'2 Q'2. inverts Hp'2. inverts Hq'2. splits; eauto.
eapply lts_taul'; eauto.
apply sc0_def; auto with howe hopi sc. apply sc_trans with (appr F C); auto with sc.
apply sc_appr_appl.
apply sc0_def; auto with howe hopi sc. apply sc_trans with (appr F2 C2); auto with sc.
apply sc_appr_appl.
+ forwards: lpseudo_sim H2 H3; eauto.
destruct H as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
∃ (appr F2 C2) P'2 Q'2. inverts Hp'2. inverts Hq'2. splits; eauto with sc.
eapply lts_taur'; eauto.
- inverts HltsP1. destruct A as [ P'1 | [] | [] ]; inverts H2.
pick_fresh_fset_V V (fn P'1 \u
fn (bind (fun x1 ⇒ mapN (fun x2 ⇒ S x2) (f x1)) Q)) x.
forwards*: H4 x.
assert (∀ y, is_proc (mapN (fun x0 ⇒ S x0) (f y))) by auto with hopi.
rewrite× <- @bind_open in H1. forwards: H0 x H1; eauto.
destruct H3 as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
inverts Hp'1p''1. inverts Hq'1q''1.
∃ (nu (close 0 x Q'1)) (nu (close 0 x P''1)) (nu (close 0 x Q''1)).
splits.
apply (lts_new' L) with (ag_proc (close 0 x Q'1)); try solve [simpl; auto].
fold @bind. intros. simpl. rewrite bind_open in HltsQ'; auto.
forwards:lts_open HltsQ'; eauto.
rewrite× <- @bind_open. apply× @is_proc_bind.
forwards: H x; intuition.
destruct H12 as [A' [Ha' [HxA' HltsAy]]]. specialize (HltsAy x0).
destruct A' as [Q'' |[]|[]]; inverts Ha'. simpl in HltsAy.
rewrite× @close_open.
apply sc0_def; auto with howe hopi sc.
apply (proc_nu L). intros. apply is_proc_rename with x; auto.
apply (proc_nu L). intros. apply is_proc_rename with x; auto.
rewrite× @open_close.
apply sc_nu'.
replace P'1 with (close 0 x (open 0 x P'1)) by (rewrite× @close_open).
apply× @sc_close.
apply sc0_def; auto with howe hopi sc.
apply (proc_nu L). intros. apply is_proc_rename with x; auto.
rewrite× @open_close.
apply (proc_nu L). intros. apply is_proc_rename with x; auto.
rewrite× @open_close.
apply× @sc_nu'. apply× @sc_close.
apply (howe_nu (L \u fn (close 0 x P''1) \u fn (close 0 x Q''1))). intros.
assert (0 \notin bn P''1).
apply is_proc_bn in H5. rewrite× H5.
assert (0 \notin bn Q''1).
apply is_proc_bn in H8. rewrite× H8.
rewrite× <- (open_close_gen P''1 0 x) in Hhowe.
rewrite× <- (open_close_gen Q''1 0 x) in Hhowe.
forwards: @howe_rename Hhowe x0; eauto.
autofnF.
rewrite× @open_close_gen.
rewrite× @open_close_gen.
Qed.
Lemma conc_to_proc : ∀ (C:conc) a, conc_wf C → is_agent C →
∃ P, is_proc P ∧ lts P (out a) C ∧
(∀ (C':conc), lts P (out a) C' → C = C').
Proof.
intros. destruct C as [n P1 P2]. gen P1 P2. induction n; intros.
+ ∃ (a!(P1) P2); intuition; auto with hopi. simpl in H0.
assert (bn P1 = \{}). autofs. forwards*: H0 x; autofs. omega.
assert (bn P2 = \{}). autofs. forwards*: H0 x; autofs. omega.
apply proc_out; apply× @is_proc_bn_rev.
inverts× H1.
+ pick_fresh x. forwards*: IHn (open n x P1) (open n x P2).
intros. rewrite bn_open. forwards*: H k. autofs. omega.
intros. forwards*: H0 k. autobnF. autobnF; omega.
destruct H1 as [P []]. forwards*: @decomp_proc P 0 x.
destruct H3 as [P' [H13 [H12 H22]]]. subst.
∃ (nu P'). splits.
- apply (proc_nu (fn P')). intros. unfold open. eapply is_proc_rename; eauto.
- apply (lts_new' (fn P' \u fn P1 \u fn P2 \u \{ a})) with
(conc_def n P1 P2). intros.
simpl. forwards*: lts_open H2.
destruct H5 as [A' [Ha' [HxA' HltsA']]].
destruct A' as [ |[]|[]]; inverts Ha'.
simpl in HxA'. forwards*: @open_injective H7. forwards*: @open_injective H8.
subst. specialize (HltsA' x0). rewrite subst_lab_id in HltsA'; try simpl; auto.
simpl. assert (n \in bn P1). forwards*: H n. case_if×.
- intros. inverts H3. pick_fresh y. forwards*: H7 y.
forwards*: lts_out_conc H3. destruct H4 as [[]].
forwards× HltsA': lts_rename H3 x.
destruct A as [ |[]|[]]; inverts H4.
destruct H2. rewrite subst_lab_id in HltsA'; try solve [simpl; autofs].
simpl in HltsA'. forwards*: H4 HltsA'. inverts H6.
assert (x \notin (fn p1 \u fn p2)).
forwards*: lts_fn H3. simpl in H6. forwards: @fn_open_sub P' 0 y.
forwards*: @subset_trans H6 H8. clear H6 H8.
forwards: @fn_open_rev p1 n0 y. forwards: @fn_open_rev p2 n0 y.
assert (fn p1 \u fn p2 \c fn P' \u \{ y}).
apply subset_trans with (fn (open n0 y p1) \u fn(open n0 y p2)); autofs.
clear H8 H6 H9. intros_all. apply H13 in H6. autofs.
forwards*: @open_injective H10. forwards*: @open_injective H11. subst.
inverts H5. assert (n0 \in bn p1). apply H. omega. case_if×.
Qed.
Lemma abs_to_proc : ∀ (F:abs) a, is_agent F →
∃ P, is_proc P ∧ lts P (inp a) F ∧
(∀ (F':abs), lts P (inp a) F' → F = F').
Proof.
intros. destruct F as [P]. ∃ (a? P); splits*; auto with hopi.
intros. inverts× H0.
Qed.
Lemma simulation_up_to_sc_howe : ∀ Rel, simulation Rel → refl0 Rel → rename_compatible Rel →
(Rincl sc0 Rel) → trans Rel → simulation_up_to_sc (howe Rel).
Proof.
intros. split.
intros_all. auto with howe.
intros. splits; intros.
+ replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
forwards: @pseudo_tau H3; eauto with hopi.
destruct H5 as [Q' [P'' [Q'' [HltsQ' [Hpp'' [Hq'q'' Hhowe]]]]]].
replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ' by (rewrite× bind_proc0).
∃ Q'. split×. do 2 (eexists; intuition eauto with sc).
+ replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
forwards*: conc_to_proc C a. destruct H7 as [R [Hr [Hlts Hc']]].
assert (howe Rel R R) by apply× @howe_refl.
replace R with (bind (pr_var (V:=Empty_set)) R) in Hlts by (rewrite× bind_proc0).
forwards: lpseudo_sim H7 H3; eauto with hopi.
destruct H8 as [F2 [C2 [P'2 [Q'2 [HltsQ [HltsR [Hpp'' [Hq'q'' Hhowe]]]]]]]].
replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ by (rewrite× bind_proc0).
replace (bind (pr_var (V:=Empty_set)) R) with R in HltsR by (rewrite× bind_proc0).
forwards*: Hc' HltsR. subst. do 3 (eexists; intuition eauto with sc).
+ replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
forwards*: abs_to_proc F a. destruct H6 as [R [Hr [Hlts Hf']]].
assert (howe Rel R R) by apply× @howe_refl.
replace R with (bind (pr_var (V:=Empty_set)) R) in Hlts by (rewrite× bind_proc0).
forwards: lpseudo_sim H3 H6; eauto with hopi.
destruct H7 as [F2 [C2 [P'2 [Q'2 [HltsR [HltsQ [Hpp'' [Hq'q'' Hhowe]]]]]]]].
replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ by (rewrite× bind_proc0).
replace (bind (pr_var (V:=Empty_set)) R) with R in HltsR by (rewrite× bind_proc0).
forwards*: Hf' HltsR. subst. do 3 (eexists; intuition eauto with sc).
Qed.
Lemma Rincl_sc0_howe : ∀ Rel, (Rincl sc0 Rel) → Rincl sc0 (howe Rel).
Proof.
intros_all. apply howe_comp with x; auto with sc howe.
apply× oe_proc0.
Qed.
Lemma bisimulation_tclos_howe : ∀ Rel, simulation Rel → refl0 Rel
→ rename_compatible Rel → (Rincl sc0 Rel) → trans Rel → sym Rel
→ bisimulation (tclosure (howe Rel)).
Proof.
intros. rename H3 into Hsym. apply sim_sym_imply_bisim.
×
split.
intros_all. induction H3; intuition auto with howe.
intros. assert (Rincl sc0 (tclosure (howe Rel))).
intros_all. apply× tclosure_once. apply× Rincl_sc0_howe.
induction H3.
+ forwards*: simulation_up_to_sc_howe Rel.
destruct H5. specialize (H6 x y H3).
splits; intros; forwards_test (sc0° (howe Rel) ° sc0); destruct_comp;
repeat (eexists; intuition (try eassumption)); intuition;
repeat (match goal with
| H1: Rincl sc0 (tclosure (howe Rel)),
H2: sc0 _ _ |- _ ⇒ apply H1 in H2 end); eauto with howe.
+ splits; intros; forwards_test (tclosure (@howe Empty_set Rel)); clear H3_;
forwards_test (tclosure (@howe Empty_set Rel)); destruct_comp;
repeat (eexists; intuition (try eassumption)); intuition eauto with howe.
× apply× @howe_sym.
Qed.
Theorem bisimilarity_howe : bisimilarity = howe bisimilarity.
Proof.
apply binary_ext; split.
- intros. assert (Hbisim:=H). unfold bisimilarity in H. destruct H. destruct H.
apply howe_comp with x; auto with bisim. apply howe_refl; auto with bisim.
apply× oe_proc0.
- intros. ∃ (tclosure (@howe Empty_set bisimilarity)).
split. apply bisimulation_tclos_howe; auto using bisim_sym, bisim_trans, bisim_refl,
bisim_rename_compatible.
forwards*: bisim_is_bisimulation; intuition.
intros_all. ∃ sc0. intuition. apply struct_congr_bisim.
apply× tclosure_once.
Qed.
Lemma pseudo_tau {V:Set}: ∀ Rel (P Q:proc V) P'
(f:V → proc0), simulation Rel → refl0 Rel → rename_compatible Rel →
(Rincl sc0 Rel) → trans Rel → howe Rel P Q → (∀ v, is_proc (f v)) →
lts (bind f P) tau (ag_proc P') →
∃ Q' P'' Q'', lts (bind f Q) tau (ag_proc Q') ∧
sc0 P' P'' ∧ sc0 Q' Q'' ∧ howe Rel P'' Q''.
Proof.
introv Hsim Hrefl Hrename Hincl Htrans Hp1q1. gen f P'.
induction Hp1q1; introv Hf HltsP1; try solve [inverts HltsP1].
- forwards*: IHHp1q1 P'.
destruct H1 as [R' [P'' [R'' [HltsR [Hp'p'' [Hr'r'' HhoweP1R]]]]]].
forwards: H0 f; auto. destruct Hsim as [Hisproc Hsim]. forwards_test Rel.
∃ Q'0 P'' Q'0; intuition.
apply howe_comp with R''; auto with hopi howe.
apply oe_trans with R'; auto. apply oe_sc0; auto with sc. apply× oe_proc0.
- ∃ P' P' P'; intuition.
- inversion HltsP1; subst.
+ forwards: lts_tau_proc H2. destruct H as [P'1]. subst. simpl in H3.
forwards: IHHp1q1_1 H2; auto.
destruct H as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
inverts Hp'1p''1. inverts Hq'1q''1.
∃ (Q'1 // (bind f Q')) (P''1 // (bind f P')) (Q''1 // (bind f Q')).
inverts H3. splits; auto with sc howe hopi.
eapply lts_parl'; eauto.
+ forwards: lts_tau_proc H2. destruct H as [P'1]. subst. simpl in H3.
forwards: IHHp1q1_2 H2; auto.
destruct H as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
inverts Hp'1p''1. inverts Hq'1q''1.
∃ ((bind f Q) // Q'1) ((bind f P) // P''1) ((bind f Q) // Q''1).
inverts H3. splits; auto with sc howe hopi.
eapply lts_parr'; eauto.
+ forwards: lpseudo_sim H3 H2; eauto.
destruct H as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
∃ (appl C2 F2) P'2 Q'2. inverts Hp'2. inverts Hq'2. splits; eauto.
eapply lts_taul'; eauto.
apply sc0_def; auto with howe hopi sc. apply sc_trans with (appr F C); auto with sc.
apply sc_appr_appl.
apply sc0_def; auto with howe hopi sc. apply sc_trans with (appr F2 C2); auto with sc.
apply sc_appr_appl.
+ forwards: lpseudo_sim H2 H3; eauto.
destruct H as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
∃ (appr F2 C2) P'2 Q'2. inverts Hp'2. inverts Hq'2. splits; eauto with sc.
eapply lts_taur'; eauto.
- inverts HltsP1. destruct A as [ P'1 | [] | [] ]; inverts H2.
pick_fresh_fset_V V (fn P'1 \u
fn (bind (fun x1 ⇒ mapN (fun x2 ⇒ S x2) (f x1)) Q)) x.
forwards*: H4 x.
assert (∀ y, is_proc (mapN (fun x0 ⇒ S x0) (f y))) by auto with hopi.
rewrite× <- @bind_open in H1. forwards: H0 x H1; eauto.
destruct H3 as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
inverts Hp'1p''1. inverts Hq'1q''1.
∃ (nu (close 0 x Q'1)) (nu (close 0 x P''1)) (nu (close 0 x Q''1)).
splits.
apply (lts_new' L) with (ag_proc (close 0 x Q'1)); try solve [simpl; auto].
fold @bind. intros. simpl. rewrite bind_open in HltsQ'; auto.
forwards:lts_open HltsQ'; eauto.
rewrite× <- @bind_open. apply× @is_proc_bind.
forwards: H x; intuition.
destruct H12 as [A' [Ha' [HxA' HltsAy]]]. specialize (HltsAy x0).
destruct A' as [Q'' |[]|[]]; inverts Ha'. simpl in HltsAy.
rewrite× @close_open.
apply sc0_def; auto with howe hopi sc.
apply (proc_nu L). intros. apply is_proc_rename with x; auto.
apply (proc_nu L). intros. apply is_proc_rename with x; auto.
rewrite× @open_close.
apply sc_nu'.
replace P'1 with (close 0 x (open 0 x P'1)) by (rewrite× @close_open).
apply× @sc_close.
apply sc0_def; auto with howe hopi sc.
apply (proc_nu L). intros. apply is_proc_rename with x; auto.
rewrite× @open_close.
apply (proc_nu L). intros. apply is_proc_rename with x; auto.
rewrite× @open_close.
apply× @sc_nu'. apply× @sc_close.
apply (howe_nu (L \u fn (close 0 x P''1) \u fn (close 0 x Q''1))). intros.
assert (0 \notin bn P''1).
apply is_proc_bn in H5. rewrite× H5.
assert (0 \notin bn Q''1).
apply is_proc_bn in H8. rewrite× H8.
rewrite× <- (open_close_gen P''1 0 x) in Hhowe.
rewrite× <- (open_close_gen Q''1 0 x) in Hhowe.
forwards: @howe_rename Hhowe x0; eauto.
autofnF.
rewrite× @open_close_gen.
rewrite× @open_close_gen.
Qed.
Lemma conc_to_proc : ∀ (C:conc) a, conc_wf C → is_agent C →
∃ P, is_proc P ∧ lts P (out a) C ∧
(∀ (C':conc), lts P (out a) C' → C = C').
Proof.
intros. destruct C as [n P1 P2]. gen P1 P2. induction n; intros.
+ ∃ (a!(P1) P2); intuition; auto with hopi. simpl in H0.
assert (bn P1 = \{}). autofs. forwards*: H0 x; autofs. omega.
assert (bn P2 = \{}). autofs. forwards*: H0 x; autofs. omega.
apply proc_out; apply× @is_proc_bn_rev.
inverts× H1.
+ pick_fresh x. forwards*: IHn (open n x P1) (open n x P2).
intros. rewrite bn_open. forwards*: H k. autofs. omega.
intros. forwards*: H0 k. autobnF. autobnF; omega.
destruct H1 as [P []]. forwards*: @decomp_proc P 0 x.
destruct H3 as [P' [H13 [H12 H22]]]. subst.
∃ (nu P'). splits.
- apply (proc_nu (fn P')). intros. unfold open. eapply is_proc_rename; eauto.
- apply (lts_new' (fn P' \u fn P1 \u fn P2 \u \{ a})) with
(conc_def n P1 P2). intros.
simpl. forwards*: lts_open H2.
destruct H5 as [A' [Ha' [HxA' HltsA']]].
destruct A' as [ |[]|[]]; inverts Ha'.
simpl in HxA'. forwards*: @open_injective H7. forwards*: @open_injective H8.
subst. specialize (HltsA' x0). rewrite subst_lab_id in HltsA'; try simpl; auto.
simpl. assert (n \in bn P1). forwards*: H n. case_if×.
- intros. inverts H3. pick_fresh y. forwards*: H7 y.
forwards*: lts_out_conc H3. destruct H4 as [[]].
forwards× HltsA': lts_rename H3 x.
destruct A as [ |[]|[]]; inverts H4.
destruct H2. rewrite subst_lab_id in HltsA'; try solve [simpl; autofs].
simpl in HltsA'. forwards*: H4 HltsA'. inverts H6.
assert (x \notin (fn p1 \u fn p2)).
forwards*: lts_fn H3. simpl in H6. forwards: @fn_open_sub P' 0 y.
forwards*: @subset_trans H6 H8. clear H6 H8.
forwards: @fn_open_rev p1 n0 y. forwards: @fn_open_rev p2 n0 y.
assert (fn p1 \u fn p2 \c fn P' \u \{ y}).
apply subset_trans with (fn (open n0 y p1) \u fn(open n0 y p2)); autofs.
clear H8 H6 H9. intros_all. apply H13 in H6. autofs.
forwards*: @open_injective H10. forwards*: @open_injective H11. subst.
inverts H5. assert (n0 \in bn p1). apply H. omega. case_if×.
Qed.
Lemma abs_to_proc : ∀ (F:abs) a, is_agent F →
∃ P, is_proc P ∧ lts P (inp a) F ∧
(∀ (F':abs), lts P (inp a) F' → F = F').
Proof.
intros. destruct F as [P]. ∃ (a? P); splits*; auto with hopi.
intros. inverts× H0.
Qed.
Lemma simulation_up_to_sc_howe : ∀ Rel, simulation Rel → refl0 Rel → rename_compatible Rel →
(Rincl sc0 Rel) → trans Rel → simulation_up_to_sc (howe Rel).
Proof.
intros. split.
intros_all. auto with howe.
intros. splits; intros.
+ replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
forwards: @pseudo_tau H3; eauto with hopi.
destruct H5 as [Q' [P'' [Q'' [HltsQ' [Hpp'' [Hq'q'' Hhowe]]]]]].
replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ' by (rewrite× bind_proc0).
∃ Q'. split×. do 2 (eexists; intuition eauto with sc).
+ replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
forwards*: conc_to_proc C a. destruct H7 as [R [Hr [Hlts Hc']]].
assert (howe Rel R R) by apply× @howe_refl.
replace R with (bind (pr_var (V:=Empty_set)) R) in Hlts by (rewrite× bind_proc0).
forwards: lpseudo_sim H7 H3; eauto with hopi.
destruct H8 as [F2 [C2 [P'2 [Q'2 [HltsQ [HltsR [Hpp'' [Hq'q'' Hhowe]]]]]]]].
replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ by (rewrite× bind_proc0).
replace (bind (pr_var (V:=Empty_set)) R) with R in HltsR by (rewrite× bind_proc0).
forwards*: Hc' HltsR. subst. do 3 (eexists; intuition eauto with sc).
+ replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
forwards*: abs_to_proc F a. destruct H6 as [R [Hr [Hlts Hf']]].
assert (howe Rel R R) by apply× @howe_refl.
replace R with (bind (pr_var (V:=Empty_set)) R) in Hlts by (rewrite× bind_proc0).
forwards: lpseudo_sim H3 H6; eauto with hopi.
destruct H7 as [F2 [C2 [P'2 [Q'2 [HltsR [HltsQ [Hpp'' [Hq'q'' Hhowe]]]]]]]].
replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ by (rewrite× bind_proc0).
replace (bind (pr_var (V:=Empty_set)) R) with R in HltsR by (rewrite× bind_proc0).
forwards*: Hf' HltsR. subst. do 3 (eexists; intuition eauto with sc).
Qed.
Lemma Rincl_sc0_howe : ∀ Rel, (Rincl sc0 Rel) → Rincl sc0 (howe Rel).
Proof.
intros_all. apply howe_comp with x; auto with sc howe.
apply× oe_proc0.
Qed.
Lemma bisimulation_tclos_howe : ∀ Rel, simulation Rel → refl0 Rel
→ rename_compatible Rel → (Rincl sc0 Rel) → trans Rel → sym Rel
→ bisimulation (tclosure (howe Rel)).
Proof.
intros. rename H3 into Hsym. apply sim_sym_imply_bisim.
×
split.
intros_all. induction H3; intuition auto with howe.
intros. assert (Rincl sc0 (tclosure (howe Rel))).
intros_all. apply× tclosure_once. apply× Rincl_sc0_howe.
induction H3.
+ forwards*: simulation_up_to_sc_howe Rel.
destruct H5. specialize (H6 x y H3).
splits; intros; forwards_test (sc0° (howe Rel) ° sc0); destruct_comp;
repeat (eexists; intuition (try eassumption)); intuition;
repeat (match goal with
| H1: Rincl sc0 (tclosure (howe Rel)),
H2: sc0 _ _ |- _ ⇒ apply H1 in H2 end); eauto with howe.
+ splits; intros; forwards_test (tclosure (@howe Empty_set Rel)); clear H3_;
forwards_test (tclosure (@howe Empty_set Rel)); destruct_comp;
repeat (eexists; intuition (try eassumption)); intuition eauto with howe.
× apply× @howe_sym.
Qed.
Theorem bisimilarity_howe : bisimilarity = howe bisimilarity.
Proof.
apply binary_ext; split.
- intros. assert (Hbisim:=H). unfold bisimilarity in H. destruct H. destruct H.
apply howe_comp with x; auto with bisim. apply howe_refl; auto with bisim.
apply× oe_proc0.
- intros. ∃ (tclosure (@howe Empty_set bisimilarity)).
split. apply bisimulation_tclos_howe; auto using bisim_sym, bisim_trans, bisim_refl,
bisim_rename_compatible.
forwards*: bisim_is_bisimulation; intuition.
intros_all. ∃ sc0. intuition. apply struct_congr_bisim.
apply× tclosure_once.
Qed.