Require Export HOASSyntax.

Notation abs := proc1 (only parsing).

Inductive conc : Set :=
| conc_def : proc0 → proc0 → conc
| conc_nu : (name → conc) → conc
.

Inductive conc_notin : name → conc → Prop :=
| nc_def : ∀ a P Q, notin a P → notin a Q →
            conc_notin a (conc_def P Q)
| nc_nu : ∀ a C, (∀ b, a≠b → conc_notin a (C b)) →
            conc_notin a (conc_nu C).

Hint Constructors conc_notin:hopi.

Definition conc_notin_ho a C :=
      ∀ b, a≠b → conc_notin a (C b).

Ltac simpl_conc_notin :=
  repeat match goal with
  | [ H : conc_notin _ ?t |- _ ] ⇒ head_constructor t; inverts H
  | [ H : conc_notin _ _ ∧ _ |- _ ] ⇒ destruct H
  end.
Ltac simpl_notin ::=
  repeat (simpl_notin_list; simpl_notin_proc; simpl_conc_notin; simpl in *; auto).

Axiom conc_ext : ∀ a C C', conc_notin_ho a C →
  conc_notin_ho a C' → C a = C' a → C = C'.

Ltac auto_conc_ext :=
  match goal with
  | [ H : ?P ?X = ?Q ?X |- _ ] ⇒
    (forwards*: @conc_ext X P Q; intros_all; auto with hopi);
    subst; simpl_notin; clear H; auto with hopi
  end.

Axiom conc_beta_exp : ∀ a C,
  ∃ C', conc_notin_ho a C' ∧ C = C' a.
Axiom conc_ho_beta_exp : ∀ a (C:name → conc),
  ∃ C', conc_notin_ho a (fun x ⇒ conc_nu (C' x)) ∧ C = C' a.
Axiom conc_ho_ho_beta_exp : ∀ a (C:name → name → conc),
  ∃ C', conc_notin_ho a
    (fun y ⇒ conc_nu (fun x ⇒ conc_nu (C' x y))) ∧ C = C' a.

Ltac conc_exp x C := let Cr := fresh C in
   destruct (conc_beta_exp x C) as [Cr []]; subst.
Ltac ho_conc_exp x C := let Cr := fresh C in
   destruct (conc_ho_beta_exp x C) as [Cr []]; subst.

Ltac all_conc_exp x := repeat match goal with
  | [ C : conc |- _ ] ⇒ conc_exp x C
  | [ P : proc _ |- _ ] ⇒ exp x P
  end.

Ltac conc_change_ext :=
  match goal with
  | [ H : ?C = ?C' ?x |- _ ] ⇒
    let C'' := (eval pattern x in C) in change (C'' = C' x) in H; auto_conc_ext
  end.
Ltac conc_exp_ext x := all_conc_exp x; repeat conc_change_ext.

Axiom conc_unsat : ∀ C, ∃ a, conc_notin a C.

Ltac fresh_conc C := destruct (conc_unsat C); simpl_notin.

Inductive list_in_proc {V:Set}: list name → proc V → Prop :=
| list_in_proc_nil : ∀ P, list_in_proc nil P
| list_in_proc_rec : ∀ a L P, list_in_proc L P →
                  isin a P → list_in_proc (a::L) P.

Inductive cwf_aux : list name → conc → Prop :=
| cwf_def : ∀ L P Q, list_in_proc L P →
                cwf_aux L (conc_def P Q)
| cwf_nu : ∀ L C L', (∀ a, ¬In a L' → conc_notin_ho a C →
               cwf_aux (a::L) (C a) ) → cwf_aux L (conc_nu C).

Definition conc_wf C := cwf_aux nil C.

Fixpoint conc_parl C P : conc :=
  match C with
  | conc_def P' Q ⇒ conc_def P' (Q // P)
  | conc_nu C' ⇒ conc_nu (fun x ⇒ (conc_parl (C' x) P))
  end.

Fixpoint conc_parr P C : conc :=
  match C with
  | conc_def P' Q ⇒ conc_def P' (P // Q)
  | conc_nu C' ⇒ conc_nu (fun x ⇒ (conc_parr P (C' x)))
  end.

