agda-spa/Map.agda
Danila Fedorin 461732244a Finish all in/not-in proofs.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-07-26 20:40:28 -07:00

318 lines
16 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
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)))
∈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
∈-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 ∈k 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 xs k∈kxs in (v , there k,v∈xs)
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 l 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 = {!!}
-- ------------------------------------------------------------------------
--
-- The following can be proven using plain properties of insert:
--
-- prove that ¬ k ∈k m₁ → (k , v) ∈ m₂ → (k , v) ∈ merge m₁ m₂ (done)
-- prove that k ≢ k' → (k , v) ∈ m → (k , v) ∈ insert k' v' m (done)
-- prove that (k , v) ∈ m₁ → ¬ k ∈k m₂ → (k , v) ∈ merge m₁ m₂ (done)
-- prove that ¬ k ∈k m → (k , v) ∈ insert k v m (done)
--
-- ------------------------------------------------------------------------
--
-- The following relies on uniqueness, since inserts stops after the first encounter.
--
-- prove that (k , v) ∈ m₁ → (k , v') ∈ m₂ → (k, f v v') ∈ merge m₁ m₂ (done)
--
-- ------------------------------------------------------------------------
--
-- The following can probably be proven via keys.
--
-- prove that k ∉k m₁ → k ∉k m₂ → k ∉k merge m₁ m₂ (done)
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₁