From ff92006d387bd1e407dd1a8fe50476a2481a537c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 26 Jul 2022 21:03:56 +0200
Subject: [PATCH] Add `map_Exists_lookup_{1,2}`.
---
theories/fin_maps.v | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 06769b8a..b1a2c185 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1585,6 +1585,12 @@ Section map_Exists.
Lemma map_Exists_lookup m :
map_Exists P m ↔ ∃ i x, m !! i = Some x ∧ P i x.
Proof. done. Qed.
+ Lemma map_Exists_lookup_1 m :
+ map_Exists P m → ∃ i x, m !! i = Some x ∧ P i x.
+ Proof. by rewrite map_Exists_lookup. Qed.
+ Lemma map_Exists_lookup_2 m i x :
+ m !! i = Some x → P i x → map_Exists P m.
+ Proof. rewrite map_Exists_lookup. by eauto. Qed.
Lemma map_Exists_foldr_delete m is :
map_Exists P (foldr delete m is) → map_Exists P m.
Proof. induction is; eauto using map_Exists_delete. Qed.
--
GitLab