Require Export Semantics.

Notation Rincl := LibRelation.rel_incl.

Definition comp_rel {A:Type} (R S :binary A) x y := ∃ z, R x z ∧ S z y.

Notation "R ° S" := (@comp_rel _ R S) (at level 42, right associativity).

Lemma comp_trans{A}: ∀ (R S:binary A), inverse (R°S) = (inverse S ° inverse R).
Proof.
  intros. apply binary_ext.
    split; intros H; destruct H as [ z [ H1 H2 ]]; eexists; eauto.
Qed.

Lemma comp_assoc {A} : ∀ (R S T:binary A), R ° S ° T = (R ° S) ° T.
Proof.
  intros. apply binary_ext. intros.
    split; introv H; inverts H as [H1 H2].
    inverts H2; repeat (eexists; intuition eauto).
    inverts H1; repeat (eexists; intuition eauto).
Qed.

Ltac destruct_comp :=
  repeat match goal with
    | H: (_ ° _) _ _ |- _ ⇒ unfold comp_rel in H; destruct_hyps
  end.

Notation test_proc Rel P Q :=
    (∀ P', ltsproc P P' → ∃ Q', ltsproc Q Q' ∧ Rel P' Q').

Notation test_abs Rel P Q :=
  (∀ a (F:abs), ltsabs P a F → ∀ (C:conc),
   conc_wf C → ∃ (F':abs), ltsabs Q a F' ∧ Rel (appr F C) (appr F' C)).

Notation test_conc Rel P Q :=
  (∀ a (C:conc), ltsconc P a C → ∀ (F:abs),
   ∃ (C':conc), ltsconc Q a C' ∧ Rel (appr F C) (appr F C')).

Definition simulation (Rel: binary proc0) : Prop :=
  ∀ P Q, Rel P Q → test_proc Rel P Q ∧ test_abs Rel P Q ∧ test_conc Rel P Q.

Definition bisimulation (Rel : binary proc0) : Prop :=
  (simulation Rel) ∧ (simulation (inverse Rel)).

Ltac forwards_test Rel := try (match goal with
  | H1: ∀ P Q, Rel P Q → _,
    H2: Rel ?P ?Q |- _ ⇒ specialize (H1 P Q H2)
  end); intuition auto; match goal with
  | H1: test_proc Rel ?P ?Q, H2: ltsproc ?P _ |- _ ⇒
      let H' := fresh "H" in
      let Q' := fresh "Q'" in forwards H': H1 H2; destruct H' as [Q' []]
| H1: test_abs Rel ?P ?Q, H2: ltsabs ?P _ _, C:conc |- _ ⇒
      let H' := fresh "H" in
      let F' := fresh "F'" in forwards× H': H1 H2 C; destruct H' as [F' []]
| H1: test_conc Rel ?P ?Q, H2: ltsconc ?P _ _, F:abs |- _ ⇒
      let H' := fresh "H" in
      let F' := fresh "C'" in forwards× H': H1 H2 F; destruct H' as [F' []]
end.

Lemma transp_bisim_is_bisim: ∀ Rel, bisimulation (inverse Rel) ↔ bisimulation Rel.
Proof.
  unfold bisimulation; intuition.
Qed.

Lemma sim_sym_imply_bisim : ∀ Rel, simulation Rel → sym Rel → bisimulation Rel.
Proof.
  intros Rel Hsim Hsym.
  split; intuition.
  rewrite inverse_sym; auto.
Qed.

Lemma comp_sim_is_sim : ∀ R S, simulation R → simulation S → simulation (R°S).
Proof.
  intros_all. destruct_comp. unfold simulation in ×.
  forwards_test R; forwards_test S; eexists;
       intuition; try solve [eassumption]; eexists; intuition eassumption.
Qed.

Lemma comp_bisim_is_bisim : ∀ R S, bisimulation R → bisimulation S → bisimulation (R°S).
Proof.
  unfold bisimulation. intros; split; intuition auto using comp_sim_is_sim.
  rewrite× @comp_trans. auto using comp_sim_is_sim.
Qed.

Lemma union_sim_is_sim : ∀ Rel Rel', simulation Rel → simulation Rel'
    → simulation (LibRelation.union Rel Rel').
Proof.
  intros_all. unfold simulation in ×. inverts H1;
      [forwards_test Rel; eexists; intuition eauto; left× |
       forwards_test Rel'; eexists; intuition eauto; right*].
Qed.

Definition bisimilarity (P Q:proc0) := ∃ Rel, bisimulation Rel ∧ Rel P Q.

Lemma bisim_sym: sym bisimilarity.
Proof.
  intros_all. destruct H as [ Rel ]. ∃ (inverse Rel); intuition.
  apply transp_bisim_is_bisim; auto.
Qed.

Lemma bisim_trans: trans bisimilarity.
Proof.
  intros_all. inversion H as [ Rel ]. inversion H0 as [ Rel' ].
  ∃ (Rel ° Rel'). intuition. apply comp_bisim_is_bisim; auto.
  ∃ y; auto.
Qed.

Definition id_bisim (P Q:proc0) := P=Q.

Hint Unfold id_bisim bisimulation bisimilarity:bisim.

Lemma id_bisim_bisim: bisimulation id_bisim.
Proof.
  unfold id_bisim. apply sim_sym_imply_bisim.
  intros_all. subst. eexists; intuition eauto with hopi.
  intros_all; subst; intuition.
Qed.

Lemma bisim_refl: ∀ P, bisimilarity P P.
Proof.
  intros P. ∃ id_bisim. split. apply id_bisim_bisim. auto with bisim.
Qed.

Lemma bisim_is_bisimulation : bisimulation bisimilarity.
Proof.
  apply sim_sym_imply_bisim.
  + intros_all. inverts H. destruct H0. assert (Hbisim:=H).
      destruct H as [Hr Hrconv]. unfold simulation in ×.
      forwards_test x; eexists; intuition; try eassumption; ∃ x; intuition.
  + apply bisim_sym.
Qed.

Lemma bisim_exists_sym_rel : ∀ P Q, bisimilarity P Q →
    ∃ Rel, sym Rel ∧ simulation Rel ∧ Rel P Q.
Proof.
  intros.
  destruct H as [Rel [Hbis Hpq]].
  ∃ (LibRelation.union Rel (inverse Rel)).
  destruct Hbis as [ Hsim Hsimsym ].
  splits.
  - intros_all. destruct H. right. auto. left. auto.
  - apply union_sim_is_sim; auto.
  - left. auto.
Qed.

Definition rename_compatible {V:Set} Rel := ∀ (P Q:name → proc V) a,
  notin_ho a P → notin_ho a Q → Rel (P a)(Q a) →
  ∀ b, notin_ho b P → notin_ho b Q → Rel (P b)(Q b).

Inductive rel_renamed (Rel: binary proc0) : binary proc0 :=
| rrenamed_base : ∀ (P Q:proc0), Rel P Q → rel_renamed Rel P Q
| rrenamed_def : ∀ (P Q:proc0), rel_renamed Rel P Q →
    ∀ a P' Q', notin_ho a P' → notin_ho a Q' →
    P = P' a → Q = Q' a → ∀ b,
    notin_ho b P' → notin_ho b Q' → rel_renamed Rel (P' b)(Q' b).

Lemma simulation_rel_renamed: ∀ Rel, simulation Rel → simulation (rel_renamed Rel).
Proof.
    intros_all. unfold simulation in ×. induction H0; intros.
      + forwards_test Rel; eauto using rrenamed_base.
      + splits; intros; subst.
        - all_exp b. forwards*: ltsproc_rename H5 a.
          forwards*: ltsproc_notin_ho H5 a.
          forwards_test (rel_renamed Rel). all_exp a.
          forwards*: ltsproc_rename H10 b.
          forwards*: ltsproc_notin_ho H10 b.
          eexists; split; try eassumption.
          apply rrenamed_def with (P'1 a)(Q'1 a) a; auto with hopi.
        - all_exp b. destruct (exists_sname a0 b a) as [d].
          forwards*: ltsabs_rename H7 a.
          forwards*: ltsabs_notin_ho H7 a.
          destruct (dec_name a b); subst.
          forwards_test (rel_renamed Rel).
          conc_exp b C. ho_conc_exp a C0.
          fresh_lpc (a::b::d::nil) ((nu P') // (a0 ? (nu F0)) // nu Q')
                    (conc_nu (fun x ⇒ conc_nu (fun y ⇒ C1 x y))).
          rename x into c. destruct IHrel_renamed as [Hp []].
          forwards*: H15 H9 (C1 c a).
            unfold conc_wf. assert (cwf_aux nil (C1 c b)).
            change (cwf_aux nil ((fun x ⇒ C1 x b) c)).
            eapply cwf_aux_rename; eauto; auto with hopi.
            eapply cwf_aux_rename; eauto; auto with hopi.
          destruct_hyps. rename x into F'. all_exp a.
          assert (subst_name a b d a0).
            inverts H4; constructor.
            destruct (dec_name a b); subst; auto.
            forwards*: ltsabs_notin_label H7.
          forwards*: ltsabs_rename H22 b.
          forwards*: ltsabs_notin_ho H22 b.
          eexists; split; try eassumption.
          change (rel_renamed Rel ((fun x ⇒ appr (F0 b) (C1 x b)) a)
                                  ((fun x ⇒ appr (F'0 b) (C1 x b)) a)).
          apply rrenamed_def with (appr (F0 b)(C1 c b)) (appr (F'0 b)(C1 c b))
          c; eauto; auto with hopi.
          change (rel_renamed Rel ((fun x ⇒ appr (F0 x) (C1 c x)) b)
                                  ((fun x ⇒ appr (F'0 x) (C1 c x)) b)).
          eapply rrenamed_def; eauto; auto with hopi.
          intros_all. solve_notin'; auto with hopi.
          eapply ltsabs_notin; eauto; auto with hopi.
        - conc_exp b C. destruct (exists_sname a0 b a) as [d].
          forwards*: ltsconc_rename H7 a.
          forwards*: ltsconc_notin_ho H7 a.
          destruct (dec_name a b); subst.
          forwards_test (rel_renamed Rel).
          all_exp b. ho_exp a F0.
          fresh_lpc (a::b::d::nil) ((nu P') //
                    (a0 ? (nu (fun x ⇒ (nu fun y =>(F1 x y))))) // nu Q')
                    (conc_nu C0).
          rename x into c. destruct IHrel_renamed as [Hp []].
          forwards*: H17 H8 (F1 c a).
          destruct_hyps. rename x into C'. conc_exp a C'.
          assert (subst_name a b d a0).
            inverts H4; constructor.
            destruct (dec_name a b); subst; auto.
            forwards*: ltsconc_notin_label H7.
          forwards*: ltsconc_rename H21 b.
          forwards*: ltsconc_notin_ho H21 b.
          eexists; split; try eassumption.
          change (rel_renamed Rel ((fun x ⇒ appr (F1 x b) (C0 b)) a)
                                  ((fun x ⇒ appr (F1 x b) (C'0 b)) a)).
          apply rrenamed_def with (appr (F1 c b)(C0 b)) (appr (F1 c b)(C'0 b))
          c; eauto; auto with hopi.
          change (rel_renamed Rel ((fun x ⇒ appr (F1 c x) (C0 x)) b)
                                  ((fun x ⇒ appr (F1 c x) (C'0 x)) b)).
          eapply rrenamed_def; eauto; auto with hopi.
          intros_all. solve_notin'; auto with hopi.
          eapply ltsconc_notin; eauto; auto with hopi.
Qed.

Lemma bisim_rename_compatible : rename_compatible bisimilarity.
Proof.
  intros_all.
  forwards: bisim_exists_sym_rel H1.
  destruct H4 as [Rel [Hsym [Hsim Hpq]]].
  ∃ (rel_renamed Rel).
  split.
  - apply sim_sym_imply_bisim.
    apply× simulation_rel_renamed.
    intros_all. induction H4. apply rrenamed_base; auto.
    subst. apply rrenamed_def with (Q' a0) (P' a0) a0; eauto.
  - apply rrenamed_def with (P a)(Q a) a; eauto. apply rrenamed_base; auto.
Qed.

Definition open_extension {V:Set} (Rel:binary proc0) (P Q:proc V) :=
   ∀ (s: V→ proc0), Rel (bind s P) (bind s Q).

Lemma oe_refl {V:Set} : ∀ Rel, refl Rel → refl (@open_extension V Rel).
Proof.
  intros_all. apply H.
Qed.

Lemma oe_sym {V:Set} : ∀ Rel, sym Rel → sym (@open_extension V Rel).
Proof.
  intros_all. apply H; auto.
Qed.

Lemma oe_trans {V:Set} : ∀ Rel, trans Rel → trans (@open_extension V Rel).
Proof.
  intros_all. eauto.
Qed.

Lemma oe_mapV {V W:Set}: ∀ Rel (P Q:proc V) (f:V→W),
    open_extension Rel P Q → open_extension Rel (mapV f P)(mapV f Q).
Proof.
   intros_all. repeat(rewrite bind_mapV_comp); auto.
Qed.

Lemma oe_bind{V W:Set}: ∀ Rel (P Q:proc V) (f:V→ proc W),
    open_extension Rel P Q → open_extension Rel (bind f P)(bind f Q).
Proof.
  unfold open_extension. intros. repeat (rewrite bind_bind). apply H.
Qed.

Lemma oe_proc0 : ∀ (Rel:binary proc0) (P Q:proc0), Rel P Q → open_extension Rel P Q.
Proof.
  intros_all. repeat (rewrite bind_proc0); auto.
Qed.

Axiom fun_beta_exp : ∀ {V:Set} a (s: V → proc0), ∃ s',
  ∀ v, notin_ho a (s' v) ∧ s v = s' v a.

Axiom fun_ho_beta_exp : ∀ {V:Set} a (s: V → name → proc0), ∃ s',
  ∀ v, notin_ho a (fun x ⇒ s v x) ∧ s v = s' v a.

Lemma oe_rename: ∀ (Rel:binary proc0), (rename_compatible Rel) →
   ∀ V, (@rename_compatible V (open_extension Rel)).
Proof.
  intros_all.
  destruct (dec_name a b); subst; auto.
  destruct (fun_beta_exp b s) as [s'].
  destruct (fun_ho_beta_exp a s') as [s''].
  fresh_lp (a::b::nil) (bind s (P a) // bind s (Q a)).
  rename x into c. forwards*: H1 (fun v ⇒ s'' v c a).
  change (Rel ((fun x ⇒ (bind (fun v : V ⇒ s'' v c x) (P x))) a)
       ((fun x ⇒ (bind (fun v : V ⇒ s'' v c x) (Q x))) a)) in H8.
  forwards*: X a b.
    intros_all. apply× @notin_bind. intros.
    forwards*: H6 v. forwards*: H5 v. destruct_hyps.
    forwards*: H14 b0. rewrite H17 in H18.
    change (notin a ((fun x ⇒ s'' v x b0) c)).
    eapply notin_rename; eauto; auto with hopi.
    intros_all. apply× @notin_bind. intros.
    forwards*: H6 v. forwards*: H5 v. destruct_hyps.
    forwards*: H14 b0. rewrite H17 in H18.
    change (notin a ((fun x ⇒ s'' v x b0) c)).
    eapply notin_rename; eauto; auto with hopi.
    intros_all. apply× @notin_bind. intros.
    forwards*: H6 v. forwards*: H5 v. destruct_hyps.
    forwards*: H15 b0. rewrite H17 in H18.
    change (notin b ((fun x ⇒ s'' v x b0) c)).
    eapply notin_rename; eauto; auto with hopi.
    intros_all. apply× @notin_bind. intros.
    forwards*: H6 v. forwards*: H5 v. destruct_hyps.
    forwards*: H15 b0. rewrite H17 in H18.
    change (notin b ((fun x ⇒ s'' v x b0) c)).
    eapply notin_rename; eauto; auto with hopi.
  simpl in H10. change (Rel ((fun c ⇒ (bind (fun v : V ⇒ s'' v c b) (P b))) c)
       ((fun c ⇒ (bind (fun v : V ⇒ s'' v c b) (Q b))) c)) in H10.
  forwards*: X c a.
    intros_all. apply notin_bind_rev in H12.
    apply× @notin_bind. intros.
    forwards*: H6 v. forwards*: H5 v. destruct_hyps.
    assert (isinV v (P a)) by (eapply isinV_rename; eauto).
    forwards*: H12. rewrite H17 in H21. rewrite H18 in H21.
    change (notin c ((fun b0 ⇒ s'' v b0 b) b0)).
    eapply notin_rename; eauto; auto with hopi.
    destruct_hyps. eapply notin_rename; eauto.
    intros_all. apply notin_bind_rev in H13.
    apply× @notin_bind. intros.
    forwards*: H6 v. forwards*: H5 v. destruct_hyps.
    assert (isinV v (Q a)) by (eapply isinV_rename; eauto).
    forwards*: H13. rewrite H17 in H21. rewrite H18 in H21.
    change (notin c ((fun b0 ⇒ s'' v b0 b) b0)).
    eapply notin_rename; eauto; auto with hopi.
    destruct_hyps. eapply notin_rename; eauto.
    intros_all. apply× @notin_bind. intros.
    forwards*: H6 v. forwards*: H5 v. destruct_hyps.
    forwards*: H15 b. rewrite H18 in H19.
    change (notin a ((fun x ⇒ s'' v x b) b0)).
    eapply notin_rename; eauto; auto with hopi.
    intros_all. apply× @notin_bind. intros.
    forwards*: H6 v. forwards*: H5 v. destruct_hyps.
    forwards*: H15 b. rewrite H18 in H19.
    change (notin a ((fun x ⇒ s'' v x b) b0)).
    eapply notin_rename; eauto; auto with hopi.
  simpl in H11. asserts_rewrite (s = (fun v ⇒ s'' v a b)).
    extens. intros. forwards*: H5 x1. forwards*: H6 x1.
    destruct_hyps. rewrite H17. rewrite× H16.
  auto.
Qed.