Library HOC23PrimeDecomposition
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 HOC18ONORbis.
Require Import HOC22Decidability.
Require Import Relations.
Require Import Program.Wf.
Inductive RCancel (n : nat) : binary wfprocess :=
| RCMain : ∀ p q, (∃ r, wfp_sizeP p + wfp_sizeP q + wfp_sizeP r ≤ n ∧ wfp_Par p r ≈ wfp_Par q r) → RCancel n p q.
Lemma IO_ex_IO_RCancel : ∀ n, (IO_bisimulation_ex (RCancel n) ↔ IO_bisimulation (RCancel n)).
Proof.
introv; apply IObisim_ex_IObisim_when_swap.
introv Hr; inverts Hr as (r & Hsr & Hbispar).
constructor; ∃ (wfp_swap X Y r); split.
unfold wfp_sizeP in *; simpls.
repeat rewrite¬ sizeP_swap.
clear Hsr; ∃ R_swap; splits.
apply R_swap_IObis.
repeat rewrite <- wfp_eq_swap_par.
constructor¬.
Qed.
Lemma RCancel_step_forward : ∀ p q n, RCancel n p q → ∀ n´, n´ > n → RCancel n´ p q.
Proof.
introv Hr; inverts Hr as (r & Hsr & Hbis).
introv Hgt; constructor.
∃ r; splits~; nat_math.
Qed.
Hint Resolve RCMain.
Lemma RCancel_IObis : ∀ n,
IO_bisimulation (RCancel n) ∧
(∀ (p q r r´ : wfprocess) X, wfp_sizeP p + wfp_sizeP q + wfp_sizeP r ≤ n →
{{r -- LabRem X ->> AP r´}} → (wfp_Par p r) ≈ (wfp_Par q r´) →
∃ (q´ : wfprocess), {{q -- LabRem X ->> AP q´}} ∧ RCancel n p q´) ∧
(∀ (p p´ p´´ q r r´ r´´ : wfprocess) a,
wfp_sizeP p´ + wfp_sizeP q + wfp_sizeP r ≤ n →
{{p -- LabOut a p´´ ->> AP p´}} → {{r -- LabOut a r´´ ->> AP r´}} → (wfp_Par p´ r) ≈ (wfp_Par q r´) →
∃ (q´ q´´ : wfprocess), {{q -- LabOut a q´´ ->> AP q´}} ∧ RCancel n p´ q´ ∧ RCancel n r´´ q´´) ∧
(∀ (p q r : wfprocess) fp fr a X
(Hp : {{p -- LabIn a ->> AA fp}})
(Hr : {{r -- LabIn a ->> AA fr}}),
wfp_sizeP p + wfp_sizeP q + wfp_sizeP r ≤ n + 1 →
wfp_Par (wfp_inst_Abs fp (wfp_Gvar X)) r ≈ wfp_Par q (wfp_inst_Abs fr (wfp_Gvar X)) →
∃ fq, ∃ (Hq : {{q -- LabIn a ->> AA fq}}),
RCancel n (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X))).
Proof with automate.
intro n; apply (lt_wf_ind n); rewrite <- lt_peano; clear.
assert (Haux : ∀ fp X r, wfp_Par (wfp_inst_Abs fp (wfp_Gvar X)) r = wfp_inst_Abs (AbsPar1 fp r) (wfp_Gvar X)) by (introv; auto).
introv Hyp; splits.
rewrite <- IO_ex_IO_RCancel; splits.
introv Hxy; inverts Hxy as (r & Hs & Hbis).
constructor; ∃ r; splits~; nat_math.
introv Hr Ht; inverts Hr as (r & Hs & Hbis).
assert (Htpar : {{wfp_Par p r -- LabIn a ->> AA (AbsPar1 fp r)}}).
introv...
lets (fq & Htrq & Hrq´) : (IObis_in_full _ _ Hbis _ _ Htpar).
inverts Htrq...
rename fq into fq´. destruct ap; inverts H3... rename a0 into fq.
lets (X & Hfx) : find_fresh (proc p :: proc q :: proc r :: nil).
rewrite Forall_to_conj_3 in Hfx.
∃ fq; splits~; ∃ X; splits×.
constructor; ∃ r; splits.
unfold wfp_sizeP in *; simpls.
assert (Hsaux : sizeP (wfp_Gvar X) = 1) by auto.
lets Hsize1 : sizeP_in Hsaux Ht; lets Hsize2 : sizeP_in Hsaux H2; nat_math.
repeat rewrite Haux.
apply Hrq´; simpl; rewrite× gfresh_par_iff; splits¬.
destruct aq; inverts H3... rename a0 into fr.
elim (zerop n); introv Hneq; subst.
false; assert (Hsp : ¬ (wfp_sizeP r > 0)) by nat_math.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 2. ∃¬ a fr.
assert (Hlt : n - 1 < n) by nat_math.
specializes Hyp Hlt; destruct Hyp as (Hio & _ & _ & Hin); clear Hlt.
lets (X & Hfx) : find_fresh (proc p :: proc q :: proc r :: nil);
rewrite Forall_to_conj_3 in Hfx; destruct Hfx as (Hfxp & Hfxq & Hfxr).
specialize (Hin _ q _ _ _ _ X Ht H2).
assert (Hrq´´ : wfp_Par (wfp_inst_Abs fp (wfp_Gvar X)) r ≈ wfp_Par q (wfp_inst_Abs fr (wfp_Gvar X))).
introv; specialize (Hrq´ X); simpls.
specializes¬ Hin Hrq´.
replace (n - 1 + 1) with n by nat_math; auto.
specializes¬ Hin Hrq´´.
replace (n - 1 + 1) with n by nat_math; auto.
destruct Hin as (fq & Hq & Hin).
∃ fq; splits~; ∃ X; splits×. eapply RCancel_step_forward.
eapply Hin.
nat_math.
introv Hr Ht. inverts Hr as (r & Hs & Hbis).
assert (Htpar : {{wfp_Par p r -- LabOut a p´´ ->> AP (wfp_Par p´ r)}}). introv...
lets (q1 & q2 & Htrq & Hrq1 & Hrq2) : IObis_out Hbis Htpar.
inverts Htrq...
destruct ap; inverts H3.
∃ w q2; splits¬.
constructor; ∃ r; splits¬.
lets Hsize1 : sizeP_out Ht; lets Hsize2 : sizeP_out H2.
unfold wfp_sizeP in *; nat_math.
constructor; ∃ wfp_Nil; splits.
lets Hsize1 : sizeP_out Ht; lets Hsize2 : sizeP_out H2;
unfold wfp_sizeP in *; simpl; nat_math.
applys¬ IObis_congr_par1.
rename q2 into r´´.
destruct aq; inverts H3.
cut (∃ q´ q´´ : wfprocess, {{q -- LabOut a q´´ ->> AP q´}} ∧ RCancel (n-1) p´ q´ ∧ RCancel (n-1) p´´ q´´).
introv (q´ & q´´ & Htq & Hrq´ & Hrq´´); ∃ q´ q´´; splits~;
elim (zerop n); introv H; subst; simpls~; eapply RCancel_step_forward.
exact Hrq´. nat_math. exact Hrq´´. nat_math.
cut (∃ q´ q´´ : wfprocess, {{q -- LabOut a q´´ ->> AP q´}} ∧ RCancel (n-1) p´ q´ ∧ RCancel (n-1) r´´ q´´).
introv (q´ & q´´ & Htq & Hrq´ & Hrq´´); ∃ q´ q´´; splits¬.
assert (r´´ ≈ q´´). ∃ (RCancel (n-1)); splits~; eapply Hyp.
elim (zerop n); introv H; subst; simpl; [false | nat_math].
assert (Hsp : ¬ (wfp_sizeP r > 0)) by nat_math.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 3. ∃¬ a w r´´.
constructor; ∃ wfp_Nil; splits.
lets Hsize1 : sizeP_out Ht; lets Hsize2 : sizeP_out Htq;
unfold wfp_sizeP in *; simpl; nat_math.
applys¬ IObis_congr_par1. etransitivity; eassumption.
eapply Hyp; jauto.
Focus 2. lets Hsize1 : sizeP_out Ht; lets Hsize2 : sizeP_out H2.
unfold wfp_sizeP in *; nat_math.
elim (zerop n); introv H; subst; simpl; [false | nat_math].
assert (Hsp : ¬ (wfp_sizeP r > 0)) by nat_math.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 3. ∃¬ a w r´´.
introv Hr Ht; inverts Hr as (r & Hs & Hbis).
assert (Htpar : {{wfp_Par p r -- LabRem X ->> AP (wfp_Par p´ r)}}). introv...
lets (q´´ & Htqr & Hr´) : IObis_var Hbis Htpar.
inverts Htqr...
destruct ap; inverts H3...
∃ w; splits¬.
constructor; ∃ r; splits¬.
lets Hsize1 : sizeP_remove Ht; lets Hsize2 : sizeP_remove H2;
unfold wfp_sizeP in *; nat_math.
destruct aq; inverts H3...
cut (∃ q´ : wfprocess, {{q -- LabRem X ->> AP q´}} ∧ RCancel (n-1) p´ q´).
introv (q´ & Htq & Hrq); ∃ q´; splits¬.
elim (zerop n); introv H; subst; simpls¬.
eapply RCancel_step_forward. exact Hrq. nat_math.
eapply Hyp. Focus 4. exact Hr´. Focus 3. auto.
Focus 2. lets Hh : sizeP_remove Ht; unfold wfp_sizeP in *; nat_math.
elim (zerop n); introv H; subst; simpl; [false | nat_math].
assert (Hsp : ¬ (wfp_sizeP p > 0)) by nat_math.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 1. ∃¬ X p´.
introv Hs Htr Hparbis.
assert (Htpar : {{wfp_Par p r -- LabRem X ->> AP (wfp_Par p r´)}}) by automate.
lets (q´´ & Htqr & Hr´) : IObis_var Hparbis Htpar.
inverts Htqr...
destruct ap; inverts H3.
∃ w; splits¬.
constructor; ∃ r´; splits¬.
lets Hsq : sizeP_remove H2; lets Hsr : sizeP_remove Htr.
unfold wfp_sizeP in *; nat_math.
destruct aq; inverts H3.
cut (∃ q´ : wfprocess, {{q -- LabRem X ->> AP q´}} ∧ RCancel (n-1) p q´).
introv (q´ & Htq & Hrq); ∃ q´; splits¬.
elim (zerop n); introv H; subst; simpls¬.
eapply RCancel_step_forward. exact Hrq. nat_math.
eapply Hyp. Focus 3. exact H2. Focus 3. auto.
Focus 2. lets Hsize1 : sizeP_remove Htr; lets Hsize2 : sizeP_remove H2.
unfold wfp_sizeP in *; nat_math.
elim (zerop n); introv H; subst; simpl; [false | nat_math].
assert (Hsp : ¬ (wfp_sizeP r > 0)) by nat_math.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 1. ∃¬ X r´.
introv Hs Htp Htr Hparbis.
assert (Htpar : {{wfp_Par p´ r -- LabOut a r´´ ->> AP (wfp_Par p´ r´)}}) by automate.
lets (q1 & q´´ & Htrq & Hrq´ & Hrq´´) : IObis_out Hparbis Htpar.
inverts Htrq...
destruct ap; inverts H3.
∃ w q´´; splits¬.
constructor; ∃ r´; splits¬.
lets Hsize1 : sizeP_out Htr; lets Hsize2 : sizeP_out H2.
unfold wfp_sizeP in *; nat_math.
assert (Hbis´ : p´ ≈ w).
∃ (RCancel (n-1)); splits.
eapply Hyp. elim (zerop n); introv H; subst; simpl; [false | nat_math].
assert (Hsp : ¬ (wfp_sizeP q > 0)) by nat_math.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 3. ∃¬ a w q´´.
constructor. ∃ r´; splits¬.
lets Hsize1 : sizeP_out H2; lets Hsize2 : sizeP_out Htr.
unfold wfp_sizeP in *; nat_math.
constructor; ∃ wfp_Nil; splits.
lets Hsize1 : sizeP_out H2; lets Hsize2 : sizeP_out Htr;
unfold wfp_sizeP in *; simpl; nat_math.
applys¬ IObis_congr_par1.
destruct aq; inverts H3.
rename w into r1´; rename q´´ into r1´´; rename r´ into r1.
cut (∃ q´ q´´ : wfprocess, {{q -- LabOut a q´´ ->> AP q´}} ∧ RCancel (n-1) p´ q´ ∧ RCancel (n-1) r1´´ q´´).
introv (q1 & q2 & Htq & Hrq1 & Hrq2); ∃ q1 q2; splits¬.
apply RCancel_step_forward with (n := n-1); auto.
elim (zerop n); introv H; subst; simpl; [false | nat_math].
assert (Hsp : ¬ (wfp_sizeP r > 0)) by nat_math.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 3. ∃¬ a r1 r´´.
assert (Hbis´ : r1´´ ≈ q2).
∃ (RCancel (n-1)); splits¬.
eapply Hyp. elim (zerop n); introv H; subst; simpl; [false | nat_math].
assert (Hsp : ¬ (wfp_sizeP q > 0)) by nat_math.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 3. ∃¬ a q1 q2.
constructor; ∃ wfp_Nil; splits.
lets Hsize1 : sizeP_out H2; lets Hsize2 : sizeP_out Htq; lets Hsize3 : sizeP_out Htr;
unfold wfp_sizeP in *; simpl; nat_math.
applys¬ IObis_congr_par1. etransitivity; eassumption.
eapply Hyp; jauto.
Focus 2. lets Hsize1 : sizeP_out Htr; lets Hsize2 : sizeP_out H2.
unfold wfp_sizeP in *; nat_math.
elim (zerop n); introv H; subst; simpl; [false | nat_math].
assert (Hsp : ¬ (wfp_sizeP r > 0)) by nat_math.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 3. ∃¬ a r1 r´´.
introv Ht Hr Hs Hparbis.
assert (Htpar : {{wfp_Par (wfp_inst_Abs fp (wfp_Gvar X)) r -- LabIn a ->> AA (AbsPar2 (wfp_inst_Abs fp (wfp_Gvar X)) fr)}}) by automate.
lets (fpar & Htpar´ & Hf) : (IObis_in_full _ _ Hparbis _ _ Htpar).
specializes Hf X. simpls.
inverts Htpar´...
destruct ap; inverts H3; rename a0 into fq.
∃ fq H2; simpls.
elim (zerop n); introv Hneq; subst.
false; assert (Hsp : ¬ (wfp_sizeP p > 0) ∨ ¬ (wfp_sizeP q > 0)) by nat_math.
inverts Hsp as Hsp.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 2. ∃¬ a fp.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 2. ∃¬ a fq.
apply RCancel_step_forward with (n := n-1); try nat_math.
constructor. ∃ (wfp_inst_Abs fr (wfp_Gvar X)); splits¬.
assert (Hsaux : sizeP (wfp_Gvar X) = 1) by auto.
lets Hsize1 : sizeP_in Hsaux Ht; lets Hsize2 : sizeP_in Hsaux H2; lets Hsize3 : sizeP_in Hsaux Hr.
unfold wfp_sizeP in *; simpls; nat_math.
destruct aq; inverts H3; rename a0 into fr´; simpls.
elim (zerop n); introv Hneq; subst.
false; assert (Hsp : ¬ (wfp_sizeP p > 0) ∨ ¬ (wfp_sizeP r > 0)) by nat_math.
inverts Hsp as Hsp.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 2. ∃¬ a fp.
rewrite wfp_sizeP_S_tr in Hsp; apply Hsp.
branch 2. ∃¬ a fr.
assert (Hlt : n - 1 < n) by nat_math.
specializes Hyp Hlt; destruct Hyp as (Hio & _ & _ & Hin); clear Hlt.
specialize (Hin p q _ _ _ _ X Ht H2).
specializes Hin Hf.
replace (n - 1 + 1) with n by nat_math.
assert (Hsaux : sizeP (wfp_Gvar X) = 1) by auto.
lets Hsize1 : sizeP_in Hsaux Hr.
unfold wfp_sizeP in *; simpls; nat_math.
destruct Hin as (fq & Hq & Hyp).
∃ fq Hq; introv. eapply RCancel_step_forward.
applys¬ Hyp.
nat_math.
Qed.
Lemma IObis_cancellation : ∀ p q r, (wfp_Par p r) ≈ (wfp_Par q r) → p ≈ q.
Proof.
introv Hpar.
∃ (RCancel (wfp_sizeP p + wfp_sizeP q + wfp_sizeP r)); splits.
eapply RCancel_IObis.
constructor; ∃ r; splits~; nat_math.
Qed.
Lemma wfp_sizeP_0_IO_nil : ∀ (p : wfprocess),
wfp_sizeP p = 0 ↔ p ≈ wfp_Nil.
Proof.
introv; split; intro Hyp.
induction p using wfp_ind; unfold wfp_sizeP in *; simpls; try solve [nat_math].
assert (sizeP p1 = 0 ∧ sizeP p2 = 0) by nat_math.
destruct H as (Hsp1 & Hsp2).
specialize (IHp1 Hsp1); specialize (IHp2 Hsp2).
lets H´ : IObis_congr_par IHp1 IHp2.
assert (wfp_Par wfp_Nil wfp_Nil ≈ wfp_Nil).
apply congr_IObis; simpls; constructor¬.
etransitivity; try eassumption.
etransitivity; try eassumption.
apply congr_IObis; simpls; constructor¬.
apply congr_IObis; simpls; constructor¬.
lets H : IObis_sizeP_eq Hyp;
unfold wfp_sizeP in *; simpls¬.
Qed.
Fixpoint wfp_prod (l : list wfprocess) :=
match l with
| nil ⇒ wfp_Nil
| h :: nil ⇒ h
| h :: t ⇒ wfp_Par h (wfp_prod t)
end.
Lemma wfp_prod_cons : ∀ a b c,
wfp_prod (a :: b :: c) = wfp_Par a (wfp_prod (b :: c)).
Proof.
auto.
Qed.
Lemma wfp_prod_cons_inv : ∀ p lp,
wfp_Par p (wfp_prod lp) ≈ wfp_prod (p :: lp).
Proof.
destruct lp.
simpls¬. apply congr_IObis; repeat constructor.
rewrite¬ wfp_prod_cons.
Qed.
Lemma wfp_prod_cons_wfp_sizeP : ∀ p lp,
wfp_sizeP (wfp_prod (p :: lp)) = wfp_sizeP p + wfp_sizeP (wfp_prod lp).
Proof with automate.
inductions lp. simpls...
rewrite wfp_prod_cons. unfolds wfp_sizeP...
Qed.
Lemma wfp_prod_IO_app : ∀ (l1 l2 : list wfprocess),
wfp_prod (l1 ++ l2) ≈ wfp_Par (wfp_prod l1) (wfp_prod l2).
Proof with (try solve [applys× t_step]; automate).
inductions l1; introv.
replace (nil ++ l2) with l2 by auto; simpl.
apply congr_IObis.
etransitivity. constructor.
apply WfCgrPar_nil1... auto...
destruct l1; destruct l2.
apply congr_IObis.
simpls...
replace ((a :: nil) ++ w :: l2) with (a :: (w :: l2)) by auto.
rewrite wfp_prod_cons.
apply congr_IObis.
simpl wfp_prod at 2; repeat constructor×.
replace ((a :: w :: l1) ++ nil) with (a :: w :: l1) by (rewrite¬ app_nil_r).
apply congr_IObis.
simpl wfp_prod at 3...
replace ((a :: w :: l1) ++ w0 :: l2) with (a :: ((w :: l1) ++ w0 :: l2)) by auto.
specialize (IHl1 (w0 :: l2)).
rewrite wfp_prod_cons.
replace (wfp_prod (a :: (w :: l1) ++ w0 :: l2)) with (wfp_Par a (wfp_prod ((w :: l1) ++ w0 :: l2))).
etransitivity.
Focus 2.
assert (wfp_Par a (wfp_Par (wfp_prod (w :: l1)) (wfp_prod (w0 :: l2))) ≈ (wfp_Par (wfp_Par a (wfp_prod (w :: l1))) (wfp_prod (w0 :: l2)))).
apply congr_IObis...
eassumption.
applys¬ IObis_congr_par.
remember ((w :: l1) ++ w0 :: l2) as L; destruct L.
inverts HeqL; rewrite¬ wfp_prod_cons. auto.
Qed.
Lemma wfp_prod_wfcgr_permut : ∀ (l l´ : list wfprocess), permut l´ l → wfp_prod l ≡* wfp_prod l´.
Proof with (try solve [applys× t_step]; automate).
induction l using (measure_induction length); introv Hper;
destruct l; lets Hl : permut_len Hper.
apply length_zero_inv in Hl; substs¬. reflexivity.
apply lengthn in Hl.
destruct Hl as (w´ & l´´ & Heq); subst; rename l´´ into l´.
assert (Hmw´ : Mem w´ (w :: l)).
eapply permut_mem; try eassumption.
rewrite× Mem_cons_eq.
elim (classic (w = w´)); introv Hneq; substs¬.
rewrite <- permut_cons_iff in Hper. apply H in Hper.
Focus 2. rew_length; nat_math.
destruct l; destruct l´; try solve [simpls; reflexivity].
simpl wfp_prod at 1; rewrite wfp_prod_cons.
apply wfcgr_par with (p1 := w´) (q1 := w´) in Hper; auto.
etransitivity; try eassumption; unfold wfp_prod.
apply wfcgr_nil_l. reflexivity.
rewrite wfp_prod_cons.
apply wfcgr_par with (p1 := w´) (q1 := w´) in Hper; auto.
etransitivity; try eassumption; unfold wfp_prod.
apply wfcgr_nil_r. reflexivity.
repeat rewrite wfp_prod_cons. applys¬ wfcgr_par. reflexivity.
inverts Hmw´; try solve [false~].
lets (l´´ & Hper1) : permut_mem_exists H1.
assert (Mem w (w´ :: l´)).
eapply permut_mem. apply permut_sym; eassumption.
rewrite¬ Mem_cons_eq.
inverts H0; try solve [false~].
lets (l´´´ & Hper2) : permut_mem_exists H3.
assert (Hper3 : permut l´´ l´´´).
rewrite (permut_cons_iff _ _ w) in Hper1.
rewrite (permut_cons_iff _ _ w´) in Hper2.
rewrite (permut_cons_iff _ _ w); rewrite (permut_cons_iff _ _ w´).
apply permut_sym; apply permut_flip_first_two.
eapply permut_trans. apply permut_sym; eassumption.
eapply permut_trans. Focus 2. eassumption. auto.
lets Hprod1 : H Hper1.
apply permut_len in Hper;
apply permut_len in Hper1;
apply permut_len in Hper2; rew_length in *; nat_math.
symmetry in Hprod1.
destruct l. false. apply permut_len in Hper1; rew_length in *; nat_math.
rewrite wfp_prod_cons. apply wfcgr_par with (p1 := w) (q1 := w) in Hprod1; auto.
etransitivity. eassumption. remember (w0 :: l) as L; clear HeqL w0 l.
lets Hprod2 : H Hper2.
apply permut_len in Hper;
apply permut_len in Hper2; rew_length in *; nat_math.
symmetry in Hprod2.
destruct l´. false. apply permut_len in Hper2; rew_length in *; nat_math.
rewrite wfp_prod_cons. apply wfcgr_par with (p1 := w´) (q1 := w´) in Hprod2; auto.
etransitivity. Focus 2. symmetry; eassumption. remember (w0 :: l´) as L´; clear HeqL´ w0 l´.
clear Hprod1 Hprod2 H1 H3.
destruct l´´; destruct l´´´.
simpls. apply wfcgr_par_com.
simpl wfp_prod at 1. etransitivity. apply wfcgr_par_com.
apply wfcgr_par. reflexivity. rewrite wfp_prod_cons.
etransitivity. apply wfcgr_nil_l. apply wfcgr_par. reflexivity.
replace (wfp_Nil) with (wfp_prod nil) by auto.
apply H.
rew_length; nat_math.
applys¬ permut_sym.
rewrite wfp_prod_cons. simpl wfp_prod at 2.
assert (wfp_Par w w´ ≡* wfp_Par w´ w) by
(apply wfcgr_par_com).
etransitivity. Focus 2. apply H0. applys¬ wfcgr_par. reflexivity.
assert (w´ ≡* wfp_Par w´ wfp_Nil) by
(apply wfcgr_nil_l).
etransitivity. Focus 2. symmetry. apply H1. applys¬ wfcgr_par. reflexivity.
replace (wfp_Nil) with (wfp_prod nil) by auto.
apply H.
apply permut_len in Hper;
apply permut_len in Hper1; rew_length in *; nat_math.
applys¬ permut_sym.
repeat rewrite wfp_prod_cons.
assert (wfp_Par w (wfp_Par w´ (wfp_prod (w0 :: l´´))) ≡* wfp_Par (wfp_Par w w´) (wfp_prod (w0 :: l´´))). apply wfcgr_par_assoc_l.
assert (wfp_Par w´ (wfp_Par w (wfp_prod (w1 :: l´´´))) ≡* wfp_Par (wfp_Par w´ w) (wfp_prod (w1 :: l´´´))). apply wfcgr_par_assoc_l.
etransitivity. eassumption.
etransitivity. Focus 2. symmetry; eassumption.
apply wfcgr_par. apply wfcgr_par_com.
applys¬ H.
apply permut_len in Hper;
apply permut_len in Hper1; rew_length in *; nat_math.
applys¬ permut_sym. reflexivity. reflexivity.
Qed.
Lemma wfp_prod_IO_permut : ∀ (l l´ : list wfprocess), permut l´ l → wfp_prod l ≈ wfp_prod l´.
Proof.
introv Hper. apply congr_IObis.
applys× wfp_prod_wfcgr_permut.
Qed.
Lemma wfp_prod_trans_rem : ∀ lp (p : wfprocess) X (p´ : wfprocess),
{{p -- LabRem X ->> AP p´}} →
{{wfp_prod (p :: lp) -- LabRem X ->> AP (wfp_prod (p´ :: lp))}}.
Proof with automate.
destruct lp; introv Ht; [simpls¬ | ].
do 2 rewrite wfp_prod_cons...
Qed.
Lemma wfp_prod_trans_out : ∀ lp (p : wfprocess) a (p´ p´´ : wfprocess),
{{p -- LabOut a p´´ ->> AP p´}} →
{{wfp_prod (p :: lp) -- LabOut a p´´ ->> AP (wfp_prod (p´ :: lp))}}.
Proof with automate.
destruct lp; introv Ht; [simpls¬ | ].
do 2 rewrite wfp_prod_cons...
Qed.
Lemma wfp_prod_trans_in : ∀ lp (p : wfprocess) a fp,
{{p -- LabIn a ->> AA fp}} →
match lp with
| nil ⇒ True
| q :: lq ⇒ {{wfp_prod (p :: lp) -- LabIn a ->> AA (AbsPar1 fp (wfp_prod (q :: lq)))}}
end.
Proof with automate.
destruct lp; introv Ht; [simpls¬ | ].
rewrite wfp_prod_cons...
Qed.
Lemma wfp_prod_sizeP_mem : ∀ p lp,
Mem p lp → wfp_sizeP p ≤ wfp_sizeP (wfp_prod lp).
Proof.
inductions lp; introv Hm; inverts Hm.
destruct lp.
simpl; nat_math.
rewrite wfp_prod_cons;
unfold wfp_sizeP; simpls; nat_math.
destruct lp.
inverts H0.
apply IHlp in H0.
rewrite wfp_prod_cons;
unfold wfp_sizeP in *; simpls; nat_math.
Qed.
Fixpoint IO_pointwise (lp1 lp2 : list wfprocess) : Prop :=
match lp1, lp2 with
| nil, nil ⇒ True
| p1 :: lp1, p2 :: lp2 ⇒ (p1 ≈ p2) ∧ IO_pointwise lp1 lp2
| _, _ ⇒ False
end.
Lemma IO_pw_len : ∀ lp1 lp2,
IO_pointwise lp1 lp2 → length lp1 = length lp2.
Proof.
inductions lp1; destruct lp2; simpls×.
introv (_ & H); rew_length; apply IHlp1 in H; nat_math.
Qed.
Lemma IO_pw_wfp_prod : ∀ lp1 lp2,
IO_pointwise lp1 lp2 → wfp_prod lp1 ≈ wfp_prod lp2.
Proof.
induction lp1 using (measure_induction length);
destruct lp1; destruct lp2; try solve [simpls~]; introv HIOpw; inverts HIOpw.
destruct lp1; destruct lp2; try solve [simpls~]; try solve [inverts H1].
repeat rewrite wfp_prod_cons.
applys¬ IObis_congr_par.
applys¬ H; rew_length; nat_math.
Qed.
Definition prime (p : wfprocess) : Prop :=
¬ (p ≈ wfp_Nil) ∧
(∀ p1 p2, p ≈ wfp_Par p1 p2 → p1 ≈ wfp_Nil ∨ p2 ≈ wfp_Nil).
Lemma prime_IO : ∀ p, prime p → ∀ q, p ≈ q → prime q.
Proof.
introv Hpp Hio.
apply not_not_elim; intro Hnpq.
unfold prime in *; rew_logic in Hnpq; inverts Hnpq as Hnpq.
rewrite <- wfp_sizeP_0_IO_nil in ×.
apply IObis_sizeP_eq in Hio; nat_math.
destruct Hnpq as (p1 & Hpnq). rew_logic in Hpnq.
destruct Hpnq as (p2 & Hpnq). rew_logic in Hpnq.
destruct Hpnq as (Hio´ & Hp1 & Hp2).
destruct Hpp as (_ & Hpp).
assert (p ≈ wfp_Par p1 p2).
etransitivity; eassumption.
specializes Hpp H. intuition.
Qed.
Lemma prime_parallel : ∀ p1 p2, prime (wfp_Par p1 p2) ↔
((prime p1 ∧ p2 ≈ wfp_Nil) ∨ (prime p2 ∧ p1 ≈ wfp_Nil)).
Proof with (try solve [applys× t_step]; automate).
introv; splits; introv Hyp.
inverts Hyp.
elim (zerop (wfp_sizeP p1)); introv Hsp1;
elim (zerop (wfp_sizeP p2)); introv Hsp2.
rewrite <- wfp_sizeP_0_IO_nil in H.
unfold wfp_sizeP in *; simpls; nat_math.
right; rewrite wfp_sizeP_0_IO_nil in Hsp1; repeat splits¬.
rewrite <- wfp_sizeP_0_IO_nil; nat_math; clear H.
intros q1 q2 Hpar.
apply IObis_congr_par1 with (r := p1) in Hpar.
assert (wfp_Par p1 p2 ≈ wfp_Par (wfp_Par p1 q1) q2).
etransitivity. Focus 2. etransitivity. apply Hpar.
apply congr_IObis. etransitivity.
constructor. apply WfCgrPar_com.
constructor. apply WfCgrPar_assoc1.
apply congr_IObis...
specializes H0 H1; inverts H0; [left | right]; auto.
rewrite <- wfp_sizeP_0_IO_nil in *;
unfold wfp_sizeP in *; simpls; nat_math.
left; rewrite wfp_sizeP_0_IO_nil in Hsp2; repeat splits¬.
rewrite <- wfp_sizeP_0_IO_nil; nat_math; clear H.
intros q1 q2 Hpar.
apply IObis_congr_par1 with (r := p2) in Hpar.
assert (wfp_Par p1 p2 ≈ wfp_Par (wfp_Par p2 q1) q2).
etransitivity. apply Hpar.
apply congr_IObis. etransitivity.
constructor. apply WfCgrPar_com.
constructor. apply WfCgrPar_assoc1.
specializes H0 H1; inverts H0; [left | right]; auto.
rewrite <- wfp_sizeP_0_IO_nil in *;
unfold wfp_sizeP in *; simpls; nat_math.
assert (Hpar : wfp_Par p1 p2 ≈ wfp_Par p1 p2) by auto.
specializes H0 Hpar; inverts H0;
rewrite <- wfp_sizeP_0_IO_nil in H1; nat_math.
inverts Hyp; splits; destruct H as (Hp1 & Hp2).
introv Hyp. destruct Hp1 as (Hp1 & _).
rewrite <- wfp_sizeP_0_IO_nil in ×.
unfolds wfp_sizeP; simpls.
assert (sizeP p1 = 0) by nat_math. intuition.
intros p1´ p2´ Hio.
destruct Hp1 as (Hsp1 & Hiop1). specializes Hiop1 p1´ p2´.
apply Hiop1. clear Hiop1. etransitivity. Focus 2. eassumption.
∃ wfcgr. splits. apply congr_IObisimulation.
etransitivity. constructor. apply WfCgrPar_nil1.
apply wfcgr_par. repeat constructor. symmetry.
rewrite <- wfp_sizeP_0_IO_nil in ×.
apply sizeP_0_congr_nil. unfolds¬ wfp_sizeP.
introv Hyp. destruct Hp1 as (Hp1 & _).
rewrite <- wfp_sizeP_0_IO_nil in ×.
unfolds wfp_sizeP; simpls.
assert (sizeP p2 = 0) by nat_math. intuition.
intros p1´ p2´ Hio.
destruct Hp1 as (Hsp1 & Hiop1). specializes Hiop1 p1´ p2´.
apply Hiop1. clear Hiop1. etransitivity. Focus 2. eassumption.
∃ wfcgr. splits. apply congr_IObisimulation.
etransitivity. constructor. apply WfCgrPar_nil1.
etransitivity. constructor. apply WfCgrPar_com.
apply wfcgr_par. Focus 2. repeat constructor. symmetry.
rewrite <- wfp_sizeP_0_IO_nil in ×.
apply sizeP_0_congr_nil. unfolds¬ wfp_sizeP.
Qed.
Lemma prime_in : ∀ p a fp,
prime p → ∀ (Htp : {{p -- LabIn a ->> AA fp}}),
∃ X p´, p ≈ wfp_Abs a X p´.
Proof.
induction p using (measure_induction wfp_size).
introv Hprime Htp; inverts Htp.
eexists. eexists. reflexivity.
rename p0 into p.
destruct ap; inverts H0. rename a0 into fp.
apply prime_parallel in Hprime; inverts Hprime; inverts H0.
specializes¬ H H3.
unfold wfp_size; simpl; nat_math.
destruct H as (X & p´ & Heq).
∃ X p´.
apply IObis_congr_par with (p1 := p) (p2 := p) in H2; auto.
etransitivity; try eassumption.
etransitivity. Focus 2. eassumption.
apply congr_IObis; repeat constructor.
rewrite <- wfp_sizeP_0_IO_nil in H2.
lets (X & _) : find_fresh (@nil process).
assert (sizeP (wfp_Gvar X) = 1) by auto.
apply (sizeP_in a _ _ _ H0) in H3; unfold wfp_sizeP in H2; simpls; nat_math.
rename p0 into p´.
destruct aq; inverts H0.
apply prime_parallel in Hprime; inverts Hprime; inverts H0.
Focus 2.
specializes¬ H H3.
unfold wfp_size; simpl; nat_math.
destruct H as (X & p´´ & Heq).
apply IObis_congr_par with (p1 := q) (p2 := q) in H2; auto.
∃ X p´´.
etransitivity.
apply IObis_congr_par_com.
etransitivity. eassumption.
etransitivity. Focus 2. eassumption.
apply congr_IObis; repeat constructor.
rewrite <- wfp_sizeP_0_IO_nil in H2.
lets (X & _) : find_fresh (@nil process).
assert (sizeP (wfp_Gvar X) = 1) by auto.
apply (sizeP_in a _ _ _ H0) in H3; unfold wfp_sizeP in H2; simpls; nat_math.
Qed.
Lemma prime_out : ∀ p a (p´ p´´ : wfprocess),
prime p → {{p -- LabOut a p´´ ->> AP p´}} → p ≈ wfp_Send a p´´ ∧ p´ ≈ wfp_Nil.
Proof.
induction p using (measure_induction wfp_size).
introv Hprime Htp; inverts Htp.
splits¬.
rename p0 into p.
destruct ap; inverts H0. rename w into p´.
apply prime_parallel in Hprime; inverts Hprime; inverts H0.
specializes¬ H H3.
unfold wfp_size; simpl; nat_math.
inverts H.
lets H8 : H2; apply IObis_congr_par with (p1 := p) (p2 := p) in H8; auto.
apply IObis_congr_par with (p1 := p´) (p2 := p´) in H2; auto.
splits; etransitivity; try eassumption.
etransitivity. Focus 2. eassumption.
apply congr_IObis; repeat constructor.
etransitivity. Focus 2. eassumption.
apply congr_IObis; repeat constructor.
rewrite <- wfp_sizeP_0_IO_nil in H2.
apply sizeP_out in H3; unfold wfp_sizeP in H2; simpls; nat_math.
rename p´ into q´; rename p0 into p.
destruct aq; inverts H0; rename w into q´.
apply prime_parallel in Hprime; inverts Hprime; inverts H0.
Focus 2.
specializes¬ H H3.
unfold wfp_size; simpl; nat_math.
inverts H.
lets H7 : H2; apply IObis_congr_par with (p1 := q) (p2 := q) in H7; auto.
apply IObis_congr_par with (p1 := q´) (p2 := q´) in H2; auto.
splits; etransitivity.
apply IObis_congr_par_com.
etransitivity. eassumption.
etransitivity. Focus 2. eassumption.
apply congr_IObis; repeat constructor.
apply IObis_congr_par_com.
etransitivity. eassumption.
etransitivity. Focus 2. eassumption.
apply congr_IObis; repeat constructor.
rewrite <- wfp_sizeP_0_IO_nil in H2.
apply sizeP_out in H3; unfold wfp_sizeP in H2; simpls; nat_math.
Qed.
Lemma prime_remove : ∀ p X (p´ : wfprocess),
prime p → {{p -- LabRem X ->> AP p´}} → p ≈ wfp_Gvar X ∧ p´ ≈ wfp_Nil.
Proof.
induction p using (measure_induction wfp_size).
introv Hprime Htp; inverts Htp. splits¬.
rename p0 into p; rename p´ into p´´.
destruct ap; inverts H0; rename w into p´.
apply prime_parallel in Hprime; inverts Hprime; inverts H0.
specializes¬ H H3.
unfold wfp_size; simpl; nat_math.
inverts H.
lets H8 : H2; apply IObis_congr_par with (p1 := p) (p2 := p) in H8; auto.
apply IObis_congr_par with (p1 := p´) (p2 := p´) in H2; auto.
splits; etransitivity; try eassumption.
etransitivity. Focus 2. eassumption.
apply congr_IObis; repeat constructor.
etransitivity. Focus 2. eassumption.
apply congr_IObis; repeat constructor.
rewrite <- wfp_sizeP_0_IO_nil in H2.
apply sizeP_remove in H3; unfold wfp_sizeP in H2; simpls; nat_math.
rename q into w; rename p´ into q´; rename p0 into p´.
destruct aq; inverts H0; rename w0 into w´.
apply prime_parallel in Hprime; inverts Hprime; inverts H0.
Focus 2.
specializes¬ H H3.
unfold wfp_size; simpl; nat_math.
inverts H.
lets H7 : H2; apply IObis_congr_par with (p1 := w´) (p2 := w´) in H7; auto.
apply IObis_congr_par with (p1 := w) (p2 := w) in H2; auto.
splits; etransitivity.
apply IObis_congr_par_com.
etransitivity. eassumption.
etransitivity. Focus 2. eassumption.
apply congr_IObis; repeat constructor.
apply IObis_congr_par_com.
etransitivity. eassumption.
etransitivity. Focus 2. eassumption.
apply congr_IObis; repeat constructor.
rewrite <- wfp_sizeP_0_IO_nil in H2.
apply sizeP_remove in H3; unfold wfp_sizeP in H2; simpls; nat_math.
Qed.
Lemma wfp_prod_in_compat : ∀ lq a fq´
(Htp : {{wfp_prod lq -- LabIn a ->> AA fq´}}),
(Forall (fun q ⇒ prime q) lq) →
∃ (q : wfprocess) fq (Ht : {{q -- LabIn a ->> AA fq}}),
Mem q lq ∧
∃ lq´, permut lq (q :: lq´) ∧
∀ X, wfp_inst_Abs fq´ (wfp_Gvar X) ≈
wfp_Par (wfp_inst_Abs fq (wfp_Gvar X)) (wfp_prod lq´).
Proof with (try solve [applys× t_step]; automate).
induction lq using (measure_induction length).
intros a fq´ Htlq Hplq; destruct lq; [inverts Htlq | ].
destruct lq.
simpl wfp_prod in Htlq; inverts Htlq.
∃ (wfp_Abs a X p) (AbsPure X p). constructor¬. splits~; try constructor.
∃ (@nil wfprocess); splits×.
introv; simpl. apply congr_IObis; repeat constructor.
destruct ap; inverts H0; rename a0 into fp.
inverts Hplq; inverts H2. specializes H1 p q.
assert (wfp_Par p q ≈ wfp_Par p q) by auto.
specializes H1 H2; clear H2; inverts H1.
rewrite <- wfp_sizeP_0_IO_nil in H2.
lets (X & _) : find_fresh (@nil process).
assert (sizeP (wfp_Gvar X) = 1) by auto.
apply (sizeP_in a _ _ _ H1) in H3; unfold wfp_sizeP in H2; simpls; nat_math.
∃ (wfp_Par p q) (AbsPar1 fp q). constructor...
splits; try constructor.
∃ (@nil wfprocess); splits×.
introv; simpl.
apply congr_IObis...
destruct aq; inverts H0. rename a0 into fq.
inverts Hplq; inverts H2. specializes H1 p q.
assert (wfp_Par p q ≈ wfp_Par p q) by auto.
specializes H1 H2; clear H2; inverts H1.
∃ (wfp_Par p q) (AbsPar2 p fq). constructor...
splits; try constructor.
∃ (@nil wfprocess); splits×.
introv; simpl.
apply congr_IObis...
lets (X & _) : find_fresh (@nil process).
rewrite <- wfp_sizeP_0_IO_nil in H2.
assert (sizeP (wfp_Gvar X) = 1) by auto.
apply (sizeP_in a _ _ _ H1) in H3. unfold wfp_sizeP in H2; simpls; nat_math.
rewrite wfp_prod_cons in ×.
set (L := wfp_prod (w0 :: lq)). fold L in Htlq.
inverts Htlq...
lets (fpw & Hw´) : wfp_agent_in H3; subst ap; inverts H4.
∃ w fpw H3; splits*; try constructor.
lets (fpw & Hw´) : wfp_agent_in H3; subst aq; inverts H4.
subst L.
inverts Hplq.
assert (length (w0 :: lq) < length (w :: w0 :: lq)).
rew_length; nat_math.
specializes H H0 a fpw. specialize (H H3 H4).
destruct H as (q & q´ & Htq & Hmq & (lq´ & Hplq´ & Hiolq´)).
∃ q q´ Htq; splits.
repeat constructor¬.
∃ (w :: lq´); splits.
apply permut_flip_first_two. rewrite¬ <- permut_cons_iff.
introv. specializes Hiolq´ X; simpl wfp_inst_Abs.
apply IObis_congr_par with (p1 := w) (p2 := w) in Hiolq´; auto.
etransitivity. eassumption.
remember (wfp_inst_Abs q´ (wfp_Gvar X)) as r; clear Heqr.
assert (wfp_Par w (wfp_Par r (wfp_prod lq´)) ≈
wfp_Par r (wfp_Par w (wfp_prod lq´))).
assert (wfp_Par w (wfp_Par r (wfp_prod lq´)) ≈ wfp_Par (wfp_Par w r) (wfp_prod lq´)).
apply congr_IObis...
etransitivity. eassumption.
assert (wfp_Par r (wfp_Par w (wfp_prod lq´)) ≈ (wfp_Par (wfp_Par r w) (wfp_prod lq´))).
apply congr_IObis...
etransitivity. Focus 2. symmetry; eassumption.
apply¬ IObis_congr_par. apply¬ IObis_congr_par_com.
etransitivity. eassumption.
lets H1 : wfp_prod_cons_inv w lq´.
apply IObis_congr_par with (p1 := r) (p2 := r) in H1; auto.
Qed.
Lemma wfp_prod_out_compat : ∀ lq a (lq´´ q´´ : wfprocess),
{{wfp_prod lq -- LabOut a q´´ ->> AP lq´´}} →
(Forall (fun q ⇒ prime q) lq) →
∃ (q q´ : wfprocess), Mem q lq ∧
{{q -- LabOut a q´´ ->> AP q´}} ∧
∃ lq´, permut lq (q :: lq´) ∧ lq´´ ≈ wfp_prod (q´ :: lq´).
Proof with (try solve [applys× t_step]; automate).
induction lq using (measure_induction length).
introv Htlq Hplq; destruct lq; [inverts Htlq | ].
destruct lq.
simpl wfp_prod in Htlq; inverts Htlq.
∃ (wfp_Send a q´´) wfp_Nil; splits~; try constructor.
∃ (@nil wfprocess); splits×.
destruct ap; inverts H0... rename w into p´; rename q´´ into p´´.
inverts Hplq; inverts H2. specializes H1 p q.
assert (wfp_Par p q ≈ wfp_Par p q) by auto.
specializes H1 H2; clear H2; inverts H1.
rewrite <- wfp_sizeP_0_IO_nil in H2.
apply sizeP_out in H3; unfold wfp_sizeP in H2; simpls; nat_math.
∃ (wfp_Par p q) (wfp_Par p´ q).
splits; try constructor...
destruct aq; inverts H0; rename w into q´...
inverts Hplq; inverts H2. specializes H1 p q.
assert (wfp_Par p q ≈ wfp_Par p q) by auto.
specializes H1 H2; clear H2; inverts H1.
∃ (wfp_Par p q) (wfp_Par p q´).
splits; try constructor...
rewrite <- wfp_sizeP_0_IO_nil in H2.
apply sizeP_out in H3; unfold wfp_sizeP in H2; simpls; nat_math.
rewrite wfp_prod_cons in *; remember (wfp_prod (w0 :: lq)) as L; inverts Htlq...
lets (w´ & Hw´) : wfp_agent_out H3; subst ap; inverts H4.
∃ w w´; splits*; try constructor.
lets (w´ & Hw´) : wfp_agent_out H3; subst aq; inverts H4.
specializes H H3.
rew_length; nat_math.
inverts Hplq. specializes H H4.
destruct H as (q & q´ & Hmq & Htq & (lq´ & Hplq´ & Hiolq´)).
∃ q q´; splits¬.
repeat constructor¬.
∃ (w :: lq´); splits.
apply permut_flip_first_two. rewrite¬ <- permut_cons_iff.
apply IObis_congr_par with (p1 := w) (p2 := w) in Hiolq´; auto.
etransitivity. eassumption.
rewrite <- wfp_prod_cons. apply wfp_prod_IO_permut.
apply¬ permut_flip_first_two.
Qed.
Lemma wfp_prod_rem_compat : ∀ lq X (lq´´ : wfprocess),
{{wfp_prod lq -- LabRem X ->> AP lq´´}} →
(Forall (fun q ⇒ prime q) lq) →
∃ (q q´ : wfprocess), Mem q lq ∧
{{q -- LabRem X ->> AP q´}} ∧
∃ lq´, permut lq (q :: lq´) ∧ lq´´ ≈ wfp_prod (q´ :: lq´).
Proof with (try solve [applys× t_step]; automate).
induction lq using (measure_induction length).
introv Htlq Hplq; destruct lq; [inverts Htlq | ].
destruct lq.
simpl wfp_prod in Htlq; inverts Htlq.
∃ (wfp_Gvar X) wfp_Nil; splits~; try constructor.
∃ (@nil wfprocess); splits×.
destruct ap; inverts H0; rename w into p´...
inverts Hplq; inverts H2. specializes H1 p q.
assert (wfp_Par p q ≈ wfp_Par p q) by auto.
specializes H1 H2; clear H2; inverts H1.
rewrite <- wfp_sizeP_0_IO_nil in H2.
apply sizeP_remove in H3; unfold wfp_sizeP in H2; simpls; nat_math.
∃ (wfp_Par p q) (wfp_Par p´ q).
splits; try constructor...
destruct aq; inverts H0; rename w into q´...
inverts Hplq; inverts H2. specializes H1 p q.
assert (wfp_Par p q ≈ wfp_Par p q) by auto.
specializes H1 H2; clear H2; inverts H1.
∃ (wfp_Par p q) (wfp_Par p q´).
splits; try constructor...
rewrite <- wfp_sizeP_0_IO_nil in H2.
apply sizeP_remove in H3; unfold wfp_sizeP in H2; simpls; nat_math.
rewrite wfp_prod_cons in *; remember (wfp_prod (w0 :: lq)) as L; inverts Htlq...
lets (w´ & Hw´) : wfp_agent_rem H3; subst ap; inverts H4.
∃ w w´; splits*; try constructor.
lets (w´ & Hw´) : wfp_agent_rem H3; subst aq; inverts H4.
specializes H H3.
rew_length; nat_math.
inverts Hplq. specializes H H4.
destruct H as (q & q´ & Hmq & Htq & (lq´ & Hplq´ & Hiolq´)).
∃ q q´; splits¬.
repeat constructor¬.
∃ (w :: lq´); splits.
apply permut_flip_first_two. rewrite¬ <- permut_cons_iff.
apply IObis_congr_par with (p1 := w) (p2 := w) in Hiolq´; auto.
etransitivity. eassumption.
rewrite <- wfp_prod_cons. apply wfp_prod_IO_permut.
apply¬ permut_flip_first_two.
Qed.
Definition prime_decomposition (p : wfprocess) (lp : list wfprocess) : Prop :=
p ≈ wfp_prod lp ∧ (Forall (fun p ⇒ prime p) lp).
Lemma prime_decomposition_IO : ∀ p1 p2 lp,
prime_decomposition p1 lp → p1 ≈ p2 → prime_decomposition p2 lp.
Proof.
introv (H1 & H2) Hio; splits×.
Qed.
Lemma prime_decomposition_exists :
∀ p,
∃ lp,
prime_decomposition p lp.
Proof.
induction p using (measure_induction wfp_sizeP).
elim (zerop (wfp_sizeP p)); introv Hsp.
∃ (@nil wfprocess); splits.
rewrite wfp_sizeP_0_IO_nil in Hsp.
simpl; etransitivity. eassumption. auto.
apply Forall_nil.
elim (classic (prime p)); introv Hpr.
∃ (p :: nil); splits¬.
repeat constructor¬.
unfold prime in Hpr; rew_logic in Hpr; inverts Hpr.
rewrite <- wfp_sizeP_0_IO_nil in H0. nat_math.
destruct H0 as (p1 & H0); rew_logic in H0.
destruct H0 as (p2 & H0); rew_logic in H0.
destruct H0 as (Hio & Hn1 & Hn2).
rewrite <- wfp_sizeP_0_IO_nil in *;
assert (wfp_sizeP p1 < wfp_sizeP p ∧ wfp_sizeP p2 < wfp_sizeP p).
apply IObis_sizeP_eq in Hio.
unfold wfp_sizeP in *; simpls; splits; nat_math.
destruct H0 as (Hs1 & Hs2).
lets (lp1 & Hpr1) : H Hs1; lets (lp2 & Hpr2) : H Hs2.
inverts Hpr1; inverts Hpr2.
∃ (lp1 ++ lp2); splits¬.
etransitivity. eassumption.
etransitivity. Focus 2. symmetry. apply wfp_prod_IO_app.
apply¬ IObis_congr_par.
apply¬ Forall_app.
Qed.
Lemma prime_decomposition_unique : ∀ p lp1 lp2,
prime_decomposition p lp1 → prime_decomposition p lp2 →
∃ lp1´ lp2´, permut lp1 lp1´ ∧ permut lp2 lp2´ ∧ IO_pointwise lp1´ lp2´.
Proof.
induction p using (measure_induction wfp_sizeP).
introv Hpd1 Hpd2.
elim (classic (∃ p1 p2, Mem p1 lp1 ∧ Mem p2 lp2 ∧ p1 ≈ p2)); introv Hyp.
destruct Hyp as (p1 & p2 & Hmp1 & Hmp2 & Hio).
lets (lp1t & Hper1) : permut_mem_exists Hmp1.
lets (lp2t & Hper2) : permut_mem_exists Hmp2.
specializes H (wfp_prod lp1t).
assert (Ha0 : wfp_sizeP (wfp_prod lp1t) < wfp_sizeP p).
inverts Hpd1. lets Hio´ : wfp_prod_IO_permut Hper1.
apply IObis_sizeP_eq in H0; apply IObis_sizeP_eq in Hio´.
rewrite H0; rewrite <- Hio´.
assert (wfp_sizeP p1 > 0).
apply Forall_permut with (l2 := (p1 :: lp1t)) in H1; auto.
inverts H1; inverts H4. rewrite <- wfp_sizeP_0_IO_nil in H1; nat_math.
destruct lp1t.
simpl; unfold wfp_sizeP in *; simpl; nat_math.
rewrite wfp_prod_cons; unfold wfp_sizeP in *; simpl; nat_math.
specializes H Ha0 lp1t lp2t.
assert (Ha1 : prime_decomposition (wfp_prod lp1t) lp1t).
splits¬.
inverts Hpd1; apply Forall_permut with (l2 := (p1 :: lp1t)) in H1; inverts¬ H1.
assert (Ha2 : prime_decomposition (wfp_prod lp1t) lp2t).
splits¬.
inverts Hpd1; inverts Hpd2.
lets H4 : wfp_prod_IO_permut Hper1; lets H5 : wfp_prod_IO_permut Hper2.
assert (Hprod : wfp_prod (p1 :: lp1t) ≈ wfp_prod (p2 :: lp2t)).
etransitivity. eassumption.
etransitivity. symmetry; apply H0.
etransitivity. apply H2.
symmetry; auto.
clear H5 H4 H2 H0.
apply Forall_permut with (l2 := (p1 :: lp1t)) in H1; auto.
apply Forall_permut with (l2 := (p2 :: lp2t)) in H3; auto.
inverts H1; inverts H3; clear Hper1 Hper2 Hmp1 Hmp2 Ha0.
destruct lp1t; destruct lp2t; try solve [simpls*].
simpl wfp_prod at 1. simpl wfp_prod at 1 in Hprod.
rewrite wfp_prod_cons in Hprod; remember (w :: lp2t) as L.
symmetry; rewrite <- wfp_sizeP_0_IO_nil.
apply IObis_sizeP_eq in Hio.
apply IObis_sizeP_eq in Hprod.
unfold wfp_sizeP in *; simpls; nat_math.
simpl wfp_prod at 2. simpl wfp_prod at 2 in Hprod.
rewrite wfp_prod_cons in Hprod; remember (w :: lp1t) as L.
rewrite <- wfp_sizeP_0_IO_nil.
apply IObis_sizeP_eq in Hio.
apply IObis_sizeP_eq in Hprod.
unfold wfp_sizeP in *; simpls; nat_math.
repeat rewrite wfp_prod_cons in Hprod.
apply IObis_cancellation with (r := p1).
etransitivity. apply IObis_congr_par_com.
etransitivity. eassumption.
etransitivity. Focus 2. apply IObis_congr_par_com.
apply¬ IObis_congr_par.
inverts Hpd2; apply Forall_permut with (l2 := (p2 :: lp2t)) in H1; inverts¬ H1.
assert (wfp_sizeP (wfp_prod lp1t) = wfp_sizeP (wfp_prod lp2t)).
inverts Hpd1; inverts Hpd2.
assert (wfp_prod (p1 :: lp1t) ≈ wfp_prod (p2 :: lp2t)).
lets H4 : wfp_prod_IO_permut Hper1; lets H5 : wfp_prod_IO_permut Hper2.
etransitivity. eassumption.
etransitivity. Focus 2. symmetry; eassumption.
etransitivity. Focus 2. apply H2. auto.
apply IObis_sizeP_eq in H4. apply IObis_sizeP_eq in Hio.
destruct lp1t; destruct lp2t; try solve [simpls~];
repeat rewrite wfp_prod_cons in H4;
unfold wfp_sizeP in *; simpls; nat_math.
elim (zerop (wfp_sizeP (wfp_prod lp1t))); intro Hs1.
rewrite Hs1 in H0; symmetry in H0.
assert (lp1t = nil).
destruct lp1t; auto.
inverts Hpd1. lets H3 : Forall_permut H2 Hper1.
inverts H3. inverts H7. inverts H5.
rewrite <- wfp_sizeP_0_IO_nil in *;
unfold wfp_sizeP in ×.
destruct lp1t.
simpl in Hs1; nat_math.
rewrite wfp_prod_cons in Hs1; simpls; nat_math.
assert (lp2t = nil).
destruct lp2t; auto.
inverts Hpd2. lets H4 : Forall_permut H3 Hper2.
inverts H4. inverts H8. inverts H6.
rewrite <- wfp_sizeP_0_IO_nil in *;
unfold wfp_sizeP in ×.
destruct lp2t.
simpl in H0; nat_math.
rewrite wfp_prod_cons in H0; simpls; nat_math.
subst; simpls.
∃ (p1 :: nil) (p2 :: nil); splits~; simpls¬.
assert (wfp_sizeP (wfp_prod lp1t) > 0) by nat_math.
specializes¬ H Ha2.
destruct H as (lp1´´ & lp2´´ & Hper1´´ & Hper2´´ & Hiop).
∃ (p1 :: lp1´´) (p2 :: lp2´´); splits¬.
apply permut_trans with (l2 := (p1 :: lp1t)); auto.
apply permut_trans with (l2 := (p2 :: lp2t)); auto.
simpls¬.
assert (HnoIO : ∀ p1 p2, Mem p1 lp1 → Mem p2 lp2 → ¬ (p1 ≈ p2)).
introv Hm1 Hm2.
rew_logic in Hyp; specializes Hyp p1.
rew_logic in Hyp; specializes Hyp p2.
intuition.
clear Hyp.
elim (zerop (wfp_sizeP p)); introv Hsp.
rewrite wfp_sizeP_0_IO_nil in Hsp.
lets Hpd1´ : prime_decomposition_IO Hpd1 Hsp.
lets Hpd2´ : prime_decomposition_IO Hpd2 Hsp.
inverts Hpd1´; inverts Hpd2´.
destruct lp1; destruct lp2.
∃ (@nil wfprocess) (@nil wfprocess); splits~; simpls¬.
lets Hio´ : wfp_prod_cons_inv w lp2.
inverts H3. inverts H6.
assert (wfp_Nil ≈ wfp_Par w (wfp_prod lp2)) by jauto.
apply IObis_sizeP_eq in H5.
rewrite <- wfp_sizeP_0_IO_nil in H3;
unfold wfp_sizeP in *; simpls; nat_math.
lets Hio´ : wfp_prod_cons_inv w lp1.
inverts H1. inverts H6.
assert (wfp_Nil ≈ wfp_Par w (wfp_prod lp1)) by jauto.
apply IObis_sizeP_eq in H5.
rewrite <- wfp_sizeP_0_IO_nil in H1;
unfold wfp_sizeP in *; simpls; nat_math.
lets Hio´ : wfp_prod_cons_inv w lp1.
inverts H1. inverts H6.
assert (wfp_Nil ≈ wfp_Par w (wfp_prod lp1)) by jauto.
apply IObis_sizeP_eq in H5.
rewrite <- wfp_sizeP_0_IO_nil in H1;
unfold wfp_sizeP in *; simpls; nat_math.
fold (Peano.gt (wfp_sizeP p) 0) in Hsp; rewrite <- gt_peano in Hsp.
false.
Lemma list_exists_min : ∀ l, length l > 0 → ∃ p, Mem p l ∧ ∀ p´, Mem p´ l → wfp_sizeP p ≤ wfp_sizeP p´.
Proof.
induction l using (measure_induction length); destruct l; introv Hl.
rew_length in *; nat_math.
destruct l.
∃ w; splits¬.
repeat constructor.
introv Hm; inverts Hm; [nat_math | inverts H1].
assert (length (w0 :: l) > 0) by (rew_length; nat_math).
lets (p´´ & Hmp´´ & Hminp´´) : H H0.
rew_length; nat_math.
elim (le_lt_dec (wfp_sizeP w) (wfp_sizeP p´´)); introv Hdec.
∃ w; splits.
repeat constructor.
introv Hm; inverts Hm; [ | specializes Hminp´´ H2]; nat_math.
∃ p´´; splits.
repeat constructor¬.
introv Hm; inverts Hm; [ | specializes Hminp´´ H2]; nat_math.
Qed.
assert (Hl : length (lp1 ++ lp2) > 0).
destruct lp1; destruct lp2;
inverts Hpd1; inverts Hpd2; simpls;
try (rewrite <-wfp_sizeP_0_IO_nil in *; nat_math).
rew_length; nat_math.
lets (r & Hmr & Hminr) : list_exists_min Hl.
assert (HnoIO´ : ∀ s p´, wfp_sizeP s < wfp_sizeP r → Mem p´ (lp1 ++ lp2) → ¬ (s ≈ p´)).
introv Hs Hm Hio.
apply IObis_sizeP_eq in Hio.
specializes Hminr Hm; nat_math.
assert (Hsr : wfp_sizeP r > 0).
rewrite Mem_app_or_eq in Hmr; inverts Hmr;
[inverts Hpd1 | inverts Hpd2];
rewrite <- Forall_Mem in H2;
specializes H2 H0; inverts H2;
rewrite <- wfp_sizeP_0_IO_nil in H3; nat_math.
assert (Hio : wfp_prod lp1 ≈ wfp_prod lp2) by
(inverts Hpd1; inverts× Hpd2).
rewrite Mem_app_or_eq in Hmr; inverts Hmr.
lets (lp1´ & Hplp1´) : permut_mem_exists H0.
assert (Hio´ : wfp_prod (r :: lp1´) ≈ wfp_prod lp2).
etransitivity. eapply wfp_prod_IO_permut. eassumption. auto.
assert (Hpd1´ : prime_decomposition p (r :: lp1´)).
splits¬. etransitivity. Focus 2. symmetry; eassumption.
etransitivity. Focus 2. apply Hio.
inverts¬ Hpd1.
eapply Forall_permut. Focus 2. eassumption. inverts¬ Hpd1.
lets (Hpd11 & Hpd12) : Hpd1; lets (Hpd21 & Hpd22) : Hpd2.
rewrite wfp_sizeP_S_tr in Hsr.
inverts Hsr as Hsr.
destruct Hsr as (X & r´ & Htr).
lets Htlp1 : wfp_prod_trans_rem lp1´ Htr.
lets (lp2´ & Htlp2 & Hio´´) : IObis_var Hio´ Htlp1.
lets (q & q´ & Hmq´ & Htq´ & (lq´ & Hplq´ & Hioq´)) : wfp_prod_rem_compat Htlp2 Hpd22.
assert (HioM : wfp_prod (r´ :: lp1´) ≈ wfp_prod (q´ :: lq´)) by jauto.
assert (Hpr : prime r) by (inverts Hpd1´; inverts¬ H2).
assert (Hpq : prime q).
rewrite <- Forall_Mem in Hpd22. specializes¬ Hpd22 Hmq´.
lets (Hio_r & _) : prime_remove Hpr Htr.
lets (Hio_q & _) : prime_remove Hpq Htq´.
specializes HnoIO H0 Hmq´; apply HnoIO.
inverts Hsr as Hsr. Focus 2.
destruct Hsr as (a & r´ & r´´ & Htr).
lets Htlp1 : wfp_prod_trans_out lp1´ Htr.
lets (lp2´ & lp2´´ & Htlp2 & Hiol´ & Hiol´´) : IObis_out Hio´ Htlp1.
lets (q & q´ & Hmq´ & Htq´ & (lq´ & Hplq´ & Hioq´)) : wfp_prod_out_compat Htlp2 Hpd22.
assert (HioM : wfp_prod (r´ :: lp1´) ≈ wfp_prod (q´ :: lq´)) by jauto.
assert (Hpr : prime r) by (inverts Hpd1´; inverts¬ H2).
assert (Hpq : prime q).
rewrite <- Forall_Mem in Hpd22. specializes¬ Hpd22 Hmq´.
lets (Hio_r & _) : prime_out Hpr Htr.
lets (Hio_q & _) : prime_out Hpq Htq´.
specializes HnoIO H0 Hmq´; apply HnoIO.
etransitivity. eassumption.
etransitivity. Focus 2. symmetry; eassumption.
apply¬ IObis_congr_send.
destruct Hsr as (a & fr & Htr).
lets Htlp1 : wfp_prod_trans_in lp1´ Htr; destruct lp1´.
clear Htlp1. destruct lp2.
apply IObis_sizeP_eq in Hpd21. apply IObis_sizeP_eq in Hio´.
lets (X & _) : find_fresh (@nil process).
assert (sizeP (wfp_Gvar X) = 1) by auto.
lets Hsize1 : sizeP_in H1 Htr.
unfold wfp_sizeP in *; simpls; nat_math.
destruct lp2.
specializes HnoIO r w; apply HnoIO.
apply permut_mem with (l := r :: nil).
apply¬ permut_sym. constructor. constructor.
simpl in Hpd21. etransitivity. Focus 2. eassumption.
symmetry. etransitivity. apply Hpd11.
apply wfp_prod_IO_permut in Hplp1´; simpls¬.
assert (r ≈ wfp_Par w (wfp_prod (w0 :: lp2))).
rewrite wfp_prod_cons in Hpd21.
etransitivity. Focus 2. eassumption.
symmetry. etransitivity. apply Hpd11.
apply wfp_prod_IO_permut in Hplp1´; simpls¬.
assert (prime r).
inverts Hpd1. rewrite× <- Forall_Mem in H3.
inverts H2. specializes H4 H1. inverts H4.
inverts Hpd22. inverts H6. false.
lets H4 : wfp_prod_cons_inv w0 lp2.
inverts Hpd22. inverts H8. inverts H9.
apply IObis_sizeP_eq in H4. apply IObis_sizeP_eq in H2.
rewrite <- wfp_sizeP_0_IO_nil in H5.
unfold wfp_sizeP in *; simpls; nat_math.
remember (w :: lp1´) as lp1´´; clear dependent lp1´; rename lp1´´ into lp1´.
lets (fp´ & Htlp2 & Hiol´) : (IObis_in_full _ _ Hio´ _ _ Htlp1).
lets (q & fq & Htq & Hmq & (lq´ & Hplq´ & Hioq´)) : (wfp_prod_in_compat _ _ _ Htlp2 Hpd22).
assert (∀ X : var, wfp_inst_Abs (AbsPar1 fr (wfp_prod lp1´)) (wfp_Gvar X) ≈ wfp_Par (wfp_inst_Abs fq (wfp_Gvar X)) (wfp_prod lq´)).
introv; jauto.
assert (Hpr : prime r) by (inverts Hpd1´; inverts¬ H3).
assert (Hpq : prime q).
rewrite <- Forall_Mem in Hpd22. specializes¬ Hpd22 Hmq.
assert (∀ X, wfp_inst_Abs (AbsPar1 fr (wfp_prod lp1´)) (wfp_Gvar X) ≈ wfp_Par (wfp_inst_Abs fr (wfp_Gvar X)) (wfp_prod lp1´)).
destruct lp1; simpls×.
assert (∀ X : var, wfp_Par (wfp_inst_Abs fr (wfp_Gvar X)) (wfp_prod lp1´) ≈ wfp_Par (wfp_inst_Abs fq (wfp_Gvar X)) (wfp_prod lq´)) by jauto.
clear H2 H1 Hioq´ Hiol´ Hio.
lets (X & _) : find_fresh (@nil process).
specializes H3 X.
set (r´ := wfp_inst_Abs fr (wfp_Gvar X)).
set (q´ := wfp_inst_Abs fq (wfp_Gvar X)).
fold r´ in H3; fold q´ in H3.
lets (lr´´ & Hpdr´´) : prime_decomposition_exists r´.
lets (lq´´ & Hpdq´´) : prime_decomposition_exists q´.
assert (prime_decomposition (wfp_Par r´ (wfp_prod lp1´)) (lr´´ ++ lp1´)).
splits.
etransitivity. Focus 2. symmetry; apply wfp_prod_IO_app.
apply¬ IObis_congr_par. inverts¬ Hpdr´´.
apply¬ Forall_app. inverts¬ Hpdr´´.
apply Forall_permut with (l2 := (r :: lp1´)) in Hpd12; auto.
inverts¬ Hpd12.
assert (prime_decomposition (wfp_Par r´ (wfp_prod lp1´)) (lq´´ ++ lq´)).
splits.
etransitivity. eassumption.
etransitivity. Focus 2. symmetry. apply wfp_prod_IO_app.
apply¬ IObis_congr_par. inverts¬ Hpdq´´.
apply¬ Forall_app. inverts¬ Hpdq´´.
apply Forall_permut with (l2 := (q :: lq´)) in Hpd22; auto.
inverts¬ Hpd22.
specializes H H1 H2.
inverts Hpd1. apply IObis_sizeP_eq in H.
assert (sizeP (wfp_Gvar X) = 1) by auto.
lets Hsize1 : sizeP_in H5 Htr.
apply wfp_prod_IO_permut in Hplp1´.
apply IObis_sizeP_eq in Hplp1´.
lets Hsize2 : wfp_prod_cons_inv r lp1´.
apply IObis_sizeP_eq in Hsize2.
unfold wfp_sizeP in *; simpls; fold r´ in Hsize1.
nat_math.
destruct H as (l1 & l2 & Hpl1 & Hpl2 & Hiol).
destruct lp1´; destruct lq´.
specializes HnoIO r q. applys¬ HnoIO.
lets Hp1 : wfp_prod_IO_permut Hplp1´.
lets Hp2 : wfp_prod_IO_permut Hplq´.
simpls×.
assert (r ≈ wfp_Par q (wfp_prod (w0 :: lq´))).
apply wfp_prod_IO_permut in Hplq´.
rewrite wfp_prod_cons in Hplq´.
etransitivity. Focus 2. symmetry; eassumption.
inverts Hpd1´; simpl in H.
etransitivity. symmetry; eassumption. auto.
inverts Hpr. specializes H5 H. inverts H5.
inverts Hpq. false.
lets H5 : wfp_prod_cons_inv w0 lq´.
apply Forall_permut with (l2 := (q :: w0 :: lq´)) in Hpd22; auto.
inverts Hpd22. inverts H10. inverts H11.
apply IObis_sizeP_eq in H6. apply IObis_sizeP_eq in H5.
rewrite <- wfp_sizeP_0_IO_nil in H7.
unfold wfp_sizeP in *; simpls; nat_math.
assert (q ≈ wfp_Par r (wfp_prod (w0 :: lp1´))).
apply wfp_prod_IO_permut in Hplp1´.
rewrite wfp_prod_cons in Hplp1´.
etransitivity. Focus 2. symmetry; eassumption.
apply wfp_prod_IO_permut in Hplq´; simpl wfp_prod in Hplq´ at 1; auto.
inverts Hpq. specializes H5 H. inverts H5.
inverts Hpr. false.
lets H5 : wfp_prod_cons_inv w0 lp1´.
apply Forall_permut with (l2 := (r :: w0 :: lp1´)) in Hpd12; auto.
inverts Hpd12. inverts H10. inverts H11.
apply IObis_sizeP_eq in H6. apply IObis_sizeP_eq in H5.
rewrite <- wfp_sizeP_0_IO_nil in H7.
unfold wfp_sizeP in *; simpls; nat_math.
assert (∀ p, Mem p l2 → ∃ q, Mem q l1 ∧ p ≈ q).
gen Hiol; clear. gen l1.
induction l2 using (measure_induction length); destruct l2.
introv _ Hm; inverts Hm.
destruct l1; introv Hf.
false¬.
inverts Hf.
specializes H H1.
rew_length; nat_math.
introv Hm; inverts Hm.
∃ w0; splits~; constructor¬.
lets (q & Hmq & Hioq) : H H3.
∃ q; splits~; repeat constructor¬.
assert (Hmw0 : Mem w1 l2).
apply permut_mem with (l := lq´´ ++ w1 :: lq´); auto.
rewrite Mem_app_or_eq; right; constructor.
lets (w2 & Hmw2 & Hiow2) : H Hmw0.
apply permut_mem with (t := lr´´ ++ w0 :: lp1´) in Hmw2; [ | apply¬ permut_sym].
rewrite Mem_app_or_eq in Hmw2; inverts Hmw2.
assert (wfp_sizeP w2 < wfp_sizeP r).
assert (sizeP (wfp_Gvar X) = 1) by auto.
lets Hsize1 : sizeP_in H5 Htr.
inverts Hpdr´´.
apply IObis_sizeP_eq in H6; clear H7.
apply wfp_prod_sizeP_mem in H4.
unfold wfp_sizeP in *; simpls; fold r´ in Hsize1; nat_math.
assert (wfp_sizeP r ≤ wfp_sizeP w1).
apply Hminr. rewrite Mem_app_or_eq; right.
apply permut_mem with (l := q :: w1 :: lq´).
apply¬ permut_sym. repeat constructor.
apply IObis_sizeP_eq in Hiow2. nat_math.
inverts H4.
specializes HnoIO w0 w1. symmetry in Hiow2. apply¬ HnoIO.
apply permut_mem with (l := r :: w0 :: lp1´).
apply¬ permut_sym. repeat constructor.
apply permut_mem with (l := q :: w1 :: lq´).
apply¬ permut_sym. repeat constructor.
specializes HnoIO w2 w1. symmetry in Hiow2. apply¬ HnoIO.
apply permut_mem with (l := r :: w0 :: lp1´).
apply¬ permut_sym. repeat constructor¬.
apply permut_mem with (l := q :: w1 :: lq´).
apply¬ permut_sym. repeat constructor.
rename lp1 into lp3. rename lp2 into lp1. rename lp3 into lp2.
rename Hpd2 into Hpd3; rename Hpd1 into Hpd2; rename Hpd3 into Hpd1.
symmetry in Hio.
lets (lp1´ & Hplp1´) : permut_mem_exists H0.
assert (Hio´ : wfp_prod (r :: lp1´) ≈ wfp_prod lp2).
etransitivity. eapply wfp_prod_IO_permut. eassumption. auto.
assert (Hpd1´ : prime_decomposition p (r :: lp1´)).
splits¬. etransitivity. Focus 2. symmetry; eassumption.
etransitivity. Focus 2. apply Hio.
inverts¬ Hpd1.
eapply Forall_permut. Focus 2. eassumption. inverts¬ Hpd1.
lets (Hpd11 & Hpd12) : Hpd1; lets (Hpd21 & Hpd22) : Hpd2.
rewrite wfp_sizeP_S_tr in Hsr.
inverts Hsr as Hsr.
destruct Hsr as (X & r´ & Htr).
lets Htlp1 : wfp_prod_trans_rem lp1´ Htr.
lets (lp2´ & Htlp2 & Hio´´) : IObis_var Hio´ Htlp1.
lets (q & q´ & Hmq´ & Htq´ & (lq´ & Hplq´ & Hioq´)) : wfp_prod_rem_compat Htlp2 Hpd22.
assert (HioM : wfp_prod (r´ :: lp1´) ≈ wfp_prod (q´ :: lq´)) by jauto.
assert (Hpr : prime r) by (inverts Hpd1´; inverts¬ H2).
assert (Hpq : prime q).
rewrite <- Forall_Mem in Hpd22. specializes¬ Hpd22 Hmq´.
lets (Hio_r & _) : prime_remove Hpr Htr.
lets (Hio_q & _) : prime_remove Hpq Htq´.
specializes HnoIO Hmq´ H0; apply HnoIO.
inverts Hsr as Hsr. Focus 2.
destruct Hsr as (a & r´ & r´´ & Htr).
lets Htlp1 : wfp_prod_trans_out lp1´ Htr.
lets (lp2´ & lp2´´ & Htlp2 & Hiol´ & Hiol´´) : IObis_out Hio´ Htlp1.
lets (q & q´ & Hmq´ & Htq´ & (lq´ & Hplq´ & Hioq´)) : wfp_prod_out_compat Htlp2 Hpd22.
assert (HioM : wfp_prod (r´ :: lp1´) ≈ wfp_prod (q´ :: lq´)) by jauto.
assert (Hpr : prime r) by (inverts Hpd1´; inverts¬ H2).
assert (Hpq : prime q).
rewrite <- Forall_Mem in Hpd22. specializes¬ Hpd22 Hmq´.
lets (Hio_r & _) : prime_out Hpr Htr.
lets (Hio_q & _) : prime_out Hpq Htq´.
specializes HnoIO Hmq´ H0; apply HnoIO.
etransitivity. eassumption.
etransitivity. Focus 2. symmetry; eassumption.
apply¬ IObis_congr_send.
destruct Hsr as (a & fr & Htr).
lets Htlp1 : wfp_prod_trans_in lp1´ Htr; destruct lp1´.
clear Htlp1. destruct lp2.
apply IObis_sizeP_eq in Hpd21. apply IObis_sizeP_eq in Hio´.
lets (X & _) : find_fresh (@nil process).
assert (sizeP (wfp_Gvar X) = 1) by auto.
lets Hsize1 : sizeP_in H1 Htr.
unfold wfp_sizeP in *; simpls; nat_math.
destruct lp2.
specializes HnoIO w r; apply HnoIO.
constructor.
apply permut_mem with (l := r :: nil).
apply¬ permut_sym. constructor.
simpl in Hpd21. etransitivity. symmetry; eassumption.
etransitivity. apply Hpd11.
apply wfp_prod_IO_permut in Hplp1´; simpls¬.
assert (r ≈ wfp_Par w (wfp_prod (w0 :: lp2))).
rewrite wfp_prod_cons in Hpd21.
etransitivity. Focus 2. eassumption.
symmetry. etransitivity. apply Hpd11.
apply wfp_prod_IO_permut in Hplp1´; simpls¬.
assert (prime r).
inverts Hpd1. rewrite× <- Forall_Mem in H3.
inverts H2. specializes H4 H1. inverts H4.
inverts Hpd22. inverts H6. false.
lets H4 : wfp_prod_cons_inv w0 lp2.
inverts Hpd22. inverts H8. inverts H9.
apply IObis_sizeP_eq in H4. apply IObis_sizeP_eq in H2.
rewrite <- wfp_sizeP_0_IO_nil in H5.
unfold wfp_sizeP in *; simpls; nat_math.
remember (w :: lp1´) as lp1´´; clear dependent lp1´; rename lp1´´ into lp1´.
lets (fp´ & Htlp2 & Hiol´) : (IObis_in_full _ _ Hio´ _ _ Htlp1).
lets (q & fq & Htq & Hmq & (lq´ & Hplq´ & Hioq´)) : (wfp_prod_in_compat _ _ _ Htlp2 Hpd22).
assert (∀ X : var, wfp_inst_Abs (AbsPar1 fr (wfp_prod lp1´)) (wfp_Gvar X) ≈ wfp_Par (wfp_inst_Abs fq (wfp_Gvar X)) (wfp_prod lq´)).
introv; jauto.
assert (Hpr : prime r) by (inverts Hpd1´; inverts¬ H3).
assert (Hpq : prime q).
rewrite <- Forall_Mem in Hpd22. specializes¬ Hpd22 Hmq.
assert (∀ X, wfp_inst_Abs (AbsPar1 fr (wfp_prod lp1´)) (wfp_Gvar X) ≈ wfp_Par (wfp_inst_Abs fr (wfp_Gvar X)) (wfp_prod lp1´)).
destruct lp1´; simpls×.
assert (∀ X : var, wfp_Par (wfp_inst_Abs fr (wfp_Gvar X)) (wfp_prod lp1´) ≈ wfp_Par (wfp_inst_Abs fq (wfp_Gvar X)) (wfp_prod lq´)) by jauto.
clear H2 H1 Hioq´ Hiol´ Hio.
lets (X & _) : find_fresh (@nil process).
specializes H3 X.
set (r´ := wfp_inst_Abs fr (wfp_Gvar X)).
set (q´ := wfp_inst_Abs fq (wfp_Gvar X)).
fold r´ in H3; fold q´ in H3.
lets (lr´´ & Hpdr´´) : prime_decomposition_exists r´.
lets (lq´´ & Hpdq´´) : prime_decomposition_exists q´.
assert (prime_decomposition (wfp_Par r´ (wfp_prod lp1´)) (lr´´ ++ lp1´)).
splits.
etransitivity. Focus 2. symmetry; apply wfp_prod_IO_app.
apply¬ IObis_congr_par. inverts¬ Hpdr´´.
apply¬ Forall_app. inverts¬ Hpdr´´.
apply Forall_permut with (l2 := (r :: lp1´)) in Hpd12; auto.
inverts¬ Hpd12.
assert (prime_decomposition (wfp_Par r´ (wfp_prod lp1´)) (lq´´ ++ lq´)).
splits.
etransitivity. eassumption.
etransitivity. Focus 2. symmetry. apply wfp_prod_IO_app.
apply¬ IObis_congr_par. inverts¬ Hpdq´´.
apply¬ Forall_app. inverts¬ Hpdq´´.
apply Forall_permut with (l2 := (q :: lq´)) in Hpd22; auto.
inverts¬ Hpd22.
specializes H H1 H2.
inverts Hpd1. apply IObis_sizeP_eq in H.
assert (sizeP (wfp_Gvar X) = 1) by auto.
lets Hsize1 : sizeP_in H5 Htr.
apply wfp_prod_IO_permut in Hplp1´.
apply IObis_sizeP_eq in Hplp1´.
lets Hsize2 : wfp_prod_cons_inv r lp1´.
apply IObis_sizeP_eq in Hsize2.
unfold wfp_sizeP in *; simpls; fold r´ in Hsize1.
nat_math.
destruct H as (l1 & l2 & Hpl1 & Hpl2 & Hiol).
destruct lp1´; destruct lq´.
specializes HnoIO q r. applys¬ HnoIO.
lets Hp1 : wfp_prod_IO_permut Hplp1´.
lets Hp2 : wfp_prod_IO_permut Hplq´.
simpls×.
assert (r ≈ wfp_Par q (wfp_prod (w0 :: lq´))).
apply wfp_prod_IO_permut in Hplq´.
rewrite wfp_prod_cons in Hplq´.
etransitivity. Focus 2. symmetry; eassumption.
inverts Hpd1´; simpl in H.
etransitivity. symmetry; eassumption. auto.
inverts Hpr. specializes H5 H. inverts H5.
inverts Hpq. false.
lets H5 : wfp_prod_cons_inv w0 lq´.
apply Forall_permut with (l2 := (q :: w0 :: lq´)) in Hpd22; auto.
inverts Hpd22. inverts H10. inverts H11.
apply IObis_sizeP_eq in H6. apply IObis_sizeP_eq in H5.
rewrite <- wfp_sizeP_0_IO_nil in H7.
unfold wfp_sizeP in *; simpls; nat_math.
assert (q ≈ wfp_Par r (wfp_prod (w0 :: lp1´))).
apply wfp_prod_IO_permut in Hplp1´.
rewrite wfp_prod_cons in Hplp1´.
etransitivity. Focus 2. symmetry; eassumption.
apply wfp_prod_IO_permut in Hplq´; simpl wfp_prod in Hplq´ at 1; auto.
inverts Hpq. specializes H5 H. inverts H5.
inverts Hpr. false.
lets H5 : wfp_prod_cons_inv w0 lp1´.
apply Forall_permut with (l2 := (r :: w0 :: lp1´)) in Hpd12; auto.
inverts Hpd12. inverts H10. inverts H11.
apply IObis_sizeP_eq in H6. apply IObis_sizeP_eq in H5.
rewrite <- wfp_sizeP_0_IO_nil in H7.
unfold wfp_sizeP in *; simpls; nat_math.
assert (∀ p, Mem p l2 → ∃ q, Mem q l1 ∧ p ≈ q).
gen Hiol; clear. gen l1.
induction l2 using (measure_induction length); destruct l2.
introv _ Hm; inverts Hm.
destruct l1; introv Hf.
false¬.
inverts Hf.
specializes H H1.
rew_length; nat_math.
introv Hm; inverts Hm.
∃ w0; splits~; constructor¬.
lets (q & Hmq & Hioq) : H H3.
∃ q; splits~; repeat constructor¬.
assert (Hmw0 : Mem w1 l2).
apply permut_mem with (l := lq´´ ++ w1 :: lq´); auto.
rewrite Mem_app_or_eq; right; constructor.
lets (w2 & Hmw2 & Hiow2) : H Hmw0.
apply permut_mem with (t := lr´´ ++ w0 :: lp1´) in Hmw2; [ | apply¬ permut_sym].
rewrite Mem_app_or_eq in Hmw2; inverts Hmw2.
assert (wfp_sizeP w2 < wfp_sizeP r).
assert (sizeP (wfp_Gvar X) = 1) by auto.
lets Hsize1 : sizeP_in H5 Htr.
inverts Hpdr´´.
apply IObis_sizeP_eq in H6; clear H7.
apply wfp_prod_sizeP_mem in H4.
unfold wfp_sizeP in *; simpls; fold r´ in Hsize1; nat_math.
assert (wfp_sizeP r ≤ wfp_sizeP w1).
apply Hminr. rewrite Mem_app_or_eq; left.
apply permut_mem with (l := q :: w1 :: lq´).
apply¬ permut_sym. repeat constructor.
apply IObis_sizeP_eq in Hiow2. nat_math.
inverts H4.
specializes HnoIO w1 w0. apply¬ HnoIO.
apply permut_mem with (l := q :: w1 :: lq´).
apply¬ permut_sym. repeat constructor.
apply permut_mem with (l := r :: w0 :: lp1´).
apply¬ permut_sym. repeat constructor.
specializes HnoIO w1 w2. apply¬ HnoIO.
apply permut_mem with (l := q :: w1 :: lq´).
apply¬ permut_sym. repeat constructor.
apply permut_mem with (l := r :: w0 :: lp1´).
apply¬ permut_sym. repeat constructor¬.
Qed.
Lemma prime_send : ∀ a p´, prime (wfp_Send a p´).
Proof with automate.
introv; splits.
intro Hio; rewrite <- wfp_sizeP_0_IO_nil in Hio.
unfold wfp_sizeP in Hio; simpls; nat_math.
introv Hio; destruct Hio as (R & Hio & Hr).
lets Hio´ : Hio; destruct Hio´ as (_ & _ & Ho & _).
specializes Ho Hr.
assert ({{wfp_Send a p´ -- LabOut a p´ ->> AP wfp_Nil}}) by constructor.
specializes Ho H; destruct Ho as (q´ & q´´ & Ht & r´ & r´´).
assert (Hq´ : wfp_Nil ≈ q´) by (∃ R; splits*).
symmetry in Hq´; rewrite <- wfp_sizeP_0_IO_nil in Hq´; clear r´.
inverts Ht...
destruct ap; inverts H4.
right; rewrite <- wfp_sizeP_0_IO_nil.
unfold wfp_sizeP in *; simpls; nat_math.
destruct aq; inverts H4.
left; rewrite <- wfp_sizeP_0_IO_nil.
unfold wfp_sizeP in *; simpls; nat_math.
Qed.
Lemma prime_gvar : ∀ X, prime (wfp_Gvar X).
Proof with automate.
introv; splits.
intro Hio; rewrite <- wfp_sizeP_0_IO_nil in Hio.
unfold wfp_sizeP in Hio; simpls; nat_math.
introv Hio; destruct Hio as (R & Hio & Hr).
lets Hio´ : Hio; destruct Hio´ as (_ & _ & _ & Hv).
specializes Hv Hr.
assert ({{wfp_Gvar X -- LabRem X ->> AP wfp_Nil}}) by constructor.
specializes Hv H; destruct Hv as (q´ & Ht & r´).
assert (Hq´ : wfp_Nil ≈ q´) by (∃ R; splits*).
symmetry in Hq´; rewrite <- wfp_sizeP_0_IO_nil in Hq´; clear r´.
inverts Ht...
destruct ap; inverts H4.
right; rewrite <- wfp_sizeP_0_IO_nil.
unfold wfp_sizeP in *; simpls; nat_math.
destruct aq; inverts H4.
left; rewrite <- wfp_sizeP_0_IO_nil.
unfold wfp_sizeP in *; simpls; nat_math.
Qed.
Lemma not_prime_nil : ¬ prime wfp_Nil.
Proof.
introv (Hr & _); jauto.
Qed.
Fixpoint wfp_prod_In (l : list (chan × var × wfprocess)) :=
match l with
| nil ⇒ wfp_Nil
| (a, X, p) :: nil ⇒ wfp_Abs a X p
| (a, X, p) :: l ⇒ wfp_Par (wfp_Abs a X p) (wfp_prod_In l)
end.
Lemma wfp_prod_In_cons : ∀ a X p b c,
wfp_prod_In ((a, X, p) :: b :: c) = wfp_Par (wfp_Abs a X p) (wfp_prod_In (b :: c)).
Proof.
auto.
Qed.
Lemma wfp_prod_In_app : ∀ l a X p,
wfp_prod_In ((a, X, p) :: l) ≡* wfp_Par (wfp_Abs a X p) (wfp_prod_In l).
Proof.
induction l using (measure_induction length).
destruct l. simpl. constructor. apply WfCgrPar_nil1.
introv; rewrite wfp_prod_In_cons. repeat constructor.
Qed.
Lemma wfp_prod_In_par_app : ∀ l1 l2,
wfp_Par (wfp_prod_In l1) (wfp_prod_In l2) ≡* wfp_prod_In (l1 ++ l2).
Proof.
induction l1 using (measure_induction length).
destruct l1; introv.
rewrite app_nil_l; simpl.
etransitivity. constructor. apply WfCgrPar_com.
etransitivity. constructor. apply WfCgrPar_nil2.
repeat constructor.
destruct l1.
rewrite app_cons_one. clear H.
destruct p as (a & p). destruct a as (a & X). simpl wfp_prod_In at 1.
etransitivity. Focus 2. symmetry. apply wfp_prod_In_app. repeat constructor.
destruct p as ((a & X) & p). rewrite wfp_prod_In_cons.
etransitivity. constructor. apply WfCgrPar_assoc2.
rewrite <- app_cons_one at 2. rewrite app_cons.
etransitivity. Focus 2. symmetry. apply wfp_prod_In_app.
apply wfcgr_par. repeat constructor.
rewrite app_cons_one. apply H.
rew_length; nat_math.
Qed.
Fixpoint wfp_prod_Out (l : list (chan × wfprocess)) :=
match l with
| nil ⇒ wfp_Nil
| (a, p) :: nil ⇒ wfp_Send a p
| (a, p) :: l ⇒ wfp_Par (wfp_Send a p) (wfp_prod_Out l)
end.
Lemma wfp_prod_Out_cons : ∀ a p b c,
wfp_prod_Out ((a, p) :: b :: c) = wfp_Par (wfp_Send a p) (wfp_prod_Out (b :: c)).
Proof.
auto.
Qed.
Lemma wfp_prod_Out_app : ∀ l a p,
wfp_prod_Out ((a, p) :: l) ≡* wfp_Par (wfp_Send a p) (wfp_prod_Out l).
Proof.
induction l using (measure_induction length).
destruct l. simpl. constructor. apply WfCgrPar_nil1.
introv; rewrite wfp_prod_Out_cons. repeat constructor.
Qed.
Lemma wfp_prod_Out_par_app : ∀ l1 l2,
wfp_Par (wfp_prod_Out l1) (wfp_prod_Out l2) ≡* wfp_prod_Out (l1 ++ l2).
Proof.
induction l1 using (measure_induction length).
destruct l1; introv.
rewrite app_nil_l; simpl.
etransitivity. constructor. apply WfCgrPar_com.
etransitivity. constructor. apply WfCgrPar_nil2.
repeat constructor.
destruct l1.
rewrite app_cons_one. clear H.
destruct p as (a & p). simpl wfp_prod_Out at 1.
etransitivity. Focus 2. symmetry. apply wfp_prod_Out_app. repeat constructor.
destruct p as (a & p). rewrite wfp_prod_Out_cons.
etransitivity. constructor. apply WfCgrPar_assoc2.
rewrite <- app_cons_one at 2. rewrite app_cons.
etransitivity. Focus 2. symmetry. apply wfp_prod_Out_app.
apply wfcgr_par. repeat constructor.
rewrite app_cons_one. apply H.
rew_length; nat_math.
Qed.
Fixpoint wfp_prod_Var (lx : list var) :=
match lx with
| nil ⇒ wfp_Nil
| X :: nil ⇒ wfp_Gvar X
| X :: lx ⇒ wfp_Par (wfp_Gvar X) (wfp_prod_Var lx)
end.
Lemma wfp_prod_Var_cons : ∀ X b c,
wfp_prod_Var (X :: b :: c) = wfp_Par (wfp_Gvar X) (wfp_prod_Var (b :: c)).
Proof.
auto.
Qed.
Lemma wfp_prod_Var_app : ∀ l X,
wfp_prod_Var (X :: l) ≡* wfp_Par (wfp_Gvar X) (wfp_prod_Var l).
Proof.
induction l using (measure_induction length).
destruct l. simpl. constructor. apply WfCgrPar_nil1.
introv; rewrite wfp_prod_Var_cons. repeat constructor.
Qed.
Lemma wfp_prod_Var_par_app : ∀ l1 l2,
wfp_Par (wfp_prod_Var l1) (wfp_prod_Var l2) ≡* wfp_prod_Var (l1 ++ l2).
Proof.
induction l1 using (measure_induction length).
destruct l1; introv.
rewrite app_nil_l; simpl.
etransitivity. constructor. apply WfCgrPar_com.
etransitivity. constructor. apply WfCgrPar_nil2.
repeat constructor.
destruct l1.
rewrite app_cons_one. clear H.
simpl wfp_prod_Var at 1.
etransitivity. Focus 2. symmetry. apply wfp_prod_Var_app. repeat constructor.
rewrite wfp_prod_Var_cons.
etransitivity. constructor. apply WfCgrPar_assoc2.
rewrite <- app_cons_one at 2. rewrite app_cons.
etransitivity. Focus 2. symmetry. apply wfp_prod_Var_app.
apply wfcgr_par. repeat constructor.
rewrite app_cons_one. apply H.
rew_length; nat_math.
Qed.
Lemma wfprocess_list_prime_separation : ∀ lp,
Forall (fun p : wfprocess ⇒ prime p) lp →
∃ (li : list (chan × var × wfprocess)),
∃ (lo : list (chan × wfprocess)),
∃ (lv : list var),
wfp_prod lp ≈ wfp_Par (wfp_prod_In li) (wfp_Par (wfp_prod_Out lo) (wfp_prod_Var lv)) ∧
(∀ a X p, Mem (a, X, p) li → prime (wfp_Abs a X p)) ∧
(∀ a p, Mem (a, p) lo → prime (wfp_Send a p)).
Proof with automate.
induction lp using (measure_induction length). destruct lp.
clear H. introv Hf; simpl.
∃ (@nil (chan × var × wfprocess)).
∃ (@nil (chan × wfprocess)).
∃ (@nil var). simpls. splits.
∃ wfcgr; splits. apply congr_IObisimulation.
etransitivity. constructor. apply WfCgrPar_nil1.
etransitivity. Focus 2. constructor. apply WfCgrPar_com.
etransitivity. constructor. apply WfCgrPar_nil1.
repeat constructor.
introv Hmem. rewrite Mem_nil_eq in Hmem; intuition.
introv Hmem. rewrite Mem_nil_eq in Hmem; intuition.
introv Hf. inverts Hf. destruct lp.
simpls. clear H3 H.
induction w using (measure_induction wfp_size). destruct_wf w.
∃ (@nil (chan × var × wfprocess)).
∃ ((a, p) :: nil).
∃ (@nil var). simpls. splits.
∃ wfcgr; splits. apply congr_IObisimulation.
etransitivity. constructor. apply WfCgrPar_nil1.
etransitivity. constructor. apply WfCgrPar_nil1.
etransitivity. Focus 2. constructor. apply WfCgrPar_com.
repeat constructor.
introv Hmem. rewrite Mem_nil_eq in Hmem; intuition.
introv Hyp; inverts Hyp. auto. rewrite Mem_nil_eq in H1; intuition.
∃ ((a, X, p) :: nil).
∃ (@nil (chan × wfprocess)).
∃ (@nil var). simpls. splits.
∃ wfcgr; splits. apply congr_IObisimulation.
etransitivity. constructor. apply WfCgrPar_nil1.
etransitivity. constructor. apply WfCgrPar_nil1.
etransitivity. constructor. apply WfCgrPar_assoc2.
repeat constructor.
introv Hyp; inverts Hyp. auto. rewrite Mem_nil_eq in H1; intuition.
introv Hmem. rewrite Mem_nil_eq in Hmem; intuition.
∃ (@nil (chan × var × wfprocess)).
∃ (@nil (chan × wfprocess)).
∃ (X :: nil). simpls. splits.
∃ wfcgr; splits. apply congr_IObisimulation.
etransitivity. Focus 2. constructor. apply WfCgrPar_com.
etransitivity. Focus 2. constructor. apply WfCgrPar_nil1.
etransitivity. constructor. apply WfCgrPar_nil1.
etransitivity. Focus 2. constructor. apply WfCgrPar_com.
repeat constructor.
introv Hmem. rewrite Mem_nil_eq in Hmem; intuition.
introv Hmem. rewrite Mem_nil_eq in Hmem; intuition.
Focus 2.
∃ (@nil (chan × var × wfprocess)).
∃ (@nil (chan × wfprocess)).
∃ (@nil var). simpls. splits.
∃ wfcgr; splits. apply congr_IObisimulation.
etransitivity. constructor. apply WfCgrPar_nil1.
etransitivity. Focus 2. constructor. apply WfCgrPar_com.
etransitivity. constructor. apply WfCgrPar_nil1.
repeat constructor.
introv Hmem. rewrite Mem_nil_eq in Hmem; intuition.
introv Hmem. rewrite Mem_nil_eq in Hmem; intuition.
assert (Hs1 : wfp_size p1 < wfp_size (wfp_Par p1 p2)) by automate.
assert (Hs2 : wfp_size p2 < wfp_size (wfp_Par p1 p2)) by automate.
apply prime_parallel in H2; inverts H2 as H2.
destruct H2 as (Hp1 & Hp2).
lets (li1 & lo1 & lv1 & Hc1) : H Hs1. auto.
destruct Hc1 as (Hiop & Hf1 & Hf2).
clear H Hs1 Hs2.
∃ li1 lo1 lv1. splits×.
etransitivity. apply IObis_congr_par. reflexivity. eassumption.
etransitivity. ∃ wfcgr. splits. apply congr_IObisimulation.
constructor. apply WfCgrPar_nil2. auto.
destruct H2 as (Hp2 & Hp1).
lets (li2 & lo2 & lv2 & Hc2) : H Hs2. auto.
destruct Hc2 as (Hiop & Hf1 & Hf2).
clear H Hs1 Hs2.
∃ li2 lo2 lv2. splits×.
etransitivity. apply IObis_congr_par. eassumption. reflexivity.
etransitivity. ∃ wfcgr. splits. apply congr_IObisimulation.
constructor. apply WfCgrPar_com.
etransitivity. ∃ wfcgr. splits. apply congr_IObisimulation.
constructor. apply WfCgrPar_nil2. auto.
lets H´ : H; specializes H H3. rew_length; nat_math.
destruct H as (li´´ & lo´´ & lv´´ & Hio´´ & Hf1´´ & Hf2´´).
assert (length (w :: nil) < length (w :: w0 :: lp)) by (rew_length; nat_math).
assert (Forall (fun p ⇒ prime p) (w :: nil)) by (repeat constructor~).
specializes¬ H´ H0.
destruct H´ as (li´ & lo´ & lv´ & Hio´ & Hf1´ & Hf2´).
∃ (li´ ++ li´´) (lo´ ++ lo´´) (lv´ ++ lv´´). splits.
rewrite wfp_prod_cons. simpl in Hio´.
etransitivity. apply IObis_congr_par. eassumption. eassumption.
∃ wfcgr. splits. apply congr_IObisimulation.
etransitivity. constructor. apply WfCgrPar_assoc1.
etransitivity. apply wfcgr_par. constructor. apply WfCgrPar_com. reflexivity.
etransitivity. apply wfcgr_par. constructor. apply WfCgrPar_assoc1. reflexivity.
etransitivity. apply wfcgr_par. apply wfcgr_par. constructor. apply WfCgrPar_com. reflexivity. reflexivity.
etransitivity. constructor. apply WfCgrPar_assoc2.
apply wfcgr_par. apply wfp_prod_In_par_app.
etransitivity. constructor. apply WfCgrPar_assoc1.
etransitivity. apply wfcgr_par. constructor. apply WfCgrPar_com. reflexivity.
etransitivity. apply wfcgr_par. constructor. apply WfCgrPar_assoc1. reflexivity.
etransitivity. apply wfcgr_par. apply wfcgr_par. constructor. apply WfCgrPar_com. reflexivity. reflexivity.
etransitivity. constructor. apply WfCgrPar_assoc2.
apply wfcgr_par. apply wfp_prod_Out_par_app.
apply wfp_prod_Var_par_app.
introv Hyp. rewrite Mem_app_or_eq in Hyp; inverts Hyp.
intuition. intuition.
introv Hyp. rewrite Mem_app_or_eq in Hyp; inverts Hyp.
intuition. intuition.
Qed.
Lemma wfprocess_prime_separation : ∀ p,
∃ (li : list (chan × var × wfprocess)),
∃ (lo : list (chan × wfprocess)),
∃ (lv : list var),
p ≈ wfp_Par (wfp_prod_In li) (wfp_Par (wfp_prod_Out lo) (wfp_prod_Var lv)) ∧
(∀ a X p, Mem (a, X, p) li → prime (wfp_Abs a X p)) ∧
(∀ a p, Mem (a, p) lo → prime (wfp_Send a p)).
Proof.
introv; lets (lp & Hio & Hf) : prime_decomposition_exists p.
lets (li & lo & lv & Hio´ & Hf1 & Hf2) : wfprocess_list_prime_separation Hf.
∃ li lo lv; splits×.
Qed.