-- Bounded lattices: least and greatest elements, and complementary pairs
-- 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.Bounded
import LatticeLaws

predicate IsBoundedLattice (A r bot top : Set) :=
  IsLattice(A, r) ∧ Least(A, r, A, bot) ∧ Greatest(A, r, A, top)

-- Two elements are complementary when they meet at the bottom and join
-- at the top.
predicate Complementary (A r bot top x y : Set) :=
  y ∈ A ∧ meet(A, r, x, y) = bot ∧ join(A, r, x, y) = top

theorem IsBoundedLattice.lattice (A r bot top : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  shows IsLattice(A, r)
proof
  simp [IsBoundedLattice]

theorem IsBoundedLattice.least (A r bot top : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  shows Least(A, r, A, bot)
proof
  simp [IsBoundedLattice]

theorem IsBoundedLattice.greatest (A r bot top : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  shows Greatest(A, r, A, top)
proof
  simp [IsBoundedLattice]

theorem IsBoundedLattice.of_bounds (A r bot top : Set)
  requires lattice : IsLattice(A, r)
  requires least : Least(A, r, A, bot)
  requires greatest : Greatest(A, r, A, top)
  shows IsBoundedLattice(A, r, bot, top)
proof
  refine ⟨lattice, least, greatest⟩

theorem IsBoundedLattice.bottom_member (A r bot top : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  shows bot ∈ A
proof
  exact Least.member with (IsBoundedLattice.least with h)

theorem IsBoundedLattice.top_member (A r bot top : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  shows top ∈ A
proof
  exact Greatest.member with (IsBoundedLattice.greatest with h)

theorem IsBoundedLattice.bottom_le (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows relates(r, bot, x)
proof
  exact Least.below with (IsBoundedLattice.least with h), hx

theorem IsBoundedLattice.le_top (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows relates(r, x, top)
proof
  exact Greatest.above with (IsBoundedLattice.greatest with h), hx

theorem IsBoundedLattice.nonempty (A r bot top : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  shows Nonempty(A)
proof
  refine ⟨bot, IsBoundedLattice.bottom_member with h⟩

theorem IsBoundedLattice.bottom_unique (A r bot top c : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hc : Least(A, r, A, c)
  shows c = bot
proof
  have order := IsLattice.order with (IsBoundedLattice.lattice with h)
  exact Least.unique with order, hc, (IsBoundedLattice.least with h)

theorem IsBoundedLattice.top_unique (A r bot top c : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hc : Greatest(A, r, A, c)
  shows c = top
proof
  have order := IsLattice.order with (IsBoundedLattice.lattice with h)
  exact Greatest.unique with order, hc, (IsBoundedLattice.greatest with h)

theorem IsBoundedLattice.le_bottom_iff (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows relates(r, x, bot) ↔ x = bot
proof
  have lattice := IsBoundedLattice.lattice with h
  have antisymmetric := IsLattice.antisymmetric with lattice
  have reflexive := IsLattice.reflexive with lattice
  have botA := IsBoundedLattice.bottom_member with h
  constructor
  . intro below
    have above := IsBoundedLattice.bottom_le with h, hx
    exact antisymmetric with x, hx, bot, botA, below, above
  . intro equal
    rw equal
    exact reflexive with bot, botA

theorem IsBoundedLattice.top_le_iff (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows relates(r, top, x) ↔ x = top
proof
  have lattice := IsBoundedLattice.lattice with h
  have antisymmetric := IsLattice.antisymmetric with lattice
  have reflexive := IsLattice.reflexive with lattice
  have topA := IsBoundedLattice.top_member with h
  constructor
  . intro above
    have below := IsBoundedLattice.le_top with h, hx
    exact antisymmetric with x, hx, top, topA, below, above
  . intro equal
    rw equal
    exact reflexive with top, topA

-- The bottom and top as units and absorbing elements

theorem join.bottom_right (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows join(A, r, x, bot) = x
proof
  have lattice := IsBoundedLattice.lattice with h
  have botA := IsBoundedLattice.bottom_member with h
  exact join.of_ge with lattice, hx, botA,
    (IsBoundedLattice.bottom_le with h, hx)

theorem join.bottom_left (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows join(A, r, bot, x) = x
proof
  have lattice := IsBoundedLattice.lattice with h
  have botA := IsBoundedLattice.bottom_member with h
  exact join.of_le with lattice, botA, hx,
    (IsBoundedLattice.bottom_le with h, hx)

theorem meet.bottom_right (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows meet(A, r, x, bot) = bot
proof
  have lattice := IsBoundedLattice.lattice with h
  have botA := IsBoundedLattice.bottom_member with h
  exact meet.of_ge with lattice, hx, botA,
    (IsBoundedLattice.bottom_le with h, hx)

theorem meet.bottom_left (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows meet(A, r, bot, x) = bot
proof
  have lattice := IsBoundedLattice.lattice with h
  have botA := IsBoundedLattice.bottom_member with h
  exact meet.of_le with lattice, botA, hx,
    (IsBoundedLattice.bottom_le with h, hx)

theorem join.top_right (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows join(A, r, x, top) = top
proof
  have lattice := IsBoundedLattice.lattice with h
  have topA := IsBoundedLattice.top_member with h
  exact join.of_le with lattice, hx, topA, (IsBoundedLattice.le_top with h, hx)

theorem join.top_left (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows join(A, r, top, x) = top
proof
  have lattice := IsBoundedLattice.lattice with h
  have topA := IsBoundedLattice.top_member with h
  exact join.of_ge with lattice, topA, hx, (IsBoundedLattice.le_top with h, hx)

theorem meet.top_right (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows meet(A, r, x, top) = x
proof
  have lattice := IsBoundedLattice.lattice with h
  have topA := IsBoundedLattice.top_member with h
  exact meet.of_le with lattice, hx, topA, (IsBoundedLattice.le_top with h, hx)

theorem meet.top_left (A r bot top x : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  shows meet(A, r, top, x) = x
proof
  have lattice := IsBoundedLattice.lattice with h
  have topA := IsBoundedLattice.top_member with h
  exact meet.of_ge with lattice, topA, hx, (IsBoundedLattice.le_top with h, hx)

theorem join.eq_bottom_iff (A r bot top x y : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows join(A, r, x, y) = bot ↔ x = bot ∧ y = bot
proof
  have lattice := IsBoundedLattice.lattice with h
  constructor
  . intro equal
    have xJ := join.upper_left with lattice, hx, hy
    have yJ := join.upper_right with lattice, hx, hy
    rw equal at xJ
    rw equal at yJ
    constructor
    . exact IsBoundedLattice.le_bottom_iff.forward with h, hx, xJ
    . exact IsBoundedLattice.le_bottom_iff.forward with h, hy, yJ
  . intro both
    rw [both.left, both.right]
    exact join.idempotent with lattice, (IsBoundedLattice.bottom_member with h)

theorem meet.eq_top_iff (A r bot top x y : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows meet(A, r, x, y) = top ↔ x = top ∧ y = top
proof
  have lattice := IsBoundedLattice.lattice with h
  constructor
  . intro equal
    have mX := meet.lower_left with lattice, hx, hy
    have mY := meet.lower_right with lattice, hx, hy
    rw equal at mX
    rw equal at mY
    constructor
    . exact IsBoundedLattice.top_le_iff.forward with h, hx, mX
    . exact IsBoundedLattice.top_le_iff.forward with h, hy, mY
  . intro both
    rw [both.left, both.right]
    exact meet.idempotent with lattice, (IsBoundedLattice.top_member with h)

-- The bounds as suprema and infima

theorem IsBoundedLattice.supremum_empty (A r bot top : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  shows Supremum(A, r, ∅, bot)
proof
  exact Supremum.empty_iff.backward with (IsBoundedLattice.least with h)

theorem IsBoundedLattice.infimum_empty (A r bot top : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  shows Infimum(A, r, ∅, top)
proof
  exact Infimum.empty_iff.backward with (IsBoundedLattice.greatest with h)

theorem IsBoundedLattice.supremum_whole (A r bot top : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  shows Supremum(A, r, A, top)
proof
  exact Supremum.whole_iff.backward with (IsBoundedLattice.greatest with h)

theorem IsBoundedLattice.infimum_whole (A r bot top : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  shows Infimum(A, r, A, bot)
proof
  exact Infimum.whole_iff.backward with (IsBoundedLattice.least with h)

theorem IsBoundedLattice.converse (A r bot top : Set)
  requires h : IsBoundedLattice(A, r, bot, top)
  shows IsBoundedLattice(A, converse(r, A, A), top, bot)
proof
  have lattice := IsBoundedLattice.lattice with h
  refine ⟨IsLattice.converse with lattice,
    Greatest.converse with (IsBoundedLattice.greatest with h),
    Least.converse with (IsBoundedLattice.least with h)⟩

-- Complementary pairs

theorem Complementary.member (A r bot top x y : Set)
  requires h : Complementary(A, r, bot, top, x, y)
  shows y ∈ A
proof
  simp [Complementary]

theorem Complementary.meet (A r bot top x y : Set)
  requires h : Complementary(A, r, bot, top, x, y)
  shows meet(A, r, x, y) = bot
proof
  rcases h with ⟨member, meetEq, joinEq⟩
  exact meetEq

theorem Complementary.join (A r bot top x y : Set)
  requires h : Complementary(A, r, bot, top, x, y)
  shows join(A, r, x, y) = top
proof
  rcases h with ⟨member, meetEq, joinEq⟩
  exact joinEq

theorem Complementary.symmetric (A r bot top x y : Set)
  requires bounded : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  requires h : Complementary(A, r, bot, top, x, y)
  shows Complementary(A, r, bot, top, y, x)
proof
  have lattice := IsBoundedLattice.lattice with bounded
  have hy := Complementary.member with h
  have meetSwap := meet.commutative with lattice, hy, hx
  have joinSwap := join.commutative with lattice, hy, hx
  refine ⟨hx, ?_, ?_⟩
  . rw meetSwap
    exact Complementary.meet with h
  . rw joinSwap
    exact Complementary.join with h

theorem Complementary.bottom_top (A r bot top : Set)
  requires bounded : IsBoundedLattice(A, r, bot, top)
  shows Complementary(A, r, bot, top, bot, top)
proof
  have botA := IsBoundedLattice.bottom_member with bounded
  have topA := IsBoundedLattice.top_member with bounded
  refine ⟨topA, (meet.bottom_left with bounded, topA),
      (join.top_right with bounded, botA)⟩

theorem Complementary.top_bottom (A r bot top : Set)
  requires bounded : IsBoundedLattice(A, r, bot, top)
  shows Complementary(A, r, bot, top, top, bot)
proof
  have botA := IsBoundedLattice.bottom_member with bounded
  have topA := IsBoundedLattice.top_member with bounded
  refine ⟨botA, (meet.bottom_right with bounded, topA),
      (join.top_left with bounded, botA)⟩

theorem Complementary.converse (A r bot top x y : Set)
  requires bounded : IsBoundedLattice(A, r, bot, top)
  requires hx : x ∈ A
  requires h : Complementary(A, r, bot, top, x, y)
  shows Complementary(A, converse(r, A, A), top, bot, x, y)
proof
  have lattice := IsBoundedLattice.lattice with bounded
  have hy := Complementary.member with h
  have joinDual := join.converse with lattice, hx, hy
  have meetDual := meet.converse with lattice, hx, hy
  refine ⟨hy, ?_, ?_⟩
  . rw meetDual
    exact Complementary.join with h
  . rw joinDual
    exact Complementary.meet with h