From 47b6bcc0722a29f26b589515d6edd00f0177af70 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Apr 2021 17:20:44 +0200
Subject: [PATCH] Add `Inj2` instance for singleton on maps.

---
 theories/fin_maps.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 74ef0e8e..1f0bc31b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -622,6 +622,15 @@ Proof. by rewrite lookup_singleton_None. Qed.
 Lemma lookup_total_singleton_ne `{!Inhabited A} i j (x : A) :
   i ≠ j → ({[i := x]} : M A) !!! j = inhabitant.
 Proof. intros. by rewrite lookup_total_alt, lookup_singleton_ne. Qed.
+
+Global Instance map_singleton_inj {A} : Inj2 (=) (=) (=) (singletonM (M:=M A)).
+Proof.
+  intros i1 x1 i2 x2 Heq%(f_equal (lookup i1)).
+  rewrite lookup_singleton in Heq. destruct (decide (i1 = i2)) as [->|].
+  - rewrite lookup_singleton in Heq. naive_solver.
+  - rewrite lookup_singleton_ne in Heq by done. naive_solver.
+Qed.
+
 Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ≠ (∅ : M A).
 Proof.
   intros Hix. apply (f_equal (.!! i)) in Hix.
-- 
GitLab