/-
Port of `Fixedpoint.agda`.

Same gas-based algorithm: iterate `f` starting at the chain-bottom `⊥`; since
the lattice has fixed height `h`, a fixed point must be reached within `h + 1`
steps, or we would build a `<`-chain longer than the longest one. We
deliberately do *not* use mathlib's `OrderHom.lfp` (different proof approach,
and not computable).

Correspondence:
  doStep             ↦ Spa.Fixedpoint.doStep   (the chain argument now carries
                                                 `a₁ = ⊥` and its length in the
                                                 `LTSeries` structure itself)
  fix                ↦ Spa.Fixedpoint.fix
  aᶠ                 ↦ Spa.Fixedpoint.aFix
  aᶠ≈faᶠ             ↦ Spa.Fixedpoint.aFix_eq
  stepPreservesLess  ↦ Spa.Fixedpoint.doStep_le
  aᶠ≼                ↦ Spa.Fixedpoint.aFix_le
-/
import Spa.Lattice

namespace Spa.Fixedpoint

variable {α : Type*} [Lattice α] [DecidableEq α] {h : ℕ}

/-- Agda: `doStep`. `g` is gas; the invariant `c.length + g = h + 1` guarantees
that when gas runs out the chain contradicts boundedness. -/
def doStep (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) :
    ∀ (g : ℕ) (c : LTSeries α), c.length + g = h + 1 →
      c.last ≤ f c.last → {a : α // a = f a}
  | 0, c, hlen, _ =>
    absurd (fh.bounded c) (by omega)
  | g + 1, c, hlen, hle =>
    if heq : c.last = f c.last then
      ⟨c.last, heq⟩
    else
      doStep fh 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)

/-- Agda: `fix`. Start iterating from `⊥`. -/
def fix (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) : {a : α // a = f a} :=
  doStep fh f hf (h + 1) (RelSeries.singleton _ fh.bot)
    (by simp)
    (by simpa [RelSeries.last_singleton] using fh.bot_le (f fh.bot))

/-- Agda: `aᶠ`. -/
def aFix (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) : α :=
  (fix fh f hf).1

/-- Agda: `aᶠ≈faᶠ`. -/
theorem aFix_eq (fh : FixedHeight α h) (f : α → α) (hf : Monotone f) :
    aFix fh f hf = f (aFix fh f hf) :=
  (fix fh f hf).2

/-- Agda: `stepPreservesLess` — iteration stays below any fixed point. -/
theorem doStep_le (fh : FixedHeight α h) (f : α → α) (hf : Monotone f)
    {b : α} (hb : b = f b) :
    ∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = h + 1)
      (hle : c.last ≤ f c.last), c.last ≤ b →
      (doStep fh f hf g c hlen hle : α) ≤ b
  | 0, c, hlen, _ => fun _ => absurd (fh.bounded c) (by omega)
  | g + 1, c, hlen, hle => fun hcb => by
    rw [doStep]
    split
    · exact hcb
    · exact doStep_le fh f hf hb g _ _ _
        (by rw [RelSeries.last_snoc]; exact le_of_le_of_eq (hf hcb) hb.symm)

/-- Agda: `aᶠ≼` — `aFix` is below every fixed point of `f`. -/
theorem aFix_le (fh : FixedHeight α h) (f : α → α) (hf : Monotone f)
    {a : α} (ha : a = f a) : aFix fh f hf ≤ a :=
  doStep_le fh f hf ha _ _ _ _ (by simpa using fh.bot_le a)

end Spa.Fixedpoint
