Define big operators on uPred in terms of those on CMRAs.

algebra/cmra_big_op.v

@@ -62,8 +62,13 @@ Context {M : ucmraT}.
 Implicit Types xs : list M.
 
 (** * Big ops *)
+Lemma big_op_Forall2 R :
+  Reflexive R → Proper (R ==> R ==> R) (@op M _) →
+  Proper (Forall2 R ==> R) (@big_op M).
+Proof. rewrite /Proper /respectful. induction 3; eauto. Qed.
+
 Global Instance big_op_ne n : Proper (dist n ==> dist n) (@big_op M).
-Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
+Proof. apply big_op_Forall2; apply _. Qed.
 Global Instance big_op_proper : Proper ((≡) ==> (≡)) (@big_op M) := ne_proper _.
 
 Lemma big_op_nil : [⋅] (@nil M) = ∅.
@@ -108,54 +113,48 @@ Section list.
   Implicit Types l : list A.
   Implicit Types f g : nat → A → M.
 
+  Lemma big_opL_nil f : ([⋅ list] k↦y ∈ nil, f k y) = ∅.
+  Proof. done. Qed.
+  Lemma big_opL_cons f x l :
+    ([⋅ list] k↦y ∈ x :: l, f k y) = f 0 x ⋅ [⋅ list] k↦y ∈ l, f (S k) y.
+  Proof. by rewrite /big_opL imap_cons. Qed.
+  Lemma big_opL_singleton f x : ([⋅ list] k↦y ∈ [x], f k y) ≡ f 0 x.
+  Proof. by rewrite big_opL_cons big_opL_nil right_id. Qed.
+  Lemma big_opL_app f l1 l2 :
+    ([⋅ list] k↦y ∈ l1 ++ l2, f k y)
+    ≡ ([⋅ list] k↦y ∈ l1, f k y) ⋅ ([⋅ list] k↦y ∈ l2, f (length l1 + k) y).
+  Proof. by rewrite /big_opL imap_app big_op_app. Qed.
+
+  Lemma big_opL_forall R f g l :
+    Reflexive R → Proper (R ==> R ==> R) (@op M _) →
+    (∀ k y, l !! k = Some y → R (f k y) (g k y)) →
+    R ([⋅ list] k ↦ y ∈ l, f k y) ([⋅ list] k ↦ y ∈ l, g k y).
+  Proof.
+    intros ? Hop. revert f g. induction l as [|x l IH]=> f g Hf; [done|].
+    rewrite !big_opL_cons. apply Hop; eauto.
+  Qed.
+
   Lemma big_opL_mono f g l :
     (∀ k y, l !! k = Some y → f k y ≼ g k y) →
     ([⋅ list] k ↦ y ∈ l, f k y) ≼ [⋅ list] k ↦ y ∈ l, g k y.
-  Proof.
-    intros Hf. apply big_op_mono.
-    revert f g Hf. induction l as [|x l IH]=> f g Hf; first constructor.
-    rewrite !imap_cons; constructor; eauto.
-  Qed.
+  Proof. apply big_opL_forall; apply _. Qed.
   Lemma big_opL_proper f g l :
     (∀ k y, l !! k = Some y → f k y ≡ g k y) →
     ([⋅ list] k ↦ y ∈ l, f k y) ≡ ([⋅ list] k ↦ y ∈ l, g k y).
-  Proof.
-    intros Hf; apply big_op_proper.
-    revert f g Hf. induction l as [|x l IH]=> f g Hf; first constructor.
-    rewrite !imap_cons; constructor; eauto.
-  Qed.
+  Proof. apply big_opL_forall; apply _. Qed.
 
   Global Instance big_opL_ne l n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
            (big_opL (M:=M) l).
-  Proof.
-    intros f g Hf. apply big_op_ne.
-    revert f g Hf. induction l as [|x l IH]=> f g Hf; first constructor.
-    rewrite !imap_cons; constructor. by apply Hf. apply IH=> n'; apply Hf.
-  Qed.
+  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
   Global Instance big_opL_proper' l :
     Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡))
            (big_opL (M:=M) l).
-  Proof. intros f1 f2 Hf. by apply big_opL_proper; intros; last apply Hf. Qed.
+  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
   Global Instance big_opL_mono' l :
     Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> (≼))
            (big_opL (M:=M) l).
-  Proof. intros f1 f2 Hf. by apply big_opL_mono; intros; last apply Hf. Qed.
-
-  Lemma big_opL_nil f : ([⋅ list] k↦y ∈ nil, f k y) = ∅.
-  Proof. done. Qed.
-
-  Lemma big_opL_cons f x l :
-    ([⋅ list] k↦y ∈ x :: l, f k y) = f 0 x ⋅ [⋅ list] k↦y ∈ l, f (S k) y.
-  Proof. by rewrite /big_opL imap_cons. Qed.
-
-  Lemma big_opL_singleton f x : ([⋅ list] k↦y ∈ [x], f k y) ≡ f 0 x.
-  Proof. by rewrite big_opL_cons big_opL_nil right_id. Qed.
-
-  Lemma big_opL_app f l1 l2 :
-    ([⋅ list] k↦y ∈ l1 ++ l2, f k y)
-    ≡ ([⋅ list] k↦y ∈ l1, f k y) ⋅ ([⋅ list] k↦y ∈ l2, f (length l1 + k) y).
-  Proof. by rewrite /big_opL imap_app big_op_app. Qed.
+  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_opL_lookup f l i x :
     l !! i = Some x → f i x ≼ [⋅ list] k↦y ∈ l, f k y.
