HOcore.ComplLat

Require Import HOcore.Prelim.

Require Import Coq.Classes.Equivalence
               Coq.Classes.Morphisms.

This file contains elementary definitions and lemmas about the complete lattice of binary relations over a type T

Section CompleteLattice.

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

Monotonicity


  (* Notation as used in Paco Library (http://plv.mpi-sws.org/paco/) *)
  Definition monotone2 (f: relation T -> relation T): Prop :=
    forall (p q: T) (r r' : relation T),
      f r p q ->
      (forall (p' q': T), (r p' q' : Prop) -> r' p' q' : Prop) -> f r' p q.

  (* Monotonicity *)
  Class Mono (f: relation T -> relation T): Prop :=
    mono: monotone2 f.

  (* Monotonicity is preserved when two monotone functions are composed *)
  Global Instance compose_preserv_mono
    {f: relation T -> relation T} {f_mono: Mono f}
    {g: relation T -> relation T} {g_mono: Mono g}:
    Mono (f °° g).
  Proof.
    repeat intro; eauto.
  Qed.

  (* Identity map is monotone *)
  Global Instance id_mono:
    Mono (@id (relation T)).
  Proof.
    repeat intro; eauto.
  Qed.

  (* Constant-to-x map is monotone *)
  Global Instance const_to_x_mono {x: relation T}:
    Mono (const x).
  Proof.
    repeat intro; eauto.
  Qed.

Relation inclusion


  (* Relation equivalence *)
  Definition rel_equiv (x y: relation T): Prop :=
    forall p q, x p q <-> y p q.
  Notation " x =2= y " := (rel_equiv x y) (at level 50, no associativity).

  Lemma rel_equiv_refl:
    reflexive rel_equiv.
  Proof.
    repeat intro. now split.
  Qed.

  Lemma rel_equiv_sym:
    symmetric rel_equiv.
  Proof.
    do 2 intro. intro H1. split; intro; now apply H1.
  Qed.

  Lemma rel_equiv_trans:
    transitive rel_equiv.
  Proof.
    do 3 intro. intros H1 H2. split; intro H3.
    - apply H2. now apply H1.
    - apply H1. now apply H2.
  Qed.

  (* rel_equiv is an equivalence relation *)
  Global Instance rel_equiv_equivalence:
    Equivalence rel_equiv.
  Proof.
    constructor; hnf.
    - apply rel_equiv_refl.
    - apply rel_equiv_sym.
    - apply rel_equiv_trans.
  Qed.

Pointwise extension of relation inclusion to functions


  (* Relation function inclusion: Pointwise extension of rel_incl to functions *)
  Definition rel_fun_incl (f g: relation T -> relation T): Prop :=
    forall x, f x <2= g x.
  Notation " x <2=^ y " := (rel_fun_incl x y) (at level 90, no associativity).

  (* Function inclusion is transitive *)
  Lemma rel_fun_incl_trans:
    transitive rel_fun_incl.
  Proof.
    hnf. repeat intro. eauto.
  Qed.

  (* Relation function equivalence: Pointwise extension of "=2=" to functions *)
  Definition rel_fun_equiv (f g: relation T -> relation T): Prop :=
    forall x, f x =2= g x.
  Notation " x =2=^ y " := (rel_fun_equiv x y) (at level 90, no associativity).

  Lemma rel_fun_equiv_refl:
    reflexive rel_fun_equiv.
  Proof.
    hnf. repeat intro. split; eauto.
  Qed.

  Lemma rel_fun_equiv_sym:
    symmetric rel_fun_equiv.
  Proof.
    intros f1 f2 H1. repeat intro; split; now apply H1.
  Qed.

  Lemma rel_fun_equiv_trans:
    transitive rel_fun_equiv.
  Proof.
    intros f1 f2 f3 H1 H2. repeat intro. split; intro.
    - apply H2. now apply H1.
    - apply H1. now apply H2.
  Qed.

  (* rel_fun_equiv is an equivalence relation *)
  Global Instance rel_fun_equiv_equivalence:
    Equivalence rel_fun_equiv.
  Proof.
    constructor; hnf.
    - apply rel_fun_equiv_refl.
    - apply rel_fun_equiv_sym.
    - apply rel_fun_equiv_trans.
  Qed.

Reflexive closure


  (* Constant to identity relation *)
  Definition refl_clos: relation T -> relation T :=
    fun _ => @identity T.

  (* refl_clos is monotone *)
  Global Instance refl_clos_mono:
    Mono refl_clos.
  Proof.
    hnf. eauto.
  Qed.

Union


  (* Union operator
     It implements the least upper bound operator of the complete lattice.
     The binary union operator (unifying two sets) is given by "\2/". *)

  Definition union (X: relation T -> Prop): relation T :=
    fun p q => exists x, X x /\ x p q.

  (* Union operators for functions:
     Pointwise extension of union to functions
     Not defined in terms of union operator, but directly with exists quantifier *)

  Definition union_fun
    (F: (relation T -> relation T) -> Prop):
    relation T -> relation T :=
    fun x => fun p q => exists f, F f /\ f x p q.

  (* A function which is in a set of functions if it is pointwisely included
    Pendant to intersect_fun_subset_member *)

  Lemma member_subset_union_fun
        (F: (relation T -> relation T) -> Prop)
        (f: relation T -> relation T):
    F f ->
    f <2=^ (union_fun F).
  Proof.
    repeat intro.
    unfold union_fun. exists f. split; auto.
  Qed.

  (* Binary union operator for functions: Pointwise extension of "\2/" to functions *)
  Definition union_fun_bin
    (f g: relation T -> relation T):
    relation T -> relation T :=
    fun x => fun p q => f x p q \/ g x p q.
  Notation " x \2/^ y " := (union_fun_bin x y) (at level 90, no associativity).

  (* Binary union operator for functions preserves monotonicity *)
  Global Instance union_fun_bin_preserv_mono
    {f: relation T -> relation T} {f_mono: Mono f}
    {g: relation T -> relation T} {g_mono: Mono g}:
    Mono (union_fun_bin f g).
  Proof.
    repeat intro. hnf in *. intuition.
    - left. eapply f_mono; eauto.
    - right. eapply g_mono; eauto.
  Qed.

Extensiveness


  Class Ext
    (s: relation T -> relation T): Prop :=
    ext: id <2=^ s.

  (* When a function is composed with another extensive function, it becomes greater *)
  Lemma compose_with_ext_is_superset
    {f: relation T -> relation T} {f_mono: Mono f}
    (g: relation T -> relation T):
    Ext g ->
    f <2=^ f °° g.
  Proof.
    intros H1 x p q H2; eauto.
  Qed.


(Pre-, Post-, Greatest) Fixed Points


  Definition prefp
    (s: relation T -> relation T)
    (x: relation T): Prop :=
    s x <2= x.

  Definition postfp
    (s: relation T -> relation T)
    (x: relation T): Prop :=
    x <2= s x.

  Definition nu
    (s: relation T -> relation T)
    (p q: T): Prop :=
    exists x,
      postfp s x /\ x p q.

  (* Properties of maps (= monotone functions *)
  Section Map.

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

    (* nu is a postfp itself *)
    Lemma nu_is_postfp:
      postfp s (nu s).
    Proof.
      unfold postfp. intros p q [x [H1 H2]].
      eapply s_mono.
      - now apply H1.
      - repeat intro. exists x. split; auto.
    Qed.

    Lemma nu_is_prefp:
      s (nu s) <2= nu s.
    Proof.
      intros p q H1.
      exists (s (nu s)). split; auto.
      intros p' q' H2.
      eapply s_mono.
      - exact H2.
      - apply nu_is_postfp.
    Qed.

    (* nu s is the greatest fixed-point of s *)
    Theorem knaster_tarski:
      forall x, prefp s x /\ postfp s x ->
        x <2= nu s.
    Proof.
      intros x [H1 H2] p q H3.
      exists x. split; auto.
    Qed.

    (* Any postfp is included in nu *)
    Lemma postfp_subset_nu:
      forall x, postfp s x -> x <2= nu s.
    Proof.
      intros x H1 p q H2. exists x. split; auto.
    Qed.

  End Map.

Congruence


  (* We use the term 'congruence' here for the closure property of a greatest fixed-point *)

  (* Functional s is congruent for closure f *)
  Definition congruence
    (s: relation T -> relation T)
    (f: relation T -> relation T): Prop :=
    f (nu s) <2= nu s.


Soundness and Correctness


  Definition sound
    (s: relation T -> relation T)
    (f: relation T -> relation T): Prop :=
    forall x,
      x <2= s (f x) -> x <2= nu s.

  Definition correct
    (s: relation T -> relation T)
    (f: relation T -> relation T): Prop :=
    nu (s °° f) <2= nu s.

  Lemma sound_impl_correct_for_mono
    (s: relation T -> relation T) (s_mono: Mono s)
    (f: relation T -> relation T) (f_mono: Mono f):
    sound s f -> correct s f.
  Proof.
    intros H1 p q H2. eapply H1.
    Focus 2. exact H2.
    Focus 1. do 2 intro. intros [x [H31 H32]].
      eapply s_mono.
      - now apply H31.
      - do 2 intro. intro H4. eapply f_mono.
        + exact H4.
        + do 3 intro. exists x. split; auto.
  Qed.

Intersection


  (* Definition of intersection
     It implements the greatest lower bound operator of the complete lattice *)

  Definition intersect
    (X: relation T -> Prop): relation T :=
    fun p q => forall x, X x -> x p q.

  (* Pointwise extension of intersections to functions *)
  Definition intersect_fun
    (F: (relation T -> relation T) -> Prop):
    relation T -> relation T :=
    fun x => fun p q => forall f, F f -> f x p q.

  (* A function which is in a set of functions is pointwise-included
     Pendant to member_subset_union_fun *)

  Lemma intersect_fun_subset_member
        (F: (relation T -> relation T) -> Prop)
        (f: relation T -> relation T):
    F f ->
    (intersect_fun F) <2=^ f.
  Proof.
    intros H1 x p q H2.
    now apply H2.
  Qed.

  (* Intersection of functions preserves monotonicity *)
  Definition intersect_fun_preserv_mono
    {F: (relation T -> relation T) -> Prop}
    {F_mono: forall f, F f -> Mono f}:
    Mono (intersect_fun F).
  Proof.
    intros p q x x' H1 H2 f H3.
    specialize (H1 f H3).
    eapply (F_mono f H3).
    - exact H1.
    - exact H2.
  Qed.

  (* Binary intersection operator *)
  Definition intersect_bin
    (x y: relation T):
    relation T :=
    fun p q => x p q /\ y p q.
  Notation " x /2\ y " := (intersect_bin x y) (at level 50, no associativity).

  (* Binary intersection function operator *)
  Definition intersect_fun_bin
    (f g: relation T -> relation T):
    relation T -> relation T :=
    fun x => fun p q => f x p q /\ g x p q.
  Notation " x /2\^ y " := (intersect_fun_bin x y) (at level 90, no associativity).

  Global Instance intersect_fun_bin_preserv_mono
    {f1: relation T -> relation T} {f1_mono: Mono f1}
    {f2: relation T -> relation T} {f2_mono: Mono f2}:
    Mono (f1 /2\^ f2).
  Proof.
    intros p q x x' [H31 H32] H4. split; eauto.
  Qed.

  Global Instance rel_fun_equiv_intersect_fun_bin_morphism:
    Proper (rel_fun_equiv ==> rel_fun_equiv ==> rel_fun_equiv) intersect_fun_bin.
  Proof.
    constructor; hnf; intros [H1 H2]; split;
    match goal with H : _ |- _ => now apply H end.
  Qed.

  (* Prop 1.8 (i)
     The postfps of /\S are exactly the intersection of
     the postfps of all s in S *)

  Lemma intersect_postfp_iff_postfp_in_every_member
    (S: (relation T -> relation T) -> Prop):
    forall x, postfp (intersect_fun S) x <->
              forall s, S s -> postfp s x.
  Proof.
    intros x. split.
    - intros H1 s H2 p q H3.
      specialize (H1 p q H3 s H2). exact H1.
    - intros H1 p q H2 s H3.
      now apply H1.
  Qed.

Transposition


  (* Transposition (inversion) of a relation is already defined: transp *)

  (* Relation transposition is monotone *)
  Global Instance transp_mono:
    Mono (@transp T).
  Proof.
    hnf. intuition.
  Qed.

  (* Inversion preserves relation inclusion: -> side *)
  Lemma rel_incl_impl_transp_rel_incl:
    forall x y,
      x <2= y -> @transp T x <2= transp y.
  Proof.
    intuition.
  Qed.

  (* Inversion preserves relation inclusion: <- side *)
  Lemma transp_rel_incl_impl_rel_incl:
    forall x y,
      @transp T x <2= transp y -> x <2= y.
  Proof.
    do 2 intro. intro H1. repeat intro. now apply H1.
  Qed.

  (* transp (union X) = union (transped X)
     <2= side *)

  Lemma transp_into_union
    (X: (relation T) -> Prop):
    forall p q,
      transp (union X) p q ->
      exists x, X x /\ transp x p q.
  Proof.
    do 2 intro. intros [x H1]. now exists x.
  Qed.

  (* =2> side *)
  Lemma union_into_transp
    (X: (relation T) -> Prop):
    forall p q,
      (exists x, X x /\ transp x p q) ->
      transp (union X) p q.
  Proof.
    do 2 intro. intros [x H1]. now exists x.
  Qed.

  (* Function which acts on the inversion of a relation *)
  Definition transp_fun
    (f: relation T -> relation T): relation T -> relation T :=
    @transp T °° f °° @transp T.

  (* Inversion of functions preserves their monotonicity *)
  Global Instance transp_fun_preserv_mono
    {f: relation T -> relation T}
    {mono_f: Mono f}:
    Mono (transp_fun f).
  Proof.
    intros p q x x' H2 H3.
    unfold transp_fun. unfold transp_fun in H2.
    eapply compose_preserv_mono.
    - exact H2.
    - exact H3.
  Qed.

  (* transp_fun distributes over intersect_fun_bin *)
  Lemma transp_fun_distributes_over_intersect_fun_bin
    (f1 f2: relation T -> relation T):
    (transp_fun (f1 /2\^ f2)) =2=^
    (transp_fun f1 /2\^ transp_fun f2).
  Proof.
    repeat intro. split; intro; eauto.
  Qed.

  Lemma transp_fun_distributes_over_compose
    (f1 f2: relation T -> relation T):
    (transp_fun (f1 °° f2)) =2=^
    (transp_fun f1) °° (transp_fun f2).
  Proof.
    repeat intro. split; eauto.
  Qed.

Symmetry


  (* symmetric is already defined *)

  Class SymFun (f: relation T -> relation T): Prop :=
    sym_fun: f =2=^ (transp_fun f).

  (* id is symmetric *)
  Global Instance id_sym:
    SymFun id.
  Proof.
    repeat intro. intuition eauto.
  Qed.

  Global Instance const_sym
    (x: relation T)
    (H1: symmetric x):
    SymFun (const x).
  Proof.
    repeat intro. split; intro; hnf; now apply H1.
  Qed.

  Global Instance const_bot2_sym:
    SymFun (const bot2).
  Proof.
    apply const_sym. hnf. eauto.
  Qed.

  Global Instance const_top2_sym:
    SymFun (const top2).
  Proof.
    apply const_sym. hnf. eauto.
  Qed.

  (* refl_clos is symmetric *)
  Global Instance refl_clos_sym:
    SymFun refl_clos.
  Proof.
    do 3 intro. split; intros H1; now destruct H1.
  Qed.

  Global Instance compose_preserv_symmetric_fun
    {f g: relation T -> relation T} {f_mono: Mono f}
    {f_sym: SymFun f}
    {g_sym: SymFun g}:
    SymFun (f °° g).
  Proof.
    intros x p q. split.
    - intros H3. unfold transp_fun, "°°". unfold transp at 1.
      unfold "°°" in H3.
      rewrite (f_sym (g x) p q) in H3.
      unfold transp_fun, "°°" in H3. unfold transp at 1 in H3.
      eapply f_mono; eauto.
      intros p' q' H4. unfold transp in H4.
      now rewrite <- (g_sym x q' p').
    - intros H3.
      unfold transp_fun, "°°" in H3.
      unfold transp in H3 at 1.
      apply f_sym. unfold transp_fun, "°°". unfold transp at 1.
      eapply f_mono; eauto.
      intros p' q' H4. unfold transp.
      apply g_sym. unfold transp_fun, "°°". unfold transp at 1.
      auto.
  Qed.

  Global Instance union_fun_bin_preserv_sym_fun
    {f1: relation T -> relation T} {f1_mono: Mono f1}
    {f2: relation T -> relation T} {f2_mono: Mono f2}
    {f1_sym: SymFun f1}
    {f2_sym: SymFun f2}:
    SymFun (f1 \2/^ f2).
  Proof.
    intros x p q. split; intros H1; destruct H1.
    - left. now apply f1_sym.
    - right. now apply f2_sym.
    - left. now apply f1_sym.
    - right. now apply f2_sym.
  Qed.

  Lemma sym_f_impl_sym_nu
    {f: relation T -> relation T} {f_mono: Mono f}:
    SymFun f ->
    symmetric (nu f).
  Proof.
    intros H1 p q H2.
    destruct H2 as [x [H2 H3]].
    exists (transp x). split; auto.
    intros p' q' H4.
    specialize (H2 q' p' H4).
    apply H1. unfold transp_fun, "°°". unfold transp at 1.
    eapply f_mono; eauto.
  Qed.

  (* Conjunction of a function f and (transp_fun f) *)
  Definition symmetrize_fun
    (f: relation T -> relation T): relation T -> relation T :=
    f /2\^ (transp_fun f).

  Global Instance symmetrize_fun_correct
    (f: relation T -> relation T):
    SymFun (symmetrize_fun f).
  Proof.
    unfold symmetrize_fun.
    split.
    - intros [H1 H2].
      apply transp_fun_distributes_over_intersect_fun_bin.
      split; auto.
    - intros H1.
      apply transp_fun_distributes_over_intersect_fun_bin in H1.
      destruct H1 as [H1 H2].
      split; auto.
  Qed.

  (* Symmetrization of a function preserves monotonicity *)
  Global Instance symmetrize_fun_preserv_mono
    {f: relation T -> relation T} {f_mono: Mono f}:
    Mono (symmetrize_fun f).
  Proof.
    intros p q x x' [H11 H12] H2.
    split.
    - eapply f_mono.
      + exact H11.
      + auto.
    - eapply f_mono.
      + exact H12.
      + repeat intro. intuition.
  Qed.

Relation composition


  (* Relation composition (associative product of monoid)
     The monoid's neutral element is @identity T *)

  Definition rel_comp (x y: relation T): relation T :=
    fun p q => exists p', x p p' /\ y p' q.
  Notation " x ° y " := (rel_comp x y) (at level 69, right associativity).

  (* Relation composition is monotone with respect to left operand *)
  Lemma rel_comp_mono_left:
    forall x x' y,
      x <2= x' ->
      (x ° y) <2= (x' ° y).
  Proof.
    intros x x' y H1 p q [p' [H2 H3]].
    exists p'. auto.
  Qed.

  (* Relation composition is monotone with respect to right operand *)
  Lemma rel_comp_mono_right:
    forall x y y',
      y <2= y' ->
      (x ° y) <2= (x ° y').
  Proof.
    intros x y y' H1 p q [p' [H2 H3]].
    exists p'. auto.
  Qed.

  (* Combination of rel_comp_mono_{left, right} *)
  Lemma rel_comp_mono:
    forall x x' y y',
      x <2= x' ->
      y <2= y' ->
      (x ° y) <2= (x' ° y').
  Proof.
    intros x x' y y' H1 H2 p q H3.
    eapply rel_comp_mono_left. apply H1.
    eapply rel_comp_mono_right. apply H2.
    exact H3.
  Qed.

  (* Equivalence, <- part *)
  Lemma rel_comp_into_transp:
    forall x y,
      ((transp x) ° (transp y)) <2= transp (y ° x).
  Proof.
    intros x y p q [p' [H1 H2]]. hnf. eauto.
  Qed.

  (* <- part *)
  Lemma transp_into_rel_comp:
    forall x y,
      transp (y ° x) <2= ((transp x) ° (transp y)).
  Proof.
    intros x y p q [p' [H1 H2]]. eexists. eauto.
  Qed.

  (* Composition of functions: Pointwise extension of rel_comp to functions *)
  Definition rel_comp_fun
    (f g: relation T -> relation T):
    relation T -> relation T :=
    fun x => (f x) ° (g x).
  Notation " x °^ y " := (rel_comp_fun x y) (at level 69, right associativity).

  (* Pointwise relation composition preserves monotonicity *)
  Global Instance rel_comp_fun_preserv_mono
    {f: relation T -> relation T} {f_mono: Mono f}
    {g: relation T -> relation T} {g_mono: Mono g}:
    Mono (f °^ g).
  Proof.
    intros p q x x' H1 H2.
    unfold "°^" in H1. unfold "°^".
    eapply rel_comp_mono.
    - intros p' q' H3.
      now apply (f_mono p' q' x x' H3).
    - intros p' q' H3.
      now apply (g_mono p' q' x x' H3).
    - exact H1.
  Qed.

Monoid preservation


  (* Function s preserves the monoid:
     Split into two properties:
     - preserv_monoid_refl
     - preserv_monoid_trans *)


  Class PreservMonoidRefl (s: relation T -> relation T): Prop :=
    preserv_monoid_refl: postfp s (@identity T).

  Class PreservMonoidTrans (s: relation T -> relation T): Prop :=
    preserv_monoid_trans: forall x y, (s x ° s y) <2= (s (x ° y)).

  Global Instance intersect_fun_bin_preserv_preserv_monoid_refl
    {s1 s2: relation T -> relation T}
    {H1: PreservMonoidRefl s1}
    {H2: PreservMonoidRefl s2}:
    PreservMonoidRefl (s1 /2\^ s2).
  Proof.
    intros p q H3. destruct H3. split; auto.
  Qed.

  Global Instance symmetrize_fun_preserv_preserv_monoid_refl
    {s: relation T -> relation T} {s_mono: Mono s}
    {H1: PreservMonoidRefl s}:
    PreservMonoidRefl (symmetrize_fun s).
  Proof.
    intros p q H2. destruct H2. split; auto.
    hnf. eapply s_mono.
    - now apply H1.
    - intuition.
  Qed.

  Global Instance intersect_fun_bin_preserv_preserv_monoid_trans
    {s1 s2: relation T -> relation T}
    {H1: PreservMonoidTrans s1}
    {H2: PreservMonoidTrans s2}:
    PreservMonoidTrans (s1 /2\^ s2).
  Proof.
    intros x y p q [p' [[H31 H32] [H41 H42]]].
    split.
    - apply H1. eexists. eauto.
    - apply H2. eexists. eauto.
  Qed.

  Global Instance symmetrize_fun_preserv_preserv_monoid_trans
    {s: relation T -> relation T} {s_mono: Mono s}
    {H1: PreservMonoidTrans s}:
    PreservMonoidTrans (symmetrize_fun s).
  Proof.
    intros x y p q [p' [[H21 H22] [H31 H32]]].
    split.
    - apply H1. eexists; eauto.
    - unfold transp_fun, "°°" in *.
      unfold transp at 1.
      eapply s_mono.
      + apply H1. eexists. eauto.
      + apply rel_comp_into_transp.
  Qed.

  (* Properties gained when s preserves the monoid *)
  Section PreservMonoidProperties.

    Context {s: relation T -> relation T}
            {s_mono: Mono s}
            {s_preserv_monoid_refl: PreservMonoidRefl s}
            {s_preserv_monoid_trans: PreservMonoidTrans s}.

    (* Prop. 1.15 *)
    (* Prop. 1.15 (i)
       If s preserves the monoid, then the product of two s-postfps is an s-postfp (rel_comp preserves s-postfp) *)

    Lemma preserv_monoid_trans_impl_rel_comp_preserv_postfp:
      forall x y,
        postfp s x ->
        postfp s y ->
        postfp s (x ° y).
    Proof.
      intros x y H2 H3 p q [p' [H4 H5]].
      apply s_preserv_monoid_trans. exists p'. split.
      - apply H2. exact H4.
      - apply H3. exact H5.
    Qed.

    (* Prop. 1.15 (ii)
       If s preserves the monoid, then s-nu is reflexive *)

    Lemma preserv_monoid_refl_impl_nu_is_reflexive:
      reflexive (nu s).
    Proof.
      intros p.
      eapply postfp_subset_nu.
      - exact s_preserv_monoid_refl.
      - constructor.
    Qed.

    (* Prop. 1.15 (ii)
       If s preserves the monoid, then s-nu is reflexive *)

    Lemma preserv_monoid_refl_impl_nu_is_reflexive':
      prefp refl_clos (nu s).
    Proof.
      intros p q H1. destruct H1.
      eapply postfp_subset_nu.
      - exact s_preserv_monoid_refl.
      - constructor.
    Qed.

    (* Prop. 1.15 (ii)
       If s preserves the monoid, then s-nu is transitive *)

    Lemma preserv_monoid_trans_impl_nu_is_transitive:
      transitive (nu s).
    Proof.
      intros p p' q H1 H2.
      eapply postfp_subset_nu.
      - eapply preserv_monoid_trans_impl_rel_comp_preserv_postfp.
        + now apply nu_is_postfp.
        + now apply nu_is_postfp.
      - exists p'. now split.
    Qed.

  End PreservMonoidProperties.


Decreasify


  (* Takes a function and makes it decreasing *)
  Definition decreasify
    (f: relation T -> relation T):
    relation T -> relation T :=
    f /2\^ id.

  Lemma decreasing_subset
    (f: relation T -> relation T):
    decreasify f <2=^ f.
  Proof.
    intros x p q [H1 H2]. auto.
  Qed.

  (* Decreasify is monotone *)
  Global Instance decreasify_preserv_mono
    {f: relation T -> relation T} {f_mono: Mono f}:
    Mono (decreasify f).
  Proof.
    intros p q x x' [H2 H3] H4. split; eauto.
  Qed.

Increasify


  (* Takes a function and makes it increasing *)
  Definition increasify
    (f: relation T -> relation T):
    relation T -> relation T :=
    f \2/^ id.

  Global Instance increasify_preserv_mono
    {f: relation T -> relation T} {f_mono: Mono f}:
    Mono (increasify f).
  Proof.
    intros p q x x' H1 H2.
    destruct H1.
    - left. eauto.
    - right. eauto.
  Qed.

  Global Instance increasify_preserv_sym
    {f: relation T -> relation T}
    {f_sym: SymFun f}:
    SymFun (increasify f).
  Proof.
    intros x p q. split; intros [H2 | H2].
    - left. apply f_sym. eauto.
    - right. auto.
    - left. apply f_sym in H2. auto.
    - right. auto.
  Qed.

  Global Instance increasify_impl_ext
    (f: relation T -> relation T):
    Ext (increasify f).
  Proof.
    intros x p q H1. now right.
  Qed.

  Global Instance compose_preserv_ext
    (f1 f2: relation T -> relation T):
    Ext f1 ->
    Ext f2 ->
    Ext (f1 °° f2).
  Proof.
    intros H1 H2 x p q H3.
    apply H1. now apply H2.
  Qed.

  Global Instance union_fun_bin_preserv_ext_left
    {f1: relation T -> relation T} {f1_ext: Ext f1}
    {f2: relation T -> relation T}:
    Ext (f1 \2/^ f2).
  Proof.
    intros x p q H1. left. now apply f1_ext.
  Qed.

Monotonization


  Definition monotonize (f: relation T -> relation T): relation T -> relation T :=
    fun x => fun p q => exists y, y <2= x /\ f y p q.

  Global Instance monotonized_mono:
    forall f, Mono (monotonize f).
  Proof.
    intros f p q x y [x' [H1 H2]] H3. exists x'. split; auto.
  Qed.

  Lemma monotonize_extensive:
    forall f, f <2=^ monotonize f.
  Proof.
    intros f x p q H1.
    exists x. eauto.
  Qed.

End CompleteLattice.

(* Notations defined again to make them global *)
Notation " x =2= y " := (forall p q, x p q <-> y p q) (at level 50, no associativity).
Notation " x °° y " := (compose x y) (at level 69, right associativity).
Notation " x <2=^ y " := (rel_fun_incl x y) (at level 90, no associativity).
Notation " x =2=^ y " := (rel_fun_equiv x y) (at level 90, no associativity).
Notation " x /2\ y " := (intersect_bin x y) (at level 50, no associativity).
Notation " x /2\^ y " := (intersect_fun_bin x y) (at level 90, no associativity).
Notation " x \2/^ y " := (union_fun_bin x y) (at level 90, no associativity).
Notation " x ° y " := (rel_comp x y) (at level 69, right associativity).
Notation " x °^ y " := (rel_comp_fun x y) (at level 69, right associativity).