From dbfaf7b80ce39ca321922be65dbc42ec7d5d8e6e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Sep 2016 13:30:01 +0200
Subject: [PATCH] Generic decider for emptyness of finite maps.

---
 theories/fin_maps.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 48d8ae53..8164fd51 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -730,6 +730,12 @@ Proof.
   exists i, x. rewrite <-elem_of_map_to_list, Hm. by left.
 Qed.
 
+Global Instance map_eq_dec_empty {A} (m : M A) : Decision (m = ∅) | 20.
+Proof.
+  refine (cast_if (decide (elements m = [])));
+    [apply _|by rewrite <-?map_to_list_empty' ..].
+Defined.
+
 (** Properties of the imap function *)
 Lemma lookup_imap {A B} (f : K → A → option B) m i :
   map_imap f m !! i = m !! i ≫= f i.
-- 
GitLab