seal big_opM, big_opS, big_opMS and big_sepM2

theories/algebra/big_op.v

@@ -35,11 +35,13 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
   (at level 200, o at level 1, l at level 10, x at level 1, right associativity,
    format "[^ o  list]  x  ∈  l ,  P") : stdpp_scope.
 
-Definition big_opM `{Monoid M o} `{Countable K} {A} (f : K → A → M)
-    (m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
+Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K → A → M)
+  (m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
+Definition big_opM_aux : seal (@big_opM_def). by eexists. Qed.
+Definition big_opM := big_opM_aux.(unseal).
+Arguments big_opM {M} o {_ K _ _ A} _ _.
+Definition big_opM_eq : @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
 Instance: Params (@big_opM) 7 := {}.
-Arguments big_opM {M} o {_ K _ _ A} _ _ : simpl never.
-Typeclasses Opaque big_opM.
 Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
   (at level 200, o at level 1, m at level 10, k, x at level 1, right associativity,
    format "[^  o  map]  k ↦ x  ∈  m ,  P") : stdpp_scope.
@@ -47,20 +49,24 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
   (at level 200, o at level 1, m at level 10, x at level 1, right associativity,
    format "[^ o  map]  x  ∈  m ,  P") : stdpp_scope.
 
-Definition big_opS `{Monoid M o} `{Countable A} (f : A → M)
+Definition big_opS_def `{Monoid M o} `{Countable A} (f : A → M)
   (X : gset A) : M := big_opL o (λ _, f) (elements X).
+Definition big_opS_aux : seal (@big_opS_def). by eexists. Qed.
+Definition big_opS := big_opS_aux.(unseal).
+Arguments big_opS {M} o {_ A _ _} _ _.
+Definition big_opS_eq : @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
 Instance: Params (@big_opS) 6 := {}.
-Arguments big_opS {M} o {_ A _ _} _ _ : simpl never.
-Typeclasses Opaque big_opS.
 Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
   (at level 200, o at level 1, X at level 10, x at level 1, right associativity,
    format "[^ o  set]  x  ∈  X ,  P") : stdpp_scope.
 
-Definition big_opMS `{Monoid M o} `{Countable A} (f : A → M)
+Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A → M)
   (X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
-Instance: Params (@big_opMS) 7 := {}.
-Arguments big_opMS {M} o {_ A _ _} _ _ : simpl never.
-Typeclasses Opaque big_opMS.
+Definition big_opMS_aux : seal (@big_opMS_def). by eexists. Qed.
+Definition big_opMS := big_opMS_aux.(unseal).
+Arguments big_opMS {M} o {_ A _ _} _ _.
+Definition big_opMS_eq : @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
+Instance: Params (@big_opMS) 6 := {}.
 Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
   (at level 200, o at level 1, X at level 10, x at level 1, right associativity,
    format "[^ o  mset]  x  ∈  X ,  P") : stdpp_scope.
@@ -171,7 +177,7 @@ Section gmap.
     (∀ k x, m !! k = Some x → R (f k x) (g k x)) →
     R ([^o map] k ↦ x ∈ m, f k x) ([^o map] k ↦ x ∈ m, g k x).
   Proof.
-    intros ?? Hf. apply (big_opL_forall R); auto.
+    intros ?? Hf. rewrite big_opM_eq. apply (big_opL_forall R); auto.
     intros k [i x] ?%elem_of_list_lookup_2. by apply Hf, elem_of_map_to_list.
   Qed.
 
@@ -194,12 +200,12 @@ Section gmap.
   Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_opM_empty f : ([^o map] k↦x ∈ ∅, f k x) = monoid_unit.
-  Proof. by rewrite /big_opM map_to_list_empty. Qed.
+  Proof. by rewrite big_opM_eq /big_opM_def map_to_list_empty. Qed.
 
   Lemma big_opM_insert f m i x :
     m !! i = None →
     ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ m, f k y.
-  Proof. intros ?. by rewrite /big_opM map_to_list_insert. Qed.
+  Proof. intros ?. by rewrite big_opM_eq /big_opM_def map_to_list_insert. Qed.
 
   Lemma big_opM_delete f m i x :
     m !! i = Some x →
@@ -216,12 +222,12 @@ Section gmap.
   Qed.
 
   Lemma big_opM_unit m : ([^o map] k↦y ∈ m, monoid_unit) ≡ (monoid_unit : M).
-  Proof. induction m using map_ind; rewrite /= ?big_opM_insert ?left_id //. Qed.
+  Proof. by induction m using map_ind; rewrite /= ?big_opM_insert ?left_id // big_opM_eq. Qed.
 
   Lemma big_opM_fmap {B} (h : A → B) (f : K → B → M) m :
     ([^o map] k↦y ∈ h <$> m, f k y) ≡ ([^o map] k↦y ∈ m, f k (h y)).
   Proof.
-    rewrite /big_opM map_to_list_fmap big_opL_fmap.
+    rewrite big_opM_eq /big_opM_def map_to_list_fmap big_opL_fmap.
     by apply big_opL_proper=> ? [??].
   Qed.
 
@@ -262,7 +268,7 @@ Section gmap.
   Lemma big_opM_op f g m :
     ([^o map] k↦x ∈ m, f k x `o` g k x)
     ≡ ([^o map] k↦x ∈ m, f k x) `o` ([^o map] k↦x ∈ m, g k x).
-  Proof. rewrite /big_opM -big_opL_op. by apply big_opL_proper=> ? [??]. Qed.
+  Proof. rewrite big_opM_eq /big_opM_def -big_opL_op. by apply big_opL_proper=> ? [??]. Qed.
 End gmap.
 
 
@@ -277,7 +283,7 @@ Section gset.
     (∀ x, x ∈ X → R (f x) (g x)) →
     R ([^o set] x ∈ X, f x) ([^o set] x ∈ X, g x).
   Proof.
-    intros ?? Hf. apply (big_opL_forall R); auto.
+    rewrite big_opS_eq. intros ?? Hf. apply (big_opL_forall R); auto.
     intros k x ?%elem_of_list_lookup_2. by apply Hf, elem_of_elements.
   Qed.
 
@@ -298,11 +304,11 @@ Section gset.
   Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_opS_empty f : ([^o set] x ∈ ∅, f x) = monoid_unit.
-  Proof. by rewrite /big_opS elements_empty. Qed.
+  Proof. by rewrite big_opS_eq /big_opS_def elements_empty. Qed.
 
   Lemma big_opS_insert f X x :
     x ∉ X → ([^o set] y ∈ {[ x ]} ∪ X, f y) ≡ (f x `o` [^o set] y ∈ X, f y).
-  Proof. intros. by rewrite /big_opS elements_union_singleton. Qed.
+  Proof. intros. by rewrite big_opS_eq /big_opS_def elements_union_singleton. Qed.
   Lemma big_opS_fn_insert {B} (f : A → B → M) h X x b :
     x ∉ X →
     ([^o set] y ∈ {[ x ]} ∪ X, f y (<[x:=b]> h y))
@@ -334,22 +340,22 @@ Section gset.
   Qed.
 
   Lemma big_opS_singleton f x : ([^o set] y ∈ {[ x ]}, f y) ≡ f x.
-  Proof. intros. by rewrite /big_opS elements_singleton /= right_id. Qed.
+  Proof. intros. by rewrite big_opS_eq /big_opS_def elements_singleton /= right_id. Qed.
 
   Lemma big_opS_unit X : ([^o set] y ∈ X, monoid_unit) ≡ (monoid_unit : M).
   Proof.
-    induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id //.
+    by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_eq.
   Qed.
 
   Lemma big_opS_op f g X :
     ([^o set] y ∈ X, f y `o` g y) ≡ ([^o set] y ∈ X, f y) `o` ([^o set] y ∈ X, g y).
-  Proof. by rewrite /big_opS -big_opL_op. Qed.
+  Proof. by rewrite big_opS_eq /big_opS_def -big_opL_op. Qed.
 End gset.
 
 Lemma big_opM_dom `{Countable K} {A} (f : K → M) (m : gmap K A) :
   ([^o map] k↦_ ∈ m, f k) ≡ ([^o set] k ∈ dom _ m, f k).
 Proof.
-  induction m as [|i x ?? IH] using map_ind; [by rewrite dom_empty_L|].
+  induction m as [|i x ?? IH] using map_ind; [by rewrite big_opM_eq big_opS_eq dom_empty_L|].
   by rewrite dom_insert_L big_opM_insert // IH big_opS_insert ?not_elem_of_dom.
 Qed.
 
@@ -364,7 +370,7 @@ Section gmultiset.
     (∀ x, x ∈ X → R (f x) (g x)) →
     R ([^o mset] x ∈ X, f x) ([^o mset] x ∈ X, g x).
   Proof.
-    intros ?? Hf. apply (big_opL_forall R); auto.
+    rewrite big_opMS_eq. intros ?? Hf. apply (big_opL_forall R); auto.
     intros k x ?%elem_of_list_lookup_2. by apply Hf, gmultiset_elem_of_elements.
   Qed.
 
@@ -385,15 +391,15 @@ Section gmultiset.
   Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_opMS_empty f : ([^o mset] x ∈ ∅, f x) = monoid_unit.
-  Proof. by rewrite /big_opMS gmultiset_elements_empty. Qed.
+  Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. Qed.
 
   Lemma big_opMS_disj_union f X Y :
     ([^o mset] y ∈ X ⊎ Y, f y) ≡ ([^o mset] y ∈ X, f y) `o` [^o mset] y ∈ Y, f y.
-  Proof. by rewrite /big_opMS gmultiset_elements_disj_union big_opL_app. Qed.
+  Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
 
   Lemma big_opMS_singleton f x : ([^o mset] y ∈ {[ x ]}, f y) ≡ f x.
   Proof.
-    intros. by rewrite /big_opMS gmultiset_elements_singleton /= right_id.
+    intros. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_singleton /= right_id.
   Qed.
 
   Lemma big_opMS_delete f X x :
@@ -405,13 +411,13 @@ Section gmultiset.
 
   Lemma big_opMS_unit X : ([^o mset] y ∈ X, monoid_unit) ≡ (monoid_unit : M).
   Proof.
-    induction X using gmultiset_ind;
-      rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id //.
+    by induction X using gmultiset_ind;
+      rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id // big_opMS_eq.
   Qed.
 
   Lemma big_opMS_op f g X :
     ([^o mset] y ∈ X, f y `o` g y) ≡ ([^o mset] y ∈ X, f y) `o` ([^o mset] y ∈ X, g y).
-  Proof. by rewrite /big_opMS -big_opL_op. Qed.
+  Proof. by rewrite big_opMS_eq /big_opMS_def -big_opL_op. Qed.
 End gmultiset.
 End big_op.
 

theories/algebra/cmra_big_op.v

@@ -13,7 +13,7 @@ Qed.
 Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K → A → option M) m :
   ([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
 Proof.
-  induction m as [|i x m ? IH] using map_ind=> //=.
+  induction m as [|i x m ? IH] using map_ind=> /=; first by rewrite big_opM_eq.
   rewrite -equiv_None big_opM_insert // equiv_None op_None IH. split.
   { intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
   intros Hm; split.
@@ -23,7 +23,7 @@ Qed.
 Lemma big_opS_None {M : cmraT} `{Countable A} (f : A → option M) X :
   ([^op set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
 Proof.
-  induction X as [|x X ? IH] using set_ind_L; [done|].
+  induction X as [|x X ? IH] using set_ind_L; [by rewrite big_opS_eq |].
   rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver.
 Qed.
 Lemma big_opMS_None {M : cmraT} `{Countable A} (f : A → option M) X :

theories/base_logic/lib/boxes.v

@@ -100,7 +100,7 @@ Qed.
 
 Lemma box_alloc : box N ∅ True%I.
 Proof.
-  iIntros. iExists (λ _, True)%I. iSplit; by auto.
+  iIntros. iExists (λ _, True)%I. by rewrite !big_opM_empty.
 Qed.
 
 Lemma slice_insert_empty E q f Q P :

theories/bi/big_op.v

@@ -50,12 +50,15 @@ Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
 Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" :=
   (big_sepL2 (λ _ x1 x2, P) l1 l2) : bi_scope.
 
-Definition big_sepM2 {PROP : bi} `{Countable K} {A B}
+Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
     (Φ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : PROP :=
   (⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝ ∧
    [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2)%I.
+Definition big_sepM2_aux : seal (@big_sepM2_def). by eexists. Qed.
+Definition big_sepM2 := big_sepM2_aux.(unseal).
+Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
+Definition big_sepM2_eq : @big_sepM2 = @big_sepM2_def := big_sepM2_aux.(seal_eq).
 Instance: Params (@big_sepM2) 6 := {}.
-Typeclasses Opaque big_sepM2.
 Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
   (big_sepM2 (λ k x1 x2, P) m1 m2) : bi_scope.
 Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P" :=
@@ -687,7 +690,7 @@ Section map.
   Proof. apply big_opM_proper. Qed.
   Lemma big_sepM_subseteq `{BiAffine PROP} Φ m1 m2 :
     m2 ⊆ m1 → ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Φ k x.
-  Proof. intros. by apply big_sepL_submseteq, map_to_list_submseteq. Qed.
+  Proof. rewrite big_opM_eq. intros. by apply big_sepL_submseteq, map_to_list_submseteq. Qed.
 
   Global Instance big_sepM_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
@@ -834,7 +837,7 @@ Section map.
     [∗ map] k↦x ∈ m, Ψ k x.
   Proof.
     apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
-    { by rewrite sep_elim_r. }
+    { by rewrite big_opM_eq sep_elim_r. }
     rewrite !big_sepM_insert // intuitionistically_sep_dup.
     rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
     - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
@@ -848,17 +851,17 @@ Section map.
 
   Global Instance big_sepM_empty_persistent Φ :
     Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
-  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
+  Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_persistent Φ m :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x).
-  Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
+  Proof. rewrite big_opM_eq. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
 
   Global Instance big_sepM_empty_affine Φ :
     Affine ([∗ map] k↦x ∈ ∅, Φ k x).
-  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
+  Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_affine Φ m :
     (∀ k x, Affine (Φ k x)) → Affine ([∗ map] k↦x ∈ m, Φ k x).
-  Proof. intros. apply big_sepL_affine=> _ [??]; apply _. Qed.
+  Proof. rewrite big_opM_eq. intros. apply big_sepL_affine=> _ [??]; apply _. Qed.
 End map.
 
 (** ** Big ops over two maps *)
@@ -869,7 +872,7 @@ Section map2.
   Lemma big_sepM2_dom Φ m1 m2 :
     ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) -∗ ⌜ dom (gset K) m1 = dom (gset K) m2 ⌝.
   Proof.
-    rewrite /big_sepM2 and_elim_l. apply pure_mono=>Hm.
+    rewrite big_sepM2_eq /big_sepM2_def and_elim_l. apply pure_mono=>Hm.
     set_unfold=>k. by rewrite !elem_of_dom.
   Qed.
 
@@ -877,7 +880,8 @@ Section map2.
     (∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → Φ k y1 y2 ⊢ Ψ k y1 y2) →
     ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢ [∗ map] k ↦ y1;y2 ∈ m1;m2, Ψ k y1 y2.
   Proof.
-    intros Hm1m2. rewrite /big_sepM2. apply and_mono_r, big_sepM_mono.
+    intros Hm1m2. rewrite big_sepM2_eq /big_sepM2_def.
+    apply and_mono_r, big_sepM_mono.
     intros k [x1 x2]. rewrite map_lookup_zip_with.
     specialize (Hm1m2 k x1 x2).
     destruct (m1 !! k) as [y1|]; last done.
@@ -897,8 +901,8 @@ Section map2.
       ==> (=) ==> (=) ==> (dist n))
            (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
   Proof.
-    intros Φ1 Φ2 HΦ x1 ? <- x2 ? <-. rewrite /big_sepM2. f_equiv.
-    f_equiv=> k [y1 y2]. apply HΦ.
+    intros Φ1 Φ2 HΦ x1 ? <- x2 ? <-. rewrite big_sepM2_eq /big_sepM2_def.
+    f_equiv. f_equiv=> k [y1 y2]. apply HΦ.
   Qed.
   Global Instance big_sepM2_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢)))
@@ -913,7 +917,7 @@ Section map2.
 
   Lemma big_sepM2_empty Φ : ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2) ⊣⊢ emp.
   Proof.
-    rewrite /big_sepM2 pure_True ?left_id //.
+    rewrite big_sepM2_eq /big_sepM2_def big_opM_eq pure_True ?left_id //.
     intros k. rewrite !lookup_empty; split; by inversion 1.
   Qed.
   Lemma big_sepM2_empty' `{BiAffine PROP} P Φ : P ⊢ [∗ map] k↦y1;y2 ∈ ∅;∅, Φ k y1 y2.
@@ -938,7 +942,7 @@ Section map2.
     ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
     ⊣⊢ Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2.
   Proof.
-    intros Hm1 Hm2. rewrite /big_sepM2 -map_insert_zip_with.
+    intros Hm1 Hm2. rewrite big_sepM2_eq /big_sepM2_def -map_insert_zip_with.
     rewrite big_sepM_insert;
       last by rewrite map_lookup_zip_with Hm1.
     rewrite !persistent_and_affinely_sep_l /=.
@@ -959,7 +963,7 @@ Section map2.
     ([∗ map] k↦x;y ∈ m1;m2, Φ k x y) ⊣⊢
       Φ i x1 x2 ∗ [∗ map] k↦x;y ∈ delete i m1;delete i m2, Φ k x y.
   Proof.
-    rewrite /big_sepM2 => Hx1 Hx2.
+    rewrite big_sepM2_eq /big_sepM2_def => Hx1 Hx2.
     rewrite !persistent_and_affinely_sep_l /=.
     rewrite sep_assoc (sep_comm  (Φ _ _ _)) -sep_assoc.
     apply sep_proper.
@@ -993,7 +997,7 @@ Section map2.
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) -∗
     ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2).
   Proof.
-    intros Ha. rewrite /big_sepM2.
+    intros Ha. rewrite big_sepM2_eq /big_sepM2_def.
     assert (TCOr (∀ x, Affine (Φ i x.1 x.2)) (Absorbing (Φ i x1 x2))).
     { destruct Ha; try apply _. }
     apply wand_intro_r.
@@ -1027,7 +1031,7 @@ Section map2.
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
     ⊢ ∃ x2, ⌜m2 !! i = Some x2⌝ ∧ Φ i x1 x2.
   Proof.
-    intros Hm1. rewrite /big_sepM2.
+    intros Hm1. rewrite big_sepM2_eq /big_sepM2_def.
     rewrite persistent_and_sep_1.
     apply wand_elim_l'. apply pure_elim'=>Hm.
     assert (is_Some (m2 !! i)) as [x2 Hm2].
@@ -1044,7 +1048,7 @@ Section map2.
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
     ⊢ ∃ x1, ⌜m1 !! i = Some x1⌝ ∧ Φ i x1 x2.
   Proof.
-    intros Hm2. rewrite /big_sepM2.
+    intros Hm2. rewrite big_sepM2_eq /big_sepM2_def.
     rewrite persistent_and_sep_1.
     apply wand_elim_l'. apply pure_elim'=>Hm.
     assert (is_Some (m1 !! i)) as [x1 Hm1].
@@ -1059,7 +1063,8 @@ Section map2.
   Lemma big_sepM2_singleton Φ i x1 x2 :
     ([∗ map] k↦y1;y2 ∈ {[ i := x1 ]}; {[ i := x2 ]}, Φ k y1 y2) ⊣⊢ Φ i x1 x2.
   Proof.
-    rewrite /big_sepM2 map_zip_with_singleton big_sepM_singleton.
+    rewrite big_sepM2_eq /big_sepM2_def.
+    rewrite map_zip_with_singleton big_sepM_singleton.
     apply (anti_symm _).
     - apply and_elim_r.
     - rewrite <- (left_id True%I (∧)%I (Φ i x1 x2)).
@@ -1072,7 +1077,7 @@ Section map2.
     ([∗ map] k↦y1;y2 ∈ f <$> m1; g <$> m2, Φ k y1 y2)
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k (f y1) (g y2)).
   Proof.
-    rewrite /big_sepM2. rewrite map_fmap_zip.
+    rewrite big_sepM2_eq /big_sepM2_def. rewrite map_fmap_zip.
     apply and_proper.
     - apply pure_proper. split.
       + intros Hm k. specialize (Hm k). revert Hm.
@@ -1096,7 +1101,7 @@ Section map2.
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2 ∗ Ψ k y1 y2)
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2).
   Proof.
