Require Export Bisimulation.

Inductive struct_congr {V : Set} : binary (proc V) :=
| sc_par_assoc : ∀ P Q R, struct_congr (P // (Q // R)) ((P // Q) // R)
| sc_par_assoc_rev : ∀ P Q R, struct_congr ((P // Q) // R) (P // (Q // R))
| sc_par_comm : ∀ P Q, struct_congr (P // Q) (Q // P)
| sc_par_nil : ∀ P, struct_congr (P // PO) P
| sc_par_nil_conv : ∀ P, struct_congr P (P // PO)
| sc_scope: ∀ P Q, struct_congr (nu (P // (shiftN 1 Q))) ((nu P) // Q)
| sc_scope_rev: ∀ P Q, struct_congr ((nu P) // Q) (nu (P // (shiftN 1 Q)))
| sc_nu_nil : struct_congr (nu PO) PO
| sc_nu_nil_rev : struct_congr PO (nu PO)
| sc_nu_nu : ∀ P, struct_congr (nu nu P) (nu nu (mapN (permut 1) P))
| sc_nu_nu_rev : ∀ P, struct_congr (nu nu (mapN (permut 1) P)) (nu nu P)
| sc_nil : struct_congr PO PO
| sc_var : ∀ x, struct_congr (pr_var x) (pr_var x)
| sc_par : ∀ P Q P' Q', struct_congr P Q → struct_congr P' Q'
                                              → struct_congr (P // P') (Q // Q')
| sc_inp : ∀ a P Q, @struct_congr (incV V) P Q → struct_congr (a? P) (a? Q)
| sc_out : ∀ a P Q P' Q', struct_congr P Q → struct_congr P' Q'
                                                 → struct_congr (a!(P) P') (a!(Q) Q')
| sc_nu : ∀ P Q, struct_congr P Q → struct_congr (nu P) (nu Q)
| sc_trans : ∀ P Q R, struct_congr P Q → struct_congr Q R → struct_congr P R
.

Hint Constructors struct_congr:sc.

Lemma sc_refl {V : Set} : ∀ P, @struct_congr V P P.
Proof.
  induction P; auto with sc.
Qed.

Lemma sc_symmetric {V : Set} : ∀ (P Q:proc V),
  struct_congr P Q → struct_congr Q P.
Proof.
  intros P Q H. induction H; eauto with sc.
Qed.

Lemma sc_genNu {V:Set}: ∀ k (P Q:proc V), struct_congr P Q → struct_congr (genNu k P) (genNu k Q).
Proof.
  induction k; simpl; auto with sc.
Qed.

Hint Resolve sc_refl sc_symmetric sc_genNu:sc.

Lemma sc_mapV: ∀ (V W:Set) P Q (f:V → W), @struct_congr V P Q
   → @struct_congr W (mapV f P) (mapV f Q).
Proof.
  intros. gen W.
  induction H;
  simpl; auto with sc; try (intros; rewrite mapV_mapN; auto with sc).
   eauto with sc.
Qed.

Lemma sc_mapN: ∀ (V:Set) (P:proc V) Q f, injective f → struct_congr P Q
   → struct_congr (mapN f P) (mapN f Q).
Proof.
  intros. gen f. induction H0; simpl; auto with sc; intros.
  - replace (mapN (liftN f 1) (mapN (fun x ⇒ S x) Q)) with (mapN S (mapN f Q));
      auto with sc.
    repeat (rewrite mapN_mapN). fequals. extens. simpl_liftN. auto with arith.
  - replace (mapN (liftN f 1) (mapN (fun x ⇒ S x) Q)) with (mapN S (mapN f Q));
      auto with sc.
    repeat (rewrite mapN_mapN). fequals. extens. simpl_liftN. auto with arith.
  - replace (mapN (liftN (liftN f 1) 1) (mapN (permut 1) P)) with
                    (mapN (permut 1) (mapN (liftN (liftN f 1) 1) P)); auto with sc.
    repeat (rewrite mapN_mapN). fequals. extens. simpl_liftN; simpl_permut.
  - replace (mapN (liftN (liftN f 1) 1) (mapN (permut 1) P)) with
                    (mapN (permut 1) (mapN (liftN (liftN f 1) 1) P)); auto with sc.
    repeat (rewrite mapN_mapN). fequals. extens. simpl_liftN; simpl_permut.
  - apply sc_nu. apply IHstruct_congr. auto using liftN_preserves_injectivity.
  - eauto with sc.
Qed.

Lemma sc_liftV: ∀ (V W:Set) (f:V → proc W) (g:V → proc W),
   (∀ x, @struct_congr W (f x) (g x)) →
   (∀ x, @struct_congr (incV W) (liftV f x) (liftV g x)).
Proof.
  intros.
  destruct x; simpl; auto with sc.
  apply sc_mapV. auto with sc.
Qed.

Lemma sc_bind': ∀ (V W:Set) (P : proc V) (f:V → proc W) (g:V → proc W),
   (∀ x, @struct_congr W (f x) (g x)) →
   @struct_congr W (bind f P) (bind g P).
Proof.
  intros. gen W.
  induction P; intros; simpl; auto with sc.
  - apply sc_inp. apply IHP. intros. apply× sc_liftV.
  - apply sc_nu. apply IHP. intros. apply× sc_mapN.
Qed.

Hint Resolve sc_bind' sc_liftV sc_mapN sc_mapV:sc.

Lemma sc_bind: ∀ (V W:Set) (P Q : proc V) (f:V → proc W) (g:V → proc W), @struct_congr V P Q →
   (∀ x, @struct_congr W (f x) (g x)) →
   @struct_congr W (bind f P) (bind g Q).
Proof.
  intros. gen W. induction H; simpl; try solve [auto with sc]; intros.
  - apply sc_trans with (bind f P // (bind f Q // bind g R)); auto with sc.
    apply sc_trans with (bind f P // (bind g Q // bind g R)); eauto with sc.
  - apply sc_trans with (bind f P // bind f Q // bind g R); auto with sc.
    apply sc_trans with (bind f P // bind g Q // bind g R); eauto with sc.
  - eauto with sc.
  - eauto with sc.
  - eauto with sc.
  - replace (bind (fun x : V ⇒ mapN (fun x0 ⇒ S x0) (f x))
        (mapN (fun x ⇒ S x) Q)) with (shiftN 1 (bind f Q)).
    apply sc_trans with (((nu bind (fun x : V ⇒ shiftN 1 (f x)) P) // bind f Q));
      auto using (shiftN_injective 1) with sc.
    rewrite bind_mapN. auto.
  - replace (bind (fun x : V ⇒ mapN (fun x0 ⇒ S x0) (g x))
        (mapN (fun x ⇒ S x) Q)) with (shiftN 1 (bind g Q))
        by (rewrite bind_mapN;auto).
    apply sc_trans with (((nu bind (fun x : V ⇒ mapN (fun x0 ⇒ S x0)(g x)) P) // bind g Q));
      auto using (shiftN_injective 1) with sc.
  - apply sc_trans with (nu nu bind (fun x : V ⇒ shiftN 1 (shiftN 1 (g x))) P).
    × repeat (apply sc_nu). auto using (shiftN_injective 1) with sc.
    × asserts_rewrite ((fun x ⇒ mapN (fun x0 ⇒ S x0) (mapN (fun x0 ⇒ S x0) (g x)))
        = (fun x ⇒ mapN (permut 1) (mapN (fun x0 ⇒ S x0) (mapN (fun x0 ⇒ S x0) (g x))))).
        extens. intros. repeat (rewrite mapN_mapN).
      asserts_rewrite× ((fun x ⇒ S (S x))= fun x ⇒ permut 1 (S (S x))); auto.
        extens. simpl_permut.
      rewrite <-bind_mapN; auto with sc.
  - apply sc_trans with (nu nu bind (fun x : V ⇒ shiftN 1 (shiftN 1 (f x))) P).
    × asserts_rewrite ((fun x ⇒ mapN (fun x0 ⇒ S x0) (mapN (fun x0 ⇒ S x0) (f x)))
         = (fun x ⇒ mapN (permut 1) (mapN (fun x0 ⇒ S x0) (mapN (fun x0 ⇒ S x0) (f x))))).
        extens. intros. repeat (rewrite mapN_mapN).
      asserts_rewrite× ((fun x ⇒ S (S x))= fun x ⇒ permut 1 (S (S x))).
        extens. simpl_permut.
      rewrite <-bind_mapN; auto with sc.
    × repeat (apply sc_nu). auto using (shiftN_injective 1) with sc.
  - eauto with sc.
Qed.

Hint Resolve sc_bind:sc.

Lemma sc_nuK_permutK {V:Set}: ∀ k (P:proc V),
  struct_congr (genNu (S k) P) (genNu (S k) (mapN (permut k) P)).
Proof.
  induction k.
  - intros. simpl. erewrite mapN_id. auto with sc. simpl_permut.
  - intros. apply sc_trans with (genNu (S k)(mapN (permut k) (nu P))).
    Opaque mapN. simpl. rewrite nu_genNu.
    replace (nu genNu k (nu P)) with (genNu (S k) (nu P)) by reflexivity.
    apply IHk.
    replace (genNu (S (S k)) (mapN (permut (S k)) P)) with
      (genNu (S k)(nu (mapN (permut (S k)) P))) by (simpl; rewrite <- nu_genNu; auto).
    simpl. repeat (rewrite nu_genNu). apply sc_genNu.
    Transparent mapN. simpl.
    apply sc_trans with (nu nu mapN (permut 1)(mapN (liftN (permut k) 1) P)).
    auto with sc.
    replace (mapN (permut 1) (mapN (liftN (permut k) 1) P)) with (mapN (permut (S k)) P).
    auto with sc.
    rewrite mapN_mapN. fequals. extens; simpl_liftN; simpl_permut.
Qed.

Lemma sc_scope_genNu {V:Set}: ∀ k (P Q:proc V),
   struct_congr (genNu k (P // (shiftN k Q))) ((genNu k P) // Q).
Proof.
  induction k; intros.
  - simpl. rewrite mapN_id'; auto with sc.
  - simpl. repeat (rewrite nu_genNu).
    apply sc_trans with (genNu k ((nu P) // (mapN (fun x⇒k+x) Q))); auto.
    apply sc_genNu.
    replace (mapN (fun x ⇒ S (k + x)) Q)
         with (shiftN 1 (mapN (fun x ⇒ k+x) Q)). auto with sc.
    simpl. rewrite mapN_mapN. auto.
Qed.

Lemma sc_scope_genNu' {V:Set}: ∀ k (P Q:proc V),
   struct_congr (genNu k (nu (P // (mapN (liftN S k) Q)))) (genNu k ((nu (mapN (permut k) P)) // Q)).
Proof.
  intros. apply sc_trans with (genNu k (nu (mapN (permut k)(P // mapN (liftN S k) Q)))).
   repeat (rewrite genNu_fold). apply sc_nuK_permutK.
   simpl. replace (mapN (permut k) (mapN (liftN S k) Q)) with (shiftN 1 Q); auto with sc.
   rewrite mapN_mapN. fequals. extens; simpl_liftN; simpl_permut.
Qed.

Hint Resolve sc_scope_genNu sc_scope_genNu':sc.

Lemma clusterfuck: ∀ Pr' k' P,
  bind (fun x : incV Empty_set ⇒ mapN (fun x0 ⇒ S x0) (subst_func Pr' x))
       (mapN (liftN (fun x ⇒ k' + x) 1)(mapN (fun x ⇒ S x) P)) =
  ((shiftN 1)(subst ((shiftN k') (P)) Pr')).
Proof.
  intros. rewrite bind_mapN.
  simpl. repeat (rewrite mapN_mapN). repeat fequals.
    extens. simpl_liftN.
Qed.

Lemma sc_new_A_shift: ∀ A (Q:proc0), sim_test struct_congr
  (new (parl A (mapN (fun x ⇒ S x) Q))) (parl (new A) Q).
Proof.
  intros; destruct_agent_sim A; intros; auto with sc.
  × simpl. rewrite (mapV_mapN _ _ (@VS _)). rewrite clusterfuck.
    auto with sc.
  × simpl. case_if. simpl. rewrite mapN_mapN. replace (fun x ⇒ n + S x) with
     (fun x ⇒ S (n + x)); auto with sc.
    extens; intros; omega.
    simpl.
    rewrite (mapN_mapN _ (fun x ⇒ S x) (fun x ⇒ n+x)).
    replace (fun x ⇒ n + S x) with (fun x ⇒ (S n) + x) by (extens; intros; omega).
    rewrite permut_shiftN; auto.
    replace ((shiftN (S n)) Q) with (shiftN 1 (shiftN n Q) )
    by (rewrite mapN_mapN; simpl; auto). auto with sc.
Qed.

Lemma sc_new_shift_A {V:Set}: ∀ A (P:proc V) f, sim_test struct_congr
 (new (parr (mapV f P)(amapN S A))) (parr (mapV f (nu P)) A).
Proof.
  intros; destruct_agent_sim A; simpl in *; intros; auto with sc.
  × rewrite clusterfuck. auto with sc.
  × case_if. false. simplfs. simpl_liftN.
    repeat (rewrite mapN_mapN).
    asserts_rewrite (mapN (fun x ⇒ permut n (liftN S n x)) p0 = shiftN 1 p0).
      apply mapN_eq_on_fn. intros. simpl_liftN; simpl_permut.
    asserts_rewrite (mapN (fun x : nat ⇒ permut n (n + x)) (mapV f P)
      = mapN (liftN (fun x ⇒ n + x) 1)(mapV f P)).
      apply mapN_eq_on_fn. simpl_liftN; simpl_permut.
    asserts_rewrite (mapN (fun x : nat ⇒ down n (liftN S n x)) p = p).
      apply mapN_id. simpl_name.
    eauto with sc.
Qed.

Lemma sc_appl_new_conc: ∀ C F,
   struct_congr (nu appl C (fmapN S F)) (appl (conc_new C) F).
Proof.
  intros [] []. simpl. case_if; simpl.
  - rewrite mapN_mapN. asserts_rewrite (mapN (fun x : nat ⇒ n + S x) p1 = mapN (fun x : nat ⇒ S (n + x)) p1).
    fequals. extens; intros; omega. auto with sc.
  - rewrite nu_genNu. assert (p = mapN (liftN S n)(mapN (down n) p)).
      rewrite <- (mapN_id' p) at 1. rewrite mapN_mapN. apply mapN_eq_on_fn. intros. simpl_name.
      assert (k=n) by omega. substs; intuition.
    rewrite H at 1. asserts_rewrite (subst ((shiftN n) (mapN S p1)) (mapN (liftN S n)(mapN (down n) p))=
        (mapN (liftN S n) (subst ((shiftN n) p1)(mapN (down n) p)))).
       rewrite subst_mapN. rewrite shiftN_mapN. auto.
    apply sc_scope_genNu'.
Qed.

Lemma sc_appr_new_abs: ∀ C F,
   struct_congr (nu appr F (cmapN S C)) (appr (abs_new F) C).
Proof.
  intros [] []. simpl. rewrite nu_genNu.
  apply sc_trans with (genNu n ((nu mapN (permut n) ((subst ((shiftN n) p1) (mapN (liftN S n) p)))) //
          p0)). apply sc_scope_genNu'.
  asserts_rewrite (mapN (permut n) (subst ((shiftN n) p1) (mapN (liftN S n) p)) = bind
           (fun x : incV Empty_set ⇒ mapN (fun x0 : name ⇒ S x0) (subst_func p x))
           (mapN (liftN (fun x : name ⇒ n + x) 1) p1)); auto with sc.
  rewrite bind_mapN. fequals.
  extens. intros [ |]; simpl; auto. rewrite mapN_mapN. fequals. extens; simpl_name.
  rewrite mapN_mapN. fequals. extens; simpl_name.
Qed.

Lemma sc_appr_appl: ∀ F C,
   struct_congr (appr F C) (appl C F).
Proof.
  intros; destruct C as [ n Q R]. destruct F as [ S ]; simpl.
  auto with sc.
Qed.

Lemma sc_appl_appr: ∀ F C,
   struct_congr (appl C F) (appr F C).
Proof.
  intros; destruct C as [ n Q R]. destruct F as [ S ]; simpl.
  auto with sc.
Qed.

Hint Resolve sc_appr_appl sc_appl_appr sc_appl_new_conc sc_appr_new_abs:sc.

Lemma sc_nuK_compL_permutK {V:Set}: ∀ k l (P:proc V),
  struct_congr (genNu (S k) P) (genNu (S k) (mapN (comp l (permut k)) P)).
Proof.
  induction l; intros.
  - simpl. erewrite mapN_id; auto with sc.
  - apply sc_trans with (genNu (S k) (mapN (permut k)(mapN (comp l (permut k)) P))).
    apply sc_trans with (genNu (S k) (mapN (comp l (permut k)) P)); auto.
    apply sc_nuK_permutK.
    rewrite mapN_mapN. simpl. auto with sc.
Qed.

Lemma sc_nuK_permut1 {V:Set}: ∀ (P:proc V) k,
    struct_congr (genNu (S (S k)) P)(genNu (S (S k))(mapN (liftN (permut 1) k) P)).
Proof.
  intros. apply sc_trans with (genNu (S (S k))(mapN (permut (S k)) P)).
  apply sc_nuK_permutK.
  apply sc_trans with (genNu (S (S k))(mapN (comp k (permut k))(mapN (permut (S k)) P))).
  apply sc_nu. fold (@genNu V). apply sc_nuK_compL_permutK.
  replace (mapN (comp k (permut k)) (mapN (permut (S k)) P))
            with (mapN (liftN (permut 1) k) P); auto with sc.
  rewrite mapN_mapN; fequals; extens; intros.
  destruct k.
  - simpl. rewrite× liftN_0.
  - unfold liftN. case_if.
    + rewrite compK_permutK_leb; auto. unfold permut; repeat (case_if; try omega).
      replace (S k+(x1+1)) with (x1 + 1×S (S k)) by omega.
      rewrite Nat.mod_add; auto. rewrite Nat.mod_small; try omega. simpl_permut.
    + destruct (classic (x1 = S k)). subst.
      rewrite compK_permutK_gt; simpl_permut; omega.
      destruct (classic (x1=(S (S k)))). subst.
      rewrite compK_permutK_leb; try omega.
      rewrite Nat.mod_small; unfold permut; repeat (case_if; try omega). simpl_permut.
      rewrite compK_permutK_gt; try (simpl_permut; omega).
Qed.

Lemma nu_nu_conc: ∀ F C, struct_congr (appr F (conc_new (conc_new C)))
          (appr F (conc_new (conc_new (cmapN (permut 1) C)))).
Proof.
  intros F C.
  apply sc_trans with (nu nu (appr (fmapN S (fmapN S F)) C)).
  apply sc_trans with (nu (appr (fmapN S F) (conc_new C))). eauto with sc. apply sc_nu. eauto with sc.
  apply sc_trans with (nu nu (appr (fmapN S (fmapN S F)) (cmapN (permut 1) C))).
  destruct F, C. simpl. asserts_rewrite ((subst ((shiftN n) (mapN S (mapN S p))) (mapN (liftN (permut 1) n) p0) //
            mapN (liftN (permut 1) n) p1) = (mapN (liftN (permut 1) n)(subst ((shiftN n)(mapN S (mapN S p))) p0 //
            p1))).
  simpl. fequals. rewrite subst_mapN. fequals. repeat (rewrite mapN_mapN). fequals. extens; simpl_name.
  repeat (rewrite nu_genNu; rewrite genNu_fold). apply sc_nuK_permut1.
  apply sc_trans with (nu (appr (fmapN S F)(conc_new (cmapN (permut 1) C)))).
  apply sc_nu. eauto with sc. eauto with sc.
Qed.

Lemma sc_nu_nu_permut : ∀ A,
  sim_test struct_congr (new (new A)) (new (new (amapN (permut 1) A))).
Proof.
  intros; destruct_agent_sim A; auto with sc.
  × simpl.
    replace (bind (fun x : incV Empty_set ⇒ mapN (fun x0 ⇒ S x0)
      (mapN (fun x0 ⇒ S x0) (subst_func p0 x)))(mapN (liftN (liftN (fun x ⇒ n + x) 1) 1)
               (mapN (permut 1) p))) with
      (mapN (permut 1)(bind (fun x : incV Empty_set ⇒ mapN (fun x0 ⇒ S x0)
               (mapN (fun x0 ⇒ S x0) (subst_func p0 x)))(mapN (liftN (liftN (fun x ⇒ n + x) 1) 1)
               p))); auto with sc.
    erewrite bind_mapN. fequals.
      extens. intros [ | ]; simpl; auto.
      repeat (rewrite mapN_mapN). apply mapN_eq_on_fn; intros. simpl_permut.
      repeat (rewrite mapN_mapN). apply mapN_eq_on_fn; intros.
      repeat (rewrite liftN_liftN). simpl. simpl_liftN; simpl_permut.
  × remember (abs_def p1) as F. fold (conc_new (conc_def n p p0)).
    asserts_rewrite ((If n \in fn (mapN (liftN (permut 1) n) p)
         then conc_def (S n) (mapN (liftN (permut 1) n) p)
                (mapN (liftN (permut 1) n) p0)
         else conc_def n (mapN (down n) (mapN (liftN (permut 1) n) p))
                (nu mapN (permut n) (mapN (liftN (permut 1) n) p0)))= conc_new (cmapN (permut 1)(conc_def n p p0))).
    simpl. auto. apply nu_nu_conc.
Qed.

Lemma struct_congr_sim' {V : Set} : ∀ P Q f, @struct_congr V P Q →
  ∀ P' l A, lts P' l A → P' = (mapV f P) →
  ∃ A', lts (mapV f Q) l A' ∧ sim_test struct_congr A A'.
Proof.
  intros P Q f Hstruct.
  induction Hstruct; intros P'' l A Hlts Hp'; subst.
  -
    inverts Hlts.
    +
      ∃ (parl (parl A0 (mapV f Q)) (mapV f R)). split;simpl.
      eapply lts_parl'; eauto with hopi.
      destruct_agent_sim A0; simpl; eauto with sc.
    + inversion H3; subst.
     ×
      ∃ (parl (parr (mapV f P) A) (mapV f R)). split;simpl.
      eapply lts_parl'; eauto with hopi.
      destruct_agent_sim A; simpl; eauto with sc.
     ×
      ∃ (parr ((mapV f P)// (mapV f Q)) A). split;simpl.
      eapply lts_parr'; subst; eauto with hopi.
      destruct_agent_sim A; simpl; eauto with sc.
     ×
      ∃ (ag_proc(appl (conc_parr (mapV f P) C) F)).
      split. eapply lts_taul'; eauto with hopi. eapply lts_parr'. apply H1. simpl; auto with hopi.
      apply st_proc.
      destruct C. simpl.
      apply sc_trans with (genNu n ((p0 // asubst (fshiftN n F) p) // (shiftN n)(mapV f P))); eauto with sc.
     ×
      ∃ (ag_proc(appr (abs_parr (mapV f P) F) C)).
      split. eapply lts_taur'; eauto with hopi. eapply lts_parr'; eauto.
      apply st_proc. destruct C as [ n Q' R']; simpl. destruct F as [ S ]; simpl.
      apply sc_trans with (genNu n (shiftN n (mapV f P) // (subst ((shiftN n) S) Q' // R'))); eauto with sc.
      apply sc_genNu. rewrite <- (mapV_mapN _ _(@VS _)). rewrite subst_shift. auto with sc.
    +
      inversion H4; subst.
      ×
        destruct A as [| F' | ]; inversion H5; subst.
        ∃ (ag_proc(appl C F' // mapV f R)).
        split. eapply lts_parl'; eauto with hopi.
        apply st_proc. destruct C as [ n Q' R']. destruct F' as [ S ]; simpl.
        rewrite <- (mapV_mapN _ _ (@VS _)). rewrite subst_shift. eauto with sc.
      ×
        destruct A as [| F' | ]; inversion H5; subst.
        ∃ (ag_proc(appl (conc_parl C (mapV f Q)) F')).
        split. eapply lts_taul'; eauto with hopi. eapply lts_parl'; eauto with hopi.
        apply st_proc. destruct C as [ n Q' R']. destruct F' as [ S ]; simpl.
        rewrite <- (mapV_mapN _ _ (@VS _)). rewrite subst_shift. auto with sc.
    +
      inversion H4; subst.
      ×
        destruct A as [| | C']; inversion H5; subst.
        ∃ (ag_proc(appr F C' // mapV f R)).
        split. eapply lts_parl'; eauto with hopi.
        apply st_proc. destruct C' as [ n Q' R']. destruct F as [ S ]; simpl.
        eauto with sc.
      ×
        destruct A as [| | C']; inversion H5; subst.
        ∃ (ag_proc(appr (abs_parl F (mapV f Q)) C')).
        split. eapply lts_taur'; eauto with hopi. eapply lts_parl'; eauto with hopi.
        apply st_proc. destruct C' as [ n Q' R']. destruct F as [ S ]; simpl.
        repeat (rewrite <- (mapV_mapN _ _ (@VS _))). rewrite subst_shift. auto with sc.
  -
    inversion Hlts; subst.
    + inversion H3; subst.
     ×
      ∃ (parl A (mapV f Q // mapV f R)). split;simpl.
      eapply lts_parl'; eauto with hopi.
      destruct_agent_sim A; simpl; eauto with sc.
     ×
      ∃ (parr (mapV f P) (parl A (mapV f R))). split;simpl.
      eapply lts_parr'; eauto with hopi.
      destruct_agent_sim A; simpl; eauto with sc.
     ×
      ∃ (ag_proc (appl C (abs_parl F (mapV f R)))).
      split. eapply lts_taul'; eauto with hopi. eapply lts_parl'; eauto with hopi.
      apply st_proc.
      destruct C. simpl. destruct F as [ P' ]; simpl.
      rewrite <- (mapV_mapN _ _ (@VS _)). rewrite subst_shift. eauto with sc.
     ×
      ∃ (ag_proc(appr F (conc_parl C (mapV f R)))).
      split. eapply lts_taur'; eauto with hopi. eapply lts_parl'; eauto.
      apply st_proc. destruct C as [ n Q' R']; simpl. destruct F as [ P' ]; simpl. eauto with sc.
    +
      eexists. split. eapply lts_parr'; eauto. eapply lts_parr'; eauto. fold (@mapV V).
      destruct_agent_sim A0; simpl; eauto with sc.
    +
      inversion H1; subst.
      ×
        destruct A as [| | C']; inversion H5; subst.
        eexists. split. eapply lts_taul'; eauto with hopi. eapply lts_parr'; eauto with hopi.
        fold (@mapV V). simpl; eauto.
        apply st_proc. destruct C' as [ n Q' R']. destruct F as [ S ]; simpl.
        repeat (rewrite <- (mapV_mapN _ _ (@VS _))). rewrite subst_shift. auto with sc.
      ×
        destruct A as [| | C']; inversion H5; subst.
        eexists. split. eapply lts_parr'; eauto with hopi. fold (@mapV V).
        apply st_proc. destruct C' as [ n Q' R']. destruct F as [ S ]; simpl. eauto with sc.
   +
      inversion H1; subst.
      ×
        destruct A as [| F' | ]; inversion H5; subst.
        eexists. split. eapply lts_taur'; eauto with hopi. eapply lts_parr'; eauto with hopi. simpl; eauto.
        fold (@mapV V). destruct C as [ n Q' R']. destruct F' as [ S ]; simpl. apply st_proc.
        rewrite <- (mapV_mapN _ _ (@VS _)). rewrite subst_shift. auto with sc.
      ×
        destruct A as [| F' | ]; inversion H5; subst.
        eexists. split. eapply lts_parr'; eauto with hopi. fold (@mapV V).
        apply st_proc. destruct C as [ n Q' R']. destruct F' as [ S ]; simpl.
        rewrite <- (mapV_mapN _ _ (@VS _)). rewrite subst_shift. eauto with sc.
  -
    inversion Hlts; subst.
    +
      ∃ (parr (mapV f Q) A0). split; subst; simpl; eauto with hopi.
      destruct_agent_sim A0; simpl; eauto with sc.
    +
      ∃ (parl A0 (mapV f P)). split; subst; simpl; eauto with hopi.
      destruct_agent_sim A0; simpl; eauto with sc.
    +
      ∃ (ag_proc (appr F C)).
      split. eapply lts_taur'; eauto with hopi. apply st_proc. apply sc_appl_appr.
    +
      ∃ (ag_proc (appl C F)).
      split. eapply lts_taul'; eauto with hopi. apply st_proc. apply sc_appr_appl.
  -
    inversion Hlts; subst.
    + ∃ A0; subst; split; eauto with hopi.
      destruct_agent_sim A0; simpl; eauto with sc.
    + inversion H3.
    + inversion H4.
    + inversion H4.
  -
    eexists. split. eapply lts_parl'; eauto. destruct_agent_sim A; simpl; eauto with sc.
  -
    inverts Hlts. inverts H1.
    +
      ∃ (parl (new A) (mapV f Q)). split; subst; simpl; eauto with hopi.
      rewrite mapV_mapN. apply sc_new_A_shift.
    +
      rewrite mapV_mapN in H5.
      eapply mapN_lts_rev in H5; eauto with hopi.
      destruct H5 as [ A' [ l' [ HA' [ HltsQ Hl' ]]]].
      ∃ (parr (mapV f (nu P)) A').
      split. simpl. eapply lts_parr'; eauto. subst.
      asserts_rewrite (down_lab (lmapN (fun x : nat ⇒ S x) l') = l').
        destruct l'; simpl; auto with arith.
      auto. subst. apply sc_new_shift_A.
    +
      rewrite mapV_mapN in H6. eapply mapN_lts_rev in H6; eauto.
      destruct H6 as [A' [ l' [ HFA' [ HltsA' Hl' ]]]]. destruct A' as [ | F' | ]; inverts HFA'.
      destruct l'; inverts Hl'.
      ∃ (ag_proc (appl (conc_new C) F')).
      split. simpl. eapply lts_taul'; eauto with hopi.
      replace (ag_conc (conc_new C)) with (new (ag_conc C)); auto.
      clear H0. eapply lts_new'; eauto with hopi; simpl; [ fsetdec | auto with arith].
      simpl. apply st_proc. apply sc_appl_new_conc.
    +
      rewrite mapV_mapN in H6. eapply mapN_lts_rev in H6; eauto.
      destruct H6 as [A' [ l' [ HFA' [ HltsA' Hl' ]]]]. destruct A' as [ | | C' ]; inverts HFA'.
      destruct l'; inverts Hl'.
      ∃ (ag_proc (appr (abs_new F) C')).
      split. simpl. eapply lts_taur'; eauto.
      replace (ag_abs (abs_new F)) with (new (ag_abs F)); eauto with hopi.
      clear H0. eapply lts_new'; eauto with hopi; simpl; [ fsetdec | auto with arith].
      simpl. apply st_proc. apply sc_appr_new_abs.
  -
    inverts Hlts. inverts H3.
    +
      eexists. split. eapply lts_new; eauto. eapply lts_parl'; eauto with hopi. fold (@mapV V).
      rewrite mapV_mapN. apply sim_test_sym. unfold sym; apply sc_symmetric. apply sc_new_A_shift.
    +
      eexists. split. eapply lts_new'; eauto. Focus 2. eapply lts_parr'; eauto with hopi.
      rewrite mapV_mapN. apply mapN_lts; eauto.
      destruct l; simpl; auto with hopi. destruct l; simpl; auto with arith. fold (@mapV V). simpl.
      apply sim_test_sym. unfold sym; apply sc_symmetric. apply sc_new_shift_A.
   +
      inverts H1. destruct A; inverts H2. destruct l0; inverts H0.
      eexists. split. eapply lts_new'; auto with hopi. Focus 2.
      eapply lts_taul'; eauto with hopi. rewrite mapV_mapN.
      apply (mapN_lts _ _ _ S) in H4; simpl in *; auto. destruct_notin.
      replace (S(n-1)) with n in H4. apply H4. destruct n; intuition.
      auto. auto. apply sim_test_sym. unfold sym; auto with sc.
      apply st_proc. apply sc_appl_new_conc.
   +
      inverts H1. destruct A; inverts H2. destruct l0; inverts H0.
      eexists. split. eapply lts_new'; auto with hopi. Focus 2.
      eapply lts_taur'; eauto with hopi. rewrite mapV_mapN.
      apply (mapN_lts _ _ _ S) in H4; simpl in ×. replace (S(n-1)) with n in H4. apply H4.
      destruct n; intuition. auto. auto. apply sim_test_sym. unfold sym; auto with sc.
      apply st_proc. apply sc_appr_new_abs.
  - simpl in Hlts; inverts Hlts. inverts H1.
  - inversion Hlts.
  -
    inverts Hlts. inverts H1.
    ∃ (new (new (amapN (permut 1) A))).
    split.
    + eapply lts_new; eauto. eapply lts_new; eauto. fold (@mapV V).
      replace l0 with (lmapN (permut 1) l0).
      rewrite mapV_mapN. apply mapN_lts; auto.
      destruct l0; simpl in *; destruct_notin; simpl_permut; auto.
    + apply sc_nu_nu_permut.
  -
    inverts Hlts. inverts H1. rewrite mapV_mapN in H3. eapply mapN_lts_rev in H3; eauto.
    destruct H3 as [ A' [ l' [ HA' [ HltsA' Hl ] ] ] ].
    subst. eexists. split. simpl. eapply lts_new; eauto with hopi.
    eapply lts_new; eauto with hopi.
    destruct l'; simpl in *; destruct_notin; simpl_permut; eassumption.
    apply sim_test_sym. unfold sym; auto with sc. apply sc_nu_nu_permut.
    intros_all; simpl_permut.
  - simpl in Hlts; inversion Hlts.
  - simpl in Hlts; inversion Hlts.
  -
    inverts Hlts.
    +
      forwards: IHHstruct1 A0 H3; auto. destruct H as [ A' [ Hq HAA' ]].
      ∃ (parl A' (mapV f Q')).
      split. eapply lts_parl'; eauto.
      destruct A0; destruct A'; inversion HAA'; subst.
      × apply st_proc. auto with sc.
      × apply st_abs. intros. forwards: H2 C; auto. destruct C as [ k R S ]; simpl.
        destruct a; destruct a0; simpl. repeat (rewrite <- (mapV_mapN _ _ (@VS _))).
        repeat (rewrite subst_shift).
        apply sc_trans with (genNu k (subst ((shiftN k) p) R // S) // (mapV f P')).
        apply sc_trans with (genNu k ((subst ((shiftN k) p) R // S) // shiftN k (mapV f P'))); eauto with sc.
        apply sc_trans with (genNu k (subst ((shiftN k) p0) R // S) // (mapV f Q')); eauto with sc.
        apply sc_trans with (genNu k ((subst ((shiftN k) p0) R // S) // shiftN k (mapV f Q'))); eauto with sc.
      × apply st_conc. intros; forwards: H2 F; auto. destruct F as [ R ]; simpl.
        destruct c; destruct c0; simpl; simpl in H2.
        apply sc_trans with (genNu n ((subst ((shiftN n) R) p // p0) // shiftN n (mapV f P'))); auto with sc.
        apply sc_trans with (genNu n0 ((subst ((shiftN n0) R) p1 // p2) // shiftN n0 (mapV f Q'))); auto with sc.
        apply sc_trans with (genNu n ((subst ((shiftN n) R) p // p0)) // mapV f P'); auto with sc.
        apply sc_trans with (genNu n0 ((subst ((shiftN n0) R) p1 // p2)) // mapV f Q'); auto with sc.
    +
      forwards: IHHstruct2 A0 H3; auto. destruct H as [ A' [ Hq HAA' ]].
      ∃ (parr (mapV f Q) A').
      split. eapply lts_parr'; eauto.
      destruct A0; destruct A'; inversion HAA'; subst.
      × apply st_proc. auto with sc.
      × apply st_abs. intros. forwards: H2 C; auto. destruct C as [ k R S ]; simpl.
        destruct a; destruct a0; simpl. simpl in H2. repeat (rewrite <- (mapV_mapN _ _ (@VS _))).
        repeat (rewrite subst_shift). simpl in H0.
        apply sc_trans with (genNu k ((subst ((shiftN k) p) R // S) // (shiftN k) (mapV f P))); eauto with sc.
        apply sc_trans with (genNu k ((subst ((shiftN k) p0) R // S) // (shiftN k) (mapV f Q))); eauto with sc.
        apply sc_trans with (genNu k ((subst ((shiftN k) p) R // S)) // (mapV f P)); eauto with sc.
      × apply st_conc. intros. forwards: H2 F; auto. destruct F as [ R ]; simpl.
        destruct c; destruct c0; simpl. simpl in H.
        apply sc_trans with (genNu n ((subst ((shiftN n) R) p // p0) // (shiftN n) (mapV f P))); eauto with sc.
        apply sc_trans with (genNu n0 ((subst ((shiftN n0) R) p1 // p2) // (shiftN n0) (mapV f Q))); eauto with sc.
        apply sc_trans with (genNu n ((subst ((shiftN n) R) p // p0)) // (mapV f P)); eauto with sc.
    +
      forwards: IHHstruct1 H1; auto. destruct H as [ A' [ Hq HAA' ]].
      forwards: IHHstruct2 H4; auto. destruct H as [ A'' [ Hq' HAA'' ]].
      assert (Hbla:=Hq'). apply lts_inp_abs in Hq'. destruct Hq' as [ F' ]; subst.
      assert (Hbla':=Hq). apply lts_out_conc in Hq. destruct Hq as [ C' ]; subst.
      ∃ (ag_proc (appl C' F')).
      split. eapply lts_taul'; eauto.
      apply st_proc. inverts HAA'. forwards: H3 F; auto with hopi.
      inverts HAA''. forwards: H6 C'; auto with hopi.
         eapply lts_conc_wf; eauto.
      apply sc_trans with (appr F C). apply sc_appl_appr.
      apply sc_trans with (appr F' C'); eauto with sc.
    +
      forwards: IHHstruct1 f H1; auto. destruct H as [ A' [ Hq HAA' ]].
      forwards: IHHstruct2 H4; auto. destruct H as [ A'' [ Hq' HAA'' ]].
      assert (Hbla:=Hq'). apply lts_out_conc in Hq'. destruct Hq' as [ C' ]; subst.
      assert (Hbla':=Hq). apply lts_inp_abs in Hq. destruct Hq as [ F' ]; subst.
      ∃ (ag_proc (appr F' C')).
      split. eapply lts_taur'; eauto.
      apply st_proc. inverts HAA'. forwards: H3 C; auto with hopi.
        eapply lts_conc_wf; eauto.
      inverts HAA''. forwards: H6 F'; auto with hopi. eauto with sc.
  -
    inverts Hlts. ∃ (ag_abs (abs_def (mapV (incV_map f) Q))).
    simpl; split; auto with hopi.
    apply st_abs; intros [k R S] H'; simpl. apply sc_genNu. apply sc_par;
      auto using (shiftN_injective k) with sc.
  -
    inverts Hlts. ∃ (ag_conc (conc_def 0 (mapV f Q) (mapV f Q'))).
    simpl; split; auto with hopi.
    apply st_conc. intros [ R]. simpl. apply sc_par; auto with sc. apply sc_bind; auto with sc.
    intros [ |]; simpl; auto with sc.
  -
    simpl in Hlts. inverts Hlts.
    edestruct IHHstruct as [ A' [HltsA' HAA'] ]. exact H1. eauto.
    ∃ (new A'). split.
    simpl. apply lts_new; auto.
    destruct A0 as [ P' | F | C ]; inverts HAA'; simpl; auto.
    × apply st_proc; auto with sc.
    × apply st_abs. intros. specialize (H3 (cmapN S C)).
      apply sc_trans with (nu (appr F (cmapN S C))). apply sc_symmetric. apply sc_appr_new_abs.
      apply sc_trans with (nu (appr F' (cmapN S C))). apply sc_nu. apply H3. apply× mapN_concwf.
      apply sc_appr_new_abs.
    × apply st_conc. intros. specialize (H3 (fmapN S F)).
      assert (struct_congr (appl C (fmapN S F)) (appl C' (fmapN S F))).
      { eapply sc_trans. apply sc_appl_appr. eapply sc_trans. apply H3. apply sc_appr_appl. }
      apply sc_trans with (appl (conc_new C) F). apply sc_appr_appl.
      apply sc_trans with (nu (appl C (fmapN S F))); auto with sc.
      apply sc_trans with (nu (appl C' (fmapN S F))); auto with sc.
      apply sc_trans with (appl (conc_new C') F); auto with sc.
  -
    edestruct IHHstruct1 as [A1 [HltsA1 HAA1]]; eauto.
    edestruct IHHstruct2 as [A2 [HltsA2 HAA2]]; eauto.
    ∃ A2. split; auto.
    eapply sim_test_trans; eauto.
    intros P' Q' R' Hpq Hqr; eapply sc_trans; eauto.
Qed.

Notation sc0 := (@struct_congr Empty_set).

Lemma struct_congr_sim: simulation sc0.
Proof.
  apply late_implies_sim.
  intros P Q Hstruct.
  replace Q with (mapV (fun x ⇒ x) Q) by (apply mapV_id).
  replace P with (mapV (fun x ⇒ x) P) by (apply mapV_id).
  intros; forwards: @struct_congr_sim'; eauto.
Qed.

Lemma struct_congr_bisim: bisimulation sc0.
Proof.
  apply sim_sym_imply_bisim; auto with sc.
  apply struct_congr_sim.
  unfold sym; apply sc_symmetric.
Qed.

Lemma oe_sc0 : ∀ Rel, Rincl sc0 Rel → Rincl sc0 (open_extension Rel).
Proof.
  intros_all. apply× oe_proc0.
Qed.

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

Definition bisimulation_up_to_sc (Rel : binary proc0) : Prop :=
  (simulation_up_to_sc Rel) ∧ (simulation_up_to_sc (inverse Rel)).

Lemma up_to_sc_sim : ∀ Rel, simulation_up_to_sc Rel
      → simulation (sc0 ° Rel ° sc0).
Proof.
  intros_all. destruct_comp. destruct struct_congr_bisim.
  forwards*: H3 P. forwards*: H3 x0. specialize (H x x0 H1).
  splits; intros; forwards_test (@struct_congr Empty_set); forwards_test (sc0 ° Rel ° sc0);
      forwards_test (@struct_congr Empty_set); eexists; intuition (try eassumption);
    destruct_comp; ∃ x1; split; eauto with sc; ∃ x2; eauto with sc.
Qed.

Lemma up_to_sc_sound : ∀ Rel, bisimulation_up_to_sc Rel
    → Rincl Rel bisimilarity.
Proof.
  intros_all. inverts H.
  ∃ (sc0 ° Rel ° sc0).
  split. split. apply× up_to_sc_sim.
  replace (inverse (sc0 ° Rel ° sc0)) with (sc0 ° inverse Rel ° sc0).
  apply× up_to_sc_sim. repeat (rewrite comp_trans).
  asserts_rewrite (inverse sc0 = sc0).
    rewrite inverse_sym; auto with sc. unfold sym; apply sc_symmetric.
  apply comp_assoc.
  ∃ x. intuition.
  ∃ y. intuition.
Qed.