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

Add an instance of Semilattice for Map.

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2023-07-30 20:36:19 -07:00
parent a4eaa6269f
commit 1b7a3f02eb
2 changed files with 123 additions and 93 deletions
Download Patch File Download Diff File Expand all files Collapse all files

40
Lattice.agda
View File

@@ -112,12 +112,12 @@ module IsEquivalenceInstances where
, ⊆-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₃
}
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
@@ -216,6 +216,34 @@ module IsSemilatticeInstances where
; ⊔-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
private
infix 4 _≈_
infixl 20 _⊔_
_≈_ : Map → Map → Set a
_≈_ = lift (_≈₂_)
_⊔_ : Map → Map → Map
m₁ ⊔ m₂ = union _⊔₂_ m₁ m₂
module MapEquiv = IsEquivalenceInstances.ForMap A B ≡-dec-A _≈₂_ (IsSemilattice.≈-equiv sB)
MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_
MapIsUnionSemilattice = record
{ ≈-equiv = MapEquiv.LiftEquivalence
; ⊔-assoc = union-assoc _≈₂_ (IsSemilattice.≈-refl sB) (IsSemilattice.≈-sym sB) _⊔₂_ (IsSemilattice.⊔-assoc sB)
; ⊔-comm = union-comm _≈₂_ (IsSemilattice.≈-refl sB) (IsSemilattice.≈-sym sB) _⊔₂_ (IsSemilattice.⊔-comm sB)
; ⊔-idemp = union-idemp _≈₂_ (IsSemilattice.≈-refl sB) (IsSemilattice.≈-sym sB) _⊔₂_ (IsSemilattice.⊔-idemp sB)
}
module IsLatticeInstances where
module ForNat where
open Nat