From e2a38b9a7043234dcf0ff59a104b73ebe332b8cc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Jun 2021 11:38:26 +0200
Subject: [PATCH] Add lemma `map_fmap_singleton_inv`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index ea77ec1a..9b076482 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -807,6 +807,18 @@ Lemma map_fmap_singleton {A B} (f : A → B) i x :
 Proof.
   by unfold singletonM, map_singleton; rewrite fmap_insert, fmap_empty.
 Qed.
+Lemma map_fmap_singleton_inv {A B} (f : A → B) (m : M A) i y :
+  f <$> m = {[i := y]} → ∃ x, y = f x ∧ m = {[ i := x ]}.
+Proof.
+  intros Hm. pose proof (f_equal (.!! i) Hm) as Hmi.
+  rewrite lookup_fmap, lookup_singleton, fmap_Some in Hmi.
+  destruct Hmi as (x&?&->). exists x. split; [done|].
+  apply map_eq; intros j. destruct (decide (i = j)) as[->|?].
+  - by rewrite lookup_singleton.
+  - rewrite lookup_singleton_ne by done.
+    apply (fmap_None f). by rewrite <-lookup_fmap, Hm, lookup_singleton_ne.
+Qed.
+
 Lemma omap_singleton {A B} (f : A → option B) i x :
   omap f {[ i := x ]} =@{M B} match f x with Some y => {[ i:=y ]} | None => ∅ end.
 Proof.
-- 
GitLab