agda-spa/Map.agda
Danila Fedorin 4033a1b33d Prove most of commutativity by relying on in-dec.
The "no" case still needs to be dismissed, but that can probably
be done by some lemma about keys in maps.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-07-28 00:05:41 -07:00

343 lines
19 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; trans; cong)
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; _⊔_)
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; map; []; _∷_; _++_)
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 = map proj₁
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}
¬ 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
All¬-¬Any : {p c} {C : Set c} {P : C Set p} {l : List C} All (λ x ¬ P x) l ¬ Any P l
All¬-¬Any {l = x xs} (¬Px _) (here Px) = ¬Px Px
All¬-¬Any {l = x xs} (_ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
absurd : {a} {A : Set a} A
absurd ()
private module _ where
open MemProp using (_∈_)
unique-not-in : {k : A} {v : B} {l : List (A × B)}
¬ (All (λ k' ¬ k k') (keys l) × (k , v) l)
unique-not-in {l = (k' , _) xs} (k≢k' _ , here k',≡x) =
k≢k' (cong proj₁ k',≡x)
unique-not-in {l = _ xs} (_ rest , there k,v'∈xs) =
unique-not-in (rest , k,v'∈xs)
ListAB-functional : {k : A} {v v' : B} {l : List (A × B)}
Unique (keys l) (k , v) l (k , v') l v v'
ListAB-functional _ (here k,v≡x) (here k,v'≡x) =
cong proj₂ (trans k,v≡x (sym k,v'≡x))
ListAB-functional (push k≢xs _) (here k,v≡x) (there k,v'∈xs)
rewrite sym k,v≡x = absurd (unique-not-in (k≢xs , k,v'∈xs))
ListAB-functional (push k≢xs _) (there k,v∈xs) (here k,v'≡x)
rewrite sym k,v'≡x = absurd (unique-not-in (k≢xs , k,v∈xs))
ListAB-functional {l = _ xs } (push _ uxs) (there k,v∈xs) (there k,v'∈xs) =
ListAB-functional uxs k,v∈xs k,v'∈xs
∈k-dec : (k : A) (l : List (A × B)) Dec (k keys 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 keys ((k' , v) xs)
witness (here k≡k') = k≢k' k≡k'
witness (there k∈kxs) = k∉kxs k∈kxs
∈-cong : {c d} {C : Set c} {D : Set d} {c : C} {l : List C}
(f : C D) c l f c map f l
∈-cong f (here c≡c') = here (cong f c≡c')
∈-cong f (there c∈xs) = there (∈-cong f c∈xs)
locate : {k : A} {l : List (A × B)} k keys l Σ B (λ v (k , v) l)
locate {k} {(k' , v) xs} (here k≡k') rewrite k≡k' = (v , here refl)
locate {k} {(k' , v) xs} (there k∈kxs) = let (v , k,v∈xs) = locate k∈kxs in (v , there k,v∈xs)
private module ImplRelation (_≈_ : B B Set b) where
open MemProp using (_∈_)
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
open import Data.List using (map)
open MemProp using (_∈_)
private
_∈k_ : A List (A × B) Set a
_∈k_ k m = k (keys 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)
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)))
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₂)
insert-preserves-∈-right : (k k' : A) (v v' : B) (l : List (A × B))
¬ k k' (k , v) l (k , v) insert k' v' l
insert-preserves-∈-right k k' v v' (x xs) k≢k' (here k,v=x)
rewrite sym k,v=x with ≡-dec-A k' k
... | yes k'≡k = absurd (k≢k' (sym k'≡k))
... | no _ = here refl
insert-preserves-∈-right k k' v v' ((k'' , _) xs) k≢k' (there k,v∈xs)
with ≡-dec-A k' k''
... | yes _ = there k,v∈xs
... | no _ = there (insert-preserves-∈-right k k' v v' xs k≢k' k,v∈xs)
insert-preserves-∈k-right : (k k' : A) (v' : B) (l : List (A × B))
¬ k k' k ∈k l k ∈k insert k' v' l
insert-preserves-∈k-right k k' v' l k≢k' k∈kl =
let (v , k,v∈l) = locate k∈kl
in ∈-cong proj₁ (insert-preserves-∈-right k k' v v' l k≢k' k,v∈l)
insert-preserves-∉-right : (k k' : A) (v' : B) (l : List (A × B))
¬ k k' ¬ k ∈k l ¬ k ∈k insert k' v' l
insert-preserves-∉-right k k' v' [] k≢k' k∉kl (here k≡k') = k≢k' k≡k'
insert-preserves-∉-right k k' v' [] k≢k' k∉kl (there ())
insert-preserves-∉-right k k' v' ((k'' , v'') xs) k≢k' k∉kl k∈kil
with ≡-dec-A k k''
... | yes k≡k'' = k∉kl (here k≡k'')
... | no k≢k'' with ≡-dec-A k' k'' | k∈kil
... | yes k'≡k'' | here k≡k'' = k≢k'' k≡k''
... | yes k'≡k'' | there k∈kxs = k∉kl (there k∈kxs)
... | no k'≢k'' | here k≡k'' = k∉kl (here k≡k'')
... | no k'≢k'' | there k∈kxs = insert-preserves-∉-right k k' v' xs k≢k'
(λ k∈kxs k∉kl (there k∈kxs)) k∈kxs
merge-preserves-∉ : (k : A) (l₁ l₂ : List (A × B))
¬ k ∈k l₁ ¬ k ∈k l₂ ¬ k ∈k merge l₁ l₂
merge-preserves-∉ k [] l₂ _ k∉kl₂ = k∉kl₂
merge-preserves-∉ k ((k' , v') xs₁) l₂ k∉kl₁ k∉kl₂
with ≡-dec-A k k'
... | yes k≡k' = absurd (k∉kl₁ (here k≡k'))
... | no k≢k' = insert-preserves-∉-right k k' v' _ k≢k' (merge-preserves-∉ k xs₁ l₂ (λ k∈kxs₁ k∉kl₁ (there k∈kxs₁)) k∉kl₂)
merge-preserves-keys₁ : (k : A) (v : B) (l₁ l₂ : List (A × B))
¬ k ∈k l₁ (k , v) l₂ (k , v) merge l₁ l₂
merge-preserves-keys₁ k v [] l₂ _ k,v∈l₂ = k,v∈l₂
merge-preserves-keys₁ k v ((k' , v') xs₁) l₂ k∉kl₁ k,v∈l₂ =
let recursion = merge-preserves-keys₁ k v xs₁ l₂ (λ k∈xs₁ k∉kl₁ (there k∈xs₁)) k,v∈l₂
in insert-preserves-∈-right k k' v v' _ (λ k≡k' k∉kl₁ (here k≡k')) recursion
insert-fresh : (k : A) (v : B) (l : List (A × B))
¬ k ∈k l (k , v) insert k v l
insert-fresh k v [] k∉kl = here refl
insert-fresh k v ((k' , v') xs) k∉kl
with ≡-dec-A k k'
... | yes k≡k' = absurd (k∉kl (here k≡k'))
... | no _ = there (insert-fresh k v xs (λ k∈kxs k∉kl (there k∈kxs)))
merge-preserves-keys₂ : (k : A) (v : B) (l₁ l₂ : List (A × B))
Unique (keys l₁) (k , v) l₁ ¬ k ∈k l₂ (k , v) merge l₁ l₂
merge-preserves-keys₂ k v ((k' , v') xs₁) l₂ (push k'≢xs₁ uxs₁) (there k,v∈xs₁) k∉kl₂ =
insert-preserves-∈-right k k' v v' (merge xs₁ l₂) k≢k' k,v∈mxs₁l
where
k,v∈mxs₁l = merge-preserves-keys₂ k v xs₁ l₂ uxs₁ k,v∈xs₁ k∉kl₂
k≢k' : ¬ k k'
k≢k' with ≡-dec-A k k'
... | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁))
... | no k≢k' = k≢k'
merge-preserves-keys₂ k v ((k' , v') xs₁) l₂ (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂
rewrite cong proj₁ k,v≡k',v' rewrite cong proj₂ k,v≡k',v' =
insert-fresh k' v' _ (merge-preserves-∉ k' xs₁ l₂ (All¬-¬Any k'≢xs₁) k∉kl₂)
insert-combines : (k : A) (v v' : B) (l : List (A × B))
Unique (keys l) (k , v') l (k , f v v') (insert k v l)
insert-combines k v v' ((k' , v'') xs) _ (here k,v'≡k',v'')
rewrite cong proj₁ k,v'≡k',v'' rewrite cong proj₂ k,v'≡k',v''
with ≡-dec-A k' k'
... | yes _ = here refl
... | no k≢k' = absurd (k≢k' refl)
insert-combines k v v' ((k' , v'') xs) (push k'≢xs uxs) (there k,v'∈xs)
with ≡-dec-A k k'
... | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs (∈-cong proj₁ k,v'∈xs))
... | no k≢k' = there (insert-combines k v v' xs uxs k,v'∈xs)
merge-combines : forall (k : A) (v₁ v₂ : B) (l₁ l₂ : List (A × B))
Unique (keys l₁) Unique (keys l₂)
(k , v₁) l₁ (k , v₂) l₂ (k , f v₁ v₂) merge l₁ l₂
merge-combines k v₁ v₂ ((k' , v) xs₁) l₂ (push k'≢xs₁ uxs₁) ul₂ (here k,v₁≡k',v) k,v₂∈l₂
rewrite cong proj₁ (sym (k,v₁≡k',v)) rewrite cong proj₂ (sym (k,v₁≡k',v)) =
insert-combines k v₁ v₂ _ (merge-preserves-Unique xs₁ l₂ ul₂) (merge-preserves-keys₁ k v₂ xs₁ l₂ (All¬-¬Any k'≢xs₁) k,v₂∈l₂)
merge-combines k v₁ v₂ ((k' , v) xs₁) l₂ (push k'≢xs₁ uxs₁) ul₂ (there k,v₁∈xs₁) k,v₂∈l₂ =
insert-preserves-∈-right k k' (f v₁ v₂) v _ k≢k' (merge-combines k v₁ v₂ xs₁ l₂ uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂)
where
k≢k' : ¬ k k'
k≢k' with ≡-dec-A k k'
... | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v₁∈xs₁))
... | no k≢k' = k≢k'
Map : Set (a b)
Map = Σ (List (A × B)) (λ l Unique (keys l))
_∈_ : (A × B) Map Set (a b)
_∈_ p (kvs , _) = MemProp._∈_ p kvs
_∈k_ : A Map Set a
_∈k_ k (kvs , _) = MemProp._∈_ k (keys kvs)
Map-functional : {k : A} {v v' : B} {m : Map} (k , v) m (k , v') m v v'
Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m
data Provenance (k : A) (m₁ m₂ : Map) : Set (a b) where
both : (v₁ v₂ : B) (k , v₁) m₁ (k , v₂) m₂ Provenance k m₁ m₂
in₁ : (v₁ : B) (k , v₁) m₁ ¬ k ∈k m₂ Provenance k m₁ m₂
in₂ : (v₂ : B) ¬ k ∈k m₁ (k , v₂) m₂ Provenance k m₁ m₂
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₂)
MergeResult : {k : A} {m₁ m₂ : Map} Provenance k m₁ m₂ Set (a b)
MergeResult {k} {m₁} {m₂} (both v₁ v₂ _ _) = (k , f v₁ v₂) merge m₁ m₂
MergeResult {k} {m₁} {m₂} (in v₁ _ _) = (k , v₁) merge m₁ m₂
MergeResult {k} {m₁} {m₂} (in v₂ _ _) = (k , v₂) merge m₁ m₂
merge-provenance : (m₁ m₂ : Map) (k : A) k ∈k merge m₁ m₂ Σ (Provenance k m₁ m₂) MergeResult
merge-provenance m₁@(l₁ , u₁) m₂@(l₂ , u₂) k k∈km₁m₂
with ∈k-dec k l₁ | ∈k-dec k l₂
... | yes k∈kl₁ | yes k∈kl₂ =
let
(v₁ , k,v₁∈l₁) = locate k∈kl₁
(v₂ , k,v₂∈l₂) = locate k∈kl₂
in
(both v₁ v₂ k,v₁∈l₁ k,v₂∈l₂ , merge-combines k v₁ v₂ l₁ l₂ u₁ u₂ k,v₁∈l₁ k,v₂∈l₂)
... | yes k∈kl₁ | no k∉kl₂ =
let
(v₁ , k,v₁∈l₁) = locate k∈kl₁
in
(in v₁ k,v₁∈l₁ k∉kl₂ , merge-preserves-keys₂ k v₁ l₁ l₂ u₁ k,v₁∈l₁ k∉kl₂)
... | no k∉kl₁ | yes k∈kl₂ =
let
(v₂ , k,v₂∈l₂) = locate k∈kl₂
in
(in v₂ k∉kl₁ k,v₂∈l₂ , merge-preserves-keys₁ k v₂ l₁ l₂ k∉kl₁ k,v₂∈l₂)
... | no k∉kl₁ | no k∉kl₂ = absurd (merge-preserves-∉ k l₁ l₂ k∉kl₁ k∉kl₂ k∈km₁m₂)
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₁
module _ (f : B B B) where
module _ (f-comm : (b₁ b₂ : B) f b₁ b₂ f b₂ b₁) where
merge-comm : forall (m₁ m₂ : Map) lift (_≡_) (merge f m₁ m₂) (merge f m₂ m₁)
merge-comm m₁ m₂ = (merge-comm-subset m₁ m₂ , merge-comm-subset m₂ m₁)
where
merge-comm-subset : (m₁ m₂ : Map) subset (_≡_) (merge f m₁ m₂) (merge f m₂ m₁)
merge-comm-subset m₁ m₂ k v k,v∈m₁m₂
with ∈k-dec k (proj₁ (merge f m₂ m₁) )
... | no k∉km₂m₁ = {!!}
... | yes k∈km₂m₁ with merge-provenance f m₁ m₂ k (∈-cong proj₁ k,v∈m₁m₂) | merge-provenance f m₂ m₁ k k∈km₂m₁
... | (both v₁ v₂ v₁∈m₁ v₂∈m₂ , v₁v₂∈m₁m₂) | (both v₂' v₁' v₂'∈m₂ v₁'∈m₁ , v₂'v₁'∈m₂m₁)
rewrite Map-functional {m = merge f m₁ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂
rewrite Map-functional {m = m₁} v₁∈m₁ v₁'∈m₁
rewrite Map-functional {m = m₂} v₂∈m₂ v₂'∈m₂ = (f v₂' v₁' , (f-comm v₁' v₂' , v₂'v₁'∈m₂m₁))
... | (in v₁ v₁∈m₁ _ , v₁∈m₁m₂) | (in v₁' _ v₁'∈m₁ , v₁'∈m₂m₁)
rewrite Map-functional {m = merge f m₁ m₂} k,v∈m₁m₂ v₁∈m₁m₂ =
(v₁' , (Map-functional {m = m₁} v₁∈m₁ v₁'∈m₁ , v₁'∈m₂m₁))
... | (in v₂ _ v₂∈m₂ , v₂∈m₁m₂) | (in v₂' v₂'∈m₂ _ , v₂'∈m₂m₁)
rewrite Map-functional {m = merge f m₁ m₂} k,v∈m₁m₂ v₂∈m₁m₂ =
(v₂' , (Map-functional {m = m₂} v₂∈m₂ v₂'∈m₂ , v₂'∈m₂m₁))
-- The rest of the cases are to be dismissed.
... | (both v₁ v₂ v₁∈m₁ v₂∈m₂ , _) | (in v₂' v₂'∈m₂ k∉km₁ , _) = absurd (k∉km₁ (∈-cong proj₁ v₁∈m₁))
... | (both v₁ v₂ v₁∈m₁ v₂∈m₂ , _) | (in v₁' k∉km₂ v₁'∈m₁ , _) = absurd (k∉km₂ (∈-cong proj₁ v₂∈m₂))
... | (in v₁ v₁∈m₁ k∉km₂ , _) | (both v₂' v₁' v₂'∈m₂ v₁'∈m₁ , _) = absurd (k∉km₂ (∈-cong proj₁ v₂'∈m₂))
... | (in v₁ v₁∈m₁ k∉km₂ , _) | (in v₂' v₂'∈m₂ k∉km₁ , _) = absurd (k∉km₂ (∈-cong proj₁ v₂'∈m₂))
... | (in v₂ k∉km₁ v₂∈m₂ , v₂∈m₁m₂) | (both v₂' v₁' v₂'∈m₂ v₁'∈m₁ , _) = absurd (k∉km₁ (∈-cong proj₁ v₁'∈m₁))
... | (in v₂ k∉km₁ v₂∈m₂ , v₂∈m₁m₂) | (in v₁' _ v₁'∈m₁ , v₁'∈m₂m₁) = absurd (k∉km₁ (∈-cong proj₁ v₁'∈m₁))