HOcore.InclIoMultiBisIoCxtBis
Require Import HOcore.Prelim.
Require Import HOcore.ComplLat
HOcore.CondClos
HOcore.HoCore
HOcore.Multiset
HOcore.Ren
HOcore.Subst
HOcore.Bis
HOcore.IoMultiBis.
Require Import HOcore.ComplLat
HOcore.CondClos
HOcore.HoCore
HOcore.Multiset
HOcore.Ren
HOcore.Subst
HOcore.Bis
HOcore.IoMultiBis.
This file contains the proof that IO bisimilarity defined via variable multiset bisimulations is contained in IO bisimilarity defined via variable context bisimulations
Connection between unguarded variable occurrence and variable context transitions
Lemma unguarded_var_then_step
(n: nat)
(p: process):
1 <= mult (count p) n ->
exists p',
step_var_cxt n p p'.
Proof.
intros H1.
induction p; try (cbv in H1; omega).
- simpl in H1.
destruct (nat_dec v n).
+ exists (Var 0). inv e. constructor.
+ omega.
- simpl in H1.
rewrite union_mult in H1.
remember (mult (count p1) n) as z.
destruct z.
+ simpl in H1.
specialize (IHp2 H1). destruct IHp2 as [p' H3].
eexists. eapply StVarCxtParR; eauto.
+ assert (1 <= S z) by omega.
specialize (IHp1 H). destruct IHp1 as [p' H3].
exists (Par p' p2.[ren (+1)]).
eapply StVarCxtParL; eauto.
Qed.
Lemma step_then_unguarded_var
(n: nat)
(p p': process):
step_var_cxt n p p' ->
1 <= mult (count p) n.
Proof.
intros H1. induction H1.
- simpl. destruct (nat_dec n n); try omega.
- simpl. rewrite union_mult. omega.
- simpl. rewrite union_mult. omega.
Qed.
(* Lifting all unguarded variables preserves their counts *)
Lemma lifted_iff_nonlifted
(p: process)
(n: var):
mult (count p) n =
mult (count p.[ren (+1)]) (S n).
Proof.
induction p; try (cbv; omega).
- simpl.
destruct (nat_dec v n); destruct (nat_dec (S v) (S n)); omega.
- simpl. do 2 rewrite union_mult. omega.
Qed.
Lemma lifted_has_no_zero
(p: process):
mult (count p.[ren (+1)]) 0 = 0.
Proof.
induction p; try reflexivity; simpl. rewrite union_mult. omega.
Qed.
Lemma contexts_decrease_var_occurrence
(p p': process)
(n: var):
step_var_cxt n p p' ->
S (mult (count p') (S n)) =
mult (count p) n.
Proof.
intros H1. induction H1; subst.
- simpl. destruct (nat_dec n n).
+ destruct (nat_dec 0 (S n)); omega.
+ exfalso. now apply n0.
- simpl. do 2 rewrite union_mult.
rewrite <- IHstep_var_cxt. simpl.
now rewrite <- lifted_iff_nonlifted.
- (* analog *)
simpl. do 2 rewrite union_mult.
rewrite <- IHstep_var_cxt. simpl.
now rewrite <- lifted_iff_nonlifted.
Qed.
Lemma contexts_maintain_var_occurrence
(p p': process)
(n: var):
step_var_cxt n p p' ->
forall i, i <> n ->
mult (count p') (S i) =
mult (count p) i.
Proof.
intros H1. induction H1; subst.
- simpl. intros i H2.
destruct (nat_dec n i); destruct (nat_dec 0 (S i)); try omega.
inv e. exfalso. now apply H2.
- intros i H4.
simpl. do 2 rewrite union_mult.
specialize (IHstep_var_cxt i H4). rewrite IHstep_var_cxt.
f_equal. now rewrite <- lifted_iff_nonlifted.
- (* analog *)
intros i H4.
simpl. do 2 rewrite union_mult.
specialize (IHstep_var_cxt i H4). rewrite IHstep_var_cxt.
f_equal. now rewrite <- lifted_iff_nonlifted.
Qed.
Lemma contexts_have_single_zero
(p p': process)
(n: var):
step_var_cxt n p p' ->
mult (count p') 0 = 1.
Proof.
intros H1. induction H1; subst.
- simpl. destruct (nat_dec 0 0); omega.
- simpl. rewrite union_mult.
rewrite IHstep_var_cxt.
now rewrite lifted_has_no_zero.
- simpl. rewrite union_mult.
rewrite IHstep_var_cxt.
now rewrite lifted_has_no_zero.
Qed.
Definition f_reach
(x: relation process)
(p' q': process) :=
exists p q n,
x p q /\
step_var_cxt n p p' /\
step_var_cxt n q q'.
Global Instance f_reach_mono: Mono f_reach.
Proof.
intros p q r r' [p' [q' [n [H3 [H4 H5]]]]] H6.
hnf. exists p', q', n. repeat split; auto.
Qed.
Global Instance f_reach_sym: SymFun f_reach.
Proof.
intros x p' q'.
split; intros [p [q [n [H2 [H3 H4]]]]]; repeat eexists; eauto.
Qed.
Lemma var_implication:
forall n p p',
step_var_cxt n p p' ->
p = p'.[(Var n)/].
Proof.
intros n p p' H1. induction H1; subst.
- reflexivity.
- asimpl. reflexivity.
- asimpl. reflexivity.
Qed.
Lemma var_then_out_step_impl_lifted_output:
forall p n p',
step_var_cxt n p p' ->
forall a r p'',
step_out a r p' p'' ->
exists r',
r = r'.[ren (+1)].
Proof.
intros p n p' H1.
induction H1; intros a r p'' H2; subst.
- ainv.
- inv H2.
+ destruct (IHstep_var_cxt a r p'0 H6) as [r' H7].
eexists. eauto.
+ revert q' H6.
induction q; intros q' H6; try ainv.
* eexists. eauto.
* { simpl in H6.
inv H6.
- destruct (IHq1 p'0 H5) as [r' H7]. eexists. eauto.
- destruct (IHq2 q'0 H5) as [r' H7]. eexists. eauto.
}
(* analog *)
- inv H2.
+ revert p' H6.
induction p; intros p' H6; try ainv.
* eexists. eauto.
* { simpl in H6.
inv H6.
- destruct (IHp1 p'0 H5) as [r' H7]. eexists. eauto.
- destruct (IHp2 q'0 H5) as [r' H7]. eexists. eauto.
}
+ destruct (IHstep_var_cxt a r q'0 H6) as [r' H7].
eexists. eauto.
Qed.
Lemma var_then_out_step_can_be_reversed:
forall p v p',
step_var_cxt v p p' ->
forall a r p'',
step_out a r.[ren (+1)] p' p'' ->
step_out a r p p''.[(Var v)/] /\
step_var_cxt v p''.[(Var v)/] p''.
Proof.
intros p v p' H1.
induction H1; intros a r p'' H2; subst.
- ainv.
- inv H2.
+ asimpl.
destruct (IHstep_var_cxt a r p'0 H6) as [H31 H32]. split.
* now constructor.
* econstructor; eauto.
+ asimpl.
destruct (var_implication H1).
destruct (step_out_preserv_ren H6) as [p2' [p2'' [H31 [H32 H33]]]].
subst q'.
eapply inj_ren_inv in H32.
Focus 2. apply decidable_inj_ren_is_inj_ren.
apply shift_decidable_inj_ren.
split.
* constructor.
eapply step_out_substit with (sigma := Nil .: ids) in H6.
asimpl. now asimpl in H6.
* econstructor; eauto. now asimpl.
(* analog *)
- inv H2.
+ asimpl.
destruct (var_implication H1).
destruct (step_out_preserv_ren H6) as [p2' [p2'' [H31 [H32 H33]]]].
subst p'.
eapply inj_ren_inv in H32.
Focus 2. apply decidable_inj_ren_is_inj_ren.
apply shift_decidable_inj_ren.
split.
* constructor.
eapply step_out_substit with (sigma := Nil .: ids) in H6.
asimpl. now asimpl in H6.
* eapply StVarCxtParR; eauto. now asimpl.
+ asimpl.
destruct (IHstep_var_cxt a r q'0 H6) as [H31 H32]. split.
* now constructor.
* eapply StVarCxtParR; eauto.
Qed.
Lemma var_then_in_step_can_be_reversed:
forall p v p',
step_var_cxt v p p' ->
forall a p'',
step_in a p' p'' ->
step_in a p p''.[up ((Var v) .: ids)] /\
step_var_cxt (S v) p''.[up ((Var v) .: ids)] p''.[(Var 1) .: (Var 0) .: (ren (+2))].
Proof.
intros p v p' H1.
induction H1; intros a p'' H2; subst.
- ainv.
- inv H2; asimpl.
+ specialize (IHstep_var_cxt a p'0 H4).
destruct IHstep_var_cxt as [H31 H32]. split.
* econstructor; eauto. now asimpl.
* asimpl in H32. econstructor; eauto. now asimpl.
+ destruct (step_in_preserv_ren H4) as [p2' [H21 H22]]. subst.
asimpl.
pose (H3 := var_implication H1). inv H3.
eapply step_in_substit with (sigma := Nil .: ids) in H4.
Focus 2. asimpl. reflexivity.
asimpl in H4.
split.
* eapply StInParR; asimpl; eauto.
* eapply StVarCxtParL.
Focus 2. reflexivity.
apply step_var_cxt_substit_ren with (xi := (+1)) in H1.
asimpl in H1.
assert (H3: ren (0 .: (+2)) = Var 0 .: ren (+2)).
{ change Var with ids. now asimpl. }
asimpl. asimpl in H1.
now rewrite <- H3.
(* analog *)
- inv H2; asimpl.
+ destruct (step_in_preserv_ren H4) as [p2' [H21 H22]]. subst.
asimpl.
pose (H3 := var_implication H1). inv H3.
eapply step_in_substit with (sigma := Nil .: ids) in H4.
Focus 2. asimpl. reflexivity.
asimpl in H4.
split.
* eapply StInParL; asimpl; eauto.
* eapply StVarCxtParR.
Focus 2. reflexivity.
apply step_var_cxt_substit_ren with (xi := (+1)) in H1.
asimpl in H1.
assert (H3: ren (0 .: (+2)) = Var 0 .: ren (+2)).
{ change Var with ids. now asimpl. }
asimpl. asimpl in H1.
now rewrite <- H3.
+ specialize (IHstep_var_cxt a q'0 H4).
destruct IHstep_var_cxt as [H31 H32]. split.
* eapply StInParR; eauto. now asimpl.
* asimpl in H32. eapply StVarCxtParR; eauto. now asimpl.
Qed.
Lemma var_and_out_can_be_combined:
forall p a r p'',
step_out a r p p'' ->
forall n p',
step_var_cxt n p p' ->
exists q,
step_out a r.[ren (+1)] p' q /\
p'' = q.[(Var n)/].
Proof.
intros p a r p'' H1. induction H1 as [ | a r p1 p'' p2 | a r q1 q'' q2 ].
- ainv.
- intros n p' H2.
inv H2.
+ destruct (IHstep_out n p'0 H4) as [q [H31 H32]]. subst.
eexists. split.
* constructor. eauto.
* asimpl. reflexivity.
+ apply var_implication in H4. subst.
exists (Par p''.[ren (+1)] q'). split.
* constructor. now apply step_out_substit.
* now asimpl.
(* analog *)
- intros n q' H2.
inv H2.
+ apply var_implication in H4. subst.
exists (Par p' q''.[ren (+1)]). split.
* constructor. now apply step_out_substit.
* now asimpl.
+ destruct (IHstep_out n q'0 H4) as [q [H31 H32]]. subst.
eexists. split.
* apply StOutParR. eauto.
* asimpl. reflexivity.
Qed.
Lemma var_and_in_can_be_combined:
forall p a p'',
step_in a p p'' ->
forall n p',
step_var_cxt n p p' ->
exists q,
step_in a p' q /\
p'' = q.[up ((Var n) .: ids)].
Proof.
intros p a p'' H1. induction H1; subst.
- ainv.
- intros n p2 H2. inv H2.
+ destruct (IHstep_in n p'0 H4) as [q2 [H31 H32]].
eexists. split.
* econstructor. eauto. reflexivity.
* subst. now asimpl.
+ eapply step_in_substit with (sigma := ren (+1)) in H1.
Focus 2. reflexivity.
eexists. split.
* econstructor. exact H1. reflexivity.
* apply var_implication in H4. subst. now asimpl.
(* analog *)
- intros n p2 H2. inv H2.
+ eapply step_in_substit with (sigma := ren (+1)) in H1.
Focus 2. reflexivity.
eexists. split.
* eapply StInParR. exact H1. reflexivity.
* apply var_implication in H4. subst. now asimpl.
+ destruct (IHstep_in n q'0 H4) as [q2 [H31 H32]].
eexists. split.
* eapply StInParR. eauto. reflexivity.
* subst. now asimpl.
Qed.
Lemma f_reach_cond_clos_for_s_ho_out:
CondClos s_ho_out
(increasify (bij_ren_clos °° f_reach))
decidable_inj_ren_clos
(const top2).
Proof.
intros x H1 _ H32 p'' q'' [H4 | H4].
- destruct H4 as [xi [xi' [p' [q' [[H511 H512] [[p [q [v [H521 [H522 H523]]]]] [H53 H54]]]]]]]. subst.
intros a r p'' H6.
(* use preserv of ren *)
assert (H6': step_out a r p'.[ren xi] p'') by auto.
apply step_out_preserv_ren in H6'.
destruct H6' as [p2'' [r2 [H61 [H62 H63]]]]. subst.
rename p2'' into p''. rename r2 into r.
apply step_out_substit with (sigma := ren (xi')) in H6.
asimpl in H6. rewrite H511 in H6. asimpl in H6.
(* r = r'.ren (+1) *)
assert (H7: exists r', r = r'.[ren (+1)]).
{ eapply var_then_out_step_impl_lifted_output.
- exact H522.
- eauto. }
destruct H7. subst. rename x0 into r.
(* reverse var and out transitions *)
pose (H7 := var_then_out_step_can_be_reversed).
specialize (H7 p v p' H522 a r p'' H6).
destruct H7 as [H71 H72].
(* q can do the same out transition *)
destruct (H32 p q H521 a r p''.[Var v/] H71) as [r' [q'' [H81 [H82 H83]]]].
(* combine q's var and out transition *)
pose (H9 := var_and_out_can_be_combined).
specialize (H9 q a r' q'' H81 v q' H523).
destruct H9 as [q2 [H91 H92]]. subst.
rename q2 into q''.
(* now we can proceed with the goal *)
exists r'.[ren (+1)].[ren xi], q''.[ren xi].
(* get variable step of q' *)
pose (H9 := var_then_out_step_can_be_reversed).
specialize (H9 q v q' H523 a r' q'' H91).
destruct H9 as [_ H102].
(* proceed with the goal *)
split; try split.
+ now apply step_out_substit.
+ left. exists xi, xi', p'', q''.
split. Focus 2. split.
* hnf. do 3 eexists. { repeat split.
- exact H82.
- eauto.
- eauto. }
* split; reflexivity.
* split; auto.
+ right. apply H1. asimpl.
exists ((+1) >>> xi), (xi' >>> minus_one).
do 2 eexists. split.
* apply decidable_inj_ren_comp_bij_ren_is_decidable_inj_ren.
exact shift_decidable_inj_ren.
split; auto.
* repeat split; auto.
- eapply s_ho_out_mono.
+ now apply H32.
+ repeat intro. now right.
Qed.
Lemma f_reach_cond_clos_for_s_ho_in:
CondClos s_ho_in
(increasify (bij_ren_clos °° f_reach))
decidable_inj_ren_clos
(const top2).
Proof.
intros x H1 _ H32 p'' q'' [H4 | H4].
- destruct H4 as [xi [xi' [p' [q' [[H411 H412] [[p [q [v [H421 [H422 H423]]]]] [H43 H44]]]]]]]. subst.
intros a p'' H5.
(* use preserv of ren *)
assert (H6: step_in a p'.[ren xi] p'') by auto.
apply step_in_preserv_ren in H6.
destruct H6 as [p2'' [H61 H62]]. subst.
rename p2'' into p''.
(* reverse var and in transitions *)
pose (H7 := var_then_in_step_can_be_reversed).
specialize (H7 p v p' H422 a p'').
pose (H71 := step_in_substit).
specialize (H71 (ren xi') a p'.[ren xi] p''.[up (ren xi)] H5).
asimpl in H71. specialize (H71 p''.[ren (upren (xi >>> xi'))]).
assert (H72: step_in a p'.[ren (xi >>> xi')] p''.[ren (upren (xi >>> xi'))]). apply H71. reflexivity. clear H71.
rewrite H411 in H72. asimpl in H72.
specialize (H7 H72). clear H72.
destruct H7 as [H71 H72].
(* q can do the same in transition *)
destruct (H32 p q H421 a p''.[up (Var v .: ids)] H71) as [q'' [H81 H82]].
(* combine q's var and in transition *)
pose (H9 := var_and_in_can_be_combined).
specialize (H9 q a q'' H81 v q' H423).
destruct H9 as [q2 [H91 H92]]. subst.
rename q2 into q''.
(* get variable step of q' *)
pose (H9 := var_then_in_step_can_be_reversed).
specialize (H9 q v q' H423 a q'' H91).
destruct H9 as [_ H102].
exists q''.[up (ren xi)]. split.
+ pose (H11 := step_in_substit).
specialize (H11 (ren xi) a q' q'' H91 q''.[up (ren xi)]).
apply H11. reflexivity.
+ left.
exists ((1 .: 0 .: (+2)) >>> (upren xi)).
exists (upren xi' >>> (1 .: 0 .: (+2))).
exists p''.[Var 1 .: Var 0 .: ren (+2)],
q''.[Var 1 .: Var 0 .: ren (+2)].
split.
* apply comp_preserv_bij_ren.
split; now asimpl.
apply upren_preserv_bij. split; auto.
* repeat split.
Focus 1. repeat eexists. exact H82. eauto. eauto.
Focus 1. now asimpl.
Focus 1. now asimpl.
- eapply s_ho_in_mono.
+ now apply H32.
+ repeat intro. now right.
Qed.
Lemma f_reach_cond_clos_for_s_var_multi:
CondClos s_var_multi
(increasify (bij_ren_clos °° f_reach))
decidable_inj_ren_clos
(const top2).
Proof.
intros x H1 _ H32 p'' q'' [H4 | H4].
- + destruct H4 as [xi [xi' [p' [q' [[H411 H412] [[p [q [n [H421 [H422 H423]]]]] [H43 H44]]]]]]]. subst.
specialize (H32 p q H421).
intros v.
assert (H52: step_var_cxt n p p') by auto.
assert (H62: step_var_cxt n q q') by auto.
apply contexts_decrease_var_occurrence in H422.
apply contexts_decrease_var_occurrence in H423.
destruct (nat_dec v (xi (S n))).
* inv e.
rewrite renaming_preserv_count
with (xi := xi) (sigma := ren xi') in H422.
Focus 2. apply bij_ren_is_decidable_inj_ren. split; auto.
rewrite renaming_preserv_count
with (xi := xi) (sigma := ren xi') in H423.
Focus 2. apply bij_ren_is_decidable_inj_ren. split; auto.
specialize (H32 n). omega.
* remember (xi' v) as z.
{destruct z.
- rewrite renaming_preserv_count
with (xi := xi') (sigma := ren xi).
Focus 2. apply bij_ren_is_decidable_inj_ren. split; auto.
asimpl. rewrite H411. asimpl.
remember (mult (count q'.[ren xi]) v) as z.
rewrite renaming_preserv_count
with (xi := xi') (sigma := ren xi) in Heqz0.
subst z.
Focus 2. apply bij_ren_is_decidable_inj_ren. split; auto.
rewrite <- Heqz.
asimpl. rewrite H411.
erewrite contexts_have_single_zero.
Focus 2. asimpl. eauto.
erewrite contexts_have_single_zero.
Focus 2. asimpl. eauto.
reflexivity.
- rename z into v'.
assert (H5: xi' v <> S n).
{
intros H5. apply n0.
rewrite <- H5.
assert (v = (xi' >>> xi) v).
rewrite H412. reflexivity.
now asimpl in H.
}
assert (H6: S v' <> S n).
{
intros H6.
apply H5.
rewrite <- H6. now rewrite Heqz.
}
assert (H7: v' <> n) by omega.
rewrite renaming_preserv_count
with (xi := xi') (sigma := ren xi).
remember (mult (count q'.[ren xi]) v) as z.
rewrite renaming_preserv_count
with (xi := xi') (sigma := ren xi) in Heqz0.
subst z.
Focus 2. apply bij_ren_is_decidable_inj_ren. split; auto.
Focus 2. apply bij_ren_is_decidable_inj_ren. split; auto.
asimpl. rewrite H411. asimpl.
rewrite <- Heqz.
do 2 (erewrite contexts_maintain_var_occurrence; eauto).
}
- eapply s_var_multi_mono.
+ now apply H32.
+ repeat intro. now right.
Qed.
Lemma nu_of_s_io_multi_sym_reach_closed:
congruence s_io_multi_sym f_reach.
Proof.
assert (H1: congruence s_io_multi_sym (increasify (bij_ren_clos °° f_reach))).
{
apply cond_clos_impl_congruence
with (g_lo := decidable_inj_ren_clos)
(g_up := const (top2)).
- apply symmetrize_fun_preserv_cond_clos_when_f_sym.
eapply intersect_fun_bin_preserv_cond_clos.
Unshelve.
+ eapply intersect_fun_bin_preserv_cond_clos.
Unshelve.
exact f_reach_cond_clos_for_s_ho_out.
exact f_reach_cond_clos_for_s_ho_in.
+ exact f_reach_cond_clos_for_s_var_multi.
- now repeat intro.
- apply s_io_multi_sym_closed_under_decidable_inj_ren.
}
intros p q H2. apply H1. left.
exists id, id. do 2 eexists. repeat split; eauto; now asimpl.
Qed.
Lemma nu_of_s_io_multi_sym_is_closed_under_s_var_cxt:
postfp s_var_cxt (nu s_io_multi_sym).
Proof.
intros p q [x [H11 H12]].
intros v p' H2.
destruct (H11 p q H12) as [[_ H13] _].
specialize (H13 v).
assert (H22 : step_var_cxt v p p') by auto.
apply step_then_unguarded_var in H22.
assert (H3: 1 <= mult (count q) v) by omega.
apply unguarded_var_then_step in H3.
destruct H3 as [q' H3].
eexists. split.
- eauto.
- apply nu_of_s_io_multi_sym_reach_closed.
hnf.
exists p, q, v. repeat split; auto. exists x; split; auto.
Qed.
Lemma io_multi_bis_subset_io_cxt_bis:
nu s_io_multi_sym <2= nu s_io_cxt_sym.
Proof.
intros p q [x [H1 H2]].
exists (nu s_io_multi_sym). split.
- clear H2 p q.
intros p q [x' [H21 H22]].
destruct (H21 p q H22) as [[[H31 H32] H33] [[H34 H365] H66]].
split.
+ repeat split.
* eapply s_ho_out_mono; eauto.
repeat intro. exists x'; auto.
* eapply s_ho_in_mono; eauto.
repeat intro. exists x'; auto.
* apply nu_of_s_io_multi_sym_is_closed_under_s_var_cxt.
exists x'. split; auto.
+ repeat split.
* eapply s_ho_out_mono; eauto.
repeat intro. exists x'; auto.
* eapply s_ho_in_mono; eauto.
repeat intro. exists x'; auto.
* { eapply s_var_cxt_mono.
- apply nu_of_s_io_multi_sym_is_closed_under_s_var_cxt.
exists (transp x'). split; auto.
repeat intro. apply symmetrize_fun_correct.
hnf. split; now apply H21.
- repeat intro.
apply sym_f_impl_sym_nu; auto.
apply symmetrize_fun_correct. }
- exists x. split; auto.
Qed.