From 324065a39c6c58cd6efac3715732ef723c983b4e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 7 Sep 2022 18:13:40 +0200
Subject: [PATCH] add map_choose_or_empty

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

diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 7179c796..776cb883 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -1015,6 +1015,9 @@ Proof.
     by rewrite <-?map_to_list_empty_iff.
 Defined.
 
+Lemma map_choose_or_empty {A} (m : M A) : (∃ i x, m !! i = Some x) ∨ m = ∅.
+Proof. destruct (decide (m = ∅)); [right|left]; auto using map_choose. Qed.
+
 (** Properties of the imap function *)
 Lemma map_lookup_imap {A B} (f : K → A → option B) (m : M A) i :
   map_imap f m !! i = m !! i ≫= f i.
-- 
GitLab