Require Export Howe.

Notation pseudo_sim :=
  (∀ {V W:Set} Rel (P1 Q1:proc V)(P2 Q2:proc W) a F1 C1 (f:V → proc0)(g: W → proc0),
   simulation Rel → refl Rel → rename_compatible Rel → (Rincl sc0 Rel) → trans Rel
   → howe Rel P2 Q2 → howe Rel P1 Q1
   → lts (bind f P1) (inp a) (ag_abs F1) → lts (bind g P2) (out a) (ag_conc C1)
   → ∃ F2 C2 P'2 Q'2, lts (bind f Q1) (inp a) (ag_abs F2) ∧
                            lts (bind g Q2) (out a) (ag_conc C2) ∧
                            sc0 P'2 (appr F1 C1) ∧
                            sc0 Q'2 (appr F2 C2) ∧
                            howe Rel P'2 Q'2).

Lemma pseudo_inp_first {V:Set}:
  ∀ Rel (P1 Q1:proc V)(P2 Q2:proc0) a F1 (f:V → proc0),
    simulation Rel → refl Rel → rename_compatible Rel
  → (∀ P Q, Rel (P // PO) (Q // PO) → Rel P Q)
  → howe Rel P1 Q1 → howe Rel P2 Q2
  → lts (bind f P1) (inp a) (ag_abs F1)
  → ∃ F2, lts (bind f Q1) (inp a) (ag_abs F2) ∧
                howe Rel (asubst F1 P2) (asubst F2 Q2).
Proof.
  introv Hsim Hrefl Hrename HpO Hp1q1. gen a f F1 P2 Q2.
  induction Hp1q1; introv Hp2q2 HltsP1; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 Hp2q2 HltsP1. destruct H0 as [F2 [Hltsf2 Hhowe]].
    forwards*: H f. remember (conc_def 0 Q2 PO) as C.
    assert (Hwf:conc_wf C). subst. intros_all. omega.
    unfold simulation in Hsim. forwards_test Rel.
    destruct F2 as [R']; destruct F'0 as [Q'1]; subst. simpl in H5.
    apply HpO in H5. repeat (rewrite mapN_id' in H5).
    ∃ (abs_def Q'1); intuition. simpl.
    apply howe_comp with (subst R' Q2); eauto with howe hopi.
      apply× oe_proc0.
  - simpl in ×. ∃ F1; intuition. destruct F1 as [P']; simpl.
    apply howe_subst; auto with howe.
  - inverts HltsP1.
    + forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
      forwards*: IHHp1q1_1 Hp2q2 H2. destruct H as [F'2 [Hltsf'2 Hhowe]].
      ∃ (abs_parl F'2 (bind f Q')). split.
      eapply lts_parl'; eauto.
      inverts H3. destruct F'1 as [P'1]. destruct F'2 as [Q'1]. simpl.
      simpl in Hhowe. apply howe_par; auto with howe.
    + forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
      forwards*: IHHp1q1_2 Hp2q2 H2. destruct H as [F'2 [Hltsf'2 Hhowe]].
      ∃ (abs_parr (bind f Q) F'2 ). split.
      eapply lts_parr'; eauto.
      inverts H3. destruct F'1 as [P'1]. destruct F'2 as [Q'1]. simpl.
      simpl in Hhowe. apply howe_par; auto with howe.
  - inverts HltsP1. ∃ (abs_def (bind (liftV f) Q)). split.
    simpl. auto with hopi.
    simpl. apply howe_subst; auto with howe.
  - simpl in ×. inverts HltsP1.
    destruct l0; inverts H0. destruct A as [ | F1' | ]; inverts H1.
    forwards*: @howe_mapN Hp2q2 S.
    forwards*: IHHp1q1 H H3. destruct H0 as [F2' [ HltsF2' Hrel ]].
    ∃ (abs_new F2'). split. eapply lts_new'; eauto. destruct F1'; destruct F2'. simpl in ×.
    apply howe_nu.
    asserts_rewrite (bind
     (fun x : incV Empty_set ⇒ mapN (fun x0 : nat ⇒ S x0) (subst_func P2 x))
     p = subst p (mapN S P2)). fequals. extens. intros [ |]; simpl; auto.
    asserts_rewrite (bind
     (fun x : incV Empty_set ⇒ mapN (fun x0 : nat ⇒ S x0) (subst_func Q2 x))
     p0 = subst p0 (mapN S Q2)). fequals. extens. intros [ |]; simpl; auto. auto.
Qed.

Lemma pseudo_inp_conc {V:Set}: ∀ Rel (P1 Q1:proc V) a F1 C (f:V → proc0),
    simulation Rel → refl Rel → rename_compatible Rel
  → (∀ P Q, Rel (P // PO) (Q // PO) → Rel P Q)
  → howe Rel P1 Q1
  → lts (bind f P1) (inp a) (ag_abs F1)
  → ∃ F2, lts (bind f Q1) (inp a) (ag_abs F2) ∧ howe Rel (appr F1 C) (appr F2 C).
Proof.
  intros. destruct C. forwards: mapN_lts (fun x ⇒ n+x) H3.
  rewrite bind_mapN in H4. forwards*: @howe_mapN H2 (fun x ⇒ n+x).
  forwards: @pseudo_inp_first p p H5 H4; auto with hopi howe.
  destruct H6 as [F2 [HltsF2 Hhowe]].
  rewrite <- bind_mapN in HltsF2. apply mapN_lts_rev in HltsF2; auto using shiftN_injective.
  destruct HltsF2 as [A' [l' [HF2 [HltsA' Hl']]]]. destruct l'; inverts Hl'.
  assert (n0=a). apply plus_reg_l in H7. auto. subst. destruct A' as [ |F'| ]; inverts HF2.
  ∃ F'; intuition. destruct F1 as [P'1]; destruct F' as [P'2]; simpl in ×.
  apply howe_genNu. apply howe_par; auto with howe.
Qed.

Lemma pseudo_sim_out : pseudo_sim.
Proof.
  introv Hsim Hrefl Hrename Hsc0 Htrans Hp2q2.
  assert (∀ P Q : proc0, Rel (P // PO) (Q // PO) → Rel P Q) as HpO.
    intros. eauto with sc.
  gen a f g F1 C1 P1 Q1.
  induction Hp2q2; introv Hp1q1 HltsP1 HltsP2; try solve [inverts HltsP2].
  - forwards*: IHHp2q2 a F1 C1 P1 Q1.
    destruct H0 as [F2 [C2 [ P'2 [R' [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]].
    forwards*: H g. unfold simulation in ×.
    forwards_test Rel.
    ∃ F2 C'0 P'2 (appr F2 C'0); intuition.
    apply howe_comp with R'; auto with hopi howe.
      apply oe_trans with (appr F2 C2); auto.
      apply× oe_sc0. apply× oe_proc0.
  - forwards: @pseudo_inp_conc P1 Q1 F1 C1; eauto with hopi.
    destruct H as [F2 []]. ∃ F2 C1 (appr F1 C1) (appr F2 C1); intuition.
  - inverts HltsP2.
    + forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
      forwards*: IHHp2q2_1 Hp1q1 HltsP1 H2.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      ∃ F'2 (conc_parl C'2 (bind g Q')) (P'2// bind g P') (Q'2//bind g Q').
      splits; eauto with hopi howe.
      eapply lts_parl'; eauto.
      apply sc_trans with (appr F1 C'1 // bind g P'); auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (appr F1 C'1 // bind g P') (appr F1 (conc_parl C'1 (bind g P')))).
        destruct F1, C'1; simpl. eauto with sc.
      eauto with sc.
      apply sc_trans with (appr F'2 C'2 // bind g Q'); auto with sc hopi howe.
      assert (struct_congr
        (appr F'2 C'2 // bind g Q') (appr F'2 (conc_parl C'2 (bind g Q')))).
        destruct F'2, C'2; simpl. eauto with sc.
      auto with sc.
    + forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
      forwards*: IHHp2q2_2 Hp1q1 HltsP1 H2.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      ∃ F'2 (conc_parr (bind g Q) C'2) (bind g P // P'2) (bind g Q // Q'2).
      splits; eauto with hopi howe.
      eapply lts_parr'; eauto.
      apply sc_trans with (bind g P // appr F1 C'1); auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (bind g P // appr F1 C'1) (appr F1 (conc_parr (bind g P) C'1))).
        destruct F1, C'1; simpl. apply sc_trans with
          (genNu n (shiftN n (bind g P) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      auto with sc hopi howe.
      apply sc_trans with (bind g Q // appr F'2 C'2); auto with sc hopi howe.
      assert (struct_congr (bind g Q // appr F'2 C'2)
                            (appr F'2 (conc_parr (bind g Q) C'2))).
        destruct F'2, C'2; simpl. apply sc_trans with
          (genNu n (shiftN n (bind g Q) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      auto with sc hopi howe.
  - inverts HltsP2. simpl.
    forwards*: @pseudo_inp_first Rel P1 Q1 (bind g P)(bind g Q).
      apply @howe_bind; auto with howe.
    destruct H as [F2 [HltsQ1 HhoweF1F2]]. assert (∀ F, fshiftN 0 F = F).
      destruct F; simpl; rewrite× @mapN_id'.
    ∃ F2 (conc_def 0 (bind g Q) (bind g Q'))
        (appr F1 (conc_def 0 (bind g P) (bind g P')))
        (appr F2 (conc_def 0 (bind g Q) (bind g Q'))); intuition auto with hopi howe;
      simpl; repeat (rewrite H); auto with sc hopi howe.
  - simpl in ×. inverts HltsP2. destruct A as [ | | C1']; inverts H1. destruct l0; inverts H0.
    simpl in H2. destruct_notin. forwards*: mapN_lts S HltsP1. simpl in H. rewrite bind_mapN in H.
    asserts_rewrite (S (n-1) = n) in H. omega. forwards*: @howe_mapN Hp1q1 S.
    forwards*: IHHp2q2 H0 H H3. destruct H1 as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
    rewrite <- bind_mapN in HltsF'2. apply mapN_lts_rev in HltsF'2; try (intros_all; omega).
    destruct HltsF'2 as [A' [l' [Hf'2 [HltsQ1 Hl']]]]. destruct A'; inverts Hf'2. destruct l'; inverts Hl'.
    asserts_rewrite (S n0 -1 = n0). omega.
    ∃ a (conc_new C'2) (nu P'2)(nu Q'2). splits; auto with hopi howe.
    eapply lts_new'; eauto. simpl; fsetdec.
    eauto with sc. eauto with sc.
Qed.

Lemma pseudo_out_first {V:Set}: ∀ Rel (P1 Q1:proc V)(P2 Q2:proc1) a C1
  (f:V → proc0), simulation Rel → refl Rel →
  rename_compatible Rel → (Rincl sc0 Rel) → trans Rel →
  howe Rel P1 Q1 → howe Rel P2 Q2 →
  lts (bind f P1) (out a) (ag_conc C1) →
  ∃ C2 P'2 Q'2, lts (bind f Q1) (out a) (ag_conc C2) ∧
     sc0 P'2 (appr (abs_def P2) C1) ∧
     sc0 Q'2 (appr (abs_def Q2) C2) ∧ howe Rel P'2 Q'2.
Proof.
  introv Hsim Hrefl Hrename Hsc0 Htrans Hp1q1. gen a f C1 P2 Q2.
  induction Hp1q1; introv Hp2q2 HltsP1; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 Hp2q2 HltsP1.
    destruct H0 as [C2 [P'2 [Q'2 [Hltsc2 [Hp'2 [Hq'2 Hhowe]]]]]].
    forwards: H f; auto. unfold simulation in ×. remember (abs_def Q2) as F.
    forwards_test Rel. subst.
    ∃ C'0 P'2 (appr (abs_def Q2) C'0); intuition.
    apply howe_comp with Q'2; auto with hopi howe.
      apply oe_trans with (appr (abs_def Q2) C2); auto.
      apply× oe_sc0. apply× oe_proc0.
  - simpl in ×.
    ∃ C1 (appr (abs_def P2) C1)(appr (abs_def Q2) C1);
                                          intuition auto with sc.
    destruct C1 as [n P Q]; simpl.
    apply howe_genNu. apply howe_par; auto with howe. apply howe_subst; auto with howe.
    apply howe_mapN; auto using shiftN_injective.
  - inverts HltsP1.
    + forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
      forwards*: IHHp1q1_1 Hp2q2 H2.
      destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
      ∃ (conc_parl C'2 (bind f Q')) (P'2// bind f P') (Q'2//bind f Q').
      splits; eauto with hopi howe.
      eapply lts_parl'; eauto.
      apply sc_trans with (appr (abs_def P2) C'1 // bind f P');
                                                        auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (appr (abs_def P2) C'1 // bind f P')
        (appr (abs_def P2) (conc_parl C'1 (bind f P')))).
        destruct C'1; simpl. eauto with sc.
      eauto with sc hopi howe.
      apply sc_trans with (appr (abs_def Q2) C'2 // bind f Q');
                                                        auto with sc hopi howe.
      assert (struct_congr
        (appr (abs_def Q2) C'2 // bind f Q')
        (appr (abs_def Q2) (conc_parl C'2 (bind f Q')))).
        destruct C'2; simpl. eauto with sc.
      eauto with sc hopi howe.
    + forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
      forwards*: IHHp1q1_2 Hp2q2 H2.
      destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
      ∃ (conc_parr (bind f Q) C'2) (bind f P // P'2) (bind f Q // Q'2).
      splits; eauto with hopi howe.
      eapply lts_parr'; eauto.
      apply sc_trans with (bind f P // appr (abs_def P2) C'1);
                                                      auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (bind f P // appr (abs_def P2) C'1)
        (appr (abs_def P2) (conc_parr (bind f P) C'1))).
        destruct C'1; simpl. apply sc_trans with
          (genNu n (shiftN n (bind f P) // (subst ((shiftN n) P2) p // p0))); eauto with sc.
      eauto with sc hopi howe.
      apply sc_trans with (bind f Q // appr (abs_def Q2) C'2); auto with sc hopi howe.
      assert (struct_congr (bind f Q // appr (abs_def Q2) C'2)
                   (appr (abs_def Q2) (conc_parr (bind f Q) C'2))).
        destruct C'2; simpl. apply sc_trans with
          (genNu n (shiftN n (bind f Q) // (subst ((shiftN n) Q2) p // p0))); eauto with sc.
      eauto with sc hopi howe.
  - inverts HltsP1. simpl.
    ∃ (conc_def 0 (bind f Q) (bind f Q'))
        (appr (abs_def P2) (conc_def 0 (bind f P) (bind f P')))
        (appr (abs_def Q2) (conc_def 0 (bind f Q) (bind f Q')));
    simpl; intuition auto with hopi sc.
    apply howe_par; auto with howe. apply howe_subst; auto with howe.
    apply howe_mapN; auto.
  - simpl in ×. inverts HltsP1. destruct l0; inverts H0. destruct A as [ | | C1' ]; inverts H1.
    forwards*: @howe_mapN Hp2q2 S.
    forwards*: IHHp1q1 H H3. destruct H0 as [C2' [P'2 [Q'2 [HltsC2' [Hp'2 [HQ'2 Hrel]]]]]].
    ∃ (conc_new C2') (nu P'2) (nu Q'2). splits. eapply lts_new'; eauto.
    remember (abs_def P2) as F1. asserts_rewrite (abs_def (mapN S P2) = fmapN S F1) in Hp'2. subst; reflexivity.
    eauto with sc.
    remember (abs_def Q2) as F2. asserts_rewrite (abs_def (mapN S Q2) = fmapN S F2) in HQ'2. subst; reflexivity.
    eauto with sc.
    auto with howe.
Qed.

Lemma pseudo_sim_in : pseudo_sim.
Proof.
  introv Hsim Hrefl Hrename Hsc0 Htrans Hp2q2 Hp1q1. gen a f g F1 C1 P2 Q2.
  induction Hp1q1; introv Hp2q2 HltsP1 HltsP2; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 a F1 C1 P2 Q2.
    destruct H0 as [F2 [C2 [ P'2 [R' [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]].
    forwards*: H f. unfold simulation in ×.
    assert (conc_wf C2). forwards*: lts_conc_wf HltsR.
    forwards_test Rel.
    ∃ F'0 C2 P'2 (appr F'0 C2); intuition.
    apply howe_comp with R'; auto with hopi howe.
      apply oe_trans with (appr F2 C2); auto.
      apply× oe_sc0. apply× oe_proc0.
  - simpl in ×. destruct F1 as [P'1].
    forwards: @pseudo_out_first P2 Q2 P'1 P'1 C1; eauto with howe hopi.
    destruct H as [C2 [ P'2 [Q'2 [HltsC2 [Hp'2 [Hq'2 Hhowe]]]]]].
    ∃ (abs_def P'1) C2 P'2 Q'2; intuition.
  - inverts HltsP1.
    + forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
      forwards*: IHHp1q1_1 Hp2q2 H2 HltsP2.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      ∃ (abs_parl F'2 (bind f Q')) C'2 (P'2// bind f P') (Q'2//bind f Q').
      splits; eauto with hopi howe.
      eapply lts_parl'; eauto.
      apply sc_trans with (appr F'1 C1 // bind f P'); auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (appr F'1 C1 // bind f P') (appr (abs_parl F'1 (bind f P')) C1)).
        destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
        apply sc_trans with
          (genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f P'))); eauto with sc.
      eauto with sc hopi howe.
      apply sc_trans with (appr F'2 C'2 // bind f Q'); auto with sc hopi howe.
      assert (struct_congr
        (appr F'2 C'2 // bind f Q') (appr (abs_parl F'2 (bind f Q')) C'2)).
        destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
        apply sc_trans with
          (genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f Q'))); eauto with sc.
      eauto with sc hopi howe.
    + forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
      forwards*: IHHp1q1_2 Hp2q2 H2 HltsP2.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      ∃ (abs_parr (bind f Q) F'2) C'2 (bind f P // P'2) (bind f Q // Q'2).
      splits; eauto with hopi howe.
      eapply lts_parr'; eauto.
      apply sc_trans with (bind f P // appr F'1 C1); auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (bind f P // appr F'1 C1) (appr (abs_parr (bind f P) F'1) C1)).
        destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
      apply sc_trans with
          (genNu n (shiftN n (bind f P) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      eauto with sc hopi howe.
      apply sc_trans with (bind f Q // appr F'2 C'2); auto with sc hopi howe.
      assert (struct_congr (bind f Q // appr F'2 C'2)
                            (appr (abs_parr (bind f Q) F'2) C'2)).
        destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
      apply sc_trans with
          (genNu n (shiftN n (bind f Q) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      eauto with sc hopi howe.
  - inverts HltsP1. simpl. forwards*: @pseudo_out_first Rel P2 Q2 (bind (liftV f) P)(bind (liftV f) Q).
      apply× @howe_bind. intros [|]; simpl; auto with howe.
    destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
    ∃ (abs_def (bind (liftV f) Q)) C'2 P'2 Q'2; intuition.
  - simpl in ×. inverts HltsP1. destruct A as [ | F1' | ]; inverts H1. destruct l0; inverts H0.
    simpl in H2. destruct_notin. forwards*: mapN_lts S HltsP2. simpl in H. rewrite bind_mapN in H.
    asserts_rewrite (S (n-1) = n) in H. omega. forwards*: @howe_mapN Hp2q2 S.
    forwards*: IHHp1q1 H0 H. destruct H1 as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
    rewrite <- bind_mapN in HltsC'2. apply mapN_lts_rev in HltsC'2; try (intros_all; omega).
    destruct HltsC'2 as [A' [l' [Hc'2 [HltsQ2 Hl']]]]. destruct A'; inverts Hc'2. destruct l'; inverts Hl'.
    asserts_rewrite (S n0 -1 = n0). omega.
    ∃ (abs_new F'2) c (nu P'2)(nu Q'2). splits; auto with hopi howe.
    eapply lts_new'; eauto. simpl; fsetdec. eauto with sc.
    eauto with sc.
Qed.

Lemma pseudo_sim_sim' :
  (∀ {V W:Set} Rel (P1 Q1:proc V)(P2 Q2:proc W) a F1 C1 (f:V → proc0)(g: W → proc0) n1 n2,
   simulation Rel → refl Rel → rename_compatible Rel → (Rincl sc0 Rel) → trans Rel
   → howe' Rel P2 Q2 n2 → howe' Rel P1 Q1 n1
   → lts (bind f P1) (inp a) (ag_abs F1) → lts (bind g P2) (out a) (ag_conc C1)
   → ∃ F2 C2 P'2 Q'2 n3, lts (bind f Q1) (inp a) (ag_abs F2) ∧
                               lts (bind g Q2) (out a) (ag_conc C2) ∧
                               sc0 P'2 (appr F1 C1) ∧
                               sc0 Q'2 (appr F2 C2) ∧
                               howe' Rel P'2 Q'2 n3).
Proof.
  introv Hsim Hrefl Hrename Hsc0 Htrans.
  Require Import TLC.LibWf.
  assert (wf (lexico2 lt lt)).
    rewrite <- LibNat.lt_peano.
    apply wf_lexico2; auto with wf.
  remember (n2, n1) as p. gen V W.
  gen n1 n2 a F1 C1.
  induction_wf IH: H p. intros n1 n2 Hp. subst.
  assert (∀ (V2 : Set) a (P1 Q1 : proc1) (n1 : nat) (P2 Q2 : proc V2),
     howe' Rel P1 Q1 n1
     → howe' Rel P2 Q2 n2
         → ∀ (g : V2 → proc0) (C1 : conc),
              lts (bind g P2) (out a) C1
                 → ∃ (C2:conc) P'2 Q'2 x3,
                     lts (bind g Q2) (out a) C2
                   ∧ sc0 P'2 (appr (abs_def P1) C1)
                   ∧ sc0 Q'2 (appr (abs_def Q1) C2) ∧ howe' Rel P'2 Q'2 x3).
  { intros.
    assert (howe' Rel (a? P1) (a? Q1)(S n0)) by auto with howe.
    remember (pr_var (V:=Empty_set)) as f.
    assert (∀ P, bind (liftV f) P = P).
      intros; rewrite× @bind_return. intros [|]; simpl; auto.
      intros. inverts e.
    destruct H1; try solve [inverts H2].
    - forwards*: IH (k, S n0) f; try solve [subst; simpl; eauto with hopi].
      destruct_hyps. specialize (H5 g). unfold simulation in ×.
      forwards_test Rel. inverts H6. rewrite H4 in ×.
      ∃ C'0 x1 (appr (abs_def Q1) C'0)(S x3); intuition.
        apply howe_comp' with x2; auto with hopi howe.
        apply oe_trans with (appr (abs_def Q1) x0); auto.
        apply× oe_sc0. apply× oe_proc0.
    - simpl in ×.
      assert (∃ n3, howe' Rel (appr (abs_def P1) C1) (appr (abs_def Q1) C1) n3).
        destruct C1 as [n P Q]; simpl. apply howe_implies_howe'.
        apply howe_genNu. apply howe_par; auto with howe. apply howe_subst; auto with howe.
        apply howe_mapN; auto with howe. eapply howe'_implies_howe; eauto.
      destruct H1. ∃ C1 (appr (abs_def P1) C1)(appr (abs_def Q1) C1) x0;
      intuition auto with sc.
  - inverts H2.
    + forwards: lts_out_conc H7. destruct H1 as [C'1].
      rewrite_all H1 in *; clear H1. simpl in H8.
      forwards*: IH f H3 H7; try solve [subst; simpl; eauto with hopi].
        apply lexico2_1. omega.
      destruct H1 as [ F2 [ C'2 [P'2 [Q'2 [ n3 [ HltsF2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
      inverts HltsF2. rewrite H4 in ×.
      assert (∃ n4, howe' Rel (P'2// bind g P') (Q'2//bind g Q') n4).
        apply× @howe_implies_howe'. apply howe'_implies_howe in H1_0.
        apply howe'_implies_howe in Hhowe. apply× @howe_par. apply× @howe_bind.
        intros; auto with howe hopi.
      destruct H1. ∃ (conc_parl C'2 (bind g Q')) (P'2// bind g P') (Q'2//bind g Q') x.
      splits; eauto with hopi howe.
      eapply lts_parl'; eauto.
      apply sc_trans with (appr (abs_def P1) C'1 // bind g P');
                                                        auto with sc hopi howe.
      inverts H8. assert (struct_congr
        (appr (abs_def P1) C'1 // bind g P')
        (appr (abs_def P1) (conc_parl C'1 (bind g P')))).
        destruct C'1; simpl. eauto with sc.
      eauto with sc hopi howe.
      apply sc_trans with (appr (abs_def Q1) C'2 // bind g Q');
                                                        auto with sc hopi howe.
      assert (struct_congr
        (appr (abs_def Q1) C'2 // bind g Q')
        (appr (abs_def Q1) (conc_parl C'2 (bind g Q')))).
        destruct C'2; simpl. eauto with sc.
      eauto with sc hopi howe.
    + forwards: lts_out_conc H7. destruct H1 as [C'1].
      rewrite_all H1 in *; clear H1. simpl in H8.
      forwards*: IH f H1_0 H7; try solve [subst; simpl; eauto with hopi].
        apply lexico2_1. omega.
      destruct H1 as [ F2 [ C'2 [P'2 [Q'2 [ n3 [ HltsF2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
      inverts HltsF2. rewrite H4 in ×.
      assert (∃ n4, howe' Rel (bind g P // P'2) (bind g Q // Q'2) n4).
        apply× @howe_implies_howe'. apply howe'_implies_howe in H1_.
        apply howe'_implies_howe in Hhowe. apply× @howe_par. apply× @howe_bind.
        intros; auto with howe hopi.
      destruct H1. ∃ (conc_parr (bind g Q) C'2) (bind g P // P'2) (bind g Q // Q'2) x.
      splits; eauto with hopi howe. eapply lts_parr'; eauto.
      apply sc_trans with (bind g P // appr (abs_def P1) C'1); auto with sc hopi howe.
      assert (struct_congr (bind g P // appr (abs_def P1) C'1)
                           (appr (abs_def P1) (conc_parr (bind g P) C'1))).
        destruct C'1; simpl. apply sc_trans with
          (genNu n (shiftN n (bind g P) // (subst ((shiftN n) P1) p // p0))); eauto with sc.
      inverts H8. eauto with sc hopi howe.
      apply sc_trans with (bind g Q // appr (abs_def Q1) C'2); auto with sc hopi howe.
      assert (struct_congr (bind g Q // appr (abs_def Q1) C'2)
                   (appr (abs_def Q1) (conc_parr (bind g Q) C'2))).
        destruct C'2; simpl. apply sc_trans with
          (genNu n (shiftN n (bind g Q) // (subst ((shiftN n) Q1) p // p0))); eauto with sc.
      eauto with sc hopi howe.
  - inverts H2. simpl.
    assert (∃ n, howe' Rel (appr (abs_def P1) (conc_def 0 (bind g P) (bind g P')))
        (appr (abs_def Q1) (conc_def 0 (bind g Q) (bind g Q'))) n).
      apply× @howe_implies_howe'. simpl. apply howe'_implies_howe in H1_.
      apply howe'_implies_howe in H1_0. apply howe'_implies_howe in H0.
      apply howe_par; auto with howe. apply howe_subst; auto with howe.
       apply howe_mapN; auto with howe.
    destruct H1. ∃ (conc_def 0 (bind g Q) (bind g Q'))
        (appr (abs_def P1) (conc_def 0 (bind g P) (bind g P')))
        (appr (abs_def Q1) (conc_def 0 (bind g Q) (bind g Q'))) x;
    intuition auto with hopi sc.
  - simpl in ×. inverts H2. destruct l0; inverts H6. destruct A as [ | | C1' ]; inverts H7.
    forwards*: @howe'_mapN H3 S. simpl in H8. destruct_notin.
    simpl in H2. asserts_rewrite (S (n-1) = n) in H2. destruct n; omega.
    forwards*: IH f H1 H2.
      apply lexico2_1. omega.
      subst. rewrite bind_return'. apply lts_inp.
    destruct H5 as [F2 [C2' [P'2 [Q'2 [n3 [HltsF2 [HltsC2' [Hp'2 [HQ'2 Hrel]]]]]]]]].
    ∃ (conc_new C2') (nu P'2) (nu Q'2)(S n3). splits. eapply lts_new'; eauto. simpl; fsetdec.
    remember (abs_def P1) as F1. asserts_rewrite (abs_def (mapN S P1) = fmapN S F1) in Hp'2. subst; reflexivity.
    eauto with sc.
    remember (abs_def Q1) as F'2. inverts HltsF2. rewrite H4 in ×.
    asserts_rewrite (abs_def (mapN S Q1) = fmapN S F'2) in HQ'2. subst; reflexivity.
    eauto with sc. auto with howe.
    }
  intros. destruct H2; try solve [inverts H3].
  + forwards*: IH H1 H3; try solve [simpl; eauto with hopi].
    destruct H6 as [F2 [C2 [ P'2 [R' [n3 [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]]].
    forwards*: H5 f. unfold simulation in ×. assert (conc_wf C2). forwards*: lts_conc_wf HltsR.
    forwards_test Rel.
    assert (∃ n, howe' Rel P'2 (appr F'0 C2) n).
      apply× @howe_implies_howe'. apply howe'_implies_howe in HhoweP1R.
      apply howe_comp with R'; auto with hopi howe.
      apply oe_trans with (appr F2 C2); auto.
      apply× oe_sc0. apply× oe_proc0.
    destruct H13. ∃ F'0 C2 P'2 (appr F'0 C2) x; intuition.
  + simpl in ×. destruct F1 as [P1'].
    assert (∃ n1, howe' Rel P1' P1' n1).
      apply howe_implies_howe'; auto with howe hopi.
    destruct H2. forwards*: H0 H2 H1 H4. destruct_hyps.
    do 5 eexists; intuition (try eassumption).
  + inverts H3.
    - forwards: lts_inp_abs H7. destruct H2 as [F'1]. subst. simpl in H8.
      forwards*: IH H1 H2_; try solve [simpl; eauto with hopi].
        apply lexico2_2; omega.
      destruct H2 as [F'2 [ C'2 [P'2 [Q'2 [n3 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
      assert (∃ n4, howe' Rel (P'2 // bind f P') (Q'2 // bind f Q') n4).
        apply× @howe_implies_howe'. apply howe'_implies_howe in H2_0.
        apply howe'_implies_howe in Hhowe. auto with hopi howe.
      destruct H2. ∃ (abs_parl F'2 (bind f Q')) C'2 (P'2// bind f P') (Q'2//bind f Q') x.
      splits; eauto with hopi howe.
      eapply lts_parl'; eauto.
      apply sc_trans with (appr F'1 C1 // bind f P'); auto with sc hopi howe.
      inverts H8. assert (struct_congr
        (appr F'1 C1 // bind f P') (appr (abs_parl F'1 (bind f P')) C1)).
        destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
        apply sc_trans with
          (genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f P'))); eauto with sc.
      eauto with sc hopi howe.
      apply sc_trans with (appr F'2 C'2 // bind f Q'); auto with sc hopi howe.
      assert (struct_congr
        (appr F'2 C'2 // bind f Q') (appr (abs_parl F'2 (bind f Q')) C'2)).
        destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
        apply sc_trans with
          (genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f Q'))); eauto with sc.
      eauto with sc hopi howe.
    - forwards: lts_inp_abs H7. destruct H2 as [F'1]. subst. simpl in H8.
      forwards*: IH H1 H2_0; try solve [simpl; eauto with hopi].
        apply lexico2_2; omega.
      destruct H2 as [F'2 [ C'2 [P'2 [Q'2 [n3 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
      assert (∃ n4, howe' Rel (bind f P // P'2) (bind f Q // Q'2) n4).
        apply× @howe_implies_howe'. apply howe'_implies_howe in H2_.
        apply howe'_implies_howe in Hhowe. auto with hopi howe.
      destruct H2. ∃ (abs_parr (bind f Q) F'2) C'2 (bind f P // P'2) (bind f Q // Q'2) x.
      splits; eauto with hopi howe.
      eapply lts_parr'; eauto.
      apply sc_trans with (bind f P // appr F'1 C1); auto with sc hopi howe.
      inverts H8. assert (struct_congr
        (bind f P // appr F'1 C1) (appr (abs_parr (bind f P) F'1) C1)).
        destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
      apply sc_trans with
          (genNu n (shiftN n (bind f P) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      eauto with sc hopi howe.
      apply sc_trans with (bind f Q // appr F'2 C'2); auto with sc hopi howe.
      assert (struct_congr (bind f Q // appr F'2 C'2)
                            (appr (abs_parr (bind f Q) F'2) C'2)).
        destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
      apply sc_trans with
          (genNu n (shiftN n (bind f Q) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      eauto with sc hopi howe.
  + inverts H3. assert (∃ n1, howe' Rel (bind (liftV f) P)(bind (liftV f) Q) n1).
      apply× @howe_implies_howe'. apply× @howe_bind. apply× @howe'_implies_howe.
      intros [|]; simpl; auto with howe.
    destruct H3. forwards*: H0 H3 H1. destruct_hyps.
    do 5 eexists; intuition (try eassumption).
    simpl. auto with hopi.
  + simpl in ×. inverts H3. destruct A as [ | F1' | ]; inverts H7. destruct l0; inverts H6.
    simpl in H8. destruct_notin. forwards*: mapN_lts S H4. simpl in H3. rewrite bind_mapN in H3.
    asserts_rewrite (S (n-1) = n) in H3. omega. forwards*: @howe'_mapN H1 S.
    forwards*: IH H5 H9 H3. apply lexico2_2; omega.
    destruct H6 as [F'2 [ C'2 [P'2 [Q'2 [n3 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
    rewrite <- bind_mapN in HltsC'2. apply mapN_lts_rev in HltsC'2; try (intros_all; omega).
    destruct HltsC'2 as [A' [l' [Hc'2 [HltsQ2 Hl']]]]. destruct A'; inverts Hc'2. destruct l'; inverts Hl'.
    asserts_rewrite (S n0 -1 = n0). omega.
    ∃ (abs_new F'2) c (nu P'2)(nu Q'2)(S n3). splits; auto with hopi howe.
    eapply lts_new'; eauto. simpl; fsetdec. eauto with sc.
    eauto with sc.
Qed.

Lemma pseudo_sim_sim : pseudo_sim.
Proof.
  intros. apply howe_implies_howe' in H3; auto.
  apply howe_implies_howe' in H4; auto. destruct H3, H4.
  forwards*: @pseudo_sim_sim' H2 H3; try eassumption. destruct_hyps.
  apply howe'_implies_howe in H11. do 4 eexists; intuition eassumption.
Qed.

Notation lpseudo_sim := pseudo_sim_in .

Lemma pseudo_tau {V:Set}: ∀ Rel (P Q:proc V) P'
  (f:V → proc0), simulation Rel → refl Rel → rename_compatible Rel →
  (Rincl sc0 Rel) → trans Rel → howe Rel P Q →
  lts (bind f P) tau (ag_proc P') →
  ∃ Q' P'' Q'', lts (bind f Q) tau (ag_proc Q') ∧
                sc0 P' P'' ∧ sc0 Q' Q'' ∧ howe Rel P'' Q''.
Proof.
  introv Hsim Hrefl Hrename Hincl Htrans Hp1q1. gen f P'.
  induction Hp1q1; introv HltsP1; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 P'.
    destruct H0 as [R' [P'' [R'' [HltsR [Hp'p'' [Hr'r'' HhoweP1R]]]]]].
    forwards: H f; auto. unfold simulation in ×. forwards_test Rel.
    ∃ Q'0 P'' Q'0; intuition.
    apply howe_comp with R''; auto with hopi howe.
      apply oe_trans with R'; auto. apply oe_sc0; auto with sc. apply× oe_proc0.
  - ∃ P' P' P'; intuition.
  - inverts HltsP1.
    + forwards: lts_tau_proc H2. destruct H as [P'1]. subst. simpl in H3.
      forwards: IHHp1q1_1 H2; auto.
      destruct H as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
      ∃ (Q'1 // (bind f Q')) (P''1 // (bind f P')) (Q''1 // (bind f Q')).
      inverts H3. splits; auto with sc howe hopi.
      eapply lts_parl'; eauto.
    + forwards: lts_tau_proc H2. destruct H as [P'1]. subst. simpl in H3.
      forwards: IHHp1q1_2 H2; auto.
      destruct H as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
      ∃ ((bind f Q) // Q'1) ((bind f P) // P''1) ((bind f Q) // Q''1).
      inverts H3. splits; auto with sc howe hopi.
      eapply lts_parr'; eauto.
    + forwards: lpseudo_sim H3 H2; eauto.
      destruct H as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
      ∃ (appl C2 F2) P'2 Q'2. splits; eauto.
      eapply lts_taul'; eauto.
      apply sc_trans with (appr F C); auto with sc.
      apply sc_trans with (appr F2 C2); auto with sc.
    + forwards: lpseudo_sim H2 H3; eauto.
      destruct H as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
      ∃ (appr F2 C2) P'2 Q'2. splits; eauto with sc.
      eapply lts_taur'; eauto.
  - inverts HltsP1. destruct A as [ P'1 | [] | [] ]; inverts H1. destruct l0; inverts H0.
    forwards*: IHHp1q1 H3. destruct H as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
    ∃ (nu Q'1) (nu P''1) (nu Q''1); intuition eauto with hopi sc howe. simpl. eapply lts_new'; eauto.
Qed.

Lemma conc_to_proc : ∀ (C:conc) a, conc_wf C →
    ∃ P, lts P (out a) C ∧
        (∀ (C':conc), lts P (out a) C' → C = C').
Proof.
  intros. destruct C as [n P1 P2]. gen a P1 P2. induction n; intros.
  + ∃ (a!(P1) P2); intuition; auto with hopi. inverts H0. auto.
  + forwards*:IHn (S a) P1 P2. destruct H0 as [P' [Hlts Hc']].
    assert (n \in fn P1). apply H. omega.
    ∃ (nu P'). splits.
    - eapply lts_new'; eauto. simpl; fsetdec.
      simpl. case_if; auto. simpl; auto with arith.
    - intros. inverts H1. destruct A as [ | | C'']; inverts H4. destruct l0; inverts H3.
      simpl in H5. destruct_notin. asserts_rewrite (S(n0-1) = n0) in ×. omega.
      forwards*: Hc' H6. rewrite <- H1; simpl. case_if; auto.
Qed.

Lemma abs_to_proc : ∀ (F:abs) a,
    ∃ P, lts P (inp a) F ∧
        (∀ (F':abs), lts P (inp a) F' → F = F').
Proof.
  intros. destruct F as [P]. ∃ (a? P); splits*; auto with hopi.
  intros. inverts× H.
Qed.

Lemma simulation_up_to_sc_howe : ∀ Rel, simulation Rel → refl Rel → rename_compatible Rel →
  (Rincl sc0 Rel) → trans Rel → simulation_up_to_sc (howe Rel).
Proof.
  intros_all. splits; intros.
  + replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
    forwards: @pseudo_tau H3; eauto with hopi.
    destruct H5 as [Q' [P'' [Q'' [HltsQ' [Hpp'' [Hq'q'' Hhowe]]]]]].
    replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ' by (rewrite× bind_proc0).
    ∃ Q'. split×. do 2 (eexists; intuition eauto with sc).
  + replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
    forwards*: conc_to_proc C a. destruct H6 as [R [Hlts Hc']].
    assert (howe Rel R R) by apply× @howe_refl.
    replace R with (bind (pr_var (V:=Empty_set)) R) in Hlts by (rewrite× bind_proc0).
    forwards: lpseudo_sim H6 H3; eauto with hopi.
    destruct H7 as [F2 [C2 [P'2 [Q'2 [HltsQ [HltsR [Hpp'' [Hq'q'' Hhowe]]]]]]]].
    replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ by (rewrite× bind_proc0).
    replace (bind (pr_var (V:=Empty_set)) R) with R in HltsR by (rewrite× bind_proc0).
    forwards*: Hc' HltsR. subst. eexists; intuition eauto with sc.
    ∃ P'2; intuition eauto with sc. eexists; intuition eauto with sc.
  + replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
    forwards*: abs_to_proc F a. destruct H5 as [R [Hlts Hf']].
    assert (howe Rel R R) by apply× @howe_refl.
    replace R with (bind (pr_var (V:=Empty_set)) R) in Hlts by (rewrite× bind_proc0).
    forwards: lpseudo_sim H3 H5; eauto with hopi.
    destruct H6 as [F2 [C2 [P'2 [Q'2 [HltsR [HltsQ [Hpp'' [Hq'q'' Hhowe]]]]]]]].
    replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ by (rewrite× bind_proc0).
    replace (bind (pr_var (V:=Empty_set)) R) with R in HltsR by (rewrite× bind_proc0).
    forwards*: Hf' HltsR. subst. eexists; intuition eauto with sc.
    ∃ P'2; intuition eauto with sc. eexists; intuition eauto with sc.
Qed.

Lemma Rincl_sc0_howe : ∀ Rel, (Rincl sc0 Rel) → Rincl sc0 (howe Rel).
Proof.
  intros_all. apply howe_comp with x; auto with sc howe.
  apply× oe_proc0.
Qed.

Lemma bisimulation_tclos_howe : ∀ Rel, simulation Rel → refl Rel
   → rename_compatible Rel → (Rincl sc0 Rel) → trans Rel → sym Rel
   → bisimulation (tclosure (howe Rel)).
Proof.
  intros. rename H3 into Hsym. apply sim_sym_imply_bisim.
  ×
    intros. assert (Rincl sc0 (tclosure (howe Rel))).
      intros_all. apply× tclosure_once. apply× Rincl_sc0_howe.
    intros_all. induction H4.
    + forwards*: simulation_up_to_sc_howe Rel.
      specialize (H5 x y H4).
      splits; intros; forwards_test (sc0° (howe Rel) ° sc0); destruct_comp;
      repeat (eexists; intuition (try eassumption)); intuition;
      repeat (match goal with
        | H1: Rincl sc0 (tclosure (howe Rel)),
          H2: sc0 _ _ |- _ ⇒ apply H1 in H2 end); eauto with howe.
    + splits; intros; forwards_test (tclosure (@howe Empty_set Rel)); clear H4_;
      forwards_test (tclosure (@howe Empty_set Rel)); destruct_comp;
        repeat (eexists; intuition (try eassumption)); intuition eauto with howe.
 × apply× @howe_sym.
Qed.

Theorem bisimilarity_howe : bisimilarity = howe bisimilarity.
Proof.
  apply binary_ext; split.
  - intros. assert (Hbisim:=H). unfold bisimilarity in H. destruct H. destruct H.
    apply howe_comp with x; auto with bisim. apply howe_refl; auto with bisim.
    apply× oe_proc0.
  - intros. ∃ (tclosure (@howe Empty_set bisimilarity)).
    split. apply bisimulation_tclos_howe; auto using bisim_sym, bisim_trans, bisim_refl,
      bisim_rename_compatible.
      forwards*: bisim_is_bisimulation; intuition.
      intros_all; apply bisim_refl.
      intros_all. ∃ sc0. intuition. apply struct_congr_bisim.
      apply× tclosure_once.
Qed.