Library HOC24PreCompleteness
Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC04DefLTS.
Require Import HOC05WFProcesses.
Require Import HOC06FreshLemmas.
Require Import HOC07SizeLemmas.
Require Import HOC08SubstLemmas.
Require Import HOC10CongrLemmas.
Require Import HOC11TransLemmas.
Require Import HOC13Bisimulations.
Require Import HOC14IObis.
Require Import HOC22Decidability.
Require Import HOC23PrimeDecomposition.
Require Program.Wf.
Require Import Relations.
Lemma wfp_sizeP_size : ∀ p, wfp_sizeP p ≤ wfp_size p.
Proof with automate.
induction p using (measure_induction wfp_size).
destruct_wf p; unfolds wfp_sizeP; unfolds wfp_size; simpls; try solve [nat_math].
+ specializes H p0...
+ specializes H p0... rewrite size_subst in *; auto.
rewrite¬ sizeP_subst...
+ lets H1 : H p1; lets¬ H2 : H p2...
Qed.
Lemma wfp_sizeP_swap : ∀ p X Y, wfp_sizeP (wfp_swap X Y p) = wfp_sizeP p.
Proof with automate.
induction p using (measure_induction wfp_size).
destruct_wf p; introv...
+ unfolds wfp_sizeP; simpls. rewrite H...
+ repeat rewrite wfp_sizeP_abs. rewrite H...
+ repeat cases_if×.
+ unfolds wfp_sizeP; simpls. repeat rewrite H...
Qed.
Fixpoint wfp_repeat (n : nat) (p : wfprocess) : list wfprocess :=
match n with
| 0 ⇒ nil
| S n ⇒ p :: wfp_repeat n p
end.
Lemma wfp_prod_repeat_SS : ∀ n p, (wfp_prod (wfp_repeat (S (S n)) p) = (wfp_Par p (wfp_prod (wfp_repeat (S n) p)))).
Proof.
inductions n; simpls¬.
Qed.
Lemma wfp_prod_repeat_subst : ∀ n p q X, n > 0 → wfp_subst q X (wfp_prod (wfp_repeat n p)) = wfp_prod (wfp_repeat n (wfp_subst q X p)).
Proof with automate.
inductions n; [nat_math | ].
destruct n; introv _. simpls¬.
repeat rewrite wfp_prod_repeat_SS... fequals.
apply IHn...
Qed.
Lemma wfp_subst_X_prod_repeat_Abs : ∀ n p a X q,
wfp_subst q X (wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))) =
(wfp_prod (wfp_repeat (S n) (wfp_Abs a X p))).
Proof.
inductions n.
simpl. intros. rewrite¬ wfp_eq_subst_abs1.
introv; rewrite wfp_prod_repeat_SS. rewrite_wfp_subst. fequals.
rewrite¬ wfp_eq_subst_abs1.
Qed.
Lemma wfp_prod_repeat_swap : ∀ n p X Y, wfp_swap X Y (wfp_prod (wfp_repeat n p)) = wfp_prod (wfp_repeat n (wfp_swap X Y p)).
Proof with automate.
inductions n; introv...
destruct n...
repeat rewrite wfp_prod_repeat_SS...
rewrite¬ IHn.
Qed.
Lemma IObis_wfcgr_nil_iff : ∀ p, p ≈ wfp_Nil ↔ p ≡* wfp_Nil.
Proof with automate.
introv; splits.
gen p. induction p using (measure_induction wfp_size); destruct_wf p; intro Hio.
apply IObis_sizeP_eq in Hio. false...
apply IObis_sizeP_eq in Hio. false...
apply IObis_sizeP_eq in Hio. false...
etransitivity. Focus 2. constructor. apply WfCgrPar_nil2.
apply IObis_sizeP_eq in Hio.
apply wfcgr_par; apply H; try rewrite <- wfp_sizeP_0_IO_nil in ×...
constructor×.
introv Hyp. applys¬ congr_IObis.
Qed.
Lemma wfcgr_nil_has_top_nil : ∀ p, p ≠ wfp_Nil → p ≡* wfp_Nil → has_top_nil p.
Proof with automate.
induction p using (measure_induction wfp_size); introv Hneq Hcgr.
destruct_wf p; simpl_has_top_nil; jauto; try congr_impossible.
clear Hneq.
tests : (p1 = wfp_Nil); tests : (p2 = wfp_Nil); simpl_has_top_nil; jauto.
left. apply H... assert (wfp_sizeP p1 = 0).
apply wfcgr_sizeP in Hcgr...
applys¬ wfp_sizeP_0_wfcgr_nil.
Qed.
Lemma wfcgr_send_par_has_nil : ∀ a p p1 p2, (wfp_Send a p ≡* wfp_Par p1 p2) → has_free_par_nil (wfp_Par p1 p2).
Proof.
introv Hio. apply has_top_has_free_nil. intro Heq; inverts Heq. apply congr_IObis in Hio.
apply prime_send in Hio. simpl_has_top_nil.
inverts Hio as Hio; apply IObis_wfcgr_nil_iff in Hio.
tests Heq : (p1 = wfp_Nil); simpl_has_top_nil; jauto.
left. applys¬ wfcgr_nil_has_top_nil.
tests Heq : (p2 = wfp_Nil); simpl_has_top_nil; jauto.
right. applys¬ wfcgr_nil_has_top_nil.
Qed.
Lemma wfcgr_gvar_par_has_nil : ∀ X p1 p2, (wfp_Gvar X ≡* wfp_Par p1 p2) → has_free_par_nil (wfp_Par p1 p2).
Proof.
introv Hio. apply has_top_has_free_nil. intro Heq; inverts Heq. apply congr_IObis in Hio.
apply prime_gvar in Hio. simpl_has_top_nil.
inverts Hio as Hio; apply IObis_wfcgr_nil_iff in Hio.
tests Heq : (p1 = wfp_Nil); simpl_has_top_nil; jauto.
left. applys¬ wfcgr_nil_has_top_nil.
tests Heq : (p2 = wfp_Nil); simpl_has_top_nil; jauto.
right. applys¬ wfcgr_nil_has_top_nil.
Qed.
Lemma wfcgr_abs_par_has_nil : ∀ a X p p1 p2, (wfp_Abs a X p ≡* wfp_Par p1 p2) → has_free_par_nil (wfp_Par p1 p2).
Proof with automate.
introv Hcgr.
lets Hyp_s : num_send_wfcgr Hcgr.
lets Hyp_a : num_abs_wfcgr Hcgr.
lets Hyp_v : num_var_wfcgr Hcgr.
destruct_wf p1; destruct_wf p2;
try solve [simpls; false; nat_math]; simpls; jauto.
+ do 3 right.
lets Hyp : (nil_process_char p3).
assert (num_var p3 = 0) by nat_math.
specializes Hyp H... inverts× Hyp.
+ do 2 right.
lets Hyp : (nil_process_char p3).
assert (num_var p3 = 0) by nat_math.
specializes Hyp H... inverts× Hyp.
+ do 2 right.
assert (num_var p1 = 0 ∧ num_var p3 = 0 ∧ num_var p4 = 0 ∧ num_var p5 = 0)
by nat_math.
assert (num_abs p1 = 0 ∨ num_abs p3 = 0 ∨ num_abs p4 = 0 ∨ num_abs p5 = 0)
by nat_math.
destruct H as (Hnv1 & Hnv3 & Hnv4 & Hnv5).
inverts H0.
lets Hyp : (nil_process_char p1). specializes Hyp Hnv1...
inverts× Hyp.
inverts H.
lets Hyp : (nil_process_char p3). specializes Hyp Hnv3...
inverts× Hyp.
inverts H0.
lets Hyp : (nil_process_char p4). specializes Hyp Hnv4...
inverts× Hyp.
lets Hyp : (nil_process_char p5). specializes Hyp Hnv5...
inverts× Hyp.
Qed.
Program Fixpoint remove_par_nils (p : wfprocess) {measure (wfp_size p)} :=
match p with
| mkWfP (Par p q) wfc ⇒
let wfp := mkWfP p (wf_par1 p q wfc) in
let wfq := mkWfP q (wf_par2 p q wfc) in
ifb (wfp_sizeP wfp = 0) then (remove_par_nils wfq)
else ifb (wfp_sizeP wfq = 0) then (remove_par_nils wfp)
else (wfp_Par (remove_par_nils wfp) (remove_par_nils wfq))
| mkWfP (Send a p´) wfc ⇒ (wfp_Send a (remove_par_nils (mkWfP p´ (wf_send a p´ wfc))))
| mkWfP (Receive a x p´) wfc ⇒ wfp_Abs a (fst (Abs_from_Receive a x p´ wfc nil))
(remove_par_nils (snd (Abs_from_Receive a x p´ wfc nil)))
| _ ⇒ p
end.
Next Obligation. solve_wfp_size. Qed.
Next Obligation. solve_wfp_size. Qed.
Next Obligation. solve_wfp_size. Qed.
Next Obligation. solve_wfp_size. Qed.
Next Obligation.
unfold wfp_size; simpl.
lets Hyp : Abs_from_Receive_spec a x p´.
specialize (Hyp wfc nil). destruct Hyp as (Hyp & _).
simpl in Hyp; unfold Abs in Hyp; inverts Hyp. rewrite H1 at 2.
rewrite¬ size_subst.
Qed.
Next Obligation. splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq. Qed.
Next Obligation. splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq. Qed.
Next Obligation. splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq. Qed.
Lemma remove_par_nils_eq : ∀ p, remove_par_nils p =
match p with
| mkWfP (Par p q) wfc ⇒
let wfp := mkWfP p (wf_par1 p q wfc) in
let wfq := mkWfP q (wf_par2 p q wfc) in
ifb (wfp_sizeP wfp = 0) then (remove_par_nils wfq)
else ifb (wfp_sizeP wfq = 0) then (remove_par_nils wfp)
else (wfp_Par (remove_par_nils wfp) (remove_par_nils wfq))
| mkWfP (Send a p´) wfc ⇒ (wfp_Send a (remove_par_nils (mkWfP p´ (wf_send a p´ wfc))))
| mkWfP (Receive a x p´) wfc ⇒ wfp_Abs a (fst (Abs_from_Receive a x p´ wfc nil))
(remove_par_nils (snd (Abs_from_Receive a x p´ wfc nil)))
| _ ⇒ p
end.
Proof.
intros.
unfold remove_par_nils at 1. rewrite Wf.Fix_eq.
destruct p; simpl.
destruct proc; try solve [simpls*].
clear p; intros.
destruct x; simpl.
inductions proc; simpl; try solve [repeat rewrite H; intuition; repeat fequals].
destruct proc1; destruct proc2;
repeat cases_if*; try solve [false; solve_wfp_sizeP]; repeat fequals.
Qed.
Lemma remove_par_nils_eq_send : ∀ a p,
remove_par_nils (wfp_Send a p) = wfp_Send a (remove_par_nils p).
Proof.
introv; rewrite remove_par_nils_eq; simpls¬.
repeat fequals. rewrite_wfp_equal.
Qed.
Lemma remove_par_nils_eq_gvar : ∀ X,
remove_par_nils (wfp_Gvar X) = wfp_Gvar X.
Proof.
introv; rewrite remove_par_nils_eq; simpls¬.
Qed.
Lemma remove_par_nils_eq_nil : remove_par_nils (wfp_Nil) = wfp_Nil.
Proof.
introv; rewrite remove_par_nils_eq; simpls¬.
Qed.
Lemma remove_par_nils_eq_par : ∀ p q,
remove_par_nils (wfp_Par p q) =
ifb (wfp_sizeP p = 0) then (remove_par_nils q)
else ifb (wfp_sizeP q = 0) then (remove_par_nils p)
else (wfp_Par (remove_par_nils p) (remove_par_nils q)).
Proof.
introv; rewrite remove_par_nils_eq; simpls; repeat cases_if*;
repeat fequals; rewrite_wfp_equal.
Qed.
Lemma remove_par_nils_fresh : ∀ (p : wfprocess) X, X # p ↔ X # remove_par_nils p.
Proof with solve_wfp_size.
induction p using (measure_induction wfp_size).
destruct_wf p; introv; splits; introv Hyp;
repeat rewrite remove_par_nils_eq_send in *;
repeat rewrite remove_par_nils_eq_gvar in *;
repeat rewrite remove_par_nils_eq_par in *;
repeat rewrite remove_par_nils_eq_nil in *; jauto.
+ simpl; rewrite gfresh_send.
rewrite <- H... fresh_solve.
+ simpl; rewrite gfresh_send.
rewrite H... fresh_solve.
+ rewrite remove_par_nils_eq.
lets H_cond : WfAbs a X p0 (wf_cond p0). unfolds Abs.
assert (Heq_abs : wfp_Abs a X p0 = wfp_Abs a (fst
(Abs_from_Receive a (f X p0) ([Lvar (f X p0) // X]p0)
(WfAbs a X p0 (wf_cond p0)) nil)) (snd
(Abs_from_Receive a (f X p0) ([Lvar (f X p0) // X]p0)
(WfAbs a X p0 (wf_cond p0)) nil))).
lets (Heq & _) : (Abs_from_Receive_spec a (f X p0) ([Lvar (f X p0) // X]p0) H_cond (@nil process)). rewrite_wfp_equal.
rewrite Heq_abs in Hyp.
rewrite wfp_gfresh_Abs in Hyp. simpls.
remember (fst
(Abs_from_Receive a (f X p0) ([Lvar (f X p0) // X]p0)
(WfAbs a X p0 (wf_cond p0)) nil)) as Y.
remember (snd
(Abs_from_Receive a (f X p0) ([Lvar (f X p0) // X]p0)
(WfAbs a X p0 (wf_cond p0)) nil)) as q.
replace (Abs f a Y (remove_par_nils q)) with (proc (wfp_Abs a Y (remove_par_nils q))).
rewrite wfp_gfresh_Abs; inverts Hyp; jauto. rewrite H in H0. jauto.
rewrite Heq_abs... simpls¬.
+ rewrite remove_par_nils_eq in Hyp.
lets H_cond : WfAbs a X p0 (wf_cond p0). unfolds Abs.
assert (Heq_abs : wfp_Abs a X p0 = wfp_Abs a (fst
(Abs_from_Receive a (f X p0) ([Lvar (f X p0) // X]p0)
(WfAbs a X p0 (wf_cond p0)) nil)) (snd
(Abs_from_Receive a (f X p0) ([Lvar (f X p0) // X]p0)
(WfAbs a X p0 (wf_cond p0)) nil))).
lets (Heq & _) : (Abs_from_Receive_spec a (f X p0) ([Lvar (f X p0) // X]p0) H_cond (@nil process)). rewrite_wfp_equal.
rewrite Heq_abs.
remember (fst
(Abs_from_Receive a (f X p0) ([Lvar (f X p0) // X]p0)
(WfAbs a X p0 (wf_cond p0)) nil)) as Y.
remember (snd
(Abs_from_Receive a (f X p0) ([Lvar (f X p0) // X]p0)
(WfAbs a X p0 (wf_cond p0)) nil)) as q.
simpl in Hyp. rewrite <- HeqY in Hyp. rewrite <- Heqq in Hyp.
clear HeqY Heqq.
replace (Abs f a Y (remove_par_nils q)) with (proc (wfp_Abs a Y (remove_par_nils q))) in Hyp.
rewrite wfp_gfresh_Abs in ×. inverts× Hyp. right.
rewrite H... auto. rewrite Heq_abs... simpls¬.
+ simpls; rewrite gfresh_par_iff in Hyp. repeat cases_if×.
- rewrite <- H... jauto.
- rewrite <- H... jauto.
- simpl; rewrite gfresh_par_iff. splits; rewrite <- H... jauto. jauto.
+ repeat cases_if*; simpl; rewrite gfresh_par_iff; splits; try solve [rewrite H; try solve_wfp_size; jauto]; rewrite wfp_sizeP_0_wfcgr_nil in ×.
- eapply wfcgr_fresh. symmetry; eassumption. fresh_solve.
- eapply wfcgr_fresh. symmetry; eassumption. fresh_solve.
- simpls; rewrite gfresh_par_iff in Hyp. rewrite H... jauto.
- simpls; rewrite gfresh_par_iff in Hyp. rewrite H... jauto.
Qed.
Lemma remove_par_nils_swap : ∀ p X Y,
remove_par_nils (wfp_swap X Y p) = wfp_swap X Y (remove_par_nils p).
Proof with automate.
induction p using (measure_induction wfp_size).
introv; destruct_wf p.
+ repeat (rewrite remove_par_nils_eq_send; rewrite_wfp_swap). fequals.
apply H...
+ rewrite_wfp_swap. rename p0 into p. do 2 rewrite remove_par_nils_eq; simpls.
rename X0 into Z; rename X into X0; rename Z into X.
lets Hyp1 : (Abs_from_Receive_spec a (f X p) ([Lvar (f X p) // X]p) (WfAbs a X p (wf_cond p)) nil).
lets Hyp2 : (Abs_from_Receive_spec a (f ({{X0, Y}}X) ({{[X0, Y]}} p))
([Lvar (f ({{X0, Y}}X) ({{[X0, Y]}} p)) // {{X0, Y}}X]({{[X0, Y]}} p))
(WfAbs a ({{X0, Y}}X) ({{[X0, Y]}} p)
(wf_swapping p X0 Y (wf_cond p))) nil).
destruct Hyp1 as (Hyp1 & _); destruct Hyp2 as (Hyp2 & _).
remember (fst
(Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p)
(WfAbs a X p (wf_cond p)) nil)) as Z1.
remember (snd
(Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p)
(WfAbs a X p (wf_cond p)) nil)) as q1.
remember (fst (Abs_from_Receive a (f ({{X0, Y}}X) ({{[X0, Y]}} p))
([Lvar (f ({{X0, Y}}X) ({{[X0, Y]}} p)) // {{X0, Y}}X]({{[X0, Y]}} p))
(WfAbs a ({{X0, Y}}X) ({{[X0, Y]}} p)
(wf_swapping p X0 Y (wf_cond p))) nil)) as Z2.
remember (snd (Abs_from_Receive a (f ({{X0, Y}}X) ({{[X0, Y]}} p))
([Lvar (f ({{X0, Y}}X) ({{[X0, Y]}} p)) // {{X0, Y}}X]({{[X0, Y]}} p))
(WfAbs a ({{X0, Y}}X) ({{[X0, Y]}} p)
(wf_swapping p X0 Y (wf_cond p))) nil)) as q2.
clear HeqZ1 HeqZ2 Heqq1 Heqq2.
lets Hwf1 : wf_cond (wfp_Abs a Z1 q1). rewrite <- Hyp1 in Hwf1.
lets Hwf2 : wf_cond (wfp_Abs a Z2 q2). rewrite <- Hyp2 in Hwf2.
lets (Z & Hfz) : find_fresh (proc p :: (Gvar Y) :: (Gvar X0) :: (Gvar X) :: nil);
rewrite Forall_to_conj_4 in Hfz. destruct Hfz as (Hfz1 & Hfz2 & Hfz3 & Hfz4).
apply wf_receive with (X := Z) in Hwf1; try fresh_solve.
apply wf_receive with (X := Z) in Hwf2.
Focus 2. fresh_solve. assert (Z = {{X0, Y}}Z).
unfold swap_gvar; repeat cases_if; subst; fresh_solve;
rewrite gfresh_gvar in *; false×.
rewrite H0. applys¬ gfresh_swap_inv.
rewrite <- subst_decomposition_l in *; try apply f_is_good; try apply¬ wf_lfresh.
Focus 2. apply wf_swapping. apply wf_cond.
destruct Hwf1 as (Hwf1 & Heq1); destruct Hwf2 as (Hwf2 & Heq2).
rewrite Heq1 in Hyp1; rewrite Heq2 in Hyp2; clear Heq1 Heq2 Hwf1 Hwf2.
assert (Abs f a Z ([Gvar Z // X]p) = wfp_Abs a ({{X, Z}}X) (wfp_swap X Z p)).
simpl; fequals. unfolds swap_gvar; repeat cases_if×.
rewrite× gfresh_subst_is_swap. rewrite H0 in Hyp1. clear H0.
assert (Abs f a Z ([Gvar Z // {{X0, Y}}X]({{[X0, Y]}} p)) = wfp_Abs a ({{({{X0, Y}}X), Z}}({{X0, Y}}X)) (wfp_swap ({{X0, Y}}X) Z (wfp_swap X0 Y p))).
simpl; fequals. unfolds swap_gvar; repeat cases_if×.
rewrite× gfresh_subst_is_swap.
assert (Z = {{X0, Y}}Z).
unfold swap_gvar; repeat cases_if; subst; fresh_solve;
rewrite gfresh_gvar in *; false×.
rewrite H0. applys¬ gfresh_swap_inv.
rewrite H0 in Hyp2. clear H0.
rewrite <- (wfp_eq_swap_abs p a X Z X) in Hyp1.
rewrite <- wfp_gfresh_subst_is_swap in Hyp1.
Focus 2. rewrite× wfp_gfresh_Abs.
rewrite wfp_eq_subst_abs1 in Hyp1.
rewrite <- wfp_eq_swap_abs in Hyp2.
rewrite <- wfp_gfresh_subst_is_swap in Hyp2.
Focus 2. rewrite× wfp_gfresh_Abs. right.
simpl. assert (Z = {{X0, Y}}Z).
unfold swap_gvar; repeat cases_if; subst; fresh_solve;
rewrite gfresh_gvar in *; false×.
rewrite H0. applys¬ gfresh_swap_inv.
rewrite wfp_eq_subst_abs1 in Hyp2.
rewrite <- wfp_eq_swap_abs in Hyp2.
rewrite <- wfprocess_eq in ×. rewrite Hyp1 in ×.
clear dependent Z. clear dependent p. clear X. rename X0 into X.
automate. lets Hyp3 : Hyp2; rewrite wfp_Abs_equal in Hyp2.
destruct Hyp2 as (_ & Hyp). cases_if×.
rewrite <- Hyp. subst Z2. rewrite H...
remember ({{X, Y}}Z1) as T. clear HeqT.
destruct Hyp as (Hyp & HfT).
rewrite wfp_gfresh_subst_is_swap in Hyp; auto.
replace q2 with (wfp_swap Z2 T (wfp_swap X Y q1)).
Focus 2. rewrite <- (wfp_swap_involutive Z2 T). fequals.
lets Hyp1 : H (wfp_swap X Y q1) Z2 T...
unfolds wfp_size. simpls. rewrite size_swap. rewrite¬ size_subst...
rewrite Hyp1. rewrite H...
symmetry in Hyp3. rewrite wfp_Abs_equal in Hyp3.
destruct Hyp3 as (_ & Hyp3). cases_if×.
rewrite wfp_Abs_equal; splits×. cases_if×.
assert (Z2 # wfp_swap X Y (remove_par_nils q1)).
rewrite <- H... rewrite× <- remove_par_nils_fresh.
splits×. remember (wfp_swap X Y (remove_par_nils q1)) as p; clear Heqp.
rewrite¬ wfp_gfresh_subst_is_swap. rewrite¬ wfp_swap_sym.
+ repeat (rewrite remove_par_nils_eq_gvar; rewrite_wfp_swap).
repeat cases_if×.
+ repeat (rewrite remove_par_nils_eq_par; rewrite_wfp_swap).
repeat cases_if*; try solve [unfolds wfp_sizeP; simpls;
rewrite sizeP_swap in *; nat_math]; try solve [rewrite¬ H; automate].
rewrite_wfp_swap. fequals; apply H...
+ repeat (rewrite remove_par_nils_eq_nil; rewrite_wfp_swap; auto).
Qed.
Lemma remove_par_nils_eq_abs : ∀ a X p,
remove_par_nils (wfp_Abs a X p) = wfp_Abs a X (remove_par_nils p).
Proof.
introv; rewrite remove_par_nils_eq; simpls¬.
lets H : WfAbs a X p (wf_cond p). unfolds Abs.
assert (Heq_abs : wfp_Abs a X p = wfp_Abs a (fst
(Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p)
(WfAbs a X p (wf_cond p)) nil)) (snd
(Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p)
(WfAbs a X p (wf_cond p)) nil))).
lets (Heq & _) : (Abs_from_Receive_spec a (f X p) ([Lvar (f X p) // X]p) H (@nil process)). rewrite_wfp_equal; simpls¬.
lets Heq : Heq_abs. rewrite wfp_Abs_equal in Heq; destruct Heq as (_ & Heq); cases_if×.
rewrite <- e. rewrite¬ <- Heq.
clear H.
remember (fst
(Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p)
(WfAbs a X p (wf_cond p)) nil)) as Y.
remember (snd
(Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p)
(WfAbs a X p (wf_cond p)) nil)) as q.
clear HeqY Heqq.
destruct Heq as (Heq & Hf).
rewrite wfp_gfresh_subst_is_swap in Heq; auto. subst.
rewrite remove_par_nils_swap.
assert (Hff : Y # wfp_swap Y X (remove_par_nils q)).
rewrite <- wfp_gfresh_subst_is_swap. simpls; fresh_solve.
rewrite¬ <- remove_par_nils_fresh.
rewrite wfp_Abs_equal; splits×. cases_if×. splits×.
rewrite¬ wfp_gfresh_subst_is_swap.
rewrite wfp_swap_sym. rewrite¬ wfp_swap_involutive.
Qed.
Ltac simpl_remove_par_nils := repeat
(repeat rewrite remove_par_nils_eq_send in *;
repeat rewrite remove_par_nils_eq_abs in *;
repeat rewrite remove_par_nils_eq_gvar in *;
repeat rewrite remove_par_nils_eq_nil in *;
repeat rewrite remove_par_nils_eq_par in *).
Lemma remove_par_nils_sizeP_0 : ∀ p,
wfp_sizeP p = 0 ↔ remove_par_nils p = wfp_Nil.
Proof with automate.
induction p using (measure_induction wfp_size).
destruct_wf p; simpl_remove_par_nils; splits; introv Hyp;
try solve [false*; automate]; jauto.
assert (wfp_sizeP p1 = 0 ∧ wfp_sizeP p2 = 0) by automate.
cases_if×. rewrite <- H...
repeat cases_if×... rewrite <- H in Hyp...
rewrite <- H in Hyp...
Qed.
Lemma remove_nil_no_par_nil : ∀ p, ¬ has_free_par_nil (remove_par_nils p).
Proof.
induction p using (measure_induction wfp_size).
destruct_wf p; simpl_remove_par_nils; try rewrite has_free_par_nil_abs; simpls*;
try solve [eapply H; solve_wfp_size].
repeat cases_if; try apply H; solve_wfp_size.
simpls; rew_logic; splits*; try solve [eapply H; solve_wfp_size];
rewrite remove_par_nils_sizeP_0 in *; subst_wfp; rewrite¬ <- wfprocess_eq.
Qed.
Lemma remove_nil_wfcgr_step : ∀ p q, p ≡ q → remove_par_nils p ≡ remove_par_nils q.
Proof with automate.
induction p using (measure_induction wfp_size).
destruct_wf p; introv Hcgr.
+ inverts Hcgr...
- simpl_remove_par_nils. constructor. apply H...
- simpl_remove_par_nils; repeat cases_if×...
+ inverts Hcgr. rename p0 into q; rename X into Y; rename X0 into X.
assert (wfp_Abs a X p = wfp_Abs a Y q).
rewrite_wfp_equal; simpls. unfolds Abs.
rewrite H3. rewrite¬ H2. clear H2 H3.
rewrite <- H0 in ×. simpl_remove_par_nils. constructor. apply H...
simpl_remove_par_nils; repeat cases_if×... reflexivity.
+ inverts Hcgr...
simpl_remove_par_nils; repeat cases_if×...
+ inverts Hcgr...
- assert (wfp_sizeP p1 = wfp_sizeP p´).
apply (t_step wfprocess wfcgr_step) in H2. apply wfcgr_sizeP in H2...
assert (wfp_sizeP p2 = wfp_sizeP q´).
apply (t_step wfprocess wfcgr_step) in H4. apply wfcgr_sizeP in H4...
simpl_remove_par_nils; repeat cases_if*; try solve [apply H; automate].
constructor; apply H...
- remember (wfp_Par p1 p2) as q. simpl_remove_par_nils; repeat cases_if×...
apply remove_par_nils_sizeP_0 in e. rewrite e. reflexivity.
- simpl_remove_par_nils; repeat cases_if×.
apply remove_par_nils_sizeP_0 in e. rewrite e. reflexivity.
- simpl_remove_par_nils; repeat cases_if×...
apply remove_par_nils_sizeP_0 in e; apply remove_par_nils_sizeP_0 in e0.
rewrite e, e0. reflexivity.
- assert (p2 = wfp_Par q0 r) by rewrite_wfp_equal. subst. clear H2.
simpl_remove_par_nils; repeat cases_if×...
- assert (p1 = wfp_Par p q0) by rewrite_wfp_equal. subst. clear H1.
simpl_remove_par_nils; repeat cases_if×...
+ apply (t_step wfprocess wfcgr_step) in Hcgr. apply wfcgr_sizeP in Hcgr...
symmetry in Hcgr. eapply remove_par_nils_sizeP_0 in Hcgr. rewrite Hcgr.
simpl_remove_par_nils; auto.
Qed.
Lemma remove_nil_wfcgr : ∀ p q, p ≡* q → remove_par_nils p ≡* remove_par_nils q.
Proof.
introv Hc. inductions Hc...
+ constructor. applys¬ remove_nil_wfcgr_step.
+ etransitivity; eassumption.
Qed.
Lemma remove_par_nils_wfcgr : ∀ p, p ≡* remove_par_nils p.
Proof with automate.
induction p using (measure_induction wfp_size).
destruct_wf p; simpl_remove_par_nils; try reflexivity.
+ apply wfcgr_send. apply H...
+ apply wfcgr_abs. apply H...
+ repeat cases_if×.
- etransitivity. apply wfcgr_par. instantiate (1 := wfp_Nil).
applys¬ wfp_sizeP_0_wfcgr_nil. apply H...
etransitivity. apply wfcgr_par_com. apply wfcgr_nil_r.
- etransitivity. apply wfcgr_par. apply H...
instantiate (1 := wfp_Nil). applys¬ wfp_sizeP_0_wfcgr_nil.
apply wfcgr_nil_r.
- apply wfcgr_par; apply H...
Qed.
Lemma remove_par_nils_sizeP : ∀ p, wfp_sizeP p = wfp_sizeP (remove_par_nils p).
Proof.
introv. applys (wfcgr_sizeP _ _ (remove_par_nils_wfcgr p)).
Qed.
Lemma remove_par_nils_wfp_prod_repeat_abs : ∀ n a X p, remove_par_nils (wfp_prod (wfp_repeat n (wfp_Abs a X p))) = wfp_prod (wfp_repeat n (wfp_Abs a X (remove_par_nils p))).
Proof with automate.
induction n using (lt_wf_ind); destruct n; introv.
+ simpls. simpl_remove_par_nils. reflexivity.
+ destruct n. simpls. simpl_remove_par_nils. reflexivity.
repeat rewrite wfp_prod_repeat_SS. simpl_remove_par_nils.
cases_if×. automate. clear n0. cases_if×. false.
destruct n; simpls; automate. clear n0.
fequals. apply H...
Qed.
Lemma remove_par_nils_size : ∀ p, wfp_size (remove_par_nils p) ≤ wfp_size p.
Proof with automate.
induction p using (measure_induction wfp_size).
destruct_wf p; simpl_remove_par_nils...
specializes H p0...
assert (wfp_size p0 < wfp_size (wfp_Abs a X p0)) by automate.
simpl_sizes.
specializes H H0...
lets Hp1 : H p1. lets Hp2 : H p2.
repeat cases_if×...
Qed.
Lemma wfcgr_size_remove_nil : ∀ p q, p ≡* q → wfp_size (remove_par_nils p) = wfp_size (remove_par_nils q).
Proof with automate.
introv Hc. inductions Hc...
inductions H; simpl_remove_par_nils.
+ unfolds wfp_size. simpls...
+ repeat rewrite wfp_size_Abs in ×...
+ apply (t_step wfprocess wfcgr_step) in H. apply wfcgr_sizeP in H.
apply (t_step wfprocess wfcgr_step) in H0. apply wfcgr_sizeP in H0.
repeat cases_if×. unfolds wfp_size. simpls...
+ repeat cases_if×. apply remove_par_nils_sizeP_0 in e. rewrite¬ e.
+ repeat cases_if×. apply remove_par_nils_sizeP_0 in e. rewrite¬ e.
+ repeat cases_if×... rewrite remove_par_nils_sizeP_0 in e, e0. rewrite e, e0; auto.
+ repeat cases_if×...
+ repeat cases_if×...
+ auto.
Qed.
Lemma core_remove_nil_invariant : ∀ p, Core p = None → Core (remove_par_nils p) = None.
Proof.
induction p using (measure_induction wfp_size).
destruct_wf p; simpl_remove_par_nils; simpl_core;
introv Hyp; try solve [inverts Hyp]; auto.
repeat cases_if*; try solve [applys H; automate].
clear n n0 Hyp. lets H1 : remove_par_nils_sizeP p1.
lets H2 : remove_par_nils_sizeP p2.
simpl_core; repeat cases_if×...
Qed.
Lemma core_none_char : ∀ p,
wfp_sizeP p > 0 → Core p = None →
∃ p1 p2, remove_par_nils p = wfp_Par p1 p2 ∧
wfp_sizeP p1 > 0 ∧ wfp_sizeP p2 > 0 ∧
¬ has_free_par_nil p1 ∧ ¬ has_free_par_nil p2.
Proof with automate.
introv Hs Hcp.
lets Hcrp : core_remove_nil_invariant Hcp.
remember (remove_par_nils p) as r. destruct_wf r;
try rewrite Hyp in *; simpl_core; try solve [inverts Hcrp].
Focus 2. false.
lets Hs´ : remove_par_nils_sizeP p. rewrite H in ×...
lets Hn : remove_nil_no_par_nil p. rewrite Hyp in Hn.
simpls; rew_logic in Hn... repeat rewrite <- wfprocess_eq in ×.
∃ p1 p2. splits×.
destruct Hn as (H1 & _ & H2 & _). clear dependent p2. gen H1 H2. clear.
induction p1 using (measure_induction wfp_size).
destruct_wf p1; introv Hneq Hnf...
clear Hneq. simpls... rewrite <- wfprocess_eq in ×. rew_logic in ×.
destruct Hnf as (Hp0 & Hp2 & Hfp0 & Hfp2).
lets¬ H0 : H Hfp0... false...
destruct Hn as (_ & H1 & _ & H2). clear dependent p1. gen H1 H2. clear.
induction p2 using (measure_induction wfp_size).
destruct_wf p2; introv Hneq Hnf...
clear Hneq. simpls... rewrite <- wfprocess_eq in ×. rew_logic in ×.
destruct Hnf as (Hp1 & Hp0 & Hfp1 & Hfp0).
lets¬ H0 : H Hfp1... false...
Qed.
Lemma core_remove_par_nils : ∀ p p´,
Core p = Some p´ → remove_par_nils p = remove_par_nils p´.
Proof with automate.
induction p using (measure_induction wfp_size).
destruct_wf p; introv Hc; simpl_core; try solve [inverts¬ Hc].
simpl_remove_par_nils. repeat cases_if*; apply H...
Qed.
Program Fixpoint dpd (p : wfprocess) {measure (wfp_size p)} : Prop :=
match p with
| mkWfP (Send a p) wfc ⇒
let wfp := mkWfP p (wf_send a p wfc) in
dpd wfp
| mkWfP (Receive a x p´) wfc ⇒
prime p ∧
dpd (snd (Abs_from_Receive a x p´ wfc nil))
| mkWfP (Gvar X) wfc ⇒ True
| mkWfP (Par p q) wfc ⇒
let wfp := mkWfP p (wf_par1 p q wfc) in
let wfq := mkWfP q (wf_par2 p q wfc) in
wfp_sizeP wfp > 0 ∧ wfp_sizeP wfq > 0 ∧ dpd wfp ∧ dpd wfq
| _ ⇒ True
end.
Next Obligation.
unfold wfp_size; simpl.
lets Hyp : Abs_from_Receive_spec a x p´.
specialize (Hyp wfc nil). destruct Hyp as (Hyp & _).
simpl in Hyp; unfold Abs in Hyp; inverts Hyp. rewrite H1 at 2.
rewrite¬ size_subst.
Qed.
Next Obligation.
unfold wfp_size; simpl; nat_math.
Qed.
Next Obligation.
unfold wfp_size; simpl; nat_math.
Qed.
Next Obligation.
splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Lemma dpd_eq : ∀ p, dpd p =
match p with
| mkWfP (Send a p) wfc ⇒
let wfp := mkWfP p (wf_send a p wfc) in
dpd wfp
| mkWfP (Receive a x p´) wfc ⇒ prime p ∧ dpd (snd (Abs_from_Receive a x p´ wfc nil))
| mkWfP (Gvar X) wfc ⇒ True
| mkWfP (Par p q) wfc ⇒
let wfp := mkWfP p (wf_par1 p q wfc) in
let wfq := mkWfP q (wf_par2 p q wfc) in
wfp_sizeP wfp > 0 ∧ wfp_sizeP wfq > 0 ∧ dpd wfp ∧ dpd wfq
| _ ⇒ True
end.
Proof.
intros.
unfold dpd at 1. rewrite Wf.Fix_eq.
destruct p; simpl.
destruct proc; try solve [simpls*].
clear p; intros.
destruct x; simpl.
destruct proc; simpl; try solve [repeat rewrite H; intuition]; repeat fequals.
Qed.
Lemma dpd_eq_send : ∀ p a, dpd (wfp_Send a p) = dpd p.
Proof.
introv. rewrite dpd_eq; simpl. fequals. rewrite_wfp_equal.
Qed.
Lemma dpd_eq_gvar : ∀ X, dpd (wfp_Gvar X) = True.
Proof.
introv. rewrite dpd_eq; simpls¬.
Qed.
Lemma dpd_eq_par : ∀ p q, dpd (wfp_Par p q) = (wfp_sizeP p > 0 ∧ wfp_sizeP q > 0 ∧ dpd p ∧ dpd q).
Proof.
introv. rewrite dpd_eq; simpls.
assert (Hp : p = mkWfP p (wf_par1 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hp.
assert (Hq : q = mkWfP q (wf_par2 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hq.
Qed.
Lemma dpd_eq_nil : dpd wfp_Nil = True.
Proof.
introv. rewrite dpd_eq; simpls¬.
Qed.
Lemma prime_gswap : ∀ (p : wfprocess) X Y,
prime p = prime (wfp_swap X Y p).
Proof with automate.
introv; apply prop_ext; splits; intros (Hn & Hp); unfolds prime; splits...
rewrite <- wfp_sizeP_0_IO_nil in *; unfolds wfp_sizeP.
simpls; rewrite sizeP_swap...
Focus 2.
rewrite <- wfp_sizeP_0_IO_nil in *; unfolds wfp_sizeP.
simpls; rewrite sizeP_swap in ×...
Focus 2.
introv Hio.
apply IObis_swap with (X := X) (Y := Y) in Hio...
specializes Hp Hio; inverts Hp as Hp.
rewrite <- wfp_sizeP_0_IO_nil in *; unfolds wfp_sizeP.
simpls; rewrite sizeP_swap in ×...
repeat rewrite <- wfp_sizeP_0_IO_nil in *; unfolds wfp_sizeP.
simpls; rewrite sizeP_swap in ×...
introv Hio.
apply IObis_swap with (X := X) (Y := Y) in Hio...
rewrite wfp_swap_involutive in Hio.
specializes Hp Hio; inverts Hp as Hp; [left | right].
rewrite <- wfp_sizeP_0_IO_nil in *; unfolds wfp_sizeP.
simpls; rewrite sizeP_swap in ×...
repeat rewrite <- wfp_sizeP_0_IO_nil in *; unfolds wfp_sizeP.
simpls; rewrite sizeP_swap in ×...
Qed.
Lemma dpd_gswap : ∀ (p : wfprocess) X Y,
(dpd p = dpd (wfp_swap X Y p)).
Proof with automate.
induction p using (measure_induction wfp_size).
destruct_wf p; introv.
automate. do 2 rewrite dpd_eq_send. apply H...
Focus 2. automate.
repeat cases_if×.
Focus 2.
repeat rewrite dpd_eq_par; simpls... rewrite dpd_eq_par.
repeat rewrite wfp_sizeP_swap.
fequals. fequals. fequals; applys H...
Focus 2. automate.
automate. do 2 rewrite dpd_eq; simpl; fequals.
lets Hyp : prime_gswap (wfp_Abs a X p0) X0 Y. rewrite Hyp...
assert (Hyp_AfR : ∀ a X p wfc, wfp_Abs a X p = wfp_Abs a
(fst (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p) wfc nil))
(snd (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p) wfc nil))).
clear. introv. rewrite_wfp_equal; unfolds Abs.
lets Hyp : Abs_from_Receive_spec a (f X p) ([Lvar (f X p) // X]p).
specialize (Hyp wfc (@nil process)). destruct Hyp as (Hyp & _).
inverts Hyp; auto.
lets Hpr1 : (WfAbs a X p0 (wf_cond p0)). unfolds Abs.
lets Hyp1 : Hyp_AfR a X p0. specialize (Hyp1 Hpr1).
lets Hpr2 : (WfAbs a ({{X0, Y}}X) ({{[X0, Y]}} p0) (wf_swapping p0 X0 Y (wf_cond p0))). unfolds Abs.
lets Hyp2 : Hyp_AfR a ({{X0, Y}}X) (wfp_swap X0 Y p0).
specialize (Hyp2 Hpr2).
symmetry in Hyp1, Hyp2.
rewrite wfp_Abs_equal in Hyp1, Hyp2.
destruct Hyp1 as (_ & Hyp1); destruct Hyp2 as (_ & Hyp2); repeat cases_if*;
simpls; try rewrite Hyp1; try rewrite Hyp2.
apply H...
destruct Hyp1 as (Hyp1 & Hf1). rewrite Hyp1.
rewrite¬ wfp_gfresh_subst_is_swap. etransitivity.
symmetry. apply H... apply H...
destruct Hyp2 as (Hyp2 & Hf2). rewrite Hyp2.
rewrite¬ wfp_gfresh_subst_is_swap. etransitivity.
Focus 2. apply H. unfolds wfp_size; simpls.
rewrite size_swap. rewrite size_subst...
apply H...
destruct Hyp1 as (Hyp1 & Hf1). rewrite Hyp1.
rewrite¬ wfp_gfresh_subst_is_swap.
destruct Hyp2 as (Hyp2 & Hf2). rewrite Hyp2.
rewrite¬ wfp_gfresh_subst_is_swap.
etransitivity. symmetry. apply H...
etransitivity. Focus 2. apply H. unfolds wfp_size; simpls.
rewrite size_swap. rewrite size_subst...
apply H...
Qed.
Lemma dpd_eq_abs : ∀ p a X, dpd (wfp_Abs a X p) = (prime (wfp_Abs a X p) ∧ dpd p).
Proof.
introv. rewrite dpd_eq; simpl.
lets Hyp : Abs_from_Receive_spec a (f X p) ([Lvar (f X p) // X]p).
lets Hwf : WfAbs a X p (wf_cond p); unfolds Abs; specialize (Hyp Hwf (@nil process)).
remember (fst (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p) Hwf nil)) as Y.
remember (snd (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p) Hwf nil)) as p´.
destruct Hyp as (Hyp & _). assert (Heq : wfp_Abs a X p = wfp_Abs a Y p´) by rewrite_wfp_equal.
assert (snd (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p) (WfAbs a X p (wf_cond p)) nil) = p´).
subst p´. fequals.
rewrite H. cut (dpd p´ = dpd p). intro Heq´; rewrite¬ Heq´. clear HeqY Heqp´ H.
rewrite wfp_Abs_equal in Heq; destruct Heq as (_ & Heq); cases_if×. rewrite¬ Heq.
destruct Heq as (Heq & Hfx); subst p.
rewrite¬ wfp_gfresh_subst_is_swap. apply dpd_gswap.
Qed.
Ltac simpl_dpd := repeat
(repeat rewrite dpd_eq_send in *;
repeat rewrite dpd_eq_abs in *;
repeat rewrite dpd_eq_gvar in *;
repeat rewrite dpd_eq_par in *;
repeat rewrite dpd_eq_nil in *).
Definition deep_prime_decomposition (p : wfprocess) (dp : wfprocess) :=
p ≈ dp ∧ dpd dp.
Program Fixpoint components (p : wfprocess) {measure (wfp_size p)} : list wfprocess :=
match p with
| mkWfP (Par p q) wfc ⇒
let wfp := mkWfP p (wf_par1 p q wfc) in
let wfq := mkWfP q (wf_par2 p q wfc) in
components wfp ++ components wfq
| mkWfP Nil wfc ⇒ (@nil wfprocess)
| _ ⇒ (p :: nil)
end.
Next Obligation.
automate.
Qed.
Next Obligation.
automate.
Qed.
Next Obligation.
splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Next Obligation.
splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq.
Qed.
Lemma components_eq : ∀ p, components p =
match p with
| mkWfP (Par p q) wfc ⇒
let wfp := mkWfP p (wf_par1 p q wfc) in
let wfq := mkWfP q (wf_par2 p q wfc) in
components wfp ++ components wfq
| mkWfP Nil wfc ⇒ (@nil wfprocess)
| _ ⇒ (p :: nil)
end.
Proof.
intros.
unfold components at 1. rewrite Wf.Fix_eq.
destruct p; simpl.
destruct proc; try solve [simpls*].
clear p; intros.
destruct x; simpl.
destruct proc; simpl; try solve [repeat rewrite H; intuition]; repeat fequals.
Qed.
Lemma components_eq_send : ∀ p a, components (wfp_Send a p) = (wfp_Send a p :: nil).
Proof.
introv. rewrite components_eq; simpls¬.
Qed.
Lemma components_eq_abs : ∀ p a X, components (wfp_Abs a X p) = (wfp_Abs a X p :: nil).
Proof.
introv. rewrite components_eq; simpls¬.
Qed.
Lemma components_eq_gvar : ∀ X, components (wfp_Gvar X) = (wfp_Gvar X :: nil).
Proof.
introv. rewrite components_eq; simpls¬.
Qed.
Lemma components_eq_par : ∀ p q, components (wfp_Par p q) = components p ++ components q.
Proof.
introv. rewrite components_eq; simpls.
assert (Hp : p = mkWfP p (wf_par1 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hp.
assert (Hq : q = mkWfP q (wf_par2 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hq.
Qed.
Lemma components_eq_nil : components wfp_Nil = nil.
Proof.
introv. rewrite components_eq; simpls¬.
Qed.
Ltac simpl_components := repeat
(repeat rewrite components_eq_send in *;
repeat rewrite components_eq_abs in *;
repeat rewrite components_eq_gvar in *;
repeat rewrite components_eq_par in *;
repeat rewrite components_eq_nil in *).
Lemma wfp_prod_components_lr : ∀ p,
p ≈ wfp_prod (components p).
Proof with automate.
induction p using (measure_induction wfp_size).
destruct_wf p; simpl_components; simpls¬.
lets Hyp : wfp_prod_IO_app (components p1) (components p2).
etransitivity. Focus 2. symmetry. eassumption. apply IObis_congr_par; apply H...
Qed.
Lemma prime_in_dpd : ∀ dp,
dpd dp → (Forall (fun p ⇒ prime p) (components dp)).
Proof with (try apply Forall_nil; automate).
introv Hyp; induction dp using (measure_induction wfp_size).
destruct_wf dp; simpl_components; simpl_dpd...
constructor... apply prime_send.
constructor...
constructor... apply prime_gvar.
apply Forall_app. applys× H... applys× H...
Qed.
Lemma dpd_implies_pd : ∀ p dp,
deep_prime_decomposition p dp →
prime_decomposition p (components dp).
Proof with (try solve [repeat constructor*]; automate).
introv (Hio & Hdp).
splits. etransitivity. eassumption. apply wfp_prod_components_lr.
applys× prime_in_dpd.
Qed.
Lemma prime_characterization : ∀ p, prime p →
((∃ a p´, p ≈ wfp_Send a p´) ∨
(∃ X, p ≈ wfp_Gvar X) ∨
(∃ a X p´, p ≈ wfp_Abs a X p´)).
Proof with automate.
induction p using (measure_induction wfp_size).
destruct_wf p; introv Hprime.
branch 1. eexists. eexists. reflexivity.
Focus 2. branch 2. eexists. reflexivity.
Focus 3. false. applys¬ not_prime_nil.
Focus 2. rewrite prime_parallel in Hprime; inverts Hprime; destruct H0 as (H0 & H1).
specializes H H0...
inverts H; [branch 1 | inverts H2; [branch 2 | branch 3]].
destruct H2 as (a & p´ & Hyp). ∃ a p´.
etransitivity. apply IObis_congr_par; eassumption.
∃ wfcgr; splits. apply congr_IObisimulation.
repeat constructor.
destruct H as (X & Hyp). ∃ X.
etransitivity. apply IObis_congr_par; eassumption.
∃ wfcgr; splits. apply congr_IObisimulation.
repeat constructor.
destruct H as (a & X & p´ & Hyp). ∃ a X p´.
etransitivity. apply IObis_congr_par; eassumption.
∃ wfcgr; splits. apply congr_IObisimulation.
repeat constructor.
specializes H H0...
inverts H; [branch 1 | inverts H2; [branch 2 | branch 3]].
destruct H2 as (a & p´ & Hyp). ∃ a p´.
etransitivity. apply IObis_congr_par; eassumption.
etransitivity. apply IObis_congr_par_com.
∃ wfcgr; splits. apply congr_IObisimulation.
repeat constructor.
destruct H as (X & Hyp). ∃ X.
etransitivity. apply IObis_congr_par; eassumption.
etransitivity. apply IObis_congr_par_com.
∃ wfcgr; splits. apply congr_IObisimulation.
repeat constructor.
destruct H as (a & X & p´ & Hyp). ∃ a X p´.
etransitivity. apply IObis_congr_par; eassumption.
etransitivity. apply IObis_congr_par_com.
∃ wfcgr; splits. apply congr_IObisimulation.
repeat constructor.
clear H. branch 3. rename p0 into p.
∃¬ a X p.
Qed.
Lemma deep_prime_decomposition_exists :
∀ p, ∃ dp, deep_prime_decomposition p dp.
Proof with automate.
induction p using (measure_induction wfp_sizeP).
elim (classic (prime p)); introv Hpr. Focus 2.
unfold prime in Hpr. rew_logic in Hpr. inverts Hpr as Hpr.
∃ wfp_Nil; splits×. simpl_dpd. auto.
destruct Hpr as (p1 & Hpr). rew_logic in Hpr.
destruct Hpr as (p2 & Hpr). rew_logic in Hpr.
destruct Hpr as (Hio & Hnp1 & Hnp2).
lets Hsize : IObis_sizeP_eq Hio.
rewrite <- wfp_sizeP_0_IO_nil in ×.
lets (dp1 & Hdp1) : H p1...
lets (dp2 & Hdp2) : H p2...
inverts¬ Hdp1. inverts¬ Hdp2.
∃ (wfp_Par dp1 dp2); simpl_dpd. splits.
etransitivity. eassumption. applys× IObis_congr_par.
simpl_dpd; splits*; solve_wfp_sizeP.
apply IObis_sizeP_eq in H0. nat_math.
apply IObis_sizeP_eq in H2. nat_math.
lets Hyp : prime_characterization Hpr.
inverts Hyp as Hyp.
destruct Hyp as (a & p´ & Hio).
lets (dp´ & Hdp´) : H p´. apply IObis_sizeP_eq in Hio...
inverts Hdp´. ∃ (wfp_Send a dp´). splits×.
etransitivity. apply Hio. applys× IObis_congr_send.
simpl_dpd; auto.
inverts Hyp as Hyp.
destruct Hyp as (X & Hio).
∃ (wfp_Gvar X); splits×. simpl_dpd; auto.
destruct Hyp as (a & X & p´ & Hio).
lets (dp´ & Hdp´) : H p´. apply IObis_sizeP_eq in Hio.
rewrite Hio... inverts Hdp´.
∃ (wfp_Abs a X dp´). splits×.
etransitivity. eassumption. applys× IObis_congr_abs.
simpl_dpd; splits×. eapply prime_IO.
Focus 2. apply IObis_congr_abs. eassumption.
eapply prime_IO; eassumption.
Qed.
Lemma deep_prime_decomposition_unique : ∀ p dp1 dp2,
deep_prime_decomposition p dp1 → deep_prime_decomposition p dp2 →
∃ lp1´ lp2´, permut (components dp1) lp1´ ∧
permut (components dp2) lp2´ ∧ IO_pointwise lp1´ lp2´.
Proof.
introv Hd1 Hd2.
apply dpd_implies_pd in Hd1; apply dpd_implies_pd in Hd2.
lets Hyp : prime_decomposition_unique Hd1 Hd2. auto.
Qed.
Lemma dpd_remove_nil_congr : ∀ p, dpd (remove_par_nils p) →
∀ q, p ≡* q → dpd (remove_par_nils q).
Proof with automate.
introv Hp Hcgr. inductions Hcgr; jauto.
inductions H; simpl_remove_par_nils; simpl_dpd; jauto.
+ splits×.
eapply prime_IO. apply Hp. apply IObis_congr_abs.
apply congr_IObis. apply remove_nil_wfcgr. constructor¬.
+ assert (Hsp : wfp_sizeP p = wfp_sizeP p´).
apply wfcgr_sizeP. constructor¬.
assert (Hsq : wfp_sizeP q = wfp_sizeP q´).
apply wfcgr_sizeP. constructor¬.
repeat cases_if*; try solve [false; nat_math].
simpl_dpd. destruct Hp as (Hp & Hq & Hdrp & Hdrq). splits×.
- apply remove_nil_wfcgr_step in H.
apply (t_step wfprocess wfcgr_step) in H. apply wfcgr_sizeP in H...
- apply remove_nil_wfcgr_step in H0.
apply (t_step wfprocess wfcgr_step) in H0. apply wfcgr_sizeP in H0...
+ repeat cases_if×. simpl_dpd; auto.
+ repeat cases_if×.
rewrite remove_par_nils_sizeP_0 in e. rewrite¬ e.
+ repeat cases_if×...
- rewrite remove_par_nils_sizeP_0 in ×. rewrite¬ e0. simpl_dpd; auto.
- simpl_dpd. splits×.
+ repeat cases_if×...
simpl_dpd. simpl_sizes. splits×. nat_math.
+ repeat cases_if×...
simpl_dpd. simpl_sizes. splits×. nat_math.
Qed.
Lemma dpd_equiv_par_nil : ∀ p, dpd p ↔ (¬ has_free_par_nil p ∧ dpd (remove_par_nils p)).
Proof with automate.
induction p using (measure_induction wfp_size).
destruct_wf p; splits; introv Hyp; simpl_dpd; auto.
+ simpl_remove_par_nils. specializes H p0.
simpl; splits×. applys× H... simpl_dpd. applys× H...
+ rewrite H; solve_wfp_size. splits×.
inverts Hyp. simpl_remove_par_nils. simpl_dpd. auto.
+ specializes H p0. rewrite has_free_par_nil_abs.
simpl_remove_par_nils. simpl_dpd.
inverts Hyp. rewrite H in H1; solve_wfp_size. inverts H1. splits×.
unfolds prime. inverts H0. splits. introv Hyp.
apply IObis_sizeP_eq in Hyp. automate.
introv Hio. apply H4. etransitivity. Focus 2. eassumption.
apply IObis_congr_abs. apply congr_IObis. apply remove_par_nils_wfcgr.
+ inverts Hyp. rewrite has_free_par_nil_abs in H0.
simpl_remove_par_nils. simpl_dpd. inverts H1. splits×.
unfolds prime. inverts H2. splits. introv Hyp.
apply IObis_sizeP_eq in Hyp. automate.
introv Hio. apply H4. etransitivity. Focus 2. eassumption.
apply IObis_congr_abs. apply congr_IObis. symmetry. apply remove_par_nils_wfcgr.
rewrite× H...
+ destruct Hyp as (Hs1 & Hs2 & Hd1 & Hd2).
rewrite H in Hd1... rewrite H in Hd2...
splits×. simpls. rew_logic; splits*; subst_wfp; rewrite¬ <- wfprocess_eq.
introv Heq; subst... introv Heq; subst...
simpl_remove_par_nils. repeat cases_if×...
simpl_dpd. splits*; rewrite remove_par_nils_sizeP in n, n0...
+ inverts Hyp. simpls; rew_logic in ×... destruct H0 as (Hp1 & Hp2 & Hfp1 & Hfp2);
rewrite <- wfprocess_eq in ×. simpl_remove_par_nils; repeat cases_if×.
false; apply Hfp1. applys¬ has_top_has_free_nil.
clear Hfp1. clear dependent p2. induction p1 using (measure_induction wfp_size).
destruct_wf p1; try solve [false; automate].
tests : (p0 = wfp_Nil); simpl_has_top_nil; jauto.
left. applys H...
false; apply Hfp2. applys¬ has_top_has_free_nil.
clear Hfp2. clear dependent p1. induction p2 using (measure_induction wfp_size).
destruct_wf p2; try solve [false; automate].
tests : (p0 = wfp_Nil); simpl_has_top_nil; jauto.
right. applys H... splits; solve_wfp_sizeP.
simpl_dpd. rewrite H... simpl_dpd. rewrite H...
Qed.
Lemma dpd_congr_invariant : ∀ p q, p ≡* q → dpd p → ¬ has_free_par_nil q → dpd q.
Proof.
introv Hc Hnp Hnfq.
rewrite dpd_equiv_par_nil in *; splits¬.
apply dpd_remove_nil_congr in Hc; jauto.
Qed.
Lemma dpd_components_prime : ∀ dp, dpd dp →
(Forall (fun p : wfprocess ⇒ prime p) (components dp)).
Proof with automate.
induction dp using (measure_induction wfp_size); destruct_wf dp;
simpl_components; introv Hdp; simpl_dpd; try solve [do 2 constructor*].
constructor. apply prime_send. constructor.
constructor. apply prime_gvar. constructor.
apply Forall_app; applys× H...
Qed.
Lemma dpd_remove_par_nils : ∀ dp, dpd dp → ¬ has_free_par_nil dp.
Proof with automate.
induction dp using (measure_induction wfp_size).
destruct_wf dp; introv Hd; simpl_dpd; simpls; jauto.
+ applys× H...
+ rewrite <- has_free_par_nil_lsubst. applys× H...
+ rew_logic; subst_wfp; repeat rewrite <- wfprocess_eq. splits×.
- introv Heq. subst. false; solve_wfp_sizeP.
- introv Heq. subst. false; solve_wfp_sizeP.
- applys× H...
- applys× H...
Qed.
Lemma trans_rem_wfcgr : ∀ q X q´, {{q -- LabRem X ->> AP q´}} →
∃ p´, q ≡* wfp_Par (wfp_Gvar X) p´ ∧ ¬ has_free_par_nil p´.
Proof.
introv Ht; inductions Ht.
∃ wfp_Nil. repeat constructor×.
destruct ap; inverts x.
lets¬ (p´ & Hcgrp´ & Hfpn) : IHHt w.
∃ (remove_par_nils (wfp_Par p´ q)). splits.
etransitivity. apply wfcgr_par. eassumption. apply remove_par_nils_wfcgr.
etransitivity. apply wfcgr_par_assoc_r.
apply wfcgr_par. reflexivity. simpl_remove_par_nils.
repeat cases_if×. apply wfp_sizeP_0_wfcgr_nil in e.
etransitivity. Focus 2. apply wfcgr_nil_r.
etransitivity. apply wfcgr_par_com. applys¬ wfcgr_par. reflexivity.
etransitivity. Focus 2. apply wfcgr_nil_r.
applys¬ wfcgr_par. apply remove_par_nils_wfcgr.
apply wfp_sizeP_0_wfcgr_nil. rewrite¬ <- remove_par_nils_sizeP.
apply wfcgr_par. apply remove_par_nils_wfcgr. reflexivity.
apply remove_nil_no_par_nil.
destruct aq; inverts x.
lets¬ (p´ & Hcgrp´ & Hfpn) : IHHt w.
∃ (remove_par_nils (wfp_Par p p´)). splits.
etransitivity. apply wfcgr_par. Focus 2. eassumption. apply remove_par_nils_wfcgr.
etransitivity. apply wfcgr_par_com. etransitivity. apply wfcgr_par_assoc_r.
apply wfcgr_par. reflexivity. simpl_remove_par_nils.
repeat cases_if×. rewrite remove_par_nils_sizeP in e.
apply wfp_sizeP_0_wfcgr_nil in e.
etransitivity. Focus 2. apply wfcgr_nil_r.
applys¬ wfcgr_par. apply remove_par_nils_wfcgr.
apply wfp_sizeP_0_wfcgr_nil in e.
etransitivity. apply wfcgr_par_com. etransitivity. applys¬ wfcgr_par.
symmetry. apply remove_par_nils_wfcgr. eassumption.
etransitivity. apply wfcgr_nil_r. apply remove_par_nils_wfcgr.
etransitivity. apply wfcgr_par_com.
apply wfcgr_par. reflexivity. apply remove_par_nils_wfcgr.
apply remove_nil_no_par_nil.
Qed.
Lemma trans_out_wfcgr : ∀ q q´ q´´ a, {{q -- LabOut a q´´ ->> AP q´}} →
∃ p´, q ≡* wfp_Par (wfp_Send a (remove_par_nils q´´)) p´ ∧ ¬ has_free_par_nil p´.
Proof.
introv Ht; inductions Ht.
∃ wfp_Nil. splits×.
etransitivity. Focus 2. apply wfcgr_nil_l.
apply wfcgr_send. apply remove_par_nils_wfcgr.
destruct ap; inverts x.
lets¬ (p´ & Hcgrp´ & Hfpn) : IHHt w.
∃ (remove_par_nils (wfp_Par p´ q)). splits.
etransitivity. apply wfcgr_par. eassumption. apply remove_par_nils_wfcgr.
etransitivity. apply wfcgr_par_assoc_r.
apply wfcgr_par. reflexivity. simpl_remove_par_nils.
repeat cases_if×. apply wfp_sizeP_0_wfcgr_nil in e.
etransitivity. Focus 2. apply wfcgr_nil_r.
etransitivity. apply wfcgr_par_com. applys¬ wfcgr_par. reflexivity.
etransitivity. Focus 2. apply wfcgr_nil_r.
applys¬ wfcgr_par. apply remove_par_nils_wfcgr.
apply wfp_sizeP_0_wfcgr_nil. rewrite¬ <- remove_par_nils_sizeP.
apply wfcgr_par. apply remove_par_nils_wfcgr. reflexivity.
apply remove_nil_no_par_nil.
destruct aq; inverts x.
lets¬ (p´ & Hcgrp´ & Hfpn) : IHHt w.
∃ (remove_par_nils (wfp_Par p p´)). splits.
etransitivity. apply wfcgr_par. Focus 2. eassumption. apply remove_par_nils_wfcgr.
etransitivity. apply wfcgr_par_com. etransitivity. apply wfcgr_par_assoc_r.
apply wfcgr_par. reflexivity. simpl_remove_par_nils.
repeat cases_if×. rewrite remove_par_nils_sizeP in e.
apply wfp_sizeP_0_wfcgr_nil in e.
etransitivity. Focus 2. apply wfcgr_nil_r.
applys¬ wfcgr_par. apply remove_par_nils_wfcgr.
apply wfp_sizeP_0_wfcgr_nil in e.
etransitivity. apply wfcgr_par_com. etransitivity. applys¬ wfcgr_par.
symmetry. apply remove_par_nils_wfcgr. eassumption.
etransitivity. apply wfcgr_nil_r. apply remove_par_nils_wfcgr.
etransitivity. apply wfcgr_par_com.
apply wfcgr_par. reflexivity. apply remove_par_nils_wfcgr.
apply remove_nil_no_par_nil.
Qed.