agda-spa/Map.agda
Danila Fedorin 87a476ab9e Add proofs of uniqueness preservation for map insert
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-07-24 22:51:40 -07:00

116 lines
6.0 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
open import Relation.Nullary using (¬_)
open import Data.Nat using ()
open import Data.List using (List; []; _∷_; _++_)
open import Data.List.Membership.Propositional using ()
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.Unit using ()
open import Data.Empty using ()
Map : Set (a b)
Map = List (A × B)
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)
Unique-append : {c} {C : Set c} {x : C} {xs : List C} ¬ Data.List.Membership.Propositional._∈_ 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 = Data.List.Membership.Propositional._∈_ p m
_∈k_ : A List (A × B) Set a
_∈k_ k m = Data.List.Membership.Propositional._∈_ k (keys m)
subset : (_≈_ : B B Set b) 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₂))
lift : (_≈_ : B B Set b) List (A × B) List (A × B) Set (a b)
lift _≈_ m₁ m₂ = (m₁ m₂) × (m₂ m₁)
where
_⊆_ : List (A × B) List (A × B) Set (a b)
_⊆_ = subset _≈_
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)
insert : (B B B) A B List (A × B) List (A × B)
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
merge : (B B B) List (A × B) List (A × B) List (A × B)
merge f m₁ m₂ = foldr (insert f) m₂ m₁
absurd : {a} {A : Set a} A
absurd ()
insert-keys-∈ : (f : B B B) (k : A) (v : B) (l : List (A × B)) k ∈k l keys l keys (insert f k v l)
insert-keys-∈ f 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-∈ f k v ((k' , _) xs) (there k∈kxs) with (≡-dec-A k k')
... | yes _ = refl
... | no _ = cong (λ xs' k' xs') (insert-keys-∈ f k v xs k∈kxs)
insert-keys-∉ : (f : B B B) (k : A) (v : B) (l : List (A × B)) ¬ (k ∈k l) (keys l ++ (k [])) keys (insert f k v l)
insert-keys-∉ f k v [] _ = refl
insert-keys-∉ f 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-∉ f 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 : (f : B B B) (k : A) (v : B) (l : List (A × B)) Unique (keys l) Unique (keys (insert f k v l))
insert-preserves-unique f k v l u with (∈k-dec k l)
... | yes k∈kl rewrite insert-keys-∈ f k v l k∈kl = u
... | no k∉kl rewrite sym (insert-keys-∉ f k v l k∉kl) = Unique-append k∉kl u
Map-functional : (k : A) (v v' : B) (xs : List (A × B)) Unique (keys ((k , v) xs)) Data.List.Membership.Propositional._∈_ (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)