From 4033a1b33dfaac7daeead1f8dcab4205c0b3f65e Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 28 Jul 2023 00:05:41 -0700
Subject: [PATCH] Prove most of commutativity by relying on in-dec.

The "no" case still needs to be dismissed, but that can probably
be done by some lemma about keys in maps.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Map.agda | 73 ++++++++++++++++++++++++++++++++++++++------------------
 1 file changed, 50 insertions(+), 23 deletions(-)

diff --git a/Map.agda b/Map.agda
index bea637a..e655783 100644
--- a/Map.agda
+++ b/Map.agda
@@ -69,6 +69,28 @@ private module _ where
     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 : ∀ {k : A} {l : List (A × B)} → k ∈ keys l → Σ B (λ v → (k , v) ∈ l)
+    locate {k} {(k' , v) ∷ xs} (here k≡k') rewrite k≡k' = (v , here refl)
+    locate {k} {(k' , v) ∷ xs} (there k∈kxs) = let (v , k,v∈xs) = locate k∈kxs in (v , there k,v∈xs)
+
 private module ImplRelation (_≈_ : B → B → Set b) where
     open MemProp using (_∈_)
 
@@ -117,28 +139,6 @@ private module ImplInsert (f : B → B → B) where
     ...   | no _ = cong (λ xs' → k' ∷ xs')
                         (insert-keys-∉ k v xs (λ k∈kxs → k∉kl (there k∈kxs)))
 
-    ∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈k 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 ∈k ((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 : ∀ {k : A} {l : List (A × B)} → k ∈k l → Σ B (λ v → (k , v) ∈ l)
-    locate {k} {(k' , v) ∷ xs} (here k≡k') rewrite k≡k' = (v , here refl)
-    locate {k} {(k' , v) ∷ xs} (there k∈kxs) = let (v , k,v∈xs) = locate k∈kxs in (v , there k,v∈xs)
-
     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
@@ -304,7 +304,6 @@ module _ (f : B → B → B) where
             (in₂ v₂ k∉kl₁ k,v₂∈l₂ , merge-preserves-keys₁ k v₂ l₁ l₂ k∉kl₁ k,v₂∈l₂)
     ...   | no k∉kl₁ | no k∉kl₂  = absurd (merge-preserves-∉ k l₁ l₂ k∉kl₁ k∉kl₂ k∈km₁m₂)
 
-
 module _ (_≈_ : B → B → Set b) where
     open ImplRelation _≈_ renaming (subset to subset-impl)
 
@@ -313,3 +312,31 @@ module _ (_≈_ : B → B → Set b) where
 
     lift : Map → Map → Set (a ⊔ b)
     lift m₁ m₂ = subset m₁ m₂ × subset m₂ m₁
+
+module _ (f : B → B → B) where
+    module _ (f-comm : ∀ (b₁ b₂ : B) → f b₁ b₂ ≡ f b₂ b₁) where
+        merge-comm : forall (m₁ m₂ : Map) → lift (_≡_) (merge f m₁ m₂) (merge f m₂ m₁)
+        merge-comm m₁ m₂ = (merge-comm-subset m₁ m₂ , merge-comm-subset m₂ m₁)
+            where
+                merge-comm-subset : ∀ (m₁ m₂ : Map) → subset (_≡_) (merge f m₁ m₂) (merge f m₂ m₁)
+                merge-comm-subset m₁ m₂ k v k,v∈m₁m₂
+                    with ∈k-dec k (proj₁ (merge f m₂ m₁) )
+                ...   | no k∉km₂m₁ = {!!}
+                ...   | yes k∈km₂m₁ with merge-provenance f m₁ m₂ k (∈-cong proj₁ k,v∈m₁m₂) | merge-provenance f m₂ m₁ k k∈km₂m₁
+                ...       | (both v₁ v₂ v₁∈m₁ v₂∈m₂ , v₁v₂∈m₁m₂) | (both v₂' v₁' v₂'∈m₂ v₁'∈m₁ , v₂'v₁'∈m₂m₁)
+                            rewrite Map-functional {m = merge f m₁ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂
+                            rewrite Map-functional {m = m₁} v₁∈m₁ v₁'∈m₁
+                            rewrite Map-functional {m = m₂} v₂∈m₂ v₂'∈m₂ = (f v₂' v₁' , (f-comm v₁' v₂' , v₂'v₁'∈m₂m₁))
+                ...       | (in₁ v₁ v₁∈m₁ _ , v₁∈m₁m₂) | (in₂ v₁' _ v₁'∈m₁ , v₁'∈m₂m₁)
+                            rewrite Map-functional {m = merge f m₁ m₂} k,v∈m₁m₂ v₁∈m₁m₂ =
+                                (v₁' , (Map-functional {m = m₁} v₁∈m₁ v₁'∈m₁ , v₁'∈m₂m₁))
+                ...       | (in₂ v₂ _ v₂∈m₂ , v₂∈m₁m₂) | (in₁ v₂' v₂'∈m₂ _ , v₂'∈m₂m₁)
+                            rewrite Map-functional {m = merge f m₁ m₂} k,v∈m₁m₂ v₂∈m₁m₂ =
+                                (v₂' , (Map-functional {m = m₂} v₂∈m₂ v₂'∈m₂ , v₂'∈m₂m₁))
+                -- The rest of the cases are to be dismissed.
+                ...       | (both v₁ v₂ v₁∈m₁ v₂∈m₂ , _) | (in₁ v₂' v₂'∈m₂ k∉km₁ , _) = absurd (k∉km₁ (∈-cong proj₁ v₁∈m₁))
+                ...       | (both v₁ v₂ v₁∈m₁ v₂∈m₂ , _) | (in₂ v₁' k∉km₂ v₁'∈m₁ , _) = absurd (k∉km₂ (∈-cong proj₁ v₂∈m₂))
+                ...       | (in₁ v₁ v₁∈m₁ k∉km₂ , _) | (both v₂' v₁' v₂'∈m₂ v₁'∈m₁ , _) = absurd (k∉km₂ (∈-cong proj₁ v₂'∈m₂))
+                ...       | (in₁ v₁ v₁∈m₁ k∉km₂ , _) | (in₁ v₂' v₂'∈m₂ k∉km₁ , _) = absurd (k∉km₂ (∈-cong proj₁ v₂'∈m₂))
+                ...       | (in₂ v₂ k∉km₁ v₂∈m₂ , v₂∈m₁m₂) | (both v₂' v₁' v₂'∈m₂ v₁'∈m₁ , _) = absurd (k∉km₁ (∈-cong proj₁ v₁'∈m₁))
+                ...       | (in₂ v₂ k∉km₁ v₂∈m₂ , v₂∈m₁m₂) | (in₂ v₁' _ v₁'∈m₁ , v₁'∈m₂m₁) = absurd (k∉km₁ (∈-cong proj₁ v₁'∈m₁))