From fe9771cc617ac34b5066cd1b4e232ac4ace675db Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 3 Sep 2014 13:01:38 +0200
Subject: [PATCH] Decider for empty listsets.

---
 theories/listset.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/listset.v b/theories/listset.v
index 5c3df887..1f318c7b 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -24,6 +24,16 @@ Proof.
   * by apply elem_of_list_singleton.
   * intros [?] [?]. apply elem_of_app.
 Qed.
+Lemma listset_empty_alt X : X ≡ ∅ ↔ listset_car X = [].
+Proof.
+  destruct X as [l]; split; [|by intros; simplify_equality'].
+  intros [Hl _]; destruct l as [|x l]; [done|]. feed inversion (Hl x); left.
+Qed. 
+Global Instance listset_empty_dec (X : listset A) : Decision (X ≡ ∅).
+Proof.
+ refine (cast_if (decide (listset_car X = [])));
+  abstract (by rewrite listset_empty_alt).
+Defined.
 
 Context `{∀ x y : A, Decision (x = y)}.
 
-- 
GitLab