From ad26d20274589f0d7f8591380fba01c4847377fa Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 11 Feb 2024 12:45:43 -0800
Subject: [PATCH] Add facts about equal-key maps

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Map.agda | 39 ++++++++++++++++++++++++++++++++++++++-
 1 file changed, 38 insertions(+), 1 deletion(-)

diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index 2f74dc0..fa6935e 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -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.Empty using (⊥; ⊥-elim)
 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
     ( ≈-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
     ...   | 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₂
@@ -346,6 +360,29 @@ private module ImplInsert (f : B → B → B) where
             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₂ =