-- Fixed points of monotone maps 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.Tarski
import Monotone

def latticePrefixed (f A r : Set) : Set := { x ∈ A | relates(r, f(x), x) }
def latticePostfixed (f A r : Set) : Set := { x ∈ A | relates(r, x, f(x)) }
def latticeFixedPoints (f A : Set) : Set := { x ∈ A | f(x) = x }

-- The least fixed point is the infimum of the prefixed points, and the
-- greatest fixed point is the supremum of the postfixed points.
def latticeLeastFixed (f A r : Set) : Set :=
  infimum(A, r, latticePrefixed(f, A, r))
def latticeGreatestFixed (f A r : Set) : Set :=
  supremum(A, r, latticePostfixed(f, A, r))

theorem latticeLeastFixed.value (f A r : Set)
  shows latticeLeastFixed(f, A, r) = infimum(A, r, latticePrefixed(f, A, r))
proof
  simp [latticeLeastFixed]

theorem latticeGreatestFixed.value (f A r : Set)
  shows
    latticeGreatestFixed(f, A, r) = supremum(A, r, latticePostfixed(f, A, r))
proof
  simp [latticeGreatestFixed]

theorem latticePrefixed.subset (f A r : Set)
  shows latticePrefixed(f, A, r) ⊆ A
proof
  intros x hx
  have member := latticePrefixed.membership.forward with hx
  exact member.left

theorem latticePostfixed.subset (f A r : Set)
  shows latticePostfixed(f, A, r) ⊆ A
proof
  intros x hx
  have member := latticePostfixed.membership.forward with hx
  exact member.left

theorem latticeFixedPoints.subset (f A : Set)
  shows latticeFixedPoints(f, A) ⊆ A
proof
  intros x hx
  have member := latticeFixedPoints.membership.forward with hx
  exact member.left

-- The least fixed point

