From 0666a61f7010d4897e922c2706df90fb6479ff76 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 9 Jun 2021 01:51:47 +0200
Subject: [PATCH] Add lemmas `map_singleton_equiv_inj` and
 `map_fmap_equiv_inj`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 59bd16ce..510074c1 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -677,6 +677,14 @@ Proof.
   - rewrite lookup_singleton in Heq. naive_solver.
   - rewrite lookup_singleton_ne in Heq by done. naive_solver.
 Qed.
+Global Instance map_singleton_equiv_inj `{Equiv A} :
+  Inj2 (=) (≡) (≡) (singletonM (M:=M A)).
+Proof.
+  intros i1 x1 i2 x2 Heq. specialize (Heq i1).
+  rewrite lookup_singleton in Heq. destruct (decide (i1 = i2)) as [->|].
+  - rewrite lookup_singleton in Heq. apply (inj _) in Heq. naive_solver.
+  - rewrite lookup_singleton_ne in Heq by done. inversion Heq.
+Qed.
 
 Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ≠ (∅ : M A).
 Proof.
@@ -716,6 +724,12 @@ Proof.
   intros ? m1 m2 Hm. apply map_eq; intros i.
   apply (inj (fmap (M:=option) f)). by rewrite <-!lookup_fmap, Hm.
 Qed.
+Global Instance map_fmap_equiv_inj `{Equiv A, Equiv B} (f : A → B) :
+  Inj (≡) (≡) f → Inj (≡@{M A}) (≡@{M B}) (fmap f).
+Proof.
+  intros ? m1 m2 Hm i. apply (inj (fmap (M:=option) f)).
+  rewrite <-!lookup_fmap. by apply lookup_proper.
+Qed.
 
 Lemma lookup_fmap_Some {A B} (f : A → B) (m : M A) i y :
   (f <$> m) !! i = Some y ↔ ∃ x, f x = y ∧ m !! i = Some x.
-- 
GitLab