From bd4a6a841d9e7fbfacd884b15480cd23897502a9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 6 Mar 2018 15:26:34 +0100
Subject: [PATCH] Prove `map_fmap_empty_inv`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 124966f7..f6067783 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -261,6 +261,11 @@ Proof.
 Qed.
 Lemma map_fmap_empty {A B} (f : A → B) : f <$> (∅ : M A) = ∅.
 Proof. by apply map_eq; intros i; rewrite lookup_fmap, !lookup_empty. Qed.
+Lemma map_fmap_empty_inv {A B} (f : A → B) m : f <$> m = ∅ → m = ∅.
+Proof.
+  intros Hm. apply map_eq; intros i. generalize (f_equal (lookup i) Hm).
+  by rewrite lookup_fmap, !lookup_empty, fmap_None.
+Qed.
 
 Lemma map_subset_alt {A} (m1 m2 : M A) :
   m1 ⊂ m2 ↔ m1 ⊆ m2 ∧ ∃ i, m1 !! i = None ∧ is_Some (m2 !! i).
-- 
GitLab