Require Import base ord.

Section TarskiLfp.
  Variable (X : clat) (f : X -> X).
  Context {fP : monotone f}.
  Implicit Types (x y z : X).

  Definition lfp_above x : X :=
    ∀ y | (x ≤ y) /\ (f y ≤ y), y.

  Lemma lfp_above_ind x y :
    x ≤ y -> f y ≤ y -> lfp_above x ≤ y.
  Proof.
    move=> le_x_y le_fy_y. exact: allEc le_refl.
  Qed.

  Lemma lfp_above_ge x :
    x ≤ lfp_above x.
  Proof.
    rewrite/lfp_above. by focus=> y [].
  Qed.

  Lemma lfp_above_fold x :
    f (lfp_above x) ≤ lfp_above x.
  Proof.
    rewrite{2}/lfp_above; focus=> y [le_x_y le_fy_y].
    rewrite -le_fy_y. apply: mono. exact: allEc le_refl.
  Qed.

  Lemma lfp_aboveE x :
    x ≤ f x -> f (lfp_above x) = lfp_above x.
  Proof.
    move=> le_x_fx. apply: le_eq. exact: lfp_above_fold. apply: lfp_above_ind.
    - rewrite {1}le_x_fx. apply: mono. exact: lfp_above_ge.
    - apply: mono. exact: lfp_above_fold.
  Qed.
End TarskiLfp.

Section TarskiGfp.
  Variables (X : clat) (f : X -> X).
  Context {fP : monotone f}.
  Implicit Types (x y z : X).

  Let fr := f : X^r -> X^r.

  Definition gfp_below y := ∃ x | (x ≤ y) /\ (x ≤ f x), x.

  Lemma gfp_below_coind x y :
    x ≤ y -> x ≤ f x -> x ≤ gfp_below y.
  Proof.
    move=> le_x_y le_x_fx. exact: exIc le_refl.
  Qed.

  Lemma gfp_below_le x :
    gfp_below x ≤ x.
  Proof.
    rewrite/gfp_below. by focus=> y [].
  Qed.

  Lemma gfp_below_unfold x :
    gfp_below x ≤ f (gfp_below x).
  Proof.
    rewrite{1}/gfp_below; focus=> y [le_y_x le_y_fy].
    rewrite le_y_fy. apply: mono. exact: exIc le_refl.
  Qed.

  Lemma gfp_belowE x :
    f x ≤ x -> f (gfp_below x) = gfp_below x.
  Proof.
    move=> le_fx_x. apply: le_eq; last by exact: gfp_below_unfold. apply: gfp_below_coind.
    - rewrite -{2}le_fx_x. apply: mono. exact: gfp_below_le.
    - apply: mono. exact: gfp_below_unfold.
  Qed.
End TarskiGfp.

Structure fp {X : Type} (f : X -> X) := mk_fp
  { point : X
  ; fpP : f point = point
  }.
Arguments mk_fp {X f} point fpP.

Lemma fp_eq {X : Type} (f : X -> X) (p q : fp f) :
  point p = point q -> p = q.
Proof.
  destruct p,q; cbn; intros E; destruct E. f_equal. exact: pi.
Qed.

Canonical fp_proType (X : proType) (f : X -> X) :=
  Eval hnf in InducedProType (fp f) (@point X f).

Canonical fp_ordType (X : ordType) (f : X -> X) :=
  Eval hnf in InducedOrdType (fp f) (@fp_eq X f).

Lemma fp_leE (X : proType) (f : X -> X) (p q : fp f) :
  (p ≤ q) = (point p ≤ point q).
Proof. by []. Qed.

Section FpCLat.
  Variables (X : clat) (f : X -> X).
  Context {fP : monotone f}.
  Implicit Types (p q r : fp f).

  Program Definition fp_inf I (F : I -> fp f) : fp f :=
    mk_fp (@gfp_below X f (∀ i, point (F i))) _.
  Next Obligation.
    apply: gfp_belowE. focus=> i. rewrite -fpP. apply: mono.
    apply: allE (i) le_refl.
  Qed.

  Lemma fp_infP I (F : I -> fp f) : is_glb F (fp_inf F).
  Proof.
    apply: mk_glb => [i|/=p h1].
    - rewrite fp_leE /=. rewrite gfp_below_le. exact: allE.
    - rewrite fp_leE /=. apply: gfp_below_coind.
      focus. exact: h1. by rewrite fpP.
  Qed.

  Canonical fp_clatMixin := CLatMixin fp_infP.
  Canonical fp_clat := Eval hnf in CLat (fp f) fp_clatMixin.

  Lemma fp_topE : point (⊤ : fp f) = ∃ x | (x ≤ f x), x.
  Proof.
    cbn. set T := ∀ _, _. have->: T = ⊤. apply: top_eq. rewrite/T; by focus.
    rewrite/gfp_below. apply: le_eq; focus=> x H; apply: exIc (x) _ le_refl => //.
      by case: H.
  Qed.

  Lemma fp_botE : point (⊥ : fp f) = ∀ x | (f x ≤ x), x.
  Proof.
    cbn. apply: le_eq.
    - focus=> x le_fx_x. rewrite/gfp_below. focus=> y [le_y_b le_y_fy].
      rewrite -(gfp_below_le f x) le_y_b.
      exact: allE (mk_fp (gfp_below f x) (gfp_belowE le_fx_x)) _.
    - apply: gfp_below_coind.
      + focus=> i. apply: allEc (point i) _ le_refl. by rewrite fpP.
      + apply: allEc le_refl. apply: mono. focus=> i le_fi_i.
        rewrite -le_fi_i. apply: mono. exact: allEc le_refl.
  Qed.
End FpCLat.

Definition lfp {X : clat} (f : X -> X) : X := lfp_above f ⊥.
Definition gfp {X : clat} (f : X -> X) : X := gfp_below f ⊤.

Lemma lfp_def {X : clat} (f : X -> X) :
  lfp f = ∀ x | (f x ≤ x), x.
Proof.
  apply: le_eq. focus=> x le_fx_x. exact: lfp_above_ind.
  rewrite/lfp/lfp_above. focus=> x [_ le_fx_x]. exact: allEc le_refl.
Qed.

Lemma gfp_def {X : clat} (f : X -> X) :
  gfp f = ∃ x | (x ≤ f x), x.
Proof.
  apply: le_eq. rewrite/gfp/gfp_below. focus=> x [_ le_x_fx]. exact: exIc le_refl.
  focus=> x le_x_fx. exact: gfp_below_coind.
Qed.

Lemma lfpE {X : clat} (f : X -> X) : monotone f -> f (lfp f) = lfp f.
Proof. move=> fP. apply: lfp_aboveE. exact: botE. Qed.

Lemma gfpE {X : clat} (f : X -> X) : monotone f -> f (gfp f) = gfp f.
Proof. move=> fP. apply: gfp_belowE. exact: topI. Qed.