Finally prove the provenance properties of merge.

Map.agda

@@ -135,9 +135,9 @@ private module ImplInsert (f : B → B → B) where
     ∈-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 : 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} (here k≡k') rewrite k≡k' = (v , here refl)
-    locate k ((k' , v) ∷ xs) (there k∈kxs) = let (v , k,v∈xs) = locate k xs k∈kxs in (v , there k,v∈xs)
+    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))
@@ -167,7 +167,7 @@ private module ImplInsert (f : B → B → B) where
     insert-preserves-∈k-right : ∀ (k k' : A) (v' : B) (l : List (A × B)) →
                                   ¬ k ≡ k' → k ∈k l → k ∈k insert k' v' l
     insert-preserves-∈k-right k k' v' l k≢k' k∈kl =
-        let (v , k,v∈l) = locate k l k∈kl
+        let (v , k,v∈l) = locate k∈kl
         in ∈-cong proj₁ (insert-preserves-∈-right k k' v v' l k≢k' k,v∈l)
 
     insert-preserves-∉-right : ∀ (k k' : A) (v' : B) (l : List (A × B)) →
@@ -284,28 +284,26 @@ module _ (f : B → B → B) where
     MergeResult {k} {m₁} {m₂} (in₂ v₂ _ _) = (k , v₂) ∈ merge m₁ m₂
 
     merge-provenance : ∀ (m₁ m₂ : Map) (k : A) → k ∈k merge m₁ m₂ → Σ (Provenance k m₁ m₂) MergeResult
-    merge-provenance = {!!}
+    merge-provenance m₁@(l₁ , u₁) m₂@(l₂ , u₂) k k∈km₁m₂
+        with ∈k-dec k l₁ | ∈k-dec k l₂
+    ...   | yes k∈kl₁ | yes k∈kl₂ =
+        let
+            (v₁ , k,v₁∈l₁) = locate k∈kl₁
+            (v₂ , k,v₂∈l₂) = locate k∈kl₂
+        in
+            (both v₁ v₂ k,v₁∈l₁ k,v₂∈l₂ , merge-combines k v₁ v₂ l₁ l₂ u₁ u₂ k,v₁∈l₁ k,v₂∈l₂)
+    ...   | yes k∈kl₁ | no k∉kl₂ =
+        let
+            (v₁ , k,v₁∈l₁) = locate k∈kl₁
+        in
+            (in₁ v₁ k,v₁∈l₁ k∉kl₂ , merge-preserves-keys₂ k v₁ l₁ l₂ u₁ k,v₁∈l₁ k∉kl₂)
+    ...   | no k∉kl₁ | yes k∈kl₂ =
+        let
+            (v₂ , k,v₂∈l₂) = locate k∈kl₂
+        in
+            (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₂)
 
-    -- ------------------------------------------------------------------------
-    --
-    -- The following can be proven using plain properties of insert:
-    --
-    -- prove that ¬ k ∈k m₁ → (k , v) ∈ m₂ → (k , v) ∈ merge m₁ m₂ (done)
-    --   prove that k ≢ k' → (k , v) ∈ m → (k , v) ∈ insert k' v' m (done)
-    -- prove that (k , v) ∈ m₁ → ¬ k ∈k m₂ → (k , v) ∈ merge m₁ m₂ (done)
-    --   prove that ¬ k ∈k m → (k , v) ∈ insert k v m (done)
-    --
-    -- ------------------------------------------------------------------------
-    --
-    -- The following relies on uniqueness, since inserts stops after the first encounter.
-    --
-    -- prove that (k , v) ∈ m₁ → (k , v') ∈ m₂ → (k, f v v') ∈ merge m₁ m₂ (done)
-    --
-    -- ------------------------------------------------------------------------
-    --
-    -- The following can probably be proven via keys.
-    --
-    -- prove that k ∉k m₁ → k ∉k m₂ → k ∉k merge m₁ m₂ (done)
 
 module _ (_≈_ : B → B → Set b) where
     open ImplRelation _≈_ renaming (subset to subset-impl)