From c20e4f25cbf65ff53f758bc8f339c588c860aed3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 May 2019 08:07:38 +0200
Subject: [PATCH] Lemmas for big-ops and bind.

---
 theories/algebra/big_op.v |  6 ++++++
 theories/bi/big_op.v      | 12 ++++++++++++
 2 files changed, 18 insertions(+)

diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index d4d0ec2d9..ee57b0dfa 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -154,6 +154,12 @@ Section list.
   Qed.
 End list.
 
+Lemma big_opL_bind {A B} (h : A → list B) (f : B → M) l :
+  ([^o list] y ∈ l ≫= h, f y) ≡ ([^o list] x ∈ l, [^o list] y ∈ h x, f y).
+Proof.
+  revert f. induction l as [|x l IH]=> f; csimpl=> //. by rewrite big_opL_app IH.
+Qed.
+
 (** ** Big ops over finite maps *)
 Section gmap.
   Context `{Countable K} {A : Type}.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 9c9469a5a..66915c353 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -136,6 +136,10 @@ Section sep_list.
     ([∗ list] k↦y ∈ f <$> l, Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k (f y)).
   Proof. by rewrite big_opL_fmap. Qed.
 
+  Lemma big_sepL_bind {B} (f : A → list B) (Φ : B → PROP) l :
+    ([∗ list] y ∈ l ≫= f, Φ y) ⊣⊢ ([∗ list] x ∈ l, [∗ list] y ∈ f x, Φ y).
+  Proof. by rewrite big_opL_bind. Qed.
+
   Lemma big_sepL_sep Φ Ψ l :
     ([∗ list] k↦x ∈ l, Φ k x ∗ Ψ k x)
     ⊣⊢ ([∗ list] k↦x ∈ l, Φ k x) ∗ ([∗ list] k↦x ∈ l, Ψ k x).
@@ -511,6 +515,10 @@ Section and_list.
     ([∧ list] k↦y ∈ f <$> l, Φ k y) ⊣⊢ ([∧ list] k↦y ∈ l, Φ k (f y)).
   Proof. by rewrite big_opL_fmap. Qed.
 
+  Lemma big_andL_bind {B} (f : A → list B) (Φ : B → PROP) l :
+    ([∧ list] y ∈ l ≫= f, Φ y) ⊣⊢ ([∧ list] x ∈ l, [∧ list] y ∈ f x, Φ y).
+  Proof. by rewrite big_opL_bind. Qed.
+
   Lemma big_andL_and Φ Ψ l :
     ([∧ list] k↦x ∈ l, Φ k x ∧ Ψ k x)
     ⊣⊢ ([∧ list] k↦x ∈ l, Φ k x) ∧ ([∧ list] k↦x ∈ l, Ψ k x).
@@ -597,6 +605,10 @@ Section or_list.
     ([∨ list] k↦y ∈ f <$> l, Φ k y) ⊣⊢ ([∨ list] k↦y ∈ l, Φ k (f y)).
   Proof. by rewrite big_opL_fmap. Qed.
 
+  Lemma big_orL_bind {B} (f : A → list B) (Φ : B → PROP) l :
+    ([∨ list] y ∈ l ≫= f, Φ y) ⊣⊢ ([∨ list] x ∈ l, [∨ list] y ∈ f x, Φ y).
+  Proof. by rewrite big_opL_bind. Qed.
+
   Lemma big_orL_or Φ Ψ l :
     ([∨ list] k↦x ∈ l, Φ k x ∨ Ψ k x)
     ⊣⊢ ([∨ list] k↦x ∈ l, Φ k x) ∨ ([∨ list] k↦x ∈ l, Ψ k x).
-- 
GitLab