From eeae7519050a0a93cb00ea4de0a9677493b902ed Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 15 Oct 2023 11:25:50 +0200
Subject: [PATCH] Add lemma `lookup_total_fmap`.

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

diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 603fd13a..05006006 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -715,6 +715,15 @@ Proof.
 Qed.
 
 (** ** Properties of the map operations *)
+Lemma lookup_total_fmap `{!Inhabited A, !Inhabited B} (f : A → B) (m : M A) i :
+  (f <$> m) !!! i =
+    match m !! i with Some _ => f (m !!! i) | None => inhabitant end.
+Proof. rewrite !lookup_total_alt, lookup_fmap. by destruct (m !! i). Qed.
+Lemma lookup_total_fmap' `{!Inhabited A, !Inhabited B}
+    (f : A → B) (m : M A) i :
+  is_Some (m !! i) → (f <$> m) !!! i = f (m !!! i).
+Proof. intros [x Hi]. by rewrite lookup_total_fmap, Hi. Qed.
+
 Global Instance map_fmap_inj {A B} (f : A → B) :
   Inj (=) (=) f → Inj (=@{M A}) (=@{M B}) (fmap f).
 Proof.
-- 
GitLab