Require Import HOcore.Prelim.

Require Import HOcore.ComplLat
               HOcore.CondClos
               HOcore.HoCore
               HOcore.Multiset
               HOcore.Ren
               HOcore.Bis.

Definition send_clos
  (x: relation process): relation process :=
  fun p q => exists p' q' a, x p' q' /\
                             p = Send a p' /\
                             q = Send a q'.

Global Instance send_clos_mono: Mono send_clos.
Proof.
  intros p q x x' H1 H2.
  unfold send_clos in H1. decompose [ex and] H1.
  clear H1. subst. repeat eexists; eauto.
Qed.

Global Instance send_clos_sym:
  SymFun send_clos.
Proof.
  intros x p q. split; intros H1.
  - hnf in H1. decompose [ex and] H1. clear H1.
    subst. repeat eexists. eauto.
  - hnf in H1. decompose [ex and] H1. clear H1.
    subst. repeat eexists. eauto.
Qed.

Definition receive_clos
  (x: relation process): relation process :=
  fun p q => exists p' q' a, x p' q' /\
                             p = Receive a p' /\
                             q = Receive a q'.

Instance receive_clos_mono: Mono receive_clos.
Proof.
  intros p q x x' H1 H2.
  hnf in H1. decompose [ex and] H1; clear H1.
  repeat eexists; eauto.
Qed.

Global Instance receive_clos_sym:
  SymFun receive_clos.
Proof.
  intros x p q. split; intros H1.
  - hnf in H1. decompose [ex and] H1. clear H1. subst.
    repeat eexists; eauto.
  - hnf in H1. decompose [ex and] H1. clear H1. subst.
    repeat eexists; eauto.
Qed.

Definition par_clos
  (x: relation process): relation process :=
  fun p q => exists p1 q1 p2 q2, x p1 q1 /\
                                 x p2 q2 /\
                                 p = Par p1 p2 /\
                                 q = Par q1 q2.

Instance par_clos_mono: Mono par_clos.
Proof.
  intros p q x x' H1 H2.
  hnf in H1. decompose [ex and] H1. clear H1. subst.
  repeat eexists; eauto.
Qed.

Global Instance par_clos_sym:
  SymFun par_clos.
Proof.
  intros x p q.
  split; intros H1; hnf in H1; decompose [ex and] H1; subst;
  now repeat eexists.
Qed.

(* When showing CondClos for the increasing version of the closure, we get a slightly stronger result. Because the first part of the increasing function (identity) is trivial, we do not show it every time and use the following notion, which is strong enough to let the proof go through but as weak as possible. *)

Section CongrCondClos.

  (* Type of binary relation *)
  Context {T: Type}.

  Class CongrCondClos
    (s f g_lo g_up: relation T -> relation T): Prop :=
    congr_cond_clos: forall x,
      g_lo x <2= x ->
      x <2= g_up x ->
      x <2= s x ->
      f x <2= s (increasify f x).

  (* Strengthen CongrCondResp *)
  Global Instance congr_cond_clos_impl_cond_clos
    {s: relation T -> relation T} {s_mono: Mono s}
    {f g_lo g_up: relation T -> relation T}
    {H1: CongrCondClos s f g_lo g_up}:
    CondClos s (increasify f) g_lo g_up.
  Proof.
    intros x H2 H32 H4 p q [H5 | H5].
    - eapply H1; eauto.
    - eapply s_mono.
        Focus 2. repeat intro. right. eauto.
        Focus 1. now apply H4.
  Qed.

  (* The strengthened version implies congruence *)
  Lemma cond_clos_of_increasing_impl_congruence
    {s: relation T -> relation T} {s_mono: Mono s}
    {f: relation T -> relation T} {f_mono: Mono f}
    (g_up g_lo: relation T -> relation T)
    (H1: CondClos s (increasify f) g_lo g_up)
    (H2: prefp g_lo (nu s))
    (H3: postfp g_up (nu s)):
    congruence s f.
  Proof.
    intros p q H4.
    eapply cond_clos_impl_congruence.
      Focus 3. exact H2.
      Focus 2. exact H3.
      - eauto.
      - now left.
  Qed.

End CongrCondClos.

Global Instance s_ho_out_fulfills_cond_compat_for_send_clos:
  CongrCondClos
    s_ho_out
    send_clos
    refl_clos
    (const top2).
Proof.
  intros x H1 H2 H3 p q H4 a p'' p' H5.
  destruct H4 as [p2' [q2' H4]].
  decompose [ex and] H4; clear H4; subst.
  inv H5.
  exists q2', Nil. repeat split; auto.
  - right. now apply H1. (* need reflexivity *)
  - now right.
Qed.

Global Instance s_ho_in_fulfills_cond_compat_for_send_clos:
  CongrCondClos
    s_ho_in
    send_clos
    (const bot2)
    (const top2).
Proof.
  intros x H11 p q H1 p' a H2.
  ainv.
Qed.

Global Instance s_var_cxt_fulfills_cond_compat_for_send_clos:
  CongrCondClos
    s_var_cxt
    send_clos
    (const bot2)
    (const top2).
Proof.
  intros x H1 H2 H3 p' q' H4.
  destruct H4 as [p [q [a [H5 [H6 H7]]]]]. subst.
  intros v p' H6. inv H6.
Qed.

Global Instance s_var_multi_fulfills_cond_compat_for_send_clos:
  CongrCondClos
    s_var_multi
    send_clos
    (const bot2)
    (const top2).
Proof.
  intros x H1 H2 H3 p q H4.
  destruct H4 as [p' [q' [a [H5 [H6 H7]]]]]. subst.
  - cbv. auto.
