From 87abb52a400e1040cdf6484d69c3488addf423aa Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 9 Dec 2016 16:11:04 +0100
Subject: [PATCH] Lemmas about Big ops and contains.

---
 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 42f06e44b..5c34694b7 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -157,6 +157,9 @@ Section list.
   Lemma big_opL_permutation (f : A → M) l1 l2 :
     l1 ≡ₚ l2 → ([⋅ list] x ∈ l1, f x) ≡ ([⋅ list] x ∈ l2, f x).
   Proof. intros Hl. by rewrite /big_opL !imap_const Hl. Qed.
+  Lemma big_opL_contains (f : A → M) l1 l2 :
+    l1 `contains` l2 → ([⋅ list] x ∈ l1, f x) ≼ ([⋅ list] x ∈ l2, f x).
+  Proof. intros Hl. apply big_op_contains. rewrite !imap_const. by rewrite ->Hl. Qed.
 
   Global Instance big_opL_ne l n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
diff --git a/base_logic/big_op.v b/base_logic/big_op.v
index 088389bb3..17df7d692 100644
--- a/base_logic/big_op.v
+++ b/base_logic/big_op.v
@@ -219,6 +219,9 @@ Section list.
     (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) →
     ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∗ list] k ↦ y ∈ l, Ψ k y).
   Proof. apply big_opL_proper. Qed.
+  Lemma big_sepL_contains (Φ : A → uPred M) l1 l2 :
+    l1 `contains` l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
+  Proof. intros ?. apply uPred_included. by apply: big_opL_contains. Qed.
 
   Global Instance big_sepL_mono' l :
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))
-- 
GitLab