Library HOC16CONbis

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.

Lemma CONbis_sym : Symmetric CONbis.
Proof.
  introv H. inversion H as [R HR].
  unfold CONbis. ∃ R. split. apply HR.
  unfold Context_bisimulation in HR.
  apply HR. apply HR.
Qed.

Lemma CONbisC_sym : Symmetric CONbisC.
Proof.
  introv H. destructs H. splits¬. apply¬ CONbis_sym.
Qed.

Lemma CONbis_tau : tau_relation CONbis.
Proof.
  introv Hio Ht.
  inversion Hio as (R & HR).
  assert (∃ (q´ : wfprocess), {{q -- Tau ->> AP q´}} ∧ R p´ q´).
  unfold Context_bisimulation, tau_relation in HR. eapply HR.
  apply HR.
  assumption. inversion H as (q´ & Hq).
  ∃ q´. split. apply Hq.
  ∃ R. split. apply HR. apply Hq.
Qed.

Lemma CONbisC_tau: tau_relation CONbisC.
Proof.
  introv Hio Ht. destruct Hio as (Hcp1 & Hcp2 & Hio).
  apply CONbis_tau in Hio; auto. destruct (Hio _ Ht) as (q´ & Ht´ & Hio´).
  lets Hcp3: cp_trans_tau Hcp1 Ht. lets Hcp4: cp_trans_tau Hcp2 Ht´.
  ∃ q´. unfolds CONbisC. splits¬.
Qed.

Lemma CONbis_out_context : out_context_relation CONbis.
Proof.
  introv Hio Ht.
  inversion Hio as [R HR].
  assert (∃ (q´ q´´ : wfprocess), ({{q--LabOut a q´´->>(AP q´)}} ∧ (∀ X (s : wfprocess),
  GV s \c singleton X → R (wfp_Par (wfp_subst p´´ X s) p´) (wfp_Par (wfp_subst q´´ X s) q´)))).
  unfold Context_bisimulation, out_context_relation in HR. eapply HR.
  apply HR.
  eassumption. inversion H as [q´ Hex]. inversion Hex as [q´´ Hq].
  ∃ q´ q´´. split. apply Hq.
  ∃ R. split. apply HR. apply Hq.
  assumption.
Qed.

Lemma CONbisC_out_context: out_context_relation CONbisC.
Proof.
  introv Hio Ht. destruct Hio as (Hcp1 & Hcp2 & Hio).
  apply CONbis_out_context in Hio; auto. destruct (Hio _ _ _ Ht) as (q´ & q´´ & Ht´ & Hr).
  lets (Hcp3 & Hcp3´): cp_trans_out Hcp1 Ht. lets (Hcp4 & Hcp4´): cp_trans_out Hcp2 Ht´.
  ∃ q´ q´´. splits¬. intros. splits¬.
    applys cp_par. split¬. unfolds.
      simpl; rewrite¬ GV_subst_cp. apply fset_extens; unfolds subset; introv H´.
      rewrite in_remove in H´. destruct H´ as (H´&H´´). specializes H H´.
      unfolds notin. false.
      rewrite in_empty in H´. false.
    applys cp_par. split¬. unfolds.
      simpl; rewrite¬ GV_subst_cp. apply fset_extens; unfolds subset; introv H´.
      rewrite in_remove in H´. destruct H´ as (H´&H´´). specializes H H´.
      unfolds notin. false.
      rewrite in_empty in H´. false.
Qed.

Lemma CONbis_closed : closed_relation CONbis.
Proof.
  introv Hio Ht.
  inversion Hio as (R & HR & HO).
  unfold Context_bisimulation, closed_relation in HR. lets HR´ : HR. destruct HR as (Hsym & Htau & Hout & HR).
  specialize (HR p q HO a fp Ht); destruct HR as (fq & H´ & HR).
  ∃ fq; splits¬.
  introv HC. ∃ R. split¬.
Qed.

Lemma CONbisC_closed: closed_relation CONbisC.
Proof.
  introv Hio Ht. destruct Hio as (Hcp1 & Hcp2 & Hio).
  apply CONbis_closed in Hio; auto. destruct (Hio _ _ Ht) as (fq & Ht´ & Hio´).
  lets Hcp3: cp_trans_in Hcp1 Ht. lets Hcp4: cp_trans_in Hcp2 Ht´.
  ∃ fq. splits¬. introv Hc. splits¬.
Qed.