Make iDestruct and iCombine work with (sep)conjunctions under big_ops.

algebra/upred_big_op.v

@@ -214,6 +214,18 @@ Section gmap.
     induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
     by rewrite later_sep IH.
   Qed.
+
+  Lemma big_sepM_always Φ m :
+    (□ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □ Φ k x).
+  Proof.
+    rewrite /uPred_big_sepM.
+    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?always_const //.
+    by rewrite always_sep IH.
+  Qed.
+
+  Lemma big_sepM_always_if p Φ m :
+    (□?p [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x).
+  Proof. destruct p; simpl; auto using big_sepM_always. Qed.
 End gmap.
 
 (** ** Big ops over finite sets *)
@@ -295,6 +307,17 @@ Section gset.
     induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
     by rewrite later_sep IH.
   Qed.
+
+  Lemma big_sepS_always Φ X : (□ [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y).
+  Proof.
+    rewrite /uPred_big_sepS.
+    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_const.
+    by rewrite always_sep IH.
+  Qed.
+
+  Lemma big_sepS_always_if q Φ X :
+    (□?q [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y).
+  Proof. destruct q; simpl; auto using big_sepS_always. Qed.
 End gset.
 
 (** ** Persistence *)

proofmode/coq_tactics.v

@@ -681,6 +681,20 @@ Proof. done. Qed.
 Global Instance sep_split_ownM (a b : M) :
   SepSplit (uPred_ownM (a ⋅ b)) (uPred_ownM a) (uPred_ownM b) | 99.
 Proof. by rewrite /SepSplit ownM_op. Qed.
+Global Instance sep_split_big_sepM
+    `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) m :
+  (∀ k x, SepSplit (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
+  SepSplit ([★ map] k ↦ x ∈ m, Φ k x)
+    ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x).
+Proof.
+  rewrite /SepSplit=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
+Qed.
+Global Instance sep_split_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) X :
+  (∀ x, SepSplit (Φ x) (Ψ1 x) (Ψ2 x)) →
+  SepSplit ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
+Proof.
+  rewrite /SepSplit=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
+Qed.
 
 Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
   SepSplit P Q1 Q2 →
@@ -759,6 +773,23 @@ Global Instance sep_destruct_later p P Q1 Q2 :
   SepDestruct p P Q1 Q2 → SepDestruct p (▷ P) (▷ Q1) (▷ Q2).
 Proof. by rewrite /SepDestruct -later_sep !always_if_later=> ->. Qed.
 
+Global Instance sep_destruct_big_sepM
+    `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) p m :
+  (∀ k x, SepDestruct p (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
+  SepDestruct p ([★ map] k ↦ x ∈ m, Φ k x)
+    ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x).
+Proof.
+  rewrite /SepDestruct=> ?. rewrite -big_sepM_sepM !big_sepM_always_if.
+  by apply big_sepM_mono.
+Qed.
+Global Instance sep_destruct_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X :
+  (∀ x, SepDestruct p (Φ x) (Ψ1 x) (Ψ2 x)) →
+  SepDestruct p ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
+Proof.
+  rewrite /SepDestruct=> ?. rewrite -big_sepS_sepS !big_sepS_always_if.
+  by apply big_sepS_mono.
+Qed.
+
 Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) → SepDestruct p P P1 P2 →
   envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' →