Library Nom_Struct_congr
Require Export Nom_Bisimulation.
Inductive struct_congr {V : Set} : binary (proc V) :=
| sc_par_assoc : ∀ P Q R, struct_congr (P // (Q // R)) ((P // Q) // R)
| sc_par_assoc_rev : ∀ P Q R, struct_congr ((P // Q) // R) (P // (Q // R))
| sc_par_comm : ∀ P Q, struct_congr (P // Q) (Q // P)
| sc_par_nil : ∀ P, struct_congr (P // PO) P
| sc_par_nil_conv : ∀ P, struct_congr P (P // PO)
| sc_scope: ∀ a P Q, a `notin` fn Q → struct_congr (nu a, (P // Q)) ((nu a, P) // Q)
| sc_scope_rev: ∀ a P Q, a `notin` fn Q → struct_congr ((nu a, P) // Q) (nu a, (P // Q))
| sc_nu_nil : ∀ a, struct_congr (nu a, PO) PO
| sc_nu_nil_rev : ∀ a, struct_congr PO (nu a, PO)
| sc_nu_nu : ∀ a b P, struct_congr (nu a, (nu b, P)) (nu b, (nu a, P))
| sc_nil : struct_congr PO PO
| sc_var : ∀ x, struct_congr (pr_var x) (pr_var x)
| sc_par : ∀ P Q P' Q', struct_congr P Q → struct_congr P' Q'
→ struct_congr (P // P') (Q // Q')
| sc_inp : ∀ a P Q, @struct_congr (incV V) P Q → struct_congr (a? P) (a? Q)
| sc_out : ∀ a P Q P' Q', struct_congr P Q → struct_congr P' Q'
→ struct_congr (a!(P) P') (a!(Q) Q')
| sc_nu : ∀ a P Q, struct_congr P Q → struct_congr (nu a, P)(nu a, Q)
| sc_aeq : ∀ P Q, P=A=Q → struct_congr P Q
| sc_trans : ∀ P Q R, struct_congr P Q → struct_congr Q R → struct_congr P R
.
Notation "P =sc= Q" := (struct_congr P Q) (at level 70, no associativity).
Hint Constructors struct_congr:sc.
Lemma sc_refl {V : Set} : ∀ P, @struct_congr V P P.
Proof. induction P; auto with sc. Qed.
Lemma sc_symmetric {V : Set} : ∀ (P Q:proc V),
struct_congr P Q → struct_congr Q P.
Proof.
intros P Q H. induction H; eauto with sc. apply aeq_sym in H. eauto with sc.
Qed.
Lemma sc_genNu {V:Set}: ∀ L (P Q:proc V), struct_congr P Q →
struct_congr (genNu L P) (genNu L Q).
Proof.
induction L; simpl; auto with sc.
Qed.
Lemma fn_sc : ∀ V (P Q : proc V), struct_congr P Q → fn P [=] fn Q.
Proof. intros. induction H; simpl; try fsetdec. apply aeq_fn. auto.
Qed.
Lemma swap_struct_congr : ∀ V b c (P Q : proc V), struct_congr P Q →
struct_congr (swap b c P) (swap b c Q).
Proof.
intros. gen b c. induction H; simpl; intros; try solve [auto with sc];
try solve [constructor; simpl_swap];
apply sc_trans with (swap b c Q); auto with sc.
Qed.
Lemma swap_struct_congr' : ∀ V b c (P Q : proc V),
struct_congr (swap b c P) (swap b c Q) → struct_congr P Q.
Proof. intros. rewrite <- (swap_invo _ b c P). rewrite <- (swap_invo _ b c Q).
apply swap_struct_congr. auto.
Qed.
Hint Resolve sc_refl sc_aeq sc_symmetric sc_genNu:sc.
Add Parametric Relation (V:Set) : (proc V) (@struct_congr V)
reflexivity proved by (@sc_refl V)
symmetry proved by (@sc_symmetric V)
transitivity proved by (@sc_trans V)
as aeq_eq_rel.
Add Parametric Morphism (V:Set) (a:name): (pr_nu a)
with signature (@struct_congr V) ==> (@struct_congr V)
as nu_sc_morphism.
Proof. intros; constructor; auto. Qed.
Add Parametric Morphism (V:Set) L: (genNu L)
with signature (@struct_congr V) ==> (@struct_congr V)
as genNu_sc_morphism.
Proof. intros. apply sc_genNu; auto. Qed.
Add Parametric Morphism (V:Set) (a:name): (pr_inp a)
with signature (@struct_congr (incV V)) ==> (@struct_congr V)
as inp_sc_morphism.
Proof. intros; constructor; auto. Qed.
Add Parametric Morphism (V:Set) (a:name): (pr_snd a)
with signature (@struct_congr V) ==> (@struct_congr V) ==> (@struct_congr V)
as snd_sc_morphism.
Proof. intros; constructor; auto. Qed.
Add Parametric Morphism (V:Set): (@pr_par V)
with signature (@struct_congr V) ==> (@struct_congr V) ==> (@struct_congr V)
as par_sc_morphism.
Proof. intros; constructor; auto. Qed.
Add Parametric Morphism (V:Set): (fn)
with signature (@struct_congr V) ==> (Equal)
as fn_sc_morphism.
Proof. intros. apply fn_sc; auto. Qed.
Add Parametric Morphism (V:Set) b c : (swap b c)
with signature (@struct_congr V) ==> (@struct_congr V)
as swap_sc_morphism.
Proof. intros. apply swap_struct_congr; auto. Qed.
Instance subrel_aeq_sc (V:Set):
subrelation (@aeq V) (@struct_congr V).
Proof. intros_all. apply sc_aeq; auto. Qed.
Lemma sc_mapV: ∀ (V W:Set) P Q (f:V → W), @struct_congr V P Q
→ @struct_congr W (mapV f P) (mapV f Q).
Proof.
intros. gen W. induction H; simpl; auto with sc.
- intros. apply sc_scope. simpl_swap.
- intros. apply sc_scope_rev. simpl_swap.
- intros. constructor. apply aeq_mapV. auto.
- eauto with sc.
Qed.
Lemma sc_liftV: ∀ (V W:Set) (f:V → proc W) (g:V → proc W),
(∀ x, @struct_congr W (f x) (g x)) →
(∀ x, @struct_congr (incV W) (liftV f x) (liftV g x)).
Proof.
intros. destruct x; simpl; auto with sc.
apply sc_mapV. auto with sc.
Qed.
Lemma sc_bind_1: ∀ (V W:Set) (P : proc V) N (f:V → proc W) (g:V → proc W),
(∀ x, @struct_congr W (f x) (g x)) →
@struct_congr W (bind f N P) (bind g N P).
Proof.
intros V'' W P''. gen W. apply size_induction with (x:=P'').
intros V P IH; intros. destruct P; unfold bind; simpl in *; foldbind;
try solve [apply H]; try solve [constructor; try apply IH; try nat_math; auto;
try fsetdec; try intro; auto].
- constructor. apply IH. nat_math. intro. apply× sc_liftV. intro; auto.
- destruct atom_fresh. apply sc_nu. foldbind. apply IH.
+ rewrite swap_size_eq. nat_math.
+ intro; auto.
Qed.
Hint Resolve sc_bind_1 sc_liftV sc_mapV:sc.
Lemma bind_para_simpl : ∀ V W (P Q : proc V) (f : V → proc W) N,
bind f N (P//Q) = bind f N P // bind f N Q.
Proof. intros. unfold bind. simpl. foldbind. auto. Qed.
Lemma sc_bind_2: ∀ (V W:Set) (P Q : proc V) N (f:V → proc W),
@struct_congr V P Q → fn P [<=] N → (∀ x, fn (f x) [<=] N) →
@struct_congr W (bind f N P) (bind f N Q).
Proof. intros. gen W N. induction H; simpl; intros;
repeat rewrite bind_para_simpl; try solve [auto with sc]; unfold bind;
simpl in *; repeat destruct atom_fresh; foldbind; try solve [auto with sc].
- assert (fn Q [<=] N) by fsetdec.
assert (swap a x Q =A= Q). { destruct (x==a); subst.
simpl_swap. apply aeq_swap_indep; auto. } rewrite sc_scope_rev.
constructor. apply sc_par; auto with sc. apply sc_aeq.
rewrites (>>aeq_bind_3 (swap a x Q) Q); auto. fsetdec.
apply aeq_bind_2; try fsetdec; intro; rewrite H1; fsetdec.
rewrite fn_bind; try rewrite H3; auto.
- assert (fn Q [<=] N) by fsetdec.
assert (swap a x Q =A= Q). { destruct (x==a); subst.
simpl_swap. apply aeq_swap_indep; auto. } rewrite sc_scope_rev.
constructor. apply sc_par; auto with sc. apply sc_aeq.
rewrites (>>aeq_bind_3 (swap a x Q) Q); auto. fsetdec.
apply aeq_bind_2; try fsetdec; intro; rewrite H1; fsetdec.
rewrite fn_bind; try rewrite H3; auto.
- destruct (a==b); subst; try reflexivity. assert (x≠x0) by fsetdec.
apply sc_trans with (swap x x0 (nu x, ( nu x0, ( bind f (add x0 (add x N))
(swap (swap_aux a x b) x0 (swap a x P)))))). apply sc_aeq. symmetry.
apply aeq_swap_indep; simpl; fsetdec.
simpl. simpl_swap. rewrite sc_nu_nu. constructor. constructor.
assert (fn (swap (swap_aux a x b) x0 (swap a x P)) [<=] add x0 (add x N)).
{ clears W. simpl_swap_aux; intro; intro; simpl_swap in H1;
simpl_swap_aux×. 6:destruct (a0==x0); subst.
7:enough (a0 `in` N) by fsetdec; clears x x0.
all:fsetdec. }
rewrite swap_bind_f_indep; auto; try solve [intros; rewrite H1; fsetdec].
assert ((swap_fs x x0 (add x0 (add x N))) [=] (add x0 (add x N))).
{ symmetry; apply swap_fs_in; fsetdec. } simpl_swap in H2.
rewrites (>>aeq_bind_2 (swap_fs x x0 (add x0 (add x N))) (add x0 (add x N)));
try solve [intros; rewrite H1; try rewrite H3; fsetdec].
rewrite <- H3. simpl_swap. simpl_swap.
apply sc_aeq. symmetry. apply aeq_bind_3. rewrite <- H3. simpl_swap.
simpl_swap_aux*; simpl_swap.
+ rewrite swap_sym. rewrite shuffle_swap; auto. rewrite swap_sym .
rewrite (swap_sym _ b x0). reflexivity.
+ rewrite (swap_sym _ a x0 (swap a x P)). rewrite (shuffle_swap _ x0 a x); auto.
rewrite (swap_sym _ x x0). rewrite swap_sym. simpl_swap.
+ destruct (a==x0); destruct (b==x0); subst; simpl_swap. fsetdec.
× rewrite (swap_sym _ b x0). rewrite shuffle_swap; auto.
rewrite (swap_sym _ x x0). simpl_swap. rewrite swap_sym. reflexivity.
× rewrite (swap_equivariance _ x x0); simpl_swap_aux.
rewrite (swap_sym _ x x0). reflexivity.
× rewrite swap_indep; auto. rewrite (swap_equivariance _ x x0);
simpl_swap_aux. rewrite (swap_equivariance _ x x0); simpl_swap_aux.
rewrite (aeq_swap_indep _ x x0). reflexivity. auto.
fsetdec. fsetdec.
- constructor.
apply IHstruct_congr1 ; auto; fsetdec.
apply IHstruct_congr2 ; auto; fsetdec.
- constructor. apply IHstruct_congr; auto.
fsetdec. intros [|x]; simpl; simpl_swap; fsetdec.
- unfold bind. simpl. foldbind. constructor. apply IHstruct_congr1; auto.
fsetdec. apply IHstruct_congr2; auto. fsetdec.
- constructor. apply (swap_struct_congr' _ a x). rewrite swap_bind.
2:apply fnsaxp; auto. 2:intro; rewrite H1; fsetdec. simpl_swap.
rewrite IHstruct_congr. 2:forwards: fnsaxp H0 n; simpl_swap in H2; simpl_swap.
2:intro; simpl_swap; rewrite H1; fsetdec.
rewrite swap_bind. simpl_swap. apply fnsaxp; auto.
rewrites <- (>>fn_sc H). auto. intro; rewrite H1; fsetdec.
- constructor. rewrite H in H0. apply aeq_bind_3; auto.
- apply sc_trans with (bind f N Q). eauto with sc. apply IHstruct_congr2.
rewrite <- H. auto. auto.
Qed.
Lemma sc_bind: ∀ (V W:Set) (P Q : proc V) N (f:V → proc W) (g:V → proc W),
@struct_congr V P Q → fn P [<=] N → (∀ x, fn (f x) [<=] N) →
(∀ x, @struct_congr W (f x) (g x)) →
@struct_congr W (bind f N P) (bind g N Q).
Proof. intros. apply sc_trans with (bind f N Q).
apply sc_bind_2; auto. apply sc_bind_1; auto.
Qed.
Hint Resolve sc_bind:sc.
Lemma sc_nu_genNu {V:Set}: ∀ L a (P Q:proc V),
struct_congr (genNu L (nu a, P)) (nu a, (genNu L P)).
Proof. intro L; gen V. induction L; intros; simpl; try reflexivity.
rewrite IHL; auto. constructor.
Qed.
Lemma sc_scope_genNu {V:Set}: ∀ L (P Q:proc V),
inter (list_to_fs L) (fn Q) [=] empty →
struct_congr (genNu L (P//Q)) (genNu L P//Q).
Proof. induction L; intros; simpls; try reflexivity.
rewrite IHL. constructor. all:fsetdec. Qed.
Lemma sc_appr_appl : ∀ F C, struct_congr (appr F C) (appl C F).
Proof. intros. unfold appr. unfold appl. destruct conc_convert.
apply sc_genNu. auto with sc. Qed.
Lemma sc_appr_nu_indep_left : ∀ x P (C:conc), x `notin` fn_agent C → conc_wf C →
appr (nu x, P) C =sc= nu x, (appr P C).
Proof. intros. remember (conc_convert C (add x (fn P))) as C'.
assert (C =Ac= C'). { rewrite HeqC'. apply aeq_conc_convert. } rewrite H1.
destruct C as [CL CP CQ]; destruct C' as [C'L C'P C'Q].
symmetry in HeqC'. simpl in HeqC'. forwards: fn_conc_convert_0' HeqC'.
unfold appr. simpl. repeat (rewrite conc_convert_indep_wf; auto; try fsetdec).
simpl in H. rewrite <- sc_nu_genNu; auto. apply sc_genNu. rewrite sc_scope.
constructor. rewrite subst_nu_indep. 1,3:reflexivity.
forwards: fn_conc_convert_1 HeqC'. fsetdec.
forwards: fn_conc_convert_2 HeqC'. fsetdec.
Qed.
Lemma sc_appr_nu_indep_right : ∀ x (F:abs) C, x `notin` fn F → conc_wf C →
nu x, (appr F C) =sc= appr F (conc_new x C).
Proof. intros. remember (conc_convert C (add x (fn F))) as C'.
assert (C =Ac= C'). { rewrite HeqC'. apply aeq_conc_convert. } rewrite H1.
destruct C' as [L' P' Q']. destruct C as [L P Q]. unfold conc_new. simpl.
assert (conc_wf (conc_def L' P' Q')). { rewrite HeqC'; auto. }
assert (inter (list_to_fs L') (add x (fn F)) [=] empty).
{ eapply fn_conc_convert_0'. symmetry; eauto. }
rewrite conc_convert_indep_wf; auto; try fsetdec. case_if;
unfold appr; simpl; repeat (rewrite conc_convert_indep_wf; auto; try fsetdec).
- case_if; try fsetdec. simpl. reflexivity.
- rewrite <- sc_nu_genNu; auto. apply sc_genNu. rewrite sc_par_comm.
rewrite (sc_par_comm _ (nu x, Q')). constructor. rewrite fn_subst. fsetdec.
Qed.
Lemma sc_appr_par_shift_right : ∀ P Q (C:conc), conc_wf C →
appr (P// shiftV Q) C =sc= appr P C // Q.
Proof. intros. remember (conc_convert C (union (fn (shiftV Q)) (fn P))) as C'.
assert (C =Ac= C'). { rewrite HeqC'. apply aeq_conc_convert. } rewrite H0.
destruct C as [CL CP CQ]; destruct C' as [C'L C'P C'Q].
symmetry in HeqC'. simpl in HeqC'. forwards: fn_conc_convert_0' HeqC'.
unfold appr. simpl. repeat (rewrite conc_convert_indep_wf; auto; try fsetdec).
rewrite subst_par. rewrite subst_shift. rewrite <- sc_scope_genNu.
apply sc_genNu. eauto with sc. simpl_swap in H1. fsetdec.
Qed.
Lemma sc_appr_par_shift_left : ∀ P Q (C:conc), conc_wf C →
appr (shiftV Q // P) C =sc= Q // appr P C.
Proof. intros. remember (conc_convert C (union (fn (shiftV Q)) (fn P))) as C'.
assert (C =Ac= C'). { rewrite HeqC'. apply aeq_conc_convert. } rewrite H0.
destruct C as [CL CP CQ]; destruct C' as [C'L C'P C'Q].
symmetry in HeqC'. simpl in HeqC'. forwards: fn_conc_convert_0' HeqC'.
unfold appr. simpl. repeat (rewrite conc_convert_indep_wf; auto; try fsetdec).
rewrite subst_par. rewrite (sc_par_comm Q). rewrite subst_shift.
rewrite <- sc_scope_genNu. apply sc_genNu. eauto with sc.
simpl_swap in H1. fsetdec.
Qed.
Lemma sc_appr_conc_parl : ∀ F P (C:conc), conc_wf C →
appr F C // P =sc= appr F (conc_parl C P).
Proof. intros. remember (conc_convert C (union (fn P) (fn F))) as CR.
assert (C =Ac= CR). { rewrite HeqCR. apply aeq_conc_convert. } rewrite H0.
assert (conc_wf CR). { rewrite HeqCR. auto. }
destruct CR as [CRL CRP CRQ]; destruct C as [CL CP CR].
simpls. symmetry in HeqCR. forwards: fn_conc_convert_0' HeqCR.
unfold conc_parl. simpl. rewrite conc_convert_indep_wf; [ | auto| fsetdec].
unfold appr. simpl. repeat (rewrite conc_convert_indep_wf; [ | auto| fsetdec]).
rewrite <- sc_scope_genNu. 2:fsetdec. apply sc_genNu. auto with sc.
Qed.
Lemma sc_appr_conc_parr : ∀ F P (C:conc), conc_wf C →
P // appr F C =sc= appr F (conc_parr P C).
Proof. intros. remember (conc_convert C (union (fn P) (fn F))) as CR.
assert (C =Ac= CR). { rewrite HeqCR. apply aeq_conc_convert. } rewrite H0.
assert (conc_wf CR). { rewrite HeqCR. auto. }
destruct CR as [CRL CRP CRQ]; destruct C as [CL CP CR].
simpls. symmetry in HeqCR. forwards: fn_conc_convert_0' HeqCR.
unfold conc_parr. simpl. rewrite conc_convert_indep_wf; [ | auto| fsetdec].
unfold appr. simpl. repeat (rewrite conc_convert_indep_wf; [ | auto| fsetdec]).
rewrite sc_par_comm. rewrite <- sc_scope_genNu. apply sc_genNu. eauto with sc. fsetdec.
Qed.
Definition sc0 := (@struct_congr Empty_set).
Notation "P =sc0= Q" := (sc0 P Q) (at level 70, no associativity).
Hint Unfold sc0:sc.
Lemma sc0_trans : trans sc0.
Proof. intros_all. rewrite H. auto. Qed.
Lemma sc0_sym : sym sc0.
Proof. intros_all. auto with sc. Qed.
Lemma sc0_refl : refl sc0.
Proof. intros_all. auto with sc. Qed.
Hint Resolve sc0_trans sc0_sym:sc.
Lemma struct_congr_sim' {V : Set} : ∀ P Q f, @struct_congr V P Q →
∀ l A, lts (mapV f P) l A →
∃ A', lts (mapV f Q) l A' ∧ sim_test struct_congr A A'.
Proof. intros P Q f Hsc. induction Hsc; intros.
- simpls; inversion H; subst.
+ ∃ (parl (parl A0 (mapV f Q)) (mapV f R)).
split. constructor. constructor. auto. destruct_agent_sim A0.
constructor. unsimpl (shiftV (mapV f Q // mapV f R)).
repeat rewrite sc_appr_par_shift_right; auto. constructor.
repeat rewrite <- sc_appr_conc_parl; auto. constructor.
+ inversion H4; subst.
× eexists. split. constructor. constructor 4. eauto.
destruct_agent_sim A.
constructor.
rewrite sc_appr_par_shift_right; auto. repeat rewrite sc_appr_par_shift_left; auto.
rewrite sc_appr_par_shift_right; auto. constructor.
rewrite <- sc_appr_conc_parr; auto.
repeat rewrite <- sc_appr_conc_parl; auto.
repeat rewrite <- sc_appr_conc_parr; auto. constructor.
× eexists. split. constructor 4. eauto. destruct_agent_sim A.
constructor. unsimpl (shiftV (mapV f P // mapV f Q)).
repeat rewrite sc_appr_par_shift_left; auto. constructor.
repeat rewrite <- sc_appr_conc_parr; auto. constructor.
× eexists. split. constructor 6 with a.
eapply lts_parr'; eauto with sc. reflexivity. eauto.
simpl. constructor. repeat rewrite <- sc_appr_appl. apply sc_appr_conc_parr; auto.
× eexists. split. constructor 7 with a.
eapply lts_parr'; eauto with sc. reflexivity. eauto.
simpl. constructor. symmetry. apply sc_appr_par_shift_left; auto.
+ inversion H5; subst; destructA A; inversion H6; subst.
× eexists. split. constructor. constructor 6 with a; eauto.
simpl. constructor. repeat rewrite <- sc_appr_appl. apply sc_appr_par_shift_right; auto.
× eexists. split. constructor 6 with a. eapply lts_parl'; eauto.
reflexivity. eauto. constructor. repeat rewrite <- sc_appr_appl.
rewrite sc_appr_par_shift_left; auto. rewrite <- sc_appr_conc_parl; auto.
constructor.
+ inversion H5; subst; destructA A; inversion H6; subst.
× eexists. split. constructor. constructor 7 with a; eauto.
simpl. constructor. symmetry. apply sc_appr_conc_parl; auto.
× eexists. split. constructor 7 with a. eapply lts_parl'; eauto.
reflexivity. eauto. constructor; auto. rewrite <- sc_appr_conc_parr; auto.
rewrite sc_appr_par_shift_right; auto. constructor.
- simpls; inversion H; subst.
+ inversion H4; subst.
× eexists. split. constructor. eauto. destruct_agent_sim A.
constructor. unsimpl (shiftV (mapV f Q // mapV f R)).
repeat rewrite sc_appr_par_shift_right; auto. constructor.
repeat rewrite <- sc_appr_conc_parl; auto. constructor.
× eexists. split. constructor 4. constructor. eauto.
destruct_agent_sim A. constructor.
rewrite sc_appr_par_shift_right; auto. repeat rewrite sc_appr_par_shift_left; auto.
rewrite sc_appr_par_shift_right; auto. constructor.
rewrite <- sc_appr_conc_parr; auto.
repeat rewrite <- sc_appr_conc_parl; auto.
repeat rewrite <- sc_appr_conc_parr; auto. constructor.
× eexists. split. constructor 6 with a. eauto.
eapply lts_parl'; eauto with sc. reflexivity.
simpl. constructor. repeat rewrite <- sc_appr_appl.
symmetry. apply sc_appr_par_shift_right; auto.
× eexists. split. constructor 7 with a. eauto.
eapply lts_parl'; eauto with sc. reflexivity. simpl. constructor.
apply sc_appr_conc_parl; auto.
+ eexists. split. constructor 4. constructor 4. eauto.
destruct_agent_sim A0. constructor.
unsimpl (shiftV (mapV f P // mapV f Q)).
repeat rewrite sc_appr_par_shift_left; auto. constructor.
repeat rewrite <- sc_appr_conc_parr; auto. constructor.
+ inversion H2; subst; destructA A; inversion H6; subst.
× eexists. split. constructor 6 with a; eauto. eapply lts_parr'; eauto.
reflexivity. constructor. repeat rewrite <- sc_appr_appl.
rewrite sc_appr_par_shift_left; auto. rewrite <- sc_appr_conc_parl; auto. constructor.
× eexists. split. constructor 4. constructor 6 with a; eauto.
constructor. repeat rewrite <- sc_appr_appl.
symmetry. apply sc_appr_conc_parr; auto.
+ inversion H2; subst; destructA A; inversion H6; subst.
× eexists. split. constructor 7 with a; eauto. eapply lts_parr'; eauto.
reflexivity. constructor. rewrite <- sc_appr_conc_parr; auto.
rewrite sc_appr_par_shift_right; auto. constructor.
× eexists. split. constructor 4. constructor 7 with a; eauto.
simpl. constructor. apply sc_appr_par_shift_left; auto.
- simpls. inversion H; subst.
+ ∃ (parr (mapV f Q) A0). split. auto with hopi.
destruct_agent_sim A0.
× eauto with sc.
× rewrite sc_appr_par_shift_right; auto. rewrite sc_appr_par_shift_left; auto with sc.
× rewrite <- sc_appr_conc_parl; auto. rewrite <- sc_appr_conc_parr; auto with sc.
+ ∃ (parl A0 (mapV f P)). split. auto with hopi.
destruct_agent_sim A0.
× eauto with sc.
× rewrite sc_appr_par_shift_right; auto. rewrite sc_appr_par_shift_left; auto with sc.
× rewrite <- sc_appr_conc_parl; auto. rewrite <- sc_appr_conc_parr; auto with sc.
+ ∃ (ag_proc (appr F C)). split. constructor 7 with a; auto.
constructor. symmetry; apply sc_appr_appl.
+ ∃ (ag_proc (appl C F)). split. constructor 6 with a; auto.
constructor. apply sc_appr_appl.
- inversion H; subst; try solve [inversion H5];
try solve [inversion H4]. eexists; intuition eauto. destruct_agent_sim A0.
+ eauto with sc.
+ asserts_rewrite (PO = (mapV (@VS Empty_set)) PO).
{ simpl. auto. } rewrite sc_appr_par_shift_right; auto with sc.
+ rewrite <- sc_appr_conc_parl; auto with sc.
- eexists. split. simpl. eauto with hopi.
destruct_agent_sim A.
+ eauto with sc.
+ asserts_rewrite (PO = (mapV (@VS Empty_set)) PO).
{ simpl. auto. } rewrite sc_appr_par_shift_right; auto with sc.
+ rewrite <- sc_appr_conc_parl; auto with sc.
- simpls. inversion H0; subst.
inversion H6; subst.
+ ∃ (parl (new a A) (mapV f Q)). split. eauto with hopi.
destruct_agent_sim A.
× constructor. simpl_swap.
× pick fresh x. assert (x≠a) by fsetdec.
repeat rewrite (aeq_nu_diff a x); auto.
3,5:rewrite swap_invo; reflexivity. 2-3:simpl; simpl_swap.
rewrite sc_appr_par_shift_right; auto.
repeat (rewrite sc_appr_nu_indep_left; auto; simpl; try fsetdec).
rewrite swap_shiftV. rewrite sc_appr_par_shift_right; auto.
rewrites (>>aeq_swap_indep (mapV f Q)); simpl_swap.
constructor. simpl_swap.
× pick fresh x. assert (x≠a) by fsetdec.
repeat rewrite (aeq_conc_new_2 _ a x); simpl; auto.
2: unfold conc_parl; destruct conc_convert eqn:?; simpls;
forwards: fn_conc_convert_1 Heqc; forwards: fn_conc_convert_2 Heqc;
simpl_swap; fsetdec.
rewrite <- sc_appr_conc_parl; auto.
repeat (rewrite <- sc_appr_nu_indep_right; [ | simpl; fsetdec | ]); auto.
rewrite swap_conc_parl. rewrite <- sc_appr_conc_parl; auto.
rewrites (>>aeq_swap_indep (mapV f Q)); simpl_swap.
constructor. simpl_swap.
+ ∃ (parr (nu a, (mapV f P)) A). split. eauto with hopi.
destruct_agent_sim A; try (assert (a `notin` fn p) by
(rewrites (>>lts_fn H7); simpl_swap)).
× constructor; auto.
× pick fresh x. assert (x≠a) by fsetdec. repeat rewrite (aeq_nu_diff a x).
4,7:rewrite swap_invo; reflexivity. 2,4:auto. 2,3:simpl; simpl_swap.
rewrite sc_appr_nu_indep_left; simpl; auto.
rewrite swap_shiftV. unsimpl (shiftV (nu x, (swap a x (mapV f P)))).
repeat rewrite sc_appr_par_shift_left; auto. rewrites (>>aeq_swap_indep p); auto.
constructor. rewrite fn_appr. simpl. fsetdec.
× pick fresh x. assert (x≠a) by fsetdec. rewrite (aeq_nu_diff a x).
4:rewrite swap_invo; reflexivity. 2:auto. 2:simpl_swap.
repeat rewrite (aeq_conc_new_2 _ a x); simpl; auto.
2: unfold conc_parr; destruct conc_convert eqn:?; simpls;
forwards: fn_conc_convert_1 Heqc; forwards: fn_conc_convert_2 Heqc;
simpl_swap; fsetdec.
rewrite <- sc_appr_conc_parr; auto. rewrites <- (>>sc_appr_nu_indep_right); auto.
rewrite swap_conc_parr. rewrite aeq_conc_swap_indep; auto. 2:simpl; fsetdec.
2:rewrites (>>lts_fn H7); simpl_swap.
rewrite <- sc_appr_conc_parr; auto.
constructor. rewrite fn_appr; simpl; fsetdec.
+ assert (a≠a0).
{ forwards: notin_fn_notin_fnlab H8. simpl_swap. simpls. fsetdec. }
∃ (ag_proc (appl (conc_new a C) F)). split.
constructor 6 with a0; try unsimpl (new a C); eauto with hopi.
simpl; constructor. repeat rewrite <- sc_appr_appl. apply sc_appr_nu_indep_right; auto.
rewrites (>>lts_fn H8). simpl_swap.
+ assert (a≠a0).
{ forwards: notin_fn_notin_fnlab H8. simpl_swap. simpls. fsetdec. }
∃ (ag_proc (appr (nu a, F) C)). split.
constructor 7 with a0; try unsimpl (new a (ag_abs F)); eauto with hopi.
simpl; constructor. symmetry. apply sc_appr_nu_indep_left; auto.
rewrites (>>lts_fn H8). simpl_swap.
- simpls. inversion H0; subst.
+ inversion H5; subst. ∃ (new a (parl A (mapV f Q))).
split. eauto with hopi.
destruct_agent_sim A.
× constructor. simpl_swap.
× pick fresh x. assert (x≠a) by fsetdec. symmetry.
repeat rewrite (aeq_nu_diff a x).
4,7:rewrite swap_invo; reflexivity. 2,4:auto. 2,3:simpl; simpl_swap.
rewrite sc_appr_par_shift_right; auto.
repeat (rewrite sc_appr_nu_indep_left; auto; simpl; try fsetdec).
rewrite swap_shiftV. rewrite sc_appr_par_shift_right; auto.
rewrites (>>aeq_swap_indep (mapV f Q)); simpl_swap.
constructor. simpl_swap.
× pick fresh x. assert (x≠a) by fsetdec. symmetry.
repeat rewrite (aeq_conc_new_2 _ a x); simpl; auto.
2: unfold conc_parl; destruct conc_convert eqn:?; simpls;
forwards: fn_conc_convert_1 Heqc; forwards: fn_conc_convert_2 Heqc;
simpl_swap; fsetdec.
rewrite <- sc_appr_conc_parl; auto.
repeat (rewrite <- sc_appr_nu_indep_right; [ | simpl; fsetdec | ]); auto.
rewrite swap_conc_parl. rewrite <- sc_appr_conc_parl; auto.
rewrites (>>aeq_swap_indep (mapV f Q)); simpl_swap.
constructor. simpl_swap.
+ ∃ (new a (parr (mapV f P) A0)). split. constructor.
eapply notin_fn_notin_fnlab; eauto. simpl_swap.
eauto with hopi. destruct_agent_sim A0; try (assert (a `notin` fn p) by
(rewrites (>>lts_fn H5); simpl_swap)).
× constructor; auto.
× pick fresh x. assert (x≠a) by fsetdec. symmetry.
repeat rewrite (aeq_nu_diff a x).
4,7:rewrite swap_invo; reflexivity. 2,4:auto. 2,3:simpl; simpl_swap.
rewrite sc_appr_nu_indep_left; simpl; auto.
rewrite swap_shiftV. unsimpl (shiftV (nu x, (swap a x (mapV f P)))).
repeat rewrite sc_appr_par_shift_left; auto. rewrites (>>aeq_swap_indep p); auto.
constructor. rewrite fn_appr. simpl. fsetdec.
× pick fresh x. assert (x≠a) by fsetdec. symmetry. rewrite (aeq_nu_diff a x).
4:rewrite swap_invo; reflexivity. 2:auto. 2:simpl_swap.
repeat rewrite (aeq_conc_new_2 _ a x); simpl; auto.
2: unfold conc_parr; destruct conc_convert eqn:?; simpls;
forwards: fn_conc_convert_1 Heqc; forwards: fn_conc_convert_2 Heqc;
simpl_swap; fsetdec.
rewrite <- sc_appr_conc_parr; auto. rewrites <- (>>sc_appr_nu_indep_right); auto.
rewrite swap_conc_parr. rewrite aeq_conc_swap_indep; auto. 2:simpl; fsetdec.
2:rewrites (>>lts_fn H5); simpl_swap.
rewrite <- sc_appr_conc_parr; auto.
constructor. rewrite fn_appr; simpl; fsetdec.
+ assert (a≠a0).
{ forwards: notin_fn_notin_fnlab H6. simpl_swap. simpls. fsetdec. }
inversion H3; subst. destruct A; inversion H5; clear H5.
∃ (new a (ag_proc (appl c F))). split. constructor. fsetdec.
constructor 6 with a0; eauto with hopi.
simpl; constructor. repeat rewrite <- sc_appr_appl. symmetry.
apply sc_appr_nu_indep_right; auto. rewrites (>>lts_fn H6). simpl_swap.
+ assert (a≠a0).
{ forwards: notin_fn_notin_fnlab H6. simpl_swap. simpls. fsetdec. }
inversion H3; subst. destruct A as [ | | ]; inversion H5; clear H5.
eexists. split. constructor. fsetdec. constructor 7 with a0; eauto with sc.
simpl; constructor; auto. apply sc_appr_nu_indep_left; auto.
rewrites (>>lts_fn H6). simpl_swap.
- inversion H; try solve [inversion H5]; try solve [inversion H6].
- inversion H.
- inversion H; subst. inversion H5; subst; simpl.
∃ (new b (new a A)). split; intuition eauto with hopi.
destruct (a==b);subst. destruct_agent_sim A; reflexivity. destruct_agent_sim A.
+ constructor.
+ clears V l. pick fresh x. assert (a≠x) by fsetdec; assert (b≠x) by fsetdec.
pick fresh y. assert (a≠y) by fsetdec; assert (b≠y) by fsetdec;
assert (x≠y) by fsetdec. repeat rewrite (aeq_nu_diff a x).
4,7:rewrite swap_invo; reflexivity. 2,4:auto. 2,3:simpl; simpl_swap.
repeat rewrite (aeq_nu_diff b y). 4,7:rewrite swap_invo; reflexivity.
2,4:auto. 2,3:simpl; simpl_swap; simpl_swap_aux.
repeat (rewrite sc_appr_nu_indep_left; simpl; auto); simpl_swap_aux.
rewrite swap_indep; auto. constructor.
+ forwards: lts_conc_wf H7. clears V l. pick fresh x. assert (a≠x) by fsetdec;
assert (b≠x) by fsetdec. pick fresh y. assert (a≠y) by fsetdec;
assert (b≠y) by fsetdec; assert (x≠y) by fsetdec.
repeat rewrite (aeq_conc_new_2 _ a x); auto.
2-3: try rewrite fn_conc_new; simpl; fsetdec.
repeat rewrite (aeq_conc_new_2 _ b y); auto.
2-3: try rewrite fn_conc_new; simpl_swap; simpl_swap_aux; fsetdec.
repeat rewrite swap_conc_new; simpl_swap_aux. repeat rewrite <-
sc_appr_nu_indep_right; auto. rewrite swap_list_indep; auto.
repeat rewrite (swap_indep _ b); auto. constructor.
- inversion H.
- inversion H.
- simpls; inversion H; subst.
+ forwards: IHHsc1 H4. destruct_hyps.
eexists. splits; eauto with hopi. destructA A0; destructA x;
inversion H1; subst; simpl; constructor; intros_all.
× apply sc_par; eauto with sc.
× repeat rewrite sc_appr_par_shift_right; auto. apply sc_par; eauto with sc.
× repeat rewrite <- sc_appr_conc_parl; auto. apply sc_par; eauto with sc.
+ forwards: IHHsc2 H4. destruct_hyps.
eexists. splits; eauto with hopi. destructA A0; destructA x;
inversion H1; subst; simpl; constructor; intros_all.
× apply sc_par; eauto with sc.
× repeat rewrite sc_appr_par_shift_left; auto. apply sc_par; eauto with sc.
× repeat rewrite <- sc_appr_conc_parr; auto. apply sc_par; eauto with sc.
+ forwards: IHHsc1 H2. forwards: IHHsc2 H5. destruct_hyps.
inversion H3; inversion H4; subst.
eexists. split; eauto with hopi. simpl; constructor.
repeat rewrite <- sc_appr_appl. apply transitivity with (appr F' C); auto.
+ forwards: IHHsc1 H2. forwards: IHHsc2 H5. destruct_hyps.
inversion H3; inversion H4; subst.
eexists. split; eauto with hopi. simpl; constructor.
apply transitivity with (appr F' C); auto.
- simpls; inversion H; subst.
eexists; splits; eauto with hopi. constructor. intros.
remember (conc_convert C (union (fn (mapV (incV_map f) P)) (fn (mapV (incV_map f) Q)))) as C'.
asserts_rewrite (C =Ac= C'). { subst. apply aeq_conc_convert. }
assert (conc_wf C'). { subst; auto. }
unfold appr. destruct C' as [L' P' Q']; destruct C as [CL CP CQ]. simpls.
symmetry in HeqC'. forwards: fn_conc_convert_0' HeqC'.
repeat (rewrite conc_convert_indep_wf; [ | auto | fsetdec]).
apply sc_genNu. constructor; try reflexivity. unfold subst.
rewrites (>>aeq_bind_2 (union (union (fn (mapV (incV_map f) P)) (fn P'))
(fn (mapV (incV_map f) Q)))). 2,4:fsetdec. 1-2: intros [|x]; simpl; fsetdec.
rewrites (>>aeq_bind_2 (union (fn (mapV (incV_map f) Q)) (fn P'))
(union (union (fn (mapV (incV_map f) P)) (fn P')) (fn (mapV (incV_map f) Q)))).
2,4:fsetdec. 1-2: intros [|x]; simpl; fsetdec.
apply sc_bind. auto with sc. fsetdec.
intros [|x]; simpl; fsetdec. intro; reflexivity.
- simpls; inversion H; subst.
eexists; splits; eauto with hopi. constructor. intros F.
unfold appr. simpl. apply sc_par; auto with sc. unfold subst.
rewrites (>>aeq_bind_2 (union (union (fn F) (fn (mapV f P))) (fn (mapV f Q)))).
2,4:fsetdec. 1-2: intros [|x]; simpl; fsetdec.
rewrites (>>aeq_bind_2 (union (fn F) (fn (mapV f Q)))
(union (union (fn F) (fn (mapV f P))) (fn (mapV f Q)))).
2,4:fsetdec. 1-2: intros [|x]; simpl; fsetdec.
apply sc_bind. reflexivity. fsetdec. intros [|x]; simpl; fsetdec.
intros [|x]; simpl; auto with sc.
- inversion H; subst. forwards: IHHsc H5. destruct_hyps.
eexists; intuition (simpl; eauto with hopi).
destructA A0; destructA x; inversion H1; subst; constructor; try intros.
+ auto with sc.
+ pick fresh x. forwards: H7 (swap_c a x C); auto.
apply (swap_struct_congr _ a x) in H4.
repeat rewrite swap_appr in H4. subst; simpl_swap in H4.
repeat rewrite (aeq_nu_diff a x).
4,7:rewrite swap_invo; reflexivity. 2,4:auto. 2,3: simpl_swap.
repeat (rewrite sc_appr_nu_indep_left; auto; try fsetdec).
constructor; auto.
+ pick fresh x. forwards: H7 (swap a x F). apply (swap_struct_congr _ a x) in H3.
repeat rewrite swap_appr in H3. subst; simpl_swap in H3.
repeat rewrite (aeq_conc_new_2 _ a x); auto. 2-3:simpl; fsetdec.
repeat rewrite <- sc_appr_nu_indep_right; auto. constructor; auto.
- forwards: aeq_lts_2 H0. apply aeq_mapV. eauto.
destruct_hyps. eexists; intuition eauto with hopi.
destructA A; inversion H1; inversion H5; subst; constructor; intros_all;
rewrite H4; reflexivity.
- forwards: IHHsc1 H; destruct_hyps.
forwards: IHHsc2 H0; destruct_hyps. eexists; intuition eauto.
eapply sim_test_trans; eauto. intros_all. rewrite H4; auto.
Qed.
Lemma struct_congr_sim: simulation sc0.
Proof. apply late_implies_sim. intros_all.
forwards: @struct_congr_sim' H. rewrite mapV_id. eauto.
destruct_hyps. rewrite mapV_id in H1. eexists; eauto.
Qed.
Lemma struct_congr_bisim: bisimulation sc0.
Proof. apply sim_sym_imply_bisim. apply struct_congr_sim. apply sc0_sym. Qed.
Lemma oe_sc0 : ∀ Rel,
mod_aeq Rel → Rincl sc0 Rel → Rincl sc0 (open_extension Rel).
Proof. intros_all. apply oe_proc0; auto. Qed.
Inductive struct_congr {V : Set} : binary (proc V) :=
| sc_par_assoc : ∀ P Q R, struct_congr (P // (Q // R)) ((P // Q) // R)
| sc_par_assoc_rev : ∀ P Q R, struct_congr ((P // Q) // R) (P // (Q // R))
| sc_par_comm : ∀ P Q, struct_congr (P // Q) (Q // P)
| sc_par_nil : ∀ P, struct_congr (P // PO) P
| sc_par_nil_conv : ∀ P, struct_congr P (P // PO)
| sc_scope: ∀ a P Q, a `notin` fn Q → struct_congr (nu a, (P // Q)) ((nu a, P) // Q)
| sc_scope_rev: ∀ a P Q, a `notin` fn Q → struct_congr ((nu a, P) // Q) (nu a, (P // Q))
| sc_nu_nil : ∀ a, struct_congr (nu a, PO) PO
| sc_nu_nil_rev : ∀ a, struct_congr PO (nu a, PO)
| sc_nu_nu : ∀ a b P, struct_congr (nu a, (nu b, P)) (nu b, (nu a, P))
| sc_nil : struct_congr PO PO
| sc_var : ∀ x, struct_congr (pr_var x) (pr_var x)
| sc_par : ∀ P Q P' Q', struct_congr P Q → struct_congr P' Q'
→ struct_congr (P // P') (Q // Q')
| sc_inp : ∀ a P Q, @struct_congr (incV V) P Q → struct_congr (a? P) (a? Q)
| sc_out : ∀ a P Q P' Q', struct_congr P Q → struct_congr P' Q'
→ struct_congr (a!(P) P') (a!(Q) Q')
| sc_nu : ∀ a P Q, struct_congr P Q → struct_congr (nu a, P)(nu a, Q)
| sc_aeq : ∀ P Q, P=A=Q → struct_congr P Q
| sc_trans : ∀ P Q R, struct_congr P Q → struct_congr Q R → struct_congr P R
.
Notation "P =sc= Q" := (struct_congr P Q) (at level 70, no associativity).
Hint Constructors struct_congr:sc.
Lemma sc_refl {V : Set} : ∀ P, @struct_congr V P P.
Proof. induction P; auto with sc. Qed.
Lemma sc_symmetric {V : Set} : ∀ (P Q:proc V),
struct_congr P Q → struct_congr Q P.
Proof.
intros P Q H. induction H; eauto with sc. apply aeq_sym in H. eauto with sc.
Qed.
Lemma sc_genNu {V:Set}: ∀ L (P Q:proc V), struct_congr P Q →
struct_congr (genNu L P) (genNu L Q).
Proof.
induction L; simpl; auto with sc.
Qed.
Lemma fn_sc : ∀ V (P Q : proc V), struct_congr P Q → fn P [=] fn Q.
Proof. intros. induction H; simpl; try fsetdec. apply aeq_fn. auto.
Qed.
Lemma swap_struct_congr : ∀ V b c (P Q : proc V), struct_congr P Q →
struct_congr (swap b c P) (swap b c Q).
Proof.
intros. gen b c. induction H; simpl; intros; try solve [auto with sc];
try solve [constructor; simpl_swap];
apply sc_trans with (swap b c Q); auto with sc.
Qed.
Lemma swap_struct_congr' : ∀ V b c (P Q : proc V),
struct_congr (swap b c P) (swap b c Q) → struct_congr P Q.
Proof. intros. rewrite <- (swap_invo _ b c P). rewrite <- (swap_invo _ b c Q).
apply swap_struct_congr. auto.
Qed.
Hint Resolve sc_refl sc_aeq sc_symmetric sc_genNu:sc.
Add Parametric Relation (V:Set) : (proc V) (@struct_congr V)
reflexivity proved by (@sc_refl V)
symmetry proved by (@sc_symmetric V)
transitivity proved by (@sc_trans V)
as aeq_eq_rel.
Add Parametric Morphism (V:Set) (a:name): (pr_nu a)
with signature (@struct_congr V) ==> (@struct_congr V)
as nu_sc_morphism.
Proof. intros; constructor; auto. Qed.
Add Parametric Morphism (V:Set) L: (genNu L)
with signature (@struct_congr V) ==> (@struct_congr V)
as genNu_sc_morphism.
Proof. intros. apply sc_genNu; auto. Qed.
Add Parametric Morphism (V:Set) (a:name): (pr_inp a)
with signature (@struct_congr (incV V)) ==> (@struct_congr V)
as inp_sc_morphism.
Proof. intros; constructor; auto. Qed.
Add Parametric Morphism (V:Set) (a:name): (pr_snd a)
with signature (@struct_congr V) ==> (@struct_congr V) ==> (@struct_congr V)
as snd_sc_morphism.
Proof. intros; constructor; auto. Qed.
Add Parametric Morphism (V:Set): (@pr_par V)
with signature (@struct_congr V) ==> (@struct_congr V) ==> (@struct_congr V)
as par_sc_morphism.
Proof. intros; constructor; auto. Qed.
Add Parametric Morphism (V:Set): (fn)
with signature (@struct_congr V) ==> (Equal)
as fn_sc_morphism.
Proof. intros. apply fn_sc; auto. Qed.
Add Parametric Morphism (V:Set) b c : (swap b c)
with signature (@struct_congr V) ==> (@struct_congr V)
as swap_sc_morphism.
Proof. intros. apply swap_struct_congr; auto. Qed.
Instance subrel_aeq_sc (V:Set):
subrelation (@aeq V) (@struct_congr V).
Proof. intros_all. apply sc_aeq; auto. Qed.
Lemma sc_mapV: ∀ (V W:Set) P Q (f:V → W), @struct_congr V P Q
→ @struct_congr W (mapV f P) (mapV f Q).
Proof.
intros. gen W. induction H; simpl; auto with sc.
- intros. apply sc_scope. simpl_swap.
- intros. apply sc_scope_rev. simpl_swap.
- intros. constructor. apply aeq_mapV. auto.
- eauto with sc.
Qed.
Lemma sc_liftV: ∀ (V W:Set) (f:V → proc W) (g:V → proc W),
(∀ x, @struct_congr W (f x) (g x)) →
(∀ x, @struct_congr (incV W) (liftV f x) (liftV g x)).
Proof.
intros. destruct x; simpl; auto with sc.
apply sc_mapV. auto with sc.
Qed.
Lemma sc_bind_1: ∀ (V W:Set) (P : proc V) N (f:V → proc W) (g:V → proc W),
(∀ x, @struct_congr W (f x) (g x)) →
@struct_congr W (bind f N P) (bind g N P).
Proof.
intros V'' W P''. gen W. apply size_induction with (x:=P'').
intros V P IH; intros. destruct P; unfold bind; simpl in *; foldbind;
try solve [apply H]; try solve [constructor; try apply IH; try nat_math; auto;
try fsetdec; try intro; auto].
- constructor. apply IH. nat_math. intro. apply× sc_liftV. intro; auto.
- destruct atom_fresh. apply sc_nu. foldbind. apply IH.
+ rewrite swap_size_eq. nat_math.
+ intro; auto.
Qed.
Hint Resolve sc_bind_1 sc_liftV sc_mapV:sc.
Lemma bind_para_simpl : ∀ V W (P Q : proc V) (f : V → proc W) N,
bind f N (P//Q) = bind f N P // bind f N Q.
Proof. intros. unfold bind. simpl. foldbind. auto. Qed.
Lemma sc_bind_2: ∀ (V W:Set) (P Q : proc V) N (f:V → proc W),
@struct_congr V P Q → fn P [<=] N → (∀ x, fn (f x) [<=] N) →
@struct_congr W (bind f N P) (bind f N Q).
Proof. intros. gen W N. induction H; simpl; intros;
repeat rewrite bind_para_simpl; try solve [auto with sc]; unfold bind;
simpl in *; repeat destruct atom_fresh; foldbind; try solve [auto with sc].
- assert (fn Q [<=] N) by fsetdec.
assert (swap a x Q =A= Q). { destruct (x==a); subst.
simpl_swap. apply aeq_swap_indep; auto. } rewrite sc_scope_rev.
constructor. apply sc_par; auto with sc. apply sc_aeq.
rewrites (>>aeq_bind_3 (swap a x Q) Q); auto. fsetdec.
apply aeq_bind_2; try fsetdec; intro; rewrite H1; fsetdec.
rewrite fn_bind; try rewrite H3; auto.
- assert (fn Q [<=] N) by fsetdec.
assert (swap a x Q =A= Q). { destruct (x==a); subst.
simpl_swap. apply aeq_swap_indep; auto. } rewrite sc_scope_rev.
constructor. apply sc_par; auto with sc. apply sc_aeq.
rewrites (>>aeq_bind_3 (swap a x Q) Q); auto. fsetdec.
apply aeq_bind_2; try fsetdec; intro; rewrite H1; fsetdec.
rewrite fn_bind; try rewrite H3; auto.
- destruct (a==b); subst; try reflexivity. assert (x≠x0) by fsetdec.
apply sc_trans with (swap x x0 (nu x, ( nu x0, ( bind f (add x0 (add x N))
(swap (swap_aux a x b) x0 (swap a x P)))))). apply sc_aeq. symmetry.
apply aeq_swap_indep; simpl; fsetdec.
simpl. simpl_swap. rewrite sc_nu_nu. constructor. constructor.
assert (fn (swap (swap_aux a x b) x0 (swap a x P)) [<=] add x0 (add x N)).
{ clears W. simpl_swap_aux; intro; intro; simpl_swap in H1;
simpl_swap_aux×. 6:destruct (a0==x0); subst.
7:enough (a0 `in` N) by fsetdec; clears x x0.
all:fsetdec. }
rewrite swap_bind_f_indep; auto; try solve [intros; rewrite H1; fsetdec].
assert ((swap_fs x x0 (add x0 (add x N))) [=] (add x0 (add x N))).
{ symmetry; apply swap_fs_in; fsetdec. } simpl_swap in H2.
rewrites (>>aeq_bind_2 (swap_fs x x0 (add x0 (add x N))) (add x0 (add x N)));
try solve [intros; rewrite H1; try rewrite H3; fsetdec].
rewrite <- H3. simpl_swap. simpl_swap.
apply sc_aeq. symmetry. apply aeq_bind_3. rewrite <- H3. simpl_swap.
simpl_swap_aux*; simpl_swap.
+ rewrite swap_sym. rewrite shuffle_swap; auto. rewrite swap_sym .
rewrite (swap_sym _ b x0). reflexivity.
+ rewrite (swap_sym _ a x0 (swap a x P)). rewrite (shuffle_swap _ x0 a x); auto.
rewrite (swap_sym _ x x0). rewrite swap_sym. simpl_swap.
+ destruct (a==x0); destruct (b==x0); subst; simpl_swap. fsetdec.
× rewrite (swap_sym _ b x0). rewrite shuffle_swap; auto.
rewrite (swap_sym _ x x0). simpl_swap. rewrite swap_sym. reflexivity.
× rewrite (swap_equivariance _ x x0); simpl_swap_aux.
rewrite (swap_sym _ x x0). reflexivity.
× rewrite swap_indep; auto. rewrite (swap_equivariance _ x x0);
simpl_swap_aux. rewrite (swap_equivariance _ x x0); simpl_swap_aux.
rewrite (aeq_swap_indep _ x x0). reflexivity. auto.
fsetdec. fsetdec.
- constructor.
apply IHstruct_congr1 ; auto; fsetdec.
apply IHstruct_congr2 ; auto; fsetdec.
- constructor. apply IHstruct_congr; auto.
fsetdec. intros [|x]; simpl; simpl_swap; fsetdec.
- unfold bind. simpl. foldbind. constructor. apply IHstruct_congr1; auto.
fsetdec. apply IHstruct_congr2; auto. fsetdec.
- constructor. apply (swap_struct_congr' _ a x). rewrite swap_bind.
2:apply fnsaxp; auto. 2:intro; rewrite H1; fsetdec. simpl_swap.
rewrite IHstruct_congr. 2:forwards: fnsaxp H0 n; simpl_swap in H2; simpl_swap.
2:intro; simpl_swap; rewrite H1; fsetdec.
rewrite swap_bind. simpl_swap. apply fnsaxp; auto.
rewrites <- (>>fn_sc H). auto. intro; rewrite H1; fsetdec.
- constructor. rewrite H in H0. apply aeq_bind_3; auto.
- apply sc_trans with (bind f N Q). eauto with sc. apply IHstruct_congr2.
rewrite <- H. auto. auto.
Qed.
Lemma sc_bind: ∀ (V W:Set) (P Q : proc V) N (f:V → proc W) (g:V → proc W),
@struct_congr V P Q → fn P [<=] N → (∀ x, fn (f x) [<=] N) →
(∀ x, @struct_congr W (f x) (g x)) →
@struct_congr W (bind f N P) (bind g N Q).
Proof. intros. apply sc_trans with (bind f N Q).
apply sc_bind_2; auto. apply sc_bind_1; auto.
Qed.
Hint Resolve sc_bind:sc.
Lemma sc_nu_genNu {V:Set}: ∀ L a (P Q:proc V),
struct_congr (genNu L (nu a, P)) (nu a, (genNu L P)).
Proof. intro L; gen V. induction L; intros; simpl; try reflexivity.
rewrite IHL; auto. constructor.
Qed.
Lemma sc_scope_genNu {V:Set}: ∀ L (P Q:proc V),
inter (list_to_fs L) (fn Q) [=] empty →
struct_congr (genNu L (P//Q)) (genNu L P//Q).
Proof. induction L; intros; simpls; try reflexivity.
rewrite IHL. constructor. all:fsetdec. Qed.
Lemma sc_appr_appl : ∀ F C, struct_congr (appr F C) (appl C F).
Proof. intros. unfold appr. unfold appl. destruct conc_convert.
apply sc_genNu. auto with sc. Qed.
Lemma sc_appr_nu_indep_left : ∀ x P (C:conc), x `notin` fn_agent C → conc_wf C →
appr (nu x, P) C =sc= nu x, (appr P C).
Proof. intros. remember (conc_convert C (add x (fn P))) as C'.
assert (C =Ac= C'). { rewrite HeqC'. apply aeq_conc_convert. } rewrite H1.
destruct C as [CL CP CQ]; destruct C' as [C'L C'P C'Q].
symmetry in HeqC'. simpl in HeqC'. forwards: fn_conc_convert_0' HeqC'.
unfold appr. simpl. repeat (rewrite conc_convert_indep_wf; auto; try fsetdec).
simpl in H. rewrite <- sc_nu_genNu; auto. apply sc_genNu. rewrite sc_scope.
constructor. rewrite subst_nu_indep. 1,3:reflexivity.
forwards: fn_conc_convert_1 HeqC'. fsetdec.
forwards: fn_conc_convert_2 HeqC'. fsetdec.
Qed.
Lemma sc_appr_nu_indep_right : ∀ x (F:abs) C, x `notin` fn F → conc_wf C →
nu x, (appr F C) =sc= appr F (conc_new x C).
Proof. intros. remember (conc_convert C (add x (fn F))) as C'.
assert (C =Ac= C'). { rewrite HeqC'. apply aeq_conc_convert. } rewrite H1.
destruct C' as [L' P' Q']. destruct C as [L P Q]. unfold conc_new. simpl.
assert (conc_wf (conc_def L' P' Q')). { rewrite HeqC'; auto. }
assert (inter (list_to_fs L') (add x (fn F)) [=] empty).
{ eapply fn_conc_convert_0'. symmetry; eauto. }
rewrite conc_convert_indep_wf; auto; try fsetdec. case_if;
unfold appr; simpl; repeat (rewrite conc_convert_indep_wf; auto; try fsetdec).
- case_if; try fsetdec. simpl. reflexivity.
- rewrite <- sc_nu_genNu; auto. apply sc_genNu. rewrite sc_par_comm.
rewrite (sc_par_comm _ (nu x, Q')). constructor. rewrite fn_subst. fsetdec.
Qed.
Lemma sc_appr_par_shift_right : ∀ P Q (C:conc), conc_wf C →
appr (P// shiftV Q) C =sc= appr P C // Q.
Proof. intros. remember (conc_convert C (union (fn (shiftV Q)) (fn P))) as C'.
assert (C =Ac= C'). { rewrite HeqC'. apply aeq_conc_convert. } rewrite H0.
destruct C as [CL CP CQ]; destruct C' as [C'L C'P C'Q].
symmetry in HeqC'. simpl in HeqC'. forwards: fn_conc_convert_0' HeqC'.
unfold appr. simpl. repeat (rewrite conc_convert_indep_wf; auto; try fsetdec).
rewrite subst_par. rewrite subst_shift. rewrite <- sc_scope_genNu.
apply sc_genNu. eauto with sc. simpl_swap in H1. fsetdec.
Qed.
Lemma sc_appr_par_shift_left : ∀ P Q (C:conc), conc_wf C →
appr (shiftV Q // P) C =sc= Q // appr P C.
Proof. intros. remember (conc_convert C (union (fn (shiftV Q)) (fn P))) as C'.
assert (C =Ac= C'). { rewrite HeqC'. apply aeq_conc_convert. } rewrite H0.
destruct C as [CL CP CQ]; destruct C' as [C'L C'P C'Q].
symmetry in HeqC'. simpl in HeqC'. forwards: fn_conc_convert_0' HeqC'.
unfold appr. simpl. repeat (rewrite conc_convert_indep_wf; auto; try fsetdec).
rewrite subst_par. rewrite (sc_par_comm Q). rewrite subst_shift.
rewrite <- sc_scope_genNu. apply sc_genNu. eauto with sc.
simpl_swap in H1. fsetdec.
Qed.
Lemma sc_appr_conc_parl : ∀ F P (C:conc), conc_wf C →
appr F C // P =sc= appr F (conc_parl C P).
Proof. intros. remember (conc_convert C (union (fn P) (fn F))) as CR.
assert (C =Ac= CR). { rewrite HeqCR. apply aeq_conc_convert. } rewrite H0.
assert (conc_wf CR). { rewrite HeqCR. auto. }
destruct CR as [CRL CRP CRQ]; destruct C as [CL CP CR].
simpls. symmetry in HeqCR. forwards: fn_conc_convert_0' HeqCR.
unfold conc_parl. simpl. rewrite conc_convert_indep_wf; [ | auto| fsetdec].
unfold appr. simpl. repeat (rewrite conc_convert_indep_wf; [ | auto| fsetdec]).
rewrite <- sc_scope_genNu. 2:fsetdec. apply sc_genNu. auto with sc.
Qed.
Lemma sc_appr_conc_parr : ∀ F P (C:conc), conc_wf C →
P // appr F C =sc= appr F (conc_parr P C).
Proof. intros. remember (conc_convert C (union (fn P) (fn F))) as CR.
assert (C =Ac= CR). { rewrite HeqCR. apply aeq_conc_convert. } rewrite H0.
assert (conc_wf CR). { rewrite HeqCR. auto. }
destruct CR as [CRL CRP CRQ]; destruct C as [CL CP CR].
simpls. symmetry in HeqCR. forwards: fn_conc_convert_0' HeqCR.
unfold conc_parr. simpl. rewrite conc_convert_indep_wf; [ | auto| fsetdec].
unfold appr. simpl. repeat (rewrite conc_convert_indep_wf; [ | auto| fsetdec]).
rewrite sc_par_comm. rewrite <- sc_scope_genNu. apply sc_genNu. eauto with sc. fsetdec.
Qed.
Definition sc0 := (@struct_congr Empty_set).
Notation "P =sc0= Q" := (sc0 P Q) (at level 70, no associativity).
Hint Unfold sc0:sc.
Lemma sc0_trans : trans sc0.
Proof. intros_all. rewrite H. auto. Qed.
Lemma sc0_sym : sym sc0.
Proof. intros_all. auto with sc. Qed.
Lemma sc0_refl : refl sc0.
Proof. intros_all. auto with sc. Qed.
Hint Resolve sc0_trans sc0_sym:sc.
Lemma struct_congr_sim' {V : Set} : ∀ P Q f, @struct_congr V P Q →
∀ l A, lts (mapV f P) l A →
∃ A', lts (mapV f Q) l A' ∧ sim_test struct_congr A A'.
Proof. intros P Q f Hsc. induction Hsc; intros.
- simpls; inversion H; subst.
+ ∃ (parl (parl A0 (mapV f Q)) (mapV f R)).
split. constructor. constructor. auto. destruct_agent_sim A0.
constructor. unsimpl (shiftV (mapV f Q // mapV f R)).
repeat rewrite sc_appr_par_shift_right; auto. constructor.
repeat rewrite <- sc_appr_conc_parl; auto. constructor.
+ inversion H4; subst.
× eexists. split. constructor. constructor 4. eauto.
destruct_agent_sim A.
constructor.
rewrite sc_appr_par_shift_right; auto. repeat rewrite sc_appr_par_shift_left; auto.
rewrite sc_appr_par_shift_right; auto. constructor.
rewrite <- sc_appr_conc_parr; auto.
repeat rewrite <- sc_appr_conc_parl; auto.
repeat rewrite <- sc_appr_conc_parr; auto. constructor.
× eexists. split. constructor 4. eauto. destruct_agent_sim A.
constructor. unsimpl (shiftV (mapV f P // mapV f Q)).
repeat rewrite sc_appr_par_shift_left; auto. constructor.
repeat rewrite <- sc_appr_conc_parr; auto. constructor.
× eexists. split. constructor 6 with a.
eapply lts_parr'; eauto with sc. reflexivity. eauto.
simpl. constructor. repeat rewrite <- sc_appr_appl. apply sc_appr_conc_parr; auto.
× eexists. split. constructor 7 with a.
eapply lts_parr'; eauto with sc. reflexivity. eauto.
simpl. constructor. symmetry. apply sc_appr_par_shift_left; auto.
+ inversion H5; subst; destructA A; inversion H6; subst.
× eexists. split. constructor. constructor 6 with a; eauto.
simpl. constructor. repeat rewrite <- sc_appr_appl. apply sc_appr_par_shift_right; auto.
× eexists. split. constructor 6 with a. eapply lts_parl'; eauto.
reflexivity. eauto. constructor. repeat rewrite <- sc_appr_appl.
rewrite sc_appr_par_shift_left; auto. rewrite <- sc_appr_conc_parl; auto.
constructor.
+ inversion H5; subst; destructA A; inversion H6; subst.
× eexists. split. constructor. constructor 7 with a; eauto.
simpl. constructor. symmetry. apply sc_appr_conc_parl; auto.
× eexists. split. constructor 7 with a. eapply lts_parl'; eauto.
reflexivity. eauto. constructor; auto. rewrite <- sc_appr_conc_parr; auto.
rewrite sc_appr_par_shift_right; auto. constructor.
- simpls; inversion H; subst.
+ inversion H4; subst.
× eexists. split. constructor. eauto. destruct_agent_sim A.
constructor. unsimpl (shiftV (mapV f Q // mapV f R)).
repeat rewrite sc_appr_par_shift_right; auto. constructor.
repeat rewrite <- sc_appr_conc_parl; auto. constructor.
× eexists. split. constructor 4. constructor. eauto.
destruct_agent_sim A. constructor.
rewrite sc_appr_par_shift_right; auto. repeat rewrite sc_appr_par_shift_left; auto.
rewrite sc_appr_par_shift_right; auto. constructor.
rewrite <- sc_appr_conc_parr; auto.
repeat rewrite <- sc_appr_conc_parl; auto.
repeat rewrite <- sc_appr_conc_parr; auto. constructor.
× eexists. split. constructor 6 with a. eauto.
eapply lts_parl'; eauto with sc. reflexivity.
simpl. constructor. repeat rewrite <- sc_appr_appl.
symmetry. apply sc_appr_par_shift_right; auto.
× eexists. split. constructor 7 with a. eauto.
eapply lts_parl'; eauto with sc. reflexivity. simpl. constructor.
apply sc_appr_conc_parl; auto.
+ eexists. split. constructor 4. constructor 4. eauto.
destruct_agent_sim A0. constructor.
unsimpl (shiftV (mapV f P // mapV f Q)).
repeat rewrite sc_appr_par_shift_left; auto. constructor.
repeat rewrite <- sc_appr_conc_parr; auto. constructor.
+ inversion H2; subst; destructA A; inversion H6; subst.
× eexists. split. constructor 6 with a; eauto. eapply lts_parr'; eauto.
reflexivity. constructor. repeat rewrite <- sc_appr_appl.
rewrite sc_appr_par_shift_left; auto. rewrite <- sc_appr_conc_parl; auto. constructor.
× eexists. split. constructor 4. constructor 6 with a; eauto.
constructor. repeat rewrite <- sc_appr_appl.
symmetry. apply sc_appr_conc_parr; auto.
+ inversion H2; subst; destructA A; inversion H6; subst.
× eexists. split. constructor 7 with a; eauto. eapply lts_parr'; eauto.
reflexivity. constructor. rewrite <- sc_appr_conc_parr; auto.
rewrite sc_appr_par_shift_right; auto. constructor.
× eexists. split. constructor 4. constructor 7 with a; eauto.
simpl. constructor. apply sc_appr_par_shift_left; auto.
- simpls. inversion H; subst.
+ ∃ (parr (mapV f Q) A0). split. auto with hopi.
destruct_agent_sim A0.
× eauto with sc.
× rewrite sc_appr_par_shift_right; auto. rewrite sc_appr_par_shift_left; auto with sc.
× rewrite <- sc_appr_conc_parl; auto. rewrite <- sc_appr_conc_parr; auto with sc.
+ ∃ (parl A0 (mapV f P)). split. auto with hopi.
destruct_agent_sim A0.
× eauto with sc.
× rewrite sc_appr_par_shift_right; auto. rewrite sc_appr_par_shift_left; auto with sc.
× rewrite <- sc_appr_conc_parl; auto. rewrite <- sc_appr_conc_parr; auto with sc.
+ ∃ (ag_proc (appr F C)). split. constructor 7 with a; auto.
constructor. symmetry; apply sc_appr_appl.
+ ∃ (ag_proc (appl C F)). split. constructor 6 with a; auto.
constructor. apply sc_appr_appl.
- inversion H; subst; try solve [inversion H5];
try solve [inversion H4]. eexists; intuition eauto. destruct_agent_sim A0.
+ eauto with sc.
+ asserts_rewrite (PO = (mapV (@VS Empty_set)) PO).
{ simpl. auto. } rewrite sc_appr_par_shift_right; auto with sc.
+ rewrite <- sc_appr_conc_parl; auto with sc.
- eexists. split. simpl. eauto with hopi.
destruct_agent_sim A.
+ eauto with sc.
+ asserts_rewrite (PO = (mapV (@VS Empty_set)) PO).
{ simpl. auto. } rewrite sc_appr_par_shift_right; auto with sc.
+ rewrite <- sc_appr_conc_parl; auto with sc.
- simpls. inversion H0; subst.
inversion H6; subst.
+ ∃ (parl (new a A) (mapV f Q)). split. eauto with hopi.
destruct_agent_sim A.
× constructor. simpl_swap.
× pick fresh x. assert (x≠a) by fsetdec.
repeat rewrite (aeq_nu_diff a x); auto.
3,5:rewrite swap_invo; reflexivity. 2-3:simpl; simpl_swap.
rewrite sc_appr_par_shift_right; auto.
repeat (rewrite sc_appr_nu_indep_left; auto; simpl; try fsetdec).
rewrite swap_shiftV. rewrite sc_appr_par_shift_right; auto.
rewrites (>>aeq_swap_indep (mapV f Q)); simpl_swap.
constructor. simpl_swap.
× pick fresh x. assert (x≠a) by fsetdec.
repeat rewrite (aeq_conc_new_2 _ a x); simpl; auto.
2: unfold conc_parl; destruct conc_convert eqn:?; simpls;
forwards: fn_conc_convert_1 Heqc; forwards: fn_conc_convert_2 Heqc;
simpl_swap; fsetdec.
rewrite <- sc_appr_conc_parl; auto.
repeat (rewrite <- sc_appr_nu_indep_right; [ | simpl; fsetdec | ]); auto.
rewrite swap_conc_parl. rewrite <- sc_appr_conc_parl; auto.
rewrites (>>aeq_swap_indep (mapV f Q)); simpl_swap.
constructor. simpl_swap.
+ ∃ (parr (nu a, (mapV f P)) A). split. eauto with hopi.
destruct_agent_sim A; try (assert (a `notin` fn p) by
(rewrites (>>lts_fn H7); simpl_swap)).
× constructor; auto.
× pick fresh x. assert (x≠a) by fsetdec. repeat rewrite (aeq_nu_diff a x).
4,7:rewrite swap_invo; reflexivity. 2,4:auto. 2,3:simpl; simpl_swap.
rewrite sc_appr_nu_indep_left; simpl; auto.
rewrite swap_shiftV. unsimpl (shiftV (nu x, (swap a x (mapV f P)))).
repeat rewrite sc_appr_par_shift_left; auto. rewrites (>>aeq_swap_indep p); auto.
constructor. rewrite fn_appr. simpl. fsetdec.
× pick fresh x. assert (x≠a) by fsetdec. rewrite (aeq_nu_diff a x).
4:rewrite swap_invo; reflexivity. 2:auto. 2:simpl_swap.
repeat rewrite (aeq_conc_new_2 _ a x); simpl; auto.
2: unfold conc_parr; destruct conc_convert eqn:?; simpls;
forwards: fn_conc_convert_1 Heqc; forwards: fn_conc_convert_2 Heqc;
simpl_swap; fsetdec.
rewrite <- sc_appr_conc_parr; auto. rewrites <- (>>sc_appr_nu_indep_right); auto.
rewrite swap_conc_parr. rewrite aeq_conc_swap_indep; auto. 2:simpl; fsetdec.
2:rewrites (>>lts_fn H7); simpl_swap.
rewrite <- sc_appr_conc_parr; auto.
constructor. rewrite fn_appr; simpl; fsetdec.
+ assert (a≠a0).
{ forwards: notin_fn_notin_fnlab H8. simpl_swap. simpls. fsetdec. }
∃ (ag_proc (appl (conc_new a C) F)). split.
constructor 6 with a0; try unsimpl (new a C); eauto with hopi.
simpl; constructor. repeat rewrite <- sc_appr_appl. apply sc_appr_nu_indep_right; auto.
rewrites (>>lts_fn H8). simpl_swap.
+ assert (a≠a0).
{ forwards: notin_fn_notin_fnlab H8. simpl_swap. simpls. fsetdec. }
∃ (ag_proc (appr (nu a, F) C)). split.
constructor 7 with a0; try unsimpl (new a (ag_abs F)); eauto with hopi.
simpl; constructor. symmetry. apply sc_appr_nu_indep_left; auto.
rewrites (>>lts_fn H8). simpl_swap.
- simpls. inversion H0; subst.
+ inversion H5; subst. ∃ (new a (parl A (mapV f Q))).
split. eauto with hopi.
destruct_agent_sim A.
× constructor. simpl_swap.
× pick fresh x. assert (x≠a) by fsetdec. symmetry.
repeat rewrite (aeq_nu_diff a x).
4,7:rewrite swap_invo; reflexivity. 2,4:auto. 2,3:simpl; simpl_swap.
rewrite sc_appr_par_shift_right; auto.
repeat (rewrite sc_appr_nu_indep_left; auto; simpl; try fsetdec).
rewrite swap_shiftV. rewrite sc_appr_par_shift_right; auto.
rewrites (>>aeq_swap_indep (mapV f Q)); simpl_swap.
constructor. simpl_swap.
× pick fresh x. assert (x≠a) by fsetdec. symmetry.
repeat rewrite (aeq_conc_new_2 _ a x); simpl; auto.
2: unfold conc_parl; destruct conc_convert eqn:?; simpls;
forwards: fn_conc_convert_1 Heqc; forwards: fn_conc_convert_2 Heqc;
simpl_swap; fsetdec.
rewrite <- sc_appr_conc_parl; auto.
repeat (rewrite <- sc_appr_nu_indep_right; [ | simpl; fsetdec | ]); auto.
rewrite swap_conc_parl. rewrite <- sc_appr_conc_parl; auto.
rewrites (>>aeq_swap_indep (mapV f Q)); simpl_swap.
constructor. simpl_swap.
+ ∃ (new a (parr (mapV f P) A0)). split. constructor.
eapply notin_fn_notin_fnlab; eauto. simpl_swap.
eauto with hopi. destruct_agent_sim A0; try (assert (a `notin` fn p) by
(rewrites (>>lts_fn H5); simpl_swap)).
× constructor; auto.
× pick fresh x. assert (x≠a) by fsetdec. symmetry.
repeat rewrite (aeq_nu_diff a x).
4,7:rewrite swap_invo; reflexivity. 2,4:auto. 2,3:simpl; simpl_swap.
rewrite sc_appr_nu_indep_left; simpl; auto.
rewrite swap_shiftV. unsimpl (shiftV (nu x, (swap a x (mapV f P)))).
repeat rewrite sc_appr_par_shift_left; auto. rewrites (>>aeq_swap_indep p); auto.
constructor. rewrite fn_appr. simpl. fsetdec.
× pick fresh x. assert (x≠a) by fsetdec. symmetry. rewrite (aeq_nu_diff a x).
4:rewrite swap_invo; reflexivity. 2:auto. 2:simpl_swap.
repeat rewrite (aeq_conc_new_2 _ a x); simpl; auto.
2: unfold conc_parr; destruct conc_convert eqn:?; simpls;
forwards: fn_conc_convert_1 Heqc; forwards: fn_conc_convert_2 Heqc;
simpl_swap; fsetdec.
rewrite <- sc_appr_conc_parr; auto. rewrites <- (>>sc_appr_nu_indep_right); auto.
rewrite swap_conc_parr. rewrite aeq_conc_swap_indep; auto. 2:simpl; fsetdec.
2:rewrites (>>lts_fn H5); simpl_swap.
rewrite <- sc_appr_conc_parr; auto.
constructor. rewrite fn_appr; simpl; fsetdec.
+ assert (a≠a0).
{ forwards: notin_fn_notin_fnlab H6. simpl_swap. simpls. fsetdec. }
inversion H3; subst. destruct A; inversion H5; clear H5.
∃ (new a (ag_proc (appl c F))). split. constructor. fsetdec.
constructor 6 with a0; eauto with hopi.
simpl; constructor. repeat rewrite <- sc_appr_appl. symmetry.
apply sc_appr_nu_indep_right; auto. rewrites (>>lts_fn H6). simpl_swap.
+ assert (a≠a0).
{ forwards: notin_fn_notin_fnlab H6. simpl_swap. simpls. fsetdec. }
inversion H3; subst. destruct A as [ | | ]; inversion H5; clear H5.
eexists. split. constructor. fsetdec. constructor 7 with a0; eauto with sc.
simpl; constructor; auto. apply sc_appr_nu_indep_left; auto.
rewrites (>>lts_fn H6). simpl_swap.
- inversion H; try solve [inversion H5]; try solve [inversion H6].
- inversion H.
- inversion H; subst. inversion H5; subst; simpl.
∃ (new b (new a A)). split; intuition eauto with hopi.
destruct (a==b);subst. destruct_agent_sim A; reflexivity. destruct_agent_sim A.
+ constructor.
+ clears V l. pick fresh x. assert (a≠x) by fsetdec; assert (b≠x) by fsetdec.
pick fresh y. assert (a≠y) by fsetdec; assert (b≠y) by fsetdec;
assert (x≠y) by fsetdec. repeat rewrite (aeq_nu_diff a x).
4,7:rewrite swap_invo; reflexivity. 2,4:auto. 2,3:simpl; simpl_swap.
repeat rewrite (aeq_nu_diff b y). 4,7:rewrite swap_invo; reflexivity.
2,4:auto. 2,3:simpl; simpl_swap; simpl_swap_aux.
repeat (rewrite sc_appr_nu_indep_left; simpl; auto); simpl_swap_aux.
rewrite swap_indep; auto. constructor.
+ forwards: lts_conc_wf H7. clears V l. pick fresh x. assert (a≠x) by fsetdec;
assert (b≠x) by fsetdec. pick fresh y. assert (a≠y) by fsetdec;
assert (b≠y) by fsetdec; assert (x≠y) by fsetdec.
repeat rewrite (aeq_conc_new_2 _ a x); auto.
2-3: try rewrite fn_conc_new; simpl; fsetdec.
repeat rewrite (aeq_conc_new_2 _ b y); auto.
2-3: try rewrite fn_conc_new; simpl_swap; simpl_swap_aux; fsetdec.
repeat rewrite swap_conc_new; simpl_swap_aux. repeat rewrite <-
sc_appr_nu_indep_right; auto. rewrite swap_list_indep; auto.
repeat rewrite (swap_indep _ b); auto. constructor.
- inversion H.
- inversion H.
- simpls; inversion H; subst.
+ forwards: IHHsc1 H4. destruct_hyps.
eexists. splits; eauto with hopi. destructA A0; destructA x;
inversion H1; subst; simpl; constructor; intros_all.
× apply sc_par; eauto with sc.
× repeat rewrite sc_appr_par_shift_right; auto. apply sc_par; eauto with sc.
× repeat rewrite <- sc_appr_conc_parl; auto. apply sc_par; eauto with sc.
+ forwards: IHHsc2 H4. destruct_hyps.
eexists. splits; eauto with hopi. destructA A0; destructA x;
inversion H1; subst; simpl; constructor; intros_all.
× apply sc_par; eauto with sc.
× repeat rewrite sc_appr_par_shift_left; auto. apply sc_par; eauto with sc.
× repeat rewrite <- sc_appr_conc_parr; auto. apply sc_par; eauto with sc.
+ forwards: IHHsc1 H2. forwards: IHHsc2 H5. destruct_hyps.
inversion H3; inversion H4; subst.
eexists. split; eauto with hopi. simpl; constructor.
repeat rewrite <- sc_appr_appl. apply transitivity with (appr F' C); auto.
+ forwards: IHHsc1 H2. forwards: IHHsc2 H5. destruct_hyps.
inversion H3; inversion H4; subst.
eexists. split; eauto with hopi. simpl; constructor.
apply transitivity with (appr F' C); auto.
- simpls; inversion H; subst.
eexists; splits; eauto with hopi. constructor. intros.
remember (conc_convert C (union (fn (mapV (incV_map f) P)) (fn (mapV (incV_map f) Q)))) as C'.
asserts_rewrite (C =Ac= C'). { subst. apply aeq_conc_convert. }
assert (conc_wf C'). { subst; auto. }
unfold appr. destruct C' as [L' P' Q']; destruct C as [CL CP CQ]. simpls.
symmetry in HeqC'. forwards: fn_conc_convert_0' HeqC'.
repeat (rewrite conc_convert_indep_wf; [ | auto | fsetdec]).
apply sc_genNu. constructor; try reflexivity. unfold subst.
rewrites (>>aeq_bind_2 (union (union (fn (mapV (incV_map f) P)) (fn P'))
(fn (mapV (incV_map f) Q)))). 2,4:fsetdec. 1-2: intros [|x]; simpl; fsetdec.
rewrites (>>aeq_bind_2 (union (fn (mapV (incV_map f) Q)) (fn P'))
(union (union (fn (mapV (incV_map f) P)) (fn P')) (fn (mapV (incV_map f) Q)))).
2,4:fsetdec. 1-2: intros [|x]; simpl; fsetdec.
apply sc_bind. auto with sc. fsetdec.
intros [|x]; simpl; fsetdec. intro; reflexivity.
- simpls; inversion H; subst.
eexists; splits; eauto with hopi. constructor. intros F.
unfold appr. simpl. apply sc_par; auto with sc. unfold subst.
rewrites (>>aeq_bind_2 (union (union (fn F) (fn (mapV f P))) (fn (mapV f Q)))).
2,4:fsetdec. 1-2: intros [|x]; simpl; fsetdec.
rewrites (>>aeq_bind_2 (union (fn F) (fn (mapV f Q)))
(union (union (fn F) (fn (mapV f P))) (fn (mapV f Q)))).
2,4:fsetdec. 1-2: intros [|x]; simpl; fsetdec.
apply sc_bind. reflexivity. fsetdec. intros [|x]; simpl; fsetdec.
intros [|x]; simpl; auto with sc.
- inversion H; subst. forwards: IHHsc H5. destruct_hyps.
eexists; intuition (simpl; eauto with hopi).
destructA A0; destructA x; inversion H1; subst; constructor; try intros.
+ auto with sc.
+ pick fresh x. forwards: H7 (swap_c a x C); auto.
apply (swap_struct_congr _ a x) in H4.
repeat rewrite swap_appr in H4. subst; simpl_swap in H4.
repeat rewrite (aeq_nu_diff a x).
4,7:rewrite swap_invo; reflexivity. 2,4:auto. 2,3: simpl_swap.
repeat (rewrite sc_appr_nu_indep_left; auto; try fsetdec).
constructor; auto.
+ pick fresh x. forwards: H7 (swap a x F). apply (swap_struct_congr _ a x) in H3.
repeat rewrite swap_appr in H3. subst; simpl_swap in H3.
repeat rewrite (aeq_conc_new_2 _ a x); auto. 2-3:simpl; fsetdec.
repeat rewrite <- sc_appr_nu_indep_right; auto. constructor; auto.
- forwards: aeq_lts_2 H0. apply aeq_mapV. eauto.
destruct_hyps. eexists; intuition eauto with hopi.
destructA A; inversion H1; inversion H5; subst; constructor; intros_all;
rewrite H4; reflexivity.
- forwards: IHHsc1 H; destruct_hyps.
forwards: IHHsc2 H0; destruct_hyps. eexists; intuition eauto.
eapply sim_test_trans; eauto. intros_all. rewrite H4; auto.
Qed.
Lemma struct_congr_sim: simulation sc0.
Proof. apply late_implies_sim. intros_all.
forwards: @struct_congr_sim' H. rewrite mapV_id. eauto.
destruct_hyps. rewrite mapV_id in H1. eexists; eauto.
Qed.
Lemma struct_congr_bisim: bisimulation sc0.
Proof. apply sim_sym_imply_bisim. apply struct_congr_sim. apply sc0_sym. Qed.
Lemma oe_sc0 : ∀ Rel,
mod_aeq Rel → Rincl sc0 Rel → Rincl sc0 (open_extension Rel).
Proof. intros_all. apply oe_proc0; auto. Qed.
Definition simulation_up_to_sc (Rel: binary proc0) : Prop :=
∀ P Q, Rel P Q → test_proc (sc0 ° Rel ° sc0) P Q ∧
test_abs (sc0 ° Rel ° sc0) P Q ∧
test_conc (sc0 ° Rel ° sc0) P Q.
Definition bisimulation_up_to_sc (Rel : binary proc0) : Prop :=
(simulation_up_to_sc Rel) ∧ (simulation_up_to_sc (inverse Rel)).
Lemma up_to_sc_sim : ∀ Rel, simulation_up_to_sc Rel
→ simulation (sc0 ° Rel ° sc0).
Proof.
intros Rel Hsim. intros_all. inverts H. destruct H0.
inverts H0. destruct H1. destruct struct_congr_bisim.
forwards*: H2 P x H. forwards*: H2 x0 Q.
specialize (Hsim x x0 H0).
splits; intros; forwards_test sc0; forwards_test (sc0 ° Rel ° sc0);
forwards_test sc0; eexists; intuition (try eassumption);
destruct_comp; ∃ x1; split; eauto with sc; ∃ x2; eauto with sc.
Qed.
Lemma up_to_sc_sound : ∀ Rel, bisimulation_up_to_sc Rel
→ Rincl Rel bisimilarity.
Proof.
intros_all. inverts H. ∃ (sc0 ° Rel ° sc0).
split. split. apply up_to_sc_sim; auto.
- replace (inverse (sc0 ° Rel ° sc0)) with (sc0 ° inverse Rel ° sc0).
apply up_to_sc_sim; auto.
repeat (rewrite comp_trans).
asserts_rewrite (inverse sc0 = sc0).
rewrite inverse_sym; auto with sc.
apply comp_assoc.
- ∃ x. split. reflexivity. ∃ y. intuition.
Qed.