agda-spa/Lattice.agda
Danila Fedorin 3b29ee0f74 Add a Semilattice isntance for Products.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-07-14 21:20:16 -07:00

309 lines
13 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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
}
}
private module NatInstances 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}
}
}
-- 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
-- {
-- }
-- }