Library HOC12Guarded

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 HOC09GVLemmas.
Require Import HOC10CongrLemmas.
Require Import HOC11TransLemmas.

Inductive guarded (X:var) : wfprocess → Prop :=
  | GuSend : ∀ a p, (guarded X (wfp_Send a p))
  | GuReceive : ∀ a Y p, (guarded X (wfp_Abs a Y p))
  | GuGvar : ∀ Y, X≠Y → (guarded X (wfp_Gvar Y))
  | GuPar : ∀ p q, (guarded X p) → (guarded X q) → (guarded X (wfp_Par p q))
  | GuNil : (guarded X wfp_Nil).

Hint Resolve GuSend GuReceive GuGvar GuPar GuNil.

Fixpoint size_unguardedX X p : nat :=
  match p with
    | Send _ p ⇒ 0
    | Receive _ x p ⇒ 0
    | Lvar x ⇒ 0
    | Gvar Y ⇒ ifb (X=Y) then 1 else 0
    | Par p1 p2 ⇒ (size_unguardedX X p1) + (size_unguardedX X p2)
    | Nil ⇒ 0
  end.

Fixpoint unguardeds p :=
  match p with
    | Send _ _ ⇒ \{}
    | Receive _ _ _ ⇒ \{}
    | Lvar _ ⇒ \{}
    | Gvar X ⇒ \{X}
    | Par p´ p´´ ⇒ (unguardeds p´) \u (unguardeds p´´)
    | Nil ⇒ \{}
  end.

Definition guarded_proc p : Prop := ∀ X, guarded X p.

Notation "@@ p " := (guarded_proc p) (at level 60).

Lemma guarded_size_unguardedX : ∀ X p,
  guarded X p ↔ size_unguardedX X p = 0.
Proof with automate.
  split; intros.
    induction H; simpls¬.
      cases_if¬.
      omega.
    gen X; induction p using (measure_induction wfp_size); introv Hs.
    destruct_wf p...
      constructor; simpls; cases_if×.
      constructor; simpls; apply H...
Qed.

Require Import Relations.

Instance guarded_decidable : ∀ X p, Decidable (guarded X p).
Proof.
  introv. apply prop_decidable.
Qed.


Lemma wfp_not_guarded_unguarded : ∀ X (p : wfprocess),
  ¬ guarded X p → ∃ (p´ : wfprocess), {{p -- LabRem X ->> (AP p´)}}.
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv Ht; try solve [false; apply¬ Ht].
  tests: (X = X0).
    ∃ wfp_Nil...
    false; apply¬ Ht.
  tests : (guarded X p1); tests : (guarded X p2).
    false; apply ¬Ht.
    specializes H C0... destruct H. ∃ (wfp_Par p1 x)...
    specializes H C... destruct H. ∃ (wfp_Par x p2)...
    specializes H C... destruct H. ∃ (wfp_Par x p2)...
Qed.

Lemma wfp_remove_congr : ∀ X p p´,
  {{p -- LabRem X ->> (AP p´)}} → p ≡* (wfp_Par p´ (wfp_Gvar X)).
Proof with (try solve [applys× t_step]; automate).
  introv Ht; inductions Ht...
    etransitivity. Focus 2. constructor. apply WfCgrPar_com. auto...
    destruct ap; inverts x.
      etransitivity. apply wfcgr_par1. apply¬ (IHHt w).
      etransitivity. Focus 2. constructor. apply WfCgrPar_assoc1.
      etransitivity. constructor. apply WfCgrPar_assoc2.
      apply wfcgr_par...
    destruct aq; inverts x.
      etransitivity. Focus 2. constructor. apply WfCgrPar_assoc1.
      apply wfcgr_par...
Qed.

Lemma size_unguardedX_remove : ∀ X p p´,
  {{p -- LabRem X ->> (AP p´)}} → size_unguardedX X p = S (size_unguardedX X p´).
Proof.
  introv Ht; inductions Ht; simpls.
  cases_if¬.
  destruct ap; inversion x; subst. simpl.
  rewrite (IHHt w); trivial.
  destruct aq; inversion x; subst. simpl.
  rewrite (IHHt w); trivial. nat_math.
Qed.

