# 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).