agda-spa/Map.agda

439 lines
27 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 : {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
union : List (A × B) List (A × B) List (A × B)
union 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∈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∈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-∈ {v = v} k∈kl = u
... | no k∉kl rewrite sym (insert-keys-∉ {v = v} k∉kl) = Unique-append k∉kl u
union-preserves-Unique : (l₁ l₂ : List (A × B))
Unique (keys l₂) Unique (keys (union l₁ l₂))
union-preserves-Unique [] l₂ u₂ = u₂
union-preserves-Unique ((k₁ , v₁) xs₁) l₂ u₂ =
insert-preserves-Unique (union-preserves-Unique xs₁ l₂ u₂)
insert-fresh : {k : A} {v : B} {l : List (A × B)}
¬ k ∈k l (k , v) insert k v l
insert-fresh {l = []} k∉kl = here refl
insert-fresh {k} {l = (k' , v') xs} k∉kl
with ≡-dec-A k k'
... | yes k≡k' = absurd (k∉kl (here k≡k'))
... | no _ = there (insert-fresh (λ k∈kxs k∉kl (there k∈kxs)))
insert-preserves-∉k : {k k' : A} {v' : B} {l : List (A × B)}
¬ k k' ¬ k ∈k l ¬ k ∈k insert k' v' l
insert-preserves-∉k {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k'
insert-preserves-∉k {l = []} k≢k' k∉kl (there ())
insert-preserves-∉k {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-∉k k≢k'
(λ k∈kxs k∉kl (there k∈kxs)) k∈kxs
union-preserves-∉ : {k : A} {l₁ l₂ : List (A × B)}
¬ k ∈k l₁ ¬ k ∈k l₂ ¬ k ∈k union l₁ l₂
union-preserves-∉ {l₁ = []} _ k∉kl₂ = k∉kl₂
union-preserves-∉ {k} {(k' , v') xs₁} k∉kl₁ k∉kl₂
with ≡-dec-A k k'
... | yes k≡k' = absurd (k∉kl₁ (here k≡k'))
... | no k≢k' = insert-preserves-∉k k≢k' (union-preserves-∉ (λ k∈kxs₁ k∉kl₁ (there k∈kxs₁)) k∉kl₂)
insert-preserves-∈k : {k k' : A} {v' : B} {l : List (A × B)}
k ∈k l k ∈k insert k' v' l
insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') xs} (here k≡k'')
with (≡-dec-A k' k'')
... | yes _ = here k≡k''
... | no _ = here k≡k''
insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') xs} (there k∈kxs)
with (≡-dec-A k' k'')
... | yes _ = there k∈kxs
... | no _ = there (insert-preserves-∈k k∈kxs)
union-preserves-∈k₁ : {k : A} {l₁ l₂ : List (A × B)}
k ∈k l₁ k ∈k (union l₁ l₂)
union-preserves-∈k₁ {k} {(k' , v') xs} {l₂} (here k≡k')
with ∈k-dec k (union xs l₂)
... | yes k∈kxsl₂ = insert-preserves-∈k k∈kxsl₂
... | no k∉kxsl₂ rewrite k≡k' = ∈-cong proj₁ (insert-fresh k∉kxsl₂)
union-preserves-∈k₁ {k} {(k' , v') xs} {l₂} (there k∈kxs) =
insert-preserves-∈k (union-preserves-∈k₁ k∈kxs)
union-preserves-∈k₂ : {k : A} {l₁ l₂ : List (A × B)}
k ∈k l₂ k ∈k (union l₁ l₂)
union-preserves-∈k₂ {k} {[]} {l₂} k∈kl₂ = k∈kl₂
union-preserves-∈k₂ {k} {(k' , v') xs} {l₂} k∈kl₂ =
insert-preserves-∈k (union-preserves-∈k₂ {l₁ = xs} k∈kl₂)
∉-union-∉-either : {k : A} {l₁ l₂ : List (A × B)}
¬ k ∈k union l₁ l₂ ¬ k ∈k l₁ × ¬ k ∈k l₂
∉-union-∉-either {k} {l₁} {l₂} k∉l₁l₂
with ∈k-dec k l₁
... | yes k∈kl₁ = absurd (k∉l₁l₂ (union-preserves-∈k₁ k∈kl₁))
... | no k∉kl₁ with ∈k-dec k l₂
... | yes k∈kl₂ = absurd (k∉l₁l₂ (union-preserves-∈k₂ {l₁ = l₁} k∈kl₂))
... | no k∉kl₂ = (k∉kl₁ , k∉kl₂)
insert-preserves-∈ : {k k' : A} {v v' : B} {l : List (A × B)}
¬ k k' (k , v) l (k , v) insert k' v' l
insert-preserves-∈ {k} {k'} {l = 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-∈ {k} {k'} {l = (k'' , _) xs} k≢k' (there k,v∈xs)
with ≡-dec-A k' k''
... | yes _ = there k,v∈xs
... | no _ = there (insert-preserves-∈ k≢k' k,v∈xs)
union-preserves-∈₂ : {k : A} {v : B} {l₁ l₂ : List (A × B)}
¬ k ∈k l₁ (k , v) l₂ (k , v) union l₁ l₂
union-preserves-∈₂ {l₁ = []} _ k,v∈l₂ = k,v∈l₂
union-preserves-∈₂ {l₁ = (k' , v') xs₁} k∉kl₁ k,v∈l₂ =
let recursion = union-preserves-∈₂ (λ k∈xs₁ k∉kl₁ (there k∈xs₁)) k,v∈l₂
in insert-preserves-∈ (λ k≡k' k∉kl₁ (here k≡k')) recursion
union-preserves-∈₁ : {k : A} {v : B} {l₁ l₂ : List (A × B)}
Unique (keys l₁) (k , v) l₁ ¬ k ∈k l₂ (k , v) union l₁ l₂
union-preserves-∈₁ {k} {v} {(k' , v') xs₁} (push k'≢xs₁ uxs₁) (there k,v∈xs₁) k∉kl₂ =
insert-preserves-∈ k≢k' k,v∈mxs₁l
where
k,v∈mxs₁l = union-preserves-∈₁ 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'
union-preserves-∈₁ {l₁ = (k' , v') xs₁} (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 (union-preserves-∉ (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 {l = (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} {l = (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 uxs k,v'∈xs)
union-combines : {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₂) union l₁ l₂
union-combines {l₁ = (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 (union-preserves-Unique xs₁ l₂ ul₂) (union-preserves-∈₂ (All¬-¬Any k'≢xs₁) k,v₂∈l₂)
union-combines {k} {l₁ = (k' , v) xs₁} (push k'≢xs₁ uxs₁) ul₂ (there k,v₁∈xs₁) k,v₂∈l₂ =
insert-preserves-∈ k≢k' (union-combines 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 Expr : Set (a b) where
`_ : Map Expr
__ : Expr Expr Expr
module _ (f : B B B) where
open ImplInsert f renaming
( insert to insert-impl
; union to union-impl
)
insert : A B Map Map
insert k v (kvs , uks) = (insert-impl k v kvs , insert-preserves-Unique uks)
union : Map Map Map
union (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
⟦_⟧ : Expr -> Map
` m = m
e₁ e₂ = union e₁ e₂
data Provenance (k : A) : B Expr Set (a b) where
single : {v : B} {m : Map} (k , v) m Provenance k v (` m)
in₁ : {v : B} {e₁ e₂ : Expr} Provenance k v e₁ ¬ k ∈k e₂ Provenance k v (e₁ e₂)
in₂ : {v : B} {e₁ e₂ : Expr} ¬ k ∈k e₁ Provenance k v e₂ Provenance k v (e₁ e₂)
bothᵘ : {v₁ v₂ : B} {e₁ e₂ : Expr} Provenance k v₁ e₁ Provenance k v₂ e₂ Provenance k (f v₁ v₂) (e₁ e₂)
Expr-Provenance : (k : A) (e : Expr) k ∈k e Σ B (λ v (Provenance k v e × (k , v) e ))
Expr-Provenance k (` m) k∈km = let (v , k,v∈m) = locate k∈km in (v , (single k,v∈m , k,v∈m))
Expr-Provenance k (e₁ e₂) k∈ke₁e₂
with ∈k-dec k (proj₁ e₁ ) | ∈k-dec k (proj₁ e₂ )
... | yes k∈ke₁ | yes k∈ke₂ =
let (v₁ , (g₁ , k,v₁∈e₁)) = Expr-Provenance k e₁ k∈ke₁
(v₂ , (g₂ , k,v₂∈e₂)) = Expr-Provenance k e₂ k∈ke₂
in (f v₁ v₂ , (bothᵘ g₁ g₂ , union-combines (proj₂ e₁ ) (proj₂ e₂ ) k,v₁∈e₁ k,v₂∈e₂))
... | yes k∈ke₁ | no k∉ke₂ =
let (v₁ , (g₁ , k,v₁∈e₁)) = Expr-Provenance k e₁ k∈ke₁
in (v₁ , (in g₁ k∉ke₂ , union-preserves-∈₁ (proj₂ e₁ ) k,v₁∈e₁ k∉ke₂))
... | no k∉ke₁ | yes k∈ke₂ =
let (v₂ , (g₂ , k,v₂∈e₂)) = Expr-Provenance k e₂ k∈ke₂
in (v₂ , (in k∉ke₁ g₂ , union-preserves-∈₂ k∉ke₁ k,v₂∈e₂))
... | no k∉ke₁ | no k∉ke₂ = absurd (union-preserves-∉ k∉ke₁ k∉ke₂ k∈ke₁e₂)
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 _ (≈-refl : {b : B} b b)
(≈-sym : {b₁ b₂ : B} b₁ b₂ b₂ b₁)
(f : B B B) where
module I = ImplInsert f
module _ (f-idemp : (b : B) f b b b) where
union-idemp : (m : Map) lift (union f m m) m
union-idemp m@(l , u) = (mm-m-subset , m-mm-subset)
where
mm-m-subset : subset (union f m m) m
mm-m-subset k v k,v∈mm
with Expr-Provenance f k ((` m) (` m)) (∈-cong proj₁ k,v∈mm)
... | (_ , (bothᵘ (single {v'} v'∈m) (single {v''} v''∈m) , v'v''∈mm))
rewrite Map-functional {m = m} v'∈m v''∈m
rewrite Map-functional {m = union f m m} k,v∈mm v'v''∈mm =
(v'' , (f-idemp v'' , v''∈m))
... | (_ , (in (single {v'} v'∈m) k∉km , _)) = absurd (k∉km (∈-cong proj₁ v'∈m))
... | (_ , (in k∉km (single {v''} v''∈m) , _)) = absurd (k∉km (∈-cong proj₁ v''∈m))
m-mm-subset : subset m (union f m m)
m-mm-subset k v k,v∈m = (f v v , (≈-sym (f-idemp v) , I.union-combines u u k,v∈m k,v∈m))
module _ (f-comm : (b₁ b₂ : B) f b₁ b₂ f b₂ b₁) where
union-comm : (m₁ m₂ : Map) lift (union f m₁ m₂) (union f m₂ m₁)
union-comm m₁ m₂ = (union-comm-subset m₁ m₂ , union-comm-subset m₂ m₁)
where
union-comm-subset : (m₁ m₂ : Map) subset (union f m₁ m₂) (union f m₂ m₁)
union-comm-subset m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
with Expr-Provenance f k ((` m₁) (` m₂)) (∈-cong proj₁ k,v∈m₁m₂)
... | (_ , (bothᵘ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) , v₁v₂∈m₁m₂))
rewrite Map-functional {m = union f m₁ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
(f v₂ v₁ , (f-comm v₁ v₂ , I.union-combines u₂ u₁ v₂∈m₂ v₁∈m₁))
... | (_ , (in {v₁} (single v₁∈m₁) k∉km₂ , v₁∈m₁m₂))
rewrite Map-functional {m = union f m₁ m₂} k,v∈m₁m₂ v₁∈m₁m₂ =
(v₁ , (≈-refl , I.union-preserves-∈₂ k∉km₂ v₁∈m₁))
... | (_ , (in {v₂} k∉km₁ (single v₂∈m₂) , v₂∈m₁m₂))
rewrite Map-functional {m = union f m₁ m₂} k,v∈m₁m₂ v₂∈m₁m₂ =
(v₂ , (≈-refl , I.union-preserves-∈₁ u₂ v₂∈m₂ k∉km₁))
module _ (f-assoc : (b₁ b₂ b₃ : B) f (f b₁ b₂) b₃ f b₁ (f b₂ b₃)) where
union-assoc : (m₁ m₂ m₃ : Map) lift (union f (union f m₁ m₂) m₃) (union f m₁ (union f m₂ m₃))
union-assoc m₁@(l₁ , u₁) m₂@(l₂ , u₂) m₃@(l₃ , u₃) = (union-assoc₁ , union-assoc₂)
where
union-assoc₁ : subset (union f (union f m₁ m₂) m₃) (union f m₁ (union f m₂ m₃))
union-assoc₁ k v k,v∈m₁₂m₃
with Expr-Provenance f k (((` m₁) (` m₂)) (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
... | (_ , (in k∉ke₁₂ (single {v₃} v₃∈e₃) , v₃∈m₁₂m₃))
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₃∈m₁₂m₃ =
let (k∉ke₁ , k∉ke₂) = I.∉-union-∉-either {l₁ = l₁} {l₂ = l₂} k∉ke₁₂
in (v₃ , (≈-refl , I.union-preserves-∈₂ k∉ke₁ (I.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
... | (_ , (in (in k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ , v₂∈m₁₂m₃))
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₂∈m₁₂m₃ =
(v₂ , (≈-refl , I.union-preserves-∈₂ k∉ke₁ (I.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
... | (_ , (bothᵘ (in k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₂v₃∈m₁₂m₃))
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₂v₃∈m₁₂m₃ =
(f v₂ v₃ , (≈-refl , I.union-preserves-∈₂ k∉ke₁ (I.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
... | (_ , (in (in (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ , v₁∈m₁₂m₃))
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁∈m₁₂m₃ =
(v₁ , (≈-refl , I.union-preserves-∈₁ u₁ v₁∈e₁ (I.union-preserves-∉ k∉ke₂ k∉ke₃)))
... | (_ , (bothᵘ (in (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) , v₁v₃∈m₁₂m₃))
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₃∈m₁₂m₃ =
(f v₁ v₃ , (≈-refl , I.union-combines u₁ (I.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
... | (_ , (in (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃), v₁v₂∈m₁₂m₃)
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂∈m₁₂m₃ =
(f v₁ v₂ , (≈-refl , I.union-combines u₁ (I.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
... | (_ , (bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
(f v₁ (f v₂ v₃) , (f-assoc v₁ v₂ v₃ , I.union-combines u₁ (I.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
union-assoc₂ : subset (union f m₁ (union f m₂ m₃)) (union f (union f m₁ m₂) m₃)
union-assoc₂ k v k,v∈m₁m₂₃
with Expr-Provenance f k ((` m₁) ((` m₂) (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃)
... | (_ , (in k∉ke₁ (in k∉ke₂ (single {v₃} v₃∈e₃)) , v₃∈m₁m₂₃))
rewrite Map-functional {m = union f m₁ (union f m₂ m₃)} k,v∈m₁m₂₃ v₃∈m₁m₂₃ =
(v₃ , (≈-refl , I.union-preserves-∈₂ (I.union-preserves-∉ k∉ke₁ k∉ke₂) v₃∈e₃))
... | (_ , (in k∉ke₁ (in (single {v₂} v₂∈e₂) k∉ke₃) , v₂∈m₁m₂₃))
rewrite Map-functional {m = union f m₁ (union f m₂ m₃)} k,v∈m₁m₂₃ v₂∈m₁m₂₃ =
(v₂ , (≈-refl , I.union-preserves-∈₁ (I.union-preserves-Unique l₁ l₂ u₂) (I.union-preserves-∈₂ k∉ke₁ v₂∈e₂) k∉ke₃))
... | (_ , (in k∉ke₁ (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₂v₃∈m₁m₂₃))
rewrite Map-functional {m = union f m₁ (union f m₂ m₃)} k,v∈m₁m₂₃ v₂v₃∈m₁m₂₃ =
(f v₂ v₃ , (≈-refl , I.union-combines (I.union-preserves-Unique l₁ l₂ u₂) u₃ (I.union-preserves-∈₂ k∉ke₁ v₂∈e₂) v₃∈e₃))
... | (_ , (in (single {v₁} v₁∈e₁) k∉ke₂₃ , v₁∈m₁m₂₃))
rewrite Map-functional {m = union f m₁ (union f m₂ m₃)} k,v∈m₁m₂₃ v₁∈m₁m₂₃ =
let (k∉ke₂ , k∉ke₃) = I.∉-union-∉-either {l₁ = l₂} {l₂ = l₃} k∉ke₂₃
in (v₁ , (≈-refl , I.union-preserves-∈₁ (I.union-preserves-Unique l₁ l₂ u₂) (I.union-preserves-∈₁ u₁ v₁∈e₁ k∉ke₂) k∉ke₃))
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in k∉ke₂ (single {v₃} v₃∈e₃)) , v₁v₃∈m₁m₂₃))
rewrite Map-functional {m = union f m₁ (union f m₂ m₃)} k,v∈m₁m₂₃ v₁v₃∈m₁m₂₃ =
(f v₁ v₃ , (≈-refl , I.union-combines (I.union-preserves-Unique l₁ l₂ u₂) u₃ (I.union-preserves-∈₁ u₁ v₁∈e₁ k∉ke₂) v₃∈e₃))
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in (single {v₂} v₂∈e₂) k∉ke₃) , v₁v₂∈m₁m₂₃))
rewrite Map-functional {m = union f m₁ (union f m₂ m₃)} k,v∈m₁m₂₃ v₁v₂∈m₁m₂₃ =
(f v₁ v₂ , (≈-refl , I.union-preserves-∈₁ (I.union-preserves-Unique l₁ l₂ u₂) (I.union-combines u₁ u₂ v₁∈e₁ v₂∈e₂) k∉ke₃))
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₁v₂v₃∈m₁m₂₃))
rewrite Map-functional {m = union f m₁ (union f m₂ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
(f (f v₁ v₂) v₃ , (≈-sym (f-assoc v₁ v₂ v₃) , I.union-combines (I.union-preserves-Unique l₁ l₂ u₂) u₃ (I.union-combines u₁ u₂ v₁∈e₁ v₂∈e₂) v₃∈e₃))