Qed.

Global Instance s_ho_out_fulfills_cond_compat_for_receive_clos:
  CongrCondClos
    s_ho_out
    receive_clos
    (const bot2)
    (const top2).
Proof.
  repeat intro. ainv.
Qed.

Global Instance s_ho_in_fulfills_cond_compat_for_receive_clos:
  CongrCondClos
    s_ho_in
    receive_clos
    (const bot2)
    (const top2).
Proof.
  intros x H11 H1 H2 p q H3 p' a H4.
  unfold receive_clos, "°°", decreasify, "/2\^" in H3.
  decompose [ex and] H3; clear H3. subst.
  inv H4.
  eexists. repeat split; auto.
  now right.
Qed.

Global Instance s_var_cxt_fulfills_cond_compat_for_receive_clos:
  CongrCondClos
    s_var_cxt
    receive_clos
    (const bot2)
    (const top2).
Proof.
  repeat intro. unfold receive_clos, "°°" in *. ainv.
Qed.

Global Instance s_var_multi_fulfills_cond_compat_for_receive_clos:
  CongrCondClos
    s_var_multi
    receive_clos
    (const bot2)
    (const top2).
Proof.
  intros x H1 H2 H3 p q H4.
  destruct H4 as [p' [q' [a [H5 [H6 H7]]]]]. subst.
  - cbv. auto.
Qed.

Global Instance s_ho_out_fulfills_cond_compat_for_par_clos:
  CongrCondClos
    s_ho_out
    par_clos
    (const bot2)
    (const top2).
Proof.
  intros x H1 H2 H3 p q H4.
  destruct H4 as [p1 [q1 [p2 [q2 [H5 [H6 [H7 H8]]]]]]]. subst.
  intros a p'' p H7.
  inv H7.
  (* p1 process does a step *)
  + destruct (H3 p1 q1 H5 a p'' p' H10) as [q'' [q' [H8 [H9 H11]]]].
    exists q'', (Par q' q2). repeat split; auto.
    * left. exists p', q', p2, q2. repeat split; auto.
    * now right.
  (* p2 process does a step *)
  + rename q' into p'.
    destruct (H3 p2 q2 H6 a p'' p' H10) as [q'' [q' [H8 [H9 H11]]]].
    exists q'', (Par q1 q'). repeat split; auto.
    * left. exists p1, q1, p', q'. repeat split; auto.
    * now right.
Qed.

Global Instance s_ho_in_fulfills_cond_compat_for_par_clos:
  CongrCondClos
    s_ho_in
    par_clos
    decidable_inj_ren_clos
    (const top2).
Proof.
  intros x H1 H2 H3 p q H4.
  destruct H4 as [p1 [q1 [p2 [q2 [H5 [H6 [H7 H8]]]]]]]. subst.
  intros a p H4.
  inv H4.
  (* p1 process does a step *)
  - destruct (H3 p1 q1 H5 a p' H8) as [q' [H9 H10]].
    exists (Par q' q2.[ren (+1)]). repeat split.
    + eapply StInParL; eauto.
    + left.
      repeat eexists; auto.
      apply H1. exists (+1), minus_one, p2, q2. (* need dec_inj_ren_clos *)
      split.
      * apply shift_decidable_inj_ren.
      * repeat split; auto.
  (* p2 process does a step (analog) *)
  - rename q' into p'.
    destruct (H3 p2 q2 H6 a p' H8) as [q' [H9 H10]].
    exists (Par q1.[ren (+1)] q'). repeat split.
    + eapply StInParR; eauto.
    + left.
      repeat eexists; auto.
      apply H1. exists (+1), minus_one, p1, q1. (* need dec_inj_ren_clos *)
      split.
      * apply shift_decidable_inj_ren.
      * repeat split; auto.
Qed.

Global Instance s_var_cxt_fulfills_cond_compat_for_par_clos:
  CongrCondClos
    s_var_cxt
    par_clos
    decidable_inj_ren_clos
    (const top2).
Proof.
  intros x H1 H2 H3 p q H4.
  destruct H4 as [p1 [q1 [p2 [q2 [H5 [H6 [H7 H8]]]]]]]. subst.
  intros n p2' H7. inv H7.
  (* p1 process does a step *)
  - destruct (H3 p1 q1 H5 n p' H8) as [q' [H9 H10]].
    exists (Par q' q2.[ren (+1)]). repeat split; eauto.
    left. repeat eexists; auto.
    apply H1. do 4 eexists.
    split.
    + apply shift_decidable_inj_ren.
    + repeat split. auto.
  (* p2 process does a step (analog) *)
  - rename q' into p'.
    destruct (H3 p2 q2 H6 n p' H8) as [q' [H9 H10]].
    exists (Par q1.[ren (+1)] q'). repeat split; eauto.
    left. repeat eexists; auto.
    apply H1. do 4 eexists. split.
    + apply shift_decidable_inj_ren.
    + repeat split. auto.
Qed.

Global Instance s_var_multi_fulfills_cond_compat_for_par_clos:
  CongrCondClos
    s_var_multi
    par_clos
    decidable_inj_ren_clos
    (const top2).
Proof.
  intros x H1 H2 H3 p q H4.
  destruct H4 as [p1 [q1 [p2 [q2 [H5 [H6 [H7 H8]]]]]]]. subst.
  - simpl.
    intros n. simpl.
    do 2 rewrite union_mult.
    assert (H31: forall x0 x1 : process, x x0 x1 -> s_var_multi x x0 x1) by auto.
    specialize (H3 p1 q1 H5 n).
    specialize (H31 p2 q2 H6 n).
    omega.
Qed.