From 0a55fc55a51759c3f525f9c97326298f87e9a7c5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 22 Apr 2021 00:12:44 +0200
Subject: [PATCH] `Inj` instances for set and multiset singletons.

---
 theories/gmultiset.v | 6 ++++++
 theories/sets.v      | 4 ++++
 2 files changed, 10 insertions(+)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index c07aa6c3..311ded6e 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -380,6 +380,12 @@ Section more_lemmas.
   Proof. multiset_solver. Qed.
 
   (** Misc *)
+  Global Instance gmultiset_singleton_inj : Inj (=) (=@{gmultiset A}) singletonMS.
+  Proof.
+    intros x1 x2 Hx. rewrite gmultiset_eq in Hx. specialize (Hx x1).
+    rewrite multiplicity_singleton, multiplicity_singleton' in Hx.
+    case_decide; [done|lia].
+  Qed.
   Lemma gmultiset_non_empty_singleton x : {[+ x +]} ≠@{gmultiset A} ∅.
   Proof. multiset_solver. Qed.
 
diff --git a/theories/sets.v b/theories/sets.v
index f37e6869..984e667c 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -364,6 +364,10 @@ Section semi_set.
   Proof. set_solver. Qed.
   Lemma set_equiv_subseteq X Y : X ≡ Y ↔ X ⊆ Y ∧ Y ⊆ X.
   Proof. set_solver. Qed.
+  Global Instance singleton_equiv_inj : Inj (=) (≡@{C}) singleton.
+  Proof. unfold Inj. set_solver. Qed.
+  Global Instance singleton_inj `{!LeibnizEquiv C} : Inj (=) (=@{C}) singleton.
+  Proof. unfold Inj. set_solver. Qed.
 
   (** Subset relation *)
   Global Instance set_subseteq_antisymm: AntiSymm (≡) (⊆@{C}).
-- 
GitLab