DanilaFe
/
agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Format FiniteMap a little bit better 

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-02 14:54:44 -08:00
parent 112dcb2208
commit ec2b1ec3ba
1 changed files with 26 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
Lattice/FiniteMap.agda
View File

@ -1,13 +1,13 @@
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 Relation.Binary.PropositionalEquality as Eq
using (_≡_;refl; sym; trans; cong; subst)
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}))
(≡-dec-A : IsDecidable (_≡_ {a} {A}))
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
@ -43,22 +43,36 @@ module _ (ks : List A) where
≈-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)
_⊔_ (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)
_⊓_ (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₃}
{ ≈-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₄
; ≈-⊔-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
@ -67,7 +81,9 @@ module _ (ks : List A) where
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₄
; ≈-⊔-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