From 3663aaf33f3b5358139cf9129036a4fa2ae0db1a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 20 Nov 2016 16:05:58 +0100
Subject: [PATCH] More big op lemmas.

---
 algebra/cmra_big_op.v | 3 +++
 base_logic/big_op.v   | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index b97101969..92312ba12 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -267,6 +267,9 @@ Section gmap.
   Lemma big_opM_lookup f m i x :
     m !! i = Some x → f i x ≼ [⋅ map] k↦y ∈ m, f k y.
   Proof. intros. rewrite big_opM_delete //. apply cmra_included_l. Qed.
+  Lemma big_opM_lookup_dom (f : K → M) m i :
+    is_Some (m !! i) → f i ≼ [⋅ map] k↦_ ∈ m, f k.
+  Proof. intros [x ?]. by eapply (big_opM_lookup (λ i x, f i)). Qed.
 
   Lemma big_opM_singleton f i x : ([⋅ map] k↦y ∈ {[i:=x]}, f k y) ≡ f i x.
   Proof.
diff --git a/base_logic/big_op.v b/base_logic/big_op.v
index 0a9b4b59d..40a0a71f2 100644
--- a/base_logic/big_op.v
+++ b/base_logic/big_op.v
@@ -330,6 +330,9 @@ Section gmap.
   Lemma big_sepM_lookup Φ m i x :
     m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x.
   Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. 
+  Lemma big_sepM_lookup_dom (Φ : K → uPred M) m i :
+    is_Some (m !! i) → ([∗ map] k↦_ ∈ m, Φ k) ⊢ Φ i.
+  Proof. intros [x ?]. by eapply (big_sepM_lookup (λ i x, Φ i)). Qed.
 
   Lemma big_sepM_singleton Φ i x : ([∗ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
   Proof. by rewrite big_opM_singleton. Qed.
-- 
GitLab