-- Suprema and infima of subsets of an ordered set, and order duality
-- 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.Bounds
import Set.Order

-- A supremum is a least upper bound; an infimum is a greatest lower bound.
predicate Supremum (A r S s : Set) :=
  UpperBound(A, r, S, s) ∧ (∀ b ∈ A, UpperBound(A, r, S, b) → relates(r, s, b))
predicate Infimum (A r S i : Set) :=
  LowerBound(A, r, S, i) ∧ (∀ b ∈ A, LowerBound(A, r, S, b) → relates(r, b, i))

-- Projections of the bound predicates

theorem UpperBound.member (A r S a : Set)
  requires h : UpperBound(A, r, S, a)
  shows a ∈ A
proof
  simp [UpperBound]

theorem UpperBound.subset (A r S a : Set)
  requires h : UpperBound(A, r, S, a)
  shows S ⊆ A
proof
  simp [UpperBound]

theorem UpperBound.above (A r S a x : Set)
  requires h : UpperBound(A, r, S, a)
  requires hx : x ∈ S
  shows relates(r, x, a)
proof
  rcases h with ⟨member, bounded, above⟩
  exact above with x, hx

theorem LowerBound.member (A r S a : Set)
  requires h : LowerBound(A, r, S, a)
  shows a ∈ A
proof
  simp [LowerBound]

theorem LowerBound.subset (A r S a : Set)
  requires h : LowerBound(A, r, S, a)
  shows S ⊆ A
proof
  simp [LowerBound]

theorem LowerBound.below (A r S a x : Set)
  requires h : LowerBound(A, r, S, a)
  requires hx : x ∈ S
  shows relates(r, a, x)
proof
  rcases h with ⟨member, bounded, below⟩
  exact below with x, hx

theorem Least.member (A r S a : Set)
  requires h : Least(A, r, S, a)
  shows a ∈ S
proof
  simp [Least]

theorem Least.lower (A r S a : Set)
  requires h : Least(A, r, S, a)
  shows LowerBound(A, r, S, a)
proof
  simp [Least]

theorem Least.below (A r S a x : Set)
  requires h : Least(A, r, S, a)
  requires hx : x ∈ S
  shows relates(r, a, x)
proof
  have lower := Least.lower with h
  exact LowerBound.below with lower, hx

theorem Greatest.member (A r S a : Set)
  requires h : Greatest(A, r, S, a)
  shows a ∈ S
proof
  simp [Greatest]

theorem Greatest.upper (A r S a : Set)
  requires h : Greatest(A, r, S, a)
  shows UpperBound(A, r, S, a)
proof
  simp [Greatest]

theorem Greatest.above (A r S a x : Set)
  requires h : Greatest(A, r, S, a)
  requires hx : x ∈ S
  shows relates(r, x, a)
proof
  have upper := Greatest.upper with h
  exact UpperBound.above with upper, hx

-- Bounds of the empty set, of subsets, and of pairs

theorem UpperBound.empty (A r a : Set)
  requires ha : a ∈ A
  shows UpperBound(A, r, ∅, a)
proof
  refine ⟨ha, empty.subset at A, ?_⟩
  intros x hx
  exfalso
  exact set.empty with hx

theorem LowerBound.empty (A r a : Set)
  requires ha : a ∈ A
  shows LowerBound(A, r, ∅, a)
proof
  refine ⟨ha, empty.subset at A, ?_⟩
  intros x hx
  exfalso
  exact set.empty with hx

theorem UpperBound.antitone (A r S T a : Set)
  requires hST : S ⊆ T
  requires h : UpperBound(A, r, T, a)
  shows UpperBound(A, r, S, a)
proof
  rcases h with ⟨member, bounded, above⟩
  refine ⟨member, (Subset.transitive with hST, bounded), ?_⟩
  intros x hx
  exact above with x, (hST with x, hx)

theorem LowerBound.antitone (A r S T a : Set)
  requires hST : S ⊆ T
  requires h : LowerBound(A, r, T, a)
  shows LowerBound(A, r, S, a)
