Add a 'set' lattice backed by maps

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-09-23 17:12:12 -07:00
parent 4a90a57388
commit 3c346dcd15
3 changed files with 21 additions and 4 deletions

View File

@ -1,8 +1,6 @@
open import Lattice open import Lattice
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.Core using (Rel)
open import Relation.Nullary using (Dec; yes; no; Reflects; ofʸ; ofⁿ)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔_) open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔_)
module Lattice.Map {a b : Level} (A : Set a) (B : Set b) module Lattice.Map {a b : Level} (A : Set a) (B : Set b)
@ -13,7 +11,7 @@ module Lattice.Map {a b : Level} (A : Set a) (B : Set b)
import Data.List.Membership.Propositional as MemProp import Data.List.Membership.Propositional as MemProp
open import Relation.Nullary using (¬_) open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Nat using () open import Data.Nat using ()
open import Data.List using (List; map; []; _∷_; _++_) open import Data.List using (List; map; []; _∷_; _++_)
open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.All using (All; []; _∷_)

19
Lattice/MapSet.agda Normal file
View File

@ -0,0 +1,19 @@
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 _⊔_)
module Lattice.MapSet {a : Level} (A : Set a) (≡-dec-A : Decidable (_≡_ {a} {A})) where
open import Lattice.Unit using () renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to -isLattice)
import Lattice.Map
private module UnitMap = Lattice.Map A _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A -isLattice
open UnitMap using (Map)
open UnitMap using
( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_
; isUnionSemilattice; isIntersectSemilattice; isLattice
) public
MapSet : Set a
MapSet = Map

View File

@ -3,7 +3,7 @@ module Lattice.Unit where
open import Data.Empty using (⊥-elim) open import Data.Empty using (⊥-elim)
open import Data.Product using (_,_) open import Data.Product using (_,_)
open import Data.Nat using (; _≤_; z≤n) open import Data.Nat using (; _≤_; z≤n)
open import Data.Unit using (; tt) open import Data.Unit using (; tt) public
open import Data.Unit.Properties using (_≟_; ≡-setoid) open import Data.Unit.Properties using (_≟_; ≡-setoid)
open import Relation.Binary using (Setoid) open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_)