agda-spa/Lattice.agda

353 lines
14 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 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 IsEquivalenceInstances where
module ForMap {a b} (A : Set a) (B : Set b)
(≡-dec-A : Decidable (_≡_ {a} {A}))
(_≈₂_ : B B Set b)
(eB : IsEquivalence B _≈₂_) where
open import Map A B ≡-dec-A using (Map; lift; subset)
open import Data.List using (_∷_; []) -- TODO: re-export these with nicer names from map
open IsEquivalence eB renaming
( ≈-refl to ≈₂-refl
; ≈-sym to ≈₂-sym
; ≈-trans to ≈₂-trans
)
private
_≈_ : Map Map Set (Agda.Primitive._⊔_ a b)
_≈_ = lift _≈₂_
_⊆_ : Map Map Set (Agda.Primitive._⊔_ a b)
_⊆_ = subset _≈₂_
⊆-refl : (m : Map) m m
⊆-refl _ k v k,v∈m = (v , (≈₂-refl , k,v∈m))
⊆-trans : (m₁ m₂ m₃ : Map) m₁ m₂ m₂ m₃ m₁ m₃
⊆-trans _ _ _ m₁⊆m₂ m₂⊆m₃ k v k,v∈m₁ =
let
(v' , (v≈v' , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
(v'' , (v'≈v'' , k,v''∈m₃)) = m₂⊆m₃ k v' k,v'∈m₂
in (v'' , (≈₂-trans v≈v' v'≈v'' , k,v''∈m₃))
≈-refl : (m : Map) m m
≈-refl m = (⊆-refl m , ⊆-refl m)
≈-sym : (m₁ m₂ : Map) m₁ m₂ m₂ m₁
≈-sym _ _ (m₁⊆m₂ , m₂⊆m₁) = (m₂⊆m₁ , m₁⊆m₂)
≈-trans : (m₁ m₂ m₃ : Map) m₁ m₂ m₂ m₃ m₁ m₃
≈-trans m₁ m₂ m₃ (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) =
( ⊆-trans m₁ m₂ m₃ m₁⊆m₂ m₂⊆m₃
, ⊆-trans m₃ m₂ m₁ m₃⊆m₂ m₂⊆m₁
)
LiftEquivalence : IsEquivalence Map _≈_
LiftEquivalence = record
{ ≈-refl = λ {m₁} ≈-refl m₁
; ≈-sym = λ {m₁} {m₂} ≈-sym m₁ m₂
; ≈-trans = λ {m₁} {m₂} {m₃} ≈-trans m₁ m₂ m₃
}
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 ForMap {a} {A B : Set a}
(≡-dec-A : Decidable (_≡_ {a} {A}))
(_≈₂_ : B B Set a)
(_⊔₂_ : B B B)
(sB : IsSemilattice B _≈₂_ _⊔₂_) where
open import Map A B ≡-dec-A
open IsSemilattice sB renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym
; ⊔-assoc to ⊔₂-assoc; ⊔-comm to ⊔₂-comm; ⊔-idemp to ⊔₂-idemp
)
private
infix 4 _≈_
infixl 20 _⊔_
_≈_ : Map Map Set a
_≈_ = lift (_≈₂_)
_⊔_ : Map Map Map
m₁ m₂ = union _⊔₂_ m₁ m₂
_⊓_ : Map Map Map
m₁ m₂ = intersect _⊔₂_ m₁ m₂
module MapEquiv = IsEquivalenceInstances.ForMap A B ≡-dec-A _≈₂_ (IsSemilattice.≈-equiv sB)
MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_
MapIsUnionSemilattice = record
{ ≈-equiv = MapEquiv.LiftEquivalence
; ⊔-assoc = union-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
; ⊔-comm = union-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
; ⊔-idemp = union-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp
}
MapIsIntersectSemilattice : IsSemilattice Map _≈_ _⊓_
MapIsIntersectSemilattice = record
{ ≈-equiv = MapEquiv.LiftEquivalence
; ⊔-assoc = intersect-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
; ⊔-comm = intersect-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
; ⊔-idemp = intersect-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-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-⊓-⊔
}