proof
  rcases h with ⟨member, bounded, below⟩
  refine ⟨member, (Subset.transitive with hST, bounded), ?_⟩
  intros x hx
  exact below with x, (hST with x, hx)

theorem UpperBound.raise (A r S a b : Set)
  requires order : IsPartialOrder(A, r)
  requires h : UpperBound(A, r, S, a)
  requires hb : b ∈ A
  requires hab : relates(r, a, b)
  shows UpperBound(A, r, S, b)
proof
  have transitive := IsPartialOrder.transitive with order
  rcases h with ⟨member, bounded, above⟩
  refine ⟨hb, bounded, ?_⟩
  intros x hx
  have xA := bounded with x, hx
  exact transitive with x, xA, a, member, b, hb, (above with x, hx), hab

theorem LowerBound.lower (A r S a b : Set)
  requires order : IsPartialOrder(A, r)
  requires h : LowerBound(A, r, S, a)
  requires hb : b ∈ A
  requires hba : relates(r, b, a)
  shows LowerBound(A, r, S, b)
proof
  have transitive := IsPartialOrder.transitive with order
  rcases h with ⟨member, bounded, below⟩
  refine ⟨hb, bounded, ?_⟩
  intros x hx
  have xA := bounded with x, hx
  exact transitive with b, hb, a, member, x, xA, hba, (below with x, hx)

theorem UpperBound.singleton (A r x : Set)
  requires order : IsPartialOrder(A, r)
  requires hx : x ∈ A
  shows UpperBound(A, r, {x}, x)
proof
  have reflexive := IsPartialOrder.reflexive with order
  have bounded : {x} ⊆ A by simp
  refine ⟨hx, bounded, ?_⟩
  intros y hy
  have equal := singleton.membership.forward with hy
  rw equal
  exact reflexive with x, hx

theorem LowerBound.singleton (A r x : Set)
  requires order : IsPartialOrder(A, r)
  requires hx : x ∈ A
  shows LowerBound(A, r, {x}, x)
proof
  have reflexive := IsPartialOrder.reflexive with order
  have bounded : {x} ⊆ A by simp
  refine ⟨hx, bounded, ?_⟩
  intros y hy
  have equal := singleton.membership.forward with hy
  rw equal
  exact reflexive with x, hx

theorem UpperBound.pair (A r x y a : Set)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires ha : a ∈ A
  requires hxa : relates(r, x, a)
  requires hya : relates(r, y, a)
  shows UpperBound(A, r, {x, y}, a)
proof
  have bounded : {x, y} ⊆ A by simp
  refine ⟨ha, bounded, ?_⟩
  intros z hz
  have cases := pair.membership.forward with hz
  cases cases with zx | zy
  . rw zx
    exact hxa
  . rw zy
    exact hya

theorem LowerBound.pair (A r x y a : Set)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires ha : a ∈ A
  requires hax : relates(r, a, x)
  requires hay : relates(r, a, y)
  shows LowerBound(A, r, {x, y}, a)
proof
  have bounded : {x, y} ⊆ A by simp
  refine ⟨ha, bounded, ?_⟩
  intros z hz
  have cases := pair.membership.forward with hz
  cases cases with zx | zy
  . rw zx
    exact hax
  . rw zy
    exact hay

theorem UpperBound.pair_left (A r x y a : Set)
  requires h : UpperBound(A, r, {x, y}, a)
  shows relates(r, x, a)
proof
  exact UpperBound.above with h, (pair.left at x, y)

theorem UpperBound.pair_right (A r x y a : Set)
  requires h : UpperBound(A, r, {x, y}, a)
  shows relates(r, y, a)
proof
  exact UpperBound.above with h, (pair.right at x, y)

theorem LowerBound.pair_left (A r x y a : Set)
  requires h : LowerBound(A, r, {x, y}, a)
  shows relates(r, a, x)
proof
  exact LowerBound.below with h, (pair.left at x, y)

theorem LowerBound.pair_right (A r x y a : Set)
  requires h : LowerBound(A, r, {x, y}, a)
  shows relates(r, a, y)
