Prove that Map equivalence is decidable

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Map.agda

@@ -1,4 +1,4 @@
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary using (Dec; yes; no; Reflects; ofʸ; ofⁿ)
@@ -533,6 +533,59 @@ module _ (_≈_ : B → B → Set b) where
     lift : Map → Map → Set (a ⊔ℓ b)
     lift m₁ m₂ = subset m₁ m₂ × subset m₂ m₁
 
+    private
+        data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
+            extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂
+            mismatch : (k : A) (v₁ v₂ : B) → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → ¬ v₁ ≈ v₂ → SubsetInfo m₁ m₂
+            fine : subset m₁ m₂ → SubsetInfo m₁ m₂
+
+        SubsetInfo-to-dec : ∀ {m₁ m₂ : Map} → SubsetInfo m₁ m₂ → Dec (subset m₁ m₂)
+        SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) =
+            let (v , k,v∈m₁) = locate k∈km₁
+            in no (λ m₁⊆m₂ →
+                   let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
+                   in k∉km₂ (∈-cong proj₁ k,v'∈m₂))
+        SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) =
+            no (λ m₁⊆m₂ →
+                let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁
+                in v₁̷≈v₂ (subst (λ v'' → v₁ ≈ v'') (Map-functional {k} {v'} {v₂} {m₂} k,v'∈m₂ k,v₂∈m₂) v₁≈v')) -- for some reason, can't just use subst...
+        SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂
+
+
+    module _ (≈-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈ b₂)) where
+        private
+            compute-SubsetInfo : ∀ m₁ m₂ → SubsetInfo m₁ m₂
+            compute-SubsetInfo ([] , _) m₂ = fine (λ k v ())
+            compute-SubsetInfo m₁@((k , v) ∷ xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂)
+                with compute-SubsetInfo (xs₁ , uxs₁) m₂
+            ...   | extra k' k'∈kxs₁ k'∉km₂ = extra k' (there k'∈kxs₁) k'∉km₂
+            ...   | mismatch k' v₁ v₂ k',v₁∈xs₁ k',v₂∈m₂ v₁̷≈v₂ =
+                    mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂
+            ...   | fine xs₁⊆m₂ with ∈k-dec k l₂
+            ...       | no k∉km₂ = extra k (here refl) k∉km₂
+            ...       | yes k∈km₂ with locate k∈km₂
+            ...           | (v' , k,v'∈m₂) with ≈-dec v v'
+            ...               | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v'
+            ...               | yes v≈v' = fine m₁⊆m₂
+                                    where
+                                        m₁⊆m₂ : subset m₁ m₂
+                                        m₁⊆m₂ k' v'' (here k,v≡k',v'')
+                                            rewrite cong proj₁ k,v≡k',v''
+                                            rewrite cong proj₂ k,v≡k',v'' =
+                                            (v' , (v≈v' , k,v'∈m₂))
+                                        m₁⊆m₂ k' v'' (there k,v≡k',v'') =
+                                            xs₁⊆m₂ k' v'' k,v≡k',v''
+
+        subset-dec : ∀ m₁ m₂ → Dec (subset m₁ m₂)
+        subset-dec m₁ m₂ = SubsetInfo-to-dec (compute-SubsetInfo m₁ m₂)
+
+        lift-dec : ∀ m₁ m₂ → Dec (lift m₁ m₂)
+        lift-dec m₁ m₂
+            with subset-dec m₁ m₂ | subset-dec m₂ m₁
+        ...   | yes m₁⊆m₂ | yes m₂⊆m₁ = yes (m₁⊆m₂ , m₂⊆m₁)
+        ...   | _         | no  m₂̷⊆m₁ = no (λ (_ , m₂⊆m₁) → m₂̷⊆m₁ m₂⊆m₁)
+        ...   | no  m₁̷⊆m₂ | _         = no (λ (m₁⊆m₂ , _) → m₁̷⊆m₂ m₁⊆m₂)
+
     module _ (≈-refl : ∀ {b : B} → b ≈ b)
              (≈-sym : ∀ {b₁ b₂ : B} → b₁ ≈ b₂ → b₂ ≈ b₁)
              (f : B → B → B) where