259 lines
9.6 KiB
Agda
259 lines
9.6 KiB
Agda
module Lattice where
|
||
|
||
import Data.Nat.Properties as NatProps
|
||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; isEquivalence)
|
||
open import Relation.Binary.Definitions
|
||
open import Data.Nat as Nat using (ℕ; _≤_)
|
||
open import Data.Product using (_×_; _,_)
|
||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||
open import Agda.Primitive using (lsuc; Level)
|
||
|
||
open import NatMap using (NatMap)
|
||
|
||
record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where
|
||
field
|
||
≈-refl : {a : A} → a ≈ a
|
||
≈-sym : {a b : A} → a ≈ b → b ≈ a
|
||
≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c
|
||
|
||
record IsSemilattice {a} (A : Set a)
|
||
(_≈_ : A → A → Set a)
|
||
(_⊔_ : A → A → A) : Set a where
|
||
|
||
field
|
||
≈-equiv : IsEquivalence A _≈_
|
||
|
||
⊔-assoc : (x y z : A) → ((x ⊔ y) ⊔ z) ≈ (x ⊔ (y ⊔ z))
|
||
⊔-comm : (x y : A) → (x ⊔ y) ≈ (y ⊔ x)
|
||
⊔-idemp : (x : A) → (x ⊔ x) ≈ x
|
||
|
||
open IsEquivalence ≈-equiv public
|
||
|
||
record IsLattice {a} (A : Set a)
|
||
(_≈_ : A → A → Set a)
|
||
(_⊔_ : A → A → A)
|
||
(_⊓_ : A → A → A) : Set a where
|
||
|
||
field
|
||
joinSemilattice : IsSemilattice A _≈_ _⊔_
|
||
meetSemilattice : IsSemilattice A _≈_ _⊓_
|
||
|
||
absorb-⊔-⊓ : (x y : A) → (x ⊔ (x ⊓ y)) ≈ x
|
||
absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x
|
||
|
||
open IsSemilattice joinSemilattice public
|
||
open IsSemilattice meetSemilattice public renaming
|
||
( ⊔-assoc to ⊓-assoc
|
||
; ⊔-comm to ⊓-comm
|
||
; ⊔-idemp to ⊓-idemp
|
||
)
|
||
|
||
record Semilattice {a} (A : Set a) : Set (lsuc a) where
|
||
field
|
||
_≈_ : A → A → Set a
|
||
_⊔_ : A → A → A
|
||
|
||
isSemilattice : IsSemilattice A _≈_ _⊔_
|
||
|
||
open IsSemilattice isSemilattice public
|
||
|
||
|
||
record Lattice {a} (A : Set a) : Set (lsuc a) where
|
||
field
|
||
_≈_ : A → A → Set a
|
||
_⊔_ : A → A → A
|
||
_⊓_ : A → A → A
|
||
|
||
isLattice : IsLattice A _≈_ _⊔_ _⊓_
|
||
|
||
open IsLattice isLattice public
|
||
|
||
module IsSemilatticeInstances where
|
||
module ForNat where
|
||
open Nat
|
||
open NatProps
|
||
open Eq
|
||
|
||
NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
|
||
NatIsMaxSemilattice = record
|
||
{ ≈-equiv = record
|
||
{ ≈-refl = refl
|
||
; ≈-sym = sym
|
||
; ≈-trans = trans
|
||
}
|
||
; ⊔-assoc = ⊔-assoc
|
||
; ⊔-comm = ⊔-comm
|
||
; ⊔-idemp = ⊔-idem
|
||
}
|
||
|
||
NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
|
||
NatIsMinSemilattice = record
|
||
{ ≈-equiv = record
|
||
{ ≈-refl = refl
|
||
; ≈-sym = sym
|
||
; ≈-trans = trans
|
||
}
|
||
; ⊔-assoc = ⊓-assoc
|
||
; ⊔-comm = ⊓-comm
|
||
; ⊔-idemp = ⊓-idem
|
||
}
|
||
|
||
module ForProd {a} {A B : Set a}
|
||
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
|
||
(_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
|
||
(sA : IsSemilattice A _≈₁_ _⊔₁_) (sB : IsSemilattice B _≈₂_ _⊔₂_) where
|
||
|
||
open Eq
|
||
open Data.Product
|
||
|
||
private
|
||
infix 4 _≈_
|
||
infixl 20 _⊔_
|
||
|
||
_≈_ : A × B → A × B → Set a
|
||
(a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
|
||
|
||
_⊔_ : A × B → A × B → A × B
|
||
(a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
|
||
|
||
⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≈ p₁ ⊔ (p₂ ⊔ p₃)
|
||
⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) =
|
||
( IsSemilattice.⊔-assoc sA a₁ a₂ a₃
|
||
, IsSemilattice.⊔-assoc sB b₁ b₂ b₃
|
||
)
|
||
|
||
⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≈ p₂ ⊔ p₁
|
||
⊔-comm (a₁ , b₁) (a₂ , b₂) =
|
||
( IsSemilattice.⊔-comm sA a₁ a₂
|
||
, IsSemilattice.⊔-comm sB b₁ b₂
|
||
)
|
||
|
||
⊔-idemp : (p : A × B) → p ⊔ p ≈ p
|
||
⊔-idemp (a , b) =
|
||
( IsSemilattice.⊔-idemp sA a
|
||
, IsSemilattice.⊔-idemp sB b
|
||
)
|
||
|
||
≈-refl : {p : A × B} → p ≈ p
|
||
≈-refl =
|
||
( IsSemilattice.≈-refl sA
|
||
, IsSemilattice.≈-refl sB
|
||
)
|
||
|
||
≈-sym : {p₁ p₂ : A × B} → p₁ ≈ p₂ → p₂ ≈ p₁
|
||
≈-sym (a₁≈a₂ , b₁≈b₂) =
|
||
( IsSemilattice.≈-sym sA a₁≈a₂
|
||
, IsSemilattice.≈-sym sB b₁≈b₂
|
||
)
|
||
|
||
≈-trans : {p₁ p₂ p₃ : A × B} → p₁ ≈ p₂ → p₂ ≈ p₃ → p₁ ≈ p₃
|
||
≈-trans (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) =
|
||
( IsSemilattice.≈-trans sA a₁≈a₂ a₂≈a₃
|
||
, IsSemilattice.≈-trans sB b₁≈b₂ b₂≈b₃
|
||
)
|
||
|
||
|
||
ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
|
||
ProdIsSemilattice = record
|
||
{ ≈-equiv = record
|
||
{ ≈-refl = ≈-refl
|
||
; ≈-sym = ≈-sym
|
||
; ≈-trans = ≈-trans
|
||
}
|
||
; ⊔-assoc = ⊔-assoc
|
||
; ⊔-comm = ⊔-comm
|
||
; ⊔-idemp = ⊔-idemp
|
||
}
|
||
|
||
module IsLatticeInstances where
|
||
module ForNat where
|
||
open Nat
|
||
open NatProps
|
||
open Eq
|
||
open IsSemilatticeInstances.ForNat
|
||
open Data.Product
|
||
|
||
private
|
||
max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z
|
||
max-bound₁ {x} {y} {z} x⊔y≡z
|
||
rewrite sym x⊔y≡z
|
||
rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)
|
||
|
||
min-bound₁ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ x
|
||
min-bound₁ {x} {y} {z} x⊓y≡z
|
||
rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl)
|
||
|
||
minmax-absorb : {x y : ℕ} → x ⊓ (x ⊔ y) ≡ x
|
||
minmax-absorb {x} {y} = ≤-antisym x⊓x⊔y≤x (helper x⊓x≤x⊓x⊔y (⊓-idem x))
|
||
where
|
||
x⊓x⊔y≤x = min-bound₁ {x} {x ⊔ y} {x ⊓ (x ⊔ y)} refl
|
||
x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (max-bound₁ {x} {y} {x ⊔ y} refl)
|
||
|
||
-- >:(
|
||
helper : x ⊓ x ≤ x ⊓ (x ⊔ y) → x ⊓ x ≡ x → x ≤ x ⊓ (x ⊔ y)
|
||
helper x⊓x≤x⊓x⊔y x⊓x≡x rewrite x⊓x≡x = x⊓x≤x⊓x⊔y
|
||
|
||
maxmin-absorb : {x y : ℕ} → x ⊔ (x ⊓ y) ≡ x
|
||
maxmin-absorb {x} {y} = ≤-antisym (helper x⊔x⊓y≤x⊔x (⊔-idem x)) x≤x⊔x⊓y
|
||
where
|
||
x≤x⊔x⊓y = max-bound₁ {x} {x ⊓ y} {x ⊔ (x ⊓ y)} refl
|
||
x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (min-bound₁ {x} {y} {x ⊓ y} refl)
|
||
|
||
-- >:(
|
||
helper : x ⊔ (x ⊓ y) ≤ x ⊔ x → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x
|
||
helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
|
||
|
||
NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
|
||
NatIsLattice = record
|
||
{ joinSemilattice = NatIsMaxSemilattice
|
||
; meetSemilattice = NatIsMinSemilattice
|
||
; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
|
||
; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
|
||
}
|
||
|
||
module ForProd {a} {A B : Set a}
|
||
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
|
||
(_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A)
|
||
(_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
|
||
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
|
||
|
||
private
|
||
module ProdJoin = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB)
|
||
module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)
|
||
|
||
infix 4 _≈_
|
||
infixl 20 _⊔_
|
||
|
||
_≈_ : (A × B) → (A × B) → Set a
|
||
(a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
|
||
|
||
_⊔_ : (A × B) → (A × B) → (A × B)
|
||
(a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
|
||
|
||
_⊓_ : (A × B) → (A × B) → (A × B)
|
||
(a₁ , b₁) ⊓ (a₂ , b₂) = (a₁ ⊓₁ a₂ , b₁ ⊓₂ b₂)
|
||
|
||
open Eq
|
||
open Data.Product
|
||
|
||
private
|
||
absorb-⊔-⊓ : (p₁ p₂ : A × B) → p₁ ⊔ (p₁ ⊓ p₂) ≈ p₁
|
||
absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂) =
|
||
( IsLattice.absorb-⊔-⊓ lA a₁ a₂
|
||
, IsLattice.absorb-⊔-⊓ lB b₁ b₂
|
||
)
|
||
|
||
absorb-⊓-⊔ : (p₁ p₂ : A × B) → p₁ ⊓ (p₁ ⊔ p₂) ≈ p₁
|
||
absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂) =
|
||
( IsLattice.absorb-⊓-⊔ lA a₁ a₂
|
||
, IsLattice.absorb-⊓-⊔ lB b₁ b₂
|
||
)
|
||
|
||
ProdIsLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
|
||
ProdIsLattice = record
|
||
{ joinSemilattice = ProdJoin.ProdIsSemilattice
|
||
; meetSemilattice = ProdMeet.ProdIsSemilattice
|
||
; absorb-⊔-⊓ = absorb-⊔-⊓
|
||
; absorb-⊓-⊔ = absorb-⊓-⊔
|
||
}
|