-- Knaster–Tarski: least and greatest fixed points on a complete lattice
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Lattice.FixedPoints
import Tarski
import OrderHom

-- The prefixed, postfixed, and fixed points of a map on a bundled order,
-- and its least and greatest fixed points: the infimum of the prefixed
-- points and the supremum of the postfixed points. The definitions live in
-- the section of the ordered set, so they take P as their first parameter
-- and are written without it inside the section.
section FixedPoints
variable (P : Set)

def prefixPoints (f : Set) : Set := latticePrefixed(f, points(P), le(P))
def postfixPoints (f : Set) : Set := latticePostfixed(f, points(P), le(P))
def fixedPoints (f : Set) : Set := latticeFixedPoints(f, points(P))
def lfp (f : Set) : Set := latticeLeastFixed(f, points(P), le(P))
def gfp (f : Set) : Set := latticeGreatestFixed(f, points(P), le(P))

theorem prefixPoints.membership (f x : Set)
  shows x ∈ prefixPoints(f) ↔ (x ∈ points(P) ∧ relates(le(P), f(x), x))
proof
  simp [prefixPoints, latticePrefixed]

theorem postfixPoints.membership (f x : Set)
  shows x ∈ postfixPoints(f) ↔ (x ∈ points(P) ∧ relates(le(P), x, f(x)))
proof
  simp [postfixPoints, latticePostfixed]

theorem fixedPoints.membership (f x : Set)
  shows x ∈ fixedPoints(f) ↔ (x ∈ points(P) ∧ f(x) = x)
proof
  simp [fixedPoints, latticeFixedPoints]

theorem prefixPoints.subset (f : Set)
  shows prefixPoints(f) ⊆ points(P)
proof
  unfold prefixPoints
  exact latticePrefixed.subset at f, points(P), le(P)

theorem postfixPoints.subset (f : Set)
  shows postfixPoints(f) ⊆ points(P)
proof
  unfold postfixPoints
  exact latticePostfixed.subset at f, points(P), le(P)

theorem fixedPoints.subset (f : Set)
  shows fixedPoints(f) ⊆ points(P)
proof
  unfold fixedPoints
  exact latticeFixedPoints.subset at f, points(P)

theorem lfp.unfold (f : Set)
  shows lfp(f) = latticeLeastFixed(f, points(P), le(P))
proof
  simp [lfp]

theorem gfp.unfold (f : Set)
  shows gfp(f) = latticeGreatestFixed(f, points(P), le(P))
proof
  simp [gfp]

section FixedPointLaws
variable (f : Set)
hypothesis complete : CompleteLattice(P)
hypothesis monotone : MonotoneMap(f, P, P)

theorem lfp.eq_sInf
  shows lfp(f) = sInf(P)(prefixPoints(f))
proof
  have subset := prefixPoints.subset at P, f
  rw [sInf.infimum, lfp.unfold, latticeLeastFixed.value]
  unfold prefixPoints
  rfl

theorem gfp.eq_sSup
  shows gfp(f) = sSup(P)(postfixPoints(f))
proof
  have subset := postfixPoints.subset at P, f
  rw [sSup.supremum, gfp.unfold, latticeGreatestFixed.value]
  unfold postfixPoints
  rfl

instance lfp.member
  shows lfp(f) ∈ points(P)
proof
  rw lfp.unfold
  exact latticeLeastFixed.member with (CompleteLattice.unbundled with complete)

instance gfp.member
  shows gfp(f) ∈ points(P)
proof
  rw gfp.unfold
  exact latticeGreatestFixed.member with (CompleteLattice.unbundled with complete)

theorem lfp_le (a ∈ points(P))
  requires prefixed : f(a) ≤ a
  shows lfp(f) ≤ a
proof
  rw lfp.unfold
  exact latticeLeastFixed.below with (CompleteLattice.unbundled with complete),
      *

theorem le_gfp (a ∈ points(P))
  requires postfixed : a ≤ f(a)
  shows a ≤ gfp(f)
