phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/big_op.v *)
Lemma big_opM_omap {B} (h : A → option B) (f : K → B → M) m :
    ([^o map] k↦y ∈ omap h m, f k y)
    ≡ [^o map] k↦y ∈ m, from_option (f k) u (h y).
Proof.
    revert f. induction m as [|i x m Hmi IH] using map_ind=> f.
    { by rewrite omap_empty !big_opM_empty. }
    assert (omap h m !! i = None) by (by rewrite lookup_omap Hmi).
    destruct (h x) as [y|] eqn:Hhx.
    - by rewrite omap_insert Hhx //= !big_opM_insert // IH Hhx.
    - rewrite omap_insert_None // delete_id // big_opM_insert //.
      by rewrite Hhx /= left_id.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_insert_delete `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x :
    ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ delete i m, f k y.
Proof.
    rewrite -insert_delete_eq big_opM_insert; first done. by rewrite lookup_delete_eq.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_insert_override (f : K → A → M) m i x x' :
    m !! i = Some x → f i x ≡ f i x' →
    ([^o map] k↦y ∈ <[i:=x']> m, f k y) ≡ ([^o map] k↦y ∈ m, f k y).
Proof.
    intros ? Hx. rewrite -insert_delete_eq big_opM_insert ?lookup_delete_eq //.
    by rewrite -Hx -big_opM_delete.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_fn_insert {B} (g : K → A → B → M) (f : K → B) m i (x : A) b :
    m !! i = None →
    ([^o map] k↦y ∈ <[i:=x]> m, g k y (<[i:=b]> f k))
    ≡ g i x b `o` [^o map] k↦y ∈ m, g k y (f k).
Proof.
    intros. rewrite big_opM_insert // fn_lookup_insert.
    f_equiv; apply big_opM_proper; auto=> k y ?.
    by rewrite fn_lookup_insert_ne; last set_solver.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_fn_insert' (f : K → M) m i x P :
    m !! i = None →
    ([^o map] k↦y ∈ <[i:=x]> m, <[i:=P]> f k) ≡ (P `o` [^o map] k↦y ∈ m, f k).
Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_filter' (φ : K * A → Prop) `{∀ kx, Decision (φ kx)} f m :
    ([^o map] k ↦ x ∈ filter φ m, f k x)
    ≡ ([^o map] k ↦ x ∈ m, if decide (φ (k, x)) then f k x else u).
Proof.
    induction m as [|k v m ? IH] using map_ind.
    { by rewrite map_filter_empty !big_opM_empty. }
    destruct (decide (φ (k, v))).
    - rewrite map_filter_insert_True //.
      assert (filter φ m !! k = None) by (apply map_lookup_filter_None; eauto).
      by rewrite !big_opM_insert // decide_True // IH.
    - rewrite map_filter_insert_not' //; last by congruence.
      rewrite !big_opM_insert // decide_False // IH. by rewrite left_id.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_union f m1 m2 :
    m1 ##ₘ m2 →
    ([^o map] k↦y ∈ m1 ∪ m2, f k y)
    ≡ ([^o map] k↦y ∈ m1, f k y) `o` ([^o map] k↦y ∈ m2, f k y).
Proof.
    intros. induction m1 as [|i x m ? IH] using map_ind.
    { by rewrite big_opM_empty !left_id. }
    decompose_map_disjoint.
    rewrite -insert_union_l !big_opM_insert //;
      last by apply lookup_union_None.
    rewrite -assoc IH //.
  Qed.
(* iris/algebra/big_op.v *)
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_unseal /big_opM_def -big_opL_op. by apply big_opL_proper=> ? [??].
  Qed.
(* iris/algebra/big_op.v *)
(* Shows that some property [P] is closed under [big_opM]. Examples of [P]
  are [Persistent], [Affine], [Timeless]. *)
Lemma big_opM_closed (P : M → Prop) f m :
    Proper ((≡) ==> iff) P →
    P u →
    (∀ x y, P x → P y → P (x `o` y)) →
    (∀ k x, m !! k = Some x → P (f k x)) →
    P ([^o map] k↦x ∈ m, f k x).