proof
  exact LowerBound.below with h, (pair.right at x, y)

-- Projections of suprema and infima

theorem Supremum.upper (A r S s : Set)
  requires h : Supremum(A, r, S, s)
  shows UpperBound(A, r, S, s)
proof
  simp [Supremum]

theorem Supremum.least (A r S s b : Set)
  requires h : Supremum(A, r, S, s)
  requires hb : b ∈ A
  requires bound : UpperBound(A, r, S, b)
  shows relates(r, s, b)
proof
  rcases h with ⟨upper, least⟩
  exact least with b, hb, bound

theorem Supremum.member (A r S s : Set)
  requires h : Supremum(A, r, S, s)
  shows s ∈ A
proof
  exact UpperBound.member with (Supremum.upper with h)

theorem Supremum.subset (A r S s : Set)
  requires h : Supremum(A, r, S, s)
  shows S ⊆ A
proof
  exact UpperBound.subset with (Supremum.upper with h)

theorem Supremum.above (A r S s x : Set)
  requires h : Supremum(A, r, S, s)
  requires hx : x ∈ S
  shows relates(r, x, s)
proof
  exact UpperBound.above with (Supremum.upper with h), hx

theorem Infimum.lower (A r S i : Set)
  requires h : Infimum(A, r, S, i)
  shows LowerBound(A, r, S, i)
proof
  simp [Infimum]

theorem Infimum.greatest (A r S i b : Set)
  requires h : Infimum(A, r, S, i)
  requires hb : b ∈ A
  requires bound : LowerBound(A, r, S, b)
  shows relates(r, b, i)
proof
  rcases h with ⟨lower, greatest⟩
  exact greatest with b, hb, bound

theorem Infimum.member (A r S i : Set)
  requires h : Infimum(A, r, S, i)
  shows i ∈ A
proof
  exact LowerBound.member with (Infimum.lower with h)

theorem Infimum.subset (A r S i : Set)
  requires h : Infimum(A, r, S, i)
  shows S ⊆ A
proof
  exact LowerBound.subset with (Infimum.lower with h)

theorem Infimum.below (A r S i x : Set)
  requires h : Infimum(A, r, S, i)
  requires hx : x ∈ S
  shows relates(r, i, x)
proof
  exact LowerBound.below with (Infimum.lower with h), hx

-- Uniqueness

theorem Supremum.unique (A r S s t : Set)
  requires order : IsPartialOrder(A, r)
  requires hs : Supremum(A, r, S, s)
  requires ht : Supremum(A, r, S, t)
  shows s = t
proof
  have antisymmetric := IsPartialOrder.antisymmetric with order
  have sA := Supremum.member with hs
  have tA := Supremum.member with ht
  have st := Supremum.least with hs, tA, (Supremum.upper with ht)
  have ts := Supremum.least with ht, sA, (Supremum.upper with hs)
  exact antisymmetric with s, sA, t, tA, st, ts

theorem Infimum.unique (A r S i j : Set)
  requires order : IsPartialOrder(A, r)
  requires hi : Infimum(A, r, S, i)
  requires hj : Infimum(A, r, S, j)
  shows i = j
proof
  have antisymmetric := IsPartialOrder.antisymmetric with order
  have iA := Infimum.member with hi
  have jA := Infimum.member with hj
  have ji := Infimum.greatest with hi, jA, (Infimum.lower with hj)
  have ij := Infimum.greatest with hj, iA, (Infimum.lower with hi)
  exact antisymmetric with i, iA, j, jA, ij, ji

-- Greatest elements are suprema, and a supremum that belongs to the set
-- is its greatest element.

theorem Greatest.supremum (A r S g : Set)
  requires h : Greatest(A, r, S, g)
  shows Supremum(A, r, S, g)
proof
  rcases h with ⟨member, upper⟩
  constructor
  . exact upper
  . intros b hb bound
    exact UpperBound.above with bound, member

