Library HOC20Barbed

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.
Require Import HOC12Guarded.
Require Import HOC13Bisimulations.
Require Import HOC14IObis.
Require Import HOC17NORbis.

Require Import Relations.

Inductive context : Set :=
| CSend : chan → context → context
| CAbs : chan → var → context → context
| CParL : context → wfprocess → context
| CParR : wfprocess → context → context
| CHole : context.

Fixpoint fill (C : context) (p : wfprocess) : wfprocess :=
  match C with
    | CSend a C ⇒ wfp_Send a (fill C p)
    | CAbs a X C ⇒ wfp_Abs a X (fill C p)
    | CParL C q ⇒ wfp_Par (fill C p) q
    | CParR q C ⇒ wfp_Par q (fill C p)
    | CHole ⇒ p
  end.

Definition context_closed (R : relation wfprocess) : Prop :=
  ∀ p q, (R p q) → ∀ C, R (fill C p) (fill C q).

Definition perform_output (p : wfprocess) (a:chan) : Prop :=
  ∃ (p´ p´´: wfprocess), {{p--LabOut a p´´->>(AP p´)}} .

Definition perform_input (p : wfprocess) (a:chan) : Prop :=
  ∃ f, {{p--LabIn a->>(AA f)}} .

Definition out_barb_preserving (R : relation wfprocess) : Prop :=
  ∀ p q, (R p q) → ∀ a, perform_output p a → perform_output q a.

Definition in_barb_preserving (R:relation wfprocess) : Prop :=
  ∀ p q, (R p q) → ∀ a, perform_input p a → perform_input q a.

Definition async_barbed_relation R : Prop :=
  (Symmetric R) ∧ (tau_relation R) ∧ (context_closed R) ∧ (out_barb_preserving R).

Definition async_barbed p q : Prop :=
  ∃ R, async_barbed_relation R ∧ (R p q).

Instance async_barbed_sym : Symmetric async_barbed.
Proof.
  introv (R & (Hs & Ht & Ho & Hi) & Hr). ∃× R; repeat splits×.
Qed.

Lemma async_barbed_tau : tau_relation async_barbed.
Proof.
  introv (R & (Hsym & Htau & Hcc & Houtb) & Hr) Ht.
  lets (q´ & Htq & Hr´) : Htau Hr Ht.
  ∃ q´; splits~; ∃ R; repeat splits×.
Qed.

Lemma async_barbed_context_closed : context_closed async_barbed.
Proof.
  introv (R & (Hsym & Htau & Hcc & Houtb) & Hr).
  ∃ R; repeat splits×.
Qed.

Lemma async_barbed_out_barb_preserving : out_barb_preserving async_barbed.
Proof.
  introv (R & (Hsym & Htau & Hcc & Houtb) & Hr) Ht.
  eapply Houtb; eassumption.
Qed.

Inductive R_trans_ab : binary wfprocess :=
| Rtrans_ab : ∀ p q r, async_barbed p q → async_barbed q r → R_trans_ab p r.

Hint Resolve Rtrans_ab.

Instance async_barbed_trans : Transitive async_barbed.
Proof.
  introv Hxy Hyz. ∃ R_trans_ab; splits*; clear; repeat splits×.

  + introv Hr. inverts Hr. econstructor.
      symmetry in H0. eassumption.
      symmetry in H. eassumption.

  + introv Hr Ht. inverts Hr.
    lets (q´ & Htq´ & Hab´) : async_barbed_tau H Ht.
    lets (q´´ & Htq´´ & Hab´´) : async_barbed_tau H0 Htq´.
    eexists. splits; try eassumption. econstructor; eassumption.

  + introv Hr; introv; inverts Hr.
    lets Htr´ : async_barbed_context_closed H C.
    lets Htr´´ : async_barbed_context_closed H0 C.
    econstructor; eassumption.

  + introv Hr Ht. inverts Hr.
    lets Htr´ : async_barbed_out_barb_preserving H Ht.
    lets¬ Htr´´ : async_barbed_out_barb_preserving H0 Htr´.
Qed.

Theorem IObis_async_barbed_lr : ∀ p q,
  IObis p q → async_barbed p q.
Proof.
  intros p q Hio.
  ∃ IObis. repeat splits.
    apply IObis_sym.
    apply IObis_tau.
    clear p q Hio. intros p q Hio C.
    induction C; intros; simpl.
      applys¬ IObis_congr_send.
      applys¬ IObis_congr_abs.
      applys¬ IObis_congr_par.
      applys¬ IObis_congr_par.
      assumption.
    clear p q Hio. intros p q Hio a H.
      destruct H as [p´ [p´´ H]]. eapply IObis_out in H; eauto.
      destruct H as [q´ [q´´ H]].
      ∃¬ q´ q´´. applys¬ H. auto.
Qed.