agda-spa/Lattice.agda

199 lines
7.7 KiB
Agda
Raw Normal View History

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
private module NatInstances where
open Nat
open NatProps
open Eq
open Data.Sum
NatPreorder : Preorder
NatPreorder = record
{ _≼_ = _≤_
; isPreorder = record
{ ≼-refl = ≤-refl
; ≼-trans = ≤-trans
; ≼-antisym = ≤-antisym
}
}
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
}
}
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 = 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
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}
}
}
ProdSemilattice : {a : Level} {A B : Set a} {{ Semilattice A }} {{ Semilattice B }} Semilattice (A × B)
ProdSemilattice {a} {A} {B} {{slA}} {{slB}} = record
{ _≼_ = λ (a₁ , b₁) (a₂ , b₂) Semilattice._≼_ slA a₁ a₂ × Semilattice._≼_ slB b₁ b₂
; _⊔_ = λ (a₁ , b₁) (a₂ , b₂) (Semilattice._⊔_ slA a₁ a₂ , Semilattice._⊔_ slB b₁ b₂)
; isSemilattice = record
{
}
}