-- Complete lattices bundled as ordered sets, with sSup(P) and sInf(P), and
-- the powerset 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.CompleteLattice
import Complete
import BoundedOrder

-- A complete lattice is a property of the bundled order; the supremum and
-- infimum of a subset are the set functions sSup(P) and sInf(P) on the
-- powerset of the points, applied as sSup(P)(S).
predicate CompleteLattice (P : Set) := IsCompleteLattice(points(P), le(P))

notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis CompleteLattice(P) for P.points
notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis CompleteLattice(P) for P.points
notation infix 50 "≤" => Le(P, _, _) via hypothesis CompleteLattice(P) for P.points

instance CompleteLattice.unbundled (P : Set)
  requires complete : CompleteLattice(P)
  shows IsCompleteLattice(points(P), le(P))
proof
  simp [CompleteLattice]

theorem CompleteLattice.mk (A r : Set)
  requires complete : IsCompleteLattice(A, r)
  shows CompleteLattice(Order.mk(A, r))
proof
  unfold CompleteLattice
  rw [Order.mk.points, Order.mk.le]
  exact complete

theorem CompleteLattice.lattice_of (P : Set)
  requires complete : CompleteLattice(P)
  shows Lattice(P)
proof
  unfold Join.Lattice
  exact IsCompleteLattice.lattice with (CompleteLattice.unbundled with complete)

instance CompleteLattice.bounded_of (P : Set)
  requires complete : CompleteLattice(P)
  shows BoundedLattice(P)
proof
  have unbundled := CompleteLattice.unbundled with complete
  have bounded := IsCompleteLattice.bounded with unbundled
  have lattice : Lattice(P) := CompleteLattice.lattice_of with complete
  refine ⟨lattice, ?_, ?_⟩
  . witness supremum(points(P), le(P), ∅)
    exact IsBoundedLattice.least with bounded
  . witness supremum(points(P), le(P), points(P))
    exact IsBoundedLattice.greatest with bounded

theorem CompleteLattice.subset_of_member (P S : Set)
  requires member : S ∈ 𝒫(points(P))
  shows S ⊆ points(P)
proof
  exact powerset.membership_iff.forward with member

defgraph sSup (P : Set) (S ∈ 𝒫(points(P))) : points(P) := supremum(points(P), le(P), S)
requires complete : CompleteLattice(P)
proof
  have subset := CompleteLattice.subset_of_member with member
  exact supremum.member with (CompleteLattice.unbundled with complete), subset

defgraph sInf (P : Set) (S ∈ 𝒫(points(P))) : points(P) := infimum(points(P), le(P), S)
requires complete : CompleteLattice(P)
proof
  have subset := CompleteLattice.subset_of_member with member
  exact infimum.member with (CompleteLattice.unbundled with complete), subset

-- The supremum and infimum of a subset S of the points are written ⨆ S
-- and ⨅ S, and the bounds ⊥ and ⊤, wherever a hypothesis in scope supplies
-- the complete lattice; each value lies in points(P).
notation prefix 90 "⨆" => apply(sSup(P), _) via hypothesis CompleteLattice(P) for P.points
notation prefix 90 "⨅" => apply(sInf(P), _) via hypothesis CompleteLattice(P) for P.points
notation constant "⊥" => bot(P) via hypothesis CompleteLattice(P) for P.points
notation constant "⊤" => top(P) via hypothesis CompleteLattice(P) for P.points

section CompleteLatticeLaws
variable (P : Set)
hypothesis complete : CompleteLattice(P)

-- The bundled operations are the unbundled supremum and infimum.
theorem sSup.supremum (S : Set)
  requires hS : S ⊆ points(P)
  shows sSup(P)(S) = supremum(points(P), le(P), S)
proof
  have member : S ∈ 𝒫(points(P)) := powerset.membership_iff.backward with hS
  exact sSup.value with complete, member