proof
  rw gfp.unfold
  exact latticeGreatestFixed.above with (CompleteLattice.unbundled with complete),
      *

theorem lfp_le_fixed (a ∈ points(P))
  requires fixed : f(a) = a
  shows lfp(f) ≤ a
proof
  rw lfp.unfold
  exact latticeLeastFixed.least with (CompleteLattice.unbundled with complete),
      *

theorem le_gfp_fixed (a ∈ points(P))
  requires fixed : f(a) = a
  shows a ≤ gfp(f)
proof
  rw gfp.unfold
  exact latticeGreatestFixed.greatest with (CompleteLattice.unbundled with complete),
      *

theorem map_lfp_le
  shows f(lfp(f)) ≤ lfp(f)
proof
  rw lfp.unfold
  exact latticeLeastFixed.prefixed with (CompleteLattice.unbundled with complete),
      (MonotoneMap.unbundled with monotone)

theorem le_map_gfp
  shows gfp(f) ≤ f(gfp(f))
proof
  rw gfp.unfold
  exact latticeGreatestFixed.postfixed with (CompleteLattice.unbundled with complete),
      (MonotoneMap.unbundled with monotone)

theorem lfp_fixed
  shows f(lfp(f)) = lfp(f)
proof
  have prefixed : f(lfp(f)) ≤ lfp(f) := map_lfp_le with *
  have mapped : f(f(lfp(f))) ≤ f(lfp(f)) := MonotoneMap.map_le with *
  have postfixed : lfp(f) ≤ f(lfp(f)) := lfp_le with *
  exact le_antisymm with *

theorem gfp_fixed
  shows f(gfp(f)) = gfp(f)
proof
  have postfixed : gfp(f) ≤ f(gfp(f)) := le_map_gfp with *
  have mapped : f(gfp(f)) ≤ f(f(gfp(f))) := MonotoneMap.map_le with *
  have prefixed : f(gfp(f)) ≤ gfp(f) := le_gfp with *
  exact le_antisymm with *

theorem lfp.mem_fixedPoints
  shows lfp(f) ∈ fixedPoints(f)
proof
  have fixed : f(lfp(f)) = lfp(f) := lfp_fixed with *
  have member : lfp(f) ∈ points(P) := lfp.member with *
  apply fixedPoints.membership.backward
  exact ⟨member, fixed⟩

theorem gfp.mem_fixedPoints
  shows gfp(f) ∈ fixedPoints(f)
proof
  have fixed : f(gfp(f)) = gfp(f) := gfp_fixed with *
  have member : gfp(f) ∈ points(P) := gfp.member with *
  apply fixedPoints.membership.backward
  exact ⟨member, fixed⟩

theorem lfp.isLeast
  shows IsLeast(P, fixedPoints(f), lfp(f))
proof
  unfold IsLeast
  unfold fixedPoints
  rw lfp.unfold
  exact latticeLeastFixed.least_fixed with (CompleteLattice.unbundled with complete),
      (MonotoneMap.unbundled with monotone)

theorem gfp.isGreatest
  shows IsGreatest(P, fixedPoints(f), gfp(f))
proof
  unfold IsGreatest
  unfold fixedPoints
  rw gfp.unfold
  exact latticeGreatestFixed.greatest_fixed with (CompleteLattice.unbundled with complete),
      (MonotoneMap.unbundled with monotone)

theorem exists_fixed_point
  shows ∃ a ∈ points(P), f(a) = a
proof
  exact IsMonotoneMap.exists_fixed_point with (CompleteLattice.unbundled with complete),
      (MonotoneMap.unbundled with monotone)

theorem fixedPoints.nonempty
  shows Nonempty(fixedPoints(f))
proof
  have member := lfp.mem_fixedPoints with *
  exact ⟨lfp(f), member⟩

theorem lfp_le_gfp
  shows lfp(f) ≤ gfp(f)
proof
  have fixed : f(gfp(f)) = gfp(f) := gfp_fixed with *
  exact lfp_le_fixed with *

end FixedPointLaws
end FixedPoints