40 lines
1.3 KiB
Agda
40 lines
1.3 KiB
Agda
|
module Lattice where
|
|||
|
|
|
|||
|
|
open import Relation.Binary.PropositionalEquality
|
|||
|
|
open import Relation.Binary.Definitions
|
|||
|
|
open import Data.Nat using (ℕ; _≤_)
|
|||
|
|
open import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym)
|
|||
|
|
open import Agda.Primitive using (lsuc)
|
|||
|
|
|
|||
|
|
record Preorder {a} (A : Set a) : Set (lsuc a) where
|
|||
|
|
field
|
|||
|
|
_≼_ : A → A → Set a
|
|||
|
|
|
|||
|
|
≼-refl : Reflexive (_≼_)
|
|||
|
|
≼-trans : Transitive (_≼_)
|
|||
|
|
≼-antisym : Antisymmetric (_≡_) (_≼_)
|
|||
|
|
|
|||
|
|
record Semilattice {a} (A : Set a) : Set (lsuc a) where
|
|||
|
|
field
|
|||
|
|
_⊔_ : A → A → A
|
|||
|
|
|
|||
|
|
⊔-assoc : (x : A) → (y : A) → (z : A) → x ⊔ (y ⊔ z) ≡ (x ⊔ y) ⊔ z
|
|||
|
|
⊔-comm : (x : A) → (y : A) → x ⊔ y ≡ y ⊔ x
|
|||
|
|
⊔-idemp : (x : A) → x ⊔ x ≡ x
|
|||
|
|
|
|||
|
|
record Lattice {a} (A : Set a) : Set (lsuc a) where
|
|||
|
|
field
|
|||
|
|
joinSemilattice : Semilattice A
|
|||
|
|
meetSemilattice : Semilattice A
|
|||
|
|
|
|||
|
|
_⊔_ = Semilattice._⊔_ joinSemilattice
|
|||
|
|
_⊓_ = Semilattice._⊔_ meetSemilattice
|
|||
|
|
|
|||
|
|
field
|
|||
|
|
absorb-⊔-⊓ : (x : A) → (y : A) → x ⊔ (x ⊓ y) ≡ x
|
|||
|
|
absorb-⊓-⊔ : (x : A) → (y : A) → x ⊓ (x ⊔ y) ≡ x
|
|||
|
|
|
|||
|
|
instance
|
|||
|
|
NatPreorder : Preorder ℕ
|
|||
|
|
NatPreorder = record { _≼_ = _≤_; ≼-refl = ≤-refl; ≼-trans = ≤-trans; ≼-antisym = ≤-antisym }
|