Require Import base ord.

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.

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.