-- Lattices bundled as ordered sets, with join and meet written ⊔ and ⊓
-- 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.Join
import LatticeLaws
import Order

-- A lattice as a property of a bundled order. The join and meet of two
-- elements are set functions sup(P) and inf(P) on points(P) × points(P),
-- applied as a ⊔ b and a ⊓ b wherever a hypothesis Lattice(P) is in scope.
predicate Lattice (P : Set) := IsLattice(points(P), le(P))

instance Lattice.unbundled (P : Set)
  requires lattice : Lattice(P)
  shows IsLattice(points(P), le(P))
proof
  simp [Lattice]

theorem Lattice.mk (A r : Set)
  requires lattice : IsLattice(A, r)
  shows Lattice(Order.mk(A, r))
proof
  unfold Lattice
  rw [Order.mk.points, Order.mk.le]
  exact lattice

instance Lattice.partial_order (P : Set)
  requires lattice : Lattice(P)
  shows PartialOrder(P)
proof
  unfold Order.PartialOrder
  exact IsLattice.order with (Lattice.unbundled with lattice)

def pairJoin (P p : Set) : Set :=
  join(points(P), le(P), firstOf(points(P), points(P), p), secondOf(points(P), points(P), p))
def pairMeet (P p : Set) : Set :=
  meet(points(P), le(P), firstOf(points(P), points(P), p), secondOf(points(P), points(P), p))

theorem pairJoin.pair (P a b : Set)
  requires aIn : a ∈ points(P)
  requires bIn : b ∈ points(P)
  shows pairJoin(P, (a, b)) = join(points(P), le(P), a, b)
proof
  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *
  obtain ⟨firstIn, y, yIn, shape⟩ := firstOf.selected with pairIn
  obtain ⟨secondIn, x, xIn, shape2⟩ := secondOf.selected with pairIn
  have coordinates := orderedPair.injective with shape
  have coordinates2 := orderedPair.injective with shape2
  unfold pairJoin
  cc

theorem pairMeet.pair (P a b : Set)
  requires aIn : a ∈ points(P)
  requires bIn : b ∈ points(P)
  shows pairMeet(P, (a, b)) = meet(points(P), le(P), a, b)
proof
  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *
  obtain ⟨firstIn, y, yIn, shape⟩ := firstOf.selected with pairIn
  obtain ⟨secondIn, x, xIn, shape2⟩ := secondOf.selected with pairIn
  have coordinates := orderedPair.injective with shape
  have coordinates2 := orderedPair.injective with shape2
  unfold pairMeet
  cc

defgraph sup (P : Set) (p ∈ points(P) × points(P)) : points(P) := pairJoin(P, p)
requires lattice : Lattice(P)
proof
  have unbundled := Lattice.unbundled with lattice
  have first := firstOf.selected with member
  have second := secondOf.selected with member
  unfold pairJoin
  exact join.member with unbundled, first.left, second.left

defgraph inf (P : Set) (p ∈ points(P) × points(P)) : points(P) := pairMeet(P, p)
requires lattice : Lattice(P)
proof
  have unbundled := Lattice.unbundled with lattice
  have first := firstOf.selected with member
  have second := secondOf.selected with member
  unfold pairMeet
  exact meet.member with unbundled, first.left, second.left

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

section LatticeOperations
variable (P : Set)
hypothesis lattice : Lattice(P)

-- The bundled operations are the unbundled join and meet.
theorem sup.join (a b ∈ points(P))
  shows a ⊔ b = join(points(P), le(P), a, b)
proof
  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *
  have value := sup.value at P, (a, b) with lattice, pairIn
  have pair := pairJoin.pair at P, a, b with *
  unfold call2
  cc

theorem inf.meet (a b ∈ points(P))
  shows a ⊓ b = meet(points(P), le(P), a, b)
proof
  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *
  have value := inf.value at P, (a, b) with lattice, pairIn
  have pair := pairMeet.pair at P, a, b with *
  unfold call2
  cc

instance sup.member (a b ∈ points(P))
  shows a ⊔ b ∈ points(P)
proof
  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *
  have function := sup.function with lattice
  unfold call2
  exact FunctionBetween.apply_closed with function, pairIn

instance inf.member (a b ∈ points(P))
  shows a ⊓ b ∈ points(P)
proof
  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *
  have function := inf.function with lattice
  unfold call2
  exact FunctionBetween.apply_closed with function, pairIn

-- The defining properties of join and meet.
theorem le_sup_left (a b ∈ points(P))
  shows a ≤ a ⊔ b
proof
  unfold Le
  rw sup.join
  exact join.upper_left with *

theorem le_sup_right (a b ∈ points(P))
  shows b ≤ a ⊔ b
proof
  unfold Le
  rw sup.join
  exact join.upper_right with *

theorem sup_le (a b c ∈ points(P))
  requires hac : a ≤ c
  requires hbc : b ≤ c
  shows a ⊔ b ≤ c
proof
  unfold Le
  rw sup.join
  exact join.least with *

