Lemmas for big-ops and bind.

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}.

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).