theorem Least.infimum (A r S l : Set)
  requires h : Least(A, r, S, l)
  shows Infimum(A, r, S, l)
proof
  rcases h with ⟨member, lower⟩
  constructor
  . exact lower
  . intros b hb bound
    exact LowerBound.below with bound, member

theorem Supremum.greatest_of_member (A r S s : Set)
  requires h : Supremum(A, r, S, s)
  requires hs : s ∈ S
  shows Greatest(A, r, S, s)
proof
  refine ⟨hs, Supremum.upper with h⟩

theorem Infimum.least_of_member (A r S i : Set)
  requires h : Infimum(A, r, S, i)
  requires hi : i ∈ S
  shows Least(A, r, S, i)
proof
  refine ⟨hi, Infimum.lower with h⟩

-- The empty set and the whole points

theorem Supremum.empty_iff (A r s : Set)
  shows Supremum(A, r, ∅, s) ↔ Least(A, r, A, s)
proof
  constructor
  . intro h
    have sA := Supremum.member with h
    constructor
    . exact sA
    . refine ⟨sA, Subset.reflexive at A, ?_⟩
      intros x hx
      exact Supremum.least with h, hx, (UpperBound.empty at A, r, x with hx)
  . intro h
    rcases h with ⟨sA, _, _, below⟩
    constructor
    . exact UpperBound.empty with sA
    . intros b hb bound
      exact below with b, hb

theorem Infimum.empty_iff (A r i : Set)
  shows Infimum(A, r, ∅, i) ↔ Greatest(A, r, A, i)
proof
  constructor
  . intro h
    have iA := Infimum.member with h
    constructor
    . exact iA
    . refine ⟨iA, Subset.reflexive at A, ?_⟩
      intros x hx
      exact Infimum.greatest with h, hx, (LowerBound.empty at A, r, x with hx)
  . intro h
    rcases h with ⟨iA, _, _, above⟩
    constructor
    . exact LowerBound.empty with iA
    . intros b hb bound
      exact above with b, hb

theorem Supremum.whole_iff (A r s : Set)
  shows Supremum(A, r, A, s) ↔ Greatest(A, r, A, s)
proof
  constructor
  . intro h
    exact Supremum.greatest_of_member with h, (Supremum.member with h)
  . intro h
    exact Greatest.supremum with h

theorem Infimum.whole_iff (A r i : Set)
  shows Infimum(A, r, A, i) ↔ Least(A, r, A, i)
proof
  constructor
  . intro h
    exact Infimum.least_of_member with h, (Infimum.member with h)
  . intro h
    exact Least.infimum with h

-- Singletons and pairs

theorem Supremum.singleton (A r x : Set)
  requires order : IsPartialOrder(A, r)
  requires hx : x ∈ A
  shows Supremum(A, r, {x}, x)
proof
  constructor
  . exact UpperBound.singleton with order, hx
  . intros b hb bound
    exact UpperBound.above with bound, (singleton.self at x)

theorem Infimum.singleton (A r x : Set)
  requires order : IsPartialOrder(A, r)
  requires hx : x ∈ A
  shows Infimum(A, r, {x}, x)
proof
  constructor
  . exact LowerBound.singleton with order, hx
  . intros b hb bound
    exact LowerBound.below with bound, (singleton.self at x)

theorem Supremum.of_pair (A r x y s : Set)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hs : s ∈ A
  requires hxs : relates(r, x, s)
  requires hys : relates(r, y, s)
  requires least :
    ∀ b ∈ A, relates(r, x, b) → relates(r, y, b) → relates(r, s, b)
  shows Supremum(A, r, {x, y}, s)
proof
  constructor
  . exact UpperBound.pair with hx, hy, hs, hxs, hys
  . intros b hb bound
    have xb := UpperBound.pair_left with bound
    have yb := UpperBound.pair_right with bound
    exact least with b, hb, xb, yb

theorem Infimum.of_pair (A r x y i : Set)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hi : i ∈ A
  requires hix : relates(r, i, x)
  requires hiy : relates(r, i, y)
  requires greatest :
    ∀ b ∈ A, relates(r, b, x) → relates(r, b, y) → relates(r, b, i)
  shows Infimum(A, r, {x, y}, i)