theorem sInf.infimum (S : Set)
  requires hS : S ⊆ points(P)
  shows sInf(P)(S) = infimum(points(P), le(P), S)
proof
  have member : S ∈ 𝒫(points(P)) := powerset.membership_iff.backward with hS
  exact sInf.value with complete, member

instance sSup.member (S : Set)
  requires hS : S ⊆ points(P)
  shows sSup(P)(S) ∈ points(P)
proof
  rw sSup.supremum
  exact supremum.member with *

instance sInf.member (S : Set)
  requires hS : S ⊆ points(P)
  shows sInf(P)(S) ∈ points(P)
proof
  rw sInf.infimum
  exact infimum.member with *

theorem sSup.isLUB (S : Set)
  requires hS : S ⊆ points(P)
  shows IsLUB(P, S, sSup(P)(S))
proof
  unfold IsLUB
  rw sSup.supremum
  exact supremum.supremum with *

theorem sInf.isGLB (S : Set)
  requires hS : S ⊆ points(P)
  shows IsGLB(P, S, sInf(P)(S))
proof
  unfold IsGLB
  rw sInf.infimum
  exact infimum.infimum with *

theorem le_sSup (S a : Set)
  requires hS : S ⊆ points(P)
  requires aIn : a ∈ S
  shows a ≤ ⨆ S
proof
  unfold Le
  rw sSup.supremum
  exact supremum.above with *

theorem sSup_le (S : Set) (b ∈ points(P))
  requires hS : S ⊆ points(P)
  requires bound : ∀ x ∈ S, x ≤ b
  shows sSup(P)(S) ≤ b
proof
  unfold Le
  rw sSup.supremum
  have bIn : b ∈ points(P) by assumption
  have above : ∀ x ∈ S, relates(le(P), x, b)
    intros x xIn
    exact Le.relates with (bound with x, xIn)
  have upper : UpperBound(points(P), le(P), S, b) := ⟨bIn, hS, above⟩
  exact supremum.least with *

theorem sInf_le (S a : Set)
  requires hS : S ⊆ points(P)
  requires aIn : a ∈ S
  shows ⨅ S ≤ a
proof
  unfold Le
  rw sInf.infimum
  exact infimum.below with *

theorem le_sInf (S : Set) (b ∈ points(P))
  requires hS : S ⊆ points(P)
  requires bound : ∀ x ∈ S, b ≤ x
  shows b ≤ sInf(P)(S)
proof
  unfold Le
  rw sInf.infimum
  have bIn : b ∈ points(P) by assumption
  have below : ∀ x ∈ S, relates(le(P), b, x)
    intros x xIn
    exact Le.relates with (bound with x, xIn)
  have lower : LowerBound(points(P), le(P), S, b) := ⟨bIn, hS, below⟩
  exact infimum.greatest with *

theorem sSup_le_iff (S : Set) (b ∈ points(P))
  requires hS : S ⊆ points(P)
  shows sSup(P)(S) ≤ b ↔ ∀ x ∈ S, x ≤ b
proof
  constructor
  . intros h x xIn
    have xIn2 : x ∈ points(P) := hS with x, xIn
    have above : x ≤ sSup(P)(S) := le_sSup with *
    exact le_trans with above, h
  . intro bound
    exact sSup_le with *

theorem le_sInf_iff (S : Set) (b ∈ points(P))
  requires hS : S ⊆ points(P)
  shows b ≤ sInf(P)(S) ↔ ∀ x ∈ S, b ≤ x
proof
  constructor
  . intros h x xIn
    have xIn2 : x ∈ points(P) := hS with x, xIn
    have below : sInf(P)(S) ≤ x := sInf_le with *
    exact le_trans with h, below
  . intro bound
    exact le_sInf with *

theorem sSup.of_isLUB (S s : Set)
  requires hS : S ⊆ points(P)
  requires lub : IsLUB(P, S, s)
  shows s = sSup(P)(S)
proof
  unfold IsLUB at lub
  rw sSup.supremum
  exact supremum.of_supremum with *

