From eee814ae3ce15bfc70971ad737972d942ac24ad4 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 3 Sep 2023 16:57:56 -0700
Subject: [PATCH] Add congruence for Map union and intersect

---
 Map.agda | 60 +++++++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 55 insertions(+), 5 deletions(-)

diff --git a/Map.agda b/Map.agda
index db2aee6..3cf083e 100644
--- a/Map.agda
+++ b/Map.agda
@@ -586,16 +586,66 @@ module _ (_≈_ : B → B → Set b) where
         ...   | _         | no  m₂̷⊆m₁ = no (λ (_ , m₂⊆m₁) → m₂̷⊆m₁ m₂⊆m₁)
         ...   | no  m₁̷⊆m₂ | _         = no (λ (m₁⊆m₂ , _) → m₁̷⊆m₂ m₁⊆m₂)
 
+    -- The Provenance type requires both union and intersection functions,
+    -- but sometimes here we're working with one operation only. Just use the
+    -- union/intersection function for both -- it doesn't matter, since we don't
+    -- use the dual operations in these proofs.
+
+    module _ (f : B → B → B)
+             (≈-f-cong : ∀ {b₁ b₂ b₃ b₄} → b₁ ≈ b₂ → b₃ ≈ b₄ → f b₁ b₃ ≈ f b₂ b₄) where
+        private module I = ImplInsert f
+
+        union-cong : ∀ {m₁ m₂ m₃ m₄ : Map} → lift m₁ m₂ → lift m₃ m₄ → lift (union f m₁ m₃) (union f m₂ m₄)
+        union-cong {m₁} {m₂} {m₃} {m₄} (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃) =
+            ( union-subset m₁ m₂ m₃ m₄ (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃)
+            , union-subset m₂ m₁ m₄ m₃ (m₂⊆m₁ , m₁⊆m₂) (m₄⊆m₃ , m₃⊆m₄)
+            )
+            where
+                ≈-∉-cong : ∀ {m₁ m₂ : Map} {k : A} → lift m₁ m₂ → ¬ k ∈k m₁ → ¬ k ∈k m₂
+                ≈-∉-cong (m₁⊆m₂ , m₂⊆m₁) k∉km₁ k∈km₂ =
+                    let (v₂ , k,v₂∈m₂) = locate k∈km₂
+                        (_ , (_ , k,v₁∈m₁)) = m₂⊆m₁ _ v₂ k,v₂∈m₂
+                    in k∉km₁ (∈-cong proj₁ k,v₁∈m₁)
+
+                union-subset : ∀ (m₁ m₂ m₃ m₄ : Map) → lift m₁ m₂ → lift m₃ m₄ → subset (union f m₁ m₃) (union f m₂ m₄)
+                union-subset m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
+                    with Expr-Provenance f f 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 = union f 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 (f v₂ v₄ , (≈-f-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 = union f 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 = union f 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₄))
+
+        intersect-cong : ∀ {m₁ m₂ m₃ m₄ : Map} → lift m₁ m₂ → lift m₃ m₄ → lift (intersect f m₁ m₃) (intersect f m₂ m₄)
+        intersect-cong {m₁} {m₂} {m₃} {m₄} (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃) =
+            ( intersect-subset m₁ m₂ m₃ m₄ (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃)
+            , intersect-subset m₂ m₁ m₄ m₃ (m₂⊆m₁ , m₁⊆m₂) (m₄⊆m₃ , m₃⊆m₄)
+            )
+            where
+                intersect-subset : ∀ (m₁ m₂ m₃ m₄ : Map) → lift m₁ m₂ → lift m₃ m₄ → subset (intersect f m₁ m₃) (intersect f m₂ m₄)
+                intersect-subset m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
+                    with Expr-Provenance f f 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 = intersect f 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 (f v₂ v₄ , (≈-f-cong v₁≈v₂ v₃≈v₄ , I.intersect-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
+
     module _ (≈-refl : ∀ {b : B} → b ≈ b)
              (≈-sym : ∀ {b₁ b₂ : B} → b₁ ≈ b₂ → b₂ ≈ b₁)
              (f : B → B → B) where
         private module I = ImplInsert f
 
-        -- The Provenance type requires both union and intersection functions,
-        -- but here we're working with one operation only. Just use the union function
-        -- for both -- it doesn't matter, since we don't use intersection in
-        -- these proofs.
-
         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)