From a6d4d0774caf4c1027d41f10f8a78f39890ffab8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 May 2020 15:30:41 +0200
Subject: [PATCH] prove lemma in both directions

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index de87feaf..fd55a879 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1234,9 +1234,15 @@ Proof.
 Qed.
 Lemma map_Forall_delete m i : map_Forall P m → map_Forall P (delete i m).
 Proof. intros Hm j x; rewrite lookup_delete_Some. naive_solver. Qed.
-Lemma map_Forall_lookup m i x :
-  m !! i = Some x → map_Forall P m → P i x.
-Proof. intros Hlk Hm. by apply Hm. Qed.
+Lemma map_Forall_lookup m :
+  map_Forall P m ↔ ∀ i x, m !! i = Some x → P i x.
+Proof. done. Qed.
+Lemma map_Forall_lookup_1 m i x :
+  map_Forall P m → m !! i = Some x → P i x.
+Proof. intros ?. by apply map_Forall_lookup. Qed.
+Lemma map_Forall_lookup_2 m :
+  (∀ i x, m !! i = Some x → P i x) → map_Forall P m.
+Proof. intros ?. by apply map_Forall_lookup. Qed.
 Lemma map_Forall_foldr_delete m is :
   map_Forall P m → map_Forall P (foldr delete m is).
 Proof. induction is; eauto using map_Forall_delete. Qed.
-- 
GitLab