Require Import HOcore.Prelim.

Require Import HOcore.ComplLat
               HOcore.Compat.

Section UpToNu.

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

  Definition up_to_nu
    (f: relation T -> relation T):
    relation T -> relation T :=
    (const (nu f)) °^ id °^ (const (nu f)).

  Global Instance up_to_nu_preserv_mono
    {f: relation T -> relation T}
    {f_mono: Mono f}:
    Mono (up_to_nu f).
  Proof.
    unfold up_to_nu.
    eapply rel_comp_fun_preserv_mono.
  Qed.

  Global Instance up_to_nu_preserv_symmetric_fun
    {f: relation T -> relation T}
    {f_mono: Mono f}
    {f_sym: SymFun f}:
    SymFun (up_to_nu f).
  Proof.
    intros x p q. split.
    - intros H2.
      destruct H2 as [p' [H2 [p'' [H3 H4]]]].
      unfold transp_fun, "°°". unfold transp at 1.
      exists p''. split.
      + unfold const. unfold const in H4.
        now eapply sym_f_impl_sym_nu.
      + exists p'. split; auto.
        unfold const. unfold const in H2.
        now eapply sym_f_impl_sym_nu.
    - intros H2.
      unfold transp_fun, "°°" in H2. unfold transp at 1 in H2.
      destruct H2 as [q' [H2 [q'' [H3 H4]]]].
      exists q''. split.
      + unfold const in H4. unfold const.
        now eapply sym_f_impl_sym_nu.
      + exists q'. split; auto.
        now eapply sym_f_impl_sym_nu.
  Qed.

  Global Instance up_to_nu_f_is_nu_f_compat
    {f: relation T -> relation T} {f_mono: Mono f}
    {H1: PreservMonoidTrans f}:
    Compat (symmetrize_fun f) (up_to_nu (symmetrize_fun f)).
  Proof.
    unfold up_to_nu.
    eapply preserv_trans_impl_rel_comp_fun_preserv_compat.
    Unshelve.
    - apply const_to_postfp_compat. apply nu_is_postfp.
    - eapply preserv_trans_impl_rel_comp_fun_preserv_compat.
      Unshelve.
      apply const_to_postfp_compat. apply nu_is_postfp.
  Qed.

End UpToNu.