@@ -191,38 +190,40 @@ Section gmap.
   Implicit Types m : gmap K A.
   Implicit Types f g : K → A → M.
 
+  Lemma big_opM_forall R f g m :
+    Reflexive R → Proper (R ==> R ==> R) (@op M _) →
+    (∀ k x, m !! k = Some x → R (f k x) (g k x)) →
+    R ([⋅ map] k ↦ x ∈ m, f k x) ([⋅ map] k ↦ x ∈ m, g k x).
+  Proof.
+    intros ?? Hf. apply (big_op_Forall2 R _ _), Forall2_fmap, Forall_Forall2.
+    apply Forall_forall=> -[i x] ? /=. by apply Hf, elem_of_map_to_list.
+  Qed.
+
   Lemma big_opM_mono f g m1 m2 :
     m1 ⊆ m2 → (∀ k x, m2 !! k = Some x → f k x ≼ g k x) →
     ([⋅ map] k ↦ x ∈ m1, f k x) ≼ [⋅ map] k ↦ x ∈ m2, g k x.
   Proof.
-    intros HX Hf. trans ([⋅ map] k↦x ∈ m2, f k x).
+    intros Hm Hf. trans ([⋅ map] k↦x ∈ m2, f k x).
     - by apply big_op_contains, fmap_contains, map_to_list_contains.
-    - apply big_op_mono, Forall2_fmap, Forall_Forall2.
-      apply Forall_forall=> -[i x] ? /=. by apply Hf, elem_of_map_to_list.
+    - apply big_opM_forall; apply _ || auto.
   Qed.
   Lemma big_opM_proper f g m :
     (∀ k x, m !! k = Some x → f k x ≡ g k x) →
     ([⋅ map] k ↦ x ∈ m, f k x) ≡ ([⋅ map] k ↦ x ∈ m, g k x).
-  Proof.
-    intros Hf. apply big_op_proper, equiv_Forall2, Forall2_fmap, Forall_Forall2.
-    apply Forall_forall=> -[i x] ? /=. by apply Hf, elem_of_map_to_list.
-  Qed.
+  Proof. apply big_opM_forall; apply _. Qed.
 
   Global Instance big_opM_ne m n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
            (big_opM (M:=M) m).
-  Proof.
-    intros f1 f2 Hf. apply big_op_ne, Forall2_fmap.
-    apply Forall_Forall2, Forall_true=> -[i x]; apply Hf.
-  Qed.
+  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
   Global Instance big_opM_proper' m :
     Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡))
            (big_opM (M:=M) m).
-  Proof. intros f1 f2 Hf. by apply big_opM_proper; intros; last apply Hf. Qed.
+  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
   Global Instance big_opM_mono' m :
     Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> (≼))
            (big_opM (M:=M) m).
-  Proof. intros f1 f2 Hf. by apply big_opM_mono; intros; last apply Hf. Qed.
+  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_opM_empty f : ([⋅ map] k↦x ∈ ∅, f k x) = ∅.
   Proof. by rewrite /big_opM map_to_list_empty. Qed.
@@ -296,14 +297,22 @@ Section gset.
   Implicit Types X : gset A.
   Implicit Types f : A → M.
 
+  Lemma big_opS_forall R f g X :
+    Reflexive R → Proper (R ==> R ==> R) (@op M _) →
+    (∀ x, x ∈ X → R (f x) (g x)) →
+    R ([⋅ set] x ∈ X, f x) ([⋅ set] x ∈ X, g x).
+  Proof.
+    intros ?? Hf. apply (big_op_Forall2 R _ _), Forall2_fmap, Forall_Forall2.
+    apply Forall_forall=> x ? /=. by apply Hf, elem_of_elements.
+  Qed.
+
   Lemma big_opS_mono f g X Y :
     X ⊆ Y → (∀ x, x ∈ Y → f x ≼ g x) →
     ([⋅ set] x ∈ X, f x) ≼ [⋅ set] x ∈ Y, g x.
   Proof.
     intros HX Hf. trans ([⋅ set] x ∈ Y, f x).
     - by apply big_op_contains, fmap_contains, elements_contains.
-    - apply big_op_mono, Forall2_fmap, Forall_Forall2.
-      apply Forall_forall=> x ? /=. by apply Hf, elem_of_elements.
+    - apply big_opS_forall; apply _ || auto.
   Qed.
   Lemma big_opS_proper f g X Y :
     X ≡ Y → (∀ x, x ∈ X → x ∈ Y → f x ≡ g x) →
@@ -311,23 +320,18 @@ Section gset.
   Proof.
     intros HX Hf. trans ([⋅ set] x ∈ Y, f x).
     - apply big_op_permutation. by rewrite HX.
-    - apply big_op_proper, equiv_Forall2, Forall2_fmap, Forall_Forall2.
-      apply Forall_forall=> x ? /=.
-      apply Hf; first rewrite HX; by apply elem_of_elements.
+    - apply big_opS_forall; try apply _ || set_solver.
   Qed.
 
   Lemma big_opS_ne X n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (big_opS (M:=M) X).
-  Proof.
-    intros f1 f2 Hf. apply big_op_ne, Forall2_fmap.
-    apply Forall_Forall2, Forall_true=> x; apply Hf.
-  Qed.
+  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
   Lemma big_opS_proper' X :
     Proper (pointwise_relation _ (≡) ==> (≡)) (big_opS (M:=M) X).
-  Proof. intros f1 f2 Hf. apply big_opS_proper; naive_solver. Qed.
+  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
   Lemma big_opS_mono' X :
     Proper (pointwise_relation _ (≼) ==> (≼)) (big_opS (M:=M) X).