theorem sInf.of_isGLB (S i : Set)
  requires hS : S ⊆ points(P)
  requires glb : IsGLB(P, S, i)
  shows i = sInf(P)(S)
proof
  unfold IsGLB at glb
  rw sInf.infimum
  exact infimum.of_infimum with *

theorem sSup_le_sSup (S T : Set)
  requires hST : S ⊆ T
  requires hT : T ⊆ points(P)
  shows sSup(P)(S) ≤ sSup(P)(T)
proof
  unfold Le
  have hS : S ⊆ points(P) := Subset.transitive with hST, hT
  rw [sSup.supremum, sSup.supremum]
  exact supremum.monotone with *

theorem sInf_le_sInf (S T : Set)
  requires hST : S ⊆ T
  requires hT : T ⊆ points(P)
  shows sInf(P)(T) ≤ sInf(P)(S)
proof
  unfold Le
  have hS : S ⊆ points(P) := Subset.transitive with hST, hT
  rw [sInf.infimum, sInf.infimum]
  exact infimum.antitone with *

theorem sSup_pair (a b ∈ points(P))
  shows sSup(P)({a, b}) = a ⊔ b
proof
  have hS : {a, b} ⊆ points(P) by simp
  rw [sSup.supremum, sup.join]
  exact supremum.pair with *

theorem sInf_pair (a b ∈ points(P))
  shows sInf(P)({a, b}) = a ⊓ b
proof
  have hS : {a, b} ⊆ points(P) by simp
  rw [sInf.infimum, inf.meet]
  exact infimum.pair with *

theorem sSup_singleton (a ∈ points(P))
  shows sSup(P)({a}) = a
proof
  have hS : {a} ⊆ points(P) by simp
  rw sSup.supremum
  exact supremum.singleton with *

theorem sInf_singleton (a ∈ points(P))
  shows sInf(P)({a}) = a
proof
  have hS : {a} ⊆ points(P) by simp
  rw sInf.infimum
  exact infimum.singleton with *

theorem sSup_empty
  shows sSup(P)(∅) = bot(P)
proof
  have hS : ∅ ⊆ points(P) := empty.subset at points(P)
  have least : IsLeast(P, points(P), sSup(P)(∅))
    unfold IsLeast
    rw sSup.supremum
    exact supremum.empty with *
  exact bot_unique with *

theorem sInf_empty
  shows sInf(P)(∅) = top(P)
proof
  have hS : ∅ ⊆ points(P) := empty.subset at points(P)
  have greatest : IsGreatest(P, points(P), sInf(P)(∅))
    unfold IsGreatest
    rw sInf.infimum
    exact infimum.empty with *
  exact top_unique with *

theorem sSup_univ
  shows sSup(P)(points(P)) = top(P)
proof
  have hS : points(P) ⊆ points(P) := Subset.reflexive at points(P)
  have greatest : IsGreatest(P, points(P), sSup(P)(points(P)))
    unfold IsGreatest
    rw sSup.supremum
    exact supremum.whole with *
  exact top_unique with *

theorem sInf_univ
  shows sInf(P)(points(P)) = bot(P)
proof
  have hS : points(P) ⊆ points(P) := Subset.reflexive at points(P)
  have least : IsLeast(P, points(P), sInf(P)(points(P)))
    unfold IsLeast
    rw sInf.infimum
    exact infimum.whole with *
  exact bot_unique with *

theorem sSup_union (S T : Set)
  requires hS : S ⊆ points(P)
  requires hT : T ⊆ points(P)
  shows sSup(P)(S ∪ T) = sSup(P)(S) ⊔ sSup(P)(T)
proof
  have hST : S ∪ T ⊆ points(P) := union2.subset with *
  rw [sup.join, sSup.supremum, sSup.supremum, sSup.supremum]
  exact supremum.union2 with *

