------------------------------------------------------------------------
-- The Agda standard library
--
-- Order-theoretic lattices
------------------------------------------------------------------------
{-# OPTIONS --without-K --safe #-}
module Relation.Binary.Lattice where
open import Algebra.Core
open import Algebra.Definitions
open import Data.Product using (_×_; _,_)
open import Function.Base using (flip)
open import Level using (suc; _⊔_)
open import Relation.Binary
------------------------------------------------------------------------
-- Relationships between orders and operators
open import Relation.Binary public using (Maximum; Minimum)
Supremum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Op₂ A → Set _
Supremum _≤_ _∨_ =
∀ x y → x ≤ (x ∨ y) × y ≤ (x ∨ y) × ∀ z → x ≤ z → y ≤ z → (x ∨ y) ≤ z
Infimum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Op₂ A → Set _
Infimum _≤_ = Supremum (flip _≤_)
Exponential : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Op₂ A → Op₂ A → Set _
Exponential _≤_ _∧_ _⇨_ =
∀ w x y → ((w ∧ x) ≤ y → w ≤ (x ⇨ y)) × (w ≤ (x ⇨ y) → (w ∧ x) ≤ y)
------------------------------------------------------------------------
-- Join semilattices
record IsJoinSemilattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) -- The underlying equality.
(_≤_ : Rel A ℓ₂) -- The partial order.
(_∨_ : Op₂ A) -- The join operation.
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isPartialOrder : IsPartialOrder _≈_ _≤_
supremum : Supremum _≤_ _∨_
x≤x∨y : ∀ x y → x ≤ (x ∨ y)
x≤x∨y x y = let pf , _ , _ = supremum x y in pf
y≤x∨y : ∀ x y → y ≤ (x ∨ y)
y≤x∨y x y = let _ , pf , _ = supremum x y in pf
∨-least : ∀ {x y z} → x ≤ z → y ≤ z → (x ∨ y) ≤ z
∨-least {x} {y} {z} = let _ , _ , pf = supremum x y in pf z
open IsPartialOrder isPartialOrder public
record JoinSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
_≤_ : Rel Carrier ℓ₂ -- The partial order.
_∨_ : Op₂ Carrier -- The join operation.
isJoinSemilattice : IsJoinSemilattice _≈_ _≤_ _∨_
open IsJoinSemilattice isJoinSemilattice public
poset : Poset c ℓ₁ ℓ₂
poset = record { isPartialOrder = isPartialOrder }
open Poset poset public using (preorder)
record IsBoundedJoinSemilattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) -- The underlying equality.
(_≤_ : Rel A ℓ₂) -- The partial order.
(_∨_ : Op₂ A) -- The join operation.
(⊥ : A) -- The minimum.
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isJoinSemilattice : IsJoinSemilattice _≈_ _≤_ _∨_
minimum : Minimum _≤_ ⊥
open IsJoinSemilattice isJoinSemilattice public
record BoundedJoinSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
_≤_ : Rel Carrier ℓ₂ -- The partial order.
_∨_ : Op₂ Carrier -- The join operation.
⊥ : Carrier -- The minimum.
isBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ _≤_ _∨_ ⊥
open IsBoundedJoinSemilattice isBoundedJoinSemilattice public
joinSemilattice : JoinSemilattice c ℓ₁ ℓ₂
joinSemilattice = record { isJoinSemilattice = isJoinSemilattice }
joinSemiLattice = joinSemilattice
{-# WARNING_ON_USAGE joinSemiLattice
"Warning: joinSemiLattice was deprecated in v0.17.
Please use joinSemilattice instead."
#-}
open JoinSemilattice joinSemilattice public using (preorder; poset)
------------------------------------------------------------------------
-- Meet semilattices
record IsMeetSemilattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) -- The underlying equality.
(_≤_ : Rel A ℓ₂) -- The partial order.
(_∧_ : Op₂ A) -- The meet operation.
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isPartialOrder : IsPartialOrder _≈_ _≤_
infimum : Infimum _≤_ _∧_
x∧y≤x : ∀ x y → (x ∧ y) ≤ x
x∧y≤x x y = let pf , _ , _ = infimum x y in pf
x∧y≤y : ∀ x y → (x ∧ y) ≤ y
x∧y≤y x y = let _ , pf , _ = infimum x y in pf
∧-greatest : ∀ {x y z} → x ≤ y → x ≤ z → x ≤ (y ∧ z)
∧-greatest {x} {y} {z} = let _ , _ , pf = infimum y z in pf x
open IsPartialOrder isPartialOrder public
record MeetSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
_≤_ : Rel Carrier ℓ₂ -- The partial order.
_∧_ : Op₂ Carrier -- The meet operation.
isMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_
open IsMeetSemilattice isMeetSemilattice public
poset : Poset c ℓ₁ ℓ₂
poset = record { isPartialOrder = isPartialOrder }
open Poset poset public using (preorder)
record IsBoundedMeetSemilattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) -- The underlying equality.
(_≤_ : Rel A ℓ₂) -- The partial order.
(_∧_ : Op₂ A) -- The join operation.
(⊤ : A) -- The maximum.
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_
maximum : Maximum _≤_ ⊤
open IsMeetSemilattice isMeetSemilattice public
record BoundedMeetSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
_≤_ : Rel Carrier ℓ₂ -- The partial order.
_∧_ : Op₂ Carrier -- The join operation.
⊤ : Carrier -- The maximum.
isBoundedMeetSemilattice : IsBoundedMeetSemilattice _≈_ _≤_ _∧_ ⊤
open IsBoundedMeetSemilattice isBoundedMeetSemilattice public
meetSemilattice : MeetSemilattice c ℓ₁ ℓ₂
meetSemilattice = record { isMeetSemilattice = isMeetSemilattice }
meetSemiLattice = meetSemilattice
{-# WARNING_ON_USAGE meetSemiLattice
"Warning: meetSemiLattice was deprecated in v0.17.
Please use meetSemilattice instead."
#-}
open MeetSemilattice meetSemilattice public using (preorder; poset)
------------------------------------------------------------------------
-- Lattices
record IsLattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) -- The underlying equality.
(_≤_ : Rel A ℓ₂) -- The partial order.
(_∨_ : Op₂ A) -- The join operation.
(_∧_ : Op₂ A) -- The meet operation.
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isPartialOrder : IsPartialOrder _≈_ _≤_
supremum : Supremum _≤_ _∨_
infimum : Infimum _≤_ _∧_
isJoinSemilattice : IsJoinSemilattice _≈_ _≤_ _∨_
isJoinSemilattice = record
{ isPartialOrder = isPartialOrder
; supremum = supremum
}
isMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_
isMeetSemilattice = record
{ isPartialOrder = isPartialOrder
; infimum = infimum
}
open IsJoinSemilattice isJoinSemilattice public
using (x≤x∨y; y≤x∨y; ∨-least)
open IsMeetSemilattice isMeetSemilattice public
using (x∧y≤x; x∧y≤y; ∧-greatest)
open IsPartialOrder isPartialOrder public
record Lattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
_≤_ : Rel Carrier ℓ₂ -- The partial order.
_∨_ : Op₂ Carrier -- The join operation.
_∧_ : Op₂ Carrier -- The meet operation.
isLattice : IsLattice _≈_ _≤_ _∨_ _∧_
open IsLattice isLattice public
setoid : Setoid c ℓ₁
setoid = record { isEquivalence = isEquivalence }
joinSemilattice : JoinSemilattice c ℓ₁ ℓ₂
joinSemilattice = record { isJoinSemilattice = isJoinSemilattice }
meetSemilattice : MeetSemilattice c ℓ₁ ℓ₂
meetSemilattice = record { isMeetSemilattice = isMeetSemilattice }
open JoinSemilattice joinSemilattice public using (poset; preorder)
record IsDistributiveLattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) -- The underlying equality.
(_≤_ : Rel A ℓ₂) -- The partial order.
(_∨_ : Op₂ A) -- The join operation.
(_∧_ : Op₂ A) -- The meet operation.
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isLattice : IsLattice _≈_ _≤_ _∨_ _∧_
∧-distribˡ-∨ : _DistributesOverˡ_ _≈_ _∧_ _∨_
open IsLattice isLattice public
record DistributiveLattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
_≤_ : Rel Carrier ℓ₂ -- The partial order.
_∨_ : Op₂ Carrier -- The join operation.
_∧_ : Op₂ Carrier -- The meet operation.
isDistributiveLattice : IsDistributiveLattice _≈_ _≤_ _∨_ _∧_
open IsDistributiveLattice isDistributiveLattice using (∧-distribˡ-∨) public
open IsDistributiveLattice isDistributiveLattice using (isLattice)
lattice : Lattice c ℓ₁ ℓ₂
lattice = record { isLattice = isLattice }
open Lattice lattice hiding (Carrier; _≈_; _≤_; _∨_; _∧_) public
record IsBoundedLattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) -- The underlying equality.
(_≤_ : Rel A ℓ₂) -- The partial order.
(_∨_ : Op₂ A) -- The join operation.
(_∧_ : Op₂ A) -- The meet operation.
(⊤ : A) -- The maximum.
(⊥ : A) -- The minimum.
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isLattice : IsLattice _≈_ _≤_ _∨_ _∧_
maximum : Maximum _≤_ ⊤
minimum : Minimum _≤_ ⊥
open IsLattice isLattice public
isBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ _≤_ _∨_ ⊥
isBoundedJoinSemilattice = record
{ isJoinSemilattice = isJoinSemilattice
; minimum = minimum
}
isBoundedMeetSemilattice : IsBoundedMeetSemilattice _≈_ _≤_ _∧_ ⊤
isBoundedMeetSemilattice = record
{ isMeetSemilattice = isMeetSemilattice
; maximum = maximum
}
record BoundedLattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
_≤_ : Rel Carrier ℓ₂ -- The partial order.
_∨_ : Op₂ Carrier -- The join operation.
_∧_ : Op₂ Carrier -- The meet operation.
⊤ : Carrier -- The maximum.
⊥ : Carrier -- The minimum.
isBoundedLattice : IsBoundedLattice _≈_ _≤_ _∨_ _∧_ ⊤ ⊥
open IsBoundedLattice isBoundedLattice public
boundedJoinSemilattice : BoundedJoinSemilattice c ℓ₁ ℓ₂
boundedJoinSemilattice = record
{ isBoundedJoinSemilattice = isBoundedJoinSemilattice }
boundedMeetSemilattice : BoundedMeetSemilattice c ℓ₁ ℓ₂
boundedMeetSemilattice = record
{ isBoundedMeetSemilattice = isBoundedMeetSemilattice }
lattice : Lattice c ℓ₁ ℓ₂
lattice = record { isLattice = isLattice }
open Lattice lattice public
using (joinSemilattice; meetSemilattice; poset; preorder; setoid)
------------------------------------------------------------------------
-- Heyting algebras (a bounded lattice with exponential operator)
record IsHeytingAlgebra {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) -- The underlying equality.
(_≤_ : Rel A ℓ₂) -- The partial order.
(_∨_ : Op₂ A) -- The join operation.
(_∧_ : Op₂ A) -- The meet operation.
(_⇨_ : Op₂ A) -- The exponential operation.
(⊤ : A) -- The maximum.
(⊥ : A) -- The minimum.
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isBoundedLattice : IsBoundedLattice _≈_ _≤_ _∨_ _∧_ ⊤ ⊥
exponential : Exponential _≤_ _∧_ _⇨_
transpose-⇨ : ∀ {w x y} → (w ∧ x) ≤ y → w ≤ (x ⇨ y)
transpose-⇨ {w} {x} {y} = let pf , _ = exponential w x y in pf
transpose-∧ : ∀ {w x y} → w ≤ (x ⇨ y) → (w ∧ x) ≤ y
transpose-∧ {w} {x} {y} = let _ , pf = exponential w x y in pf
open IsBoundedLattice isBoundedLattice public
record HeytingAlgebra c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 5 _⇨_
infixr 6 _∨_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
_≤_ : Rel Carrier ℓ₂ -- The partial order.
_∨_ : Op₂ Carrier -- The join operation.
_∧_ : Op₂ Carrier -- The meet operation.
_⇨_ : Op₂ Carrier -- The exponential operation.
⊤ : Carrier -- The maximum.
⊥ : Carrier -- The minimum.
isHeytingAlgebra : IsHeytingAlgebra _≈_ _≤_ _∨_ _∧_ _⇨_ ⊤ ⊥
boundedLattice : BoundedLattice c ℓ₁ ℓ₂
boundedLattice = record
{ isBoundedLattice = IsHeytingAlgebra.isBoundedLattice isHeytingAlgebra }
open IsHeytingAlgebra isHeytingAlgebra
using (exponential; transpose-⇨; transpose-∧) public
open BoundedLattice boundedLattice
hiding (Carrier; _≈_; _≤_; _∨_; _∧_; ⊤; ⊥) public
------------------------------------------------------------------------
-- Boolean algebras (a specialized Heyting algebra)
record IsBooleanAlgebra {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) -- The underlying equality.
(_≤_ : Rel A ℓ₂) -- The partial order.
(_∨_ : Op₂ A) -- The join operation.
(_∧_ : Op₂ A) -- The meet operation.
(¬_ : Op₁ A) -- The negation operation.
(⊤ : A) -- The maximum.
(⊥ : A) -- The minimum.
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
infixr 5 _⇨_
_⇨_ : Op₂ A
x ⇨ y = (¬ x) ∨ y
field
isHeytingAlgebra : IsHeytingAlgebra _≈_ _≤_ _∨_ _∧_ _⇨_ ⊤ ⊥
open IsHeytingAlgebra isHeytingAlgebra public
record BooleanAlgebra c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
infixr 7 _∧_
infix 8 ¬_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
_≤_ : Rel Carrier ℓ₂ -- The partial order.
_∨_ : Op₂ Carrier -- The join operation.
_∧_ : Op₂ Carrier -- The meet operation.
¬_ : Op₁ Carrier -- The negation operation.
⊤ : Carrier -- The maximum.
⊥ : Carrier -- The minimum.
isBooleanAlgebra : IsBooleanAlgebra _≈_ _≤_ _∨_ _∧_ ¬_ ⊤ ⊥
open IsBooleanAlgebra isBooleanAlgebra using (isHeytingAlgebra)
heytingAlgebra : HeytingAlgebra c ℓ₁ ℓ₂
heytingAlgebra = record { isHeytingAlgebra = isHeytingAlgebra }
open HeytingAlgebra heytingAlgebra public
hiding (Carrier; _≈_; _≤_; _∨_; _∧_; ⊤; ⊥)
Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.