-    rewrite /big_sepM2.
+    rewrite big_sepM2_eq /big_sepM2_def.
     rewrite -{1}(and_idem ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)⌝%I).
     rewrite -and_assoc.
     rewrite !persistent_and_affinely_sep_l /=.
@@ -1114,7 +1119,7 @@ Section map2.
     <pers> ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
     ⊣⊢ [∗ map] k↦y1;y2 ∈ m1;m2, <pers> (Φ k y1 y2).
   Proof.
-    by rewrite /big_sepM2 persistently_and
+    by rewrite big_sepM2_eq /big_sepM2_def persistently_and
          persistently_pure big_sepM_persistently.
   Qed.
 
@@ -1124,7 +1129,7 @@ Section map2.
      ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)⌝
      ∧ (∀ k x1 x2, ⌜m1 !! k = Some x1⌝ → ⌜m2 !! k = Some x2⌝ → Φ k x1 x2).
  Proof.
-   rewrite /big_sepM2=> ?. apply and_proper=>//.
+   rewrite big_sepM2_eq /big_sepM2_def=> ?. apply and_proper=>//.
    rewrite big_sepM_forall. apply forall_proper=>k.
    apply (anti_symm _).
    - apply forall_intro=> x1. apply forall_intro=> x2.
@@ -1145,7 +1150,7 @@ Section map2.
     [∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2.
   Proof.
     apply wand_intro_l.
-    rewrite /big_sepM2.
+    rewrite big_sepM2_eq /big_sepM2_def.
     rewrite !persistent_and_affinely_sep_l /=.
     rewrite sep_assoc. rewrite (sep_comm (□ _)%I) -sep_assoc.
     apply sep_mono_r. apply wand_elim_r'.
@@ -1164,7 +1169,7 @@ Section map2.
   Global Instance big_sepM2_persistent Φ m1 m2 :
     (∀ k x1 x2, Persistent (Φ k x1 x2)) →
     Persistent ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
-  Proof. rewrite /big_sepM2. apply _. Qed.
+  Proof. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
 
   Global Instance big_sepM2_empty_affine Φ :
     Affine ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
@@ -1172,7 +1177,7 @@ Section map2.
   Global Instance big_sepM2_affine Φ m1 m2 :
     (∀ k x1 x2, Affine (Φ k x1 x2)) →
     Affine ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
-  Proof. rewrite /big_sepM2. apply _. Qed.
+  Proof. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
 End map2.
 
 (** ** Big ops over finite sets *)
@@ -1191,7 +1196,7 @@ Section gset.
   Proof. apply big_opS_proper. Qed.
   Lemma big_sepS_subseteq `{BiAffine PROP} Φ X Y :
     Y ⊆ X → ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Φ x.
-  Proof. intros. by apply big_sepL_submseteq, elements_submseteq. Qed.
+  Proof. rewrite big_opS_eq. intros. by apply big_sepL_submseteq, elements_submseteq. Qed.
 
   Global Instance big_sepS_mono' :
      Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (@bi_sep PROP) (A:=A)).
@@ -1309,7 +1314,7 @@ Section gset.
     [∗ set] x ∈ X, Ψ x.
   Proof.
     apply wand_intro_l. induction X as [|x X ? IH] using set_ind_L.
-    { by rewrite sep_elim_r. }
+    { by rewrite big_opS_eq sep_elim_r. }
     rewrite !big_sepS_insert // intuitionistically_sep_dup.
     rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
     - rewrite (forall_elim x) pure_True; last set_solver.
@@ -1321,16 +1326,16 @@ Section gset.
 
   Global Instance big_sepS_empty_persistent Φ :
     Persistent ([∗ set] x ∈ ∅, Φ x).
-  Proof. rewrite /big_opS elements_empty. apply _. Qed.
+  Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
   Global Instance big_sepS_persistent Φ X :
     (∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
-  Proof. rewrite /big_opS. apply _. Qed.
+  Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
 
   Global Instance big_sepS_empty_affine Φ : Affine ([∗ set] x ∈ ∅, Φ x).
-  Proof. rewrite /big_opS elements_empty. apply _. Qed.
+  Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
   Global Instance big_sepS_affine Φ X :
     (∀ x, Affine (Φ x)) → Affine ([∗ set] x ∈ X, Φ x).
-  Proof. rewrite /big_opS. apply _. Qed.
+  Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
 End gset.
 
 Lemma big_sepM_dom `{Countable K} {A} (Φ : K → PROP) (m : gmap K A) :
@@ -1353,7 +1358,7 @@ Section gmultiset.
   Proof. apply big_opMS_proper. Qed.
   Lemma big_sepMS_subseteq `{BiAffine PROP} Φ X Y :
     Y ⊆ X → ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Φ x.
-  Proof. intros. by apply big_sepL_submseteq, gmultiset_elements_submseteq. Qed.
+  Proof. rewrite big_opMS_eq. intros. by apply big_sepL_submseteq, gmultiset_elements_submseteq. Qed.
 
   Global Instance big_sepMS_mono' :
      Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opMS (@bi_sep PROP) (A:=A)).
@@ -1400,16 +1405,16 @@ Section gmultiset.
 
   Global Instance big_sepMS_empty_persistent Φ :
     Persistent ([∗ mset] x ∈ ∅, Φ x).
-  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
+  Proof. rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. apply _. Qed.
   Global Instance big_sepMS_persistent Φ X :
     (∀ x, Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
-  Proof. rewrite /big_opMS. apply _. Qed.
+  Proof. rewrite big_opMS_eq /big_opMS_def. apply _. Qed.
 
   Global Instance big_sepMS_empty_affine Φ : Affine ([∗ mset] x ∈ ∅, Φ x).
-  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
+  Proof. rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. apply _. Qed.
   Global Instance big_sepMS_affine Φ X :
     (∀ x, Affine (Φ x)) → Affine ([∗ mset] x ∈ X, Φ x).
-  Proof. rewrite /big_opMS. apply _. Qed.
+  Proof. rewrite big_opMS_eq /big_opMS_def. apply _. Qed.
 End gmultiset.
 End bi_big_op.
 
@@ -1513,10 +1518,10 @@ Section gmap.
 
   Global Instance big_sepM_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
     Timeless ([∗ map] k↦x ∈ ∅, Φ k x).
-  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
+  Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
     (∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x).
-  Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
+  Proof. rewrite big_opM_eq. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
 End gmap.
 
 Section gmap2.
@@ -1527,7 +1532,7 @@ Section gmap2.
     (▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
     ⊢ ◇ ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2).
   Proof.
-    rewrite /big_sepM2 later_and (timeless ⌜_⌝%I).
+    rewrite big_sepM2_eq /big_sepM2_def later_and (timeless ⌜_⌝%I).
     rewrite big_sepM_later except_0_and.
     auto using and_mono_r, except_0_intro.
   Qed.
@@ -1535,7 +1540,7 @@ Section gmap2.
     ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2)
     ⊢ ▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
   Proof.
-    rewrite /big_sepM2 later_and -(later_intro ⌜_⌝%I).
+    rewrite big_sepM2_eq /big_sepM2_def later_and -(later_intro ⌜_⌝%I).
     apply and_mono_r. by rewrite big_opM_commute.
   Qed.
 
@@ -1551,18 +1556,18 @@ Section gmap2.
   Lemma big_sepM2_flip Φ m1 m2 :
     ([∗ map] k↦y1;y2 ∈ m2; m1, Φ k y2 y1) ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2).
   Proof.