Require Import HOcore.Prelim.

Require Import HOcore.ComplLat
               HOcore.HoCore
               HOcore.Compat
               HOcore.CondClos
               HOcore.Ren
               HOcore.Subst
               HOcore.Bis
               HOcore.BisDecInjRen
               HOcore.BisSubstit
               HOcore.BisCongr
               HOcore.UpToNu.

Lemma s_io_cxt_sym_closed_under_decidable_inj_ren:
  congruence s_io_cxt_sym decidable_inj_ren_clos.
Proof.
  apply compat_impl_congruence.
  eapply intersect_fun_bin_preserv_compat.
Qed.

(* auxiliary lemma, stating an obvious fact *)
Lemma nu_of_s_io_cxt_sym_is_closed_under_var_bis_f:
  postfp (symmetrize_fun s_var_cxt) (nu s_io_cxt_sym).
Proof.
  intros p q [x [H1 H2]].
  split.
  - destruct (H1 p q H2) as [[_ H3] _].
    eapply s_var_cxt_mono; eauto.
    repeat intro. exists x. split; auto.
    (* analog *)
  - destruct (H1 p q H2) as [_ [_ H3]].
    eapply s_var_cxt_mono; eauto.
    repeat intro. exists x. split; auto.
Qed.

Lemma s_io_cxt_sym_substit:
  congruence s_io_cxt_sym subst_clos.
Proof.
  eapply cond_clos_impl_congruence.
    Focus 2. apply nu_of_s_io_cxt_sym_is_closed_under_var_bis_f.
    Focus 2. apply preserv_monoid_refl_impl_nu_is_reflexive'.
    Focus 1.
      apply symmetrize_fun_preserv_cond_clos_when_f_sym.
      eapply intersect_fun_bin_preserv_cond_clos.
      Unshelve.
      - eapply intersect_fun_bin_preserv_cond_clos.
        Unshelve.
        + eapply decreasing_g_up_preserv_cond_clos.
            Focus 2. exact ho_out_substit_cond_clos.
            Focus 1. repeat intro. cbv in *. intuition.
        + eapply decreasing_g_up_preserv_cond_clos.
          Focus 2.
            eapply increasing_g_lo_preserv_cond_clos.
            Focus 2. exact ho_in_substit_cond_clos.
            Focus 1. repeat intro. contradiction.
          Focus 1. repeat intro. cbv in *. intuition.
      - eapply decreasing_g_up_preserv_cond_clos.
          Focus 2.
            eapply increasing_g_lo_preserv_cond_clos.
              Focus 2. exact var_substit_cond_clos.
              Focus 1. repeat intro. now hnf.
          Focus 1. repeat intro. cbv in *. intuition.
Qed.

Lemma send_clos_congruent_for_s_io_cxt_sym:
  congruence s_io_cxt_sym send_clos.
Proof.
  eapply cond_clos_of_increasing_impl_congruence
    with (g_lo := refl_clos)
         (g_up := const top2).
  Focus 2. intros p q H1.
    now apply preserv_monoid_refl_impl_nu_is_reflexive'.
  Focus 2. now hnf.
  Focus 1.
    eapply symmetrize_fun_preserv_cond_clos_when_f_sym.
    eapply intersect_fun_bin_preserv_cond_clos.
    Unshelve.
    - eapply intersect_fun_bin_preserv_cond_clos.
      Unshelve.
      eapply increasing_g_lo_preserv_cond_clos.
        Focus 2. eapply congr_cond_clos_impl_cond_clos.
        Focus 1. repeat intro; now hnf.
    - eapply increasing_g_lo_preserv_cond_clos.
      Focus 2. eapply congr_cond_clos_impl_cond_clos.
      Focus 1. repeat intro; now hnf.
Qed.

Lemma receive_clos_congruent_for_s_io_cxt_sym:
  congruence s_io_cxt_sym receive_clos.
Proof.
  eapply cond_clos_of_increasing_impl_congruence
    with (g_lo := const bot2) (g_up := const top2).
  Focus 2. now hnf.
  Focus 2. now hnf.
  Focus 1.
    eapply symmetrize_fun_preserv_cond_clos_when_f_sym.
    eapply intersect_fun_bin_preserv_cond_clos.
Qed.

Lemma par_clos_congruent_for_s_io_cxt_sym:
  congruence s_io_cxt_sym par_clos.
Proof.
  eapply cond_clos_of_increasing_impl_congruence
    with (g_lo := decidable_inj_ren_clos) (g_up := const top2).
  Focus 2. intros p q H1.
    now apply s_io_cxt_sym_closed_under_decidable_inj_ren.
  Focus 2. now hnf.
  Focus 1.
    eapply symmetrize_fun_preserv_cond_clos_when_f_sym.
    eapply intersect_fun_bin_preserv_cond_clos.
    Unshelve.
    - eapply intersect_fun_bin_preserv_cond_clos.
      Unshelve.
      + eapply increasing_g_lo_preserv_cond_clos.
        Focus 2. eapply congr_cond_clos_impl_cond_clos.
        Focus 1. repeat intro. contradiction.
Qed.

Definition multi_context_clos
  (x: relation process): relation process :=
  fun p q => exists sigma tau C,
    (forall n, x (sigma n) (tau n)) /\
    p = instantiate' sigma C /\
    q = instantiate' tau C.

Lemma multi_congr_s_io_cxt_sym:
  congruence s_io_cxt_sym multi_context_clos.
Proof.
  intros p q [sigma [tau [C [H1 [H2 H3]]]]]. subst.
  revert sigma tau H1.
  induction C; intros sigma tau H1.
  - simpl. apply send_clos_congruent_for_s_io_cxt_sym.
    do 3 eexists. repeat split. now apply IHC.
  - simpl. apply receive_clos_congruent_for_s_io_cxt_sym.
    do 3 eexists. repeat split. now apply IHC.
  - simpl. apply H1.
  - simpl. apply par_clos_congruent_for_s_io_cxt_sym.
    exists (instantiate' sigma C1), (instantiate' tau C1), (instantiate' sigma C2), (instantiate' tau C2).
    repeat split.
    + now apply IHC1.
    + now apply IHC2.
  - now apply preserv_monoid_refl_impl_nu_is_reflexive'.
Qed.

Definition context_clos
  (x: relation process): relation process :=
  fun p q => exists p' q' C, x p' q' /\
                             p = instantiate' (p' .: ids) C /\
                             q = instantiate' (q' .: ids) C.

Lemma context_clos_congruent_for_s_io_cxt_sym:
  congruence s_io_cxt_sym context_clos.
Proof.
  intros p q H1.
  apply multi_congr_s_io_cxt_sym.
  hnf in H1. decompose [ex and] H1. clear H1. subst.
  do 3 eexists. repeat split.
  intros n. destruct n.
  - exact H0.
  - simpl. apply preserv_monoid_refl_impl_nu_is_reflexive'.
    now hnf.
Qed.

Lemma up_to_io_bisimilarity_sound:
  sound s_io_cxt_sym (up_to_nu s_io_cxt_sym).
Proof.
  apply compat_impl_sound.
  - eapply symmetrize_fun_preserv_mono.
  - apply up_to_nu_f_is_nu_f_compat.
Qed.