# semantics.tower.associated_closure

Section AssociatedClosure.

Context {A : clat} (P : A -> Prop).

Hypothesis ic : inf_closed P.

Implicit Types (x y z : A).

Definition closure_of x : A :=

∀ y | P y /\ (x ≤ y), y.

Lemma closure_of_stable x :

P (closure_of x).

Proof.

apply: ic => i. by apply: ic => -[].

Qed.

Global Instance closure_of_is_closure :

is_closure closure_of.

Proof.

move=> x y. split=> h.

- rewrite -h /closure_of. by focus=> z [].

- apply: allEc le_refl. split=> //. exact: closure_of_stable.

Qed.

Lemma closure_of_image x :

(closure_of x ≤ x) <-> P x.

Proof.

split=> [le_cx_x|px]; last by exact: allEc le_refl.

have->: x = closure_of x. apply: le_eq => //. exact: closure_inc.

exact: closure_of_stable.

Qed.

End AssociatedClosure.

Context {A : clat} (P : A -> Prop).

Hypothesis ic : inf_closed P.

Implicit Types (x y z : A).

Definition closure_of x : A :=

∀ y | P y /\ (x ≤ y), y.

Lemma closure_of_stable x :

P (closure_of x).

Proof.

apply: ic => i. by apply: ic => -[].

Qed.

Global Instance closure_of_is_closure :

is_closure closure_of.

Proof.

move=> x y. split=> h.

- rewrite -h /closure_of. by focus=> z [].

- apply: allEc le_refl. split=> //. exact: closure_of_stable.

Qed.

Lemma closure_of_image x :

(closure_of x ≤ x) <-> P x.

Proof.

split=> [le_cx_x|px]; last by exact: allEc le_refl.

have->: x = closure_of x. apply: le_eq => //. exact: closure_inc.

exact: closure_of_stable.

Qed.

End AssociatedClosure.

Section Characterization.

Variable (A : clat).

Let closure_operatorT := { f : A -> A | is_closure f }.

Let inf_closedT := { P : A -> Prop | inf_closed P }.

Definition inf_closed_to_closure :

inf_closedT -> closure_operatorT :=

fun p => exist is_closure (closure_of p.1) (closure_of_is_closure p.2).

Program Definition closure_to_inf_closed :

closure_operatorT -> inf_closedT :=

fun p => exist inf_closed (fun x => p.1 x ≤ x) _.

Next Obligation.

move=> I F h. focus=> i. rewrite -h. destruct p => /=. apply: mono. exact: allE.

Qed.

Lemma inf_closed_to_closure_retr p :

closure_to_inf_closed (inf_closed_to_closure p) = p.

Proof.

apply: sig_eq => /=; fext=> x. destruct p as [P hP] => /=.

apply: pext; by rewrite closure_of_image.

Qed.

Lemma closure_to_inf_closed_retr p :

(inf_closed_to_closure (closure_to_inf_closed p)) = p.

Proof.

destruct p as [c clos] => /=. apply: sig_eq => /=; fext=> x. apply: le_eq.

- rewrite/closure_of. apply: allEc le_refl. split. by rewrite closure_idem.

exact: closure_inc.

- rewrite/closure_of. by focus=> y [l1 ->].

Qed.

Lemma closure_inf_closed :

{ P : A -> Prop | inf_closed P } <~> { f : A -> A | is_closure f }.

Proof.

apply: (mk_equiv inf_closed_to_closure). apply: (mk_is_equiv closure_to_inf_closed).

exact: inf_closed_to_closure_retr. exact: closure_to_inf_closed_retr.

Qed.

End Characterization.

Variable (A : clat).

Let closure_operatorT := { f : A -> A | is_closure f }.

Let inf_closedT := { P : A -> Prop | inf_closed P }.

Definition inf_closed_to_closure :

inf_closedT -> closure_operatorT :=

fun p => exist is_closure (closure_of p.1) (closure_of_is_closure p.2).

Program Definition closure_to_inf_closed :

closure_operatorT -> inf_closedT :=

fun p => exist inf_closed (fun x => p.1 x ≤ x) _.

Next Obligation.

move=> I F h. focus=> i. rewrite -h. destruct p => /=. apply: mono. exact: allE.

Qed.

Lemma inf_closed_to_closure_retr p :

closure_to_inf_closed (inf_closed_to_closure p) = p.

Proof.

apply: sig_eq => /=; fext=> x. destruct p as [P hP] => /=.

apply: pext; by rewrite closure_of_image.

Qed.

Lemma closure_to_inf_closed_retr p :

(inf_closed_to_closure (closure_to_inf_closed p)) = p.

Proof.

destruct p as [c clos] => /=. apply: sig_eq => /=; fext=> x. apply: le_eq.

- rewrite/closure_of. apply: allEc le_refl. split. by rewrite closure_idem.

exact: closure_inc.

- rewrite/closure_of. by focus=> y [l1 ->].

Qed.

Lemma closure_inf_closed :

{ P : A -> Prop | inf_closed P } <~> { f : A -> A | is_closure f }.

Proof.

apply: (mk_equiv inf_closed_to_closure). apply: (mk_is_equiv closure_to_inf_closed).

exact: inf_closed_to_closure_retr. exact: closure_to_inf_closed_retr.

Qed.

End Characterization.