-- Ordered sets bundled as one set, with the order written ≤
-- 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.Order
import Bounds

-- An ordered set is a structure of its points and its order relation,
-- Order.mk(A, r). The projections read the two back: P.points is the
-- underlying set and P.le the relation on it, so that every order structure
-- is a property of the one set P. The order structures below are separate
-- predicates over the same data, so Order carries no laws of its own.
structure Order
  | points le : Set

-- The projection laws of a constructed order as one rewrite set.
tactic order_projections := simp [Order.mk.points, Order.mk.le]

-- The order structures, as properties of the bundled set. Each is the
-- unbundled predicate at the projections, so a hypothesis Preorder(P)
-- opens to IsPreorder(points(P), le(P)).
predicate Preorder (P : Set) := IsPreorder(points(P), le(P))
predicate PartialOrder (P : Set) := IsPartialOrder(points(P), le(P))
predicate LinearOrder (P : Set) := IsLinearOrder(points(P), le(P))

-- The order of P as a predicate of its own, written a ≤ b wherever a
-- hypothesis in scope supplies the ordered set; the operands' membership in
-- points(P) selects it when several are in scope. A fact a ≤ b opens to
-- relates(le(P), a, b) wherever local evidence is consulted.
predicate Le (P a b : Set) := relates(le(P), a, b)

notation infix 50 "≤" => Le(P, _, _) via hypothesis Preorder(P) for P.points
notation infix 50 "≤" => Le(P, _, _) via hypothesis PartialOrder(P) for P.points
notation infix 50 "≤" => Le(P, _, _) via hypothesis LinearOrder(P) for P.points

theorem Le.relates (P a b : Set)
  requires h : Le(P, a, b)
  shows relates(le(P), a, b)
proof
  simp [Le]

theorem Le.of_relates (P a b : Set)
  requires h : relates(le(P), a, b)
  shows Le(P, a, b)
proof
  simp [Le]

theorem Le.iff (P a b : Set)
  shows Le(P, a, b) ↔ relates(le(P), a, b)
proof
  simp [Le]

-- Bridges to the unbundled predicates: a structure on (A, r) is one on
-- Order.mk(A, r), and the instances let `with *` read the unbundled form
-- off a bundled hypothesis.
instance Preorder.unbundled (P : Set)
  requires order : Preorder(P)
  shows IsPreorder(points(P), le(P))
proof
  simp [Preorder]

instance PartialOrder.unbundled (P : Set)
  requires order : PartialOrder(P)
  shows IsPartialOrder(points(P), le(P))
proof
  simp [PartialOrder]

instance LinearOrder.unbundled (P : Set)
  requires order : LinearOrder(P)
  shows IsLinearOrder(points(P), le(P))
proof
  simp [LinearOrder]

theorem Preorder.mk (A r : Set)
  requires order : IsPreorder(A, r)
  shows Preorder(Order.mk(A, r))
proof
  unfold Preorder
  rw [Order.mk.points, Order.mk.le]
  exact order

theorem PartialOrder.mk (A r : Set)
  requires order : IsPartialOrder(A, r)
  shows PartialOrder(Order.mk(A, r))
proof
  unfold PartialOrder
  rw [Order.mk.points, Order.mk.le]
  exact order

theorem LinearOrder.mk (A r : Set)
  requires order : IsLinearOrder(A, r)
  shows LinearOrder(Order.mk(A, r))
proof
  unfold LinearOrder
  rw [Order.mk.points, Order.mk.le]
  exact order

instance PartialOrder.preorder_of (P : Set)
  requires order : PartialOrder(P)
  shows Preorder(P)
proof
  unfold Preorder
  exact IsPartialOrder.preorder with (PartialOrder.unbundled with order)

theorem LinearOrder.partial_order (P : Set)
  requires order : LinearOrder(P)
  shows PartialOrder(P)
proof
  unfold PartialOrder
  exact IsLinearOrder.partial with (LinearOrder.unbundled with order)

