Require Import HOcore.Prelim.

Require Import HOcore.ComplLat.

Section CondClos.

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

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

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

  (* Constant-to-x functions are conditionally closed *)
  Global Instance const_to_postfp_cond_clos
    {s: relation T -> relation T}
    {g1 g2: relation T -> relation T}
    (x: relation T)
    (H1: postfp s x):
    CondClos s (const x) g1 g2.
  Proof.
    repeat intro. now apply H1.
  Qed.

  (* Weaken CondClos by increasing g_lo *)
  Global Instance increasing_g_lo_preserv_cond_clos
    {s: relation T -> relation T}
    {f: relation T -> relation T}
    {g_lo1: relation T -> relation T}
    {g_up: relation T -> relation T}
    (g_lo2: relation T -> relation T) (* explicit *)
    (H1: g_lo1 <2=^ g_lo2)
    (H2: CondClos s f g_lo1 g_up):
    CondClos s f g_lo2 g_up.
  Proof.
    repeat intro.
    eapply H2; eauto.
  Qed.

  (* Weaken CondClos by decreasing g_up *)
  Global Instance decreasing_g_up_preserv_cond_clos
    {s: relation T -> relation T}
    {f: relation T -> relation T}
    {g_lo: relation T -> relation T}
    {g_up1: relation T -> relation T}
    (g_up2: relation T -> relation T) (* explicit *)
    (H1: g_up2 <2=^ g_up1)
    (H2: CondClos s f g_lo g_up1):
    CondClos s f g_lo g_up2.
  Proof.
    repeat intro.
    eapply H2; eauto.
  Qed.

  Global Instance union_fun_bin_preserv_cond_clos
    {s: relation T -> relation T} {s_mono: Mono s}
    {g_lo: relation T -> relation T}
    {g_up: relation T -> relation T}
    (f1 f2: relation T -> relation T) (* explicit *)
    (H1: CondClos s f1 g_lo g_up)
    (H2: CondClos s f2 g_lo g_up):
    CondClos s (f1 \2/^ f2) g_lo g_up.
  Proof.
    intros x H3 H4 H5 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_cond_clos
    {f: relation T -> relation T}
    {g_lo: relation T -> relation T}
    {g_up: relation T -> relation T}
    {s1 s2: relation T -> relation T} (* explicit *)
    {H1: CondClos s1 f g_up g_lo}
    {H2: CondClos s2 f g_up g_lo}:
    CondClos (s1 /2\^ s2) f g_up g_lo.
  Proof.
    intros x H3 H4 H5 p q H7.
    split.
    - eapply H1; eauto.
      intros p' q' H8. specialize (H5 p' q' H8). now destruct H5.
    - eapply H2; eauto.
      intros p' q' H8. specialize (H5 p' q' H8). now destruct H5.
  Qed.

  Global Instance transp_fun_bin_preserv_cond_clos
    {s: relation T -> relation T}
    {f: relation T -> relation T}
    {g_lo: relation T -> relation T}
    {g_up: relation T -> relation T}
    (H1: CondClos s f g_lo g_up): (* explicit *)
    CondClos (transp_fun s) (transp_fun f) (transp_fun g_lo) (transp_fun g_up).
  Proof.
    intros x H2 H3 H4 p q H6.
    unfold CondClos in H1.
    eapply H1.
    - repeat intro. apply H2. exact PR.
    - repeat intro. eapply H3. exact PR.
    - repeat intro. now apply H4.
    - auto.
  Qed.

  Global Instance transp_fun_preserv_cond_clos_when_f_sym
    {s: relation T -> relation T} {s_mono: Mono s}
    {f: relation T -> relation T} {f_sym: SymFun f}
    {g_lo: relation T -> relation T} {g_lo_sym: SymFun g_lo}
    {g_up: relation T -> relation T} {g_up_sym: SymFun g_up}
    {H1: CondClos s f g_up g_lo}: (* explicit *)
    CondClos (transp_fun s) f g_up g_lo.
  Proof.
    intros x H2 H3 H4 p q H6.
    apply transp_fun_bin_preserv_cond_clos in H1.
    eapply transp_fun_preserv_mono.
      Focus 2. apply f_sym.
      Focus 1.
        eapply H1.
        - repeat intro. apply H2. apply g_up_sym. eauto.
        - repeat intro. apply g_lo_sym. now apply H3.
        - repeat intro. now apply H4.
        - now erewrite <- (f_sym _ p q).
  Qed.

  Global Instance symmetrize_fun_preserv_cond_clos_when_f_sym
    {s: relation T -> relation T} {s_mono: Mono s}
    {f: relation T -> relation T} {f_sym: SymFun f}
    {g_lo: relation T -> relation T} {g_lo_sym: SymFun g_lo}
    {g_up: relation T -> relation T} {g_up_sym: SymFun g_up}
    (H1: CondClos s f g_lo g_up): (* explicit *)
    CondClos (symmetrize_fun s) f g_lo g_up.
  Proof.
    apply intersect_fun_bin_preserv_cond_clos; 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_cond_clos
    {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}
    {g_lo g_up: relation T -> relation T}
    {H1: CondClos s f g_lo g_up}
    {H2: CondClos s g g_lo g_up}:
    CondClos s (f °^ g) g_lo g_up.
  Proof.
    intros x H4 H5 H6 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 CondClos and fulfillment of the conditions justifies congruence. *)
  Lemma cond_clos_impl_congruence
    {s: relation T -> relation T} {s_mono: Mono s}
    {f: relation T -> relation T}
    (g_lo: relation T -> relation T)
    (g_up: relation T -> relation T)
    (H1: CondClos s f g_lo g_up)
    (H2: postfp g_up (nu s))
    (H3: prefp g_lo (nu s)):
    congruence s f.
  Proof.
    intros p q H4.
    exists (f (nu s)). split; auto.
    intros p' q' H5.
    eapply H1.
    Focus 4. eauto.
    - auto.
    - auto.
    - repeat intro. now apply nu_is_postfp.
  Qed.

End CondClos.