Library Nom_HoweSound
Require Export Nom_Howe.
Notation pseudo_sim :=
(∀ {V W:Set} Rel (P1 Q1:proc V)(P2 Q2:proc W)
a F1 C1 (f:V → proc0)(g: W → proc0) N,
simulation Rel → refl Rel → mod_aeq Rel → mod_swap Rel → (Rincl sc0 Rel) → trans Rel
→ howe Rel P2 Q2 → howe Rel P1 Q1
→ fn P1 [<=] N → fn P2 [<=] N → fn Q1 [<=] N → fn Q2 [<=] N
→ (∀ x, fn (f x) [<=] N) → (∀ x, fn (g x) [<=] N)
→ lts (bind f N P1) (inp a) (ag_abs F1) → lts (bind g N P2) (out a) (ag_conc C1)
→ ∃ F2 C2 P'2 Q'2, lts (bind f N Q1) (inp a) (ag_abs F2) ∧
lts (bind g N Q2) (out a) (ag_conc C2) ∧
P'2 =sc0= (appr F1 C1) ∧
Q'2 =sc0= (appr F2 C2) ∧
howe Rel P'2 Q'2).
Notation pseudo_sim' :=
(∀ {V W:Set} Rel (P1 Q1:proc V)(P2 Q2:proc W)
a F1 C1 (f:V → proc0)(g: W → proc0) N k1 k2,
simulation Rel → refl Rel → mod_aeq Rel → mod_swap Rel → (Rincl sc0 Rel) → trans Rel
→ howe' Rel P2 Q2 k2 → howe' Rel P1 Q1 k1
→ fn P1 [<=] N → fn P2 [<=] N → fn Q1 [<=] N → fn Q2 [<=] N
→ (∀ x, fn (f x) [<=] N) → (∀ x, fn (g x) [<=] N)
→ lts (bind f N P1) (inp a) (ag_abs F1) → lts (bind g N P2) (out a) (ag_conc C1)
→ ∃ F2 C2 P'2 Q'2, lts (bind f N Q1) (inp a) (ag_abs F2) ∧
lts (bind g N Q2) (out a) (ag_conc C2) ∧
P'2 =sc0= (appr F1 C1) ∧
Q'2 =sc0= (appr F2 C2) ∧
∃ k, howe' Rel P'2 Q'2 k).
Lemma pseudo_sim_equiv : pseudo_sim ↔ pseudo_sim'.
Proof. split; intros_all.
- apply howe'_implies_howe in H7. apply howe'_implies_howe in H6.
forwards: H f g; eauto. destruct_hyps.
∃ x x0 x1 x2. intuition. apply howe_implies_howe'; auto.
- apply howe_implies_howe' in H7. apply howe_implies_howe' in H6.
destruct_hyps. forwards: H f g; eauto. destruct_hyps.
∃ x1 x2 x3 x4. intuition. apply howe'_implies_howe with x5; auto.
Qed.
Notation pseudo_sim :=
(∀ {V W:Set} Rel (P1 Q1:proc V)(P2 Q2:proc W)
a F1 C1 (f:V → proc0)(g: W → proc0) N,
simulation Rel → refl Rel → mod_aeq Rel → mod_swap Rel → (Rincl sc0 Rel) → trans Rel
→ howe Rel P2 Q2 → howe Rel P1 Q1
→ fn P1 [<=] N → fn P2 [<=] N → fn Q1 [<=] N → fn Q2 [<=] N
→ (∀ x, fn (f x) [<=] N) → (∀ x, fn (g x) [<=] N)
→ lts (bind f N P1) (inp a) (ag_abs F1) → lts (bind g N P2) (out a) (ag_conc C1)
→ ∃ F2 C2 P'2 Q'2, lts (bind f N Q1) (inp a) (ag_abs F2) ∧
lts (bind g N Q2) (out a) (ag_conc C2) ∧
P'2 =sc0= (appr F1 C1) ∧
Q'2 =sc0= (appr F2 C2) ∧
howe Rel P'2 Q'2).
Notation pseudo_sim' :=
(∀ {V W:Set} Rel (P1 Q1:proc V)(P2 Q2:proc W)
a F1 C1 (f:V → proc0)(g: W → proc0) N k1 k2,
simulation Rel → refl Rel → mod_aeq Rel → mod_swap Rel → (Rincl sc0 Rel) → trans Rel
→ howe' Rel P2 Q2 k2 → howe' Rel P1 Q1 k1
→ fn P1 [<=] N → fn P2 [<=] N → fn Q1 [<=] N → fn Q2 [<=] N
→ (∀ x, fn (f x) [<=] N) → (∀ x, fn (g x) [<=] N)
→ lts (bind f N P1) (inp a) (ag_abs F1) → lts (bind g N P2) (out a) (ag_conc C1)
→ ∃ F2 C2 P'2 Q'2, lts (bind f N Q1) (inp a) (ag_abs F2) ∧
lts (bind g N Q2) (out a) (ag_conc C2) ∧
P'2 =sc0= (appr F1 C1) ∧
Q'2 =sc0= (appr F2 C2) ∧
∃ k, howe' Rel P'2 Q'2 k).
Lemma pseudo_sim_equiv : pseudo_sim ↔ pseudo_sim'.
Proof. split; intros_all.
- apply howe'_implies_howe in H7. apply howe'_implies_howe in H6.
forwards: H f g; eauto. destruct_hyps.
∃ x x0 x1 x2. intuition. apply howe_implies_howe'; auto.
- apply howe_implies_howe' in H7. apply howe_implies_howe' in H6.
destruct_hyps. forwards: H f g; eauto. destruct_hyps.
∃ x1 x2 x3 x4. intuition. apply howe'_implies_howe with x5; auto.
Qed.
Lemma pseudo_inp_first {V:Set}:
∀ Rel (P1 Q1:proc V)(P2 Q2:proc0) a F1 (f:V → proc0) N k1 k2,
simulation Rel → refl Rel → mod_aeq Rel → mod_swap Rel → trans Rel
→ (∀ P Q, Rel (P // PO) (Q // PO) → Rel P Q)
→ howe' Rel P1 Q1 k1 → howe' Rel P2 Q2 k2
→ fn P1 [<=] N → fn Q1 [<=] N → (∀ x, fn (f x) [<=] N)
→ lts (bind f N P1) (inp a) (ag_abs F1)
→ ∃ F2, lts (bind f N Q1) (inp a) (ag_abs F2) ∧
∃ k', howe' Rel (subst F1 P2) (subst F2 Q2) k'.
Proof.
introv Hsim Hrefl Hmaeq Hmswap Htrans HpO Hp1q1. gen a f N k2 F1 P2 Q2.
induction Hp1q1 using howe'_ind_size; introv Hp2q2 HfnP HfnQ Hf HltsP1.
inversion Hp1q1; subst; try solve [inverts HltsP1].
- assert (N [<=] union N (fn R)) by fsetdec.
forwards: aeq_lts_2 HltsP1. apply aeq_bind_2. intro. rewrite Hf. exact H2.
fsetdec. auto. auto. destruct_hyps. inversion H3; subst. rename Q into F2. clear H3.
forwards*: H Hp2q2 H4. nat_math. 3:intro; rewrite Hf. 1-3: fsetdec. clear H.
destruct H3 as [F3 [Hlts2 [k' Hhowe]]].
forwards*: H1 f (union N (fn R)). 3:intro; rewrite Hf. 1-3: fsetdec.
assert (Hwf:conc_wf (conc_def nil Q2 PO)). simpl; split.
constructor. simpl; fsetdec.
forwards_test Rel. rename F'0 into F4. simpl in ×.
unfold appr in H9. simpl in H9. apply HpO in H9. clear Hwf.
forwards: aeq_lts_2 H5. apply aeq_bind_2; eauto. intro; rewrite Hf.
1-2: fsetdec. destruct_hyps. inversion H10; subst; clear H10. rename Q into F5.
∃ F5; intuition. ∃ (S k'). simpl.
eapply mod_aeq_left_howe'; auto. 2: rewrite H6; reflexivity.
apply howe_comp' with (subst F3 Q2); auto. apply oe_trans with (subst F4 Q2); auto.
apply oe_proc0; auto. apply oe_proc0; auto. eapply Hmaeq.
apply Hrefl. reflexivity. rewrite H13. reflexivity.
- ∃ F1; intuition. apply howe_implies_howe'. apply howe_subst; auto with howe.
eapply howe'_implies_howe; eauto.
- rewrite bind_para_simpl in HltsP1. simpl in ×. inverts HltsP1.
+ forwards: lts_inp_abs H5. destruct H2 as [F'1]. subst. simpl in H6.
forwards*: H H5; try nat_math; try fsetdec. destruct H2 as [F'2 [k'' [Hltsf'2 Hhowe]]].
∃ (F'2 // shiftV (bind f N Q'0)). inverts H6. split.
rewrite bind_para_simpl. eapply lts_parl'; eauto.
apply howe_implies_howe'. apply howe'_implies_howe in H0.
apply howe'_implies_howe in H1. apply howe'_implies_howe in Hhowe.
eapply mod_aeq_howe; auto. 2-3: rewrite subst_par; rewrite subst_shift; reflexivity.
constructor; auto. apply howe_bind; auto with howe; try fsetdec.
+ forwards: lts_inp_abs H5. destruct H2 as [F'1]. subst. simpl in H6.
forwards*: H H5; try nat_math; try fsetdec. destruct H2 as [F'2 [k'' [Hltsf'2 Hhowe]]].
∃ (shiftV (bind f N Q) // F'2). inverts H6. split.
rewrite bind_para_simpl. eapply lts_parr'; eauto.
apply howe_implies_howe'. apply howe'_implies_howe in H0.
apply howe'_implies_howe in H1. apply howe'_implies_howe in Hhowe.
eapply mod_aeq_howe; auto. 2-3: rewrite subst_par; rewrite subst_shift; reflexivity.
constructor; auto. apply howe_bind; auto with howe; try fsetdec.
- unfold bind in HltsP1; simpl in *; foldbind in HltsP1. clear H.
inverts HltsP1. simpl in ×. ∃ (bind (liftV f) N Q). split.
unfold bind; simpl; foldbind. auto with hopi.
simpl. apply howe_implies_howe'. apply howe'_implies_howe in H0.
apply howe'_implies_howe in Hp2q2. apply howe_subst; auto with howe.
apply howe_bind; auto; try intros[|x]; simpl; simpl_swap; auto with howe; try fsetdec.
- simpls. simpl_swap in HfnP. rewrite <- swap_fs_notin in HfnP; try fsetdec.
remember (union N (union (fn P2) (fn Q2))) as N'.
assert (∀ x, fn (f x) [<=] N') as Hf' by (intro; rewrite Hf; fsetdec).
forwards: aeq_lts_2 HltsP1. rewrites (>>aeq_bind_3 (nu b, P)); auto.
apply howe_nu_aeq; simpl; simpl_swap. applys (>>aeq_bind_2 N'); simpl; eauto. fsetdec.
destruct_hyps. inversion H2; subst x F1; clear H2.
unfold bind in H3; simpl in *; destruct atom_fresh eqn:?; foldbind in H3.
inverts H3. destruct A as [ | F1 | [] ]; inverts H6. simpl in H8.
assert (x≠a) as Hxa by fsetdec. clear H8.
forwards: H H9; auto. apply howe'_swap; eauto. nat_math. exact Hp2q2.
3:intro; rewrite Hf; fsetdec. 1-2: apply fnsaxp; fsetdec. clear H.
destruct_hyps. assert (lts (bind f N' (nu b, Q)) (inp a) (new x (ag_abs x0))).
{ unfold bind; simpl in *; rewrite Heqs; foldbind. unsimpl (new x (ag_abs x0)).
eauto with hopi. } clear H.
forwards: aeq_lts_2 H3. apply aeq_bind_2; simpl; try exact HfnQ; eauto. fsetdec.
destruct_hyps. inversion H; subst; clear H. rename x0 into F2.
∃ Q0. intuition. eexists. simpls. eapply mod_aeq_left_howe'; auto.
2: rewrite H5; rewrite subst_nu_indep; [ reflexivity | fsetdec].
eapply howe_comp'. 2: eapply mod_aeq_oe; auto. 2: apply oe_refl; auto. 3:reflexivity.
2: rewrite <- H7; apply subst_nu_indep; fsetdec. eauto with howe.
Qed.
Lemma pseudo_inp_conc {V:Set}: ∀ Rel (P1 Q1:proc V) a F1 C (f:V → proc0) N k,
simulation Rel → refl Rel → mod_aeq Rel → mod_swap Rel → trans Rel
→ (∀ P Q, Rel (P // PO) (Q // PO) → Rel P Q)
→ howe' Rel P1 Q1 k → conc_wf C
→ fn P1 [<=] N → fn Q1 [<=] N → (∀ x, fn (f x) [<=] N)
→ lts (bind f N P1) (inp a) (ag_abs F1)
→ ∃ F2 P'2 Q'2, lts (bind f N Q1) (inp a) (ag_abs F2) ∧
P'2 =sc0= (appr F1 C) ∧ Q'2 =sc0= (appr F2 C) ∧
∃ k', howe' Rel P'2 Q'2 k'.
Proof. intros. destruct (conc_convert C (fn (bind f N P1) `union`
fn (bind f N Q1))) as [L' P' Q'] eqn:?.
assert (C =Ac= conc_def L' P' Q').
{ forwards: aeq_conc_convert. rewrite Heqc in H11. auto. }
assert (conc_wf (conc_def L' P' Q')) by auto.
forwards: @howe'_refl Rel P'. destruct H13.
forwards: @pseudo_inp_first V Rel P' P'; eauto.
clear H6 H13.
destruct H14 as [F2]. destruct H6. ∃ F2.
∃ (appr F1 (conc_def L' P' Q')).
∃ (appr F2 (conc_def L' P' Q')).
destruct C. simpl in Heqc. forwards: fn_conc_convert_0' Heqc.
assert (fn F2 [<=] fn (bind f N Q1)). { forwards: lts_fn H6. simpls; auto. }
assert (fn F1 [<=] fn (bind f N P1)). { forwards: lts_fn H10. simpls; auto. }
splits; try rewrite H11; eauto with sc.
unfold appr. simpl. repeat rewrite conc_convert_indep_wf; auto; try fsetdec.
apply howe_implies_howe'. destruct H13. apply howe'_implies_howe in H13.
apply howe_genNu. constructor; auto with howe.
Qed.
Lemma pseudo_sim_out : pseudo_sim.
Proof. rewrite pseudo_sim_equiv.
introv Hsim Hrefl Hmaeq Hmswap Hsc0 Htrans Hp2q2.
assert (∀ P Q : proc0, Rel (P // PO) (Q // PO) → Rel P Q) as HpO.
{ intros. apply Htrans with (Q//PO). apply Htrans with (P//PO).
apply Hsc0; constructor. auto. apply Hsc0; constructor. }
gen a N f g F1 C1 P1 Q1. induction Hp2q2 using howe'_ind_size.
introv Hp1q1 HfnP1 HfnP2 HfnQ1 HfnQ2; introv Hf Hg HltsP1 HltsP2;
inversion Hp2q2; clear Hp2q2; subst; try solve [inverts HltsP2].
- assert (N [<=] union N (fn R)) by fsetdec.
forwards: aeq_lts_2 HltsP1. apply aeq_bind_2. intro. rewrite Hf. exact H2.
fsetdec. auto. auto. destruct_hyps. inversion H3; subst. rename Q into F2. clear H3.
forwards: aeq_lts_2 HltsP2. apply aeq_bind_2. intro. rewrite Hg. exact H2.
fsetdec. auto. auto. destruct_hyps. inversion H3; subst. rename C' into C2. clear H3.
forwards: H (union N (fn R)); eauto; try solve [try fsetdec; intros;
try rewrite Hf; try rewrite Hg; fsetdec]. nat_math. clear H.
destruct H3 as [F3 [C3 [ P'3 [R' [HltsQ1 [ HltsR [Hp'3 [Hr' Hhowe]]]]]]]].
forwards*: H1 g (union N (fn R)); try solve [try fsetdec; intros;
try rewrite Hf; try rewrite Hg; fsetdec].
forwards_test Rel; clear H3 H9 H10. rename C'0 into C4.
forwards: aeq_lts_2 H7. apply aeq_bind_2. intro. apply Hg. auto.
intro; rewrite Hg; fsetdec. fsetdec. destruct_hyps. inversion H3; subst.
rename C' into C5. clear H3.
forwards: aeq_lts_2 HltsQ1. apply aeq_bind_2. intro. apply Hf. auto.
intro; rewrite Hf; fsetdec. fsetdec. destruct_hyps. inversion H3; subst.
rename Q into F4. clear H3.
∃ F4 C5 P'3 (appr F4 C4); intuition.
rewrite Hp'3. rewrite H6; rewrite H8; reflexivity.
rewrite H13; reflexivity.
∃ (S x0). apply howe_comp' with R'; auto with hopi howe.
apply oe_trans with (appr F3 C3); auto. apply oe_sc0; auto.
apply oe_proc0; auto. apply Htrans with (appr F3 C4); auto.
apply Hsc0. rewrite H13; rewrite H15; reflexivity.
- forwards: @pseudo_inp_conc P1 Q1 F1 C1; eauto with hopi.
destruct H0 as [F2 [P'2 [Q'2 ]]]. ∃ F2 C1 P'2 Q'2; intuition.
- unfold bind in HltsP2; simpl in HltsP2; foldbind in HltsP2. inverts HltsP2; simpls.
+ forwards: lts_out_conc H5. destruct H2 as [C'1]. subst. inversion H6. subst.
clear H6. forwards*: H Hp1q1 HltsP1 H5; auto; try fsetdec. nat_math.
destruct H2 as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 [k'2 Hhowe]]]]]]]]].
∃ F'2 (conc_parl C'2 (bind g N Q'0)) (P'2// bind g N P'0) (Q'2//bind g N Q'0).
splits; eauto with hopi howe.
× unfold bind; simpl; foldbind; eapply lts_parl'; eauto.
× rewrite Hp'2. apply sc_appr_conc_parl; auto.
× rewrite Hq'2. apply sc_appr_conc_parl; auto.
× forwards*: @howe'_bind P'0 Q'0; auto with howe. 1-2:fsetdec.
destruct_hyps. eexists; constructor; eauto.
+ forwards: lts_out_conc H5. destruct H2 as [C'1]. subst. inversion H6. subst.
clear H6. forwards*: H Hp1q1 HltsP1 H5; auto; try fsetdec. nat_math.
destruct H2 as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 [k'2 Hhowe]]]]]]]]].
∃ F'2 (conc_parr (bind g N Q) C'2) (bind g N P//P'2) (bind g N Q//Q'2).
splits; eauto with hopi howe.
× unfold bind; simpl; foldbind; eapply lts_parr'; eauto.
× rewrite Hp'2. apply sc_appr_conc_parr; auto.
× rewrite Hq'2. apply sc_appr_conc_parr; auto.
× forwards*: @howe'_bind P Q; auto with howe. 1-2:fsetdec.
destruct_hyps. eexists; constructor; eauto.
- clear H. unfold bind in HltsP2; simpl in HltsP2; foldbind in HltsP2. inverts HltsP2.
simpls. forwards: @howe'_bind Rel P Q g g; eauto with howe. 1-2:fsetdec.
forwards: @howe'_bind Rel P'0 Q'0 g g; eauto with howe. 1-2:fsetdec. destruct_hyps.
forwards*: @pseudo_inp_first Rel P1 Q1 (bind g N P)(bind g N Q).
destruct H3 as [F2 [HltsQ1 HhoweF1F2]].
∃ F2 (conc_def nil (bind g N Q) (bind g N Q'0)). do 2 (eexists).
splits; auto; try reflexivity.
unfold bind; simpl; foldbind; constructor.
destruct_hyps; eexists; unfold appr; simpl; constructor; eauto.
- unfold bind in HltsP2; simpl in *; destruct atom_fresh eqn:?; foldbind in HltsP2.
simpl_swap in HfnP2. rewrite <- swap_fs_notin in HfnP2; try fsetdec.
inverts HltsP2. destruct A as [ | | C2 ]; inverts H4. simpl in H6.
assert (x≠a) as Hxa by fsetdec. clear H6.
assert (N [<=] add x N) by fsetdec.
forwards: aeq_lts_2 H7. rewrites (>>aeq_bind_3 (swap b x P)); auto.
apply fnsaxp; auto. rewrite swap_sym. symmetry. apply aeq_swap_cut_notin.
intuition. reflexivity. destruct_hyps. inversion H3; subst x0 C; clear H3.
rename C' into C4.
forwards: aeq_lts_2 HltsP1. apply aeq_bind_2. intro. rewrite Hf. exact H2.
fsetdec. auto. auto. destruct_hyps. inversion H3; subst. rename Q0 into F2. clear H3.
forwards: H H4; auto. apply howe'_swap; eauto. nat_math. exact Hp1q1.
5:intro; rewrite (Hf x0); fsetdec. 1,3: fsetdec. 1-2: apply fnsaxp; auto.
intro; rewrite Hg; fsetdec. exact H5. clear H.
destruct H3 as [F3 [C3 [ P'3 [R' [HltsQ1 [ HltsR [Hp'3 [Hr' [k' Hhowe]]]]]]]]].
forwards: aeq_lts_2 HltsQ1. apply aeq_bind_2. intro; apply Hf. auto.
intro; rewrite Hf; fsetdec. fsetdec. destruct_hyps. inversion H; subst.
rename Q0 into F4. clear H.
∃ F4 (conc_new x C3) (nu x, P'3) (nu x, (appr F4 C3)).
splits; auto.
+ unfold bind; simpl in *; rewrite Heqs; foldbind. unsimpl (new x (ag_conc C3)).
eauto with hopi.
+ rewrite Hp'3. rewrite <- H9. rewrite sc_appr_nu_indep_right; [| | auto]. rewrite H6; reflexivity. rewrites (>>lts_fn HltsP1). rewrite fn_bind; auto; fsetdec.
+ apply sc_appr_nu_indep_right; [| auto]. rewrites (>>lts_fn H3).
rewrite fn_bind; auto; fsetdec.
+ eexists. apply howe'_nu_same. eapply howe_comp'. eauto with howe.
eapply oe_trans; auto. apply oe_sc0; eauto. apply oe_proc0; auto.
eapply Hmaeq. apply Hrefl. reflexivity. rewrite H10; reflexivity.
Qed.
Lemma pseudo_out_first {V:Set}:
∀ Rel (P1 Q1:proc V) (P2 Q2:proc1) a C1 (f:V → proc0) N k1 k2,
simulation Rel → refl Rel → mod_aeq Rel → mod_swap Rel →
(Rincl sc0 Rel) → trans Rel →
howe' Rel P1 Q1 k1 → howe' Rel P2 Q2 k2 →
fn P1 [<=] N → fn Q1 [<=] N → (∀ x, fn (f x) [<=] N) →
lts (bind f N P1) (out a) (ag_conc C1) →
∃ C2 P'2 Q'2, lts (bind f N Q1) (out a) (ag_conc C2) ∧
P'2 =sc0= (appr P2 C1) ∧
Q'2 =sc0= (appr Q2 C2) ∧
∃ k'2, howe' Rel P'2 Q'2 k'2.
Proof. introv Hsim Hrefl Hmaeq Hmswap HRincl. introv Htrans Hp1q1 Hp2q2 HfnP HfnQ Hf HltsP1.
gen P2 Q2 k2 a C1 f N. induction Hp1q1 using howe'_ind_size. intros.
inversion Hp1q1; subst; try solve [inverts HltsP1].
- assert (N [<=] union N (fn R)) by fsetdec.
forwards: aeq_lts_2 HltsP1. apply aeq_bind_2. intro. rewrite Hf. exact H2.
fsetdec. auto. auto. destruct_hyps. inversion H3; subst. clear H3.
forwards*: H H4. nat_math. 3:intro; rewrite Hf. 1-3: fsetdec. clear H.
destruct H3 as [C2 [P'2 [Q'2 [Hlts2 [Hsc1 [Hsc2 [k' Hhowe]]]]]]].
forwards*: H1 f (union N (fn R)). 3:intro; rewrite Hf. 1-3: fsetdec.
specialize (Hsim _ _ H). intuition auto. forwards*: H8 Q2.
destruct H5 as [C'0]. clear H3 H7 H8.
forwards: aeq_lts_2 H5. apply aeq_bind_2; eauto. intro; rewrite Hf.
1-2: fsetdec. destruct_hyps. inversion H3; subst; clear H3.
∃ C'1 P'2 (appr Q2 C'0); intuition.
rewrite Hsc1. rewrite H6. reflexivity. rewrite H10. reflexivity.
∃ (S k'). apply howe_comp' with Q'2; auto.
apply oe_trans with (appr Q2 C2); auto.
apply oe_sc0; auto. apply oe_proc0; auto.
- ∃ C1 (appr P2 C1) (appr Q2 C1); intuition.
apply howe_implies_howe'. apply howe'_implies_howe in Hp2q2.
remember (conc_convert C1 (union (fn P2) (fn Q2))) as C'1.
assert (C1=Ac=C'1). { subst. apply aeq_conc_convert. }
eapply mod_aeq_howe; auto; try rewrite H0; try reflexivity.
unfold appr. destruct C'1 as [C'L C'P C'Q]; destruct C1 as [CL CP CQ]; simpls.
symmetry in HeqC'1. forwards: fn_conc_convert_0' HeqC'1.
repeat rewrite conc_convert_indep_wf; auto. 2-3:fsetdec.
apply howe_genNu. constructor; try apply howe_subst; auto with howe.
- rewrite bind_para_simpl in HltsP1. simpl in ×. inverts HltsP1.
+ forwards: lts_out_conc H5. destruct H2 as [C']. subst. simpl in H6.
forwards*: H H5; try nat_math; try fsetdec. clear H.
destruct H2 as [C'2 [P'2 [Q'2 [Hltsf' [Hsc1 [Hsc2 [k'' Hhowe]]]]]]].
∃ (conc_parl C'2 (bind f N Q'0)) (P'2//bind f N P'0) (Q'2//bind f N Q'0).
inversion H6. clear H6. splits.
× rewrite bind_para_simpl. eapply lts_parl'; eauto.
× remember (conc_convert C' (union (fn P2) (fn (bind f N P'0)))) as C'1.
assert (C'=Ac=C'1). { subst. apply aeq_conc_convert. } rewrite Hsc1. rewrite H.
unfold appr. unfold conc_parl. destruct C'1 as [C'L C'P C'Q];
destruct C' as [CL CP CQ]; simpls.
symmetry in HeqC'1. forwards: fn_conc_convert_0' HeqC'1.
repeat (rewrite conc_convert_indep_wf; auto; simpl). 2-4:fsetdec.
rewrite <- sc_scope_genNu. 2:fsetdec. eauto with sc.
× remember (conc_convert C'2 (union (fn Q2) (fn (bind f N Q'0)))) as C'1.
assert (C'2=Ac=C'1). { subst. apply aeq_conc_convert. } rewrite Hsc2. rewrite H.
unfold appr. unfold conc_parl. destruct C'1 as [C'L C'P C'Q];
destruct C'2 as [CL CP CQ]; simpls.
symmetry in HeqC'1. forwards: fn_conc_convert_0' HeqC'1.
repeat (rewrite conc_convert_indep_wf; auto; simpl). 2-4:fsetdec.
rewrite <- sc_scope_genNu. 2:fsetdec. eauto with sc.
× forwards*: @howe'_bind W H1; auto with howe. 1-2:fsetdec.
destruct_hyps. eexists; constructor; eauto.
+ forwards: lts_out_conc H5. destruct H2 as [C']. subst. simpl in H6.
forwards*: H H5; try nat_math; try fsetdec. clear H.
destruct H2 as [C'2 [P'2 [Q'2 [Hltsf' [Hsc1 [Hsc2 [k'' Hhowe]]]]]]].
∃ (conc_parr (bind f N Q) C'2) (bind f N P//P'2) (bind f N Q//Q'2).
inversion H6. clear H6. splits.
× rewrite bind_para_simpl. eapply lts_parr'; eauto.
× remember (conc_convert C' (union (fn P2) (fn (bind f N P)))) as C'1.
assert (C'=Ac=C'1). { subst. apply aeq_conc_convert. } rewrite Hsc1. rewrite H.
unfold appr. unfold conc_parr. destruct C'1 as [C'L C'P C'Q];
destruct C' as [CL CP CQ]; simpls.
symmetry in HeqC'1. forwards: fn_conc_convert_0' HeqC'1.
repeat (rewrite conc_convert_indep_wf; auto; simpl). 2-4:fsetdec.
rewrite sc_par_comm. rewrite <- sc_scope_genNu. 2:fsetdec. eauto with sc.
× remember (conc_convert C'2 (union (fn Q2) (fn (bind f N Q)))) as C'1.
assert (C'2=Ac=C'1). { subst. apply aeq_conc_convert. } rewrite Hsc2. rewrite H.
unfold appr. unfold conc_parr. destruct C'1 as [C'L C'P C'Q];
destruct C'2 as [CL CP CQ]; simpls.
symmetry in HeqC'1. forwards: fn_conc_convert_0' HeqC'1.
repeat (rewrite conc_convert_indep_wf; auto; simpl). 2-4:fsetdec.
rewrite sc_par_comm. rewrite <- sc_scope_genNu. 2:fsetdec. eauto with sc.
× forwards*: @howe'_bind W H0; auto with howe. 1-2:fsetdec.
destruct_hyps. eexists; constructor; eauto.
- unfold bind in HltsP1; simpl in *; foldbind in HltsP1. clear H.
inverts HltsP1. ∃ (conc_def nil (bind f N Q) (bind f N Q'0)). eexists. eexists.
splits. unfold bind; simpl; foldbind. auto with hopi. 1-2:reflexivity.
apply howe_implies_howe'. apply howe'_implies_howe in H0.
apply howe'_implies_howe in H1. apply howe'_implies_howe in Hp2q2.
unfold appr; simpls. constructor. apply howe_subst; auto.
1-2: apply howe_bind; auto with howe; fsetdec.
- simpls. simpl_swap in HfnP. rewrite <- swap_fs_notin in HfnP; try fsetdec.
remember (union N (union (fn P2) (fn Q2))) as N'.
assert (∀ x, fn (f x) [<=] N') as Hf' by (intro; rewrite Hf; fsetdec).
forwards: aeq_lts_2 HltsP1. rewrites (>>aeq_bind_3 (nu b, P)); auto.
apply howe_nu_aeq; simpl; simpl_swap. apply aeq_bind_2; simpl; eauto. fsetdec.
destruct_hyps. inversion H2; subst x C; clear H2.
unfold bind in H3; simpl in H3; destruct atom_fresh eqn:?; foldbind in H3.
inverts H3. destruct A as [ | | [] ]; inverts H6. simpl in H8.
assert (x≠a) as Hxa by fsetdec. clear H8.
forwards: H Hp2q2 H9; auto. apply howe'_swap; eauto. nat_math.
3:intro; rewrite Hf'; fsetdec. 1-2: apply fnsaxp; fsetdec. clear H.
destruct_hyps. assert (lts (bind f N' (nu b, Q)) (out a) (new x x0)).
{ unfold bind; simpl in *; rewrite Heqs; foldbind. unsimpl (new x x0).
eauto with hopi. }
forwards: aeq_lts_2 H6. apply aeq_bind_2; simpl; try exact HfnQ; eauto. fsetdec.
destruct_hyps. inversion H7; subst; clear H7.
∃ C' (nu x, x1) (nu x, x2). splits; auto. 3: eexists; eauto with howe.
rewrite H2; rewrite H5; apply sc_appr_nu_indep_right; auto.
rewrite H3; rewrite <- H11; apply sc_appr_nu_indep_right; auto. Qed.
Lemma pseudo_sim_in : pseudo_sim.
Proof. rewrite pseudo_sim_equiv.
introv Hsim Hrefl Hmaeq Hmswap Hsc0 Htrans Hp2q2 Hp1q1.
gen a N f g F1 C1 P2 Q2. induction Hp1q1 using howe'_ind_size.
introv Hp2q2 HfnP1 HfnP2 HfnQ1 HfnQ2; introv Hf Hg HltsP1 HltsP2;
inversion Hp1q1; clear Hp1q1; subst; try solve [inverts HltsP1].
- assert (N [<=] union N (fn R)) by fsetdec.
forwards: aeq_lts_2 HltsP1. apply aeq_bind_2. intro. rewrite Hf. exact H2.
fsetdec. auto. auto. destruct_hyps. inversion H3; subst. rename Q into F2. clear H3.
forwards: aeq_lts_2 HltsP2. apply aeq_bind_2. intro. rewrite Hg. exact H2.
fsetdec. auto. auto. destruct_hyps. inversion H3; subst. rename C' into C2. clear H3.
forwards: H (union N (fn R)); eauto; try solve [try fsetdec; intros;
try rewrite Hf; try rewrite Hg; fsetdec]. nat_math. clear H.
destruct H3 as [F3 [C3 [ P'3 [R' [HltsR [ HltsQ2 [Hp'3 [Hr' Hhowe]]]]]]]].
forwards*: H1 f (union N (fn R)); try solve [try fsetdec; intros;
try rewrite Hf; try rewrite Hg; fsetdec].
assert (conc_wf C3) by auto.
forwards_test Rel; clear H7 H10 H11. rename F'0 into F4.
forwards: aeq_lts_2 H9. apply aeq_bind_2. intro. apply Hf. auto.
intro; rewrite Hf; fsetdec. fsetdec. destruct_hyps. inversion H7; subst.
rename Q into F5. clear H7.
forwards: aeq_lts_2 HltsQ2. apply aeq_bind_2. intro. apply Hg. auto.
intro; rewrite Hg; fsetdec. fsetdec. destruct_hyps. inversion H7; subst.
rename C' into C4. clear H7.
∃ F5 C4 P'3 (appr F5 C4); intuition.
rewrite Hp'3. rewrite H6; rewrite H8; reflexivity.
∃ (S x0). apply howe_comp' with R'; auto with hopi howe.
apply oe_trans with (appr F3 C3); auto. apply oe_sc0; auto.
apply oe_proc0; auto. apply Htrans with (appr F4 C3); auto.
apply Hsc0. rewrite H14; rewrite H16; reflexivity.
- simpl in ×. forwards: @howe'_refl Rel F1. destruct_hyps.
forwards: @pseudo_out_first P2 Q2 F1 F1 C1; eauto with howe hopi.
destruct H1 as [C2 [ P'2 [Q'2 [HltsC2 [Hp'2 [Hq'2 Hhowe]]]]]].
∃ F1 C2 P'2 Q'2; intuition.
- unfold bind in HltsP1; simpl in HltsP1; foldbind in HltsP1. inverts HltsP1; simpls.
+ forwards: lts_inp_abs H5. destruct H2 as [F2]. subst. inversion H6. subst.
clear H6. forwards*: H Hp2q2 H5 HltsP2; auto; try fsetdec. nat_math. clear H.
destruct H2 as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 [k'2 Hhowe]]]]]]]]].
∃ (F'2 // shiftV (bind f N Q'0)) C'2 (P'2// bind f N P'0) (Q'2//bind f N Q'0).
splits; eauto with hopi howe.
× unfold bind; simpl; foldbind; eapply lts_parl'; eauto.
× rewrite Hp'2. symmetry. apply sc_appr_par_shift_right; auto.
× rewrite Hq'2. symmetry. apply sc_appr_par_shift_right; auto.
× forwards*: @howe'_bind P'0 Q'0; auto with howe. 1-2:fsetdec.
destruct_hyps. eexists; constructor; eauto.
+ forwards: lts_inp_abs H5. destruct H2 as [F2]. subst. inversion H6. subst.
clear H6. forwards*: H Hp2q2 H5 HltsP2; auto; try fsetdec. nat_math. clear H.
destruct H2 as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 [k'2 Hhowe]]]]]]]]].
∃ (shiftV (bind f N Q) // F'2) C'2 (bind f N P//P'2) (bind f N Q//Q'2).
splits; eauto with hopi howe.
× unfold bind; simpl; foldbind; eapply lts_parr'; eauto.
× rewrite Hp'2. symmetry. apply sc_appr_par_shift_left; auto.
× rewrite Hq'2. symmetry. apply sc_appr_par_shift_left; auto.
× forwards*: @howe'_bind P Q; auto with howe. 1-2:fsetdec.
destruct_hyps. eexists; constructor; eauto.
- clear H. unfold bind in HltsP1; simpl in HltsP1; foldbind in HltsP1. inverts HltsP1.
simpls. forwards*: @howe'_bind P Q (liftV f) (liftV f) N; auto with howe.
3-4:fsetdec. 1-2: intros [|x]; simpl; simpl_swap; fsetdec. destruct_hyps.
forwards*: @pseudo_out_first Rel P2 Q2.
destruct H1 as [C2 [P'2 [Q'2 [HltsQ2 [Hsc1 [Hsc2 [k' Hhowe]]]]]]].
∃ (bind (liftV f) N Q) C2 P'2 Q'2. splits; auto.
unfold bind; simpl; foldbind; constructor. eexists; eauto.
- unfold bind in HltsP1; simpl in *; destruct atom_fresh eqn:?; foldbind in HltsP1.
simpl_swap in HfnP1. rewrite <- swap_fs_notin in HfnP1; try fsetdec.
inverts HltsP1. destruct A as [ | F2 | ]; inverts H4. simpl in H6.
assert (x≠a) as Hxa by fsetdec. clear H6.
assert (N [<=] add x N) by fsetdec.
forwards: aeq_lts_2 HltsP2. apply aeq_bind_2. intro. rewrite Hg. exact H2.
fsetdec. auto. auto. destruct_hyps. inversion H3; subst. clear H3.
forwards: aeq_lts_2 H7. rewrites (>>aeq_bind_3 (swap b x P)); auto.
apply fnsaxp; auto. rewrite swap_sym. symmetry. apply aeq_swap_cut_notin.
intuition. reflexivity. destruct_hyps. inversion H3; subst x0 P0; clear H3.
rename Q0 into F'2.
forwards: H H5; auto. apply howe'_swap; eauto. nat_math. exact Hp2q2.
5:intro; rewrite (Hf x0); fsetdec. 6:eauto. 1,3: apply fnsaxp; auto.
1-2:fsetdec. intro; rewrite Hg; fsetdec. clear H.
destruct H3 as [F3 [C3 [ P'3 [R' [HltsQ1 [ HltsR [Hp'3 [Hr' [k' Hhowe]]]]]]]]].
forwards: aeq_lts_2 HltsR. apply aeq_bind_2. intro. apply Hg. auto.
intro; rewrite Hg; fsetdec. fsetdec. destruct_hyps. inversion H; subst. clear H.
∃ (nu x, F3) C'0 (nu x, P'3) (nu x, (appr F3 C3)).
splits; auto.
+ unfold bind; simpl in *; rewrite Heqs; foldbind. unsimpl (new x (ag_abs F3)).
eauto with hopi.
+ rewrite Hp'3. rewrite <- H6. rewrite H9. symmetry. apply sc_appr_nu_indep_left; [|auto].
rewrites (>>lts_fn HltsP2). rewrite fn_bind; auto.
+ rewrite H10. symmetry. apply sc_appr_nu_indep_left; [|auto]. rewrites (>>lts_fn H3). rewrite fn_bind; auto.
+ eexists. apply howe'_nu_same. eapply howe_comp'. eauto with howe.
eapply oe_trans; auto. apply oe_sc0; eauto. apply oe_proc0; auto.
Qed.
Simultaneous proof
Lemma pseudo_sim_sim' : pseudo_sim'.
Proof. introv Hsim Hrefl Hmaeq Hmswap Hsc0 Htrans.
Require Import TLC.LibWf. assert (wf (lexico2 Peano.lt Peano.lt)).
rewrite <- LibNat.lt_peano.
apply wf_lexico2; auto with wf.
remember (k2, k1) as p. gen V W.
gen k1 k2 a N F1 C1.
induction_wf IH: H p. intros n1 n2 Hp. subst.
assert (∀ (V2 : Set) (a:var) (P1 Q1 : proc1) N (n1 : nat) (P2 Q2 : proc V2),
howe' Rel P1 Q1 n1 → howe' Rel P2 Q2 n2 →
∀ (g : V2 → proc0) (C1 : conc),
fn P1 [<=] N → fn Q1 [<=] N →
fn P2 [<=] N → fn Q2 [<=] N → (∀ x, fn (g x) [<=] N) →
lts (bind g N P2) (out a) C1 →
∃ (C2:conc) P'2 Q'2,
lts (bind g N Q2) (out a) C2 ∧ sc0 P'2 (appr P1 C1)
∧ sc0 Q'2 (appr Q1 C2) ∧ ∃ x3, howe' Rel P'2 Q'2 x3).
{ introv Hp1q1 Hp2q2 Hfnp1 Hfnq1 Hfnp2 Hfnq2 Hg HltsP2.
assert (howe' Rel (a? P1) (a? Q1)(S n0)) by auto with howe.
remember (pr_var (V:=Empty_set)) as f.
assert (∀ P N, fn P[<=]N → bind (liftV f) N P =A= P).
intros. apply @bind_return. intros [|]; simpl; auto; inversion e. auto.
assert (a `in` N). { destruct (classic (a `in` N)); auto. forwards:
notin_fn_notin_fnlab a HltsP2. rewrite fn_bind; auto. simpl in H3. fsetdec. }
destruct Hp2q2; try solve [inverts HltsP2].
- assert (N [<=] union N (fn R)) by fsetdec.
forwards: aeq_lts_2 HltsP2. apply aeq_bind_2. intro. rewrite Hg. exact H4.
fsetdec. auto. auto. destruct_hyps. inversion H5; subst x C.
rename C' into C2. clear H5.
forwards: IH (k, S n0) f Hp2q2 H0 H6; try solve [subst; simpl; eauto with hopi].
1-4:simpl; fsetdec. intro; fsetdec. intro; rewrite Hg; auto.
unfold bind; simpl; foldbind. eauto with hopi. clear IH.
destruct H5 as [F3 [C3 [ P'3 [R' [HltsR [ HltsQ2 [Hp'3 [Hr' Hhowe]]]]]]]].
rewrite H1 in Hp'3 by fsetdec.
forwards*: H3 g (union N (fn R)); try solve [try fsetdec; intros;
try rewrite Hf; try rewrite Hg; fsetdec].
assert (conc_wf C3) by auto. forwards_test Rel; clear H9 H11 H12.
forwards: aeq_lts_2 H10. apply aeq_bind_2. intro. apply Hg. auto.
intro; rewrite Hg; fsetdec. fsetdec. destruct_hyps. inversion H9; subst. clear H9.
unfold bind in HltsR; simpl in HltsR; foldbind in HltsR. inversion HltsR;
subst F3 P0 a0. rewrite H1 in Hr' by fsetdec.
∃ C' P'3 (appr Q1 C'). intuition.
rewrite Hp'3; rewrite H8; reflexivity.
∃ (S x0). apply howe_comp' with R'; auto with hopi howe.
apply oe_trans with (appr Q1 C3); auto. apply oe_sc0; auto.
apply oe_proc0; auto. apply (Hmaeq _ _ _ _ H13); rewrite H1 by fsetdec;
try rewrite H15; reflexivity.
- ∃ C1 (appr P1 C1) (appr Q1 C1). intuition.
apply howe_implies_howe'. apply howe'_implies_howe in Hp1q1.
remember (conc_convert C1 (union (fn P1) (fn Q1))) as C'1.
assert (C1=Ac=C'1). { subst. apply aeq_conc_convert. }
eapply mod_aeq_howe; auto; try rewrite H3; try reflexivity.
unfold appr. destruct C'1 as [C'L C'P C'Q]; destruct C1 as [CL CP CQ]; simpls.
symmetry in HeqC'1. forwards: fn_conc_convert_0' HeqC'1.
repeat (rewrite conc_convert_indep_wf; auto; simpl). 2-3:clears N C'P; fsetdec.
apply howe_genNu. constructor; try apply howe_subst; auto with howe.
- unfold bind in HltsP2; simpl in HltsP2; foldbind in HltsP2. inverts HltsP2; simpls.
+ forwards: lts_out_conc H6. destruct H3 as [C']. subst A. simpl in H7.
forwards*: IH f g H6; simpl; auto; try nat_math; try fsetdec.
unfold bind; simpl; foldbind. eauto with hopi. clear IH.
destruct H3 as [F'2 [C'2 [P'2 [Q'2 [HltsQ1 [HltsQ [Hsc1 [Hsc2 [k'' Hhowe]]]]]]]]].
∃ (conc_parl C'2 (bind g N Q')) (P'2//bind g N P') (Q'2//bind g N Q').
unfold bind in HltsQ1; simpl in HltsQ1; foldbind in HltsQ1. inversion HltsQ1;
subst. rewrite H1 in Hsc1 by fsetdec. rewrite H1 in Hsc2 by fsetdec.
inversion H7. subst. clear H7. splits.
× rewrite bind_para_simpl. eapply lts_parl'; eauto.
× remember (conc_convert C' (union (fn P1) (fn (bind g N P')))) as C'1.
assert (C'=Ac=C'1). { subst. apply aeq_conc_convert. } rewrite Hsc1. rewrite H3.
unfold appr. unfold conc_parl. destruct C'1 as [C'L C'P C'Q];
destruct C' as [CL CP CQ]; simpls.
symmetry in HeqC'1. forwards: fn_conc_convert_0' HeqC'1.
repeat (rewrite conc_convert_indep_wf; auto; simpl).
rewrite <- sc_scope_genNu. eauto with sc. all:clears P Q CP C'P a; fsetdec.
× remember (conc_convert C'2 (union (fn Q1) (fn (bind g N Q')))) as C'1.
assert (C'2=Ac=C'1). { subst. apply aeq_conc_convert. } rewrite Hsc2. rewrite H3.
unfold appr. unfold conc_parl. destruct C'1 as [C'L C'P C'Q];
destruct C'2 as [CL CP CQ]; simpls.
symmetry in HeqC'1. forwards: fn_conc_convert_0' HeqC'1.
repeat (rewrite conc_convert_indep_wf; auto; simpl).
rewrite <- sc_scope_genNu. eauto with sc. all:clears P Q CP C'P a; fsetdec.
× forwards*: @howe'_bind Hp2q2_2; auto with howe. 1-2:fsetdec.
destruct_hyps. eexists; constructor; eauto.
+ forwards: lts_out_conc H6. destruct H3 as [C']. subst A. simpl in H7.
forwards*: IH f g H6; simpl; auto; try nat_math; try fsetdec.
unfold bind; simpl; foldbind. eauto with hopi. clear IH.
destruct H3 as [F'2 [C'2 [P'2 [Q'2 [HltsQ1 [HltsQ [Hsc1 [Hsc2 [k'' Hhowe]]]]]]]]].
∃ (conc_parr (bind g N Q) C'2) (bind g N P//P'2) (bind g N Q//Q'2).
unfold bind in HltsQ1; simpl in HltsQ1; foldbind in HltsQ1. inversion HltsQ1;
subst. rewrite H1 in Hsc1 by fsetdec. rewrite H1 in Hsc2 by fsetdec.
inversion H7. subst. clear H7. splits.
× rewrite bind_para_simpl. eapply lts_parr'; eauto.
× remember (conc_convert C' (union (fn P1) (fn (bind g N P)))) as C'1.
assert (C'=Ac=C'1). { subst. apply aeq_conc_convert. } rewrite Hsc1. rewrite H3.
unfold appr. unfold conc_parr. destruct C'1 as [C'L C'P C'Q];
destruct C' as [CL CP CQ]; simpls.
symmetry in HeqC'1. forwards: fn_conc_convert_0' HeqC'1.
repeat (rewrite conc_convert_indep_wf; auto; simpl).
rewrite sc_par_comm. rewrite <- sc_scope_genNu. eauto with sc.
all:clears P' Q' CP C'P a; fsetdec.
× remember (conc_convert C'2 (union (fn Q1) (fn (bind g N Q)))) as C'1.
assert (C'2=Ac=C'1). { subst. apply aeq_conc_convert. } rewrite Hsc2. rewrite H3.
unfold appr. unfold conc_parr. destruct C'1 as [C'L C'P C'Q];
destruct C'2 as [CL CP CQ]; simpls.
symmetry in HeqC'1. forwards: fn_conc_convert_0' HeqC'1.
repeat (rewrite conc_convert_indep_wf; auto; simpl).
rewrite sc_par_comm. rewrite <- sc_scope_genNu. eauto with sc.
all:clears P' Q' CP C'P a; fsetdec.
× forwards*: @howe'_bind Hp2q2_1; auto with howe. 1-2:fsetdec.
destruct_hyps. eexists; constructor; eauto.
- unfold bind in HltsP2; simpl in *; foldbind in HltsP2. clear IH.
inverts HltsP2. ∃ (conc_def nil (bind g N Q) (bind g N Q')). eexists. eexists.
splits. unfold bind; simpl; foldbind. auto with hopi. 1-2:reflexivity.
apply howe_implies_howe'. apply howe'_implies_howe in Hp1q1.
apply howe'_implies_howe in Hp2q2_1. apply howe'_implies_howe in Hp2q2_2.
unfold appr; simpls. constructor. apply howe_subst; auto.
1-2: apply howe_bind; auto with howe; fsetdec.
- simpls. simpl_swap in Hfnp2. rewrite <- swap_fs_notin in Hfnp2; try fsetdec.
forwards: aeq_lts_2 HltsP2. rewrites (>>aeq_bind_3 (nu b, P)); auto.
apply howe_nu_aeq; simpl; simpl_swap. apply aeq_bind_2; simpl; eauto.
destruct_hyps. inversion H4; subst x C; clear H4.
unfold bind in H5; simpl in H5; destruct atom_fresh eqn:?; foldbind in H5.
inverts H5. destruct A as [ | | C2 ]; inverts H8. simpl in H10.
assert (x≠a) as Hxa by fsetdec. clear H10.
forwards: IH f g H0 H11; auto. 2:apply howe'_swap; eauto. simpl; auto.
1,3: simpl; fsetdec. 1-2: apply fnsaxp; auto. intro; fsetdec. intro;
rewrite Hg; fsetdec. unfold bind; simpl; foldbind. eauto with hopi. clear IH.
destruct H4 as [F'2 [C'2 [P'2 [Q'2 [HltsQ1 [HltsQ [Hsc1 [Hsc2 [k'' Hhowe]]]]]]]]].
unfold bind in HltsQ1; simpl in HltsQ1; foldbind in HltsQ1. inversion HltsQ1;
subst. rewrite H1 in Hsc1 by fsetdec. rewrite H1 in Hsc2 by fsetdec.
∃ (conc_new x C'2) (nu x, P'2) (nu x, Q'2). splits.
unfold bind; simpl in *; rewrite Heqs; foldbind. unsimpl (new x C'2); eauto with hopi.
rewrite Hsc1. rewrite sc_appr_nu_indep_right; auto. rewrite H7. reflexivity.
rewrite Hsc2; apply sc_appr_nu_indep_right; auto. eexists; eauto with howe.
}
introv Hp2q2 Hp1q1 Hfnp1 Hfnq1 Hfnp2 Hfnq2 Hf Hg HltsP1 HltsP2.
destruct Hp1q1; try solve [inverts HltsP1].
- clear H0. assert (N [<=] union N (fn R)) by fsetdec.
forwards: aeq_lts_2 HltsP1. apply aeq_bind_2. intro. rewrite Hf. exact H0.
fsetdec. auto. auto. destruct_hyps. inversion H2; subst. rename Q0 into F2. clear H2.
forwards: aeq_lts_2 HltsP2. apply aeq_bind_2. intro. rewrite Hg. exact H0.
fsetdec. auto. auto. destruct_hyps. inversion H2; subst. rename C' into C2. clear H2.
forwards: IH (union N (fn R)) Hp2q2; eauto; try solve [try fsetdec; intros;
try rewrite Hf; try rewrite Hg; fsetdec]. simpl;auto. clear IH.
destruct H2 as [F3 [C3 [ P'3 [R' [HltsR [ HltsQ2 [Hp'3 [Hr' Hhowe]]]]]]]].
forwards*: H1 f (union N (fn R)); try solve [try fsetdec; intros;
try rewrite Hf; try rewrite Hg; fsetdec].
assert (conc_wf C3) by auto.
forwards_test Rel. clear H8 H10 H11. rename F'0 into F4.
forwards: aeq_lts_2 H9. apply aeq_bind_2. intro. apply Hf. auto.
intro; rewrite Hf; fsetdec. fsetdec. destruct_hyps. inversion H8; subst.
rename Q0 into F5. clear H8.
forwards: aeq_lts_2 HltsQ2. apply aeq_bind_2. intro. apply Hg. auto.
intro; rewrite Hg; fsetdec. fsetdec. destruct_hyps. inversion H8; subst.
rename C' into C4. clear H8.
∃ F5 C4 P'3 (appr F5 C4); intuition.
rewrite Hp'3; rewrite H5; rewrite H7; reflexivity.
∃ (S x0). apply howe_comp' with R'; auto with hopi howe.
apply oe_trans with (appr F3 C3); auto. apply oe_sc0; auto.
apply oe_proc0; auto. apply Htrans with (appr F4 C3); auto.
apply Hsc0; rewrite H14; rewrite H16; reflexivity.
- clear IH. simpl in ×. forwards*: @howe'_refl F1. destruct_hyps. forwards*: H0 H1.
1-2: rewrites (>>lts_fn HltsP1); apply fn_bind; auto. destruct_hyps.
do 4 eexists; intuition (try eassumption). eexists; eauto.
- clear H0. unfold bind in HltsP1; simpl in HltsP1; foldbind in HltsP1.
inverts HltsP1; simpls.
+ forwards: lts_inp_abs H3. destruct H0 as [F2]. subst. inversion H4. subst.
clear H4. forwards*: IH Hp2q2 H3 HltsP2; auto; try fsetdec. simpl; nat_math. clear IH.
destruct H0 as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 [k'2 Hhowe]]]]]]]]].
∃ (F'2 // shiftV (bind f N Q')) C'2 (P'2// bind f N P') (Q'2//bind f N Q').
splits; eauto with hopi howe.
× unfold bind; simpl; foldbind; eapply lts_parl'; eauto.
× rewrite Hp'2. symmetry. apply sc_appr_par_shift_right; auto.
× rewrite Hq'2. symmetry. apply sc_appr_par_shift_right; auto.
× forwards*: @howe'_bind P' Q'; auto with howe. 1-2:fsetdec.
destruct_hyps. eexists; constructor; eauto.
+ forwards: lts_inp_abs H3. destruct H0 as [F2]. subst. inversion H4. subst.
clear H4. forwards*: IH Hp2q2 H3 HltsP2; auto; try fsetdec. simpl; nat_math. clear IH.
destruct H0 as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 [k'2 Hhowe]]]]]]]]].
∃ (shiftV (bind f N Q) // F'2) C'2 (bind f N P//P'2) (bind f N Q//Q'2).
splits; eauto with hopi howe.
× unfold bind; simpl; foldbind; eapply lts_parr'; eauto.
× rewrite Hp'2. symmetry. apply sc_appr_par_shift_left; auto.
× rewrite Hq'2. symmetry. apply sc_appr_par_shift_left; auto.
× forwards*: @howe'_bind P Q; auto with howe. 1-2:fsetdec.
destruct_hyps. eexists; constructor; eauto.
- clear IH. unfold bind in HltsP1; simpl in HltsP1; foldbind in HltsP1.
inverts HltsP1; simpls.
assert (∃ n1, howe' Rel (bind (liftV f) N P)(bind (liftV f) N Q) n1).
apply @howe_implies_howe'. apply @howe_bind; auto with howe. 3-4:fsetdec.
1-2: intros [|]; simpl; simpl_swap; fsetdec.
eapply howe'_implies_howe; eauto. destruct H1.
forwards*: H0 H1 Hp2q2 HltsP2.
1-2:apply fn_bind; [fsetdec| intros [|]; simpl; simpl_swap; fsetdec].
destruct H2 as [C2 [P'2 [Q'2 [Hlts [Hp'2 [Hq'2 [x3 Hhowe]]]]]]].
do 4 eexists; intuition (try eassumption).
unfold bind; simpl; foldbind. auto with hopi. eexists; eauto.
- clear H0. unfold bind in HltsP1; simpl in *; destruct atom_fresh eqn:?;
foldbind in HltsP1. simpl_swap in Hfnp1. rewrite <- swap_fs_notin in Hfnp1;
try fsetdec. inverts HltsP1. destruct A as [ | F2 | ]; inverts H3. simpl in H5.
assert (x≠a) as Hxa by fsetdec. clear H5.
assert (N [<=] add x N) by fsetdec.
forwards: aeq_lts_2 HltsP2. apply aeq_bind_2. intro. rewrite Hg. exact H0.
fsetdec. auto. auto. destruct_hyps. inversion H2; subst. clear H2.
forwards: aeq_lts_2 H6. rewrites (>>aeq_bind_3 (swap b x P)); auto.
apply fnsaxp; auto. rewrite swap_sym. symmetry. apply aeq_swap_cut_notin.
intuition. reflexivity. destruct_hyps. inversion H2; subst x0 P0; clear H2.
rename Q0 into F'2.
forwards: IH Hp2q2 H4; auto. 2:apply howe'_swap; eauto. simpl; auto.
5:intro; rewrite (Hf x0); fsetdec. 6:eauto. 1,3: apply fnsaxp; auto.
1-2:fsetdec. intro; rewrite Hg; fsetdec. clear IH.
destruct H2 as [F3 [C3 [ P'3 [R' [HltsQ1 [ HltsR [Hp'3 [Hr' [k' Hhowe]]]]]]]]].
forwards: aeq_lts_2 HltsR. apply aeq_bind_2. intro. apply Hg. auto.
intro; rewrite Hg; fsetdec. fsetdec. destruct_hyps. inversion H2; subst. clear H2.
∃ (nu x, F3) C'0 (nu x, P'3) (nu x, (appr F3 C3)).
splits; auto.
+ unfold bind; simpl in *; rewrite Heqs; foldbind. unsimpl (new x (ag_abs F3)).
eauto with hopi.
+ rewrite Hp'3. rewrite <- H5. rewrite H8. symmetry. apply sc_appr_nu_indep_left; auto.
rewrites (>>lts_fn HltsP2). rewrite fn_bind; auto.
+ rewrite H10. symmetry. apply sc_appr_nu_indep_left; auto. rewrites (>>lts_fn H7). rewrite fn_bind; auto.
+ eexists. apply howe'_nu_same. eapply howe_comp'. eauto with howe.
eapply oe_trans; auto. apply oe_sc0; eauto. apply oe_proc0; auto.
Qed.
Lemma pseudo_sim_sim : pseudo_sim.
Proof. rewrite pseudo_sim_equiv. apply pseudo_sim_sim'. Qed.
Notation lpseudo_sim := pseudo_sim_out .
Lemma pseudo_tau' {V:Set}: ∀ Rel (P Q:proc V) P' (f:V → proc0) N k,
simulation Rel → refl Rel → (Rincl sc0 Rel) → trans Rel →
mod_aeq Rel → mod_swap Rel → howe' Rel P Q k →
fn P [<=] N → fn Q [<=] N → (∀ x, fn (f x) [<=] N) →
lts (bind f N P) tau (ag_proc P') →
∃ Q' P'' Q'', lts (bind f N Q) tau (ag_proc Q') ∧ P' =sc0= P'' ∧
Q' =sc0= Q'' ∧ ∃ k', howe' Rel P'' Q'' k'.
Proof.
introv Hsim Hrefl Hincl Htrans Hmaeq Hswap Hp1q1. gen f N P'.
induction Hp1q1 using howe'_ind_size. destruct Hp1q1;
introv HP HQ Hf HltsP1; try solve [inverts HltsP1]; simpl in ×.
- assert (N [<=] union N (fn R)) by fsetdec.
forwards: aeq_lts_2 HltsP1. apply aeq_bind_2. intro; rewrite Hf; exact H1.
fsetdec. 1-2:auto. destruct_hyps. inversion H2; subst. rename Q0 into P'0. clear H2.
forwards: H Hp1q1 H3; auto. nat_math. 3:intro; rewrite Hf. 1-3: fsetdec. clear H.
destruct H2 as [R' [P'' [R'' [HltsR [Hp'p'' [Hr'r'' HhoweP1R]]]]]].
forwards*: H0 f (union N (fn R)). 3:intro; rewrite Hf. 1-3: fsetdec.
forwards_test Rel. forwards: aeq_lts_2 H4.
apply aeq_bind_2; eauto. intro; rewrite Hf. 1-2: fsetdec.
destruct_hyps. inversion H9; subst. rename Q0 into Q'1.
∃ Q'1 P'' Q'1; intuition. rewrite H5; auto.
∃ (S x0). eapply howe_comp'; eauto with hopi howe.
eapply oe_trans; auto. apply oe_sc0; eauto with sc.
eapply oe_trans; auto. apply oe_proc0; eauto with sc.
apply oe_sc0; auto with sc.
- ∃ P' P' P'; intuition.
- rewrite bind_para_simpl in HltsP1. inverts HltsP1.
+ forwards: lts_tau_proc H3; destruct H0 as [P'1]. subst. simpl in H4.
inversion H4. clear H4. forwards: H Hp1q1_1 H3; auto; try fsetdec; try nat_math.
destruct H0 as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
∃ (Q'1 // (bind f N Q')) (P''1 // (bind f N P')) (Q''1 // (bind f N Q')).
splits; auto with sc. unfold bind; simpl; foldbind. eapply lts_parl'; eauto.
destruct_hyps. forwards: @howe'_bind W Hp1q1_2; eauto with howe.
1-2:fsetdec. destruct_hyps. ∃ (S (x+x0)). constructor; auto.
+ forwards: lts_tau_proc H3; destruct H0 as [P'1]. subst. simpl in H4.
inversion H4. clear H4. forwards: H Hp1q1_2 H3; auto; try fsetdec; try nat_math.
destruct H0 as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
∃ ((bind f N Q) // Q'1) ((bind f N P) // P''1) ((bind f N Q) // Q''1).
splits; auto with sc howe hopi.
unfold bind; simpl; foldbind. eapply lts_parr'; eauto. destruct_hyps.
forwards: @howe'_bind W Hp1q1_1; eauto with howe; try fsetdec. destruct_hyps.
∃ (S (x0+x)). constructor; auto.
+ forwards: lpseudo_sim H4 H3; try eapply howe'_implies_howe; eauto; try fsetdec.
destruct H0 as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
∃ (appl C2 F2) P'2 Q'2. splits; eauto.
unfold bind; simpl; foldbind. eapply lts_taul'; eauto.
rewrite Hp'2. symmetry. apply sc_appr_appl.
rewrite Hq'2. symmetry. apply sc_appr_appl. apply howe_implies_howe'; auto.
+ forwards: lpseudo_sim H3 H4; try eapply howe'_implies_howe; eauto; try fsetdec.
destruct H0 as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
∃ (appr F2 C2) P'2 Q'2. splits; eauto with sc.
unfold bind; simpl; foldbind. eapply lts_taur'; eauto. apply howe_implies_howe'; auto.
- unfold bind in HltsP1; simpl in *; destruct atom_fresh eqn:?; foldbind in HltsP1.
inverts HltsP1. destruct A as [ P'1 | [] | [] ]; inverts H3. clear H5.
simpl_swap in HP. rewrite <- swap_fs_notin in HP; try fsetdec.
assert (swap b x P =A= swap c x (swap b c P)).
{ rewrite (swap_sym _ c x). apply aeq_swap_cut_notin. intuition. }
forwards: H H6; auto. eapply mod_aeq_left_howe'; auto. 2:eauto.
apply howe'_swap; auto. eauto. nat_math. rewrite <- H1.
1-2: apply fnsaxp; auto. intros; rewrite Hf; fsetdec.
destruct H2 as [Q' [P'' [Q'' [Hlts [Hsc1 [Hsc2 Hhowe]]]]]].
∃ (nu x, Q') (nu x, P'') (nu x, Q''). split.
unfold bind; simpl in *; rewrite Heqs; clear Heqs; foldbind.
unsimpl (new x (ag_proc Q')). constructor; auto. splits. 1-2:auto with sc.
destruct_hyps. ∃ (S x0). eauto with howe.
Qed.
Lemma conc_to_proc : ∀ L P1 P2 a,
conc_wf (conc_def L P1 P2) → a `notin` (list_to_fs L) →
∃ P, lts P (out a) (conc_def L P1 P2) ∧
(∀ (C':conc), lts P (out a) C' → (conc_def L P1 P2) = C').
Proof. induction L; intros; simpl in ×.
+ ∃ (a!(P1) P2); intuition. inversion H; auto.
+ destruct H. inversion H; subst. forwards: IHL P1 P2 a0; intuition. fsetdec.
destruct H2 as [P [HL HR]]. ∃ (pr_nu a P). split.
- asserts_rewrite (conc_def (a::L) P1 P2 = conc_new a (conc_def L P1 P2)).
{ unfold conc_new. unfold conc_convert. rewrite conc_convert_indep_wf.
case_if; fsetdec. split; auto; fsetdec. rewrite list_to_fs_2 in H4.
fsetdec. } unsimpl (new a (conc_def L P1 P2)).
constructor; auto.
- intros. inversion H2; subst. destruct A; inversion H7.
forwards: HR c; auto. destruct c; subst. inversion H3; subst.
clear H HR H3 H9 H7 H2 H10 IHL. unfold conc_new.
unfold conc_convert. rewrite conc_convert_indep_wf; auto. case_if; fsetdec.
rewrite list_to_fs_2 in H4. fsetdec.
Qed.
Lemma abs_to_proc : ∀ (F:abs) a, ∃ P, lts P (inp a) (ag_abs F) ∧
(∀ (F':abs), lts P (inp a) (ag_abs F') → F = F').
Proof. intros. ∃ (a? F); splits; auto with hopi. intros. inverts H; auto. Qed.
Lemma simulation_up_to_sc_howe : ∀ Rel, simulation Rel → refl Rel →
mod_aeq Rel → mod_swap Rel → (Rincl sc0 Rel) → trans Rel →
simulation_up_to_sc (howe Rel).
Proof.
intros. intros_all. splits; intros.
+ forwards: aeq_lts_2 H6. symmetry. apply (bind_return' (union (fn P) (fn Q))).
fsetdec. destruct_hyps. inversion H7; subst; clear H7.
forwards: @howe_implies_howe' H5. destruct H7 as [k H'PQ].
forwards: (@pseudo_tau' Empty_set) Rel H8; eauto. 3:intro; simpl. 1-3: fsetdec.
destruct_hyps. forwards: aeq_lts_2 H7. apply bind_return'. fsetdec.
destruct_hyps. inversion H13; subst; clear H13.
∃ Q1. intuition. ∃ x0; split; [| ∃ x1; split]; auto.
rewrite H10; auto. eapply howe'_implies_howe; eauto.
rewrite <- H16; symmetry; auto.
+ destruct C as [CL CP CQ]. apply (conc_convert_wf _ {{a}}) in H7.
destruct (conc_convert _ {{a}}) as [C'L C'P C'Q] eqn:?.
forwards: conc_to_proc C'L C'P C'Q a; auto.
simpl in Heqc. forwards: fn_conc_convert_0' Heqc. fsetdec.
destruct H8 as [R [Hlts Hc']].
forwards: aeq_lts_2 H6. symmetry. apply (bind_return' (union(union(fn P)(fn Q))(fn R))).
fsetdec. destruct_hyps. inversion H8; subst; clear H8.
forwards: aeq_lts_2 Hlts. symmetry. apply (bind_return' (union(union(fn P)(fn Q))(fn R))).
fsetdec. destruct_hyps. inversion H8; subst; clear H8.
forwards: @howe_refl Rel R.
forwards: lpseudo_sim H8 H5; eauto with hopi; try fsetdec.
destruct H12 as [F2 [C2 [P'2 [Q'2 [HltsQ [HltsR [Hpp'' [Hq'q'' Hhowe]]]]]]]].
forwards: aeq_lts_2 HltsQ. apply bind_return'. fsetdec.
destruct_hyps. inversion H12; subst; clear H12.
forwards: aeq_lts_2 HltsR. apply bind_return'. fsetdec.
destruct_hyps. inversion H12; subst; clear H12.
forwards: Hc' H15. inversion H12; subst; clear H17.
eexists; intuition eauto with sc. ∃ P'2; split; [|∃ Q'2; intuition].
rewrite Hpp''. rewrite <- H13. rewrite <- Heqc.
rewrite <- aeq_conc_convert. rewrite H11. reflexivity.
rewrite Hq'q''. rewrite H18. rewrite <- Heqc.
rewrite <- aeq_conc_convert. rewrite H16. reflexivity.
+ forwards: abs_to_proc F a. destruct H7 as [R [Hlts Hf']].
forwards: aeq_lts_2 H6. symmetry. apply (bind_return' (union(union(fn P)(fn Q))(fn R))).
fsetdec. destruct_hyps. inversion H7; subst; clear H7.
forwards: aeq_lts_2 Hlts. symmetry. apply (bind_return' (union(union(fn P)(fn Q))(fn R))).
fsetdec. destruct_hyps. inversion H7; subst; clear H7.
forwards: @howe_refl Rel R.
forwards: lpseudo_sim H5 H7; eauto with hopi; try fsetdec.
destruct H11 as [F2 [C2 [P'2 [Q'2 [HltsR [HltsQ [Hpp'' [Hq'q'' Hhowe]]]]]]]].
forwards: aeq_lts_2 HltsR. apply bind_return'. fsetdec.
destruct_hyps. inversion H11; subst; clear H11.
forwards: aeq_lts_2 HltsQ. apply bind_return'. fsetdec.
destruct_hyps. inversion H11; subst; clear H11.
forwards: Hf' H13; subst.
eexists; intuition eauto with sc.
∃ P'2. split. rewrite Hpp''. rewrite H10. rewrite H12. reflexivity.
∃ Q'2. intuition. rewrite Hq'q''. rewrite H15. rewrite H17. reflexivity.
Qed.
Lemma Rincl_sc0_howe : ∀ Rel,
mod_aeq Rel → Rincl sc0 Rel → Rincl sc0 (howe Rel).
Proof.
intros_all. apply howe_comp with x; auto with howe. apply oe_proc0; auto.
Qed.
Lemma bisimulation_tclos_howe : ∀ Rel, simulation Rel
→ refl Rel → mod_aeq Rel → mod_swap Rel
→ Rincl sc0 Rel → trans Rel → sym Rel
→ bisimulation (tclosure (howe Rel)).
Proof. introv Hsim Href Hmaeq Hswap Hsc0 Htrans Hsym.
apply sim_sym_imply_bisim; [|apply howe_sym; auto].
intros_all. assert (Rincl sc0 (tclosure (howe Rel))).
{ intros_all. apply tclosure_once. apply Rincl_sc0_howe; auto. }
induction H.
+ forwards*: simulation_up_to_sc_howe Rel. specialize (H1 x y H).
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 H;
forwards_test (tclosure (@howe Empty_set Rel)); destruct_comp;
repeat (eexists; intuition (try eassumption)); intuition eauto with howe.
Qed.
Theorem bisimilarity_howe : bisimilarity = howe bisimilarity.
Proof.
apply binary_ext; split.
- intros. assert (Hbisim:=H). unfold bisimilarity in H. destruct_hyps.
apply howe_comp with x; auto with bisim howe.
apply oe_proc0; auto. apply bisim_aeq.
- intros. ∃ (tclosure (@howe Empty_set bisimilarity)). split.
apply bisimulation_tclos_howe;
auto using bisim_sym, bisim_trans, bisim_refl, bisim_aeq, bisim_swap.
forwards: bisim_is_bisimulation; intuition.
intros_all. ∃ sc0. intuition. apply struct_congr_bisim.
apply tclosure_once; auto.
Qed.
Lemma pseudo_tau' {V:Set}: ∀ Rel (P Q:proc V) P' (f:V → proc0) N k,
simulation Rel → refl Rel → (Rincl sc0 Rel) → trans Rel →
mod_aeq Rel → mod_swap Rel → howe' Rel P Q k →
fn P [<=] N → fn Q [<=] N → (∀ x, fn (f x) [<=] N) →
lts (bind f N P) tau (ag_proc P') →
∃ Q' P'' Q'', lts (bind f N Q) tau (ag_proc Q') ∧ P' =sc0= P'' ∧
Q' =sc0= Q'' ∧ ∃ k', howe' Rel P'' Q'' k'.
Proof.
introv Hsim Hrefl Hincl Htrans Hmaeq Hswap Hp1q1. gen f N P'.
induction Hp1q1 using howe'_ind_size. destruct Hp1q1;
introv HP HQ Hf HltsP1; try solve [inverts HltsP1]; simpl in ×.
- assert (N [<=] union N (fn R)) by fsetdec.
forwards: aeq_lts_2 HltsP1. apply aeq_bind_2. intro; rewrite Hf; exact H1.
fsetdec. 1-2:auto. destruct_hyps. inversion H2; subst. rename Q0 into P'0. clear H2.
forwards: H Hp1q1 H3; auto. nat_math. 3:intro; rewrite Hf. 1-3: fsetdec. clear H.
destruct H2 as [R' [P'' [R'' [HltsR [Hp'p'' [Hr'r'' HhoweP1R]]]]]].
forwards*: H0 f (union N (fn R)). 3:intro; rewrite Hf. 1-3: fsetdec.
forwards_test Rel. forwards: aeq_lts_2 H4.
apply aeq_bind_2; eauto. intro; rewrite Hf. 1-2: fsetdec.
destruct_hyps. inversion H9; subst. rename Q0 into Q'1.
∃ Q'1 P'' Q'1; intuition. rewrite H5; auto.
∃ (S x0). eapply howe_comp'; eauto with hopi howe.
eapply oe_trans; auto. apply oe_sc0; eauto with sc.
eapply oe_trans; auto. apply oe_proc0; eauto with sc.
apply oe_sc0; auto with sc.
- ∃ P' P' P'; intuition.
- rewrite bind_para_simpl in HltsP1. inverts HltsP1.
+ forwards: lts_tau_proc H3; destruct H0 as [P'1]. subst. simpl in H4.
inversion H4. clear H4. forwards: H Hp1q1_1 H3; auto; try fsetdec; try nat_math.
destruct H0 as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
∃ (Q'1 // (bind f N Q')) (P''1 // (bind f N P')) (Q''1 // (bind f N Q')).
splits; auto with sc. unfold bind; simpl; foldbind. eapply lts_parl'; eauto.
destruct_hyps. forwards: @howe'_bind W Hp1q1_2; eauto with howe.
1-2:fsetdec. destruct_hyps. ∃ (S (x+x0)). constructor; auto.
+ forwards: lts_tau_proc H3; destruct H0 as [P'1]. subst. simpl in H4.
inversion H4. clear H4. forwards: H Hp1q1_2 H3; auto; try fsetdec; try nat_math.
destruct H0 as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
∃ ((bind f N Q) // Q'1) ((bind f N P) // P''1) ((bind f N Q) // Q''1).
splits; auto with sc howe hopi.
unfold bind; simpl; foldbind. eapply lts_parr'; eauto. destruct_hyps.
forwards: @howe'_bind W Hp1q1_1; eauto with howe; try fsetdec. destruct_hyps.
∃ (S (x0+x)). constructor; auto.
+ forwards: lpseudo_sim H4 H3; try eapply howe'_implies_howe; eauto; try fsetdec.
destruct H0 as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
∃ (appl C2 F2) P'2 Q'2. splits; eauto.
unfold bind; simpl; foldbind. eapply lts_taul'; eauto.
rewrite Hp'2. symmetry. apply sc_appr_appl.
rewrite Hq'2. symmetry. apply sc_appr_appl. apply howe_implies_howe'; auto.
+ forwards: lpseudo_sim H3 H4; try eapply howe'_implies_howe; eauto; try fsetdec.
destruct H0 as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
∃ (appr F2 C2) P'2 Q'2. splits; eauto with sc.
unfold bind; simpl; foldbind. eapply lts_taur'; eauto. apply howe_implies_howe'; auto.
- unfold bind in HltsP1; simpl in *; destruct atom_fresh eqn:?; foldbind in HltsP1.
inverts HltsP1. destruct A as [ P'1 | [] | [] ]; inverts H3. clear H5.
simpl_swap in HP. rewrite <- swap_fs_notin in HP; try fsetdec.
assert (swap b x P =A= swap c x (swap b c P)).
{ rewrite (swap_sym _ c x). apply aeq_swap_cut_notin. intuition. }
forwards: H H6; auto. eapply mod_aeq_left_howe'; auto. 2:eauto.
apply howe'_swap; auto. eauto. nat_math. rewrite <- H1.
1-2: apply fnsaxp; auto. intros; rewrite Hf; fsetdec.
destruct H2 as [Q' [P'' [Q'' [Hlts [Hsc1 [Hsc2 Hhowe]]]]]].
∃ (nu x, Q') (nu x, P'') (nu x, Q''). split.
unfold bind; simpl in *; rewrite Heqs; clear Heqs; foldbind.
unsimpl (new x (ag_proc Q')). constructor; auto. splits. 1-2:auto with sc.
destruct_hyps. ∃ (S x0). eauto with howe.
Qed.
Lemma conc_to_proc : ∀ L P1 P2 a,
conc_wf (conc_def L P1 P2) → a `notin` (list_to_fs L) →
∃ P, lts P (out a) (conc_def L P1 P2) ∧
(∀ (C':conc), lts P (out a) C' → (conc_def L P1 P2) = C').
Proof. induction L; intros; simpl in ×.
+ ∃ (a!(P1) P2); intuition. inversion H; auto.
+ destruct H. inversion H; subst. forwards: IHL P1 P2 a0; intuition. fsetdec.
destruct H2 as [P [HL HR]]. ∃ (pr_nu a P). split.
- asserts_rewrite (conc_def (a::L) P1 P2 = conc_new a (conc_def L P1 P2)).
{ unfold conc_new. unfold conc_convert. rewrite conc_convert_indep_wf.
case_if; fsetdec. split; auto; fsetdec. rewrite list_to_fs_2 in H4.
fsetdec. } unsimpl (new a (conc_def L P1 P2)).
constructor; auto.
- intros. inversion H2; subst. destruct A; inversion H7.
forwards: HR c; auto. destruct c; subst. inversion H3; subst.
clear H HR H3 H9 H7 H2 H10 IHL. unfold conc_new.
unfold conc_convert. rewrite conc_convert_indep_wf; auto. case_if; fsetdec.
rewrite list_to_fs_2 in H4. fsetdec.
Qed.
Lemma abs_to_proc : ∀ (F:abs) a, ∃ P, lts P (inp a) (ag_abs F) ∧
(∀ (F':abs), lts P (inp a) (ag_abs F') → F = F').
Proof. intros. ∃ (a? F); splits; auto with hopi. intros. inverts H; auto. Qed.
Lemma simulation_up_to_sc_howe : ∀ Rel, simulation Rel → refl Rel →
mod_aeq Rel → mod_swap Rel → (Rincl sc0 Rel) → trans Rel →
simulation_up_to_sc (howe Rel).
Proof.
intros. intros_all. splits; intros.
+ forwards: aeq_lts_2 H6. symmetry. apply (bind_return' (union (fn P) (fn Q))).
fsetdec. destruct_hyps. inversion H7; subst; clear H7.
forwards: @howe_implies_howe' H5. destruct H7 as [k H'PQ].
forwards: (@pseudo_tau' Empty_set) Rel H8; eauto. 3:intro; simpl. 1-3: fsetdec.
destruct_hyps. forwards: aeq_lts_2 H7. apply bind_return'. fsetdec.
destruct_hyps. inversion H13; subst; clear H13.
∃ Q1. intuition. ∃ x0; split; [| ∃ x1; split]; auto.
rewrite H10; auto. eapply howe'_implies_howe; eauto.
rewrite <- H16; symmetry; auto.
+ destruct C as [CL CP CQ]. apply (conc_convert_wf _ {{a}}) in H7.
destruct (conc_convert _ {{a}}) as [C'L C'P C'Q] eqn:?.
forwards: conc_to_proc C'L C'P C'Q a; auto.
simpl in Heqc. forwards: fn_conc_convert_0' Heqc. fsetdec.
destruct H8 as [R [Hlts Hc']].
forwards: aeq_lts_2 H6. symmetry. apply (bind_return' (union(union(fn P)(fn Q))(fn R))).
fsetdec. destruct_hyps. inversion H8; subst; clear H8.
forwards: aeq_lts_2 Hlts. symmetry. apply (bind_return' (union(union(fn P)(fn Q))(fn R))).
fsetdec. destruct_hyps. inversion H8; subst; clear H8.
forwards: @howe_refl Rel R.
forwards: lpseudo_sim H8 H5; eauto with hopi; try fsetdec.
destruct H12 as [F2 [C2 [P'2 [Q'2 [HltsQ [HltsR [Hpp'' [Hq'q'' Hhowe]]]]]]]].
forwards: aeq_lts_2 HltsQ. apply bind_return'. fsetdec.
destruct_hyps. inversion H12; subst; clear H12.
forwards: aeq_lts_2 HltsR. apply bind_return'. fsetdec.
destruct_hyps. inversion H12; subst; clear H12.
forwards: Hc' H15. inversion H12; subst; clear H17.
eexists; intuition eauto with sc. ∃ P'2; split; [|∃ Q'2; intuition].
rewrite Hpp''. rewrite <- H13. rewrite <- Heqc.
rewrite <- aeq_conc_convert. rewrite H11. reflexivity.
rewrite Hq'q''. rewrite H18. rewrite <- Heqc.
rewrite <- aeq_conc_convert. rewrite H16. reflexivity.
+ forwards: abs_to_proc F a. destruct H7 as [R [Hlts Hf']].
forwards: aeq_lts_2 H6. symmetry. apply (bind_return' (union(union(fn P)(fn Q))(fn R))).
fsetdec. destruct_hyps. inversion H7; subst; clear H7.
forwards: aeq_lts_2 Hlts. symmetry. apply (bind_return' (union(union(fn P)(fn Q))(fn R))).
fsetdec. destruct_hyps. inversion H7; subst; clear H7.
forwards: @howe_refl Rel R.
forwards: lpseudo_sim H5 H7; eauto with hopi; try fsetdec.
destruct H11 as [F2 [C2 [P'2 [Q'2 [HltsR [HltsQ [Hpp'' [Hq'q'' Hhowe]]]]]]]].
forwards: aeq_lts_2 HltsR. apply bind_return'. fsetdec.
destruct_hyps. inversion H11; subst; clear H11.
forwards: aeq_lts_2 HltsQ. apply bind_return'. fsetdec.
destruct_hyps. inversion H11; subst; clear H11.
forwards: Hf' H13; subst.
eexists; intuition eauto with sc.
∃ P'2. split. rewrite Hpp''. rewrite H10. rewrite H12. reflexivity.
∃ Q'2. intuition. rewrite Hq'q''. rewrite H15. rewrite H17. reflexivity.
Qed.
Lemma Rincl_sc0_howe : ∀ Rel,
mod_aeq Rel → Rincl sc0 Rel → Rincl sc0 (howe Rel).
Proof.
intros_all. apply howe_comp with x; auto with howe. apply oe_proc0; auto.
Qed.
Lemma bisimulation_tclos_howe : ∀ Rel, simulation Rel
→ refl Rel → mod_aeq Rel → mod_swap Rel
→ Rincl sc0 Rel → trans Rel → sym Rel
→ bisimulation (tclosure (howe Rel)).
Proof. introv Hsim Href Hmaeq Hswap Hsc0 Htrans Hsym.
apply sim_sym_imply_bisim; [|apply howe_sym; auto].
intros_all. assert (Rincl sc0 (tclosure (howe Rel))).
{ intros_all. apply tclosure_once. apply Rincl_sc0_howe; auto. }
induction H.
+ forwards*: simulation_up_to_sc_howe Rel. specialize (H1 x y H).
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 H;
forwards_test (tclosure (@howe Empty_set Rel)); destruct_comp;
repeat (eexists; intuition (try eassumption)); intuition eauto with howe.
Qed.
Theorem bisimilarity_howe : bisimilarity = howe bisimilarity.
Proof.
apply binary_ext; split.
- intros. assert (Hbisim:=H). unfold bisimilarity in H. destruct_hyps.
apply howe_comp with x; auto with bisim howe.
apply oe_proc0; auto. apply bisim_aeq.
- intros. ∃ (tclosure (@howe Empty_set bisimilarity)). split.
apply bisimulation_tclos_howe;
auto using bisim_sym, bisim_trans, bisim_refl, bisim_aeq, bisim_swap.
forwards: bisim_is_bisimulation; intuition.
intros_all. ∃ sc0. intuition. apply struct_congr_bisim.
apply tclosure_once; auto.
Qed.