agda-spa/Lattice/FiniteMap.agda
Danila Fedorin ec31333e9a Add a 'Finite Map' lattice
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 14:19:41 -08:00

79 lines
3.7 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.

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-⊓ᵐ-⊔ᵐ
)
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₂
_⊔_ : 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₂
}