Add a generic Map module and prove its induced equivalence relation
This commit is contained in:
parent
8febffc8e3
commit
ab7ed2039a
51
Lattice.agda
51
Lattice.agda
|
@ -1,7 +1,7 @@
|
|||
module Lattice where
|
||||
|
||||
import Data.Nat.Properties as NatProps
|
||||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; isEquivalence)
|
||||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
|
||||
open import Relation.Binary.Definitions
|
||||
open import Data.Nat as Nat using (ℕ; _≤_)
|
||||
open import Data.Product using (_×_; _,_)
|
||||
|
@ -68,6 +68,55 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
|
|||
|
||||
open IsLattice isLattice public
|
||||
|
||||
module IsEquivalenceInstances where
|
||||
module ForMap {a b} (A : Set a) (B : Set b)
|
||||
(≡-dec-A : Decidable (_≡_ {a} {A}))
|
||||
(_≈₂_ : B → B → Set b)
|
||||
(eB : IsEquivalence B _≈₂_) where
|
||||
|
||||
open import Map A B ≡-dec-A using (Map; lift; subset; insert)
|
||||
open import Data.List using (_∷_; []) -- TODO: re-export these with nicer names from map
|
||||
open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
|
||||
|
||||
open IsEquivalence eB renaming
|
||||
( ≈-refl to ≈₂-refl
|
||||
; ≈-sym to ≈₂-sym
|
||||
; ≈-trans to ≈₂-trans
|
||||
)
|
||||
|
||||
private
|
||||
_≈_ : Map → Map → Set (Agda.Primitive._⊔_ a b)
|
||||
_≈_ = lift _≈₂_
|
||||
|
||||
_⊆_ : Map → Map → Set (Agda.Primitive._⊔_ a b)
|
||||
_⊆_ = subset _≈₂_
|
||||
|
||||
⊆-refl : {m : Map} → m ⊆ m
|
||||
⊆-refl k v k,v∈m = (v , (≈₂-refl , k,v∈m))
|
||||
|
||||
⊆-trans : {m₁ m₂ m₃ : Map} → m₁ ⊆ m₂ → m₂ ⊆ m₃ → m₁ ⊆ m₃
|
||||
⊆-trans m₁⊆m₂ m₂⊆m₃ k v k,v∈m₁ =
|
||||
let
|
||||
(v' , (v≈v' , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
|
||||
(v'' , (v'≈v'' , k,v''∈m₃)) = m₂⊆m₃ k v' k,v'∈m₂
|
||||
in (v'' , (≈₂-trans v≈v' v'≈v'' , k,v''∈m₃))
|
||||
|
||||
≈-refl : {m : Map} → m ≈ m
|
||||
≈-refl {m} = (⊆-refl , ⊆-refl)
|
||||
|
||||
≈-sym : {m₁ m₂ : Map} → m₁ ≈ m₂ → m₂ ≈ m₁
|
||||
≈-sym (m₁⊆m₂ , m₂⊆m₁) = (m₂⊆m₁ , m₁⊆m₂)
|
||||
|
||||
≈-trans : {m₁ m₂ m₃ : Map} → m₁ ≈ m₂ → m₂ ≈ m₃ → m₁ ≈ m₃
|
||||
≈-trans (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) = (⊆-trans m₁⊆m₂ m₂⊆m₃ , ⊆-trans m₃⊆m₂ m₂⊆m₁)
|
||||
|
||||
LiftEquivalence : IsEquivalence Map _≈_
|
||||
LiftEquivalence = record
|
||||
{ ≈-refl = ≈-refl
|
||||
; ≈-sym = ≈-sym
|
||||
; ≈-trans = ≈-trans
|
||||
}
|
||||
|
||||
module IsSemilatticeInstances where
|
||||
module ForNat where
|
||||
open Nat
|
||||
|
|
42
Map.agda
Normal file
42
Map.agda
Normal file
|
@ -0,0 +1,42 @@
|
|||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
|
||||
open import Relation.Binary.Definitions using (Decidable)
|
||||
open import Relation.Binary.Core using (Rel)
|
||||
open import Relation.Nullary using (Dec; yes; no)
|
||||
open import Agda.Primitive using (Level; _⊔_)
|
||||
|
||||
module Map {a b : Level} (A : Set a) (B : Set b)
|
||||
(≡-dec-A : Decidable (_≡_ {a} {A}))
|
||||
where
|
||||
|
||||
open import Data.Nat using (ℕ)
|
||||
open import Data.String using (String; _++_)
|
||||
open import Data.List using (List; []; _∷_)
|
||||
open import Data.List.Membership.Propositional using ()
|
||||
open import Data.Product using (_×_; _,_; Σ)
|
||||
open import Data.Unit using (⊤)
|
||||
open import Data.Empty using (⊥)
|
||||
|
||||
Map : Set (a ⊔ b)
|
||||
Map = List (A × B)
|
||||
|
||||
insert : (B → B → B) → A → B → Map → Map
|
||||
insert f k v [] = (k , v) ∷ []
|
||||
insert f k v (x@(k' , v') ∷ xs) with ≡-dec-A k k'
|
||||
... | yes _ = (k , f v v') ∷ xs
|
||||
... | no _ = x ∷ insert f k v xs
|
||||
|
||||
foldr : ∀ {c} {C : Set c} → (A → B → C → C) -> C -> Map -> C
|
||||
foldr f b [] = b
|
||||
foldr f b ((k , v) ∷ xs) = f k v (foldr f b xs)
|
||||
|
||||
_∈_ : (A × B) → Map → Set (a ⊔ b)
|
||||
_∈_ p m = Data.List.Membership.Propositional._∈_ p m
|
||||
|
||||
subset : ∀ (_≈_ : B → B → Set b) → Map → Map → Set (a ⊔ b)
|
||||
subset _≈_ m₁ m₂ = ∀ (k : A) (v : B) → (k , v) ∈ m₁ → Σ B (λ v' → v ≈ v' × ((k , v') ∈ m₂))
|
||||
|
||||
lift : ∀ (_≈_ : B → B → Set b) → Map → Map → Set (a ⊔ b)
|
||||
lift _≈_ m₁ m₂ = (m₁ ⊆ m₂) × (m₂ ⊆ m₁)
|
||||
where
|
||||
_⊆_ : Map → Map → Set (a ⊔ b)
|
||||
_⊆_ = subset _≈_
|
Loading…
Reference in New Issue
Block a user