-  Proof. intros f1 f2 Hf. apply big_opS_mono; naive_solver. Qed.
+  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_opS_empty f : ([⋅ set] x ∈ ∅, f x) = ∅.
   Proof. by rewrite /big_opS elements_empty. Qed.

algebra/upred_big_op.v

@@ -2,56 +2,23 @@ From iris.algebra Require Export upred list cmra_big_op.
 From iris.prelude Require Import gmap fin_collections functions.
 Import uPred.
 
-(** We define the following big operators:
-
-- The operator [ [★] Ps ] folds [★] over the list [Ps].
-  This operator is not a quantifier, so it binds strongly.
-- The operator [ [★ list] k ↦ x ∈ l, P ] asserts that [P] holds separately for
-  each element [x] at position [x] in the list [l]. This operator is a
-  quantifier, and thus has the same precedence as [∀] and [∃].
-- The operator [ [★ map] k ↦ x ∈ m, P ] asserts that [P] holds separately for
-  each [k ↦ x] in the map [m]. This operator is a quantifier, and thus has the
-  same precedence as [∀] and [∃].
-- The operator [ [★ set] x ∈ X, P ] asserts that [P] holds separately for each
-  [x] in the set [X]. This operator is a quantifier, and thus has the same
-  precedence as [∀] and [∃]. *)
-
-(** * Big ops over lists *)
-(* These are the basic building blocks for other big ops *)
-Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M :=
-  match Ps with [] => True | P :: Ps => P ★ uPred_big_sep Ps end%I.
-Instance: Params (@uPred_big_sep) 1.
-Notation "'[★]' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
-
-(** * Other big ops *)
-Definition uPred_big_sepL {M A} (l : list A)
-  (Φ : nat → A → uPred M) : uPred M := [★] (imap Φ l).
-Instance: Params (@uPred_big_sepL) 2.
-Typeclasses Opaque uPred_big_sepL.
-Notation "'[★' 'list' ] k ↦ x ∈ l , P" := (uPred_big_sepL l (λ k x, P))
+Notation "'[★]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.
+
+Notation "'[★' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P))
   (at level 200, l at level 10, k, x at level 1, right associativity,
    format "[★  list ]  k ↦ x  ∈  l ,  P") : uPred_scope.
-Notation "'[★' 'list' ] x ∈ l , P" := (uPred_big_sepL l (λ _ x, P))
+Notation "'[★' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ _ x, P))
   (at level 200, l at level 10, x at level 1, right associativity,
    format "[★  list ]  x  ∈  l ,  P") : uPred_scope.
 
-Definition uPred_big_sepM {M} `{Countable K} {A}
-    (m : gmap K A) (Φ : K → A → uPred M) : uPred M :=
-  [★] (curry Φ <$> map_to_list m).
-Instance: Params (@uPred_big_sepM) 6.
-Typeclasses Opaque uPred_big_sepM.
-Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (uPred_big_sepM m (λ k x, P))
+Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ k x, P))
   (at level 200, m at level 10, k, x at level 1, right associativity,
    format "[★  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
-Notation "'[★' 'map' ] x ∈ m , P" := (uPred_big_sepM m (λ _ x, P))
+Notation "'[★' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ _ x, P))
   (at level 200, m at level 10, x at level 1, right associativity,
    format "[★  map ]  x  ∈  m ,  P") : uPred_scope.
 
-Definition uPred_big_sepS {M} `{Countable A}
-  (X : gset A) (Φ : A → uPred M) : uPred M := [★] (Φ <$> elements X).
-Instance: Params (@uPred_big_sepS) 5.
-Typeclasses Opaque uPred_big_sepS.
-Notation "'[★' 'set' ] x ∈ X , P" := (uPred_big_sepS X (λ x, P))
+Notation "'[★' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) X (λ x, P))
   (at level 200, X at level 10, x at level 1, right associativity,
    format "[★  set ]  x  ∈  X ,  P") : uPred_scope.
 
@@ -70,31 +37,17 @@ Context {M : ucmraT}.
 Implicit Types Ps Qs : list (uPred M).
 Implicit Types A : Type.
 
-(** ** Generic big ops over lists of upreds *)
-Global Instance big_sep_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_sep M).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_sep M).
+Global Instance big_sep_mono' :
+  Proper (Forall2 (⊢) ==> (⊢)) (big_op (M:=uPredUR M)).
 Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
-Global Instance big_sep_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_sep M).
-Proof.
-  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
-  - by rewrite IH.
-  - by rewrite !assoc (comm _ P).
-  - etrans; eauto.
-Qed.
-
 Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ [★] Ps ★ [★] Qs.
-Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
+Proof. by rewrite big_op_app. Qed.
 
 Lemma big_sep_contains Ps Qs : Qs `contains` Ps → [★] Ps ⊢ [★] Qs.
-Proof.
-  intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
-Qed.
+Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
 Lemma big_sep_elem_of Ps P : P ∈ Ps → [★] Ps ⊢ P.
-Proof. induction 1; simpl; auto with I. Qed.
+Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
 
 (** ** Persistence *)
 Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([★] Ps).
@@ -156,117 +109,57 @@ Section list.
   Implicit Types l : list A.
   Implicit Types Φ Ψ : nat → A → uPred M.
 
