import Mathlib

variable {α : Type} [CompleteLattice α]

structure Function.IsLeastFixedPt (f : α → α) (x : α) : Prop where
  fixedPt : Function.IsFixedPt f x
  least : ∀ y, Function.IsFixedPt f y → x ≤ y

structure Function.IsGreatestFixedPt (f : α → α) (x : α) : Prop where
  fixedPt : Function.IsFixedPt f x
  greatest : ∀ y, Function.IsFixedPt f y → y ≤ x

namespace FixedPoints

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

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

lemma lfp_isLeastFixedPt (f : α → α) (hf : Monotone f) : Function.IsLeastFixedPt f (lfp f) where
  fixedPt := by
    have hmem : f (lfp f) ≤ lfp f := by
      rw [lfp, le_sInf_iff]
      intro x hx
      grw [hf (sInf_le hx)]
      exact hx
    apply Std.IsPartialOrder.le_antisymm
    · exact hmem
    · exact (sInf_le (hf hmem))
  least := by
    intro x hfix
    apply sInf_le
    simp [show f x = x from hfix]

-- TODO: Avoid repitition
lemma gfp_isGreatestFixedPt (f : α → α) (hf : Monotone f) : Function.IsGreatestFixedPt f (gfp f) where
  fixedPt := 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 hf (le_sSup hx)
    apply Std.IsPartialOrder.le_antisymm
    · apply le_sSup
      exact hf hmem
    · exact hmem
  greatest := by
    intro x hfix
    apply le_sSup
    simp [show f x = x from hfix]

end FixedPoints