theorem inf_le_left (a b ∈ points(P))
  shows a ⊓ b ≤ a
proof
  unfold Le
  rw inf.meet
  exact meet.lower_left with *

theorem inf_le_right (a b ∈ points(P))
  shows a ⊓ b ≤ b
proof
  unfold Le
  rw inf.meet
  exact meet.lower_right with *

theorem le_inf (a b c ∈ points(P))
  requires hab : a ≤ b
  requires hac : a ≤ c
  shows a ≤ b ⊓ c
proof
  unfold Le
  rw inf.meet
  exact meet.greatest with *

theorem sup.isLUB (a b ∈ points(P))
  shows IsLUB(P, {a, b}, a ⊔ b)
proof
  unfold IsLUB
  rw sup.join
  exact join.supremum with *

theorem inf.isGLB (a b ∈ points(P))
  shows IsGLB(P, {a, b}, a ⊓ b)
proof
  unfold IsGLB
  rw inf.meet
  exact meet.infimum with *

theorem sup.of_isLUB (s : Set) (a b ∈ points(P))
  requires lub : IsLUB(P, {a, b}, s)
  shows s = a ⊔ b
proof
  unfold IsLUB at lub
  rw sup.join
  exact join.of_supremum with *

theorem inf.of_isGLB (i : Set) (a b ∈ points(P))
  requires glb : IsGLB(P, {a, b}, i)
  shows i = a ⊓ b
proof
  unfold IsGLB at glb
  rw inf.meet
  exact meet.of_infimum with *

end LatticeOperations

-- The equational laws of join and meet, and the order they determine.
section LatticeLaws
variable (P : Set)
hypothesis lattice : Lattice(P)

theorem sup_comm (a b ∈ points(P))
  shows a ⊔ b = b ⊔ a
proof
  have first : a ⊔ b ≤ b ⊔ a := sup_le with (le_sup_right with *), (le_sup_left with *)
  have second : b ⊔ a ≤ a ⊔ b := sup_le with (le_sup_right with *), (le_sup_left with *)
  exact le_antisymm with *

theorem inf_comm (a b ∈ points(P))
  shows a ⊓ b = b ⊓ a
proof
  have first : a ⊓ b ≤ b ⊓ a := le_inf with (inf_le_right with *), (inf_le_left with *)
  have second : b ⊓ a ≤ a ⊓ b := le_inf with (inf_le_right with *), (inf_le_left with *)
  exact le_antisymm with *

theorem sup_idem (a ∈ points(P))
  shows a ⊔ a = a
proof
  rw sup.join
  exact join.idempotent with *

theorem inf_idem (a ∈ points(P))
  shows a ⊓ a = a
proof
  rw inf.meet
  exact meet.idempotent with *

theorem sup_eq_right (a b ∈ points(P))
  requires hab : a ≤ b
  shows a ⊔ b = b
proof
  rw sup.join
  exact join.of_le with *

theorem sup_eq_left (a b ∈ points(P))
  requires hba : b ≤ a
  shows a ⊔ b = a
proof
  rw sup.join
  exact join.of_ge with *

theorem inf_eq_left (a b ∈ points(P))
  requires hab : a ≤ b
  shows a ⊓ b = a
proof
  rw inf.meet
  exact meet.of_le with *

theorem inf_eq_right (a b ∈ points(P))
  requires hba : b ≤ a
  shows a ⊓ b = b
proof
  rw inf.meet
  exact meet.of_ge with *

theorem sup_eq_right_iff (a b ∈ points(P))
  shows a ≤ b ↔ a ⊔ b = b
proof
  constructor
  . intro hab
    exact sup_eq_right with *
  . intro same
    have upper : a ≤ a ⊔ b := le_sup_left with *
    rwa same at upper

theorem inf_eq_left_iff (a b ∈ points(P))
  shows a ≤ b ↔ a ⊓ b = a
proof
  constructor
  . intro hab
    exact inf_eq_left with *
  . intro same
    have lower : a ⊓ b ≤ b := inf_le_right with *
    rwa same at lower

theorem sup_assoc (a b c ∈ points(P))
  shows (a ⊔ b) ⊔ c = a ⊔ (b ⊔ c)
proof
  simp [sup.join]
  exact join.associative with *

theorem inf_assoc (a b c ∈ points(P))
  shows (a ⊓ b) ⊓ c = a ⊓ (b ⊓ c)
proof
  simp [inf.meet]
  exact meet.associative with *

theorem sup_left_comm (a b c ∈ points(P))
  shows a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)
proof
  simp [sup.join]
  exact join.left_commutative with *

theorem inf_left_comm (a b c ∈ points(P))
  shows a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c)
proof
  simp [inf.meet]
  exact meet.left_commutative with *

theorem sup_absorb (a b ∈ points(P))
  shows a ⊔ (a ⊓ b) = a
proof
  simp [sup.join, inf.meet]
  exact join.absorb with *

theorem inf_absorb (a b ∈ points(P))
  shows a ⊓ (a ⊔ b) = a