-- The order relation lives on the points.
theorem IsPreorder.relation (P : Set)
  requires order : Preorder(P)
  shows RelationBetween(le(P), points(P), points(P))
proof
  obtain ⟨relation, rest⟩ := Preorder.unbundled with order
  exact relation

section PreorderLaws
variable (P : Set)
hypothesis order : Preorder(P)

theorem le_refl (a ∈ points(P))
  shows a ≤ a
proof
  obtain ⟨relation, reflexive, transitive⟩ := Preorder.unbundled with order
  unfold Le
  exact reflexive with a, assumption

theorem le_trans (a b c ∈ points(P))
  requires hab : a ≤ b
  requires hbc : b ≤ c
  shows a ≤ c
proof
  obtain ⟨relation, reflexive, transitive⟩ := Preorder.unbundled with order
  unfold Le
  exact transitive with a, assumption, b, assumption, c, assumption, hab, hbc

end PreorderLaws

section PartialOrderLaws
variable (P : Set)
hypothesis order : PartialOrder(P)

theorem le_antisymm (a b ∈ points(P))
  requires hab : a ≤ b
  requires hba : b ≤ a
  shows a = b
proof
  have antisymmetric := IsPartialOrder.antisymmetric with (PartialOrder.unbundled with order)
  exact antisymmetric with a, assumption, b, assumption, hab, hba

theorem le_antisymm_iff (a b ∈ points(P))
  shows a = b ↔ (a ≤ b ∧ b ≤ a)
proof
  constructor
  . intro same
    rw same
    have reflexive : b ≤ b := le_refl with *
    exact ⟨reflexive, reflexive⟩
  . intro both
    obtain ⟨hab, hba⟩ := both
    exact le_antisymm with *

end PartialOrderLaws

section LinearOrderLaws
variable (P : Set)
hypothesis order : LinearOrder(P)

theorem le_total (a b ∈ points(P))
  shows a ≤ b ∨ b ≤ a
proof
  obtain ⟨partial, total⟩ := LinearOrder.unbundled with order
  have both := total with a, assumption, b, assumption
  cases both with ab | ba
  . left
    exact Le.of_relates with ab
  . right
    exact Le.of_relates with ba

end LinearOrderLaws

-- Bounds of a subset of a bundled order.
def upperBounds (P S : Set) : Set := { b ∈ points(P) | ∀ x ∈ S, relates(le(P), x, b) }
def lowerBounds (P S : Set) : Set := { b ∈ points(P) | ∀ x ∈ S, relates(le(P), b, x) }
predicate IsLUB (P S s : Set) := Supremum(points(P), le(P), S, s)
predicate IsGLB (P S i : Set) := Infimum(points(P), le(P), S, i)
predicate IsLeast (P S a : Set) := Least(points(P), le(P), S, a)
predicate IsGreatest (P S a : Set) := Greatest(points(P), le(P), S, a)

theorem upperBounds.of_upper_bound (P S b : Set)
  requires bound : UpperBound(points(P), le(P), S, b)
  shows b ∈ upperBounds(P, S)
proof
  obtain ⟨bIn, subset, above⟩ := bound
  apply upperBounds.membership.backward
  exact ⟨bIn, above⟩

theorem lowerBounds.of_lower_bound (P S b : Set)
  requires bound : LowerBound(points(P), le(P), S, b)
  shows b ∈ lowerBounds(P, S)
proof
  obtain ⟨bIn, subset, below⟩ := bound
  apply lowerBounds.membership.backward
  exact ⟨bIn, below⟩

section BoundLaws
variable (P : Set)
hypothesis order : PartialOrder(P)

theorem IsLUB.unique (S s t : Set)
  requires first : IsLUB(P, S, s)
  requires second : IsLUB(P, S, t)
  shows s = t
proof
  unfold IsLUB at first
  unfold IsLUB at second
  exact Supremum.unique with *