Lemma wfp_guarded_out : ∀ p a X p´ p´´,
  guarded X p → {{p -- LabOut a p´´ ->> AP p´}} → guarded X p´.
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv Hg Ht; inverts Ht...
    destruct ap; inverts H4; inverts Hg...
    constructor... eapply H... auto...
    destruct aq; inverts H4; inverts Hg...
    constructor... eapply H with (y := p2)...
Qed.

Lemma wfp_guarded_subst_trans_out : ∀ X (p : wfprocess), (guarded X p)
  → ∀ a q (p1´ p1´´ : wfprocess), {{wfp_subst q X p --LabOut a p1´´->>AP p1´}} → ∃ (p´ p´´ : wfprocess), {{p--LabOut a p´´->>AP p´}} ∧ p1´ = (wfp_subst q X p´) ∧ p1´´ = (wfp_subst q X p´´).
Proof with automate.
  introv Hgu; inductions Hgu; introv Ht; rewrite_wfp_subst; inverts Ht...

  ∃ wfp_Nil p; splits...
  cases_if×. cases_if×. cases_if×.

  destruct ap; inverts H3.
  specializes IHHgu1 H2.
  destruct IHHgu1 as [p´ [p´´ [Ht2 [Heq1 Heq2]]]].
  subst. ∃ (wfp_Par p´ q) p´´. splits...

  destruct aq; inverts H3.
  specializes IHHgu2 H2.
  destruct IHHgu2 as [q´ [q´´ [Ht2 [Heq1 Heq2]]]].
  subst. ∃ (wfp_Par p q´) q´´. splits...
Qed.

Lemma wfp_guarded_subst_trans_remove : ∀ X p, (guarded X p)
  → ∀ Z q p1´, {{(wfp_subst q X p)--LabRem Z->>(AP p1´)}} → ∃ p´, {{p--LabRem Z->>(AP p´)}} ∧ p1´ = (wfp_subst q X p´).
Proof with automate.
  introv Hgu; inductions Hgu; introv Ht; rewrite_wfp_subst; inverts Ht...
    cases_if×. rewrite <- H1. ∃ wfp_Nil. splits...
    cases_if×. cases_if×.

    destruct ap; inverts H3.
    specializes IHHgu1 H2.
    destruct IHHgu1 as [p´ [Ht1 Heq1]]...
    subst. ∃ (wfp_Par p´ q). splits...

    destruct aq; inverts H3.
    specializes IHHgu2 H2.
    destruct IHHgu2 as [q´ [Ht1 Heq1]]...
    subst. ∃ (wfp_Par p q´). splits...
Qed.

Lemma wfp_guarded_remove_subst : ∀ X Y p p´ r,
  guarded X p → {{p--LabRem Y->>(AP p´)}} → {{(wfp_subst r X p)--LabRem Y->>(AP (wfp_subst r X p´))}}.
Proof with automate.
  introv Hgu Ht. gen X r; inductions Ht; introv Hgu; introv...
    cases_if×. inverts× Hgu.

    destruct ap; inverts Hgu; inverts x...
    destruct aq; inverts Hgu; inverts x...
Qed.

Lemma wfp_guarded_remove : ∀ X Y p p´,
  guarded X p → {{p--LabRem Y->>(AP p´)}} → guarded X p´.
Proof with automate.
  introv Hgu Ht; gen X; inductions Ht; introv Hgu...
    destruct ap; inverts Hgu; inverts x...
    destruct aq; inverts Hgu; inverts x...
Qed.

Lemma wfp_guarded_subst_trans_in : ∀ X (p : wfprocess), (guarded X p)
  → ∀ a (q : wfprocess) fp1, {{wfp_subst q X p --LabIn a ->> AA fp1}} →
     ∃ fp, {{p--LabIn a->>AA fp}} ∧
     ∀ Y, X≠Y → wfp_inst_Abs fp1 (wfp_Gvar Y) = wfp_subst q X (wfp_inst_Abs fp (wfp_Gvar Y)).