Definition abs_parl (F:abs) P : abs := (F // (shiftV P)).

Definition abs_parr P (F:abs) : abs := ((shiftV P) // F).

Inductive conc_new : (name → conc) → conc → Prop :=
| cnew_extr : ∀ P Q, (∀ a, notin_ho a P → isin a (P a)) →
     conc_new (fun x ⇒ conc_def (P x)(Q x)) (conc_nu (fun x ⇒ conc_def (P x) (Q x)))
| cnew_no_extr : ∀ P Q, (∀ a, notin_ho a P → notin a (P a)) →
     ∀ a, conc_new (fun x ⇒ conc_def (P x)(Q x)) (conc_def (P a) (nu Q))
| cnew_nu : ∀ (C:name→name→conc) C' L,
    (∀ a, ¬In a L → conc_notin_ho a (fun x ⇒ conc_nu (C x)) →
   conc_new (fun x ⇒ C x a)(C' a)) →
    conc_new (fun x ⇒ conc_nu (C x)) (conc_nu C')
.

Hint Constructors conc_new:hopi.


Lemma equal_f : ∀ {A B : Type} {f g : A → B},
  f = g → ∀ x, f x = g x.
Proof.
  intros; rewrite H; auto.
Qed.

Ltac fun_eq_solve := let x:= fresh "x" in
  extens; intro x; solve [ repeat match goal with
  | [ H : ?f = ?g |- _ ] ⇒ match type of f with
    | name → _ ⇒ apply equal_f with x in H; inverts× H
     end
  end ].

Ltac fun_eq_absurd := match goal with
  [ x : name |- _ ] ⇒ solve [ repeat match goal with
  | [ H : ?f = ?g |- _ ] ⇒ match type of f with
    | name → _ ⇒ apply equal_f with x in H;
      inverts× H
     end
  end ]
end.

Fixpoint appr F C : proc0 :=
  match C with
  | conc_def P Q ⇒ subst F P // Q
  | conc_nu C'⇒ nu (fun x ⇒ appr F (C' x))
  end.

Fixpoint appl C F : proc0 :=
  match C with
  | conc_def P Q ⇒ Q // subst F P
  | conc_nu C' ⇒ nu (fun x ⇒ appl (C' x) F)
  end.

Lemma notin_appr : ∀ F C a, notin a F → conc_notin a C →
   notin a (appr F C).
Proof.
  intros; induction C; simpl_notin; auto with hopi.
  constructor×. apply× @notin_bind.
  intros [|]; simpl; auto with hopi.
Qed.

Lemma notin_appl : ∀ F C a, notin a F → conc_notin a C →
   notin a (appl C F).
Proof.
  intros; induction C; simpl_notin; auto with hopi.
  constructor×. apply× @notin_bind.
  intros [|]; simpl; auto with hopi.
Qed.

Inductive ltsabs: proc0 → name → abs → Prop :=
| ltsa_inp : ∀ a P, ltsabs (a ? P) a P
| ltsa_parl : ∀ P Q a F, ltsabs P a F →
              ltsabs (P // Q) a (abs_parl F Q)
| ltsa_parr : ∀ P Q a F, ltsabs P a F →
              ltsabs (Q // P) a (abs_parr Q F)
| ltsa_new : ∀ P a F L, (∀ b, ¬In b L → a≠b → notin_ho b P →
    notin_ho b F → ltsabs (P b) a (F b)) → ltsabs (nu P) a (nu F)
.

Inductive ltsconc: proc0 → name → conc → Prop :=
| ltsc_out : ∀ a P Q, ltsconc (a !(P) Q) a (conc_def P Q)
| ltsc_parl : ∀ P Q a C, ltsconc P a C → ltsconc (P // Q) a (conc_parl C Q)
| ltsc_parr : ∀ P Q a C, ltsconc P a C → ltsconc (Q // P) a (conc_parr Q C)
| ltsc_new : ∀ P a C L, (∀ b, ¬In b L → a≠b → notin_ho b P →
    conc_notin_ho b C → ltsconc (P b) a (C b)) →
    ∀ C', conc_new C C' → ltsconc (nu P) a C'
.

Inductive ltsproc: proc0 → proc0 → Prop :=
| ltsp_parl : ∀ P Q P', ltsproc P P' → ltsproc (P // Q) (P' // Q)
| ltsp_parr : ∀ P Q P', ltsproc P P' → ltsproc (Q // P) (Q // P')
| ltsp_new : ∀ P P' L,
    (∀ a, ¬In a L → notin_ho a P → notin_ho a P' → ltsproc (P a) (P' a)) →
    ltsproc (nu P) (nu P')
| ltsp_taul : ∀ P Q a F C, ltsconc P a C →
    ltsabs Q a F → ltsproc (P // Q)(appl C F)
| ltsp_taur : ∀ P Q a F C, ltsabs Q a F →
    ltsconc P a C → ltsproc (Q // P) (appr F C)
.

Hint Constructors ltsabs ltsconc ltsproc:hopi.

Lemma lts_taul' : ∀ P P' Q a F C,
    ltsconc P a C → ltsabs Q a F →
    (appl C F) = P' → ltsproc (P // Q) P'.
Proof.
  intros. subst. eapply ltsp_taul; eassumption.
Qed.

Lemma lts_taur' : ∀ P P' Q a F C,
    ltsconc P a C → ltsabs Q a F →
    (appr F C) = P' → ltsproc (Q // P) P'.
Proof.
  intros; subst; eapply ltsp_taur; eassumption.
Qed.

Hint Resolve lts_taul' lts_taur':hopi.

Lemma nc_parl : ∀ C P a, conc_notin a (conc_parl C P) →
  notin a P ∧ conc_notin a C.
Proof.
  intros. split.
  - induction C; simpl_notin.
    fresh_list (a::nil). forwards*: H3 x.
  - induction C; simpl_notin; auto with hopi.
Qed.

Lemma nc_parl_rev : ∀ C P a, notin a P →
   conc_notin a C → conc_notin a (conc_parl C P).
Proof.
  intros; induction C; simpl_notin; auto with hopi.
Qed.

Lemma nc_parr : ∀ C P a, conc_notin a (conc_parr P C) →
  notin a P ∧ conc_notin a C.
Proof.
  intros. split.
  - induction C; simpl_notin.
    fresh_list (a::nil). forwards*: H3 x.
  - induction C; simpl_notin; auto with hopi.
Qed.

Lemma nc_parr_rev : ∀ C P a, notin a P →
   conc_notin a C → conc_notin a (conc_parr P C).
Proof.
  intros; induction C; simpl_notin; auto with hopi.
Qed.

Ltac solve_notin_rename := match goal with
  | |- notin ?a (?P ?b ?c) ⇒ let P':= (eval pattern b in (P b c))
        in change (notin a P'); eapply notin_rename; eauto
  end.

Ltac solve_notin_aux a x := repeat match goal with
    | H : ∀ z, a≠z → notin a _ |- _ ⇒
        forwards*: H x; clear H; simpl_notin; try solve [solve_notin_rename]
    | H : ∀ z, z≠a → notin a _ |- _ ⇒
        forwards*: H x; clear H; simpl_notin; try solve [solve_notin_rename]
    | H : ∀ z, a≠z → conc_notin a _ |- _ ⇒
        forwards*: H x; clear H; simpl_notin; try solve [solve_notin_rename]
    | H : ∀ z, z≠a → conc_notin a _ |- _ ⇒
        forwards*: H x; clear H; simpl_notin; try solve [solve_notin_rename]
    | H : notin a (mapV _ _) |- _ ⇒ apply @notin_mapV_rev in H;
                                     simpl_notin
    | H : notin a (bind _ _) |- _ ⇒ apply @notin_bind_rev in H;
                                     destruct H; simpl_notin
     end.

Ltac solve_notin' := repeat match goal with
  | |- notin_ho _ _ ⇒ intros_all
  | |- conc_notin_ho _ _ ⇒ intros_all
  | |- notin _ (mapV _ _) ⇒ apply× @notin_mapV
  | |- notin _ (appl _ _) ⇒ apply× notin_appl
  | |- notin _ (appr _ _) ⇒ apply× notin_appr
  | |- notin _ (abs_parl _ _) ⇒ unfold abs_parl
  | |- notin _ (abs_parr _ _) ⇒ unfold abs_parr
  | |- conc_notin _ (conc_parl _ _) ⇒ apply× nc_parl_rev
  | |- conc_notin _ (conc_parr _ _) ⇒ apply× nc_parr_rev
  | |- notin _ ?P ⇒ head_constructor P; constructor
  | |- conc_notin _ ?C ⇒ head_constructor C; constructor
  end; unfold notin_ho in *; unfold conc_notin_ho in ×.

Lemma neq_symmetry : ∀ (a b:name), a≠b → b≠a.
Proof.
  intros; auto.
Qed.

Ltac symmetry_hyp a := repeat match goal with
  [ H : ?x ≠ a |- _ ] ⇒ apply neq_symmetry in H
  end.

Ltac solve_notin := solve_notin';
  match goal with | |- notin ?a ?P ⇒ symmetry_hyp a;
    repeat match goal with
    | H : a ≠ ?x |- _ ⇒ try solve [solve_notin_aux a x];
        apply neq_symmetry in H
    end
    | |- conc_notin ?a ?C ⇒ symmetry_hyp a;
    repeat match goal with
    | H : a ≠ ?x |- _ ⇒ try solve [solve_notin_aux a x];
        apply neq_symmetry in H
    end
  end.

Hint Extern 1 (notin_ho ?a ?P) ⇒ solve_notin:hopi.
Hint Extern 1 (notin ?a ?P) ⇒ solve_notin:hopi.
Hint Extern 1 (conc_notin _ _) ⇒ solve_notin:hopi.
Hint Extern 1 (conc_notin_ho _ _) ⇒ solve_notin:hopi.


Lemma unsat_lc: ∀ (L:list name) C, ∃ a,
                        ¬In a L ∧ conc_notin a C.
Proof.
  intros. fresh_conc (conc_parl C (listproc L PO)).
  ∃ x. forwards*: nc_parl. forwards*: @listproc_in.
Qed.

Ltac fresh_lc L C := destruct (unsat_lc L C); simpl_notin.

Inductive sizec : conc → nat → Prop :=
| szc_def : ∀ P Q, sizec (conc_def P Q) 0
| szc_nu : ∀ C n, (∀ a, sizec (C a) n) →
           sizec (conc_nu C) (1+n).

Hint Constructors sizec:hopi.

Lemma sizec_rename : ∀ n C a, conc_notin_ho a C →
  sizec (C a) n → ∀ b, sizec (C b) n.
Proof.
  induction n; intros; inverts H0.
  - conc_exp_ext a.
  - ho_conc_exp a C0. conc_change_ext.
    constructor. intros.
    fresh_lc (a0::a::nil) (conc_nu (C1 b)).
    apply IHn with x; auto.
    change (sizec ((fun b ⇒ C1 b x) b) n).
    apply IHn with a; auto.
    intros_all. forwards*: H0 b0. simpl_notin.
Qed.

Lemma exists_szc : ∀ C, ∃ n, sizec C n.
Proof.
  induction C.
  ∃ 0; auto with hopi.
  fresh_conc (conc_nu c).
  destruct (H x) as [n].
  ∃ (1+n). constructor. intros.
  eapply sizec_rename; eauto.
Qed.

Lemma conc_notin_rename' : ∀ n (C:conc), (sizec C n) →
      ∀ C' c, (conc_notin_ho c C') → C = (C' c) →
      ∀ a b, (conc_notin a (C' b)) → (conc_notin_ho a C').
Proof.
  intro n.
  induction n; introv Hs Hc Hc' Hnotin;
  inverts Hs; intros_all.
  - conc_exp_ext c.
    constructor; apply notin_rename with b; auto.
  - ho_conc_exp c C0. conc_change_ext. rename C1 into C''.
    constructor; intros z Haz.
    fresh_lc (z::a::c::nil) (conc_nu (C'' b0)). rename x into c'.
    assert (∀ x, x≠c → sizec (C'' b0 x) n).
    { intros; change (sizec ((fun c ⇒ C'' c x) b0) n).
      eapply sizec_rename; eauto. intros_all.
      forwards*: Hc b1. simpl_notin. }
    assert (conc_notin a (C'' b0 c')).
    { change (conc_notin a ((fun b0 ⇒ C'' b0 c') b0)).
      eapply IHn; eauto. intros_all.
      forwards*: Hc b1. simpl_notin. }
    clear H1. eapply IHn; eauto.
Qed.

Lemma conc_notin_rename : ∀ (C:name→conc) a b,
   conc_notin a (C b) → ∀ c, a≠c → conc_notin a (C c).
Proof.
  intros. fresh_conc (conc_nu C).
  destruct (exists_szc (conc_nu C)) as [n]. inverts H1.
  eapply conc_notin_rename'; eauto.
Qed.

Ltac solve_notin_rename ::= match goal with
  | |- notin ?a (?P ?b ?c) ⇒ let P':= (eval pattern b in (P b c))
        in change (notin a P'); eapply notin_rename; eauto
  | |- conc_notin ?a (?C ?b ?c) ⇒ let C':= (eval pattern b in (C b c))
        in change (conc_notin a C'); eapply conc_notin_rename; eauto
  end.

Lemma unsat_proc_of_conc : ∀ C, ∃ (P:proc0),
  ∀ a, notin a P → conc_notin a C.
Proof.
  induction C.
  - fresh_proc (p//p0). ∃ (x!(p) p0).
    intros_all. inverts H. apply× nc_def.
  - fresh_conc (conc_nu c).     forwards× [P]: H x. exp x P.
    ∃ (nu P0).
    intros. simpl_notin. constructor. intros b Hab.
    destruct (dec_name x a); subst; auto.
    apply conc_notin_rename with x; auto.
Qed.

Lemma list_of_conc : ∀ C, ∃ L,
  ∀ a, ¬In a L → conc_notin a C.
Proof.
  intros. destruct (unsat_proc_of_conc C) as [P].
  destruct (list_of_proc P). eexists; eauto.
Qed.

Ltac fn P := let L := fresh "L" in
  match type of P with
  | proc _ ⇒ destruct (list_of_proc P) as [L]
  | conc ⇒ destruct (list_of_conc P) as [L]
  end.

Lemma unsat_pc {V:Set}: ∀ (P:proc V) C, ∃ a,
                        notin a P ∧ conc_notin a C.
Proof.
  intros. fn P. fn C. fresh_list (L++L0).
  eexists; eauto.
Qed.

Lemma unsat_lpc {V:Set}: ∀ (L:list name) (P:proc V) C, ∃ a,
                        ¬In a L ∧ notin a P ∧ conc_notin a C.
Proof.
  intros. fn P. fn C. fresh_list (L++L0++L1).
  eexists; eauto.
Qed.

Ltac fresh_pc P C := destruct (unsat_pc P C); simpl_notin.
Ltac fresh_lpc L P C := destruct (unsat_lpc L P C); simpl_notin.

Lemma conc_unused_arg : ∀ (C:name → conc) a,
  conc_notin a (C a) → ∀ a b, C a = C b.
Proof.
  intros C a Hnotin.
  assert (conc_notin_ho a C).
  { intros z Hz. apply conc_notin_rename with a; auto. }
  induction (C a) eqn:HH; symmetry in HH; conc_change_ext.
Qed.

Lemma conc_notin_arg: ∀ (C:name → conc) a,
  conc_notin a (C a) → ∀ b, conc_notin_ho b C → conc_notin b (C b).
Proof.
  intros. destruct (dec_name a b); subst; auto.
  rewrite (conc_unused_arg C a H b a). forwards*: H0 a.
Qed.

Lemma two_unused_args : ∀ C a, conc_notin_ho a (fun x ⇒ C x a)
  → conc_notin_ho a (fun x ⇒ C a x) → conc_notin a (C a a).
Proof.
  intros. fresh_lc (a::nil) (conc_nu (fun x ⇒ (conc_nu (fun y ⇒ C x y)))).
  forwards*: H0 x.
  fresh_list (a::x::nil). rename x0 into b.
  change (conc_notin a ((fun a ⇒ C a x) a)) in H2.
  forwards: (conc_unused_arg _ a H2) a b.
  auto_conc_ext.
  rewrite H7 in ×. apply× H.
Qed.


Lemma cnew_notin : ∀ C C', conc_new C C' →
   ∀ a, conc_notin_ho a C → conc_notin a C'.
Proof.
  introv H. induction H; intros.
  - constructor; intros.
    forwards*: H0 b.
  - constructor; intros.
    destruct (dec_name a a0); subst.
    apply H. intros_all. forwards*: H0 b. simpl_notin.
    apply notin_rename with a0; auto. apply H.
    intros_all. forwards*: H0 b. simpl_notin.
    constructor; intros. forwards*: H0 z. simpl_notin.
  - constructor; intros.
    fresh_lc (a::b::L) (conc_nu (fun x ⇒ conc_nu (fun y ⇒ C x y))).
    apply conc_notin_rename with x; auto.
    eapply H0; eauto; auto with hopi.
Qed.

Lemma cnew_notin_rev : ∀ C C', conc_new C C' →
   ∀ a, conc_notin a C' → conc_notin_ho a C.
Proof.
  introv H. induction H; intros.
  - inverts H0. constructor; intros;
    forwards*: H3 b; simpl_notin.
  - simpl_notin. constructor; intros;
    eapply notin_rename; eauto.
  - inverts H1. constructor; intros.
    fresh_lc (a::b::L) (conc_nu (fun x ⇒ conc_nu (fun y ⇒ C x y))).
    forwards*: H0 x. forwards*: H5 b0.
    apply conc_notin_rename with x; auto.
Qed.

Lemma cnew_rename : ∀ C C' b, conc_notin_ho b (fun x ⇒ conc_nu (C x)) →
  conc_notin_ho b C' → conc_new (C b)(C' b) → ∀ c,
  conc_new (C c)(C' c).
Proof.
  introv HbC HbC' H. remember (C b) as Cb.
  remember (C' b) as C'b. gen C C' b. induction H; intros.
  - ho_exp b P. ho_exp b Q. conc_change_ext.
    assert (conc_nu (fun x : name ⇒ conc_def (P0 b x) (Q0 b x)) =
      conc_nu (C b)) by (rewrite× HeqCb).
    change ((fun b ⇒ (conc_nu (fun x ⇒ conc_def (P0 b x)(Q0 b x)))) b = (fun b ⇒ conc_nu (C b)) b) in H2.
    auto_conc_ext.
    apply equal_f with c in H3. inverts H3. constructor.
    intros.
    destruct (dec_name a b); subst.
    +
      fresh_lp (c::b::nil)((nu (P0 b)) // nu (P0 c)).
      destruct (isin_notin_dec b (P0 c b)); auto.
      forwards*: @notin_arg H5 x.
      change (notin x ((fun c ⇒ P0 c x) c)) in H9.
      forwards*: @notin_rename (fun c : name ⇒ P0 c x) x c H9.
      forwards*: H x.
      exfalso. forwards*: @sep x x.
    +
      change (isin a ((fun c ⇒ P0 c a) c)).
      apply isin_rename with b; auto. apply H. intros_all.
      forwards*: H2 b0. auto with hopi.
  - ho_exp b P. ho_exp b Q. conc_change_ext.
    { constructor×.
      destruct (dec_name a b); subst; auto with hopi.
      fresh_lp (c::b0::nil)((nu (P0 b0)) // nu (P0 b)).
      apply notin_arg with x; auto with hopi. }
    assert (conc_nu (fun x : name ⇒ conc_def (P0 b x) (Q0 b x)) =
       conc_nu (C b)) by (rewrite× HeqCb).
    change ((fun b ⇒ (conc_nu (fun x ⇒ conc_def (P0 b x)(Q0 b x)))) b = (fun b ⇒ conc_nu (C b)) b) in H2.
    auto_conc_ext.
    apply equal_f with c in H3. inverts H3. constructor.
    intros. fresh_lp (c::b::nil)((nu (P0 b)) // nu (P0 c)).
    apply notin_arg with x; auto with hopi. solve_notin_rename.
  - ho_conc_exp b C'. conc_change_ext.
    destruct (conc_ho_ho_beta_exp b C) as [C'' []]; subst.
    assert (conc_nu (fun x : name ⇒ conc_nu (C'' b x)) =
       conc_nu (C0 b)) by (rewrite× HeqCb).
    change ((fun b ⇒ (conc_nu (fun x ⇒ conc_nu (C'' b x)))) b = (fun b ⇒ conc_nu (C0 b)) b) in H3.
    auto_conc_ext. apply equal_f with c in H4. inverts H4.
    apply cnew_nu with (b::c::L). intros. simpl_notin.
    change ((conc_new ((fun c ⇒ fun x ⇒ C'' c x a) c)((fun c ⇒ (C'1 c a)) c))).
    eapply H0; eauto; auto with hopi.
    + intros_all. constructor; intros.
      forwards*: H4 b0. inverts H10. forwards*: H13 b1.
      change (conc_notin a ((fun b ⇒ C'' b b0 b1) b)).
      apply conc_notin_rename with c; auto.
    + intros_all. constructor; intros. forwards*: H2 b1.
      simpl_notin. forwards*: H13 b0. simpl_notin.
Qed.

Lemma dec_cnew {V:Set} : ∀ (P:name→proc V),
  (∀ a, notin_ho a P → isin a (P a)) ∨
  (∀ a, notin_ho a P → notin a (P a)).
Proof.
  intros. fresh_proc (nu P). destruct (isin_notin_dec x (P x)).
  - left; intros. apply isin_arg with x; auto.
  - right; intros. apply notin_arg with x; auto.
Qed.

Lemma exists_cnew' : ∀ n C'', sizec C'' n →
   ∀ a C, conc_notin_ho a C → C'' = C a →
   ∃ C', conc_new C C'.
Proof.
  induction n; intros; inverts H.
  - conc_exp_ext a. destruct (dec_cnew P0).
    + ∃ (conc_nu (fun x ⇒ conc_def (P0 x)(Q0 x))); auto with hopi.
    + ∃ (conc_def (P0 a)(nu Q0)); auto with hopi.
  - ho_conc_exp a C0. conc_change_ext.
    fresh_lc (a::nil) (conc_nu (fun x⇒ (conc_nu (fun y ⇒ C1 x y)))).
    forwards× [C']: IHn (fun y ⇒ C1 y x).
      { intros_all. forwards*: H0 b. simpl_notin. }
    conc_exp x C'. ∃ (conc_nu C'0).
    apply cnew_nu with (a::x::nil). intros.
    change (conc_new ((fun a0 ⇒ fun x0 ⇒ C1 x0 a0) a0) (C'0 a0)).
    apply cnew_rename with x; auto.
    intros_all. constructor; intros. forwards*: H6 b0. simpl_notin.
Qed.

Lemma exists_cnew : ∀ C, ∃ C', conc_new C C'.
Proof.
  intros. fresh_conc (conc_nu C). destruct (exists_szc (C x)).
  eapply exists_cnew'; eauto.
Qed.

Lemma cnew_unique : ∀ C C1 C2, conc_new C C1 → conc_new C C2 →
  C1 = C2.
Proof.
  intros. gen C2. induction H; intros.
  + inverts H0; try (assert (P = P0) by fun_eq_solve;
    assert (Q = Q0) by fun_eq_solve; subst); auto.
    fresh_proc (nu P0). forwards*: H2 x.
    forwards*: H x. exfalso; forwards*: @sep x x.
    fresh_list (@nil name). fun_eq_absurd.
  + inverts H0; try fun_eq_absurd; try (
    assert (P = P0) by fun_eq_solve;
    assert (Q = Q0) by fun_eq_solve; subst); auto.
    fresh_proc (nu P0). forwards*: H2 x.
    forwards*: H x. exfalso; forwards*: @sep x x.
    fequal. fresh_proc (nu P0). forwards*: H2 x.
    eapply unused_arg; eauto.
  + inverts H1; try fun_eq_absurd.
    fresh_list (@nil name). fun_eq_absurd.
    assert (C=C0). fun_eq_solve. subst. clear H2.
    fn (conc_nu C'0). fn(conc_nu C').
    fresh_lc (L++L0++L1++L2)(conc_nu (fun x ⇒ conc_nu (C0 x))).
    forwards*: H1 x. simpl_notin. clears L1.
    forwards*: H3 x. forwards*: H2. forwards*: H0 H1.
    auto_conc_ext.
Qed.


Lemma cwf_parl : ∀ L C P, cwf_aux L C →
                     cwf_aux L (conc_parl C P).
Proof.
  intros; gen L; induction C; intros.
  - simpl. inverts H. constructor. auto.
  - inverts H0. simpl. econstructor.
    intros. apply× H. apply H3. eassumption. intros_all.
    forwards*: H1 b. forwards*: nc_parl.
Qed.

Lemma cwf_parr : ∀ L C P, cwf_aux L C →
                     cwf_aux L (conc_parr P C).
Proof.
  intros; gen L; induction C; intros.
  - simpl. inverts H. constructor. auto.
  - inverts H0. simpl. econstructor; intros.
    apply× H. apply H3. eassumption. intros_all.
    forwards*: H1 b. forwards*: nc_parr.
Qed.

Lemma list_in_proc_rename {V:Set}: ∀ L (P:name→proc V) a,
  ¬In a L → list_in_proc L (P a) → ∀ b, list_in_proc L (P b).
Proof.
  induction L; intros; constructor; inverts H0; simpl_notin.
  - eapply IHL; eauto.
  - eapply isin_rename; eauto.
Qed.

Lemma cwf_aux_rename: ∀ L C a, ¬ In a L →
    conc_notin_ho a C → cwf_aux L (C a) →
    ∀ b, cwf_aux L (C b).
Proof.
  intros. remember (C a) as Ca. gen C a b.
  induction H1; intros.
  - conc_exp_ext a. constructor.
    apply list_in_proc_rename with a; auto.
  - ho_conc_exp a C. conc_change_ext.
    apply cwf_nu with (a::b::(L++L')).
    intros; simpl_notin.
    change (cwf_aux (a0 :: L) ((fun x ⇒ C1 x a0) b)).
    eapply H0; eauto; auto with hopi.
    intuition.
Qed.

Lemma cwf_new : ∀ C L L',
  (∀ b, ¬In b L' → conc_notin_ho b C → cwf_aux L (C b)) →
  ∀ C', conc_new C C' → cwf_aux L C'.
Proof.
  intros. gen L L'. induction H0; intros.
  - apply cwf_nu with L'; intros.
    constructor. constructor.
    forwards*: H0 a. simpl_notin. inverts× H3.
    apply H; intros_all. forwards*: H2 b.
    simpl_notin.
  - constructor.
    fresh_lc (a::(L'++L))(conc_nu (fun x ⇒ conc_def (P x)(Q x))).
    forwards*: H0 x. inverts H2.
    eapply list_in_proc_rename; eauto.
  - fresh_lc (L0++L++L') (conc_nu (fun x : name ⇒ conc_nu (C x))).
    forwards*: H1 x. forwards*: H x. inverts H3.
    apply cwf_nu with (x::L++L0++L'++L'0). intros. simpl_notin.
    apply cnew_notin_rev with (fun x0 : name ⇒ C x0 x) (C' x) a in H6; auto.
    simpl_notin. eapply H0; eauto; auto with hopi.
    intros_all. constructor; intros.
    forwards*: H6 b. eapply conc_notin_rename; eauto.
    intros. forwards*: H10 a.
    intros_all. forwards*: H6 x. eapply conc_notin_rename; eauto.
    change (cwf_aux (a :: L0)((fun x ⇒ C x a) b)).
    apply cwf_aux_rename with x; auto with hopi. simpl_notin.
    Unshelve. exact (@nil name).
Qed.

Lemma lts_conc_wf : ∀ P a C, ltsconc P a C → conc_wf C.
Proof.
  intros.
  induction H; try solve [inverts HC]; unfold conc_wf.
  - constructor. constructor.
  - apply cwf_parl. auto.
  - apply cwf_parr. auto.
  - fn (nu P). apply cwf_new with C (a::L++L0); eauto; intros.
    simpl_notin. forwards*: H2. simpl_notin. apply× H0.
Qed.


Lemma cwf_include : ∀ L C, cwf_aux L C →
  ∀ L', incl L' L → cwf_aux L' C.
Proof.
  introv H; induction H; intros.
  + constructor. induction L'; auto. constructor.
    assert (In a L). apply H0. apply in_eq.
    assert (incl L' L). intros_all. apply H0.
    apply× @in_cons.
    constructor×. clears L'.
    induction L; inverts× H; inverts× H1.
  + apply cwf_nu with L'; intros.
    apply× H0. intros_all. default_simp.
Qed.

Lemma list_in_proc_change {V:Set}: ∀ L' L (P:name→proc V) a,
  notin_ho a P → ¬ In a L → ¬ In a L' →
  list_in_proc (L' ++ a :: L)(P a) → ∀ b, list_in_proc (L' ++ b :: L) (P b).
Proof.
  induction L'; intros.
  - rewrite app_nil_l in ×. inverts H2. constructor.
    + apply list_in_proc_rename with a; auto.
    + apply isin_arg with a; auto.
  - rewrite <- app_comm_cons in ×. inverts H2.
    simpl_notin. constructor.
    + eapply IHL'; eauto.
    + apply isin_rename with a0; auto.
Qed.

Lemma cwf_aux_change : ∀ C L L' a,
  conc_notin_ho a C → ¬ In a L → ¬ In a L' →
  cwf_aux (L' ++ a :: L) (C a) →
  ∀ b, cwf_aux (L' ++ b :: L)(C b).
Proof.
  intros. remember (C a) as Ca.
  remember (L'++a ::L) as La. gen b C L' L.
  induction H2; intros.
  + all_exp a. conc_change_ext. constructor.
    apply list_in_proc_change with a; auto.
  + ho_conc_exp a C. conc_change_ext.
    apply cwf_nu with (a::b::(L'0++L0++L')); intros. simpl_notin.
    rewrite app_comm_cons.
    change (cwf_aux ((a0 :: L'0) ++ b :: L0) ((fun b ⇒ C1 b a0) b)).
    eapply H0; eauto; auto with hopi.
    simpl_notin.
Qed.


Inductive subst_name : name → name → name → name → Prop :=
| sn_eq : ∀ b c, subst_name b c b c
| sn_not_eq : ∀ b c a, a≠b → subst_name b c a a.

Hint Constructors subst_name:hopi.

Lemma exists_sname : ∀ a b c, ∃ d,
 subst_name b c a d.
Proof.
  intros. destruct (dec_name a b); subst; eexists; eauto with hopi.
Qed.

Lemma ltsabs_rename : ∀ P a F,
    ∀ b, notin_ho b P → notin_ho b F → ltsabs (P b) a (F b) →
    ∀ c d, subst_name b c a d → ltsabs (P c) d (F c).
Proof.
  intros. remember (P b) as Pb.
  remember (F b) as Fb. gen c d b P F. induction H1; intros.
  - destruct (dec_name a b); subst; exp_ext b;
      inverts H2; try solve [exfalso; auto]; auto with hopi.
  - all_exp b. move HeqPb after H5. change_ext.
    change ((fun b ⇒ abs_parl (F1 b) (Q0 b)) b = F0 b) in HeqFb.
    auto_proc_ext. apply ltsa_parl. eapply IHltsabs; eauto.
  - all_exp b. move HeqPb after H5. change_ext.
    change ((fun b ⇒ abs_parr (Q0 b)(F1 b)) b = F0 b) in HeqFb.
    auto_proc_ext. apply ltsa_parr. eapply IHltsabs; eauto.
  - ho_exp b P. ho_exp b F. repeat change_ext.
    apply ltsa_new with (a::b::L). intros; simpl_notin.
    change (ltsabs ((fun c ⇒ P1 c b0) c) d ((fun c ⇒ F1 c b0) c)).
    eapply H0; eauto; auto with hopi.
Qed.

Lemma ltsconc_rename : ∀ P a C,
    ∀ b, notin_ho b P → conc_notin_ho b C → ltsconc (P b) a (C b) →
    ∀ c d, subst_name b c a d → ltsconc (P c) d (C c).
Proof.
  intros. remember (P b) as Pb. remember (C b) as Cb.
  gen P C b c d. induction H1; intros.
  - destruct (dec_name a b); conc_exp_ext b;
    change_ext; inverts H2; try solve [exfalso; auto]; auto with hopi.
  - all_conc_exp b. move HeqPb after H4. change_ext.
    change ((fun b ⇒ conc_parl (C1 b) (Q0 b)) b = C0 b) in HeqCb.
    auto_conc_ext. apply ltsc_parl. eapply IHltsconc; eauto.
  - all_conc_exp b. move HeqPb after H4. change_ext.
    change ((fun b ⇒ conc_parr (Q0 b)(C1 b)) b = C0 b) in HeqCb.
    auto_conc_ext. apply ltsc_parr. eapply IHltsconc; eauto.
  - ho_exp b P. change_ext. ho_conc_exp b C.
    apply ltsc_new with (C1 c) (b::c::d::a::L).
    2:{ eapply cnew_rename; eauto. }
    intros; simpl_notin.
    change (ltsconc ((fun c ⇒ P1 c b0) c) d ((fun c ⇒ C1 c b0) c)).
    eapply H0; eauto; auto with hopi.
Qed.

Lemma ltsproc_rename : ∀ P P',
    ∀ b, notin_ho b P → notin_ho b P' → ltsproc (P b) (P' b) →
    ∀ c, ltsproc (P c) (P' c).
Proof.
  intros. remember (P b) as Pb. remember (P' b) as P'b.
  gen P P' b c. induction H1; intros.
  - exp_ext b. eapply ltsp_parl; eauto.
  - exp_ext b. eapply ltsp_parr; eauto.
  - ho_exp b P. ho_exp b P'. repeat change_ext.
    apply ltsp_new with (b::c::L). intros; simpl_notin.
    change (ltsproc ((fun c ⇒ P1 c a) c)((fun c ⇒ P'1 c a) c)).
    eapply H0; eauto; auto with hopi.
  - all_conc_exp b. move HeqPb after H5. change_ext.
    change ((fun b ⇒ appl (C0 b)(F0 b)) b = P' b) in HeqP'b.
    auto_proc_ext. destruct (exists_sname a b c) as [d].
    eapply lts_taul'; eauto.
      forwards*: ltsconc_rename H.
      forwards*: ltsabs_rename H0.
  - all_conc_exp b. move HeqPb after H5. change_ext.
    change ((fun b ⇒ appr (F0 b)(C0 b)) b = P' b) in HeqP'b.
    auto_proc_ext. destruct (exists_sname a b c) as [d].
    eapply lts_taur'; eauto.
      forwards*: ltsconc_rename H0.
      forwards*: ltsabs_rename H.
Qed.


Lemma ltsabs_notin : ∀ P a F, ltsabs P a F →
  ∀ b, notin b P → notin b F.
Proof.
  introv H. induction H; intros; simpl_notin.
  - unfold abs_parl. constructor×. apply× @notin_mapV.
  - unfold abs_parr. constructor×. apply× @notin_mapV.
  - constructor. intros.
    fresh_lp (z::a::b::L) ((nu F)//shiftV(nu P)).
    apply notin_rename with x; auto. apply× H0. auto with hopi.
Qed.

Lemma ltsabs_notin_ho : ∀ P a F,
    ∀ b, notin_ho b P → notin_ho b F → ltsabs (P b) a (F b) →
    ∀ c, (notin_ho c P → notin_ho c F).
Proof.
  intros_all. destruct (exists_sname a b b0) as [d].
  forwards*: ltsabs_rename H1. eapply ltsabs_notin; eauto.
Qed.

Lemma ltsabs_unused_arg : ∀ P,
  (∀ a, notin_ho a P → notin a (P a)) →
  ∀ b F c, notin_ho b P → notin_ho b F →
  ltsabs (P b) c (F b) → ∀ a, notin_ho a F → notin a (F a).
Proof.
  intros. fresh_proc (nu P).
  apply notin_arg with x; auto.
  destruct (exists_sname c b x) as [d].
  forwards*: ltsabs_rename H2.
  eapply ltsabs_notin; eauto.
Qed.

Lemma ltsabs_notin_label : ∀ P a F, ltsabs P a F →
  ∀ b, notin b P → a≠b.
Proof.
  introv H. induction H; intros; simpl_notin.
  fresh_lp (a::b::L) ((nu F)//shiftV(nu P)).
  apply H0 with x; auto with hopi.
Qed.

Lemma ltsconc_notin : ∀ P a C, ltsconc P a C →
  ∀ b, notin b P → conc_notin b C.
Proof.
  introv H. induction H; intros; simpl_notin.
  - constructor×.
  - apply× nc_parl_rev.
  - apply× nc_parr_rev.
  - apply cnew_notin with C; auto.
    intros_all. fresh_lpc (b0::a::b::L) (nu P) (conc_nu C).
    apply conc_notin_rename with x; auto.
Qed.

Lemma ltsconc_notin_ho : ∀ P a C,
    ∀ b, notin_ho b P → conc_notin_ho b C → ltsconc (P b) a (C b) →
    ∀ c, (notin_ho c P → conc_notin_ho c C).
Proof.
  intros_all. destruct (exists_sname a b b0) as [d].
  forwards*: ltsconc_rename H1. eapply ltsconc_notin; eauto.
Qed.

Lemma ltsconc_unused_arg : ∀ P,
  (∀ a, notin_ho a P → notin a (P a)) →
  ∀ b C c, notin_ho b P → conc_notin_ho b C →
  ltsconc (P b) c (C b) → ∀ a, conc_notin_ho a C → conc_notin a (C a).
Proof.
  intros. fresh_proc (nu P).
  apply conc_notin_arg with x; auto.
  destruct (exists_sname c b x) as [d].
  forwards*: ltsconc_rename H2.
  eapply ltsconc_notin; eauto.
Qed.

Lemma ltsconc_notin_label : ∀ P a C, ltsconc P a C →
  ∀ b, notin b P → a≠b.
Proof.
  introv H. induction H; intros; simpl_notin.
  fresh_lpc (a::b::L) (nu P) (conc_nu C).
  apply H0 with x; auto.
Qed.

Lemma ltsproc_notin : ∀ P P', ltsproc P P' →
  ∀ b, notin b P → notin b P'.
Proof.
  introv H. induction H; intros; simpl_notin; auto with hopi.
  - constructor. intros.
    fresh_lp (z::b::L) ((nu P)// nu P').
    apply notin_rename with x; auto.
  - apply notin_appl. apply× ltsabs_notin.
    apply× ltsconc_notin.
  - apply notin_appr. apply× ltsabs_notin.
    apply× ltsconc_notin.
Qed.

Lemma ltsproc_notin_ho : ∀ P P',
    ∀ b, notin_ho b P → notin_ho b P' → ltsproc (P b)(P' b) →
    ∀ c, (notin_ho c P → notin_ho c P').
Proof.
  intros_all.
  forwards*: ltsproc_rename H1. eapply ltsproc_notin; eauto.
Qed.

Lemma ltsproc_unused_arg : ∀ P,
  (∀ a, notin_ho a P → notin a (P a)) →
  ∀ P' b, notin_ho b P → notin_ho b P' →
  ltsproc (P b)(P' b) → ∀ a, notin_ho a P' → notin a (P' a).
Proof.
  intros. fresh_proc (nu P).
  apply notin_arg with x; auto.
  forwards*: ltsproc_rename H2.
  eapply ltsproc_notin; eauto.
Qed.