theorem sInf_union (S T : Set)
  requires hS : S ⊆ points(P)
  requires hT : T ⊆ points(P)
  shows sInf(P)(S ∪ T) = sInf(P)(S) ⊓ sInf(P)(T)
proof
  have hST : S ∪ T ⊆ points(P) := union2.subset with *
  rw [inf.meet, sInf.infimum, sInf.infimum, sInf.infimum]
  exact infimum.union2 with *

end CompleteLatticeLaws

-- The powerset of a set under inclusion is a complete lattice: join is
-- union, meet is intersection, and the supremum of a family is its union.
def powersetLattice (X : Set) : Set := Order.mk(𝒫(X), powersetOrder(X))

theorem powersetLattice.points (X : Set)
  shows points(powersetLattice(X)) = 𝒫(X)
proof
  simp [powersetLattice, Order.mk.points]

theorem powersetLattice.le (X : Set)
  shows le(powersetLattice(X)) = powersetOrder(X)
proof
  simp [powersetLattice, Order.mk.le]

instance powersetLattice.complete (X : Set)
  shows CompleteLattice(powersetLattice(X))
proof
  unfold powersetLattice
  exact CompleteLattice.mk with (IsCompleteLattice.powerset at X)

section PowersetLattice
variable (X : Set)
hypothesis complete : CompleteLattice(powersetLattice(X))

theorem powersetLattice.member (B : Set)
  requires hB : B ∈ 𝒫(X)
  shows B ∈ points(powersetLattice(X))
proof
  rw powersetLattice.points
  exact hB

theorem powersetLattice.le_iff (B C ∈ 𝒫(X))
  shows B ≤ C ↔ B ⊆ C
proof
  have characterization := powersetOrder.relates at X, B, C with *
  rw ← powersetLattice.le at characterization
  constructor
  . intro h
    exact characterization.forward with (Le.relates with h)
  . intro h
    exact Le.of_relates with (characterization.backward with h)

theorem powersetLattice.sup (B C ∈ 𝒫(X))
  shows B ⊔ C = B ∪ C
proof
  have BIn : B ∈ points(powersetLattice(X)) := powersetLattice.member at X, B with *
  have CIn : C ∈ points(powersetLattice(X)) := powersetLattice.member at X, C with *
  rw [sup.join, powersetLattice.points, powersetLattice.le]
  exact powersetOrder.join with *

theorem powersetLattice.inf (B C ∈ 𝒫(X))
  shows B ⊓ C = B ∩ C
proof
  have BIn : B ∈ points(powersetLattice(X)) := powersetLattice.member at X, B with *
  have CIn : C ∈ points(powersetLattice(X)) := powersetLattice.member at X, C with *
  rw [inf.meet, powersetLattice.points, powersetLattice.le]
  exact powersetOrder.meet with *

theorem powersetLattice.sSup (S : Set)
  requires hS : S ⊆ 𝒫(X)
  shows sSup(powersetLattice(X))(S) = ⋃(S)
proof
  have subset : S ⊆ points(powersetLattice(X))
    rw powersetLattice.points
    exact hS
  rw [sSup.supremum, powersetLattice.points, powersetLattice.le]
  exact powersetOrder.supremum_value with *

theorem powersetLattice.sInf (S : Set)
  requires hS : S ⊆ 𝒫(X)
  shows sInf(powersetLattice(X))(S) = relativeIntersection(X, S)
proof
  have subset : S ⊆ points(powersetLattice(X))
    rw powersetLattice.points
    exact hS
  rw [sInf.infimum, powersetLattice.points, powersetLattice.le]
  exact powersetOrder.infimum_value with *

theorem powersetLattice.bot
  shows bot(powersetLattice(X)) = ∅
proof
  unfold powersetLattice
  exact bot.mk with (powersetOrder.bounded at X)

theorem powersetLattice.top
  shows top(powersetLattice(X)) = X
proof
  unfold powersetLattice
  exact top.mk with (powersetOrder.bounded at X)

end PowersetLattice