From 949f675568405c16fbc85a040248b304c23dc545 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Jan 2016 17:24:48 +0100
Subject: [PATCH] Property about validN and big_opM.

---
 modures/cmra.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/modures/cmra.v b/modures/cmra.v
index bce799331..6c3430f8a 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -220,6 +220,17 @@ Qed.
 Lemma cmra_empty_least `{Empty A, !RAIdentity A} n x : ∅ ≼{n} x.
 Proof. by exists x; rewrite (left_id _ _). Qed.
 
+(** ** big ops *)
+Section bigop.
+  Context `{Empty A, !RAIdentity A, FinMap K M}.
+  Lemma big_opM_lookup_valid n m i x :
+    ✓{n} (big_opM m) → m !! i = Some x → ✓{n} x.
+  Proof.
+    intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
+    apply cmra_valid_op_l.
+  Qed.
+End bigop.
+
 (** ** Properties of [(⇝)] relation *)
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
-- 
GitLab