proof
  constructor
  . exact LowerBound.pair with hx, hy, hi, hix, hiy
  . intros b hb bound
    have bx := LowerBound.pair_left with bound
    have byBound := LowerBound.pair_right with bound
    exact greatest with b, hb, bx, byBound

theorem Supremum.pair_left (A r x y s : Set)
  requires h : Supremum(A, r, {x, y}, s)
  shows relates(r, x, s)
proof
  exact UpperBound.pair_left with (Supremum.upper with h)

theorem Supremum.pair_right (A r x y s : Set)
  requires h : Supremum(A, r, {x, y}, s)
  shows relates(r, y, s)
proof
  exact UpperBound.pair_right with (Supremum.upper with h)

theorem Supremum.pair_least (A r x y s b : Set)
  requires h : Supremum(A, r, {x, y}, s)
  requires hb : b ∈ A
  requires hxb : relates(r, x, b)
  requires hyb : relates(r, y, b)
  shows relates(r, s, b)
proof
  have bounded := Supremum.subset with h
  have xA := bounded with x, (pair.left at x, y)
  have yA := bounded with y, (pair.right at x, y)
  have bound := UpperBound.pair with xA, yA, hb, hxb, hyb
  exact Supremum.least with h, hb, bound

theorem Infimum.pair_left (A r x y i : Set)
  requires h : Infimum(A, r, {x, y}, i)
  shows relates(r, i, x)
proof
  exact LowerBound.pair_left with (Infimum.lower with h)

theorem Infimum.pair_right (A r x y i : Set)
  requires h : Infimum(A, r, {x, y}, i)
  shows relates(r, i, y)
proof
  exact LowerBound.pair_right with (Infimum.lower with h)

theorem Infimum.pair_greatest (A r x y i b : Set)
  requires h : Infimum(A, r, {x, y}, i)
  requires hb : b ∈ A
  requires hbx : relates(r, b, x)
  requires hby : relates(r, b, y)
  shows relates(r, b, i)
proof
  have bounded := Infimum.subset with h
  have xA := bounded with x, (pair.left at x, y)
  have yA := bounded with y, (pair.right at x, y)
  have bound := LowerBound.pair with xA, yA, hb, hbx, hby
  exact Infimum.greatest with h, hb, bound

-- Monotonicity in the set

theorem Supremum.monotone (A r S T s t : Set)
  requires hST : S ⊆ T
  requires hs : Supremum(A, r, S, s)
  requires ht : Supremum(A, r, T, t)
  shows relates(r, s, t)
proof
  have tA := Supremum.member with ht
  have bound := UpperBound.antitone with hST, (Supremum.upper with ht)
  exact Supremum.least with hs, tA, bound

theorem Infimum.antitone (A r S T i j : Set)
  requires hST : S ⊆ T
  requires hi : Infimum(A, r, S, i)
  requires hj : Infimum(A, r, T, j)
  shows relates(r, j, i)
proof
  have jA := Infimum.member with hj
  have bound := LowerBound.antitone with hST, (Infimum.lower with hj)
  exact Infimum.greatest with hi, jA, bound

-- Duality: the converse of an order exchanges the two notions.

theorem IsPartialOrder.converse (A r : Set)
  requires order : IsPartialOrder(A, r)
  shows IsPartialOrder(A, converse(r, A, A))
proof
  have reflexive := IsPartialOrder.reflexive with order
  have transitive := IsPartialOrder.transitive with order
  have antisymmetric := IsPartialOrder.antisymmetric with order
  constructor
  . constructor
    . exact converse.relation at r, A, A
    . constructor
      . intros x hx
        exact converse.relates with hx, hx, (reflexive with x, hx)
      . intros x hx y hy z hz xy yz
        have yx := converse.reflects with xy
        have zy := converse.reflects with yz
        have zx := transitive with z, hz, y, hy, x, hx, zy, yx
        exact converse.relates with hz, hx, zx
  . intros x hx y hy xy yx
    have yxR := converse.reflects with xy
    have xyR := converse.reflects with yx
    exact antisymmetric with x, hx, y, hy, xyR, yxR

