91 lines
4.0 KiB
Agda
91 lines
4.0 KiB
Agda
open import Lattice
|
||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
|
||
open import Relation.Binary.Definitions using (Decidable)
|
||
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
|
||
open import Data.List using (List)
|
||
|
||
module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
|
||
(_≈₂_ : B → B → Set b)
|
||
(_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
|
||
(≡-dec-A : Decidable (_≡_ {a} {A}))
|
||
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
|
||
|
||
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
|
||
using (Map; ⊔-equal-keys; ⊓-equal-keys)
|
||
renaming
|
||
( _≈_ to _≈ᵐ_
|
||
; _⊔_ to _⊔ᵐ_
|
||
; _⊓_ to _⊓ᵐ_
|
||
; ≈-equiv to ≈ᵐ-equiv
|
||
; ≈-⊔-cong to ≈ᵐ-⊔ᵐ-cong
|
||
; ⊔-assoc to ⊔ᵐ-assoc
|
||
; ⊔-comm to ⊔ᵐ-comm
|
||
; ⊔-idemp to ⊔ᵐ-idemp
|
||
; ≈-⊓-cong to ≈ᵐ-⊓ᵐ-cong
|
||
; ⊓-assoc to ⊓ᵐ-assoc
|
||
; ⊓-comm to ⊓ᵐ-comm
|
||
; ⊓-idemp to ⊓ᵐ-idemp
|
||
; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
|
||
; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
|
||
; ≈-dec to ≈ᵐ-dec
|
||
)
|
||
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
|
||
open import Equivalence
|
||
|
||
module _ (ks : List A) where
|
||
FiniteMap : Set (a ⊔ℓ b)
|
||
FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)
|
||
|
||
_≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b)
|
||
_≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
|
||
|
||
≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_
|
||
≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂)
|
||
|
||
_⊔_ : FiniteMap → FiniteMap → FiniteMap
|
||
_⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊔ᵐ m₂ , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
|
||
|
||
_⊓_ : FiniteMap → FiniteMap → FiniteMap
|
||
_⊓_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊓ᵐ m₂ , trans (sym (⊓-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
|
||
|
||
≈-equiv : IsEquivalence FiniteMap _≈_
|
||
≈-equiv = record
|
||
{ ≈-refl = λ {(m , _)} → IsEquivalence.≈-refl ≈ᵐ-equiv {m}
|
||
; ≈-sym = λ {(m₁ , _)} {(m₂ , _)} → IsEquivalence.≈-sym ≈ᵐ-equiv {m₁} {m₂}
|
||
; ≈-trans = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} → IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
|
||
}
|
||
|
||
isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
|
||
isUnionSemilattice = record
|
||
{ ≈-equiv = ≈-equiv
|
||
; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
|
||
; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃
|
||
; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂
|
||
; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m
|
||
}
|
||
|
||
isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
|
||
isIntersectSemilattice = record
|
||
{ ≈-equiv = ≈-equiv
|
||
; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
|
||
; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃
|
||
; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂
|
||
; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m
|
||
}
|
||
|
||
isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_
|
||
isLattice = record
|
||
{ joinSemilattice = isUnionSemilattice
|
||
; meetSemilattice = isIntersectSemilattice
|
||
; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
|
||
; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
|
||
}
|
||
|
||
lattice : Lattice FiniteMap
|
||
lattice = record
|
||
{ _≈_ = _≈_
|
||
; _⊔_ = _⊔_
|
||
; _⊓_ = _⊓_
|
||
; isLattice = isLattice
|
||
}
|