From 4ecb139a80938c06890bb707988918d342175a40 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 ∈.
---
 prelude/gmultiset.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/prelude/gmultiset.v b/prelude/gmultiset.v
index 017873926..67e2a4aab 100644
--- a/prelude/gmultiset.v
+++ b/prelude/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