From 42a87a40bf9da5794bbde639943aaf1fc2c979c7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 9 Apr 2018 22:59:12 +0200
Subject: [PATCH] `Equiv` instance for multisets.

This fixes issue #12.
---
 theories/gmultiset.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 6d6e0356..15c9b648 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -25,6 +25,8 @@ Section definitions.
     0 < multiplicity x X.
   Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, ∀ x,
     multiplicity x X ≤ multiplicity x Y.
+  Global Instance gmultiset_equiv : Equiv (gmultiset A) := λ X Y, ∀ x,
+    multiplicity x X = multiplicity x Y.
 
   Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
     let (X) := X in ''(x,n) ← map_to_list X; replicate (S n) x.
@@ -62,6 +64,8 @@ Proof.
   specialize (HXY x); unfold multiplicity in *; simpl in *.
   repeat case_match; naive_solver.
 Qed.
+Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
+Proof. intros X Y. by rewrite gmultiset_eq. Qed.
 
 (* Multiplicity *)
 Lemma multiplicity_empty x : multiplicity x ∅ = 0.
-- 
GitLab