From d56460549c766f88934a479d0e64b9ce4bbce5af Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Nov 2016 23:28:38 +0100
Subject: [PATCH] Show that gmultiset is a simple collection.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This way we can use set_solver to solve goals involving ∈.
---
 theories/gmultiset.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 3a069c8a..51b1a983 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -106,7 +106,21 @@ Proof.
   destruct (X !! _), (Y !! _); simplify_option_eq; omega.
 Qed.
 
+Lemma elem_of_multiplicity x X : x ∈ X ↔ 0 < multiplicity x X.
+Proof. done. Qed.
+
 (* Algebraic laws *)
+Global Instance gmultiset_simple_collection : SimpleCollection A (gmultiset A).
+Proof.
+  split.
+  - intros x. rewrite elem_of_multiplicity, multiplicity_empty. omega.
+  - intros x y. destruct (decide (x = y)) as [->|].
+    + rewrite elem_of_multiplicity, multiplicity_singleton. split; auto with lia.
+    + rewrite elem_of_multiplicity, multiplicity_singleton_ne by done.
+      by split; auto with lia.
+  - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. omega.
+Qed.
+
 Global Instance gmultiset_comm : Comm (@eq (gmultiset A)) (∪).
 Proof.
   intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; omega.
-- 
GitLab