Require Export Semantics.
Require Import TLC.LibEpsilon TLC.LibLogic.

Ltac auto_tilde ::= autofs.

Lemma permut_shiftN {V:Set}: ∀ (P:proc V) k n, k < n → mapN (permut k) (shiftN n P) = (shiftN n P).
Proof.
  intros. rewrite mapN_mapN. fequals.
  extens; intros. simpl_permut.
Qed.

Lemma open_injective {V:Set} : ∀ (P P':proc V) k x, open k x P = open k x P' →
    x \notin fn P → x \notin fn P' → P = P'.
Proof.
  induction P; simpl; intros; destruct P'; inverts H; auto.
  - simpl in H1. destruct n; destruct× n0; erewrite IHP; eauto;
    repeat case_if×. inverts C. inverts× C0. inverts× H3.
    inverts C. inverts H3. false¬.
    inverts C0. inverts H3. false¬.
    inverts× H3.
  - simpl in H1. destruct n; destruct n0; auto;
        erewrite IHP1; eauto; erewrite IHP2; eauto; repeat case_if×.
    inverts C. inverts× H3. inverts× C0.
    inverts× H3. inverts C. inverts× H3. false¬.
    inverts C0. inverts H3. false¬.
    inverts× H3.
  - simpl in H1. erewrite IHP1; eauto; erewrite IHP2; eauto.
  - simpl in H1. erewrite IHP; eauto.
Qed.

Lemma fn_open {V:Set}: ∀ (P:proc V) k x,
    (k \in bn P → fn (open k x P) = fn P \u \{ x})
    ∧ (k \notin bn P → fn (open k x P) = fn P).
Proof.
  induction P; simpl; intros.
  - autofs.
  - split; destruct n; repeat case_if; intros; specialize (IHP k x); destruct IHP.
    + destruct (classic (k \in bn P)). rewrite¬ H0. rewrite¬ H1.
    + rewrite in_union in H; destruct H. rewrite¬ H0. rewrite¬ H0.
    + rewrite¬ H0.
    + false. apply H. inverts¬ C.
    + rewrite H1. auto. intros_all¬.
    + rewrite× H1.
  - split; destruct n; repeat case_if; intros; specialize (IHP1 k x); destruct IHP1;
      specialize (IHP2 k x); destruct IHP2.
    + destruct (classic (k \in bn P1)); [rewrite× H0 | rewrite× H1 ];
      destruct (classic (k \in bn P2)); [rewrite¬ H2 | rewrite¬ H3 | rewrite¬ H2 | rewrite¬ H3 ].
    + rewrite in_union in H; destruct H. false. apply¬ C.
      rewrite in_union in H; destruct H.
      rewrite× H0. destruct (classic (k \in bn P2)); [ rewrite× H2 | rewrite× H3 ]; autofs.
      rewrite× H2. destruct (classic (k \in bn P1)); [ rewrite× H0 | rewrite× H1 ]; autofs.
    + rewrite in_union in H; destruct H; [
      rewrite× H0; destruct (classic (k \in bn P2)); [ rewrite× H2 | rewrite× H3 ]; autofs |
      rewrite× H2; destruct (classic (k \in bn P1)); [ rewrite× H0 | rewrite× H1 ]; autofs ].
    + false. inverts¬ C.
    + assert (k \notin bn P1). intros_all¬.
      assert (k \notin bn P2). intros_all¬.
      rewrite× H1. rewrite× H3.
    + assert (k \notin bn P1). intros_all¬.
      assert (k \notin bn P2). intros_all¬.
      rewrite× H1. rewrite× H3.
  - split; intros H12; specialize (IHP1 k x); destruct IHP1 as [H1 H2];
      specialize (IHP2 k x); destruct IHP2 as [H3 H4].
     rewrite in_union in H12; destruct H12; [
      rewrite× H1; destruct (classic (k \in bn P2)); [ rewrite× H3 | rewrite× H4 ]; autofs |
      rewrite× H3; destruct (classic (k \in bn P1)); [ rewrite× H1 | rewrite× H2 ]; autofs ].
    assert (k \notin bn P1). intros_all¬.
    assert (k \notin bn P2). intros_all¬.
      rewrite× H2. rewrite× H4.
  - split; intros H; specialize (IHP (S k) x); destruct IHP as [H1 H2].
    rewrite down_fset_spec' in H. rewrite× H1.
    rewrite× H2. intros_all. apply H. rewrite× down_fset_spec'.
  - split¬.
Qed.

Lemma fn_open_in {V:Set}: ∀ (P:proc V) k x, k \in bn P → fn (open k x P) = fn P \u \{ x}.
Proof.
  intros. forwards: @fn_open P k x. intuition.
Qed.

Lemma fn_open_sub {V:Set}: ∀ (P:proc V) k x, fn (open k x P) \c fn P \u \{ x}.
Proof.
  intros. forwards: @fn_open P k x. destruct H. destruct (classic (k \in bn P)).
  - rewrite¬ H.
  - rewrite¬ H0.
Qed.

Lemma fn_open_rev {V:Set}: ∀ (P:proc V) k x, fn P \c fn (open k x P).
Proof.
  intros. forwards: @fn_open P k x. destruct H. destruct (classic (k \in bn P)).
  - rewrite¬ H.
  - rewrite¬ H0.
Qed.

Lemma fn_agent_open_rev : ∀ A k x, fn_agent A \c fn_agent (open_agent k x A).
Proof.
  intros. destruct A as [ | [] | [] ]; simpl; auto using fn_open_rev.
   assert (fn p \c fn (open (k+n) x p)) by (apply fn_open_rev).
   assert (fn p0 \c fn (open (k+n) x p0)) by (apply fn_open_rev). autofs.
Qed.

Lemma fn_close {V:Set}: ∀ (P:proc V) k x, fn (close k x P) = fn P \- \{ x}.
Proof.
  induction P; simpl; intros; auto; try solve [autofs].
  - destruct n; case_if; simpl; try (rewrite IHP); intuition.
    + inverts¬ C.
    + autofs. left. intuition. inverts× H.
  - destruct n; case_if; simpl; try (rewrite IHP1); try (rewrite IHP2).
    + autofs.
    + inverts¬ C.
    + autofs. left. intuition. inverts× H.
  - rewrite IHP1; rewrite¬ IHP2.
Qed.

Lemma fn_mapV {V W:Set} : ∀ (P:proc V) (f: V → W), fn (mapV f P) = fn P.
Proof.
  intros; gen W; induction P; simpl; auto; intros.
  - destruct n; rewrite× IHP.
  - destruct n; rewrite× IHP1; rewrite× IHP2.
  - rewrite IHP1; rewrite× IHP2.
Qed.

Lemma fn_mapN {V} : ∀ (P:proc V) f, fn (mapN f P) = fn P.
Proof.
  induction P; simpl; auto; intros.
  - destruct n; simpl; auto. rewrite× IHP.
  - destruct n; simpl; rewrite IHP1; rewrite× IHP2.
  - rewrite IHP1; rewrite× IHP2.
Qed.

Lemma fn_bind' {V W:Set} : ∀ (P:proc V) (f g: V → proc W) x, x \in fn (bind g P) →
    (∀ v, fn (g v) = fn (f v)) →
    (∀ v, x \notin fn (f v)) → x \in fn P.
Proof.
  intros; gen W; induction P; simpl; auto; intros.
  - false. eapply H1. rewrite H0 in H. apply H.
  - destruct n. forwards: IHP (liftV f) H; try (
    intros [ |]; simpl; auto; intros; repeat (rewrite× @fn_mapV)); auto.
    autofs. right. eapply IHP; eauto.
    intros [ |]; simpl; auto; intros; repeat (rewrite fn_mapV). rewrite× (H0 v0).
  - destruct n. autofs. left. eapply IHP1; eauto. right; eapply IHP2; eauto.
    autofs. eapply IHP1 in H; eauto. eapply IHP2 in H; eauto.
  - autofs. eapply IHP1 in H2; auto. eapply IHP2 in H2; auto.
  - eapply IHP. apply H. intros. simpl. apply fn_mapN.
    intros; specialize (H1 v); rewrite <- (H0 v) in H1; auto.
Qed.

Lemma fn_bind {V W:Set} : ∀ (P:proc V) (f: V → proc W) x, x \in fn (bind f P) →
    (∀ v, x \notin fn (f v)) → x \in fn P.
Proof.
  intros. eapply fn_bind'; eauto.
Qed.

Lemma fn_subst {V:Set}: ∀ P (Q: proc V), fn (subst P Q) \c fn P \u fn Q.
Proof.
  intros_all.
  destruct (classic (x \in fn Q)). autofs.
  apply fn_bind in H. autofs.
  destruct v; simpl; auto.
Qed.

Lemma bn_open {V:Set}: ∀ (P:proc V) k x, bn (open k x P) = bn P \- \{ k}.
Proof.
  induction P; simpl; intros; auto; try solve [autofs].
  - destruct n; case_if; simpl; try (rewrite¬ IHP).
    inverts¬ C.
  - destruct n; case_if; simpl; try (rewrite IHP1); try (rewrite¬ IHP2).
    inverts¬ C.
  - rewrite IHP1; rewrite¬ IHP2.
  - apply fset_extens.
    + intros_all. rewrite down_fset_spec' in H. rewrite¬ IHP in H.
      rewrite¬ down_fset_spec'.
    + intros_all. rewrite¬ down_fset_spec'.
      rewrite IHP. rewrite¬ down_fset_spec' in H.
Qed.

Lemma bn_close {V:Set}: ∀ (P:proc V) k x,
    (x \in fn P → bn (close k x P) = bn P \u \{ k})
    ∧ (x \notin fn P → bn (close k x P) = bn P).
Proof.
  induction P; simpl; intros.
  - split¬.
  - split; destruct n; repeat case_if; intros; specialize (IHP k x); destruct IHP.
    + rewrite¬ H0.
    + destruct (classic (x \in fn P)). rewrite¬ H0. rewrite¬ H1.
    + destruct (classic (x \in fn P)). rewrite¬ H0. false. autofs.
    + rewrite× H1.
    + false. inverts¬ C.
    + rewrite¬ H1.
  - split; destruct n; repeat case_if; intros; specialize (IHP1 k x); destruct IHP1;
      specialize (IHP2 k x); destruct IHP2.
    + rewrite in_union in H; destruct H; [
      rewrite× H0; destruct (classic (x \in fn P2)); [ rewrite× H2 | rewrite× H3 ]; autofs |
      rewrite× H2; destruct (classic (x \in fn P1)); [ rewrite× H0 | rewrite× H1 ]; autofs ].
    + repeat (rewrite in_union in H). destruct H.
      destruct (classic (x \in fn P1)); [
        rewrite× H0; destruct (classic (x \in fn P2)); [ rewrite× H2 | rewrite× H3 ]; autofs |
        rewrite× H1; destruct (classic (x \in fn P2)); [ rewrite× H2 | rewrite× H3 ]; autofs ].
      destruct H; [
      rewrite× H0; destruct (classic (x \in fn P2)); [ rewrite× H2 | rewrite× H3 ]; autofs |
      rewrite× H2; destruct (classic (x \in fn P1)); [ rewrite× H0 | rewrite× H1 ]; autofs ].
    + repeat (rewrite in_union in H). destruct H. false. autofs.
      destruct H; [
      rewrite× H0; destruct (classic (x \in fn P2)); [ rewrite× H2 | rewrite× H3 ]; autofs |
      rewrite× H2; destruct (classic (x \in fn P1)); [ rewrite× H0 | rewrite× H1 ]; autofs ].
    + assert (x \notin fn P1). intros_all. autofs.
      assert (x \notin fn P2). intros_all. autofs.
      rewrite× H1. rewrite× H3.
    + false. inverts¬ C.
    + assert (x \notin fn P1). intros_all¬.
      assert (x \notin fn P2). intros_all¬.
      rewrite× H1. rewrite× H3.
  - split; intros H12; specialize (IHP1 k x); destruct IHP1 as [H1 H2];
      specialize (IHP2 k x); destruct IHP2 as [H3 H4].
     rewrite in_union in H12; destruct H12; [
      rewrite× H1; destruct (classic (x \in fn P2)); [ rewrite× H3 | rewrite× H4 ]; autofs |
      rewrite× H3; destruct (classic (x \in fn P1)); [ rewrite× H1 | rewrite× H2 ]; autofs ].
    assert (x \notin fn P1). intros_all¬.
    assert (x \notin fn P2). intros_all¬.
      rewrite× H2. rewrite× H4.
  - split; intros H; specialize (IHP (S k) x); destruct IHP as [H1 H2].
    apply fset_extens; intros_all.
    rewrite down_fset_spec' in H0. rewrite in_union. rewrite down_fset_spec'.
    rewrite¬ H1 in H0.
    rewrite down_fset_spec'. rewrite in_union in H0. destruct H0.
    rewrite down_fset_spec' in H0. rewrite¬ H1; auto.
    rewrite¬ H1.
    apply fset_extens; intros_all.
    rewrite down_fset_spec' in H0. rewrite down_fset_spec'.
    rewrite× H2 in H0.
    rewrite down_fset_spec'. rewrite down_fset_spec' in H0. rewrite× H2.
  - autofs.
Qed.

Lemma bn_mapN {V:Set}: ∀ (P:proc V) f, bn (mapN f P) = map_fset f (bn P).
Proof.
  induction P; simpl; intros_all; try solve [autofs].
  - destruct n; try (rewrite map_union in *); simpl; try (rewrite IHP);
      try (rewrite× map_singleton); auto.
  - destruct n; repeat (rewrite map_union in *); simpl; try (rewrite IHP1); try (rewrite IHP2);
      try (rewrite map_singleton); auto.
  - repeat (rewrite map_union in *); simpl; try (rewrite IHP1); try (rewrite IHP2); auto.
  - autofs.
    rewrite down_fset_spec' in ×. rewrite IHP in H.
    apply map_fset_spec in H. destruct H. simpl_liftN.
    ∃ (x0 -1); intuition. apply down_fset_spec'.
    replace (S (x0 -1)) with x0 by omega. auto.
    apply down_fset_spec'.
    rewrite down_fset_spec' in H0. rewrite IHP. apply map_fset_spec.
    ∃ (S x0). simpl_liftN. intuition.
Qed.

Lemma bn_close_in {V:Set}: ∀ (P:proc V) k x, x \in fn P → bn (close k x P) = bn P \u \{ k}.
Proof.
  intros; forwards: @bn_close P k x; intuition.
Qed.

Lemma bn_close_sub {V:Set} : ∀ (P:proc V) k x, bn (close k x P) \c bn P \u \{ k }.
Proof.
  intros. forwards: @bn_close P k x. destruct (classic (x \in fn P)); intuition; rewrite¬ H.
Qed.

Lemma bn_mapV {V W:Set} : ∀ (P:proc V) (f: V → W), bn (mapV f P) = bn P.
Proof.
  intros; gen W; induction P; simpl; auto; intros.
  - destruct n; rewrite× IHP.
  - destruct n; rewrite IHP1; rewrite× IHP2.
  - rewrite IHP1; rewrite× IHP2.
  - autofs. rewrite down_fset_spec'. rewrite down_fset_spec' in H. erewrite <- IHP; eauto.
    rewrite down_fset_spec'. rewrite down_fset_spec' in H. erewrite IHP; eauto.
Qed.

Lemma bn_bind' {V W:Set} : ∀ (P:proc V) (f g: V → proc W) k, k \in bn (bind g P) →
    (∀ v, bn (g v) = bn (f v)) →
    (∀ v, k \notin bn (f v)) → k \in bn P.
Proof.
  intros; gen W k; induction P; simpl; auto; intros.
  - false. eapply H1. rewrite H0 in H. apply H.
  - destruct n. autofs. right. eapply IHP; eauto. intros [ |]; simpl; auto.
    intros. rewrite bn_mapV. rewrite H0; auto. eapply IHP; eauto.
    intros [ |]; simpl; auto. intros. rewrite bn_mapV. rewrite H0; auto.
  - destruct n. autofs. eapply IHP1 in H; eauto. eapply IHP2 in H; auto.
    autofs. eapply IHP1 in H2; auto. eapply IHP2 in H2; auto.
  - autofs. eapply IHP1 in H2; auto. eapply IHP2 in H2; auto.
  - rewrite down_fset_spec'. rewrite down_fset_spec' in H.
     forwards*: IHP (fun x : V ⇒ mapN (fun x0 ⇒ S x0) (f x)) H.
    intros. repeat (rewrite bn_mapN). rewrite× H0.
    intros. rewrite bn_mapN. intros_all. apply (H1 v). rewrite map_fset_spec in H2.
    destruct H2. intuition. inverts× H3.
Qed.

Lemma bn_bind {V W:Set} : ∀ (P:proc V) (f: V → proc W) k, k \in bn (bind f P) →
    (∀ v, k \notin bn (f v)) → k \in bn P.
Proof.
  intros. eapply bn_bind'; eauto.
Qed.

Lemma bn_subst {V:Set}: ∀ P (Q: proc V), bn (subst P Q) \c bn P \u bn Q.
Proof.
  intros_all.
  destruct (classic (x \in bn Q)). autofs.
  apply bn_bind in H. autofs.
  destruct v; simpl; auto.
Qed.

Lemma is_proc_bn {V:Set} : ∀ (P:proc V), is_proc P → bn P = \{}.
Proof.
  induction 1; simpl; auto; intros.
  - rewrite IHis_proc1; rewrite¬ IHis_proc2.
  - rewrite IHis_proc1; rewrite¬ IHis_proc2.
  - pick_fresh_V V y. forwards*: H0 y. rewrite× @bn_open in H1.
    rewrite¬ H1. rewrite¬ down_fset_spec in H2.
Qed.

Lemma size_open {V:Set} : ∀ (P:proc V) k x, size (open k x P) = size P.
Proof.
  induction P; intros; simpl; auto.
Qed.

Lemma is_proc_bn_rev {V:Set} : ∀ (P:proc V), bn P = \{} → is_proc P.
Proof.
  induction P using size_induction; destruct P; simpl; auto with hopi.
  - destruct n; intros. assert (n \in \{}). rewrite¬ <- H0. autofs.
    apply proc_inp. apply× H. simpl. intuition.
  - destruct n; intros. assert (n \in \{}). rewrite¬ <- H0. autofs.
    assert (bn P1 = \{}). apply fset_extens. rewrite¬ <- H0. autofs.
    assert (bn P2 = \{}). apply fset_extens. rewrite¬ <- H0. autofs.
    apply proc_out. apply H; auto. simpl; intuition. apply× H. simpl; intuition.
  - intros_all. assert (bn P1 = \{}). apply fset_extens. rewrite¬ <- H0. autofs.
    assert (bn P2 = \{}). apply fset_extens. rewrite¬ <- H0. autofs.
    apply proc_par; apply H; auto; simpl; intuition.
  - intros. apply (proc_nu \{}). intros. apply H; auto.
    rewrite size_open; simpl; intuition. apply fset_extens_rev in H0.
    rewrite¬ @bn_open. destruct x0. autofs.
    forwards*: H0 x0. rewrite× down_fset_spec'. autofs.
Qed.

Lemma close_open {V:Set} : ∀ (P:proc V) k x, x \notin fn P → close k x (open k x P) = P.
Proof.
  induction P; simpl; auto; intros.
  - destruct n; simpl; auto. repeat case_if; rewrite× IHP.
    inverts× C0.
    repeat case_if. false. inverts C. autofs. rewrite× IHP.
  - destruct n; simpl. repeat case_if; rewrite× IHP1; try (rewrite× IHP2).
    inverts× C0.
    repeat case_if. false. inverts C. autofs.
    rewrite× IHP1. rewrite× IHP2.
  - intros. rewrite× IHP1. rewrite× IHP2.
  - intros. rewrite× IHP.
Qed.

Lemma close_open_neq {V:Set}: ∀ (P:proc V) k1 k2 x y, (x≠y) → (k1≠k2) →
    close k1 x (open k2 y P) = open k2 y (close k1 x P).
Proof.
  induction P; simpl; auto; intros.
  - repeat (case_if; simpl); try (rewrite× IHP).
  - repeat (case_if; simpl); try (rewrite× IHP1); try (rewrite× IHP2).
  - try (rewrite× IHP1); try(rewrite× IHP2).
  - rewrite× IHP.
Qed.

Lemma open_open {V:Set}: ∀ (P:proc V) k1 k2 x y, (k1≠k2) →
    open k1 x (open k2 y P) = open k2 y (open k1 x P).
Proof.
  induction P; simpl; auto; intros.
  - repeat (case_if; simpl); try (rewrite× IHP).
  - repeat (case_if; simpl); try (rewrite× IHP1); try (rewrite× IHP2).
  - try (rewrite× IHP1); try(rewrite× IHP2).
  - rewrite× IHP.
Qed.

Lemma close_close {V:Set}: ∀ (P:proc V) k1 k2 x y, (x≠y) →
    close k1 x (close k2 y P) = close k2 y (close k1 x P).
Proof.
  induction P; simpl; auto; intros.
  - repeat (case_if; simpl); try (rewrite× IHP).
  - repeat (case_if; simpl); try (rewrite× IHP1); try (rewrite× IHP2).
  - try (rewrite× IHP1); try(rewrite× IHP2).
  - rewrite× IHP.
Qed.

Lemma open_close_gen {V:Set} : ∀ (P:proc V) k x, k \notin bn P → (open k x (close k x P)) = P.
Proof.
  induction P; simpl; auto; intros.
  - destruct n; repeat (case_if);
      assert (k \notin bn P) by intros_all~; rewrite× IHP.
    inverts C. false. apply¬ H. inverts× C0.
  - destruct n; repeat (case_if);
      assert (k \notin bn P1) by intros_all~; rewrite× IHP1;
      assert (k \notin bn P2) by intros_all~; rewrite× IHP2.
    inverts C. false. apply¬ H. inverts× C0.
  - assert (k \notin bn P1) by intros_all~; rewrite× IHP1;
    assert (k \notin bn P2) by intros_all~; rewrite× IHP2.
  - rewrite× IHP. autofs. apply H. rewrite× down_fset_spec'.
Qed.

Lemma open_close {V:Set} : ∀ (P:proc V), is_proc P → ∀ k x, (open k x (close k x P)) = P.
Proof.
  intros; apply open_close_gen. forwards: @is_proc_bn H. rewrite H0; intros_all¬.
Qed.

Lemma close_id {V:Set} : ∀ (P:proc V) k x, x \notin fn P →
    close k x P = P.
Proof.
  induction P; simpl; auto; intros.
  - destruct n. case_if. rewrite× IHP.
    case_if. inverts C. false¬. rewrite× IHP.
  - destruct n. case_if. rewrite× IHP1. rewrite× IHP2.
    case_if. inverts C. false¬. rewrite× IHP1. rewrite× IHP2.
  - rewrite× IHP1. rewrite× IHP2.
  - rewrite× IHP.
Qed.

Lemma open_id {V:Set}: ∀ (P:proc V) k x, k \notin bn P → open k x P = P.
Proof.
  induction P; simpl; auto; intros.
  - destruct n; case_if; auto; simpl in H;
      try solve [rewrite IHP; assert (k \notin bn P) by (intros_all~); auto].
     inverts C. false¬.
  - destruct n; case_if; auto; simpl in H;
      try solve [assert (k \notin bn P1) by intros_all~;
                 assert (k \notin bn P2) by intros_all~;
                 rewrite× IHP1; rewrite× IHP2].
     inverts C. false¬.
  - assert (k \notin bn P1) by intros_all~;
    assert (k \notin bn P2) by intros_all~; rewrite× IHP1; rewrite× IHP2.
  - rewrite× IHP. intros_all¬. apply H. rewrite¬ down_fset_spec. omega.
Qed.

Lemma is_proc_open {V :Set}: ∀ (P:proc V) k x, is_proc P →
    open k x P = P.
Proof.
  intros. rewrite× @open_id. apply is_proc_bn in H. rewrite× H.
Qed.

Lemma is_proc_open_close {V:Set}: ∀ P k x z, is_proc P →
    @is_proc V (open k x (close k z P)).
Proof.
  intros; gen k. induction H; simpl; auto with hopi; intros.
  - repeat (case_if; auto with hopi).
  - repeat (case_if; auto with hopi).
  - apply (proc_nu (L \u \{ z })); eauto; intros. assert (x0 \notin L) by intuition.
    forwards: H0 x0 H2 (S k). rewrite close_open_neq in H3; auto.
    rewrite× @open_open.
Qed.

Lemma mapV_close {A B : Set} : ∀ (P : proc A) k b (f : A → B),
  mapV f (close k b P) = close k b (mapV f P).
Proof.
  intros. gen B k.
  induction P as [ A x | A a P IHP | A a P IHP Q IHQ
                     | A P IHP Q IHQ | A P IHP | A ]; simpl; intros;
  try (erewrite IHP); try (erewrite IHQ); auto.
Qed.

Lemma mapV_open {V W:Set}: ∀ (P:proc V) k x (f:V→W),
  mapV f (open k x P) = open k x (mapV f P).
Proof.
  intros. gen W k. induction P; auto; intros; simpl.
  - case_if; simpl; rewrite× IHP.
  - case_if; simpl; rewrite× IHP1; rewrite× IHP2.
  - rewrite× IHP1; rewrite× IHP2.
  - rewrite× IHP.
Qed.

Lemma is_proc_mapV {V W:Set}: ∀ (P:proc V) (f:V→W), is_proc P → is_proc (mapV f P).
Proof.
  intros. gen W. induction H; simpl; auto with hopi.
   intros. apply (proc_nu L). intros. rewrite <- mapV_open. apply× H0.
Qed.

Lemma mapN_open_gen {V}: ∀ (P:proc V) k y f,
    (∀ y, y \in bn P → f k = f y → k = y) →
    mapN f (open k y P) = open (f k) y (mapN f P).
Proof.
  induction P; intros; simpl; auto.
  - destruct n; case_if; simpl. rewrite IHP. case_if×.
    intros. apply× H. simpl. autofs.
    rewrite IHP. case_if×.
      inverts C0. forwards: H H1. simpl. autofs. false.
    intros. apply× H. simpl. autofs.
    case_if. rewrite× IHP.
  - destruct n; case_if; simpl; rewrite× IHP1; try (rewrite× IHP2); try case_if*;
      try (intros; apply× H; simpl; autofs).
      inverts C0. forwards*: H H1. simpl; autofs. false.
  - simpl; rewrite× IHP1; try (rewrite× IHP2); try case_if*;
      try (intros; apply× H; simpl; autofs).
  - forwards: IHP (S k) y (liftN f 1).
      intros. simpl_liftN.
      forwards: H (y0-1).
      rewrite down_fset_spec'. replace (S(y0-1)) with y0 by omega.
      auto. replace (S k - 1) with k in H1; omega. omega.
    rewrite× H0. repeat fequals.
    simpl_liftN. rewrite× <- minus_n_O.
Qed.

Lemma mapN_open {V}: ∀ (P:proc V) k y f, injective f →
    mapN f (open k y P) = open (f k) y (mapN f P).
Proof.
  intros; rewrite× @mapN_open_gen.
Qed.

Lemma bind_open' {V W:Set}: ∀ (P:proc V) k x (f:V→ proc W),
    bind (fun y ⇒ open k x (f y)) (open k x P) = open k x (bind f P).
Proof.
  intros. gen k W. induction P; simpl; intros; auto.
  - replace (liftV (fun y : V ⇒ open k x (f y))) with
      (fun y ⇒ open k x ((liftV f) y)). rewrite× IHP.
    extens. intros [|v]; simpl; auto. rewrite× @mapV_open.
  - rewrite× IHP1; rewrite× IHP2.
  - rewrite× IHP1; rewrite× IHP2.
  - rewrite× <- IHP. repeat fequals.
    extens; intros. rewrite mapN_open; auto. intros_all; omega.
Qed.

Lemma bind_open {V W:Set}: ∀ (P:proc V) k x (f:V→ proc W),
    (∀ y, is_proc (f y)) → bind f (open k x P) = open k x (bind f P).
Proof.
  intros. rewrite <- bind_open'. repeat fequals.
  extens; intros. rewrite× @is_proc_open.
Qed.

Lemma open_subst {V:Set}: ∀ P (Q:proc V) k x, open k x (subst P Q) =
    subst (open k x P)(open k x Q).
Proof.
  intros; rewrite <- bind_open'. repeat fequals.
    extens. intros [|]; simpl; auto.
Qed.

Lemma mapN_close {V:Set} : ∀ (P:proc V) k x f, close (f k) x (mapN f P) = mapN f (close k x P).
Proof.
  induction P; simpl; auto; intros.
  - destruct n. case_if. simpl. case_if. rewrite× IHP.
    case_if; simpl. case_if. rewrite× IHP.
    case_if. rewrite× IHP.
  - destruct n. case_if. simpl. case_if. rewrite× IHP1; rewrite× IHP2.
    case_if; simpl. case_if. rewrite× IHP1; rewrite× IHP2.
    case_if. rewrite× IHP1; rewrite× IHP2.
  - rewrite× IHP1; rewrite× IHP2.
  - rewrite× <- IHP. repeat fequals. simpl_liftN. rewrite× <- minus_n_O.
Qed.

Lemma bind_close' {V W:Set}: ∀ (P:proc V) k x (f:V→ proc W),
    bind (fun y ⇒ close k x (f y)) (close k x P) = close k x (bind f P).
Proof.
  intros. gen k W. induction P; simpl; intros; auto.
  - replace (liftV (fun y : V ⇒ close k x (f y))) with
      (fun y ⇒ close k x ((liftV f) y)). rewrite× IHP.
    extens. intros [|]; auto. intros. simpl. rewrite× @mapV_close.
  - rewrite× IHP1; rewrite× IHP2.
  - rewrite× IHP1; rewrite× IHP2.
  - rewrite× <- IHP. repeat fequals.
    extens; intros. rewrite× @mapN_close.
Qed.

Lemma close_subst {V:Set}: ∀ P (Q:proc V) k x, close k x (subst P Q) =
    subst (close k x P)(close k x Q).
Proof.
  intros; rewrite <- bind_close'. repeat fequals.
    extens. intros [|]; simpl; auto.
Qed.

Lemma is_proc_mapN {V:Set} : ∀ (P:proc V) f, is_proc P → mapN f P = P.
Proof.
  intros; gen f; induction H; simpl; auto; intros.
  - rewrite× IHis_proc.
  - rewrite× IHis_proc1; rewrite× IHis_proc2.
  - rewrite× IHis_proc1; rewrite× IHis_proc2.
  - pick_fresh_V V y. assert (y \notin L) by auto. forwards: H0 y H1 (liftN f 1).
    assert (close ((liftN f 1) 0) y (mapN (liftN f 1) (open 0 y P))
             = close ((liftN f 1) 0) y (open 0 y P)) by fequals.
    rewrite (mapN_close _ 0 y (liftN f 1)) in H3. replace ((liftN f 1) 0) with 0 in H3 by simpl_liftN.
    rewrite close_open in H3; auto. rewrite× H3.
Qed.

Lemma is_proc_bind {V W:Set}: ∀ (P:proc V) (f:V→ proc W), is_proc P →
    (∀ x, is_proc (f x)) → is_proc (bind f P).
Proof.
  intros. gen W. induction H; simpl; auto with hopi.
  - intros. apply proc_inp. apply IHis_proc. intros [ |x]; simpl; auto with hopi.
    apply× @is_proc_mapV.
  - intros. apply (proc_nu L). intros.
    assert (∀ y : V, is_proc (mapN (fun x0 : nat ⇒ S x0) (f y))).
      intros; rewrite× @is_proc_mapN.
    rewrite× <- @bind_open.
Qed.

Lemma is_proc_rename {V:Set} : ∀ (P:proc V) k x, is_proc (open k x P) → ∀ y,
    is_proc (open k y P).
Proof.
  introv H. remember (open k x P) as P'. gen k.
  induction H; intros; simpl; destruct P; try (inverts HeqP'; case_if; case_if); simpl in HeqP';
  inverts HeqP'; simpl; auto with hopi.
  - case_if; inverts H1; auto with hopi.
  - case_if; inverts H2; auto with hopi.
  - apply (proc_nu L). intros. rewrite× @open_open.
    eapply H0. exact H1. rewrite open_open; eauto.
Qed.

Definition body {V:Set} (P:proc V) k := ∀ x, is_proc (open k x P).

Definition decomp {V:Set} (P:proc V) k x R : Prop :=
     P = open k x R ∧ x \notin fn R ∧ body R k.

Lemma decomp_proc_gen {V:Set}: ∀ (P:proc V) k x, k \notin bn P → ∃ R,
     P = open k x R ∧ x \notin fn R.
Proof.
  intros. ∃ (close k x P).
  splits. rewrite× @open_close_gen.
  rewrite fn_close. intros_all¬.
Qed.

Lemma decomp_proc {V:Set}: ∀ (P:proc V) k x, is_proc P → ∃ R, (decomp P k x R).
Proof.
  intros; unfold decomp.
  destruct (decomp_proc_gen P k x) as [R]. apply is_proc_bn in H.
  rewrite H; intros_all¬.
  ∃ R; intuition.
  subst. intros_all; eapply is_proc_rename; eauto.
Qed.

Definition decomp_f {V W:Set} (f:V → proc W) k x (H:∀ v, is_proc (f v)) :
  ∃ f', ∀ (v:V), @decomp W (f v) k x (f' v).
Proof.
  assert (Inhab (proc W)).
  apply Inhab_of_val. exact PO.
  ∃ (fun (v:V) ⇒ epsilon (fun R ⇒ (decomp (f v) k x R))).
  intros.
  apply pred_epsilon. apply decomp_proc. apply (H v).
Qed.

Ltac pick_freshes_fset_V V L' n x :=
  let L := gather_vars V in (pick_freshes_gen (L \u L') n x).

Ltac pick_freshes_V V n x :=
  let L := gather_vars V in (pick_freshes_gen L n x).

Fixpoint open_list {V:Set} l (P:proc V) := match l with
| nil ⇒ P
| x::l' ⇒ open (length l') x (open_list l' P)
end.

Lemma open_list_id {V:Set} (P:proc V) l : is_proc P → open_list l P = P.
Proof.
  induction l; simpl; auto.
   intros. rewrite× IHl. forwards: @is_proc_bn H. rewrite× @open_id.
   intros_all. rewrite¬ H0 in H1.
Qed.

Lemma open_list_par {V:Set} : ∀ (P Q:proc V) l, open_list l (P // Q) = open_list l P // open_list l Q.
Proof.
  induction l; simpl; auto; intros.
    rewrite IHl. simpl. auto.
Qed.

Lemma open_list_bind {V W:Set} : ∀ (P:proc V) l (f:V → proc W), open_list l (bind f P)
    = bind (fun x ⇒ open_list l (f x)) (open_list l P).
Proof.
  induction l; simpl; auto; intros.
    rewrite IHl. rewrite× @bind_open'.
Qed.

Lemma open_list_subst {V:Set} : ∀ P l (Q:proc V), open_list l (subst P Q)
    = subst (open_list l P) (open_list l Q).
Proof.
  intros; rewrite open_list_bind.
  repeat fequals.
    extens. intros [ |]; simpl; auto. intros; induction l; simpl; auto.
    rewrite IHl; simpl; auto.
Qed.

Lemma open_open_list {V:Set} : ∀ (P:proc V) k x l,
  k ≥ length l → open k x (open_list l P) = open_list l (open k x P).
Proof.
  intros; gen k. induction l; simpl; intros; auto. rewrite length_cons in H.
  rewrite× @open_open; try omega. rewrite× IHl. omega.
Qed.

Lemma is_proc_open_list {V:Set} : ∀ (P:proc V) l,
   (∀ k, k \in bn P → k < length l) → is_proc (open_list l P).
Proof.
  intros. gen P. induction l; intros.
  - simpl in ×. rewrite length_nil in H. assert (bn P = \{}).
    apply¬ fset_extens. forwards*: H x. omega.
    apply× @is_proc_bn_rev.
  - simpl. rewrite length_cons in H. rewrite open_open_list; try omega.
    apply IHl; try omega. intros. rewrite¬ @bn_open in H0.
    forwards*: H k. omega.
Qed.

Lemma fn_open_list_sub {V:Set} : ∀ (P:proc V) l,
   fn (open_list l P) \c fn P \u from_list l.
Proof.
  intros; gen P. induction l; simpl; try solve [autofs].
    intros. rewrite open_open_list; try omega. intros_all. apply IHl in H. autofs.
    apply fn_open_sub in H0. autofs. subst. right. rewrite¬ from_list_cons.
    right. rewrite¬ from_list_cons.
Qed.