agda-spa/Map.agda
Danila Fedorin 4aea9a0358 Migrate Maps to including a uniqueness proof
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-07-24 23:55:09 -07:00

137 lines
6.8 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 Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; cong)
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
import Data.List.Membership.Propositional as MemProp
open import Relation.Nullary using (¬_)
open import Data.Nat using ()
open import Data.List using (List; []; _∷_; _++_)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
open import Data.Empty using ()
keys : List (A × B) List A
keys [] = []
keys ((k , v) xs) = k keys xs
data Unique {c} {C : Set c} : List C Set c where
empty : Unique []
push : forall {x : C} {xs : List C}
All (λ x' ¬ x x') xs
Unique xs
Unique (x xs)
Map : Set (a b)
Map = Σ (List (A × B)) (λ l Unique (keys l))
Unique-append : {c} {C : Set c} {x : C} {xs : List C} ¬ MemProp._∈_ x xs Unique xs Unique (xs ++ (x []))
Unique-append {c} {C} {x} {[]} _ _ = push [] empty
Unique-append {c} {C} {x} {x' xs'} x∉xs (push x'≢ uxs') = push (help x'≢) (Unique-append (λ x∈xs' x∉xs (there x∈xs')) uxs')
where
x'≢x : ¬ x' x
x'≢x x'≡x = x∉xs (here (sym x'≡x))
help : {l : List C} All (λ x'' ¬ x' x'') l All (λ x'' ¬ x' x'') (l ++ (x []))
help {[]} _ = x'≢x []
help {e es} (x'≢e x'≢es) = x'≢e help x'≢es
_∈_ : (A × B) List (A × B) Set (a b)
_∈_ p m = MemProp._∈_ p m
foldr : {c} {C : Set c} (A B C C) -> C -> List (A × B) -> C
foldr f b [] = b
foldr f b ((k , v) xs) = f k v (foldr f b xs)
absurd : {a} {A : Set a} A
absurd ()
private module ImplRelation (_≈_ : B B Set b) where
subset : List (A × B) List (A × B) Set (a b)
subset m₁ m₂ = (k : A) (v : B) (k , v) m₁ Σ B (λ v' v v' × ((k , v') m₂))
private module ImplInsert (f : B B B) where
_∈k_ : A List (A × B) Set a
_∈k_ k m = MemProp._∈_ k (keys m)
insert : A B List (A × B) List (A × B)
insert k v [] = (k , v) []
insert k v (x@(k' , v') xs) with ≡-dec-A k k'
... | yes _ = (k' , f v v') xs
... | no _ = x insert k v xs
merge : List (A × B) List (A × B) List (A × B)
merge m₁ m₂ = foldr insert m₂ m₁
insert-keys-∈ : (k : A) (v : B) (l : List (A × B)) k ∈k l keys l keys (insert k v l)
insert-keys-∈ k v ((k' , v') xs) (here k≡k') with (≡-dec-A k k')
... | yes _ = refl
... | no k≢k' = absurd (k≢k' k≡k')
insert-keys-∈ k v ((k' , _) xs) (there k∈kxs) with (≡-dec-A k k')
... | yes _ = refl
... | no _ = cong (λ xs' k' xs') (insert-keys-∈ k v xs k∈kxs)
insert-keys-∉ : (k : A) (v : B) (l : List (A × B)) ¬ (k ∈k l) (keys l ++ (k [])) keys (insert k v l)
insert-keys-∉ k v [] _ = refl
insert-keys-∉ k v ((k' , v') xs) k∉kl with (≡-dec-A k k')
... | yes k≡k' = absurd (k∉kl (here k≡k'))
... | no _ = cong (λ xs' k' xs') (insert-keys-∉ k v xs (λ k∈kxs k∉kl (there k∈kxs)))
∈k-dec : (k : A) (l : List (A × B)) Dec (k ∈k l)
∈k-dec k [] = no (λ ())
∈k-dec k ((k' , v) xs) with (≡-dec-A k k')
... | yes k≡k' = yes (here k≡k')
... | no k≢k' with (∈k-dec k xs)
... | yes k∈kxs = yes (there k∈kxs)
... | no k∉kxs = no witness
where
witness : ¬ k ∈k ((k' , v) xs)
witness (here k≡k') = k≢k' k≡k'
witness (there k∈kxs) = k∉kxs k∈kxs
insert-preserves-unique : (k : A) (v : B) (l : List (A × B)) Unique (keys l) Unique (keys (insert k v l))
insert-preserves-unique k v l u with (∈k-dec k l)
... | yes k∈kl rewrite insert-keys-∈ k v l k∈kl = u
... | no k∉kl rewrite sym (insert-keys-∉ k v l k∉kl) = Unique-append k∉kl u
merge-preserves-unique : (l₁ l₂ : List (A × B)) Unique (keys l₂) Unique (keys (merge l₁ l₂))
merge-preserves-unique [] l₂ u₂ = u₂
merge-preserves-unique ((k₁ , v₁) xs₁) l₂ u₂ = insert-preserves-unique k₁ v₁ (merge xs₁ l₂) (merge-preserves-unique xs₁ l₂ u₂)
-- Map-functional : ∀ (k : A) (v v' : B) (xs : List (A × B)) → Unique (keys ((k , v) ∷ xs)) → MemProp._∈_ (k , v') ((k , v) ∷ xs) → v ≡ v'
-- Map-functional k v v' _ _ (here k,v'≡k,v) = sym (cong proj₂ k,v'≡k,v)
-- Map-functional k v v' xs (push k≢ _) (there k,v'∈xs) = absurd (unique-not-in xs v' (k≢ , k,v'∈xs))
-- where
-- unique-not-in : ∀ (xs : List (A × B)) (v' : B) → ¬ (All (λ k' → ¬ k ≡ k') (keys xs) × (k , v') ∈ xs)
-- unique-not-in ((k' , _) ∷ xs) v' (k≢k' ∷ _ , here k',≡x) = k≢k' (cong proj₁ k',≡x)
-- unique-not-in (_ ∷ xs) v' (_ ∷ rest , there k,v'∈xs) = unique-not-in xs v' (rest , k,v'∈xs)
module _ (f : B B B) where
open ImplInsert f renaming
( insert to insert-impl
; merge to merge-impl
)
insert : A B Map Map
insert k v (kvs , uks) = (insert-impl k v kvs , insert-preserves-unique k v kvs uks)
merge : Map Map Map
merge (kvs₁ , _) (kvs₂ , uks₂) = (merge-impl kvs₁ kvs₂ , merge-preserves-unique kvs₁ kvs₂ uks₂)
module _ (_≈_ : B B Set b) where
open ImplRelation _≈_ renaming (subset to subset-impl)
subset : Map Map Set (a b)
subset (kvs₁ , _) (kvs₂ , _) = subset-impl kvs₁ kvs₂
lift : Map Map Set (a b)
lift m₁ m₂ = subset m₁ m₂ × subset m₂ m₁