agda-spa/Lattice/Map.agda
Danila Fedorin 3305de4710 Remove need for explicit arguments in map derivatives
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-10 18:35:29 -07:00

1122 lines
66 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
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
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; 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-⊓₂-⊔₂
; _≼_ to _≼₂_
)
private module ImplKeys where
keys : List (A × B) List A
keys = map proj₁
-- See note on `forget` for why this is defined in global scope even though
-- it operates on lists.
∈k-dec : (k : A) (l : List (A × B)) Dec (k ∈ˡ (ImplKeys.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 ∈ˡ (ImplKeys.keys ((k' , v) xs))
witness (here k≡k') = k≢k' k≡k'
witness (there k∈kxs) = k∉kxs k∈kxs
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) Dec (k l)
k∈-dec k [] = no (λ ())
k∈-dec k (x xs)
with (≡-dec-A k x)
... | yes refl = yes (here refl)
... | no k≢x with (k∈-dec k xs)
... | yes k∈xs = yes (there k∈xs)
... | no k∉xs = no (λ { (here k≡x) k≢x k≡x; (there k∈xs) k∉xs k∈xs })
∈-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₁} {[]} _ = Utils.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))
empty : Map
empty = ([] , Utils.empty)
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` and `∈k-dec` are defined this way because ∈ for maps uses
-- projection, so the full map can't be guessed. On the other hand, list can
-- be guessed.
forget : {k : A} {v : B} {l : List (A × B)} (k , v) ∈ˡ l k ∈ˡ (ImplKeys.keys l)
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; insert-preserves-Unique) renaming (insert to insert-impl; union to union-impl)
open ImplInsert _⊓₂_ using (intersect-preserves-Unique; intersect-equal-keys) renaming (intersect to intersect-impl)
insert : A B Map Map
insert k v (l , uks) = (insert-impl k v l , insert-preserves-Unique uks)
_⊔_ : 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-∉
; union-preserves-∈k₁
; union-preserves-∈k₂
)
⊔-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₂
⊔-preserves-∈k₁ : {k : A} {m₁ m₂ : Map} k ∈k m₁ k ∈k (m₁ m₂)
⊔-preserves-∈k₁ {k} {(l₁ , _)} {(l₂ , _)} k∈km₁ = union-preserves-∈k₁ {l₁ = l₁} {l₂ = l₂} k∈km₁
⊔-preserves-∈k₂ : {k : A} {m₁ m₂ : Map} k ∈k m₂ k ∈k (m₁ m₂)
⊔-preserves-∈k₂ {k} {(l₁ , _)} {(l₂ , _)} k∈km₁ = union-preserves-∈k₂ {l₁ = l₁} {l₂ = l₂} k∈km₁
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₂)
Expr-Provenance-≡ : {k : A} {v : B} (e : Expr) (k , v) e Provenance k v e
Expr-Provenance-≡ {k} {v} e k,v∈e
with (v' , (p , k,v'∈e)) Expr-Provenance k e (forget k,v∈e)
rewrite Map-functional {m = e } k,v∈e k,v'∈e = p
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₂ (forget 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-≡ ((` m₁) (` m₃)) k,v∈m₁m₃
... | bothᵘ (single {v₁} v₁∈m₁) (single {v₃} v₃∈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₃ =
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₃) =
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-≡ ((` m₁) (` m₃)) k,v∈m₁m₃
... | bothⁱ (single {v₁} v₁∈m₁) (single {v₃} v₃∈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-≡ ((` m) (` m)) k,v∈mm
... | bothᵘ (single {v'} v'∈m) (single {v''} v''∈m)
rewrite Map-functional {m = m} v'∈m v''∈m =
(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-≡ ((` m₁) (` m₂)) k,v∈m₁m₂
... | bothᵘ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) =
(v₂ ⊔₂ v₁ , (⊔₂-comm v₁ v₂ , I⊔.union-combines u₂ u₁ v₂∈m₂ v₁∈m₁))
... | in {v₁} (single v₁∈m₁) k∉km₂ =
(v₁ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉km₂ v₁∈m₁))
... | in {v₂} k∉km₁ (single v₂∈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-≡ (((` m₁) (` m₂)) (` m₃)) k,v∈m₁₂m₃
... | in k∉ke₁₂ (single {v₃} v₃∈e₃) =
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₂ , (≈₂-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₃ , (≈₂-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₁ , (≈₂-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₃ , (≈₂-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₂ , (≈₂-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₃) , (⊔₂-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-≡ ((` m₁) ((` m₂) (` m₃))) k,v∈m₁m₂₃
... | in k∉ke₁ (in k∉ke₂ (single {v₃} v₃∈e₃)) =
(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₂ , (≈₂-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₃ , (≈₂-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₂₃ =
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₃ , (≈₂-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₂ , (≈₂-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₃ , (≈₂-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-≡ ((` m) (` m)) k,v∈mm
... | bothⁱ (single {v'} v'∈m) (single {v''} v''∈m)
rewrite Map-functional {m = m} v'∈m v''∈m =
(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-≡ ((` m₁) (` m₂)) k,v∈m₁m₂
... | bothⁱ {v₁} {v₂} (single v₁∈m₁) (single v₂∈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-≡ (((` m₁) (` m₂)) (` m₃)) k,v∈m₁₂m₃
... | bothⁱ (bothⁱ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
(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-≡ ((` m₁) ((` m₂) (` m₃))) k,v∈m₁m₂₃
... | bothⁱ (single {v₁} v₁∈e₁) (bothⁱ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
((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-≡ ((` m₁) ((` m₁) (` m₂))) k,v∈m₁m₁₂
... | bothⁱ (single {v₁} k,v₁∈m₁)
(bothᵘ (single {v₁'} k,v₁'∈m₁)
(single {v₂} v₂∈m₂))
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
(v₁' , (absorb-⊓₂-⊔₂ v₁' v₂ , k,v₁'∈m₁))
... | bothⁱ (single {v₁} k,v₁∈m₁)
(in (single {v₁'} k,v₁'∈m₁) _)
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈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-≡ ((` m₁) ((` m₁) (` m₂))) k,v∈m₁m₁₂
... | bothᵘ (single {v₁} k,v₁∈m₁)
(bothⁱ (single {v₁'} k,v₁'∈m₁)
(single {v₂} k,v₂∈m₂))
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
(v₁' , (absorb-⊔₂-⊓₂ v₁' v₂ , k,v₁'∈m₁))
... | in (single {v₁} k,v₁∈m₁) k∉km₁₂ =
(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-⊓-⊔
}
open IsLattice isLattice using (_≼_) public
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₂
private module _ where
open MemProp using (_∈_)
transform : List (A × B) List A (A B) List (A × B)
transform [] _ _ = []
transform ((k , v) xs) ks f
with k∈-dec k ks
... | yes _ = (k , f k) transform xs ks f
... | no _ = (k , v) transform xs ks f
transform-keys-≡ : (l : List (A × B)) (ks : List A) (f : A B)
ImplKeys.keys l ImplKeys.keys (transform l ks f)
transform-keys-≡ [] ks f = refl
transform-keys-≡ ((k , v) xs) ks f
with k∈-dec k ks
... | yes _ rewrite transform-keys-≡ xs ks f = refl
... | no _ rewrite transform-keys-≡ xs ks f = refl
transform-∉k-forward : {l : List (A × B)} (ks : List A) (f : A B) {k : A}
¬ k ∈ˡ ImplKeys.keys l ¬ k ∈ˡ ImplKeys.keys (transform l ks f)
transform-∉k-forward {l} ks f k∉kl rewrite transform-keys-≡ l ks f = k∉kl
transform-∈k-forward : {l : List (A × B)} (ks : List A) (f : A B) {k : A}
k ∈ˡ ImplKeys.keys l k ∈ˡ ImplKeys.keys (transform l ks f)
transform-∈k-forward {l} ks f k∈kl rewrite transform-keys-≡ l ks f = k∈kl
transform-∈k-backward : {l : List (A × B)} (ks : List A) (f : A B) {k : A}
k ∈ˡ ImplKeys.keys (transform l ks f) k ∈ˡ ImplKeys.keys l
transform-∈k-backward {l} ks f k∈kt rewrite transform-keys-≡ l ks f = k∈kt
transform-k∈ks : (l : List (A × B)) {ks : List A} (f : A B) {k : A}
k ∈ˡ ks k ∈ˡ ImplKeys.keys (transform l ks f) (k , f k) ∈ˡ transform l ks f
transform-k∈ks [] _ _ ()
transform-k∈ks ((k' , v) xs) {ks} f {k} k∈ks k∈kl
with k∈-dec k' ks | k∈kl
... | yes _ | here refl = here refl
... | no k∉ks | here refl = ⊥-elim (k∉ks k∈ks)
... | yes _ | there k∈kxs = there (transform-k∈ks xs f k∈ks k∈kxs)
... | no _ | there k∈kxs = there (transform-k∈ks xs f k∈ks k∈kxs)
transform-k∉ks-forward : {l : List (A × B)} {ks : List A} (f : A B) {k : A} {v : B}
¬ k ∈ˡ ks (k , v) ∈ˡ l (k , v) ∈ˡ transform l ks f
transform-k∉ks-forward {[]} _ _ ()
transform-k∉ks-forward {(k' , v') xs} {ks} f {k} {v} k∉ks k,v∈l
with k∈-dec k' ks | k,v∈l
... | yes k∈ks | here refl = ⊥-elim (k∉ks k∈ks)
... | no k∉ks | here refl = here refl
... | yes _ | there k,v∈xs = there (transform-k∉ks-forward f k∉ks k,v∈xs)
... | no _ | there k,v∈xs = there (transform-k∉ks-forward f k∉ks k,v∈xs)
transform-k∉ks-backward : {l : List (A × B)} {ks : List A} (f : A B) {k : A} {v : B}
¬ k ∈ˡ ks (k , v) ∈ˡ transform l ks f (k , v) ∈ˡ l
transform-k∉ks-backward {[]} _ _ ()
transform-k∉ks-backward {(k' , v') xs} {ks} f {k} {v} k∉ks k,v∈tl
with k∈-dec k' ks | k,v∈tl
... | yes k∈ks | here refl = ⊥-elim (k∉ks k∈ks)
... | no k∉ks | here refl = here refl
... | yes _ | there k,v∈txs = there (transform-k∉ks-backward f k∉ks k,v∈txs)
... | no _ | there k,v∈txs = there (transform-k∉ks-backward f k∉ks k,v∈txs)
_updating_via_ : Map List A (A B) Map
_updating_via_ (kvs , uks) ks f =
( transform kvs ks f
, subst Unique (transform-keys-≡ kvs ks f) uks
)
updating-via-keys-≡ : (m : Map) (ks : List A) (f : A B)
keys m keys (m updating ks via f)
updating-via-keys-≡ (l , _) = transform-keys-≡ l
updating-via-∉k-forward : (m : Map) (ks : List A) (f : A B) {k : A}
¬ k ∈k m ¬ k ∈k (m updating ks via f)
updating-via-∉k-forward m = transform-∉k-forward
updating-via-∈k-forward : (m : Map) (ks : List A) (f : A B) {k : A}
k ∈k m k ∈k (m updating ks via f)
updating-via-∈k-forward m = transform-∈k-forward
updating-via-∈k-backward : (m : Map) (ks : List A) (f : A B) {k : A}
k ∈k (m updating ks via f) k ∈k m
updating-via-∈k-backward m = transform-∈k-backward
updating-via-k∈ks : (m : Map) {ks : List A} (f : A B) {k : A}
k ∈ˡ ks k ∈k (m updating ks via f) (k , f k) (m updating ks via f)
updating-via-k∈ks m = transform-k∈ks (proj₁ m)
updating-via-k∈ks-forward : (m : Map) {ks : List A} (f : A B) {k : A}
k ∈ˡ ks k ∈k m (k , f k) (m updating ks via f)
updating-via-k∈ks-forward m {ks} f k∈ks k∈km rewrite transform-keys-≡ (proj₁ m) ks f = transform-k∈ks (proj₁ m) f k∈ks k∈km
updating-via-k∈ks-≡ : (m : Map) {ks : List A} (f : A B) {k : A} {v : B}
k ∈ˡ ks (k , v) (m updating ks via f) v f k
updating-via-k∈ks-≡ m {ks} f k∈ks k,v∈um
with updating-via-k∈ks m f k∈ks (forget k,v∈um)
... | k,fk∈um = Map-functional {m = (m updating ks via f)} k,v∈um k,fk∈um
updating-via-k∉ks-forward : (m : Map) {ks : List A} (f : A B) {k : A} {v : B}
¬ k ∈ˡ ks (k , v) m (k , v) (m updating ks via f)
updating-via-k∉ks-forward m = transform-k∉ks-forward
updating-via-k∉ks-backward : (m : Map) {ks : List A} (f : A B) {k : A} {v : B}
¬ k ∈ˡ ks (k , v) (m updating ks via f) (k , v) m
updating-via-k∉ks-backward m = transform-k∉ks-backward
module _ {l} {L : Set l}
{_≈ˡ_ : L L Set l} {_⊔ˡ_ : L L L} {_⊓ˡ_ : L L L}
(lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
module _ (f : L Map) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)
(g : A L B) (g-Monotonicʳ : k Monotonic _≼ˡ_ _≼₂_ (g k))
(ks : List A) where
updater : L A B
updater l k = g k l
f' : L Map
f' l = (f l) updating ks via (updater l)
f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
f'-Monotonic {l₁} {l₂} l₁≼l₂ = (f'l₁f'l₂⊆f'l₂ , f'l₂⊆f'l₁f'l₂)
where
fl₁fl₂⊆fl₂ = proj₁ (f-Monotonic l₁≼l₂)
fl₂⊆fl₁fl₂ = proj₂ (f-Monotonic l₁≼l₂)
f'l₁f'l₂⊆f'l₂ : ((f' l₁) (f' l₂)) f' l₂
f'l₁f'l₂⊆f'l₂ k v k,v∈f'l₁f'l₂
with Expr-Provenance-≡ ((` (f' l₁)) (` (f' l₂))) k,v∈f'l₁f'l₂
... | in (single k,v∈f'l₁) k∉kf'l₂ =
let
k∈kfl₁ = updating-via-∈k-backward (f l₁) ks (updater l₁) (forget k,v∈f'l₁)
k∈kfl₁fl₂ = union-preserves-∈k₁ {l₁ = proj₁ (f l₁)} {l₂ = proj₁ (f l₂)} k∈kfl₁
(v' , k,v'∈fl₁l₂) = locate {m = (f l₁ f l₂)} k∈kfl₁fl₂
(v'' , (v'≈v'' , k,v''∈fl₂)) = fl₁fl₂⊆fl₂ k v' k,v'∈fl₁l₂
k∈kf'l₂ = updating-via-∈k-forward (f l₂) ks (updater l₂) (forget k,v''∈fl₂)
in
⊥-elim (k∉kf'l₂ k∈kf'l₂)
... | in k∉kf'l₁ (single k,v'∈f'l₂) =
(v , (IsLattice.≈-refl lB , k,v'∈f'l₂))
... | bothᵘ (single {v₁} k,v₁∈f'l₁) (single {v₂} k,v₂∈f'l₂)
with k∈-dec k ks
... | yes k∈ks
with refl updating-via-k∈ks-≡ (f l₁) (updater l₁) k∈ks k,v₁∈f'l₁
with refl updating-via-k∈ks-≡ (f l₂) (updater l₂) k∈ks k,v₂∈f'l₂ =
(updater l₂ k , (g-Monotonicʳ k l₁≼l₂ , k,v₂∈f'l₂))
... | no k∉ks =
let
k,v₁∈fl₁ = updating-via-k∉ks-backward (f l₁) (updater l₁) k∉ks k,v₁∈f'l₁
k,v₂∈fl₂ = updating-via-k∉ks-backward (f l₂) (updater l₂) k∉ks k,v₂∈f'l₂
k,v₁v₂∈fl₁fl₂ = ⊔-combines {m₁ = f l₁} {m₂ = f l₂} k,v₁∈fl₁ k,v₂∈fl₂
(v' , (v'≈v₁v₂ , k,v'∈fl₂)) = fl₁fl₂⊆fl₂ k _ k,v₁v₂∈fl₁fl₂
k,v'∈f'l₂ = updating-via-k∉ks-forward (f l₂) (updater l₂) k∉ks k,v'∈fl₂
in
(v' , (v'≈v₁v₂ , k,v'∈f'l₂))
f'l₂⊆f'l₁f'l₂ : f' l₂ ((f' l₁) (f' l₂))
f'l₂⊆f'l₁f'l₂ k v k,v∈f'l₂
with k∈kfl₂ updating-via-∈k-backward (f l₂) ks (updater l₂) (forget k,v∈f'l₂)
with (v' , k,v'∈fl₂) locate {m = f l₂} k∈kfl₂
with (v'' , (v'≈v'' , k,v''∈fl₁fl₂)) fl₂⊆fl₁fl₂ k v' k,v'∈fl₂
with Expr-Provenance-≡ ((` (f l₁)) (` (f l₂))) k,v''∈fl₁fl₂
... | in (single k,v''∈fl₁) k∉kfl₂ = ⊥-elim (k∉kfl₂ k∈kfl₂)
... | in k∉kfl₁ (single k,v''∈fl₂) =
let
k∉kf'l₁ = updating-via-∉k-forward (f l₁) ks (updater l₁) k∉kfl₁
in
(v , (IsLattice.≈-refl lB , union-preserves-∈₂ k∉kf'l₁ k,v∈f'l₂))
... | bothᵘ (single {v₁} k,v₁∈fl₁) (single {v₂} k,v₂∈fl₂)
with k∈-dec k ks
... | yes k∈ks with refl updating-via-k∈ks-≡ (f l₂) (updater l₂) k∈ks k,v∈f'l₂ =
let
k,uv₁∈f'l₁ = updating-via-k∈ks-forward (f l₁) (updater l₁) k∈ks (forget k,v₁∈fl₁)
k,uv₂∈f'l₂ = updating-via-k∈ks-forward (f l₂) (updater l₂) k∈ks (forget k,v₂∈fl₂)
k,uv₁uv₂∈f'l₁f'l₂ = ⊔-combines {m₁ = f' l₁} {m₂ = f' l₂} k,uv₁∈f'l₁ k,uv₂∈f'l₂
in
(updater l₁ k ⊔₂ updater l₂ k , (IsLattice.≈-sym lB (g-Monotonicʳ k l₁≼l₂) , k,uv₁uv₂∈f'l₁f'l₂))
... | no k∉ks
with k,v₁∈f'l₁ updating-via-k∉ks-forward (f l₁) (updater l₁) k∉ks k,v₁∈fl₁
with k,v₂∈f'l₂ updating-via-k∉ks-forward (f l₂) (updater l₂) k∉ks k,v₂∈fl₂
with k,v₁v₂∈f'l₁f'l₂ ⊔-combines {m₁ = f' l₁} {m₂ = f' l₂} k,v₁∈f'l₁ k,v₂∈f'l₂
with refl Map-functional {m = f' l₂} k,v∈f'l₂ k,v₂∈f'l₂
with refl Map-functional {m = f l₂} k,v'∈fl₂ k,v₂∈fl₂ =
(v₁ ⊔₂ v , (v'≈v'' , k,v₁v₂∈f'l₁f'l₂))
_[_] : Map List A List B
_[_] m [] = []
_[_] m (k ks)
with ∈k-dec k (proj₁ m)
... | yes k∈km = proj₁ (locate {m = m} k∈km) (m [ ks ])
... | no _ = m [ ks ]
m₁≼m₂⇒m₁[k]≼m₂[k] : (m₁ m₂ : Map) {k : A} {v₁ v₂ : B}
m₁ m₂ (k , v₁) m₁ (k , v₂) m₂ v₁ ≼₂ v₂
m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
with k,v₁v₂∈m₁m₂ ⊔-combines {m₁ = m₁} {m₂ = m₂} k,v₁∈m₁ k,v₂∈m₂
with (v' , (v₁v₂≈v' , k,v'∈m₂)) (proj₁ m₁≼m₂) _ _ k,v₁v₂∈m₁m₂
with refl Map-functional {m = m₂} k,v₂∈m₂ k,v'∈m₂
= v₁v₂≈v'
m₁≼m₂⇒k∈km₁⇒k∈km₂ : (m₁ m₂ : Map) {k : A}
m₁ m₂ k ∈k m₁ k ∈k m₂
m₁≼m₂⇒k∈km₁⇒k∈km₂ m₁ m₂ m₁≼m₂ k∈km₁ =
let
k∈km₁m₂ = union-preserves-∈k₁ {l₁ = proj₁ m₁} {l₂ = proj₁ m₂} k∈km₁
(v , k,v∈m₁m₂) = locate {m = m₁ m₂} k∈km₁m₂
(v' , (v≈v' , k,v'∈m₂)) = (proj₁ m₁≼m₂) _ _ k,v∈m₁m₂
in
forget k,v'∈m₂