Introduce CMRA homomorphisms.

This allows us to factor out properties about connectives that
commute with the big operators.

algebra/auth.v

@@ -189,10 +189,13 @@ Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
 
 Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
-Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
-Proof. by rewrite /op /auth_op /= left_id. Qed.
 Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
 Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
+Global Instance auth_frag_cmra_homomorphism : CMRAHomomorphism (Auth None).
+Proof. done. Qed.
+
+Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
+Proof. by rewrite /op /auth_op /= left_id. Qed.
 Lemma auth_auth_valid a : ✓ a → ✓ (● a).
 Proof. intros; split; simpl; auto using ucmra_unit_leastN. Qed.
 
@@ -246,7 +249,7 @@ Instance auth_map_cmra_monotone {A B : ucmraT} (f : A → B) :
 Proof.
   split; try apply _.
   - intros n [[[a|]|] b]; rewrite /= /cmra_validN /=; try
-      naive_solver eauto using cmra_monotoneN, validN_preserving.
+      naive_solver eauto using cmra_monotoneN, cmra_monotone_validN.
   - by intros [x a] [y b]; rewrite !auth_included /=;
       intros [??]; split; simpl; apply: cmra_monotone.
 Qed.

algebra/cmra.v

@@ -213,12 +213,26 @@ Class CMRADiscrete (A : cmraT) := {
 (** * Morphisms *)
 Class CMRAMonotone {A B : cmraT} (f : A → B) := {
   cmra_monotone_ne n :> Proper (dist n ==> dist n) f;
-  validN_preserving n x : ✓{n} x → ✓{n} f x;
+  cmra_monotone_validN n x : ✓{n} x → ✓{n} f x;
   cmra_monotone x y : x ≼ y → f x ≼ f y
 }.
-Arguments validN_preserving {_ _} _ {_} _ _ _.
+Arguments cmra_monotone_validN {_ _} _ {_} _ _ _.
 Arguments cmra_monotone {_ _} _ {_} _ _ _.
 
+(* Not all intended homomorphisms preserve validity, in particular it does not
+hold for the [ownM] and [own] connectives. *)
+Class CMRAHomomorphism {A B : cmraT} (f : A → B) := {
+  cmra_homomorphism_ne n :> Proper (dist n ==> dist n) f;
+  cmra_homomorphism x y : f (x ⋅ y) ≡ f x ⋅ f y
+}.
+Arguments cmra_homomorphism {_ _} _ _ _ _.
+
+Class UCMRAHomomorphism {A B : ucmraT} (f : A → B) := {
+  ucmra_homomorphism :> CMRAHomomorphism f;
+  ucmra_homomorphism_unit : f ∅ ≡ ∅
+}.
+Arguments ucmra_homomorphism_unit {_ _} _ _.
+
 (** * Properties **)
 Section cmra.
 Context {A : cmraT}.
@@ -631,7 +645,7 @@ Instance cmra_monotone_compose {A B C : cmraT} (f : A → B) (g : B → C) :
 Proof.
   split.
   - apply _. 
-  - move=> n x Hx /=. by apply validN_preserving, validN_preserving.
+  - move=> n x Hx /=. by apply cmra_monotone_validN, cmra_monotone_validN.
   - move=> x y Hxy /=. by apply cmra_monotone, cmra_monotone.
 Qed.
 
@@ -643,10 +657,30 @@ Section cmra_monotone.
     intros [z ->].
     apply cmra_included_includedN, (cmra_monotone f), cmra_included_l.
   Qed.
-  Lemma valid_preserving x : ✓ x → ✓ f x.
-  Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
+  Lemma cmra_monotone_valid x : ✓ x → ✓ f x.
+  Proof. rewrite !cmra_valid_validN; eauto using cmra_monotone_validN. Qed.
 End cmra_monotone.
 
+Instance cmra_homomorphism_id {A : cmraT} : CMRAHomomorphism (@id A).
+Proof. repeat split; by try apply _. Qed.
+Instance cmra_homomorphism_compose {A B C : cmraT} (f : A → B) (g : B → C) :
+  CMRAHomomorphism f → CMRAHomomorphism g → CMRAHomomorphism (g ∘ f).
+Proof.
+  split.
+  - apply _. 
+  - move=> x y /=. rewrite -(cmra_homomorphism g).
+    by apply (ne_proper _), cmra_homomorphism.
+Qed.
+
+Instance cmra_homomorphism_proper {A B : cmraT} (f : A → B) :
+  CMRAHomomorphism f → Proper ((≡) ==> (≡)) f := λ _, ne_proper _.
+
+Instance ucmra_homomorphism_id {A : ucmraT} : UCMRAHomomorphism (@id A).
+Proof. repeat split; by try apply _. Qed.
+Instance ucmra_homomorphism_compose {A B C : ucmraT} (f : A → B) (g : B → C) :
+  UCMRAHomomorphism f → UCMRAHomomorphism g → UCMRAHomomorphism (g ∘ f).
+Proof. split. apply _. by rewrite /= !ucmra_homomorphism_unit. Qed.
+
 (** Functors *)
 Structure rFunctor := RFunctor {
   rFunctor_car : cofeT → cofeT → cmraT;
@@ -1010,7 +1044,7 @@ Instance prod_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B'
   CMRAMonotone f → CMRAMonotone g → CMRAMonotone (prod_map f g).
 Proof.
   split; first apply _.
-  - by intros n x [??]; split; simpl; apply validN_preserving.
+  - by intros n x [??]; split; simpl; apply cmra_monotone_validN.
   - intros x y; rewrite !prod_included=> -[??] /=.
     by split; apply cmra_monotone.
 Qed.
@@ -1142,6 +1176,8 @@ Section option.
   (** Misc *)
   Global Instance Some_cmra_monotone : CMRAMonotone Some.
   Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed.
+  Global Instance Some_cmra_homomorphism : CMRAHomomorphism Some.
+  Proof. split. apply _. done. Qed.
 
   Lemma op_None mx my : mx ⋅ my = None ↔ mx = None ∧ my = None.
   Proof. destruct mx, my; naive_solver. Qed.
@@ -1176,7 +1212,7 @@ Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f}
   CMRAMonotone (fmap f : option A → option B).
 Proof.
   split; first apply _.
-  - intros n [x|] ?; rewrite /cmra_validN //=. by apply (validN_preserving f).
+  - intros n [x|] ?; rewrite /cmra_validN //=. by apply (cmra_monotone_validN f).
   - intros mx my; rewrite !option_included.
     intros [->|(x&y&->&->&[Hxy|?])]; simpl; eauto 10 using @cmra_monotone.
     right; exists (f x), (f y). by rewrite {3}Hxy; eauto.

algebra/cmra_big_op.v

@@ -376,62 +376,54 @@ End gset.
 End big_op.
 
 Lemma big_opL_commute {M1 M2 : ucmraT} {A} (h : M1 → M2)
-    `{!Proper ((≡) ==> (≡)) h} (f : nat → A → M1) l :
-  h ∅ ≡ ∅ →
-  (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) →
+    `{!UCMRAHomomorphism h} (f : nat → A → M1) l :
   h ([⋅ list] k↦x ∈ l, f k x) ≡ ([⋅ list] k↦x ∈ l, h (f k x)).
 Proof.
-  intros ??. revert f. induction l as [|x l IH]=> f.
-  - by rewrite !big_opL_nil.
-  - by rewrite !big_opL_cons -IH.
+  revert f. induction l as [|x l IH]=> f.
+  - by rewrite !big_opL_nil ucmra_homomorphism_unit.
+  - by rewrite !big_opL_cons cmra_homomorphism -IH.
 Qed.
 Lemma big_opL_commute1 {M1 M2 : ucmraT} {A} (h : M1 → M2)
-    `{!Proper ((≡) ==> (≡)) h} (f : nat → A → M1) l :
-  (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) →
-  l ≠ [] →
-  h ([⋅ list] k↦x ∈ l, f k x) ≡ ([⋅ list] k↦x ∈ l, h (f k x)).
+    `{!CMRAHomomorphism h} (f : nat → A → M1) l :
+  l ≠ [] → h ([⋅ list] k↦x ∈ l, f k x) ≡ ([⋅ list] k↦x ∈ l, h (f k x)).
 Proof.
-  intros ??. revert f. induction l as [|x [|x' l'] IH]=> f //.
+  intros ?. revert f. induction l as [|x [|x' l'] IH]=> f //.
   - by rewrite !big_opL_singleton.
-  - by rewrite !(big_opL_cons _ x) -IH.
+  - by rewrite !(big_opL_cons _ x) cmra_homomorphism -IH.
 Qed.
 
 Lemma big_opM_commute {M1 M2 : ucmraT} `{Countable K} {A} (h : M1 → M2)
-    `{!Proper ((≡) ==> (≡)) h} (f : K → A → M1) m :
-  h ∅ ≡ ∅ →
-  (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) →
+    `{!UCMRAHomomorphism h} (f : K → A → M1) m :
   h ([⋅ map] k↦x ∈ m, f k x) ≡ ([⋅ map] k↦x ∈ m, h (f k x)).
 Proof.
-  intros. rewrite /big_opM.
-  induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite -?IH; auto.
+  intros. induction m as [|i x m ? IH] using map_ind.
+  - by rewrite !big_opM_empty ucmra_homomorphism_unit.
+  - by rewrite !big_opM_insert // cmra_homomorphism -IH.
 Qed.
 Lemma big_opM_commute1 {M1 M2 : ucmraT} `{Countable K} {A} (h : M1 → M2)
-    `{!Proper ((≡) ==> (≡)) h} (f : K → A → M1) m :
-  (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) →
-  m ≠ ∅ →
-  h ([⋅ map] k↦x ∈ m, f k x) ≡ ([⋅ map] k↦x ∈ m, h (f k x)).
+    `{!CMRAHomomorphism h} (f : K → A → M1) m :
+  m ≠ ∅ → h ([⋅ map] k↦x ∈ m, f k x) ≡ ([⋅ map] k↦x ∈ m, h (f k x)).
 Proof.
-  rewrite -map_to_list_empty' /big_opM=> ??.
-  induction (map_to_list m) as [|[i x] [|i' x'] IH];
-    csimpl in *; rewrite ?right_id -?IH //.
+  intros. induction m as [|i x m ? IH] using map_ind; [done|].
+  destruct (decide (m = ∅)) as [->|].
+  - by rewrite !big_opM_insert // !big_opM_empty !right_id.
+  - by rewrite !big_opM_insert // cmra_homomorphism -IH //.
 Qed.
 
-Lemma big_opS_commute {M1 M2 : ucmraT} `{Countable A} (h : M1 → M2)
-    `{!Proper ((≡) ==> (≡)) h} (f : A → M1) X :
-  h ∅ ≡ ∅ →
-  (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) →
+Lemma big_opS_commute {M1 M2 : ucmraT} `{Countable A}
+    (h : M1 → M2) `{!UCMRAHomomorphism h} (f : A → M1) X :
   h ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, h (f x)).
 Proof.
