agda-spa/Lattice/Map.agda
Danila Fedorin 0774946211 Expose decidability from Map modules
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-01 23:27:49 -08:00

907 lines
55 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 Lattice
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
open import Relation.Binary.Definitions using (Decidable)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔_)
module Lattice.Map {a b : Level} (A : Set a) (B : Set b)
(_≈₂_ : B B Set b)
(_⊔₂_ : B B B) (_⊓₂_ : B B B)
(≡-dec-A : Decidable (_≡_ {a} {A}))
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
import Data.List.Membership.Propositional as MemProp
open import Relation.Nullary using (¬_; Dec; yes; no)
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 (⊥; ⊥-elim)
open import Equivalence
open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any; All-x∈xs)
open IsLattice lB using () renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
; ≈-⊔-cong to ≈₂-⊔₂-cong; ≈-⊓-cong to ≈₂-⊓₂-cong
; ⊔-idemp to ⊔₂-idemp; ⊔-comm to ⊔₂-comm; ⊔-assoc to ⊔₂-assoc
; ⊓-idemp to ⊓₂-idemp; ⊓-comm to ⊓₂-comm; ⊓-assoc to ⊓₂-assoc
; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
)
private module ImplKeys where
keys : List (A × B) List A
keys = map proj₁
private module _ where
open MemProp using (_∈_)
open ImplKeys
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 = ⊥-elim (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 = ⊥-elim (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-impl : {k : A} {l : List (A × B)} k keys l Σ B (λ v (k , v) l)
locate-impl {k} {(k' , v) xs} (here k≡k') rewrite k≡k' = (v , here refl)
locate-impl {k} {(k' , v) xs} (there k∈kxs) = let (v , k,v∈xs) = locate-impl k∈kxs in (v , there k,v∈xs)
private module ImplRelation 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 (_∈_)
open ImplKeys
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' = ⊥-elim (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' = ⊥-elim (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-subset-keys : {l₁ l₂ : List (A × B)}
All (λ k k ∈k l₂) (keys l₁)
keys l₂ keys (union l₁ l₂)
union-subset-keys {[]} _ = refl
union-subset-keys {(k , v) l₁'} (k∈kl₂ kl₁'⊆kl₂)
rewrite union-subset-keys kl₁'⊆kl₂ =
insert-keys-∈ k∈kl₂
union-equal-keys : {l₁ l₂ : List (A × B)}
keys l₁ keys l₂ keys l₁ keys (union l₁ l₂)
union-equal-keys {l₁} {l₂} kl₁≡kl₂
with subst (λ l All (λ k k l) (keys l₁)) kl₁≡kl₂ (All-x∈xs (keys l₁))
... | kl₁⊆kl₂ = trans kl₁≡kl₂ (union-subset-keys {l₁} {l₂} kl₁⊆kl₂)
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' = ⊥-elim (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' = ⊥-elim (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₁ = ⊥-elim (k∉l₁l₂ (union-preserves-∈k₁ k∈kl₁))
... | no k∉kl₁ with ∈k-dec k l₂
... | yes k∈kl₂ = ⊥-elim (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 = ⊥-elim (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' = ⊥-elim (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' = ⊥-elim (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' = ⊥-elim (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' = ⊥-elim (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v₁∈xs₁))
... | no k≢k' = k≢k'
update : A B List (A × B) List (A × B)
update k v [] = []
update k v ((k' , v') xs) with ≡-dec-A k k'
... | yes _ = (k' , f v v') xs
... | no _ = (k' , v') update k v xs
updates : List (A × B) List (A × B) List (A × B)
updates l₁ l₂ = foldr update l₂ l₁
restrict : List (A × B) List (A × B) List (A × B)
restrict l [] = []
restrict l ((k' , v') xs) with ∈k-dec k' l
... | yes _ = (k' , v') restrict l xs
... | no _ = restrict l xs
intersect : List (A × B) List (A × B) List (A × B)
intersect l₁ l₂ = restrict l₁ (updates l₁ l₂)
update-keys : {k : A} {v : B} {l : List (A × B)}
keys l keys (update k v l)
update-keys {l = []} = refl
update-keys {k} {v} {l = (k' , v') xs}
with ≡-dec-A k k'
... | yes _ = refl
... | no _ rewrite update-keys {k} {v} {xs} = refl
updates-keys : {l₁ l₂ : List (A × B)}
keys l₂ keys (updates l₁ l₂)
updates-keys {[]} = refl
updates-keys {(k , v) xs} {l₂}
rewrite updates-keys {xs} {l₂}
rewrite update-keys {k} {v} {updates xs l₂} = refl
update-preserves-Unique : {k : A} {v : B} {l : List (A × B)}
Unique (keys l) Unique (keys (update k v l ))
update-preserves-Unique {k} {v} {l} u rewrite update-keys {k} {v} {l} = u
updates-preserve-Unique : {l₁ l₂ : List (A × B)}
Unique (keys l₂) Unique (keys (updates l₁ l₂))
updates-preserve-Unique {[]} u = u
updates-preserve-Unique {(k , v) xs} u = update-preserves-Unique (updates-preserve-Unique {xs} u)
restrict-preserves-k≢ : {k : A} {l₁ l₂ : List (A × B)}
All (λ k' ¬ k k') (keys l₂) All (λ k' ¬ k k') (keys (restrict l₁ l₂))
restrict-preserves-k≢ {k} {l₁} {[]} k≢l₂ = k≢l₂
restrict-preserves-k≢ {k} {l₁} {(k' , v') xs} (k≢k' k≢xs)
with ∈k-dec k' l₁
... | yes _ = k≢k' restrict-preserves-k≢ k≢xs
... | no _ = restrict-preserves-k≢ k≢xs
restrict-preserves-Unique : {l₁ l₂ : List (A × B)}
Unique (keys l₂) Unique (keys (restrict l₁ l₂))
restrict-preserves-Unique {l₁} {[]} _ = empty
restrict-preserves-Unique {l₁} {(k , v) xs} (push k≢xs uxs)
with ∈k-dec k l₁
... | yes _ = push (restrict-preserves-k≢ k≢xs) (restrict-preserves-Unique uxs)
... | no _ = restrict-preserves-Unique uxs
intersect-preserves-Unique : {l₁ l₂ : List (A × B)}
Unique (keys l₂) Unique (keys (intersect l₁ l₂))
intersect-preserves-Unique {l₁} u = restrict-preserves-Unique (updates-preserve-Unique {l₁} u)
updates-preserve-∉₂ : {k : A} {l₁ l₂ : List (A × B)}
¬ k ∈k l₂ ¬ k ∈k updates l₁ l₂
updates-preserve-∉₂ {k} {l₁} {l₂} k∉kl₁ k∈kl₁l₂
rewrite updates-keys {l₁} {l₂} = k∉kl₁ k∈kl₁l₂
restrict-needs-both : {k : A} {l₁ l₂ : List (A × B)}
k ∈k restrict l₁ l₂ (k ∈k l₁ × k ∈k l₂)
restrict-needs-both {k} {l₁} {[]} ()
restrict-needs-both {k} {l₁} {(k' , _) xs} k∈l₁l₂
with ∈k-dec k' l₁ | k∈l₁l₂
... | yes k'∈kl₁ | here k≡k'
rewrite k≡k' =
(k'∈kl₁ , here refl)
... | yes _ | there k∈l₁xs =
let (k∈kl₁ , k∈kxs) = restrict-needs-both k∈l₁xs
in (k∈kl₁ , there k∈kxs)
... | no k'∉kl₁ | k∈l₁xs =
let (k∈kl₁ , k∈kxs) = restrict-needs-both k∈l₁xs
in (k∈kl₁ , there k∈kxs)
restrict-subset-keys : {l₁ l₂ : List (A × B)}
All (λ k k ∈k l₁) (keys l₂)
keys l₂ keys (restrict l₁ l₂)
restrict-subset-keys {l₁} {[]} _ = refl
restrict-subset-keys {l₁} {(k , v) l₂'} (k∈kl₁ kl₂'⊆kl₁)
with ∈k-dec k l₁
... | no k∉kl₁ = ⊥-elim (k∉kl₁ k∈kl₁)
... | yes _ rewrite restrict-subset-keys {l₁} {l₂'} kl₂'⊆kl₁ = refl
restrict-equal-keys : {l₁ l₂ : List (A × B)}
keys l₁ keys l₂
keys l₁ keys (restrict l₁ l₂)
restrict-equal-keys {l₁} {l₂} kl₁≡kl₂
with subst (λ l All (λ k k l) (keys l₂)) (sym kl₁≡kl₂) (All-x∈xs (keys l₂))
... | kl₂⊆kl₁ = trans kl₁≡kl₂ (restrict-subset-keys {l₁} {l₂} kl₂⊆kl₁)
intersect-equal-keys : {l₁ l₂ : List (A × B)}
keys l₁ keys l₂
keys l₁ keys (intersect l₁ l₂)
intersect-equal-keys {l₁} {l₂} kl₁≡kl₂
rewrite restrict-equal-keys (trans kl₁≡kl₂ (updates-keys {l₁} {l₂}))
rewrite updates-keys {l₁} {l₂} = refl
restrict-preserves-∉₁ : {k : A} {l₁ l₂ : List (A × B)}
¬ k ∈k l₁ ¬ k ∈k restrict l₁ l₂
restrict-preserves-∉₁ {k} {l₁} {l₂} k∉kl₁ k∈kl₁l₂ =
let (k∈kl₁ , _) = restrict-needs-both {l₂ = l₂} k∈kl₁l₂ in k∉kl₁ k∈kl₁
restrict-preserves-∉₂ : {k : A} {l₁ l₂ : List (A × B)}
¬ k ∈k l₂ ¬ k ∈k restrict l₁ l₂
restrict-preserves-∉₂ {k} {l₁} {l₂} k∉kl₂ k∈kl₁l₂ =
let (_ , k∈kl₂) = restrict-needs-both {l₂ = l₂} k∈kl₁l₂ in k∉kl₂ k∈kl₂
intersect-preserves-∉₁ : {k : A} {l₁ l₂ : List (A × B)}
¬ k ∈k l₁ ¬ k ∈k intersect l₁ l₂
intersect-preserves-∉₁ {k} {l₁} {l₂} = restrict-preserves-∉₁ {k} {l₁} {updates l₁ l₂}
intersect-preserves-∉₂ : {k : A} {l₁ l₂ : List (A × B)}
¬ k ∈k l₂ ¬ k ∈k intersect l₁ l₂
intersect-preserves-∉₂ {k} {l₁} {l₂} k∉l₂ = restrict-preserves-∉₂ (updates-preserve-∉₂ {l₁ = l₁} k∉l₂ )
restrict-preserves-∈₂ : {k : A} {v : B} {l₁ l₂ : List (A × B)}
k ∈k l₁ (k , v) l₂ (k , v) restrict l₁ l₂
restrict-preserves-∈₂ {k} {v} {l₁} {(k' , v') xs} k∈kl₁ (here k,v≡k',v')
rewrite cong proj₁ k,v≡k',v' rewrite cong proj₂ k,v≡k',v'
with ∈k-dec k' l₁
... | yes _ = here refl
... | no k'∉kl₁ = ⊥-elim (k'∉kl₁ k∈kl₁)
restrict-preserves-∈₂ {l₁ = l₁} {l₂ = (k' , v') xs} k∈kl₁ (there k,v∈xs)
with ∈k-dec k' l₁
... | yes _ = there (restrict-preserves-∈₂ k∈kl₁ k,v∈xs)
... | no _ = restrict-preserves-∈₂ k∈kl₁ k,v∈xs
update-preserves-∈ : {k k' : A} {v v' : B} {l : List (A × B)}
¬ k k' (k , v) l (k , v) update k' v' l
update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') xs} k≢k' (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 k'≡k'' = ⊥-elim (k≢k' (sym k'≡k''))
... | no _ = here refl
update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') xs} k≢k' (there k,v∈xs)
with ≡-dec-A k' k''
... | yes _ = there k,v∈xs
... | no _ = there (update-preserves-∈ k≢k' k,v∈xs)
updates-preserve-∈₂ : {k : A} {v : B} {l₁ l₂ : List (A × B)}
¬ k ∈k l₁ (k , v) l₂ (k , v) updates l₁ l₂
updates-preserve-∈₂ {k} {v} {[]} {l₂} _ k,v∈l₂ = k,v∈l₂
updates-preserve-∈₂ {k} {v} {(k' , v') xs} {l₂} k∉kl₁ k,v∈l₂ =
update-preserves-∈ (λ k≡k' k∉kl₁ (here k≡k')) (updates-preserve-∈₂ (λ k∈kxs k∉kl₁ (there k∈kxs)) k,v∈l₂)
update-combines : {k : A} {v v' : B} {l : List (A × B)}
Unique (keys l) (k , v) l (k , f v' v) update k v' l
update-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' = ⊥-elim (k'≢k' refl)
update-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' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v∈xs))
... | no _ = there (update-combines uxs k,v∈xs)
updates-combine : {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₂) updates l₁ l₂
updates-combine {k} {v₁} {v₂} {(k' , v') xs} {l₂} (push k'≢xs uxs₁) u₂ (here k,v₁≡k',v') k,v₂∈l₂
rewrite cong proj₁ k,v₁≡k',v' rewrite cong proj₂ k,v₁≡k',v' =
update-combines (updates-preserve-Unique {l₁ = xs} u₂) (updates-preserve-∈₂ (All¬-¬Any k'≢xs) k,v₂∈l₂)
updates-combine {k} {v₁} {v₂} {(k' , v') xs} {l₂} (push k'≢xs uxs₁) u₂ (there k,v₁∈xs) k,v₂∈l₂ =
update-preserves-∈ k≢k' (updates-combine uxs₁ u₂ k,v₁∈xs k,v₂∈l₂)
where
k≢k' : ¬ k k'
k≢k' with ≡-dec-A k k'
... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v₁∈xs))
... | no k≢k' = k≢k'
intersect-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₂) intersect l₁ l₂
intersect-combines u₁ u₂ k,v₁∈l₁ k,v₂∈l₂ =
restrict-preserves-∈₂ (∈-cong proj₁ k,v₁∈l₁) (updates-combine u₁ u₂ k,v₁∈l₁ k,v₂∈l₂)
Map : Set (a ⊔ℓ b)
Map = Σ (List (A × B)) (λ l Unique (ImplKeys.keys l))
keys : Map List A
keys (kvs , _) = ImplKeys.keys kvs
_∈_ : (A × B) Map Set (a ⊔ℓ b)
_∈_ p (kvs , _) = MemProp._∈_ p kvs
_∈k_ : A Map Set a
_∈k_ k m = MemProp._∈_ k (keys m)
locate : {k : A} {m : Map} k ∈k m Σ B (λ v (k , v) m)
locate k∈km = locate-impl k∈km
forget : {k : A} {v : B} {m : Map} (k , v) m k ∈k m
forget = ∈-cong proj₁
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
open ImplRelation using () renaming (subset to subset-impl) public
_⊆_ : Map Map Set (a ⊔ℓ b)
_⊆_ (kvs₁ , _) (kvs₂ , _) = subset-impl kvs₁ kvs₂
⊆-refl : (m : Map) m m
⊆-refl _ k v k,v∈m = (v , (≈₂-refl , k,v∈m))
⊆-trans : (m₁ m₂ m₃ : Map) m₁ m₂ m₂ m₃ m₁ m₃
⊆-trans _ _ _ m₁⊆m₂ m₂⊆m₃ k v k,v∈m₁ =
let
(v' , (v≈v' , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
(v'' , (v'≈v'' , k,v''∈m₃)) = m₂⊆m₃ k v' k,v'∈m₂
in (v'' , (≈₂-trans v≈v' v'≈v'' , k,v''∈m₃))
_≈_ : Map Map Set (a ⊔ℓ b)
_≈_ m₁ m₂ = m₁ m₂ × m₂ m₁
≈-equiv : IsEquivalence Map _≈_
≈-equiv = record
{ ≈-refl = λ {m} (⊆-refl m , ⊆-refl m)
; ≈-sym = λ {m₁} {m₂} (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₁ , m₁⊆m₂)
; ≈-trans = λ {m₁} {m₂} {m₃} (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂)
( ⊆-trans m₁ m₂ m₃ m₁⊆m₂ m₂⊆m₃
, ⊆-trans m₃ m₂ m₁ m₃⊆m₂ m₂⊆m₁
)
}
data Expr : Set (a ⊔ℓ b) where
`_ : Map Expr
__ : Expr Expr Expr
_∩_ : Expr Expr Expr
open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys) renaming (insert to insert-impl; union to union-impl)
open ImplInsert _⊓₂_ using (intersect-preserves-Unique; intersect-equal-keys) renaming (intersect to intersect-impl)
_⊔_ : Map Map Map
_⊔_ (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
_⊓_ : Map Map Map
_⊓_ (kvs₁ , _) (kvs₂ , uks₂) = (intersect-impl kvs₁ kvs₂ , intersect-preserves-Unique {kvs₁} {kvs₂} uks₂)
open ImplInsert _⊔₂_ using
( union-combines
; union-preserves-∈₁
; union-preserves-∈₂
; union-preserves-∉
)
⊔-combines : {k : A} {v₁ v₂ : B} {m₁ m₂ : Map} (k , v₁) m₁ (k , v₂) m₂ (k , v₁ ⊔₂ v₂) (m₁ m₂)
⊔-combines {k} {v₁} {v₂} {kvs₁ , u₁} {kvs₂ , u₂} k,v₁∈m₁ k,v₂∈m₂ = union-combines u₁ u₂ k,v₁∈m₁ k,v₂∈m₂
open ImplInsert _⊓₂_ using
( restrict-needs-both
; updates
; intersect-preserves-∉₁
; intersect-preserves-∉₂
; intersect-combines
)
⟦_⟧ : Expr -> Map
` m = m
e₁ e₂ = e₁ e₂
e₁ e₂ = 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 (v₁ ⊔₂ v₂) (e₁ e₂)
bothⁱ : {v₁ v₂ : B} {e₁ e₂ : Expr} Provenance k v₁ e₁ Provenance k v₂ e₂ Provenance k (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-impl 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 (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₂ = ⊥-elim (union-preserves-∉ k∉ke₁ k∉ke₂ k∈ke₁e₂)
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 (v₁ ⊓₂ v₂ , (bothⁱ g₁ g₂ , intersect-combines (proj₂ e₁ ) (proj₂ e₂ ) k,v₁∈e₁ k,v₂∈e₂))
... | yes k∈ke₁ | no k∉ke₂ = ⊥-elim (intersect-preserves-∉₂ {l₁ = proj₁ e₁ } k∉ke₂ k∈ke₁e₂)
... | no k∉ke₁ | yes k∈ke₂ = ⊥-elim (intersect-preserves-∉₁ {l₂ = proj₁ e₂ } k∉ke₁ k∈ke₁e₂)
... | no k∉ke₁ | no k∉ke₂ = ⊥-elim (intersect-preserves-∉₂ {l₁ = proj₁ e₁ } k∉ke₂ k∈ke₁e₂)
module _ (≈₂-dec : IsDecidable _≈₂_) where
private module _ where
data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
extra : (k : A) k ∈k m₁ ¬ k ∈k m₂ SubsetInfo m₁ m₂
mismatch : (k : A) (v₁ v₂ : B) (k , v₁) m₁ (k , v₂) m₂ ¬ v₁ ≈₂ v₂ SubsetInfo m₁ m₂
fine : m₁ m₂ SubsetInfo m₁ m₂
SubsetInfo-to-dec : {m₁ m₂ : Map} SubsetInfo m₁ m₂ Dec (m₁ m₂)
SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) =
let (v , k,v∈m₁) = locate-impl k∈km₁
in no (λ m₁⊆m₂
let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
in k∉km₂ (∈-cong proj₁ k,v'∈m₂))
SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) =
no (λ m₁⊆m₂
let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁
in v₁̷≈v₂ (subst (λ v'' v₁ ≈₂ v'') (Map-functional {k} {v'} {v₂} {m₂} k,v'∈m₂ k,v₂∈m₂) v₁≈v')) -- for some reason, can't just use subst...
SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂
compute-SubsetInfo : m₁ m₂ SubsetInfo m₁ m₂
compute-SubsetInfo ([] , _) m₂ = fine (λ k v ())
compute-SubsetInfo m₁@((k , v) xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂)
with compute-SubsetInfo (xs₁ , uxs₁) m₂
... | extra k' k'∈kxs₁ k'∉km₂ = extra k' (there k'∈kxs₁) k'∉km₂
... | mismatch k' v₁ v₂ k',v₁∈xs₁ k',v₂∈m₂ v₁̷≈v₂ =
mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂
... | fine xs₁⊆m₂ with ∈k-dec k l₂
... | no k∉km₂ = extra k (here refl) k∉km₂
... | yes k∈km₂ with locate-impl k∈km₂
... | (v' , k,v'∈m₂) with ≈₂-dec v v'
... | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v'
... | yes v≈v' = fine m₁⊆m₂
where
m₁⊆m₂ : m₁ m₂
m₁⊆m₂ k' v'' (here k,v≡k',v'')
rewrite cong proj₁ k,v≡k',v''
rewrite cong proj₂ k,v≡k',v'' =
(v' , (v≈v' , k,v'∈m₂))
m₁⊆m₂ k' v'' (there k,v≡k',v'') =
xs₁⊆m₂ k' v'' k,v≡k',v''
⊆-dec : m₁ m₂ Dec (m₁ m₂)
⊆-dec m₁ m₂ = SubsetInfo-to-dec (compute-SubsetInfo m₁ m₂)
≈-dec : m₁ m₂ Dec (m₁ m₂)
≈-dec m₁ m₂
with ⊆-dec m₁ m₂ | ⊆-dec m₂ m₁
... | yes m₁⊆m₂ | yes m₂⊆m₁ = yes (m₁⊆m₂ , m₂⊆m₁)
... | _ | no m₂̷⊆m₁ = no (λ (_ , m₂⊆m₁) m₂̷⊆m₁ m₂⊆m₁)
... | no m₁̷⊆m₂ | _ = no (λ (m₁⊆m₂ , _) m₁̷⊆m₂ m₁⊆m₂)
private module I = ImplInsert _⊔₂_
private module I = ImplInsert _⊓₂_
≈-⊔-cong : {m₁ m₂ m₃ m₄ : Map} m₁ m₂ m₃ m₄ (m₁ m₃) (m₂ m₄)
≈-⊔-cong {m₁} {m₂} {m₃} {m₄} (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃) =
( ⊔-⊆ m₁ m₂ m₃ m₄ (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃)
, ⊔-⊆ m₂ m₁ m₄ m₃ (m₂⊆m₁ , m₁⊆m₂) (m₄⊆m₃ , m₃⊆m₄)
)
where
≈-∉-cong : {m₁ m₂ : Map} {k : A} m₁ m₂ ¬ k ∈k m₁ ¬ k ∈k m₂
≈-∉-cong (m₁⊆m₂ , m₂⊆m₁) k∉km₁ k∈km₂ =
let (v₂ , k,v₂∈m₂) = locate-impl k∈km₂
(_ , (_ , k,v₁∈m₁)) = m₂⊆m₁ _ v₂ k,v₂∈m₂
in k∉km₁ (∈-cong proj₁ k,v₁∈m₁)
⊔-⊆ : (m₁ m₂ m₃ m₄ : Map) m₁ m₂ m₃ m₄ (m₁ m₃) (m₂ m₄)
⊔-⊆ m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
with Expr-Provenance k ((` m₁) (` m₃)) (∈-cong proj₁ k,v∈m₁m₃)
... | (_ , (bothᵘ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) , v₁v₃∈m₁m₃))
rewrite Map-functional {m = m₁ m₃} k,v∈m₁m₃ v₁v₃∈m₁m₃ =
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
(v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
in (v₂ ⊔₂ v₄ , (≈₂-⊔₂-cong v₁≈v₂ v₃≈v₄ , I⊔.union-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
... | (_ , (in (single {v₁} v₁∈m₁) k∉km₃ , v₁∈m₁m₃))
rewrite Map-functional {m = m₁ m₃} k,v∈m₁m₃ v₁∈m₁m₃ =
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
k∉km₄ = ≈-∉-cong {m₃} {m₄} m₃≈m₄ k∉km₃
in (v₂ , (v₁≈v₂ , I⊔.union-preserves-∈₁ (proj₂ m₂) k,v₂∈m₂ k∉km₄))
... | (_ , (in k∉km₁ (single {v₃} v₃∈m₃) , v₃∈m₁m₃))
rewrite Map-functional {m = m₁ m₃} k,v∈m₁m₃ v₃∈m₁m₃ =
let (v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
k∉km₂ = ≈-∉-cong {m₁} {m₂} m₁≈m₂ k∉km₁
in (v₄ , (v₃≈v₄ , I⊔.union-preserves-∈₂ k∉km₂ k,v₄∈m₄))
≈-⊓-cong : {m₁ m₂ m₃ m₄ : Map} m₁ m₂ m₃ m₄ (m₁ m₃) (m₂ m₄)
≈-⊓-cong {m₁} {m₂} {m₃} {m₄} (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃) =
( ⊓-⊆ m₁ m₂ m₃ m₄ (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃)
, ⊓-⊆ m₂ m₁ m₄ m₃ (m₂⊆m₁ , m₁⊆m₂) (m₄⊆m₃ , m₃⊆m₄)
)
where
⊓-⊆ : (m₁ m₂ m₃ m₄ : Map) m₁ m₂ m₃ m₄ (m₁ m₃) (m₂ m₄)
⊓-⊆ m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
with Expr-Provenance k ((` m₁) (` m₃)) (∈-cong proj₁ k,v∈m₁m₃)
... | (_ , (bothⁱ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) , v₁v₃∈m₁m₃))
rewrite Map-functional {m = m₁ m₃} k,v∈m₁m₃ v₁v₃∈m₁m₃ =
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
(v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
in (v₂ ⊓₂ v₄ , (≈₂-⊓₂-cong v₁≈v₂ v₃≈v₄ , I⊓.intersect-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
⊔-idemp : (m : Map) (m m) m
⊔-idemp m@(l , u) = (mm-m-⊆ , m-mm-⊆)
where
mm-m-⊆ : (m m) m
mm-m-⊆ k v k,v∈mm
with Expr-Provenance 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 = m m} k,v∈mm v'v''∈mm =
(v'' , (⊔₂-idemp v'' , v''∈m))
... | (_ , (in (single {v'} v'∈m) k∉km , _)) = ⊥-elim (k∉km (∈-cong proj₁ v'∈m))
... | (_ , (in k∉km (single {v''} v''∈m) , _)) = ⊥-elim (k∉km (∈-cong proj₁ v''∈m))
m-mm-⊆ : m (m m)
m-mm-⊆ k v k,v∈m = (v ⊔₂ v , (≈₂-sym (⊔₂-idemp v) , I⊔.union-combines u u k,v∈m k,v∈m))
⊔-comm : (m₁ m₂ : Map) (m₁ m₂) (m₂ m₁)
⊔-comm m₁ m₂ = (⊔-comm-⊆ m₁ m₂ , ⊔-comm-⊆ m₂ m₁)
where
⊔-comm-⊆ : (m₁ m₂ : Map) (m₁ m₂) (m₂ m₁)
⊔-comm-⊆ m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
with Expr-Provenance 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 = m₁ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
(v₂ ⊔₂ v₁ , (⊔₂-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 = 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 = m₁ m₂} k,v∈m₁m₂ v₂∈m₁m₂ =
(v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ u₂ v₂∈m₂ k∉km₁))
⊔-assoc : (m₁ m₂ m₃ : Map) ((m₁ m₂) m₃) (m₁ (m₂ m₃))
⊔-assoc m₁@(l₁ , u₁) m₂@(l₂ , u₂) m₃@(l₃ , u₃) = (⊔-assoc₁ , ⊔-assoc₂)
where
⊔-assoc₁ : ((m₁ m₂) m₃) (m₁ (m₂ m₃))
⊔-assoc₁ k v k,v∈m₁₂m₃
with Expr-Provenance k (((` m₁) (` m₂)) (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
... | (_ , (in k∉ke₁₂ (single {v₃} v₃∈e₃) , v₃∈m₁₂m₃))
rewrite Map-functional {m = (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 = (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 = (m₁ m₂) m₃} k,v∈m₁₂m₃ v₂v₃∈m₁₂m₃ =
(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 = (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 = (m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₃∈m₁₂m₃ =
(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 = (m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂∈m₁₂m₃ =
(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 = (m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
(v₁ ⊔₂ (v₂ ⊔₂ v₃) , (⊔₂-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₃)))
⊔-assoc₂ : (m₁ (m₂ m₃)) ((m₁ m₂) m₃)
⊔-assoc₂ k v k,v∈m₁m₂₃
with Expr-Provenance 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 = m₁ (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 = m₁ (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 = m₁ (m₂ m₃)} k,v∈m₁m₂₃ v₂v₃∈m₁m₂₃ =
(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 = 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-∈₁ (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 = m₁ (m₂ m₃)} k,v∈m₁m₂₃ v₁v₃∈m₁m₂₃ =
(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 = m₁ (m₂ m₃)} k,v∈m₁m₂₃ v₁v₂∈m₁m₂₃ =
(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 = m₁ (m₂ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
((v₁ ⊔₂ v₂) ⊔₂ v₃ , (≈₂-sym (⊔₂-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₃))
⊓-idemp : (m : Map) (m m) m
⊓-idemp m@(l , u) = (mm-m-⊆ , m-mm-⊆)
where
mm-m-⊆ : (m m) m
mm-m-⊆ k v k,v∈mm
with Expr-Provenance 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 = m m} k,v∈mm v'v''∈mm =
(v'' , (⊓₂-idemp v'' , v''∈m))
m-mm-⊆ : m (m m)
m-mm-⊆ k v k,v∈m = (v ⊓₂ v , (≈₂-sym (⊓₂-idemp v) , I⊓.intersect-combines u u k,v∈m k,v∈m))
⊓-comm : (m₁ m₂ : Map) (m₁ m₂) (m₂ m₁)
⊓-comm m₁ m₂ = (⊓-comm-⊆ m₁ m₂ , ⊓-comm-⊆ m₂ m₁)
where
⊓-comm-⊆ : (m₁ m₂ : Map) (m₁ m₂) (m₂ m₁)
⊓-comm-⊆ m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
with Expr-Provenance 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 = m₁ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
(v₂ ⊓₂ v₁ , (⊓₂-comm v₁ v₂ , I⊓.intersect-combines u₂ u₁ v₂∈m₂ v₁∈m₁))
⊓-assoc : (m₁ m₂ m₃ : Map) ((m₁ m₂) m₃) (m₁ (m₂ m₃))
⊓-assoc m₁@(l₁ , u₁) m₂@(l₂ , u₂) m₃@(l₃ , u₃) = (⊓-assoc₁ , ⊓-assoc₂)
where
⊓-assoc₁ : ((m₁ m₂) m₃) (m₁ (m₂ m₃))
⊓-assoc₁ k v k,v∈m₁₂m₃
with Expr-Provenance k (((` m₁) (` m₂)) (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
... | (_ , (bothⁱ (bothⁱ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
rewrite Map-functional {m = (m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
(v₁ ⊓₂ (v₂ ⊓₂ v₃) , (⊓₂-assoc v₁ v₂ v₃ , I⊓.intersect-combines u₁ (I⊓.intersect-preserves-Unique {l₂} {l₃} u₃) v₁∈e₁ (I⊓.intersect-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
⊓-assoc₂ : (m₁ (m₂ m₃)) ((m₁ m₂) m₃)
⊓-assoc₂ k v k,v∈m₁m₂₃
with Expr-Provenance k ((` m₁) ((` m₂) (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃)
... | (_ , (bothⁱ (single {v₁} v₁∈e₁) (bothⁱ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₁v₂v₃∈m₁m₂₃))
rewrite Map-functional {m = m₁ (m₂ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
((v₁ ⊓₂ v₂) ⊓₂ v₃ , (≈₂-sym (⊓₂-assoc v₁ v₂ v₃) , I⊓.intersect-combines (I⊓.intersect-preserves-Unique {l₁} {l₂} u₂) u₃ (I⊓.intersect-combines u₁ u₂ v₁∈e₁ v₂∈e₂) v₃∈e₃))
absorb-⊓-⊔ : (m₁ m₂ : Map) (m₁ (m₁ m₂)) m₁
absorb-⊓-⊔ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊓-⊔¹ , absorb-⊓-⊔²)
where
absorb-⊓-⊔¹ : (m₁ (m₁ m₂)) m₁
absorb-⊓-⊔¹ k v k,v∈m₁m₁₂
with Expr-Provenance k ((` m₁) ((` m₁) (` m₂))) (∈-cong proj₁ k,v∈m₁m₁₂)
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
(bothᵘ (single {v₁'} k,v₁'∈m₁)
(single {v₂} v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
rewrite Map-functional {m = m₁ (m₁ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
(v₁' , (absorb-⊓₂-⊔₂ v₁' v₂ , k,v₁'∈m₁))
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
(in (single {v₁'} k,v₁'∈m₁) _) , v₁v₁'∈m₁m₁₂))
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
rewrite Map-functional {m = m₁ (m₁ m₂)} k,v∈m₁m₁₂ v₁v₁'∈m₁m₁₂ =
(v₁' , (⊓₂-idemp v₁' , k,v₁'∈m₁))
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
(in k∉m₁ _ ) , _)) = ⊥-elim (k∉m₁ (∈-cong proj₁ k,v₁∈m₁))
absorb-⊓-⊔² : m₁ (m₁ (m₁ m₂))
absorb-⊓-⊔² k v k,v∈m₁
with ∈k-dec k l₂
... | yes k∈km₂ =
let (v₂ , k,v₂∈m₂) = locate-impl k∈km₂
in (v ⊓₂ (v ⊔₂ v₂) , (≈₂-sym (absorb-⊓₂-⊔₂ v v₂) , I⊓.intersect-combines u₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) k,v∈m₁ (I⊔.union-combines u₁ u₂ k,v∈m₁ k,v₂∈m₂)))
... | no k∉km₂ = (v ⊓₂ v , (≈₂-sym (⊓₂-idemp v) , I⊓.intersect-combines u₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) k,v∈m₁ (I⊔.union-preserves-∈₁ u₁ k,v∈m₁ k∉km₂)))
absorb-⊔-⊓ : (m₁ m₂ : Map) (m₁ (m₁ m₂)) m₁
absorb-⊔-⊓ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊔-⊓¹ , absorb-⊔-⊓²)
where
absorb-⊔-⊓¹ : (m₁ (m₁ m₂)) m₁
absorb-⊔-⊓¹ k v k,v∈m₁m₁₂
with Expr-Provenance k ((` m₁) ((` m₁) (` m₂))) (∈-cong proj₁ k,v∈m₁m₁₂)
... | (_ , (bothᵘ (single {v₁} k,v₁∈m₁)
(bothⁱ (single {v₁'} k,v₁'∈m₁)
(single {v₂} k,v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
rewrite Map-functional {m = m₁ (m₁ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
(v₁' , (absorb-⊔₂-⊓₂ v₁' v₂ , k,v₁'∈m₁))
... | (_ , (in (single {v₁} k,v₁∈m₁) k∉km₁₂ , k,v₁∈m₁m₁₂))
rewrite Map-functional {m = m₁ (m₁ m₂)} k,v∈m₁m₁₂ k,v₁∈m₁m₁₂ =
(v₁ , (≈₂-refl , k,v₁∈m₁))
... | (_ , (in k∉km₁ (bothⁱ (single {v₁'} k,v₁'∈m₁)
(single {v₂} k,v₂∈m₂)) , _)) =
⊥-elim (k∉km₁ (∈-cong proj₁ k,v₁'∈m₁))
absorb-⊔-⊓² : m₁ (m₁ (m₁ m₂))
absorb-⊔-⊓² k v k,v∈m₁
with ∈k-dec k l₂
... | yes k∈km₂ =
let (v₂ , k,v₂∈m₂) = locate-impl k∈km₂
in (v ⊔₂ (v ⊓₂ v₂) , (≈₂-sym (absorb-⊔₂-⊓₂ v v₂) , I⊔.union-combines u₁ (I⊓.intersect-preserves-Unique {l₁} {l₂} u₂) k,v∈m₁ (I⊓.intersect-combines u₁ u₂ k,v∈m₁ k,v₂∈m₂)))
... | no k∉km₂ = (v , (≈₂-refl , I⊔.union-preserves-∈₁ u₁ k,v∈m₁ (I⊓.intersect-preserves-∉₂ {k} {l₁} {l₂} k∉km₂)))
isUnionSemilattice : IsSemilattice Map _≈_ _⊔_
isUnionSemilattice = record
{ ≈-equiv = ≈-equiv
; ≈-⊔-cong = λ {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄ ≈-⊔-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
; ⊔-assoc = ⊔-assoc
; ⊔-comm = ⊔-comm
; ⊔-idemp = ⊔-idemp
}
isIntersectSemilattice : IsSemilattice Map _≈_ _⊓_
isIntersectSemilattice = record
{ ≈-equiv = ≈-equiv
; ≈-⊔-cong = λ {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄ ≈-⊓-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
; ⊔-assoc = ⊓-assoc
; ⊔-comm = ⊓-comm
; ⊔-idemp = ⊓-idemp
}
isLattice : IsLattice Map _≈_ _⊔_ _⊓_
isLattice = record
{ joinSemilattice = isUnionSemilattice
; meetSemilattice = isIntersectSemilattice
; absorb-⊔-⊓ = absorb-⊔-⊓
; absorb-⊓-⊔ = absorb-⊓-⊔
}
lattice : Lattice Map
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
⊔-equal-keys : {m₁ m₂ : Map} keys m₁ keys m₂ keys m₁ keys (m₁ m₂)
⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂
⊓-equal-keys : {m₁ m₂ : Map} keys m₁ keys m₂ keys m₁ keys (m₁ m₂)
⊓-equal-keys km₁≡km₂ = intersect-equal-keys km₁≡km₂