theorem IsGLB.unique (S i j : Set)
  requires first : IsGLB(P, S, i)
  requires second : IsGLB(P, S, j)
  shows i = j
proof
  unfold IsGLB at first
  unfold IsGLB at second
  exact Infimum.unique with *

theorem IsLUB.member (S s : Set)
  requires lub : IsLUB(P, S, s)
  shows s ∈ points(P)
proof
  unfold IsLUB at lub
  exact Supremum.member with lub

theorem IsGLB.member (S i : Set)
  requires glb : IsGLB(P, S, i)
  shows i ∈ points(P)
proof
  unfold IsGLB at glb
  exact Infimum.member with glb

theorem IsLUB.le_of_mem (S s x : Set)
  requires lub : IsLUB(P, S, s)
  requires xIn : x ∈ S
  shows x ≤ s
proof
  unfold IsLUB at lub
  unfold Le
  exact Supremum.above with lub, xIn

theorem IsGLB.le_of_mem (S i x : Set)
  requires glb : IsGLB(P, S, i)
  requires xIn : x ∈ S
  shows i ≤ x
proof
  unfold IsGLB at glb
  unfold Le
  exact Infimum.below with glb, xIn

theorem IsLUB.le_of_upper (S s b : Set)
  requires lub : IsLUB(P, S, s)
  requires bound : b ∈ upperBounds(P, S)
  shows s ≤ b
proof
  obtain ⟨upper, least⟩ := lub
  obtain ⟨bIn, above⟩ := upperBounds.membership.forward with bound
  have subset := UpperBound.subset with upper
  unfold Le
  exact least with b, bIn, ⟨bIn, subset, above⟩

theorem IsGLB.ge_of_lower (S i b : Set)
  requires glb : IsGLB(P, S, i)
  requires bound : b ∈ lowerBounds(P, S)
  shows b ≤ i
proof
  obtain ⟨lower, greatest⟩ := glb
  obtain ⟨bIn, below⟩ := lowerBounds.membership.forward with bound
  have subset := LowerBound.subset with lower
  unfold Le
  exact greatest with b, bIn, ⟨bIn, subset, below⟩

theorem IsGreatest.isLUB (S a : Set)
  requires greatest : IsGreatest(P, S, a)
  shows IsLUB(P, S, a)
proof
  unfold IsGreatest at greatest
  unfold IsLUB
  exact Greatest.supremum with *

theorem IsLeast.isGLB (S a : Set)
  requires least : IsLeast(P, S, a)
  shows IsGLB(P, S, a)
proof
  unfold IsLeast at least
  unfold IsGLB
  exact Least.infimum with *

end BoundLaws

-- The dual of a bundled order reverses the relation; suprema and infima
-- exchange.
def dual (P : Set) : Set := Order.mk(points(P), converse(le(P), points(P), points(P)))

theorem dual.points (P : Set)
  shows points(dual(P)) = points(P)
proof
  simp [dual, Order.mk.points]

theorem dual.le (P : Set)
  shows le(dual(P)) = converse(le(P), points(P), points(P))
proof
  simp [dual, Order.mk.le]

theorem PartialOrder.dual (P : Set)
  requires order : PartialOrder(P)
  shows PartialOrder(dual(P))
proof
  unfold dual
  apply PartialOrder.mk
  exact IsPartialOrder.converse with (PartialOrder.unbundled with order)

theorem IsLUB.dual (P S s : Set)
  requires order : PartialOrder(P)
  requires lub : IsLUB(P, S, s)
  shows IsGLB(dual(P), S, s)
proof
  unfold IsLUB at lub
  unfold IsGLB
  rw [dual.points, dual.le]
  exact Supremum.converse with *

theorem IsGLB.dual (P S i : Set)
  requires order : PartialOrder(P)
  requires glb : IsGLB(P, S, i)
  shows IsLUB(dual(P), S, i)
proof
  unfold IsGLB at glb
  unfold IsLUB
  rw [dual.points, dual.le]
  exact Infimum.converse with *