Proof with automate.
  introv Hgu; inductions Hgu; introv Ht; try solve [inverts Ht]...

  tests : (X = Y).
    rewrite wfp_gfresh_subst_rewrite in Ht.
    lets Heq : wfp_trans_in_chan_eq Ht; subst.
    lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp as Hyp; subst.
    eexists; splits...
      introv Hneq; simpl.
      rewrite wfp_gfresh_subst_rewrite with (q := q); auto.
        simpl; fresh_solve.
    destruct Hyp as (Z & Hneqz & Hfz & Heq); subst.
    eexists; splits...
      introv Hneq; simpl.
      rewrite wfp_gfresh_subst_rewrite with (q := q); auto.
      simpl. rewrite¬ <- subst_decomposition_g; fresh_solve.
    simpls; unfold Abs; rewrite gfresh_receive; fresh_solve.

    lets Hyp : wfp_eq_subst_abs3 q a p C.
    lets (Z & Hfz) : find_fresh (Gvar X :: proc p :: proc q :: nil).
    rewrite Forall_to_conj_3 in Hfz; destruct Hfz as (Hfzx & Hfzp & Hfzq).
    specializes¬ Hyp Hfzp. rewrite Hyp in Ht; clear Hyp.
    lets Heq : wfp_trans_in_chan_eq Ht; subst.
    lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp as Hyp; subst.
      eexists; splits...
      introv Hneq; simpl.
      rewrite wfp_substs_commute_gg; simpl; freshen_up.
      rewrite¬ <- wfp_subst_decomposition_g.

      destruct Hyp as (Z´ & Hneqz´ & Hfz´ & Heq); subst.
      eexists; splits...
      introv Hneq; simpl.
      rewrite¬ <- wfp_subst_decomposition_g.
      rewrite wfp_substs_commute_gg; simpl; freshen_up.
      rewrite¬ <- wfp_subst_decomposition_g.

  cases_if; inverts Ht.

  inverts Ht...
    destruct ap; inverts H3.
    specializes IHHgu1 H2.
    destruct IHHgu1 as [fp [Ht Hyp]].
    ∃ (AbsPar1 fp q); simpls; splits...
      introv Hneq... fequals...
    destruct aq; inverts H3.
    specializes IHHgu2 H2.
    destruct IHHgu2 as [fq [Ht Hyp]].
    ∃ (AbsPar2 p fq); simpls; splits...
      introv Hneq... fequals...
Qed.


Lemma unguardeds_spec: ∀ (p : wfprocess) X, X \notin (unguardeds p) = guarded X p.
Proof with automate.
  introv. extens. gen X.
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv; simpls; splits...

  introv Hg; inverts Hg. rewrite¬ notin_singleton.
  rewrite notin_union; introv [Hg1 Hg2]; constructor; rewrite <- H...

  introv Hg; inverts Hg; rewrite¬ notin_union; split; apply H...
Qed.

Lemma unguardeds_invariant: ∀ X p, X \in unguardeds p → X \in GV p.
Proof.
  introv H. induction p; simpls~; try (rewrite in_empty in H; false).
    rewrite in_union in H. rewrite in_union. destruct H.
      left¬.
      right¬.
Qed.

Lemma unguardeds_cp: ∀ p, closed_process p → unguardeds p = \{}.
Proof.
  induction p; introv Hcp; simpls¬. unfolds closed_process. simpl in Hcp.
    apply union_empty in Hcp. destruct Hcp. rewrite IHp1, IHp2; auto.
    rewrite¬ union_empty_l.
Qed.

Lemma wfp_unguardeds_cp_subst: ∀ (p r : wfprocess) X,
  closed_process r → unguardeds (wfp_subst r X p) = unguardeds p \- \{X}.
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; simpls; introv Hr; try rewrite¬ remove_from_empty.
    cases_if; subst.
      rewrite remove_same. applys¬ unguardeds_cp.
      simpls. rewrite¬ remove_while_notin.
      lets H1 : H p1 X Hr... lets H2 : H p2 X Hr...
      rewrite H1, H2. rewrite¬ union_remove.
Qed.

Lemma wfp_unguarded_remove_iff : ∀ (p : wfprocess) X,
  (X \in unguardeds p) ↔ (∃ (p´ : wfprocess), {{p -- LabRem X ->> (AP p´)}}).
Proof with automate.
  introv; split; intro Hyp.
    applys× wfp_not_guarded_unguarded.
    rewrite <- unguardeds_spec; unfold notin; applys¬ not_not_intro.
    destruct Hyp as (p´ & Hyp).
      applys¬ not_not_elim; fold (X \notin unguardeds p); rewrite unguardeds_spec.
      generalize Hyp; generalize p´; clear.
      induction p using wfp_ind; simpls; introv Hyp Hg; inverts Hyp; inverts¬ Hg;
      lets (p´´ & Heq) : wfp_agent_rem H2; subst×...
Qed.