theorem UpperBound.converse (A r S a : Set)
  requires h : UpperBound(A, r, S, a)
  shows LowerBound(A, converse(r, A, A), S, a)
proof
  rcases h with ⟨member, bounded, above⟩
  refine ⟨member, bounded, ?_⟩
  intros x hx
  have xA := bounded with x, hx
  exact converse.relates with xA, member, (above with x, hx)

theorem LowerBound.converse (A r S a : Set)
  requires h : LowerBound(A, r, S, a)
  shows UpperBound(A, converse(r, A, A), S, a)
proof
  rcases h with ⟨member, bounded, below⟩
  refine ⟨member, bounded, ?_⟩
  intros x hx
  have xA := bounded with x, hx
  exact converse.relates with member, xA, (below with x, hx)

theorem UpperBound.of_converse (A r S a : Set)
  requires h : UpperBound(A, converse(r, A, A), S, a)
  shows LowerBound(A, r, S, a)
proof
  rcases h with ⟨member, bounded, above⟩
  refine ⟨member, bounded, ?_⟩
  intros x hx
  exact converse.reflects with (above with x, hx)

theorem LowerBound.of_converse (A r S a : Set)
  requires h : LowerBound(A, converse(r, A, A), S, a)
  shows UpperBound(A, r, S, a)
proof
  rcases h with ⟨member, bounded, below⟩
  refine ⟨member, bounded, ?_⟩
  intros x hx
  exact converse.reflects with (below with x, hx)

theorem Supremum.converse (A r S s : Set)
  requires h : Supremum(A, r, S, s)
  shows Infimum(A, converse(r, A, A), S, s)
proof
  have sA := Supremum.member with h
  constructor
  . exact UpperBound.converse with (Supremum.upper with h)
  . intros b hb bound
    have upper := LowerBound.of_converse with bound
    have sb := Supremum.least with h, hb, upper
    exact converse.relates with sA, hb, sb

theorem Infimum.converse (A r S i : Set)
  requires h : Infimum(A, r, S, i)
  shows Supremum(A, converse(r, A, A), S, i)
proof
  have iA := Infimum.member with h
  constructor
  . exact LowerBound.converse with (Infimum.lower with h)
  . intros b hb bound
    have lower := UpperBound.of_converse with bound
    have bi := Infimum.greatest with h, hb, lower
    exact converse.relates with hb, iA, bi

theorem Supremum.of_converse (A r S s : Set)
  requires h : Supremum(A, converse(r, A, A), S, s)
  shows Infimum(A, r, S, s)
proof
  have sA := Supremum.member with h
  constructor
  . exact UpperBound.of_converse with (Supremum.upper with h)
  . intros b hb bound
    have upper := LowerBound.converse with bound
    have sb := Supremum.least with h, hb, upper
    exact converse.reflects with sb

theorem Infimum.of_converse (A r S i : Set)
  requires h : Infimum(A, converse(r, A, A), S, i)
  shows Supremum(A, r, S, i)
proof
  have iA := Infimum.member with h
  constructor
  . exact LowerBound.of_converse with (Infimum.lower with h)
  . intros b hb bound
    have lower := UpperBound.converse with bound
    have bi := Infimum.greatest with h, hb, lower
    exact converse.reflects with bi

theorem Least.converse (A r S a : Set)
  requires h : Least(A, r, S, a)
  shows Greatest(A, converse(r, A, A), S, a)
proof
  rcases h with ⟨member, lower⟩
  refine ⟨member, LowerBound.converse with lower⟩

theorem Greatest.converse (A r S a : Set)
  requires h : Greatest(A, r, S, a)
  shows Least(A, converse(r, A, A), S, a)
proof
  rcases h with ⟨member, upper⟩
  refine ⟨member, UpperBound.converse with upper⟩