Add facts about equal-key maps

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-02-11 12:45:43 -08:00
parent 2b27e397b6
commit ad26d20274

View File

@ -19,7 +19,7 @@ open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-ex
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂) open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
open import Data.Empty using (⊥; ⊥-elim) open import Data.Empty using (⊥; ⊥-elim)
open import Equivalence open import Equivalence
open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any) open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any; All-x∈xs)
open IsLattice lB using () renaming open IsLattice lB using () renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
@ -133,6 +133,20 @@ private module ImplInsert (f : B → B → B) where
... | yes k∈kl rewrite insert-keys-∈ {v = v} k∈kl = u ... | 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 ... | 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)) union-preserves-Unique : (l₁ l₂ : List (A × B))
Unique (keys l₂) Unique (keys (union l₁ l₂)) Unique (keys l₂) Unique (keys (union l₁ l₂))
union-preserves-Unique [] l₂ u₂ = u₂ union-preserves-Unique [] l₂ u₂ = u₂
@ -346,6 +360,29 @@ private module ImplInsert (f : B → B → B) where
let (k∈kl₁ , k∈kxs) = restrict-needs-both k∈l₁xs let (k∈kl₁ , k∈kxs) = restrict-needs-both k∈l₁xs
in (k∈kl₁ , there k∈kxs) 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)} restrict-preserves-∉₁ : {k : A} {l₁ l₂ : List (A × B)}
¬ k ∈k l₁ ¬ k ∈k restrict l₁ l₂ ¬ k ∈k l₁ ¬ k ∈k restrict l₁ l₂
restrict-preserves-∉₁ {k} {l₁} {l₂} k∉kl₁ k∈kl₁l₂ = restrict-preserves-∉₁ {k} {l₁} {l₂} k∉kl₁ k∈kl₁l₂ =