import Mathlib

namespace FixedPoints

variable {α : Type} [CompleteLattice α]

def lfp (f : α → α) : α := sInf { x | f x ≤ x }

def gfp (f : α → α) : α := sSup { x | x ≤ f x }

lemma lfp_isFixedPt (f : α → α) (h : Monotone f) : Function.IsFixedPt f (lfp f) := by
  have hmem : f (lfp f) ≤ lfp f := by
    rw [lfp, le_sInf_iff]
    intro x hx
    grw [h (sInf_le hx)]
    exact hx
  apply Std.IsPartialOrder.le_antisymm
  · exact hmem
  · exact (sInf_le (h hmem))

lemma lfp_is_least (f : α → α) :
    ∀ x, Function.IsFixedPt f x → lfp f ≤ x := by
  intro x hfix
  apply sInf_le
  simp [show f x = x from hfix]

-- TODO: Avoid repitition

lemma gfp_isFixedPt (f : α → α) (h : Monotone f) : Function.IsFixedPt f (gfp f) := by
  have hmem : gfp f ≤ f (gfp f) := by
    rw [gfp, sSup_le_iff]
    intro x hx
    grw [show x ≤ f x from hx]
    exact h (le_sSup hx)
  apply Std.IsPartialOrder.le_antisymm
  · apply le_sSup
    exact h hmem
  · exact hmem

lemma gfp_is_greatest (f : α → α) :
    ∀ x, Function.IsFixedPt f x → x ≤ gfp f := by
  intro x hfix
  apply le_sSup
  simp [show f x = x from hfix]

end FixedPoints