theorem latticeLeastFixed.member (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  shows latticeLeastFixed(f, A, r) ∈ A
proof
  have value := latticeLeastFixed.value at f, A, r
  rw value
  exact infimum.member with complete, (latticePrefixed.subset at f, A, r)

theorem latticeLeastFixed.below (f A r x : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hx : x ∈ A
  requires prefixed : relates(r, f(x), x)
  shows relates(r, latticeLeastFixed(f, A, r), x)
proof
  have value := latticeLeastFixed.value at f, A, r
  rw value
  have member : x ∈ latticePrefixed(f, A, r) :=
    latticePrefixed.membership.backward with ⟨hx, prefixed⟩
  exact infimum.below with complete, (latticePrefixed.subset at f, A, r), member

theorem latticeLeastFixed.prefixed (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  requires monotone : IsMonotoneMap(f, A, r, A, r)
  shows relates(r, f(latticeLeastFixed(f, A, r)), latticeLeastFixed(f, A, r))
proof
  have order := IsCompleteLattice.order with complete
  have transitive := IsPartialOrder.transitive with order
  have bounded := latticePrefixed.subset at f, A, r
  have leastA := latticeLeastFixed.member at f, A, r with complete
  have valueA := IsMonotoneMap.apply_member with monotone, leastA
  have lower : LowerBound(A, r, latticePrefixed(f, A, r),
      f(latticeLeastFixed(f, A, r)))
    refine ⟨valueA, bounded, ?_⟩
    intros x hx
    have member := latticePrefixed.membership.forward with hx
    have below := latticeLeastFixed.below with complete, member.left,
        member.right
    have mapped := IsMonotoneMap.preserves with monotone, leastA, member.left,
        below
    have fxA := IsMonotoneMap.apply_member with monotone, member.left
    exact transitive with f(latticeLeastFixed(f, A, r)), valueA, f(x), fxA, x,
        member.left, mapped, member.right
  have value := latticeLeastFixed.value at f, A, r
  rw value
  rw value at lower
  rw value at valueA
  exact infimum.greatest with complete, bounded, valueA, lower

theorem latticeLeastFixed.fixed (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  requires monotone : IsMonotoneMap(f, A, r, A, r)
  shows f(latticeLeastFixed(f, A, r)) = latticeLeastFixed(f, A, r)
proof
  have order := IsCompleteLattice.order with complete
  have antisymmetric := IsPartialOrder.antisymmetric with order
  have leastA := latticeLeastFixed.member at f, A, r with complete
  have valueA := IsMonotoneMap.apply_member with monotone, leastA
  have prefixed := latticeLeastFixed.prefixed with complete, monotone
  have mapped := IsMonotoneMap.preserves with monotone, valueA, leastA, prefixed
  have above := latticeLeastFixed.below with complete, valueA, mapped
  exact antisymmetric with f(latticeLeastFixed(f, A, r)), valueA,
      latticeLeastFixed(f, A, r), leastA, prefixed, above

theorem latticeLeastFixed.least (f A r x : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hx : x ∈ A
  requires fixed : f(x) = x
  shows relates(r, latticeLeastFixed(f, A, r), x)
proof
  have reflexive := IsPartialOrder.reflexive with
      (IsCompleteLattice.order with complete)
  have prefixed : relates(r, f(x), x)
    rw fixed
    exact reflexive with x, hx
  exact latticeLeastFixed.below with complete, hx, prefixed

theorem latticeLeastFixed.least_fixed (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  requires monotone : IsMonotoneMap(f, A, r, A, r)
  shows Least(A, r, latticeFixedPoints(f, A), latticeLeastFixed(f, A, r))
proof
  have leastA := latticeLeastFixed.member at f, A, r with complete
  have fixed := latticeLeastFixed.fixed with complete, monotone
  constructor
  . exact latticeFixedPoints.membership.backward with ⟨leastA, fixed⟩
  . refine ⟨leastA, (latticeFixedPoints.subset at f, A), ?_⟩
    intros x hx
    have member := latticeFixedPoints.membership.forward with hx
    exact latticeLeastFixed.least with complete, member.left, member.right

-- The greatest fixed point

theorem latticeGreatestFixed.member (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  shows latticeGreatestFixed(f, A, r) ∈ A
proof
  have value := latticeGreatestFixed.value at f, A, r
  rw value
  exact supremum.member with complete, (latticePostfixed.subset at f, A, r)

theorem latticeGreatestFixed.above (f A r x : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hx : x ∈ A
  requires postfixed : relates(r, x, f(x))
  shows relates(r, x, latticeGreatestFixed(f, A, r))
proof
  have value := latticeGreatestFixed.value at f, A, r
  rw value
  have member : x ∈ latticePostfixed(f, A, r) :=
    latticePostfixed.membership.backward with ⟨hx, postfixed⟩
  exact supremum.above with complete, (latticePostfixed.subset at f, A, r),
      member

theorem latticeGreatestFixed.postfixed (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  requires monotone : IsMonotoneMap(f, A, r, A, r)
  shows
    relates(r, latticeGreatestFixed(f, A, r), f(latticeGreatestFixed(f, A, r)))
proof
  have order := IsCompleteLattice.order with complete
  have transitive := IsPartialOrder.transitive with order
  have bounded := latticePostfixed.subset at f, A, r
  have greatestA := latticeGreatestFixed.member at f, A, r with complete
  have valueA := IsMonotoneMap.apply_member with monotone, greatestA
  have upper : UpperBound(A, r, latticePostfixed(f, A, r),
      f(latticeGreatestFixed(f, A, r)))
    refine ⟨valueA, bounded, ?_⟩
    intros x hx
    have member := latticePostfixed.membership.forward with hx
    have above := latticeGreatestFixed.above with complete, member.left,
        member.right
    have mapped := IsMonotoneMap.preserves with monotone, member.left,
        greatestA, above
    have fxA := IsMonotoneMap.apply_member with monotone, member.left
    exact transitive with x, member.left, f(x), fxA, f(latticeGreatestFixed(f,
        A, r)), valueA, member.right, mapped
  have value := latticeGreatestFixed.value at f, A, r
  rw value
  rw value at upper
  rw value at valueA
  exact supremum.least with complete, bounded, valueA, upper

theorem latticeGreatestFixed.fixed (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  requires monotone : IsMonotoneMap(f, A, r, A, r)
  shows f(latticeGreatestFixed(f, A, r)) = latticeGreatestFixed(f, A, r)
proof
  have order := IsCompleteLattice.order with complete
  have antisymmetric := IsPartialOrder.antisymmetric with order
  have greatestA := latticeGreatestFixed.member at f, A, r with complete
  have valueA := IsMonotoneMap.apply_member with monotone, greatestA
  have postfixed := latticeGreatestFixed.postfixed with complete, monotone
  have mapped := IsMonotoneMap.preserves with monotone, greatestA, valueA,
      postfixed
  have below := latticeGreatestFixed.above with complete, valueA, mapped
  exact antisymmetric with f(latticeGreatestFixed(f, A, r)), valueA,
      latticeGreatestFixed(f, A, r), greatestA, below, postfixed

theorem latticeGreatestFixed.greatest (f A r x : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hx : x ∈ A
  requires fixed : f(x) = x
  shows relates(r, x, latticeGreatestFixed(f, A, r))
proof
  have reflexive := IsPartialOrder.reflexive with
      (IsCompleteLattice.order with complete)
  have postfixed : relates(r, x, f(x))
    rw fixed
    exact reflexive with x, hx
  exact latticeGreatestFixed.above with complete, hx, postfixed

theorem latticeGreatestFixed.greatest_fixed (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  requires monotone : IsMonotoneMap(f, A, r, A, r)
  shows Greatest(A, r, latticeFixedPoints(f, A), latticeGreatestFixed(f, A, r))
proof
  have greatestA := latticeGreatestFixed.member at f, A, r with complete
  have fixed := latticeGreatestFixed.fixed with complete, monotone
  constructor
  . exact latticeFixedPoints.membership.backward with ⟨greatestA, fixed⟩
  . refine ⟨greatestA, (latticeFixedPoints.subset at f, A), ?_⟩
    intros x hx
    have member := latticeFixedPoints.membership.forward with hx
    exact latticeGreatestFixed.greatest with complete, member.left, member.right

-- Consequences

theorem IsMonotoneMap.exists_fixed_point (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  requires monotone : IsMonotoneMap(f, A, r, A, r)
  shows ∃ x ∈ A, f(x) = x
proof
  refine ⟨latticeLeastFixed(f, A, r), (latticeLeastFixed.member at f, A,
      r with complete), (latticeLeastFixed.fixed with complete, monotone)⟩

theorem latticeFixedPoints.nonempty (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  requires monotone : IsMonotoneMap(f, A, r, A, r)
  shows Nonempty(latticeFixedPoints(f, A))
proof
  have least := latticeLeastFixed.least_fixed with complete, monotone
  refine ⟨latticeLeastFixed(f, A, r), Least.member with least⟩

theorem latticeLeastFixed.le_greatest (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  requires monotone : IsMonotoneMap(f, A, r, A, r)
  shows relates(r, latticeLeastFixed(f, A, r), latticeGreatestFixed(f, A, r))
proof
  have greatestA := latticeGreatestFixed.member at f, A, r with complete
  have fixed := latticeGreatestFixed.fixed with complete, monotone
  exact latticeLeastFixed.least with complete, greatestA, fixed

theorem latticeFixedPoints.unique_of_eq (f A r : Set)
  requires complete : IsCompleteLattice(A, r)
  requires monotone : IsMonotoneMap(f, A, r, A, r)
  requires same : latticeLeastFixed(f, A, r) = latticeGreatestFixed(f, A, r)
  shows ∀ x ∈ A, f(x) = x → x = latticeLeastFixed(f, A, r)
proof
  have antisymmetric := IsPartialOrder.antisymmetric with
      (IsCompleteLattice.order with complete)
  have leastA := latticeLeastFixed.member at f, A, r with complete
  intros x hx fixed
  have below := latticeLeastFixed.least with complete, hx, fixed
  have above := latticeGreatestFixed.greatest with complete, hx, fixed
  rw ← same at above
  exact antisymmetric with x, hx, latticeLeastFixed(f, A, r), leastA, above,
      below