-  intros. rewrite /big_opS.
-  induction (elements X) as [|x l IH]; csimpl; rewrite -?IH; auto.
+  intros. induction X as [|x X ? IH] using collection_ind_L.
+  - by rewrite !big_opS_empty ucmra_homomorphism_unit.
+  - by rewrite !big_opS_insert // cmra_homomorphism -IH.
 Qed.
-Lemma big_opS_commute1 {M1 M2 : ucmraT} `{Countable A} (h : M1 → M2)
-    `{!Proper ((≡) ==> (≡)) h} (f : A → M1) X :
-  (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) →
-  X ≢ ∅ →
-  h ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, h (f x)).
+Lemma big_opS_commute1 {M1 M2 : ucmraT} `{Countable A}
+    (h : M1 → M2) `{!CMRAHomomorphism h} (f : A → M1) X :
+  X ≠ ∅ → h ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, h (f x)).
 Proof.
-  rewrite -elements_empty' /big_opS=> ??.
-  induction (elements X) as [|x [|x' l] IH];
-    csimpl in *; rewrite ?right_id -?IH //.
+  intros. induction X as [|x X ? IH] using collection_ind_L; [done|].
+  destruct (decide (X = ∅)) as [->|].
+  - by rewrite !big_opS_insert // !big_opS_empty !right_id.
+  - by rewrite !big_opS_insert // cmra_homomorphism -IH //.
 Qed.

algebra/csum.v

@@ -242,6 +242,11 @@ Proof. by move=> H[]? =>[/H||]. Qed.
 Global Instance Cinr_exclusive b : Exclusive b → Exclusive (Cinr b).
 Proof. by move=> H[]? =>[|/H|]. Qed.
 
+Global Instance Cinl_cmra_homomorphism : CMRAHomomorphism Cinl.
+Proof. split. apply _. done. Qed.
+Global Instance Cinr_cmra_homomorphism : CMRAHomomorphism Cinr.
+Proof. split. apply _. done. Qed.
+
 (** Internalized properties *)
 Lemma csum_equivI {M} (x y : csum A B) :
   x ≡ y ⊣⊢ (match x, y with
@@ -330,7 +335,7 @@ Instance csum_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B'
   CMRAMonotone f → CMRAMonotone g → CMRAMonotone (csum_map f g).
 Proof.
   split; try apply _.
-  - intros n [a|b|]; simpl; auto using validN_preserving.
+  - intros n [a|b|]; simpl; auto using cmra_monotone_validN.
   - intros x y; rewrite !csum_included.
     intros [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]; simpl;
     eauto 10 using cmra_monotone.

algebra/gmap.v

@@ -238,6 +238,9 @@ Qed.
 Lemma op_singleton (i : K) (x y : A) :
   {[ i := x ]} ⋅ {[ i := y ]} = ({[ i := x ⋅ y ]} : gmap K A).
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
+Global Instance singleton_cmra_homomorphism :
+  CMRAHomomorphism (singletonM i : A → gmap K A).
+Proof. split. apply _. intros. by rewrite op_singleton. Qed.
 
 Global Instance gmap_persistent m : (∀ x : A, Persistent x) → Persistent m.
 Proof.
@@ -434,7 +437,7 @@ Instance gmap_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B)
   `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B).
 Proof.
   split; try apply _.
-  - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _).
+  - by intros n m ? i; rewrite lookup_fmap; apply (cmra_monotone_validN _).
   - intros m1 m2; rewrite !lookup_included=> Hm i.
     by rewrite !lookup_fmap; apply: cmra_monotone.
 Qed.

algebra/iprod.v

@@ -287,7 +287,7 @@ Instance iprod_map_cmra_monotone
   (∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f).
 Proof.
   split; first apply _.
-  - intros n g Hg x; rewrite /iprod_map; apply (validN_preserving (f _)), Hg.
+  - intros n g Hg x; rewrite /iprod_map; apply (cmra_monotone_validN (f _)), Hg.
   - intros g1 g2; rewrite !iprod_included_spec=> Hf x.
     rewrite /iprod_map; apply (cmra_monotone _), Hf.
 Qed.

algebra/list.v

@@ -429,7 +429,7 @@ Instance list_fmap_cmra_monotone {A B : ucmraT} (f : A → B)
 Proof.
   split; try apply _.
   - intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
-    by apply (validN_preserving (fmap f : option A → option B)).
+    by apply (cmra_monotone_validN (fmap f : option A → option B)).
   - intros l1 l2. rewrite !list_lookup_included=> Hl i. rewrite !list_lookup_fmap.
     by apply (cmra_monotone (fmap f : option A → option B)).
 Qed.

algebra/upred.v

@@ -69,13 +69,13 @@ Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
   `{!CMRAMonotone f} (P : uPred M1) :
   uPred M2 := {| uPred_holds n x := P n (f x) |}.
 Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
-Next Obligation. naive_solver eauto using uPred_closed, validN_preserving. Qed.
+Next Obligation. naive_solver eauto using uPred_closed, cmra_monotone_validN. Qed.
 
 Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
   `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
 Proof.
   intros x1 x2 Hx; split=> n' y ??.
-  split; apply Hx; auto using validN_preserving.
+  split; apply Hx; auto using cmra_monotone_validN.
 Qed.
 Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P ≡ P.
 Proof. by split=> n x ?. Qed.
@@ -1477,7 +1477,6 @@ Qed.
 
 Theorem soundness : ¬ (True ⊢ False).
 Proof. exact (adequacy False 0). Qed.
-
 End uPred_logic.
 
 (* Hint DB for the logic *)
@@ -1490,6 +1489,8 @@ Hint Immediate True_intro False_elim : I.
 Hint Immediate iff_refl eq_refl' : I.
 End uPred.
 
+Import uPred.
+
 (* CMRA structure on uPred *)
 Section cmra.
   Context {M : ucmraT}.
@@ -1505,19 +1506,19 @@ Section cmra.
 
   Lemma uPred_validN_alt n (P : uPred M) : ✓{n} P → P ≡{n}≡ True%I.
   Proof.
-    uPred.unseal=> HP; split=> n' x ??; split; [done|].
+    unseal=> HP; split=> n' x ??; split; [done|].
     intros _. by apply HP.
   Qed.
 
   Lemma uPred_cmra_validN_op_l n P Q : ✓{n} (P ★ Q)%I → ✓{n} P.
   Proof.
-    uPred.unseal. intros HPQ n' x ??.
+    unseal. intros HPQ n' x ??.
     destruct (HPQ n' x) as (x1&x2&->&?&?); auto.
     eapply uPred_mono with x1; eauto using cmra_includedN_l.
   Qed.
 
   Lemma uPred_included P Q : P ≼ Q → Q ⊢ P.
-  Proof. intros [P' ->]. apply uPred.sep_elim_l. Qed.
+  Proof. intros [P' ->]. apply sep_elim_l. Qed.
 
   Definition uPred_cmra_mixin : CMRAMixin (uPred M).
   Proof.
@@ -1551,6 +1552,19 @@ Section cmra.
 
   Canonical Structure uPredUR :=
     UCMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.
+
+  Global Instance uPred_always_homomorphism : UCMRAHomomorphism uPred_always.
+  Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.
+  Global Instance uPred_always_if_homomorphism b :
+    UCMRAHomomorphism (uPred_always_if b).
+  Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed.
+  Global Instance uPred_later_homomorphism : UCMRAHomomorphism uPred_later.
+  Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed.
+  Global Instance uPred_except_last_homomorphism :
+    CMRAHomomorphism uPred_except_last.
+  Proof. split. apply _. apply except_last_sep. Qed.
+  Global Instance uPred_ownM_homomorphism : UCMRAHomomorphism uPred_ownM.
+  Proof. split; [split|]. apply _. apply ownM_op. apply ownM_empty'. Qed.
 End cmra.
 
 Arguments uPredR : clear implicits.

algebra/upred_big_op.v

@@ -155,15 +155,15 @@ Section list.
 
   Lemma big_sepL_later Φ l :
     ▷ ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, ▷ Φ k x).
-  Proof. apply (big_opL_commute _). apply later_True. apply later_sep. Qed.
+  Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_sepL_always Φ l :
     (□ [★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, □ Φ k x).
-  Proof. apply (big_opL_commute _). apply always_pure. apply always_sep. Qed.
+  Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_sepL_always_if p Φ l :
     □?p ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, □?p Φ k x).
-  Proof. destruct p; simpl; auto using big_sepL_always. Qed.
+  Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_sepL_forall Φ l :
     (∀ k x, PersistentP (Φ k x)) →
@@ -277,15 +277,15 @@ Section gmap.
 
   Lemma big_sepM_later Φ m :
     ▷ ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x).
-  Proof. apply (big_opM_commute _). apply later_True. apply later_sep. Qed.
+  Proof. apply (big_opM_commute _). Qed.
 
   Lemma big_sepM_always Φ m :
     (□ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □ Φ k x).
-  Proof. apply (big_opM_commute _). apply always_pure. apply always_sep. Qed.
+  Proof. apply (big_opM_commute _). 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.
+  Proof. apply (big_opM_commute _). Qed.
 
   Lemma big_sepM_forall Φ m :
     (∀ k x, PersistentP (Φ k x)) →
@@ -386,14 +386,14 @@ Section gset.
   Proof. apply: big_opS_opS. Qed.
 
   Lemma big_sepS_later Φ X : ▷ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y).
-  Proof. apply (big_opS_commute _). apply later_True. apply later_sep. Qed.
+  Proof. apply (big_opS_commute _). Qed.
 
   Lemma big_sepS_always Φ X : □ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y).
-  Proof. apply (big_opS_commute _). apply always_pure. apply always_sep. Qed.
+  Proof. apply (big_opS_commute _). 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.
+  Proof. apply (big_opS_commute _). Qed.
 
   Lemma big_sepS_forall Φ X :
     (∀ x, PersistentP (Φ x)) → ([★ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ■ (x ∈ X) → Φ x).
@@ -410,7 +410,7 @@ Section gset.
   Qed.
 
   Lemma big_sepS_impl Φ Ψ X :
-      □ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ X, Ψ x.
+    □ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ X, Ψ x.
   Proof.