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.

Inductive sim_test : binary proc0 → agent → agent → Prop :=
| st_proc : ∀ (Rel:binary proc0) P Q, Rel P Q → sim_test Rel (ag_proc P) (ag_proc Q)
| st_abs : ∀ (Rel:binary proc0) F F', (∀ (C:conc), conc_wf C →
        Rel (appr F C) (appr F' C)) → sim_test Rel (ag_abs F) (ag_abs F')
| st_conc : ∀ (Rel:binary proc0) C C', (∀ (F:abs),
        Rel (appr F C) (appr F C')) → sim_test Rel (ag_conc C) (ag_conc C').

Hint Constructors sim_test:bisim.

Definition simulation_late (Rel: binary proc0) : Prop :=
  ∀ P Q, Rel P Q → ∀ l A, lts P l A → ∃ A', lts Q l A' ∧ sim_test Rel A A'.

Ltac destruct_agent_sim A :=
  destructA A;simpl;
  [ apply st_proc | apply st_abs; intros []; intros | apply st_conc; intros []; intros ].

Hint Unfold simulation_late comp_rel:bisim.

Lemma sim_test_trans : ∀ Rel, trans Rel → trans (sim_test Rel).
Proof.
  intros_all.
  destruct x; destruct y; inverts H0; destruct z; inverts H1; subst; eauto with bisim.
Qed.

Lemma sim_test_sym : ∀ Rel, sym Rel → sym (sim_test Rel).
Proof.
  intros_all.
  destruct x; destruct y; inverts H0; subst; auto with bisim.
Qed.

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

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