+  Lemma big_sepL_nil Φ : ([★ list] k↦y ∈ nil, Φ k y) ⊣⊢ True.
+  Proof. done. Qed.
+  Lemma big_sepL_cons Φ x l :
+    ([★ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ★ [★ list] k↦y ∈ l, Φ (S k) y.
+  Proof. by rewrite big_opL_cons. Qed.
+  Lemma big_sepL_singleton Φ x : ([★ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x.
+  Proof. by rewrite big_opL_singleton. Qed.
+  Lemma big_sepL_app Φ l1 l2 :
+    ([★ list] k↦y ∈ l1 ++ l2, Φ k y)
+    ⊣⊢ ([★ list] k↦y ∈ l1, Φ k y) ★ ([★ list] k↦y ∈ l2, Φ (length l1 + k) y).
+  Proof. by rewrite big_opL_app. Qed.
+
   Lemma big_sepL_mono Φ Ψ l :
     (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) →
     ([★ list] k ↦ y ∈ l, Φ k y) ⊢ [★ list] k ↦ y ∈ l, Ψ k y.
-  Proof.
-    intros HΦ. apply big_sep_mono'.
-    revert Φ Ψ HΦ. induction l as [|x l IH]=> Φ Ψ HΦ; first constructor.
-    rewrite !imap_cons; constructor; eauto.
-  Qed.
+  Proof. apply big_opL_forall; apply _. Qed.
+
   Lemma big_sepL_proper Φ Ψ l :
     (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) →
     ([★ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([★ list] k ↦ y ∈ l, Ψ k y).
-  Proof.
-    intros ?; apply (anti_symm (⊢)); apply big_sepL_mono;
-      eauto using equiv_entails, equiv_entails_sym, lookup_weaken.
-  Qed.
+  Proof. apply big_opL_proper. Qed.
 
-  Global Instance big_sepL_ne l n :
-    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
-           (uPred_big_sepL (M:=M) l).
-  Proof.
-    intros Φ Ψ HΦ. apply big_sep_ne.
-    revert Φ Ψ HΦ. induction l as [|x l IH]=> Φ Ψ HΦ; first constructor.
-    rewrite !imap_cons; constructor. by apply HΦ. apply IH=> n'; apply HΦ.
-  Qed.
-  Global Instance big_sepL_proper' l :
-    Proper (pointwise_relation _ (pointwise_relation _ (⊣⊢)) ==> (⊣⊢))
-           (uPred_big_sepL (M:=M) l).
-  Proof. intros Φ1 Φ2 HΦ. by apply big_sepL_proper; intros; last apply HΦ. Qed.
   Global Instance big_sepL_mono' l :
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))
-           (uPred_big_sepL (M:=M) l).
-  Proof. intros Φ1 Φ2 HΦ. by apply big_sepL_mono; intros; last apply HΦ. Qed.
-
-  Lemma big_sepL_nil Φ : ([★ list] k↦y ∈ nil, Φ k y) ⊣⊢ True.
-  Proof. done. Qed.
-
-  Lemma big_sepL_cons Φ x l :
-    ([★ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ★ [★ list] k↦y ∈ l, Φ (S k) y.
-  Proof. by rewrite /uPred_big_sepL imap_cons. Qed.
-
-  Lemma big_sepL_singleton Φ x : ([★ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x.
-  Proof. by rewrite big_sepL_cons big_sepL_nil right_id. Qed.
-
-  Lemma big_sepL_app Φ l1 l2 :
-    ([★ list] k↦y ∈ l1 ++ l2, Φ k y)
-    ⊣⊢ ([★ list] k↦y ∈ l1, Φ k y) ★ ([★ list] k↦y ∈ l2, Φ (length l1 + k) y).
-  Proof. by rewrite /uPred_big_sepL imap_app big_sep_app. Qed.
+           (big_opL (M:=uPredUR M) l).
+  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_sepL_lookup Φ l i x :
     l !! i = Some x → ([★ list] k↦y ∈ l, Φ k y) ⊢ Φ i x.
-  Proof.
-    intros. rewrite -(take_drop_middle l i x) // big_sepL_app big_sepL_cons.
-    rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl.
-    by rewrite sep_elim_r sep_elim_l.
-  Qed.
+  Proof. intros. apply uPred_included. by apply: big_opL_lookup. Qed.
 
   Lemma big_sepL_elem_of (Φ : A → uPred M) l x :
     x ∈ l → ([★ list] y ∈ l, Φ y) ⊢ Φ x.
-  Proof.
-    intros [i ?]%elem_of_list_lookup; eauto using (big_sepL_lookup (λ _, Φ)).
-  Qed.
+  Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed.
 
   Lemma big_sepL_fmap {B} (f : A → B) (Φ : nat → B → uPred M) l :
     ([★ list] k↦y ∈ f <$> l, Φ k y) ⊣⊢ ([★ list] k↦y ∈ l, Φ k (f y)).
-  Proof. by rewrite /uPred_big_sepL imap_fmap. Qed.
+  Proof. by rewrite big_opL_fmap. Qed.
 
   Lemma big_sepL_sepL Φ Ψ l :
     ([★ list] k↦x ∈ l, Φ k x ★ Ψ k x)
     ⊣⊢ ([★ list] k↦x ∈ l, Φ k x) ★ ([★ list] k↦x ∈ l, Ψ k x).
-  Proof.
-    revert Φ Ψ; induction l as [|x l IH]=> Φ Ψ.
-    { by rewrite !big_sepL_nil left_id. }
-    rewrite !big_sepL_cons IH.
-    by rewrite -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc.
-  Qed.
-
-  Lemma big_sepL_commute (Ψ: uPred M → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} Φ l :
-    Ψ True ⊣⊢ True →
-    (∀ P Q, Ψ (P ★ Q) ⊣⊢ Ψ P ★ Ψ Q) →
-    Ψ ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, Ψ (Φ k x)).
-  Proof.
-    intros ??. revert Φ. induction l as [|x l IH]=> Φ //.
-    by rewrite !big_sepL_cons -IH.
-  Qed.
-  Lemma big_sepL_op_commute {B : ucmraT}
-      (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : nat → A → B) l :
-    Ψ ∅ ⊣⊢ True →
-    (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) →
-    Ψ ([⋅ list] k↦x ∈ l, f k x) ⊣⊢ ([★ list] k↦x ∈ l, Ψ (f k x)).
-  Proof.
-    intros ??. revert f. induction l as [|x l IH]=> f //.
-    by rewrite big_sepL_cons big_opL_cons -IH.
-  Qed.
-  Lemma big_sepL_op_commute1 {B : ucmraT}
-      (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : nat → A → B) l :
-    (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) →
-    l ≠ [] →
-    Ψ ([⋅ list] k↦x ∈ l, f k x) ⊣⊢ ([★ list] k↦x ∈ l, Ψ (f k x)).
-  Proof.
-    intros ??. revert f. induction l as [|x [|x' l'] IH]=> f //.
-    { by rewrite big_sepL_singleton big_opL_singleton. }
-    by rewrite big_sepL_cons big_opL_cons -IH.
-  Qed.
+  Proof. by rewrite big_opL_opL. Qed.
 
   Lemma big_sepL_later Φ l :
     ▷ ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, ▷ Φ k x).
-  Proof. apply (big_sepL_commute _); auto using later_True, later_sep. Qed.
+  Proof. apply (big_opL_commute _). apply later_True. apply later_sep. Qed.
 
   Lemma big_sepL_always Φ l :
     (□ [★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, □ Φ k x).
-  Proof. apply (big_sepL_commute _); auto using always_pure, always_sep. Qed.
+  Proof. apply (big_opL_commute _). apply always_pure. apply always_sep. Qed.
 
   Lemma big_sepL_always_if p Φ l :
     □?p ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, □?p Φ k x).
@@ -298,17 +191,16 @@ Section list.
 
   Global Instance big_sepL_nil_persistent Φ :
     PersistentP ([★ list] k↦x ∈ [], Φ k x).
-  Proof. rewrite /uPred_big_sepL. apply _. Qed.
+  Proof. rewrite /big_opL. apply _. Qed.
   Global Instance big_sepL_persistent Φ l :
     (∀ k x, PersistentP (Φ k x)) → PersistentP ([★ list] k↦x ∈ l, Φ k x).
-  Proof. rewrite /uPred_big_sepL. apply _. Qed.
-
+  Proof. rewrite /big_opL. apply _. Qed.
   Global Instance big_sepL_nil_timeless Φ :
     TimelessP ([★ list] k↦x ∈ [], Φ k x).
-  Proof. rewrite /uPred_big_sepL. apply _. Qed.
+  Proof. rewrite /big_opL. apply _. Qed.
   Global Instance big_sepL_timeless Φ l :
     (∀ k x, TimelessP (Φ k x)) → TimelessP ([★ list] k↦x ∈ l, Φ k x).
-  Proof. rewrite /uPred_big_sepL. apply _. Qed.
+  Proof. rewrite /big_opL. apply _. Qed.
 End list.
 
 
@@ -322,134 +214,74 @@ Section gmap.
     m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
     ([★ map] k ↦ x ∈ m1, Φ k x) ⊢ [★ map] k ↦ x ∈ m2, Ψ k x.
   Proof.
-    intros HX HΦ. trans ([★ map] k↦x ∈ m2, Φ k x)%I.
-    - by apply big_sep_contains, fmap_contains, map_to_list_contains.
-    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
-      apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
+    intros Hm HΦ. trans ([★ map] k↦x ∈ m2, Φ k x)%I.
+    - apply uPred_included. apply: big_op_contains.
+      by apply fmap_contains, map_to_list_contains.
+    - apply big_opM_forall; apply _ || auto.
   Qed.
+
   Lemma big_sepM_proper Φ Ψ m :
     (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
     ([★ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m, Ψ k x).
-  Proof.
-    intros ?; apply (anti_symm (⊢)); apply big_sepM_mono;
-      eauto using equiv_entails, equiv_entails_sym, lookup_weaken.
-  Qed.
+  Proof. apply big_opM_proper. Qed.
 
-  Global Instance big_sepM_ne m n :
-    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
-           (uPred_big_sepM (M:=M) m).
-  Proof.
-    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
-    apply Forall_Forall2, Forall_true=> -[i x]; apply HΦ.
-  Qed.
-  Global Instance big_sepM_proper' m :
-    Proper (pointwise_relation _ (pointwise_relation _ (⊣⊢)) ==> (⊣⊢))
-           (uPred_big_sepM (M:=M) m).
-  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_proper; intros; last apply HΦ. Qed.
   Global Instance big_sepM_mono' m :
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))
-           (uPred_big_sepM (M:=M) m).
-  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed.
+           (big_opM (M:=uPredUR M) m).
+  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_sepM_empty Φ : ([★ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True.
-  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
+  Proof. by rewrite big_opM_empty. Qed.
 
   Lemma big_sepM_insert Φ m i x :
     m !! i = None →
     ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ m, Φ k y.
-  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
+  Proof. apply: big_opM_insert. Qed.
 
   Lemma big_sepM_delete Φ m i x :
     m !! i = Some x →
     ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y.
-  Proof.
-    intros. rewrite -big_sepM_insert ?lookup_delete //.
-    by rewrite insert_delete insert_id.
-  Qed.
+  Proof. apply: big_opM_delete. Qed.
 
   Lemma big_sepM_lookup Φ m i x :
     m !! i = Some x → ([★ map] k↦y ∈ m, Φ k y) ⊢ Φ i x.
-  Proof. intros. by rewrite big_sepM_delete // sep_elim_l. Qed.
+  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. 
 
   Lemma big_sepM_singleton Φ i x : ([★ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
-  Proof.
-    rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
-    by rewrite big_sepM_empty right_id.
-  Qed.
+  Proof. by rewrite big_opM_singleton. Qed.
 
   Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → uPred M) m :
     ([★ map] k↦y ∈ f <$> m, Φ k y) ⊣⊢ ([★ map] k↦y ∈ m, Φ k (f y)).
-  Proof.
-    rewrite /uPred_big_sepM map_to_list_fmap -list_fmap_compose.
-    f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
-  Qed.
+  Proof. by rewrite big_opM_fmap. Qed.
 
   Lemma big_sepM_insert_override (Φ : K → uPred M) m i x y :
     m !! i = Some x →
     ([★ map] k↦_ ∈ <[i:=y]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k).
-  Proof.
-    intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
-    by rewrite -big_sepM_delete.
-  Qed.
+  Proof. apply: big_opM_insert_override. Qed.
 
   Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b :
     m !! i = None →
        ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     ⊣⊢ (Ψ i x b ★ [★ map] k↦y ∈ m, Ψ k y (f k)).
-  Proof.
-    intros. rewrite big_sepM_insert // fn_lookup_insert.
-    apply sep_proper, big_sepM_proper; auto=> k y ?.
-    by rewrite fn_lookup_insert_ne; last set_solver.
-  Qed.
+  Proof. apply: big_opM_fn_insert. Qed.
+
   Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P :
     m !! i = None →
     ([★ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k).
-  Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.
+  Proof. apply: big_opM_fn_insert'. Qed.
 
   Lemma big_sepM_sepM Φ Ψ m :
        ([★ map] k↦x ∈ m, Φ k x ★ Ψ k x)
     ⊣⊢ ([★ 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 ?right_id //.
-    by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc.
-  Qed.
-
-  Lemma big_sepM_commute (Ψ: uPred M → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} Φ m :
-    Ψ True ⊣⊢ True →
-    (∀ P Q, Ψ (P ★ Q) ⊣⊢ Ψ P ★ Ψ Q) →
-    Ψ ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, Ψ (Φ k x)).
-  Proof.
-    intros ??. rewrite /uPred_big_sepM.
-    induction (map_to_list m) as [|[i x] l IH]; rewrite //= -?IH; auto.
-  Qed.
-  Lemma big_sepM_op_commute {B : ucmraT}
-      (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : K → A → B) m :
-    Ψ ∅ ⊣⊢ True →
-    (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) →
-    Ψ ([⋅ map] k↦x ∈ m, f k x) ⊣⊢ ([★ map] k↦x ∈ m, Ψ (f k x)).
-  Proof.
-    intros ??. rewrite /big_opM /uPred_big_sepM.
-    induction (map_to_list m) as [|[i x] l IH]; rewrite //= -?IH; auto.
-  Qed.
-  Lemma big_sepM_op_commute1 {B : ucmraT}
-      (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : K → A → B) m :
-    (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) →
-    m ≠ ∅ →
-    Ψ ([⋅ map] k↦x ∈ m, f k x) ⊣⊢ ([★ map] k↦x ∈ m, Ψ (f k x)).
-  Proof.
-    rewrite -map_to_list_empty'. intros ??. rewrite /big_opM /uPred_big_sepM.
-    induction (map_to_list m) as [|[i x] [|i' x'] IH];
-      csimpl in *; rewrite ?right_id -?IH //.
-  Qed.
+  Proof. apply: big_opM_opM. Qed.
 
   Lemma big_sepM_later Φ m :
     ▷ ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x).
-  Proof. apply (big_sepM_commute _); auto using later_True, later_sep. Qed.
+  Proof. apply (big_opM_commute _). apply later_True. apply later_sep. Qed.
 
   Lemma big_sepM_always Φ m :
     (□ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □ Φ k x).
-  Proof. apply (big_sepM_commute _); auto using always_pure, always_sep. Qed.
+  Proof. apply (big_opM_commute _). apply always_pure. apply always_sep. Qed.
 
   Lemma big_sepM_always_if p Φ m :
     □?p ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x).
@@ -462,14 +294,14 @@ Section gmap.
     intros. apply (anti_symm _).
     { apply forall_intro=> k; apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
-    rewrite /uPred_big_sepM. setoid_rewrite <-elem_of_map_to_list.
-    induction (map_to_list m) as [|[i x] l IH]; csimpl; auto.
-    rewrite -always_and_sep_l; apply and_intro.
-    - rewrite (forall_elim i) (forall_elim x) pure_equiv; last by left.
-      by rewrite True_impl.
+    induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
+    rewrite big_sepM_insert // -always_and_sep_l. apply and_intro.
+    - rewrite (forall_elim i) (forall_elim x) lookup_insert.
+      by rewrite pure_equiv // True_impl.
     - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
-      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
-      by rewrite True_impl.
+      apply impl_intro_l, pure_elim_l=> ?.
+      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
+      by rewrite pure_equiv // True_impl.
   Qed.
 
   Lemma big_sepM_impl Φ Ψ m :
@@ -484,14 +316,13 @@ Section gmap.
 
   Global Instance big_sepM_empty_persistent Φ :
     PersistentP ([★ map] k↦x ∈ ∅, Φ k x).
-  Proof. rewrite /uPred_big_sepM map_to_list_empty. apply _. Qed.
+  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_persistent Φ m :
     (∀ k x, PersistentP (Φ k x)) → PersistentP ([★ map] k↦x ∈ m, Φ k x).
   Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
-
   Global Instance big_sepM_nil_timeless Φ :
     TimelessP ([★ map] k↦x ∈ ∅, Φ k x).
-  Proof. rewrite /uPred_big_sepM map_to_list_empty. apply _. Qed.
+  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_timeless Φ m :
     (∀ k x, TimelessP (Φ k x)) → TimelessP ([★ map] k↦x ∈ m, Φ k x).
   Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
@@ -509,104 +340,56 @@ Section gset.
     ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ Y, Ψ x.
   Proof.
     intros HX HΦ. trans ([★ set] x ∈ Y, Φ x)%I.
-    - by apply big_sep_contains, fmap_contains, elements_contains.
-    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
-      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
+    - apply uPred_included. apply: big_op_contains.
+      by apply fmap_contains, elements_contains.
+    - apply big_opS_forall; apply _ || auto.
   Qed.
+
+  Lemma big_sepS_mono' X :
+     Proper (pointwise_relation _ (⊢) ==> (⊢)) (big_opS (M:=uPredUR M) X).
+  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
+
   Lemma big_sepS_proper Φ Ψ X Y :
     X ≡ Y → (∀ x, x ∈ X → x ∈ Y → Φ x ⊣⊢ Ψ x) →
     ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ Y, Ψ x).
-  Proof.
-    move=> /collection_equiv_spec [??] ?; apply (anti_symm (⊢));
-      apply big_sepS_mono; eauto using equiv_entails, equiv_entails_sym.
-  Qed.
-
-  Lemma big_sepS_ne X n :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
-  Proof.
-    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
-    apply Forall_Forall2, Forall_true=> x; apply HΦ.
-  Qed.
-  Lemma big_sepS_proper' X :
-    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (uPred_big_sepS (M:=M) X).
-  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed.
-  Lemma big_sepS_mono' X :
-    Proper (pointwise_relation _ (⊢) ==> (⊢)) (uPred_big_sepS (M:=M) X).
-  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
+  Proof. apply: big_opS_proper. Qed.
 
   Lemma big_sepS_empty Φ : ([★ set] x ∈ ∅, Φ x) ⊣⊢ True.
-  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
+  Proof. by rewrite big_opS_empty. Qed.
 
   Lemma big_sepS_insert Φ X x :
     x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X, Φ y).
-  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
+  Proof. apply: big_opS_insert. Qed.
+
   Lemma big_sepS_fn_insert {B} (Ψ : A → B → uPred M) f X x b :
     x ∉ X →
        ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y))
     ⊣⊢ (Ψ x b ★ [★ set] y ∈ X, Ψ y (f y)).
-  Proof.
-    intros. rewrite big_sepS_insert // fn_lookup_insert.
-    apply sep_proper, big_sepS_proper; auto=> y ??.
-    by rewrite fn_lookup_insert_ne; last set_solver.
-  Qed.
+  Proof. apply: big_opS_fn_insert. Qed.
+
   Lemma big_sepS_fn_insert' Φ X x P :
     x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ★ [★ set] y ∈ X, Φ y).
-  Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
+  Proof. apply: big_opS_fn_insert'. Qed.
 
   Lemma big_sepS_delete Φ X x :
     x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y.
-  Proof.
-    intros. rewrite -big_sepS_insert; last set_solver.
-    by rewrite -union_difference_L; last set_solver.
-  Qed.
+  Proof. apply: big_opS_delete. Qed.
 
   Lemma big_sepS_elem_of Φ X x : x ∈ X → ([★ set] y ∈ X, Φ y) ⊢ Φ x.
-  Proof. intros. by rewrite big_sepS_delete // sep_elim_l. Qed.
+  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. 
 
   Lemma big_sepS_singleton Φ x : ([★ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
-  Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
+  Proof. apply: big_opS_singleton. Qed.
 
   Lemma big_sepS_sepS Φ Ψ X :
     ([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ ([★ set] y ∈ X, Φ y) ★ ([★ set] y ∈ X, Ψ y).
-  Proof.
-    rewrite /uPred_big_sepS.
-    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
-    by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc.
-  Qed.
-
-  Lemma big_sepS_commute (Ψ: uPred M → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} Φ X :
-    Ψ True ⊣⊢ True →
-    (∀ P Q, Ψ (P ★ Q) ⊣⊢ Ψ P ★ Ψ Q) →
-    Ψ ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ X, Ψ (Φ x)).
-  Proof.
-    intros ??. rewrite /uPred_big_sepS.
-    induction (elements X) as [|x l IH]; rewrite //= -?IH; auto.
-  Qed.
-  Lemma big_sepS_op_commute {B : ucmraT}
-      (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : A → B) X :
-    Ψ ∅ ⊣⊢ True →
-    (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) →
-    Ψ ([⋅ set] x ∈ X, f x) ⊣⊢ ([★ set] x ∈ X, Ψ (f x)).
-  Proof.
-    intros ??. rewrite /big_opS /uPred_big_sepS.
-    induction (elements X) as [|x l IH]; rewrite //= -?IH; auto.
-  Qed.
-  Lemma big_sepS_op_commute1 {B : ucmraT}
-      (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : A → B) X :
-    (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) →
-    X ≢ ∅ →
-    Ψ ([⋅ set] x ∈ X, f x) ⊣⊢ ([★ set] x ∈ X, Ψ (f x)).
-  Proof.
-    rewrite -elements_empty'. intros ??. rewrite /big_opS /uPred_big_sepS.
-    induction (elements X) as [|x [|x' l] IH];
-      csimpl in *; rewrite ?right_id -?IH //.
-  Qed.
+  Proof. apply: big_opS_opS. Qed.
 
   Lemma big_sepS_later Φ X : ▷ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y).
-  Proof. apply (big_sepS_commute _); auto using later_True, later_sep. Qed.
+  Proof. apply (big_opS_commute _). apply later_True. apply later_sep. Qed.
 
   Lemma big_sepS_always Φ X : □ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y).
-  Proof. apply (big_sepS_commute _); auto using always_pure, always_sep. Qed.
+  Proof. apply (big_opS_commute _). apply always_pure. apply always_sep. Qed.
 
   Lemma big_sepS_always_if q Φ X :
     □?q ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y).
@@ -618,13 +401,12 @@ Section gset.
     intros. apply (anti_symm _).
     { apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
-    rewrite /uPred_big_sepS. setoid_rewrite <-elem_of_elements.
-    induction (elements X) as [|x l IH]; csimpl; auto.
-    rewrite -always_and_sep_l; apply and_intro.
-    - rewrite (forall_elim x) pure_equiv; last by left. by rewrite True_impl.
-    - rewrite -IH. apply forall_mono=> y.
-      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
-      by rewrite True_impl.
+    induction X as [|x m ? IH] using collection_ind_L.
+    { rewrite big_sepS_empty; auto. }
+    rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
+    - by rewrite (forall_elim x) pure_equiv ?True_impl; last set_solver.
+    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
+      by rewrite pure_equiv ?True_impl; last set_solver.
   Qed.
 
   Lemma big_sepS_impl Φ Ψ X :
@@ -637,15 +419,14 @@ Section gset.
   Qed.
 
   Global Instance big_sepS_empty_persistent Φ : PersistentP ([★ set] x ∈ ∅, Φ x).
-  Proof. rewrite /uPred_big_sepS elements_empty. apply _. Qed.
+  Proof. rewrite /big_opS elements_empty. apply _. Qed.
   Global Instance big_sepS_persistent Φ X :
     (∀ x, PersistentP (Φ x)) → PersistentP ([★ set] x ∈ X, Φ x).
-  Proof. rewrite /uPred_big_sepS. apply _. Qed.
-
+  Proof. rewrite /big_opS. apply _. Qed.
   Global Instance big_sepS_nil_timeless Φ : TimelessP ([★ set] x ∈ ∅, Φ x).
-  Proof. rewrite /uPred_big_sepS elements_empty. apply _. Qed.
+  Proof. rewrite /big_opS elements_empty. apply _. Qed.
   Global Instance big_sepS_timeless Φ X :
     (∀ x, TimelessP (Φ x)) → TimelessP ([★ set] x ∈ X, Φ x).
-  Proof. rewrite /uPred_big_sepS. apply _. Qed.
+  Proof. rewrite /big_opS. apply _. Qed.
 End gset.
 End big_op.

program_logic/pviewshifts.v

@@ -126,15 +126,13 @@ Proof. by rewrite pvs_frame_r pvs_frame_l pvs_trans. Qed.
 Lemma pvs_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Σ) (m : gmap K A) :
   ([★ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=> [★ map] k↦x ∈ m, Φ k x.
 Proof.
-  rewrite /uPred_big_sepM.
-  induction (map_to_list m) as [|[i x] l IH]; csimpl; auto using pvs_intro.
-  by rewrite IH pvs_sep.
+  apply (big_opM_forall (λ P Q, P ={E}=> Q)); auto using pvs_intro.
+  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
 Qed.
 Lemma pvs_big_sepS `{Countable A} E (Φ : A → iProp Σ) X :
   ([★ set] x ∈ X, |={E}=> Φ x) ={E}=> [★ set] x ∈ X, Φ x.
 Proof.
-  rewrite /uPred_big_sepS.
-  induction (elements X) as [|x l IH]; csimpl; csimpl; auto using pvs_intro.
-  by rewrite IH pvs_sep.
+  apply (big_opS_forall (λ P Q, P ={E}=> Q)); auto using pvs_intro.
+  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
 Qed.
 End pvs.

program_logic/weakestpre.v

@@ -24,7 +24,7 @@ Proof.
   apply pvs_ne, sep_ne, later_contractive; auto=> i ?.
   apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> efs.
   apply wand_ne, pvs_ne, sep_ne, sep_ne; auto; first by apply Hwp.
-  apply big_sepL_ne=> ? ef. by apply Hwp.
+  apply big_opL_ne=> ? ef. by apply Hwp.
 Qed.
 
 Definition wp_def `{irisG Λ Σ} :

proofmode/coq_tactics.v

@@ -426,8 +426,8 @@ Proof.
   repeat apply sep_mono; try apply always_mono.
   - rewrite -later_intro; apply pure_mono; destruct 1; constructor;
       naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
-  - induction Hp; rewrite /= ?later_sep; auto using sep_mono, later_intro.
-  - induction Hs; rewrite /= ?later_sep; auto using sep_mono, later_intro.
+  - induction Hp; rewrite /= ?later_sep. apply later_intro. by apply sep_mono.
+  - induction Hs; rewrite /= ?later_sep. apply later_intro. by apply sep_mono.
 Qed.
 
 Lemma tac_next Δ Δ' Q Q' :