354 lines
15 KiB
Agda
354 lines
15 KiB
Agda
module Lattice where
|
||
|
||
import Data.Nat.Properties as NatProps
|
||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
|
||
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 IsPreorder {a} (A : Set a) (_≼_ : A → A → Set a) : Set a where
|
||
field
|
||
≼-refl : Reflexive (_≼_)
|
||
≼-trans : Transitive (_≼_)
|
||
≼-antisym : Antisymmetric (_≡_) (_≼_)
|
||
|
||
isPreorderFlip : {a : Level} → {A : Set a} → {_≼_ : A → A → Set a} → IsPreorder A _≼_ → IsPreorder A (λ x y → y ≼ x)
|
||
isPreorderFlip isPreorder = record
|
||
{ ≼-refl = IsPreorder.≼-refl isPreorder
|
||
; ≼-trans = λ {x} {y} {z} x≽y y≽z → IsPreorder.≼-trans isPreorder y≽z x≽y
|
||
; ≼-antisym = λ {x} {y} x≽y y≽x → IsPreorder.≼-antisym isPreorder y≽x x≽y
|
||
}
|
||
|
||
record Preorder {a} (A : Set a) : Set (lsuc a) where
|
||
field
|
||
_≼_ : A → A → Set a
|
||
|
||
isPreorder : IsPreorder A _≼_
|
||
|
||
open IsPreorder isPreorder public
|
||
|
||
record IsSemilattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A → A → A) : Set a where
|
||
field
|
||
isPreorder : IsPreorder 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
|
||
|
||
⊔-bound : (x y z : A) → x ⊔ y ≡ z → (x ≼ z × y ≼ z)
|
||
⊔-least : (x y z : A) → x ⊔ y ≡ z → ∀ (z' : A) → (x ≼ z' × y ≼ z') → z ≼ z'
|
||
|
||
open IsPreorder isPreorder public
|
||
|
||
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 IsLattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where
|
||
|
||
_≽_ : A → A → Set a
|
||
a ≽ b = b ≼ a
|
||
|
||
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
|
||
; ⊔-bound to ⊓-bound
|
||
; ⊔-least to ⊓-least
|
||
)
|
||
|
||
|
||
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 PreorderInstances where
|
||
module ForNat where
|
||
open NatProps
|
||
|
||
NatPreorder : Preorder ℕ
|
||
NatPreorder = record
|
||
{ _≼_ = _≤_
|
||
; isPreorder = record
|
||
{ ≼-refl = ≤-refl
|
||
; ≼-trans = ≤-trans
|
||
; ≼-antisym = ≤-antisym
|
||
}
|
||
}
|
||
|
||
module ForProd {a} {A B : Set a} (pA : Preorder A) (pB : Preorder B) where
|
||
open Eq
|
||
|
||
private
|
||
_≼_ : A × B → A × B → Set a
|
||
(a₁ , b₁) ≼ (a₂ , b₂) = Preorder._≼_ pA a₁ a₂ × Preorder._≼_ pB b₁ b₂
|
||
|
||
≼-refl : {p : A × B} → p ≼ p
|
||
≼-refl {(a , b)} = (Preorder.≼-refl pA {a}, Preorder.≼-refl pB {b})
|
||
|
||
≼-trans : {p₁ p₂ p₃ : A × B} → p₁ ≼ p₂ → p₂ ≼ p₃ → p₁ ≼ p₃
|
||
≼-trans (a₁≼a₂ , b₁≼b₂) (a₂≼a₃ , b₂≼b₃) =
|
||
( Preorder.≼-trans pA a₁≼a₂ a₂≼a₃
|
||
, Preorder.≼-trans pB b₁≼b₂ b₂≼b₃
|
||
)
|
||
|
||
≼-antisym : {p₁ p₂ : A × B} → p₁ ≼ p₂ → p₂ ≼ p₁ → p₁ ≡ p₂
|
||
≼-antisym (a₁≼a₂ , b₁≼b₂) (a₂≼a₁ , b₂≼b₁) = cong₂ (_,_) (Preorder.≼-antisym pA a₁≼a₂ a₂≼a₁) (Preorder.≼-antisym pB b₁≼b₂ b₂≼b₁)
|
||
|
||
ProdPreorder : Preorder (A × B)
|
||
ProdPreorder = record
|
||
{ _≼_ = _≼_
|
||
; isPreorder = record
|
||
{ ≼-refl = ≼-refl
|
||
; ≼-trans = ≼-trans
|
||
; ≼-antisym = ≼-antisym
|
||
}
|
||
}
|
||
|
||
module SemilatticeInstances where
|
||
module ForNat where
|
||
open Nat
|
||
open NatProps
|
||
open Eq
|
||
open PreorderInstances.ForNat
|
||
|
||
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)
|
||
|
||
max-bound₂ : {x y z : ℕ} → x ⊔ y ≡ z → y ≤ z
|
||
max-bound₂ {x} {y} {z} x⊔y≡z rewrite sym x⊔y≡z = m≤n⇒m≤o⊔n x (≤-refl)
|
||
|
||
max-least : (x y z : ℕ) → x ⊔ y ≡ z → ∀ (z' : ℕ) → (x ≤ z' × y ≤ z') → z ≤ z'
|
||
max-least x y z x⊔y≡z z' (x≤z' , y≤z') with (⊔-sel x y)
|
||
... | inj₁ x⊔y≡x rewrite trans (sym x⊔y≡z) (x⊔y≡x) = x≤z'
|
||
... | inj₂ x⊔y≡y rewrite trans (sym x⊔y≡z) (x⊔y≡y) = y≤z'
|
||
|
||
NatMaxSemilattice : Semilattice ℕ
|
||
NatMaxSemilattice = record
|
||
{ _≼_ = _≤_
|
||
; _⊔_ = _⊔_
|
||
; isSemilattice = record
|
||
{ isPreorder = Preorder.isPreorder NatPreorder
|
||
; ⊔-assoc = ⊔-assoc
|
||
; ⊔-comm = ⊔-comm
|
||
; ⊔-idemp = ⊔-idem
|
||
; ⊔-bound = λ x y z x⊔y≡z → (max-bound₁ x⊔y≡z , max-bound₂ x⊔y≡z)
|
||
; ⊔-least = max-least
|
||
}
|
||
}
|
||
|
||
private
|
||
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)
|
||
|
||
min-bound₂ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ y
|
||
min-bound₂ {x} {y} {z} x⊓y≡z rewrite sym x⊓y≡z rewrite ⊓-comm x y = m≤n⇒m⊓o≤n x (≤-refl)
|
||
|
||
min-greatest : (x y z : ℕ) → x ⊓ y ≡ z → ∀ (z' : ℕ) → (z' ≤ x × z' ≤ y) → z' ≤ z
|
||
min-greatest x y z x⊓y≡z z' (z'≤x , z'≤y) with (⊓-sel x y)
|
||
... | inj₁ x⊓y≡x rewrite trans (sym x⊓y≡z) (x⊓y≡x) = z'≤x
|
||
... | inj₂ x⊓y≡y rewrite trans (sym x⊓y≡z) (x⊓y≡y) = z'≤y
|
||
|
||
|
||
NatMinSemilattice : Semilattice ℕ
|
||
NatMinSemilattice = record
|
||
{ _≼_ = _≥_
|
||
; _⊔_ = _⊓_
|
||
; isSemilattice = record
|
||
{ isPreorder = isPreorderFlip (Preorder.isPreorder NatPreorder)
|
||
; ⊔-assoc = ⊓-assoc
|
||
; ⊔-comm = ⊓-comm
|
||
; ⊔-idemp = ⊓-idem
|
||
; ⊔-bound = λ x y z x⊓y≡z → (min-bound₁ x⊓y≡z , min-bound₂ x⊓y≡z)
|
||
; ⊔-least = min-greatest
|
||
}
|
||
}
|
||
|
||
module ForProd {a} {A B : Set a} (sA : Semilattice A) (sB : Semilattice B) where
|
||
private
|
||
_≼₁_ = Semilattice._≼_ sA
|
||
_≼₂_ = Semilattice._≼_ sB
|
||
|
||
pA = record { _≼_ = _≼₁_; isPreorder = Semilattice.isPreorder sA }
|
||
pB = record { _≼_ = _≼₂_; isPreorder = Semilattice.isPreorder sB }
|
||
|
||
open PreorderInstances.ForProd pA pB
|
||
open Eq
|
||
open Data.Product
|
||
|
||
private
|
||
_≼_ = Preorder._≼_ ProdPreorder
|
||
|
||
_⊔_ : A × B → A × B → A × B
|
||
(a₁ , b₁) ⊔ (a₂ , b₂) = (Semilattice._⊔_ sA a₁ a₂ , Semilattice._⊔_ sB b₁ b₂)
|
||
|
||
⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≡ p₁ ⊔ (p₂ ⊔ p₃)
|
||
⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃)
|
||
rewrite Semilattice.⊔-assoc sA a₁ a₂ a₃
|
||
rewrite Semilattice.⊔-assoc sB b₁ b₂ b₃ = refl
|
||
|
||
⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≡ p₂ ⊔ p₁
|
||
⊔-comm (a₁ , b₁) (a₂ , b₂)
|
||
rewrite Semilattice.⊔-comm sA a₁ a₂
|
||
rewrite Semilattice.⊔-comm sB b₁ b₂ = refl
|
||
|
||
⊔-idemp : (p : A × B) → p ⊔ p ≡ p
|
||
⊔-idemp (a , b)
|
||
rewrite Semilattice.⊔-idemp sA a
|
||
rewrite Semilattice.⊔-idemp sB b = refl
|
||
|
||
⊔-bound₁ : {p₁ p₂ p₃ : A × B} → p₁ ⊔ p₂ ≡ p₃ → p₁ ≼ p₃
|
||
⊔-bound₁ {(a₁ , b₁)} {(a₂ , b₂)} {(a₃ , b₃)} p₁⊔p₂≡p₃ = (⊔-bound-a , ⊔-bound-b)
|
||
where
|
||
⊔-bound-a = proj₁ (Semilattice.⊔-bound sA a₁ a₂ a₃ (cong proj₁ p₁⊔p₂≡p₃))
|
||
⊔-bound-b = proj₁ (Semilattice.⊔-bound sB b₁ b₂ b₃ (cong proj₂ p₁⊔p₂≡p₃))
|
||
|
||
⊔-bound₂ : {p₁ p₂ p₃ : A × B} → p₁ ⊔ p₂ ≡ p₃ → p₂ ≼ p₃
|
||
⊔-bound₂ {(a₁ , b₁)} {(a₂ , b₂)} {(a₃ , b₃)} p₁⊔p₂≡p₃ = (⊔-bound-a , ⊔-bound-b)
|
||
where
|
||
⊔-bound-a = proj₂ (Semilattice.⊔-bound sA a₁ a₂ a₃ (cong proj₁ p₁⊔p₂≡p₃))
|
||
⊔-bound-b = proj₂ (Semilattice.⊔-bound sB b₁ b₂ b₃ (cong proj₂ p₁⊔p₂≡p₃))
|
||
|
||
⊔-least : (p₁ p₂ p₃ : A × B) → p₁ ⊔ p₂ ≡ p₃ → ∀ (p₃' : A × B) → (p₁ ≼ p₃' × p₂ ≼ p₃') → p₃ ≼ p₃'
|
||
⊔-least (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) p₁⊔p₂≡p₃ (a₃' , b₃') (p₁≼p₃' , p₂≼p₃') = (⊔-least-a , ⊔-least-b)
|
||
where
|
||
⊔-least-a : a₃ ≼₁ a₃'
|
||
⊔-least-a = Semilattice.⊔-least sA a₁ a₂ a₃ (cong proj₁ p₁⊔p₂≡p₃) a₃' (proj₁ p₁≼p₃' , proj₁ p₂≼p₃')
|
||
|
||
⊔-least-b : b₃ ≼₂ b₃'
|
||
⊔-least-b = Semilattice.⊔-least sB b₁ b₂ b₃ (cong proj₂ p₁⊔p₂≡p₃) b₃' (proj₂ p₁≼p₃' , proj₂ p₂≼p₃')
|
||
|
||
ProdSemilattice : Semilattice (A × B)
|
||
ProdSemilattice = record
|
||
{ _≼_ = _≼_
|
||
; _⊔_ = _⊔_
|
||
; isSemilattice = record
|
||
{ isPreorder = Preorder.isPreorder ProdPreorder
|
||
; ⊔-assoc = ⊔-assoc
|
||
; ⊔-comm = ⊔-comm
|
||
; ⊔-idemp = ⊔-idemp
|
||
; ⊔-bound = λ x y z x⊓y≡z → (⊔-bound₁ x⊓y≡z , ⊔-bound₂ x⊓y≡z)
|
||
; ⊔-least = ⊔-least
|
||
}
|
||
}
|
||
|
||
module LatticeInstances where
|
||
module ForNat where
|
||
open Nat
|
||
open NatProps
|
||
open Eq
|
||
open SemilatticeInstances.ForNat
|
||
open Data.Product
|
||
|
||
|
||
private
|
||
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 = proj₁ (Semilattice.⊔-bound NatMinSemilattice x (x ⊔ y) (x ⊓ (x ⊔ y)) refl)
|
||
x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (proj₁ (Semilattice.⊔-bound NatMaxSemilattice 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 = proj₁ (Semilattice.⊔-bound NatMaxSemilattice x (x ⊓ y) (x ⊔ (x ⊓ y)) refl)
|
||
x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (proj₁ (Semilattice.⊔-bound NatMinSemilattice 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
|
||
|
||
NatLattice : Lattice ℕ
|
||
NatLattice = record
|
||
{ _≼_ = _≤_
|
||
; _⊔_ = _⊔_
|
||
; _⊓_ = _⊓_
|
||
; isLattice = record
|
||
{ joinSemilattice = Semilattice.isSemilattice NatMaxSemilattice
|
||
; meetSemilattice = Semilattice.isSemilattice NatMinSemilattice
|
||
; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
|
||
; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
|
||
}
|
||
}
|
||
|
||
module ForProd {a} {A B : Set a} (lA : Lattice A) (lB : Lattice B) where
|
||
private
|
||
_≼₁_ = Lattice._≼_ lA
|
||
_≼₂_ = Lattice._≼_ lB
|
||
|
||
_⊔₁_ = Lattice._⊔_ lA
|
||
_⊔₂_ = Lattice._⊔_ lB
|
||
|
||
_⊓₁_ = Lattice._⊓_ lA
|
||
_⊓₂_ = Lattice._⊓_ lB
|
||
|
||
joinA = record { _≼_ = _≼₁_; _⊔_ = _⊔₁_; isSemilattice = Lattice.joinSemilattice lA }
|
||
joinB = record { _≼_ = _≼₂_; _⊔_ = _⊔₂_; isSemilattice = Lattice.joinSemilattice lB }
|
||
|
||
|
||
meetA = record { _≼_ = λ a b → b ≼₁ a; _⊔_ = _⊓₁_; isSemilattice = Lattice.meetSemilattice lA }
|
||
meetB = record { _≼_ = λ a b → b ≼₂ a; _⊔_ = _⊓₂_; isSemilattice = Lattice.meetSemilattice lB }
|
||
|
||
module ProdJoin = SemilatticeInstances.ForProd joinA joinB
|
||
module ProdMeet = SemilatticeInstances.ForProd meetA meetB
|
||
|
||
|
||
_≼_ = Semilattice._≼_ ProdJoin.ProdSemilattice
|
||
_⊔_ = Semilattice._⊔_ ProdJoin.ProdSemilattice
|
||
_⊓_ = Semilattice._⊔_ ProdMeet.ProdSemilattice
|
||
|
||
open Eq
|
||
open Data.Product
|
||
|
||
private
|
||
absorb-⊔-⊓ : (p₁ p₂ : A × B) → p₁ ⊔ (p₁ ⊓ p₂) ≡ p₁
|
||
absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂)
|
||
rewrite Lattice.absorb-⊔-⊓ lA a₁ a₂
|
||
rewrite Lattice.absorb-⊔-⊓ lB b₁ b₂ = refl
|
||
|
||
absorb-⊓-⊔ : (p₁ p₂ : A × B) → p₁ ⊓ (p₁ ⊔ p₂) ≡ p₁
|
||
absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂)
|
||
rewrite Lattice.absorb-⊓-⊔ lA a₁ a₂
|
||
rewrite Lattice.absorb-⊓-⊔ lB b₁ b₂ = refl
|
||
|
||
ProdLattice : Lattice (A × B)
|
||
ProdLattice = record
|
||
{ _≼_ = _≼_
|
||
; _⊔_ = _⊔_
|
||
; _⊓_ = _⊓_
|
||
; isLattice = record
|
||
{ joinSemilattice = Semilattice.isSemilattice ProdJoin.ProdSemilattice
|
||
; meetSemilattice = Semilattice.isSemilattice ProdMeet.ProdSemilattice
|
||
; absorb-⊔-⊓ = absorb-⊔-⊓
|
||
; absorb-⊓-⊔ = absorb-⊓-⊔
|
||
}
|
||
}
|