Notation test_conc Rel P Q :=
  (∀ a (C:conc), lts P (out a)(ag_conc C) → ∀ (F:abs),
     ∃ (C':conc), lts Q (out a)(ag_conc 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: lts ?P tau _ |- _ ⇒
      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: lts ?P (inp _) _, 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: lts ?P (out _) _, 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.

Lemma late_implies_sim : ∀ Rel, simulation_late Rel → simulation Rel.
Proof.
  intros. unfold simulation_late in H. unfold simulation. intros. splits; intros.
  - forwards*: H. destruct_hyps. forwards*: lts_tau_proc.
    destruct H4. inverts H4. ∃ x0; intuition. inverts× H3.
  - forwards*: H. destruct_hyps. forwards*: lts_inp_abs.
    destruct H5. inverts H5. ∃ x0; intuition.
    destruct F as []; destruct x0 as []; inverts H4. forwards*: H8.
  - forwards*: H. destruct_hyps. forwards*: lts_out_conc.
    destruct H4. inverts H4. ∃ x0; intuition.
    destruct C as []; destruct x0 as []; inverts H3. forwards*: H7 F.
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:proc V),
  Rel P Q → ∀ f, injective f → Rel (mapN f P) (mapN f Q).

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
    → ∀ f, injective f → rel_renamed Rel (mapN f P) (mapN f Q).

Lemma card_max : ∀ n E, max_elt E = Some n → cardinal E ≤ S n.
Proof.
  intros. remember (cardinal E) as m. gen n E. induction m; intros.
  - omega.
  - assert (H':=H). apply max_elt_spec in H'. destruct H'.
    remember (max_elt (E \- \{ n })) as n'. destruct n'.
    forwards*: IHm n0 (E \- \{n}).
    assert (S m = S (cardinal (E \- \{ n }))).
    asserts_rewrite (E \- \{n } [=] remove n E). fsetdec.
    rewrite× IndexSetProperties.remove_cardinal_1. omega. assert (n0 < n).
    symmetry in Heqn'. apply max_elt_spec in Heqn'. destruct Heqn'.
    destruct (classic (n0=n)). subst. fsetdec.
    forwards*: H1 n0. simplfs. omega. omega.
    symmetry in Heqn'. apply max_elt_spec_empty in Heqn'.
    assert (E [=] \{n}). intros_all. split. intros. destruct (classic (a=n)). subst. fsetdec.
    assert (a \in (E \- \{n})) by fsetdec. fsetdec. fsetdec. rewrite H2 in Heqm.
    forwards*: IndexSetProperties.singleton_cardinal n. omega.
Qed.

Lemma injective_cardinal : ∀ f E, injective f → cardinal (map f E) = cardinal E.
Proof.
  intros. remember (cardinal E) as m. gen E; induction m; intros.
  - symmetry in Heqm. rewrite <- IndexSetProperties.cardinal_Empty in Heqm. asserts_rewrite (E [=] \{}).
    fsetdec. rewrite map_empty. apply IndexSetProperties.empty_cardinal.
  - symmetry in Heqm. assert (Heqm':=Heqm). apply IndexSetProperties.cardinal_inv_2 in Heqm. destruct Heqm.
    forwards*: IHm (E \- \{ x}). asserts_rewrite (E \- \{ x } [=] remove x E). fsetdec.
    assert (S m = S (cardinal (remove x E))). rewrite× IndexSetProperties.remove_cardinal_1. omega.
    asserts_rewrite (E [=] (E \- \{ x}) \u \{x}). intros_all. split; try fsetdec. intros. simplfs. intuition. fsetdec.
    rewrite map_union. rewrite IndexSetProperties.union_cardinal_inter. rewrite H0.
    rewrite map_singleton at 1. rewrite× <- map_inter. asserts_rewrite ((E \- \{x}) \n \{ x} [=] \{}). fsetdec.
    rewrite map_empty. rewrite IndexSetProperties.singleton_cardinal.
    rewrite IndexSetProperties.empty_cardinal. omega.
Qed.

Fixpoint make_In n := match n with
| 0 ⇒ \{}
| S n ⇒ add (S n) (make_In n)
end.

Lemma max_In_S : ∀ n, max_elt (make_In (S n)) = Some (S n).
Proof.
  induction n.
  - simpl. apply max_elt_spec. intuition. rewrite <- IndexSetProperties.singleton_equal_add in H. fsetdec.
  - simpl. apply max_elt_spec. apply max_elt_spec in IHn. intuition. simpl in ×.
    rewrite add_iff in H1. destruct H1. omega. forwards*: H0.
Qed.

Lemma card_In : ∀ n, cardinal (make_In n) = n.
Proof.
  induction n.
  - simpl. apply IndexSetProperties.empty_cardinal.
  - simpl. rewrite IndexSetProperties.add_cardinal_2. rewrite× IHn.
    destruct n. simpl. fsetdec. specialize (max_In_S n). intros. apply max_elt_spec in H. intros_all.
    destruct H. forwards*: H1 (S (S n)). omega.
Qed.

Lemma fresh_above_n : ∀ (f:nat→nat), injective f → ∀ n, ∃ x, x > n ∧ ∃ y, x = f y.
Proof.
  intros. Opaque make_In. forwards*: card_In (S (S n)). forwards*: max_In_S (S n).
  forwards*: injective_cardinal f (make_In (S (S n))). rewrite H0 in H2.
  remember (max_elt (map f (make_In (S (S n))))) as n'. destruct n'.
  symmetry in Heqn'. forwards*: card_max Heqn'. rewrite max_elt_spec in Heqn'. rewrite H2 in H3.
  ∃ n0; intuition. simplfs. eexists; eauto.
  symmetry in Heqn'. rewrite max_elt_spec_empty in Heqn'. apply IndexSetProperties.cardinal_inv_2 in H2.
  destruct H2. fsetdec. Transparent make_In.
Qed.

Lemma renaming_sets: ∀ F f E E' k, injective f → E [=] map f E' → ∃ g F' F'', F' \c F ∧
     map g F \c map f F'' ∧ F' \n E [=] \{} ∧ map g F' \n E [=] \{} ∧ (∀ x, x \in F → g (g x) = x) ∧ injective g ∧
     (∀ x, x \notin (F' \u map g F') → g x = x) ∧ ∀ f', f = liftN f' k → ∃ g', g = liftN g' k.
Proof.
  intros F; remember (IndexSetImpl.cardinal F) as n; gen F; induction n; intros.
  - symmetry in Heqn. rewrite <- IndexSetProperties.cardinal_Empty in Heqn. assert (F [=] \{}). fsetdec.
    ∃ (fun (x:nat) ⇒ x) \{} \{}; intuition; try (rewrite H1); repeat rewrite map_empty; try fsetdec.
    ∃ (fun (x:nat) ⇒ x). extens. intros; simpl_liftN.
  - symmetry in Heqn. assert (Heqn':=Heqn). apply IndexSetProperties.cardinal_inv_2 in Heqn. destruct Heqn.
    assert (F \n \{ x} [=] \{ x}). asserts_rewrite ((F \n \{ x }) [=] (\{ x} \n F)). fsetdec.
      apply IndexSetProperties.inter_subset_equal. fsetdec.
    destruct (classic (∃ y, x = f y)).
     × destruct H2 as [y].
       forwards*: IHn (F \- \{ x}) f (E \u \{x}) (E' \u \{y}) k.
        forwards: IndexSetProperties.diff_inter_cardinal F \{ x}. rewrite H1 in H3.
        rewrite IndexSetProperties.singleton_cardinal in H3. omega.
        rewrite map_union. rewrite H0. rewrite map_singleton. subst. fsetdec.
       destruct H3 as [g [F' [F'' [HF'f [HgFfF'' [HF'E [HgF'E [Hgg [Hginj [HE Hlift]]]]]]]]]].
       assert (g x = x).
         apply HE. intros_all. simplfs. destruct H3. apply HF'f in H3. simplfs; intuition.
         assert (x \in (map g F' \n E \u \{ x })). apply inter_iff. simplfs. intuition. ∃ x0; intuition.
         rewrite HgF'E in H4. fsetdec.
       ∃ g F' (F'' \u \{y}). intuition. intros_all. apply HF'f in H4. simplfs.
       assert (F [=] (F \- \{ x}) \u \{x}). rewrite <- H1 at 2. rewrite IndexSetProperties.diff_inter_all. fsetdec.
       rewrite H4. do 2 rewrite map_union. apply× union_s_m. do 2 rewrite map_singleton. rewrite H3. fsetdec.
       gen HF'E. clears_all. fsetdec.
       gen HgF'E. clears_all. fsetdec.
       destruct (classic (x0=x)). subst. rewrite× H3. apply Hgg. simplfs.
    × forwards*: IHn (F \- \{ x}) f E k.
        forwards: IndexSetProperties.diff_inter_cardinal F \{ x}. rewrite H1 in H3.
        rewrite IndexSetProperties.singleton_cardinal in H3. omega.
      destruct H3 as [g [F' [F'' [HF'f [HgFfF'' [HF'E [HgF'E [Hgg [Hginj [HE Hlift]]]]]]]]]].
      assert (Hmax:∃ n', IndexSetImpl.max_elt (F \u map g F \u E) = Some n').
        remember (IndexSetImpl.max_elt (F \u map g F \u E)) as bla. destruct (bla). ∃ n0; auto.
        symmetry in Heqbla. apply IndexSetImpl.max_elt_3 in Heqbla. false. gen Heqbla i. clears_all. fsetdec.
      destruct Hmax as [n' Hn'].
      destruct (fresh_above_n f H (k + n')) as [zfresh [Hfresh' [yfresh]]].
      assert (Hfresh: zfresh \notin (F \u map g F \u E)).
        gen Hn' Hfresh'. clears_all. intros_all. forwards*: IndexSetImpl.max_elt_2. omega.
      assert (Hgx:g x= x). { apply HE. intros_all. simplfs. destruct H4. apply HF'f in H4. fsetdec.
       destruct_hyps. subst. apply H2. forwards*: HgFfF'' (g x0). simplfs. ∃ x0; intuition.
       simplfs. intuition. eexists; eauto. }
      assert (Hgz:g zfresh= zfresh). { apply HE. intros_all. apply Hfresh. gen H4 i HF'f. clears_all.
       intros. simplfs. destruct H4. left. fsetdec. destruct_hyps. subst. right. left. ∃ x0; intuition. fsetdec. }
      assert (HmapF':map (fun y : IndexSetImpl.elt ⇒ If y = x then f yfresh else If y = f yfresh then x else g y) F' [=] map g F').
      { apply map_eq. intros. default_simp. false. gen H4 HF'f. clears_all. intros. fsetdec.
         false. gen Hfresh H4 HF'f. clears_all. intros. fsetdec. }
      ∃ (fun y ⇒ If y = x then zfresh else If y=zfresh then x else g y)(F'\u \{x})(F'' \u \{yfresh}).
      splits.
      + assert (F [=] (F \- \{ x}) \u \{x}). rewrite <- H1 at 2. rewrite IndexSetProperties.diff_inter_all. fsetdec.
        rewrite H4. apply× union_s_m. fsetdec.
      + intros_all. simplfs. default_simp. ∃ yfresh; intuition. forwards: HgFfF'' (g x0). simplfs. ∃ x0; intuition.
        simplfs. ∃ x1; intuition.
      + assert (x \notin E). intros_all. rewrite H0 in H4. apply H2. simplfs. ∃ x0; intuition.
        gen H4 HF'E. clears_all. fsetdec.
      + rewrite map_union. rewrite map_singleton. default_simp. rewrite HmapF'. gen HgF'E Hfresh. clears_all. intros. fsetdec.
      + default_simp. forwards*: Hginj Hgx. false. rewrite <- e in Hgz. forwards*: Hginj Hgz. false.
        apply Hgg. apply diff_iff. split; auto.
      + intros_all. default_simp. rewrite H4 in Hgz. forwards*: Hginj Hgz. false. forwards*: Hginj Hgx. false.
        rewrite <- H4 in Hgz. forwards*: Hginj Hgz. false. forwards*: Hginj Hgx. false.
      + intros_all. default_simp. false. apply H4. clears_all. fsetdec.
        false. apply H4. rewrite map_union. rewrite map_singleton. default_simp. clears_all. fsetdec.
        apply HE. intros_all. apply H4. rewrite map_union. rewrite map_singleton. default_simp. rewrite HmapF'.
        gen H3. clears_all. fsetdec.
      + intros. destruct (Hlift _ H4) as [g' Hgg']. assert (zfresh > k) by omega. assert (x ≥ k).
        { destruct (classic (x ≥k)); auto. false. apply H2. ∃ x. subst. gen H6. clears_all. simpl_liftN. }
        ∃ (fun y ⇒ If y = (x-k) then zfresh -k else If y = (zfresh -k) then x-k else g' y).
        subst. gen Hgx H5 H6. clears_all. intros. unfold liftN in ×. extens; intros. default_simp; try omega.
Qed.

Lemma invert_f_proc {V:Set}: ∀ (P:proc V) f, (∀ x, x \in fn P → ∃ y, x = f y) → ∃ P', P = mapN f P'.
Proof.
  induction P; intros.
  - ∃ (pr_var v); simpl; auto.
  - simpl in H. forwards*: IHP f. intros. apply H. fsetdec. destruct H0 as [P']. forwards*: H n. fsetdec. destruct H1 as [m].
    ∃ (m ? P'). simpl. fequals.
  - simpl in H. forwards*: IHP1 f. intros. apply H. fsetdec. destruct H0 as [P1'].
    forwards*: IHP2 f. intros. apply H. fsetdec. destruct H1 as [P2']. forwards*: H n. fsetdec. destruct H2 as [m].
    ∃ (m !( P1') P2'). simpl. fequals.
  - simpl in H. forwards*: IHP1 f. intros. apply H. fsetdec. destruct H0 as [P1'].
    forwards*: IHP2 f. intros. apply H. fsetdec. destruct H1 as [P2']. ∃ ( P1' // P2'). simpl. fequals.
  - simpl in H. forwards*: IHP (liftN f 1). intros. destruct x. simpl_liftN. ∃ 0; default_simp.
    forwards*: H x. simplfs. destruct H1 as [y]. simpl_liftN. ∃ (S y). default_simp. rewrite× <- minus_n_O.
    destruct H0 as [P']. ∃ (nu P'). simpl. fequals.
  - ∃ (@pr_nil V). simpl; eauto.
Qed.

Lemma renaming_proc {V:Set}: ∀ (P:proc V) f E E' n, injective f → E [=] map f E' → ∃ P' g,
    mapN g P = mapN f P' ∧ mapN g (mapN g P) = P ∧ injective g ∧ (∀ x, x \in E → g x = x)
    ∧ ∀ f', f = liftN f' n → ∃ g', g = liftN g' n.
Proof.
  intros. forwards*: renaming_sets (fn P) E n. destruct H1 as [g [F' [F'' [HF' [HF'' [HF'E [HgF' [Hgg [Hginj [Hid Hlift]]]]]]]]]].
  forwards*: @invert_f_proc (mapN g P) f. intros. rewrite fn_mapN in H1. apply HF'' in H1. simplfs. ∃ x0; auto.
  destruct H1 as [P']. ∃ P' g; splits; auto.
  rewrite mapN_mapN. rewrite <- (mapN_id' P) at 2. apply× @mapN_eq_on_fn.
  intros. apply Hid. intros_all. rewrite union_iff in H3. destruct H3. fsetdec. fsetdec.
Qed.

Lemma set_lift : ∀ f E E' n, E [=] map f E' → map (fun x ⇒ n+x) E [=] map (liftN f n)(map (fun x ⇒ n+x) E').
Proof.
  intros_all. split; intros.
  simplfs. rewrite H in H1. simplfs. ∃ (n+x0); split. simpl_liftN. asserts_rewrite ((n+x0-n) = x0). omega. auto.
  simplfs. ∃ x0; intuition.
  simplfs. simpl_liftN. asserts_rewrite ((n+x0-n) = x0). omega. ∃ (f x0); intuition.
  rewrite H. simplfs. ∃ x0; intuition.
Qed.

Lemma renaming : ∀ A f E E', injective f → E [=] map f E' → ∃ A' g,
    amapN g A = amapN f A' ∧ amapN g (amapN g A) = A ∧ injective g ∧ ∀ x, x \in E → g x = x.
Proof.
  intros. destructA A.
  + forwards*: @renaming_proc p 0. simpl. destruct H1 as [P' [g [h ]]]. ∃ (ag_proc P') g. simpl. intuition.
    fequals. fequals.
  + forwards*: @renaming_proc p 0. simpl. destruct H1 as [P' [g [h ]]]. ∃ (abs_def P') g. simpl. intuition.
    fequals. fequals.
  + simpl. forwards× Hbla: set_lift n H0. forwards*: @renaming_proc ( p // p0) (liftN f n) n.
    apply liftN_preserves_injectivity. auto.
    destruct_hyps. destruct x; inverts H1. rewrite mapN_mapN in H2. inverts H2.
    repeat rewrite H6. repeat rewrite H9. destruct (H5 f eq_refl) as [g'].
    ∃ (conc_def n x1 x2) g'. intuition.
    simpl. do 2 fequals.
    repeat rewrite mapN_mapN. do 2 fequals. rewrite <- (mapN_id' p) at 2.
    apply mapN_eq_on_fn. intros. rewrite <- (mapN_id' p) in H6 at 2.
    forwards*: @mapN_eq_on_fn_rev H6. simpl_liftN.
    rewrite <- (mapN_id' p0) at 2. apply mapN_eq_on_fn. intros.
    rewrite <- (mapN_id' p0) in H9 at 2. forwards*: @mapN_eq_on_fn_rev H9. simpl_liftN.
    intros_all. assert (x0 (x+n) = x0 (y+n)). subst. gen H2. clears_all. simpl_liftN.
    asserts_rewrite (x+n-n = x). omega. asserts_rewrite (y+n-n = y). omega. omega. forwards*: H3 H10. omega.
    forwards*: H4 (n+x). simplfs. ∃ x; intuition. subst. unfold liftN in H10. default_simp.
    asserts_rewrite (n+x-n = x) in H10. omega. omega.
Qed.

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.
        - forwards*: mapN_lts_rev H2. destruct_hyps. destruct x0; inverts H5. destruct x; inverts H3.
          forwards_test (rel_renamed Rel). forwards*: mapN_lts f H3. simpl in H9. eexists; intuition (try eassumption).
          apply× rrenamed_def.
        - forwards*: mapN_lts_rev H2. destruct_hyps. destruct x0; inverts H6. destruct x; inverts H4.
          forwards*: renaming C f (fn_agent (amapN f a) \u fn (mapN f Q)) (fn_agent a \u fn Q).
            destruct a; simpl. rewrite map_union. repeat rewrite fn_mapN. fsetdec.
          destruct H4 as [A' [g [ HA' [ Hgg [Hginj Hg]]]]].
          destruct A' as [ P''' | F | C' ]; inverts HA'.
          forwards*: H8 H5 C'. apply mapN_concwf with f. rewrite <- H6. apply× mapN_concwf.
          destruct H4 as [F' [ HltsF' HaF' ]]. forwards: mapN_lts f HltsF'. simpl in H4.
          eexists; intuition (try eassumption).
          forwards*: rrenamed_def HaF' f. forwards*: rrenamed_def H10 g.
          repeat (rewrite <- mapN_appr in H11). repeat (rewrite <- H6 in H11). inverts Hgg.
          rewrite H13 in ×. asserts_rewrite (fmapN g (fmapN f a) = fmapN f a) in H11.
          { forwards: (amapN_id (fmapN f a)). inverts H12. rewrite H15 at 1.
            forwards: amapN_eq_on_fn (fmapN f a) g (fun x :nat ⇒ x). simpl. intros. apply Hg. fsetdec.
            simpl in H12; inverts H12. auto. }
          asserts_rewrite (fmapN g (fmapN f F') = fmapN f F') in H11.
          { forwards: (amapN_id (fmapN f F')). inverts H12. rewrite H15 at 1.
            forwards: amapN_eq_on_fn (fmapN f F') g (fun x :nat ⇒ x). simpl. intros. apply Hg. apply union_iff. right.
            forwards: lts_fn HltsF'. forwards: amapN_subset f F' (ag_proc Q). simpl; auto. simpl in ×. auto.
            simpl in H12; inverts H12. auto. }
          auto.
        - forwards*: mapN_lts_rev H2. destruct_hyps. destruct x0; inverts H5. destruct x; inverts H3.
          Opaque amapN fn_agent.
          forwards*: renaming F f (fn_agent (amapN f c) \u fn (mapN f Q)) (fn_agent c \u fn Q).
            rewrite map_union. rewrite fn_mapN. rewrite fn_agent_amapN. fsetdec.
          Transparent amapN fn_agent.
          destruct H3 as [A' [g [ HA' [ Hgg [Hginj Hg]]]]].
          destruct A' as [ P''' | F' | C ]; inverts HA'.
          forwards*: H8 H4 F'.
          destruct H3 as [C' [ HltsC' HaC' ]]. forwards: mapN_lts f HltsC'. simpl in H3.
          eexists; intuition (try eassumption).
          forwards*: rrenamed_def HaC' f. forwards*: rrenamed_def H9 g.
          repeat (rewrite <- mapN_appr in H10). repeat (rewrite <- H5 in H10). inverts Hgg.
          rewrite H12 in ×. asserts_rewrite (cmapN g (cmapN f c) = cmapN f c) in H10.
          { forwards: (amapN_id (cmapN f c)). inverts H11. rewrite H14 at 1.
            forwards: amapN_eq_on_fn (cmapN f c) g (fun x :nat ⇒ x). simpl. intros. apply Hg. fsetdec.
            simpl in H11; inverts H11. auto. }
          asserts_rewrite (cmapN g (cmapN f C') = cmapN f C') in H10.
          { forwards: (amapN_id (cmapN f C')). inverts H11. rewrite H14 at 1.
            forwards: amapN_eq_on_fn (cmapN f C') g (fun x :nat ⇒ x). simpl. intros. apply Hg. apply union_iff. right.
            forwards: lts_fn HltsC'. forwards: amapN_subset f C' (ag_proc Q). simpl; auto. simpl in ×. auto.
            simpl in H11; inverts H11. auto. }
          auto.
Qed.

Lemma bisim_rename_compatible : rename_compatible bisimilarity.
Proof.
  intros_all.
  forwards: bisim_exists_sym_rel H.
  destruct H1 as [Rel [Hsym [Hsim Hpq]]].
  ∃ (rel_renamed Rel).
  split.
  - apply sim_sym_imply_bisim.
    apply× simulation_rel_renamed.
    intros_all. induction H1. apply rrenamed_base; auto. eapply rrenamed_def; eauto.
  - eapply rrenamed_def; 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.

Require Import Sets.Finite_sets Sets.Ensembles.

Definition downV {V:Set} (x:incV V) := match x with
| VZ ⇒ None
| VS y ⇒ Some y
end.

Inductive Down {V:Set} (E: Ensemble (incV V)) : Ensemble V :=
| Down_def: ∀ x y, In (incV V) E x → downV x = Some y → In V (Down E) y.

Hint Constructors Down:sets.

Fixpoint fv {V: Set} (P:proc V) : Ensemble V :=
  match P with
 | pr_var x ⇒ Singleton V x
 | PO ⇒ Empty_set V
 | a ? P ⇒ Down (Setminus _ (fv P) (Singleton _ VZ))
 | a!(P) Q ⇒ (Union V (fv P) (fv Q))
 | P // Q ⇒ (Union V (fv P) (fv Q))
 | nu P ⇒ (fv P)
end.

Require Import Sets.Finite_sets_facts.

Lemma Down_empty {V:Set}: Down (Empty_set (incV V)) = Empty_set V.
Proof.
  apply Extensionality_Ensembles. split.
  + intros_all. inverts H. inverts H0.
  + intros_all. inverts H.
Qed.

Lemma Down_finite {V:Set} : ∀ E, Finite _ E → Finite V (Down E).
Proof.
  intros. induction H.
  - rewrite Down_empty. auto with sets.
  - remember (downV x) as y. destruct y. asserts_rewrite (Down (Add (incV V) A x) = Add V (Down A) v). {
    apply Extensionality_Ensembles. split. intros_all. destruct H1. destruct H1. apply Add_intro1.
    eauto with sets. inverts H1. rewrite <- Heqy in H2. inverts H2. auto with sets.
    intros_all. destruct H1. inverts H1. eapply Down_def; eauto. apply Add_intro1. auto. inverts H1.
    eauto with sets. }
    apply× Add_preserves_Finite.
    asserts_rewrite (Down (Add (incV V) A x) = Down A). {
    apply Extensionality_Ensembles. split. intros_all. destruct H1. destruct H1. eauto with sets.
    inverts H1. rewrite <- Heqy in H2. inverts H2.
    intros_all. destruct H1. eapply Down_def; eauto. apply Add_intro1. auto. } auto.
Qed.

Lemma fv_finite {V:Set} : ∀ P, Finite V (fv P).
Proof.
  induction P; simpl; auto with sets.
  - apply Singleton_is_finite.
  - apply× @Down_finite. apply Finite_downward_closed with (fv P). auto. intros_all.
    inverts H. auto.
  - apply× @Union_preserves_Finite.
  - apply× @Union_preserves_Finite.
Qed.

Definition s_restr {V:Set} (s:V → proc0) P:= (fun v ⇒ If In V (fv P) v then s v else (@pr_nil Datatypes.Empty_set)).

Lemma bind_eq_on_fv {V W:Set} : ∀ (P:proc V) (f:V→proc W) g,
  (∀ k, In _ (fv P) k → f k = g k) → bind f P = bind g P.
Proof.
  intros; gen W. induction P; intros; try solve [default_simp].
  - simpl. apply H. simpl. auto with sets.
  - simpl. fequals. apply IHP. intros [|]; simpl; auto. intros. fequals. apply H. simpl.
    apply Down_def with (VS v). apply Setminus_intro. auto. intros_all. inverts H1.
    simpl. auto.
  - simpl. fequals. apply IHP1. intros; apply H. simpl. auto with sets.
    apply IHP2. intros; apply H. simpl. auto with sets.
  - simpl. fequals. apply IHP1. intros; apply H. simpl. auto with sets.
    apply IHP2. intros; apply H. simpl. auto with sets.
  - simpl. fequals. apply IHP. intros. fequals. apply H. simpl. auto.
Qed.

Lemma restricted_fn {V:Set} : ∀ (s:V→proc0) P, ∃ E, ∀ v, fn (s_restr s P v) \c E.
Proof.
  intros. assert (∀ F, Included _ F (fv P) → ∃ E, ∀ v, In _ F v → fn (s_restr s P v) \c E).
  { intros. forwards*: finite_cardinal F. apply Finite_downward_closed with (fv P); auto with sets. apply fv_finite.
    destruct H0. gen F; induction x; intros.
  - forwards*: cardinal_invert H0. ∃ \{}. intros. unfold s_restr. default_simp.
  - forwards*: cardinal_invert H0. destruct H1 as [F' [v0 [HFv0 [ Hnotin Hcard]]]]. forwards*: IHx F'.
    intros_all. assert (In _ F x0). subst. auto with sets. auto with sets. destruct H1 as [E'].
    ∃ (fn (s v0) \u E'). intros. unfold s_restr. default_simp; try fsetdec.
    destruct (classic (v=v0)). subst. fsetdec.
    forwards*: H1 v. inverts H2; try solve [intuition]. inverts H4. false. unfold s_restr in H4; default_simp.
    fsetdec. }
  forwards*: H (fv P). auto with sets. destruct H0. ∃ x; intuition. destruct (classic (In _ (fv P) v)).
  intuition. unfold s_restr; default_simp. fsetdec.
Qed.

Require Import TLC.LibEpsilon.

Lemma invert_f_subs {V:Set}: ∀ (s:V→proc0) f, (∀ v x, x \in fn (s v) → ∃ y, x = f y) → ∃ (s':V→proc0),
  s = (fun v ⇒ mapN f (s' v)).
Proof.
  intros. assert (Hp0: Inhab proc0). apply Inhab_of_val. exact (@pr_nil Datatypes.Empty_set).
  ∃ (fun v ⇒ epsilon (fun P' ⇒ s v = mapN f P')). extens. intros; simpl.
  apply pred_epsilon. apply invert_f_proc. apply H.
Qed.

Lemma renaming_subs {V:Set}: ∀ (s:V → proc0) f E E' F, injective f → E [=] map f E' →
    (∀ v, fn (s v) \c F) → ∃ s' g,
    (fun x ⇒ mapN g (s x)) = (fun x ⇒ mapN f (s' x)) ∧ (fun x ⇒ mapN g (mapN g (s x))) = s ∧ injective g
    ∧ ∀ x, x \in E → g x = x.
Proof.
  intros. forwards*: renaming_sets F E 0. destruct H2 as [g [F' [F'' [HF' [HF'' [HF'E [HgF' [Hgg [Hginj [Hid Hlift]]]]]]]]]].
  forwards*: @invert_f_subs (fun v ⇒ mapN g (s v)) f. intros. assert (x \in map g F). gen H2 H1. clears_all.
  intros. simplfs. ∃ x0. intuition. apply (H1 v) in H0. auto. apply HF'' in H3. simplfs. eexists; eauto.
  destruct H2 as [s']. ∃ s' g; intuition.
  extens; intros. rewrite <- (mapN_id' (s x1)) at 2. rewrite mapN_mapN. apply mapN_eq_on_fn. intros. apply (H1 x1) in H3.
  auto. apply Hid. gen HF'E HgF' H3. clears_all. fsetdec.
Qed.

Lemma oe_rename: ∀ (Rel:binary proc0), (rename_compatible Rel) →
   ∀ V, (@rename_compatible V (open_extension Rel)).
Proof.
  intros_all.
  forwards*: @restricted_fn s (mapN f P // mapN f Q). destruct H1 as [F].
  remember (s_restr s (mapN f P // mapN f Q)) as srestr.
  forwards*:@renaming_subs srestr f (fn (mapN f P) \u fn (mapN f Q))(fn P \u fn Q) F.
    rewrite map_union. repeat rewrite fn_mapN. fsetdec.
  destruct H2 as [s' [g [Hgs' [ Hhg [ Hinjh Hh]]]]].
  forwards: H s'. forwards*: X H2 f. do 2 rewrite bind_mapN in H3.
  asserts_rewrite (bind (fun x : V ⇒ mapN f (s' x)) (mapN f P) = bind (fun x : V ⇒ mapN g (srestr x)) (mapN f P)) in H3.
    fequals.
  asserts_rewrite (bind (fun x : V ⇒ mapN f (s' x)) (mapN f Q) = bind (fun x : V ⇒ mapN g (srestr x)) (mapN f Q)) in H3.
    fequals.
  forwards*: X H3 g. do 2 rewrite bind_mapN in H4.
  asserts_rewrite (bind (fun x : V ⇒ mapN g (mapN g (srestr x))) (mapN g (mapN f P)) = bind srestr (mapN f P)) in H4.
    fequals. rewrite <- (mapN_id' (mapN f P)) at 2. apply mapN_eq_on_fn. intros. apply Hh. fsetdec.
  asserts_rewrite (bind (fun x : V ⇒ mapN g (mapN g (srestr x))) (mapN g (mapN f Q)) = bind srestr (mapN f Q)) in H4.
    fequals. rewrite <- (mapN_id' (mapN f Q)) at 2. apply mapN_eq_on_fn. intros. apply Hh. fsetdec.
  asserts_rewrite (bind srestr (mapN f P) = bind s (mapN f P)) in H4.
    apply bind_eq_on_fv. intros. subst. unfold s_restr. default_simp. false. apply n. auto with sets.
  asserts_rewrite (bind srestr (mapN f Q) = bind s (mapN f Q)) in H4.
    apply bind_eq_on_fv. intros. subst. unfold s_restr. default_simp. false. apply n. auto with sets.
  auto.
Qed.