Proof.
    intros ?? Hop Hf. induction m as [|k x ?? IH] using map_ind.
    { by rewrite big_opM_empty. }
    rewrite big_opM_insert //. apply Hop.
    { apply Hf. by rewrite lookup_insert_eq. }
    apply IH=> k' x' ?. apply Hf. rewrite lookup_insert_ne; naive_solver.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_sep_zip_with `{Countable K} {A B C}
    (f : A → B → C) (g1 : C → A) (g2 : C → B)
    (h1 : K → A → M) (h2 : K → B → M) m1 m2 :
  (∀ x y, g1 (f x y) = x) →
  (∀ x y, g2 (f x y) = y) →
  (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
  ([^o map] k↦xy ∈ map_zip_with f m1 m2, h1 k (g1 xy) `o` h2 k (g2 xy)) ≡
  ([^o map] k↦x ∈ m1, h1 k x) `o` ([^o map] k↦y ∈ m2, h2 k y).
Proof.
  intros Hdom Hg1 Hg2. rewrite big_opM_op.
  rewrite -(big_opM_fmap g1) -(big_opM_fmap g2).
  rewrite map_fmap_zip_with_r; [|naive_solver..].
  by rewrite map_fmap_zip_with_l; [|naive_solver..].
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_sep_zip `{Countable K} {A B}
    (h1 : K → A → M) (h2 : K → B → M) m1 m2 :
  (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
  ([^o map] k↦xy ∈ map_zip m1 m2, h1 k xy.1 `o` h2 k xy.2) ≡
  ([^o map] k↦x ∈ m1, h1 k x) `o` ([^o map] k↦y ∈ m2, h2 k y).
Proof. intros. by apply big_opM_sep_zip_with. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_kmap `{Countable K1, Countable K2} {A}
    (h : K1 → K2) `{!Inj (=) (=) h} (f : K2 → A → M) (m : gmap K1 A) :
  ([^o map] k2 ↦ y ∈ kmap h m, f k2 y) ≡ ([^o map] k1 ↦ y ∈ m, f (h k1) y).
Proof.
  rewrite big_op.big_opM_unseal /big_op.big_opM_def map_to_list_kmap big_opL_fmap.
  by apply big_opL_proper=> ? [??].
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_map_seq {A} (f : nat → A → M) (start : nat) (l : list A) :
  ([^o map] k ↦ x ∈ map_seq start l, f k x) ≡
  ([^o list] i ↦ x ∈ l, f (start + i) x).
Proof.
  rewrite big_op.big_opM_unseal /big_op.big_opM_def.
  rewrite map_to_list_seq big_opL_zip_seq //.
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_map_seqZ {A} (f : Z → A → M) (start : Z) (l : list A) :
  ([^o map] k ↦ x ∈ map_seqZ start l, f k x) ≡
  ([^o list] i ↦ x ∈ l, f (start + i)%Z x).
Proof.
  rewrite big_op.big_opM_unseal /big_op.big_opM_def.
  rewrite map_to_list_seqZ big_opL_zip_seqZ //.
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_gen_proper R f g X :
    Reflexive R → Proper (R ==> R ==> R) o →
    (∀ x, x ∈ X → R (f x) (g x)) →
    R ([^o set] x ∈ X, f x) ([^o set] x ∈ X, g x).
Proof.
    rewrite big_opS_unseal. intros ?? Hf. apply (big_opL_gen_proper R); auto.
    intros k x ?%list_elem_of_lookup_2. by apply Hf, elem_of_elements.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_ext f g X :
    (∀ x, x ∈ X → f x = g x) →
    ([^o set] x ∈ X, f x) = ([^o set] x ∈ X, g x).
Proof. apply big_opS_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
(* The lemmas [big_opS_ne] and [big_opS_proper] are more generic than the
  instances as they also give [x ∈ X] in the premise. *)
Lemma big_opS_ne f g X n :
    (∀ x, x ∈ X → f x ≡{n}≡ g x) →
    ([^o set] x ∈ X, f x) ≡{n}≡ ([^o set] x ∈ X, g x).
Proof. apply big_opS_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_proper f g X :
    (∀ x, x ∈ X → f x ≡ g x) →
    ([^o set] x ∈ X, f x) ≡ ([^o set] x ∈ X, g x).
Proof. apply big_opS_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
Instance big_opS_ne' n :
    Proper (pointwise_relation _ (dist n) ==> (=) ==> dist n) (big_opS o (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opS_ne; intros; apply Hf. Qed.
(* iris/algebra/big_op.v *)
Instance big_opS_proper' :
    Proper (pointwise_relation _ (≡) ==> (=) ==> (≡)) (big_opS o (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opS_proper; intros; apply Hf. Qed.
(* iris/algebra/big_op.v *)
(* FIXME: This lemma could be generalized from [≡] to [=], but that breaks
  [setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opS_elements f X :
    ([^o set] x ∈ X, f x) ≡ [^o list] x ∈ elements X, f x.
Proof. by rewrite big_opS_unseal. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_empty f : ([^o set] x ∈ ∅, f x) = u.
Proof. by rewrite big_opS_unseal /big_opS_def elements_empty. Qed.
(* iris/algebra/big_op.v *)
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 elements_union_singleton. Qed.
(* iris/algebra/big_op.v *)
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))
    ≡ f x b `o` [^o set] y ∈ X, f y (h y).
Proof.
    intros. rewrite big_opS_insert // fn_lookup_insert.
    f_equiv; apply big_opS_proper; auto=> y ?.
    by rewrite fn_lookup_insert_ne; last set_solver.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_fn_insert' f X x P :
    x ∉ X → ([^o set] y ∈ {[ x ]} ∪ X, <[x:=P]> f y) ≡ (P `o` [^o set] y ∈ X, f y).
Proof. apply (big_opS_fn_insert (λ y, id)). Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_union f X Y :
    X ## Y →
    ([^o set] y ∈ X ∪ Y, f y) ≡ ([^o set] y ∈ X, f y) `o` ([^o set] y ∈ Y, f y).
Proof.
    intros. induction X as [|x X ? IH] using set_ind_L.
    { by rewrite left_id_L big_opS_empty left_id. }
    rewrite -assoc_L !big_opS_insert; [|set_solver..].
    by rewrite -assoc IH; last set_solver.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_delete f X x :
    x ∈ X → ([^o set] y ∈ X, f y) ≡ f x `o` [^o set] y ∈ X ∖ {[ x ]}, f y.
Proof.
    intros. rewrite -big_opS_insert; last set_solver.
    by rewrite -union_difference_L; last set_solver.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_singleton f x : ([^o set] y ∈ {[ x ]}, f y) ≡ f x.
Proof. intros. by rewrite big_opS_elements elements_singleton /= right_id. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_unit X : ([^o set] y ∈ X, u) ≡@{M} u.
Proof.
    by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_unseal.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_filter' (φ : A → Prop) `{∀ x, Decision (φ x)} f X :
    ([^o set] y ∈ filter φ X, f y)
    ≡ ([^o set] y ∈ X, if decide (φ y) then f y else u).
Proof.
    induction X as [|x X ? IH] using set_ind_L.
    { by rewrite filter_empty_L !big_opS_empty. }
    destruct (decide (φ x)).
    - rewrite filter_union_L filter_singleton_True_L //.
      rewrite !big_opS_insert //; last set_solver.
      by rewrite decide_True // IH.
    - rewrite filter_union_L filter_singleton_False_L // left_id_L.
      by rewrite !big_opS_insert // decide_False // IH left_id.
  Qed.
(* iris/algebra/big_op.v *)
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_elements -big_opL_op. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_list_to_set f (l : list A) :
    NoDup l →
    ([^o set] x ∈ list_to_set l, f x) ≡ [^o list] x ∈ l, f x.
Proof.
    induction 1 as [|x l ?? IHl].
    - rewrite big_opS_empty //.
    - rewrite /= big_opS_union; last set_solver.
      by rewrite big_opS_singleton IHl.
  Qed.
(* iris/algebra/big_op.v *)
(* Shows that some property [P] is closed under [big_opS]. Examples of [P]
  are [Persistent], [Affine], [Timeless]. *)
Lemma big_opS_closed (P : M → Prop) f X :
    Proper ((≡) ==> iff) P →
    P u →
    (∀ x y, P x → P y → P (x `o` y)) →
    (∀ x, x ∈ X → P (f x)) →
    P ([^o set] x ∈ X, f x).
Proof.
    intros ?? Hop Hf. induction X as [|x X ? IH] using set_ind_L.
    { by rewrite big_opS_empty. }
    rewrite big_opS_insert //. apply Hop.
    { apply Hf. set_solver. }
    apply IH=> x' ?. apply Hf. set_solver.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_set_map `{Countable A, Countable B} (h : A → B) (X : gset A) (f : B → M) :
  Inj (=) (=) h →
  ([^o set] x ∈ set_map h X, f x) ≡ ([^o set] x ∈ X, f (h x)).
Proof.
  intros Hinj.
  induction X as [|x X ? IH] using set_ind_L.
  { by rewrite set_map_empty !big_opS_empty. }
  rewrite set_map_union_L set_map_singleton_L.
  rewrite !big_opS_union; [|set_solver..].
  rewrite !big_opS_singleton IH //.
Qed.
(* iris/algebra/big_op.v *)
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 big_opM_unseal big_opS_unseal dom_empty_L. }
  by rewrite dom_insert_L big_opM_insert // IH big_opS_insert ?not_elem_of_dom.
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_set_to_map `{Countable K} {A}
    (f : K → A → M) (X : gset K) (g : K → A) :
  ([^o map] k↦a ∈ set_to_map g X, f k a) ≡ ([^o set] k ∈ X, f k (g k)).
Proof.
  induction X as [|k X ? IH] using set_ind_L.
  { by rewrite set_to_map_empty big_opM_empty big_opS_empty. }
  rewrite set_to_map_insert big_opS_insert //.
  rewrite big_opM_insert; last by rewrite lookup_set_to_map_None.
  by rewrite IH.
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_gset_to_gmap `{Countable K} {A} (f : K → A → M) (X : gset K) c :
  ([^o map] k↦a ∈ gset_to_gmap c X, f k a) ≡ ([^o set] k ∈ X, f k c).
Proof. by rewrite gset_to_gmap_set_to_map big_opM_set_to_map. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_gen_proper R f g X :
    Reflexive R → Proper (R ==> R ==> R) o →
    (∀ x, x ∈ X → R (f x) (g x)) →
    R ([^o mset] x ∈ X, f x) ([^o mset] x ∈ X, g x).
Proof.
    rewrite big_opMS_unseal. intros ?? Hf. apply (big_opL_gen_proper R); auto.
    intros k x ?%list_elem_of_lookup_2. by apply Hf, gmultiset_elem_of_elements.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_ext f g X :
    (∀ x, x ∈ X → f x = g x) →
    ([^o mset] x ∈ X, f x) = ([^o mset] x ∈ X, g x).
Proof. apply big_opMS_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
(* The lemmas [big_opMS_ne] and [big_opMS_proper] are more generic than the
  instances as they also give [x ∈ X] in the premise. *)
Lemma big_opMS_ne f g X n :
    (∀ x, x ∈ X → f x ≡{n}≡ g x) →
    ([^o mset] x ∈ X, f x) ≡{n}≡ ([^o mset] x ∈ X, g x).
Proof. apply big_opMS_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_proper f g X :
    (∀ x, x ∈ X → f x ≡ g x) →
    ([^o mset] x ∈ X, f x) ≡ ([^o mset] x ∈ X, g x).
Proof. apply big_opMS_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
Instance big_opMS_ne' n :
    Proper (pointwise_relation _ (dist n) ==> (=) ==> dist n) (big_opMS o (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opMS_ne; intros; apply Hf. Qed.
(* iris/algebra/big_op.v *)
Instance big_opMS_proper' :
    Proper (pointwise_relation _ (≡) ==> (=) ==> (≡)) (big_opMS o (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opMS_proper; intros; apply Hf. Qed.
(* iris/algebra/big_op.v *)
(* FIXME: This lemma could be generalized from [≡] to [=], but that breaks
  [setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opMS_elements f X :
    ([^o mset] x ∈ X, f x) ≡ [^o list] x ∈ elements X, f x.
Proof. by rewrite big_opMS_unseal. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_empty f : ([^o mset] x ∈ ∅, f x) = u.
Proof. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_empty. Qed.
(* iris/algebra/big_op.v *)
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_unseal /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_singleton f x : ([^o mset] y ∈ {[+ x +]}, f y) ≡ f x.
Proof.
    intros. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_singleton /= right_id.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_insert f X x :
    ([^o mset] y ∈ {[+ x +]} ⊎ X, f y) ≡ (f x `o` [^o mset] y ∈ X, f y).
Proof. intros. rewrite big_opMS_disj_union big_opMS_singleton //. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_delete f X x :
    x ∈ X → ([^o mset] y ∈ X, f y) ≡ f x `o` [^o mset] y ∈ X ∖ {[+ x +]}, f y.
Proof.
    intros. rewrite -big_opMS_singleton -big_opMS_disj_union.
    by rewrite -gmultiset_disj_union_difference'.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_unit X : ([^o mset] y ∈ X, u) ≡@{M} u.
Proof.
    by induction X using gmultiset_ind;
      rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id // big_opMS_unseal.
  Qed.
(* iris/algebra/big_op.v *)
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_unseal /big_opMS_def -big_opL_op. Qed.
(* iris/algebra/big_op.v *)
(* Shows that some property [P] is closed under [big_opMS]. Examples of [P]
  are [Persistent], [Affine], [Timeless]. *)
Lemma big_opMS_closed (P : M → Prop) f X :
    Proper ((≡) ==> iff) P →
    P u →
    (∀ x y, P x → P y → P (x `o` y)) →
    (∀ x, x ∈ X → P (f x)) →
    P ([^o mset] x ∈ X, f x).
Proof.
    intros ?? Hop Hf. induction X as [|x X IH] using gmultiset_ind.
    { by rewrite big_opMS_empty. }
    rewrite big_opMS_insert //. apply Hop.
    { apply Hf. set_solver. }
    apply IH=> x' ?. apply Hf. set_solver.
  Qed.
(* iris/algebra/big_op.v *)
(* Commuting lemmas *)
Lemma big_opL_opL {A B} (f : nat → A → nat → B → M) (l1 : list A) (l2 : list B) :
  ([^o list] k1↦x1 ∈ l1, [^o list] k2↦x2 ∈ l2, f k1 x1 k2 x2) ≡
  ([^o list] k2↦x2 ∈ l2, [^o list] k1↦x1 ∈ l1, f k1 x1 k2 x2).
Proof.
  revert f l2. induction l1 as [|x1 l1 IH]; simpl; intros Φ l2.
  { by rewrite big_opL_unit. }
  by rewrite IH big_opL_op.
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_opM {A} `{Countable K} {B}
    (f : nat → A → K → B → M) (l1 : list A) (m2 : gmap K B) :
  ([^o list] k1↦x1 ∈ l1, [^o map] k2↦x2 ∈ m2, f k1 x1 k2 x2) ≡
  ([^o map] k2↦x2 ∈ m2, [^o list] k1↦x1 ∈ l1, f k1 x1 k2 x2).
Proof. repeat setoid_rewrite big_opM_map_to_list. by rewrite big_opL_opL. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_opS {A} `{Countable B}
    (f : nat → A → B → M) (l1 : list A) (X2 : gset B) :
  ([^o list] k1↦x1 ∈ l1, [^o set] x2 ∈ X2, f k1 x1 x2) ≡
  ([^o set] x2 ∈ X2, [^o list] k1↦x1 ∈ l1, f k1 x1 x2).
Proof. repeat setoid_rewrite big_opS_elements. by rewrite big_opL_opL. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_opMS {A} `{Countable B}
    (f : nat → A → B → M) (l1 : list A) (X2 : gmultiset B) :
  ([^o list] k1↦x1 ∈ l1, [^o mset] x2 ∈ X2, f k1 x1 x2) ≡
  ([^o mset] x2 ∈ X2, [^o list] k1↦x1 ∈ l1, f k1 x1 x2).
Proof. repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_opL {A} `{Countable K} {B}
    (f : K → A → nat → B → M) (m1 : gmap K A) (l2 : list B) :
  ([^o map] k1↦x1 ∈ m1, [^o list] k2↦x2 ∈ l2, f k1 x1 k2 x2) ≡
  ([^o list] k2↦x2 ∈ l2, [^o map] k1↦x1 ∈ m1, f k1 x1 k2 x2).
Proof. symmetry. apply big_opL_opM. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_opM `{Countable K1} {A} `{Countable K2} {B}
    (f : K1 → A → K2 → B → M) (m1 : gmap K1 A) (m2 : gmap K2 B) :
  ([^o map] k1↦x1 ∈ m1, [^o map] k2↦x2 ∈ m2, f k1 x1 k2 x2) ≡
  ([^o map] k2↦x2 ∈ m2, [^o map] k1↦x1 ∈ m1, f k1 x1 k2 x2).
Proof. repeat setoid_rewrite big_opM_map_to_list. by rewrite big_opL_opL. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_opS `{Countable K} {A} `{Countable B}
    (f : K → A → B → M) (m1 : gmap K A) (X2 : gset B) :
  ([^o map] k1↦x1 ∈ m1, [^o set] x2 ∈ X2, f k1 x1 x2) ≡
  ([^o set] x2 ∈ X2, [^o map] k1↦x1 ∈ m1, f k1 x1 x2).
Proof.
  repeat setoid_rewrite big_opM_map_to_list.
  repeat setoid_rewrite big_opS_elements. by rewrite big_opL_opL.
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_opMS `{Countable K} {A} `{Countable B} (f : K → A → B → M)
    (m1 : gmap K A) (X2 : gmultiset B) :
  ([^o map] k1↦x1 ∈ m1, [^o mset] x2 ∈ X2, f k1 x1 x2) ≡
  ([^o mset] x2 ∈ X2, [^o map] k1↦x1 ∈ m1, f k1 x1 x2).
Proof.
  repeat setoid_rewrite big_opM_map_to_list.
  repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL.
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_opL `{Countable A} {B}
    (f : A → nat → B → M) (X1 : gset A) (l2 : list B) :
  ([^o set] x1 ∈ X1, [^o list] k2↦x2 ∈ l2, f x1 k2 x2) ≡
  ([^o list] k2↦x2 ∈ l2, [^o set] x1 ∈ X1, f x1 k2 x2).
Proof. symmetry. apply big_opL_opS. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_opM `{Countable A} `{Countable K} {B}
    (f : A → K → B → M) (X1 : gset A) (m2 : gmap K B) :
  ([^o set] x1 ∈ X1, [^o map] k2↦x2 ∈ m2, f x1 k2 x2) ≡
  ([^o map] k2↦x2 ∈ m2, [^o set] x1 ∈ X1, f x1 k2 x2).
Proof. symmetry. apply big_opM_opS. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_opS `{Countable A, Countable B}
    (X : gset A) (Y : gset B) (f : A → B → M) :
  ([^o set] x ∈ X, [^o set] y ∈ Y, f x y) ≡ ([^o set] y ∈ Y, [^o set] x ∈ X, f x y).
Proof. repeat setoid_rewrite big_opS_elements. by rewrite big_opL_opL. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_opMS `{Countable A, Countable B}
    (X : gset A) (Y : gmultiset B) (f : A → B → M) :
  ([^o set] x ∈ X, [^o mset] y ∈ Y, f x y) ≡ ([^o mset] y ∈ Y, [^o set] x ∈ X, f x y).
Proof.
  repeat setoid_rewrite big_opS_elements.
  repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL.
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_opL `{Countable A} {B}
    (f : A → nat → B → M) (X1 : gmultiset A) (l2 : list B) :
  ([^o mset] x1 ∈ X1, [^o list] k2↦x2 ∈ l2, f x1 k2 x2) ≡
  ([^o list] k2↦x2 ∈ l2, [^o mset] x1 ∈ X1, f x1 k2 x2).
Proof. symmetry. apply big_opL_opMS. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_opM `{Countable A} `{Countable K} {B} (f : A → K → B → M)
    (X1 : gmultiset A) (m2 : gmap K B) :
  ([^o mset] x1 ∈ X1, [^o map] k2↦x2 ∈ m2, f x1 k2 x2) ≡
  ([^o map] k2↦x2 ∈ m2, [^o mset] x1 ∈ X1, f x1 k2 x2).
Proof. symmetry. apply big_opM_opMS. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_opS `{Countable A, Countable B}
    (X : gmultiset A) (Y : gset B) (f : A → B → M) :
  ([^o mset] x ∈ X, [^o set] y ∈ Y, f x y) ≡ ([^o set] y ∈ Y, [^o mset] x ∈ X, f x y).
Proof. symmetry. apply big_opS_opMS. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_opMS `{Countable A, Countable B}
    (X : gmultiset A) (Y : gmultiset B) (f : A → B → M) :
  ([^o mset] x ∈ X, [^o mset] y ∈ Y, f x y) ≡ ([^o mset] y ∈ Y, [^o mset] x ∈ X, f x y).
Proof. repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL. Qed.
(* iris/algebra/big_op.v *)
(* The ssreflect rewrite tactic only works for relations that have a
  [RewriteRelation] instance. For the purpose of this section, we want to
  rewrite with arbitrary relations, so we declare any relation to be a
  [RewriteRelation]. *)
Instance : ∀ {A} (R : relation A), RewriteRelation R
:= {}.
(* iris/algebra/big_op.v *)
Lemma big_opL_commute {A} (h : M1 → M2) `{!MonoidHomomorphism o1 o2 R h}
      (f : nat → A → M1) l :
    R (h ([^o1 list] k↦x ∈ l, f k x)) ([^o2 list] k↦x ∈ l, h (f k x)).
Proof.
    revert f. induction l as [|x l IH]=> f /=.
    - apply monoid_homomorphism_unit.
    - by rewrite monoid_homomorphism IH.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_commute1 {A} (h : M1 → M2) `{!WeakMonoidHomomorphism o1 o2 R h}
      (f : nat → A → M1) l :
    l ≠ [] → R (h ([^o1 list] k↦x ∈ l, f k x)) ([^o2 list] k↦x ∈ l, h (f k x)).
Proof.
    intros ?. revert f. induction l as [|x [|x' l'] IH]=> f //.
    - by rewrite !big_opL_singleton.
    - by rewrite !(big_opL_cons _ x) monoid_homomorphism IH.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_commute `{Countable K} {A} (h : M1 → M2)
      `{!MonoidHomomorphism o1 o2 R h} (f : K → A → M1) m :
    R (h ([^o1 map] k↦x ∈ m, f k x)) ([^o2 map] k↦x ∈ m, h (f k x)).
Proof.
    intros. induction m as [|i x m ? IH] using map_ind.
    - by rewrite !big_opM_empty monoid_homomorphism_unit.
    - by rewrite !big_opM_insert // monoid_homomorphism -IH.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_commute1 `{Countable K} {A} (h : M1 → M2)
      `{!WeakMonoidHomomorphism o1 o2 R h} (f : K → A → M1) m :
    m ≠ ∅ → R (h ([^o1 map] k↦x ∈ m, f k x)) ([^o2 map] k↦x ∈ m, h (f k x)).
Proof.
    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 // monoid_homomorphism -IH //.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_commute `{Countable A} (h : M1 → M2)
      `{!MonoidHomomorphism o1 o2 R h} (f : A → M1) X :
    R (h ([^o1 set] x ∈ X, f x)) ([^o2 set] x ∈ X, h (f x)).
Proof.
    intros. induction X as [|x X ? IH] using set_ind_L.
    - by rewrite !big_opS_empty monoid_homomorphism_unit.
    - by rewrite !big_opS_insert // monoid_homomorphism -IH.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_commute1 `{Countable A} (h : M1 → M2)
      `{!WeakMonoidHomomorphism o1 o2 R h} (f : A → M1) X :
    X ≠ ∅ → R (h ([^o1 set] x ∈ X, f x)) ([^o2 set] x ∈ X, h (f x)).
Proof.
    intros. induction X as [|x X ? IH] using set_ind_L; [done|].
    destruct (decide (X = ∅)) as [->|].
    - by rewrite !big_opS_insert // !big_opS_empty !right_id.
    - by rewrite !big_opS_insert // monoid_homomorphism -IH //.
  Qed.