From deebe088c25dc84ad9dd549135290e248f80e9c6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Jun 2021 11:39:52 +0200
Subject: [PATCH] Add lemmas `merge_empty_l` and `merge_empty_r`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 31bc30b3..9e09f752 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1722,6 +1722,18 @@ Section more_merge.
   Qed.
 End more_merge.
 
+Lemma merge_empty_l {A B C} (f : option A → option B → option C) (m2 : M B) :
+  merge f ∅ m2 = omap (f None ∘ Some) m2.
+Proof.
+  apply map_eq; intros i. rewrite lookup_merge, lookup_omap, lookup_empty.
+  by destruct (m2 !! i).
+Qed.
+Lemma merge_empty_r {A B C} (f : option A → option B → option C) (m1 : M A) :
+  merge f m1 ∅ = omap (flip f None ∘ Some) m1.
+Proof.
+  apply map_eq; intros i. rewrite lookup_merge, lookup_omap, lookup_empty.
+  by destruct (m1 !! i).
+Qed.
 Lemma merge_diag {A C} (f : option A → option A → option C) (m : M A) :
   merge f m m = omap (λ x, f (Some x) (Some x)) m.
 Proof.
-- 
GitLab