From e80f1433a3086d1737ae564174fcb344320c2b14 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Sep 2020 19:53:42 +0200
Subject: [PATCH] Add lemma `omap_insert_None`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 8861aea5..9d4ce12c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -677,6 +677,14 @@ Proof.
   - by rewrite lookup_omap, !lookup_insert.
   - by rewrite lookup_omap, !lookup_insert_ne, lookup_omap by done.
 Qed.
+Lemma omap_insert_None {A B} (f : A → option B) m i x :
+  f x = None → omap f (<[i:=x]>m) = delete i (omap f m).
+Proof.
+  intros; apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
+  - by rewrite lookup_omap, lookup_insert, lookup_delete.
+  - by rewrite lookup_omap, lookup_insert_ne,
+     lookup_delete_ne, lookup_omap by done.
+Qed.
 Lemma map_fmap_singleton {A B} (f : A → B) i x : f <$> {[i := x]} = {[i := f x]}.
 Proof.
   by unfold singletonM, map_singleton; rewrite fmap_insert, map_fmap_empty.
-- 
GitLab