Require Import HOcore.Prelim.

Require Import HOcore.ComplLat.

Section Compat.

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

  Class Compat
    (s f: relation T -> relation T): Prop :=
    cond_compat: forall x y,
      x <2= s y ->
      f x <2= s (f y).

  (* The identity function is compatible *)
  Global Instance id_compat
    {s: relation T -> relation T}:
    Compat s id.
  Proof.
    repeat intro. eauto.
  Qed.

  (* Constant-to-x functions are compatible *)
  Global Instance const_to_postfp_compat
    {s: relation T -> relation T}
    (x: relation T)
    (H1: postfp s x):
    Compat s (const x).
  Proof.
    repeat intro. now apply H1.
  Qed.

  (* Function composition preserves compatibility *)
  Lemma compose_preserv_compat
    {s: relation T -> relation T}
    {f: relation T -> relation T}
    {f_compat: Compat s f}
    {g: relation T -> relation T}
    (g_compat: Compat s g): (* explicit *)
    Compat s (f °° g).
  Proof.
    intros x y H1 p q H5.
    eapply f_compat.
    Focus 2. exact H5.
    - now apply g_compat.
  Qed.

  Global Instance union_fun_bin_preserv_compat
    {s: relation T -> relation T} {s_mono: Mono s}
    (f1 f2: relation T -> relation T) (* explicit *)
    (H1: Compat s f1)
    (H2: Compat s f2):
    Compat s (f1 \2/^ f2).
  Proof.
    intros x y H4 p q [H7 | H7].
    - eapply s_mono.
      + eapply H1; eauto.
      + repeat intro. now left.
    - eapply s_mono.
      + eapply H2; eauto.
      + repeat intro. now right.
  Qed.

  Global Instance intersect_fun_bin_preserv_compat
    {f: relation T -> relation T}
    {s1 s2: relation T -> relation T} (* explicit *)
    {H1: Compat s1 f}
    {H2: Compat s2 f}:
    Compat (s1 /2\^ s2) f.
  Proof.
    intros x y H4 p q H7.
    split.
    - eapply H1.
      + intros p' q' H8. specialize (H4 p' q' H8). now destruct H4.
      + auto.
    - eapply H2.
      + intros p' q' H8. specialize (H4 p' q' H8). now destruct H4.
      + auto.
  Qed.

  Global Instance transp_fun_bin_preserv_compat
    {s: relation T -> relation T}
    {f: relation T -> relation T}
    (H1: Compat s f): (* explicit *)
    Compat (transp_fun s) (transp_fun f).
  Proof.
    intros x y H2 p q H6.
    eapply H1.
    - repeat intro. apply H2. exact PR.
    - auto.
  Qed.

  Global Instance transp_fun_preserv_compat_when_f_sym
    {s: relation T -> relation T} {s_mono: Mono s}
    {f: relation T -> relation T} {f_sym: SymFun f}
    {H1: Compat s f}: (* explicit *)
    Compat (transp_fun s) f.
  Proof.
    intros x y H2 p q H6.
    apply transp_fun_bin_preserv_compat in H1.
    eapply transp_fun_preserv_mono.
      Focus 2. apply f_sym.
      Focus 1.
        eapply H1.
        - repeat intro. apply H2. eauto.
        - now erewrite <- (f_sym _ p q).
  Qed.

  Global Instance symmetrize_fun_preserv_compat_when_f_sym
    {s: relation T -> relation T} {s_mono: Mono s}
    {f: relation T -> relation T} {f_sym: SymFun f}
    (H1: Compat s f): (* explicit *)
    Compat (symmetrize_fun s) f.
  Proof.
    apply intersect_fun_bin_preserv_compat; auto.
  Qed.

  (* Prop. 1.15 (iii)
     For any s-compatible maps f, g, if s preserves transitivity, then f °^ g is s-compatible *)
  Global Instance preserv_trans_impl_rel_comp_fun_preserv_compat
    {s: relation T -> relation T} {s_mono: Mono s}
    {s_preserv_monoid_trans: PreservMonoidTrans s}
    {f: relation T -> relation T}
    {g: relation T -> relation T}
    {H1: Compat s f}
    {H2: Compat s g}:
    Compat s (f °^ g).
  Proof.
    intros x y H4 p q H8.
    apply s_preserv_monoid_trans.
    eapply rel_comp_mono.
    - repeat intro. eapply H1; eauto.
    - repeat intro. eapply H2; eauto.
    - auto.
  Qed.

  (* Showing Compat justifies congruence. *)
  Lemma compat_impl_congruence
    {s: relation T -> relation T} {s_mono: Mono s}
    {f: relation T -> relation T}
    (H1: Compat s f):
    congruence s f.
  Proof.
    intros p q H4.
    exists (f (nu s)). split; auto.
    intros p' q' H5.
    eapply H1.
    Focus 2. eauto.
    - repeat intro. now apply nu_is_postfp.
  Qed.

  (* For (not necessarily monotone) f, Compat f implies Compat monotonize(f). *)
  Lemma monotonize_compat
    {s: relation T -> relation T} {s_mono: Mono s}
    {f: relation T -> relation T}
    (H1: Compat s f):
    Compat s (monotonize f).
  Proof.
    intros x y H2 p q [z [H5 H6]].
    eapply s_mono.
    Focus 2. apply monotonize_extensive.
    Focus 1. eapply H1.
        Focus 2. exact H6.
        - repeat intro. apply H2. now apply H5.
  Qed.

  Section CompatImplSound.

    Context (s: relation T -> relation T)
            {s_mono: Mono s}.

    (* Companion *)
    Definition companion: relation T -> relation T :=
      fun x p q => exists f,
        Compat s f /\ Mono f /\ f x p q.

    (* Companion is monotone *)
    Global Instance companion_mono:
      Mono companion.
    Proof.
      intros p q x y [f [H1 [H2 H3]]] H4.
      exists f. repeat split; auto.
      eapply H2; eauto.
    Qed.

  (* Companion is compatible *)
    Global Instance companion_compat:
      Compat s companion.
    Proof.
      intros x y H1 p q [f [H4 [H5 H6]]].
      eapply s_mono.
      - eapply H4; eauto.
      - repeat intro. now exists f.
    Qed.

    (* Companion is semi-idempotent *)
    Lemma companion_semi_idemp:
      forall x, companion (companion x) <2= companion x.
    Proof.
      intros x p q [f [H1 [H2 H3]]].
      exists (f °° companion). repeat split; auto.
      - eapply compose_preserv_compat.
        eapply companion_compat.
      - apply compose_preserv_mono.
    Qed.

    (* Companion is correct *)
    Lemma companion_correct:
      correct s companion.
    Proof.
      intros p q H1.
      destruct H1 as [x [H1 H2]].
      exists (companion x). split.
      - intros p' q' [f [H3 [H4 H5]]].
        eapply s_mono.
        Focus 2. apply companion_semi_idemp.
        Focus 1.
          eapply companion_compat.
          Focus 2.
            eapply companion_mono.
              exists f. repeat split; auto. exact H5.
              exact H1.
          Focus 1. now repeat intro.
      - exists id. repeat split; auto.
        + apply id_compat.
        + apply id_mono.
    Qed.

    (* Companion is sound *)
    Lemma companion_sound:
      sound s companion.
    Proof.
      intros x H1 p q H2.
      apply companion_correct.
      exists x. now split.
    Qed.

    Lemma compat_impl_sound
      {f: relation T -> relation T}
      {H1: Compat s f}:
      sound s f.
    Proof.
      intros x H2 p q H3.
      eapply companion_sound.
      Focus 2. exact H3.
      Focus 1. repeat intro. eapply s_mono.
      - now apply H2.
      - repeat intro. exists (monotonize f). repeat split.
        + now apply monotonize_compat.
        + apply monotonized_mono.
        + now apply monotonize_extensive.
    Qed.

  End CompatImplSound.

End Compat.