import Spa.Lattice

namespace Spa.Fixedpoint

open FiniteHeightLattice (height)

variable {α : Type*} [Lattice α] [DecidableEq α] [FiniteHeightLattice α]

def doStep (f : α → α) (hf : Monotone f) :
    ∀ (g : ℕ) (c : LTSeries α), c.length + g = height (α := α) + 1 →
      c.last ≤ f c.last → {a : α // a = f a}
  | 0, c, hlen, _ =>
    absurd (FiniteHeightLattice.chains_bounded c) (by omega)
  | g + 1, c, hlen, hle =>
    if heq : c.last = f c.last then
      ⟨c.last, heq⟩
    else
      doStep f hf g (c.snoc (f c.last) (lt_of_le_of_ne hle heq))
        (by simp [RelSeries.snoc]; omega)
        (by rw [RelSeries.last_snoc]; exact hf hle)

def fix (f : α → α) (hf : Monotone f) : {a : α // a = f a} :=
  doStep f hf (height (α := α) + 1) (RelSeries.singleton _ ⊥)
    (by simp)
    (by simpa [RelSeries.last_singleton]
          using FiniteHeightLattice.bot_le α (f ⊥))

def aFix (f : α → α) (hf : Monotone f) : α :=
  (fix f hf).1

theorem aFix_eq (f : α → α) (hf : Monotone f) :
    aFix f hf = f (aFix f hf) :=
  (fix f hf).2

theorem doStep_le (f : α → α) (hf : Monotone f)
    {b : α} (hb : b = f b) :
    ∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1)
      (hle : c.last ≤ f c.last), c.last ≤ b →
      (doStep f hf g c hlen hle : α) ≤ b
  | 0, c, hlen, _ => fun _ => absurd (FiniteHeightLattice.chains_bounded c) (by omega)
  | g + 1, c, hlen, hle => fun hcb => by
    rw [doStep]
    split
    · exact hcb
    · exact doStep_le f hf hb g _ _ _
        (by rw [RelSeries.last_snoc]; exact le_of_le_of_eq (hf hcb) hb.symm)

theorem aFix_le (f : α → α) (hf : Monotone f)
    {a : α} (ha : a = f a) : aFix f hf ≤ a :=
  doStep_le f hf ha _ _ _ _ (by simpa using FiniteHeightLattice.bot_le α a)

end Spa.Fixedpoint