proof
  simp [sup.join, inf.meet]
  exact meet.absorb with *

theorem sup_le_iff (a b c ∈ points(P))
  shows a ⊔ b ≤ c ↔ (a ≤ c ∧ b ≤ c)
proof
  constructor
  . intro h
    have left : a ≤ a ⊔ b := le_sup_left with *
    have right : b ≤ a ⊔ b := le_sup_right with *
    constructor
    . exact le_trans with left, h
    . exact le_trans with right, h
  . intro both
    obtain ⟨hac, hbc⟩ := both
    exact sup_le with *

theorem le_inf_iff (a b c ∈ points(P))
  shows a ≤ b ⊓ c ↔ (a ≤ b ∧ a ≤ c)
proof
  constructor
  . intro h
    have left : b ⊓ c ≤ b := inf_le_left with *
    have right : b ⊓ c ≤ c := inf_le_right with *
    constructor
    . exact le_trans with h, left
    . exact le_trans with h, right
  . intro both
    obtain ⟨hab, hac⟩ := both
    exact le_inf with *

theorem sup_le_sup (a b c d ∈ points(P))
  requires hac : a ≤ c
  requires hbd : b ≤ d
  shows a ⊔ b ≤ c ⊔ d
proof
  unfold Le
  rw [sup.join, sup.join]
  exact join.monotone with *

theorem inf_le_inf (a b c d ∈ points(P))
  requires hac : a ≤ c
  requires hbd : b ≤ d
  shows a ⊓ b ≤ c ⊓ d
proof
  unfold Le
  rw [inf.meet, inf.meet]
  exact meet.monotone with *

theorem sup_le_sup_left (a b c ∈ points(P))
  requires hbc : b ≤ c
  shows a ⊔ b ≤ a ⊔ c
proof
  unfold Le
  rw [sup.join, sup.join]
  exact join.monotone_right with *

theorem sup_le_sup_right (a b c ∈ points(P))
  requires hab : a ≤ b
  shows a ⊔ c ≤ b ⊔ c
proof
  unfold Le
  rw [sup.join, sup.join]
  exact join.monotone_left with *

theorem inf_le_inf_left (a b c ∈ points(P))
  requires hbc : b ≤ c
  shows a ⊓ b ≤ a ⊓ c
proof
  unfold Le
  rw [inf.meet, inf.meet]
  exact meet.monotone_right with *

theorem inf_le_inf_right (a b c ∈ points(P))
  requires hab : a ≤ b
  shows a ⊓ c ≤ b ⊓ c
proof
  unfold Le
  rw [inf.meet, inf.meet]
  exact meet.monotone_left with *

theorem le_sup_of_le_left (a b c ∈ points(P))
  requires hab : a ≤ b
  shows a ≤ b ⊔ c
proof
  exact le_trans with hab, (le_sup_left with *)

theorem le_sup_of_le_right (a b c ∈ points(P))
  requires hac : a ≤ c
  shows a ≤ b ⊔ c
proof
  exact le_trans with hac, (le_sup_right with *)

theorem inf_le_of_left_le (a b c ∈ points(P))
  requires hac : a ≤ c
  shows a ⊓ b ≤ c
proof
  exact le_trans with (inf_le_left with *), hac

theorem inf_le_of_right_le (a b c ∈ points(P))
  requires hbc : b ≤ c
  shows a ⊓ b ≤ c
proof
  exact le_trans with (inf_le_right with *), hbc

theorem inf_le_sup (a b ∈ points(P))
  shows a ⊓ b ≤ a ⊔ b
proof
  unfold Le
  rw [inf.meet, sup.join]
  exact meet.le_join with *

-- The distributive and modular inequalities, which hold in every lattice.
theorem sup_inf_le_inf_sup (a b c ∈ points(P))
  shows (a ⊓ b) ⊔ (a ⊓ c) ≤ a ⊓ (b ⊔ c)
proof
  unfold Le
  rw [inf.meet, inf.meet, sup.join, sup.join, inf.meet]
  exact meet.join_distributive_le with *

theorem sup_inf_le_inf_sup_sup (a b c ∈ points(P))
  shows a ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)
proof
  unfold Le
  rw [inf.meet, sup.join, sup.join, sup.join, inf.meet]
  exact join.meet_distributive_ge with *

theorem sup_inf_le_of_le (a b c ∈ points(P))
  requires hba : b ≤ a
  shows b ⊔ (a ⊓ c) ≤ a ⊓ (b ⊔ c)
proof
  unfold Le
  rw [inf.meet, sup.join, sup.join, inf.meet]
  exact join.modular_le with *

end LatticeLaws

-- The lattice rewrite set: idempotency, absorption, associativity, and the
-- bounds of a join and a meet, each applied where the memberships of its
-- elements are in scope.
tactic lattice_simp := simp [sup_idem, inf_idem, sup_absorb, inf_absorb, sup_assoc, inf_assoc, le_sup_left, le_sup_right, inf_le_left, inf_le_right, le_refl]