phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/big_op.v *)
Lemma big_sepM2_affinely_pure_2 (φ : K → A → B → Prop) m1 m2 :
    (∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
    <affine> ⌜∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → φ k y1 y2⌝ ⊢@{PROP}
      ([∗ map] k↦y1;y2 ∈ m1;m2, <affine> ⌜φ k y1 y2⌝).
Proof.
    intros Hdom.
    rewrite big_sepM2_alt_lookup.
    rewrite -big_sepM_affinely_pure_2.
    rewrite affinely_and_r -pure_and. f_equiv. f_equiv=>-Hforall.
    split; first done.
    intros k [y1 y2] (? & ? & [= <- <-] & Hy1 & Hy2)%map_lookup_zip_with_Some; simpl.
    by eapply Hforall.
  Qed.
(* iris/bi/big_op.v *)
(* The general backwards direction requires [BiAffine] to cover the empty case. *)
Lemma big_sepM2_pure `{!BiAffine PROP} (φ : K → A → B → Prop) m1 m2 :
    ([∗ map] k↦y1;y2 ∈ m1;m2, ⌜φ k y1 y2⌝) ⊣⊢@{PROP}
      ⌜(∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) ∧
       (∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → φ k y1 y2)⌝.
Proof.
    apply (anti_symm (⊢)).
    { rewrite pure_and. apply and_intro.
      - apply big_sepM2_lookup_iff.
      - apply big_sepM2_pure_1. }
    rewrite -(affine_affinely ⌜_⌝%I).
    rewrite pure_and -affinely_and_r.
    apply pure_elim_l=>Hdom.
    rewrite big_sepM2_affinely_pure_2 //. by setoid_rewrite affinely_elim.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_persistently `{!BiAffine PROP} Φ m1 m2 :
    <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_alt persistently_and
      persistently_pure big_sepM_persistently.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_intro Φ m1 m2 :
    (∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
    □ (∀ k x1 x2, ⌜m1 !! k = Some x1⌝ → ⌜m2 !! k = Some x2⌝ → Φ k x1 x2) ⊢
    [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
Proof.
    intros. rewrite big_sepM2_alt_lookup.
    apply and_intro; [by apply pure_intro|].
    rewrite -big_sepM_intro. f_equiv; f_equiv=> k.
    apply forall_intro=> -[x1 x2]. rewrite (forall_elim x1) (forall_elim x2).
    apply impl_intro_l, pure_elim_l.
    intros (?&?&[= <- <-]&?&?)%map_lookup_zip_with_Some.
    by rewrite !pure_True // !True_impl.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_forall `{!BiAffine PROP} Φ m1 m2 :
    (∀ k x1 x2, Persistent (Φ k x1 x2)) →
    ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢
      ⌜∀ 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.
    intros. apply (anti_symm _).
    { apply and_intro; [apply big_sepM2_lookup_iff|].
      apply forall_intro=> k. apply forall_intro=> x1. apply forall_intro=> x2.
      do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply: big_sepM2_lookup. }
    apply pure_elim_l=> Hdom. rewrite big_sepM2_alt_lookup.
    apply and_intro; [by apply pure_intro|].
    rewrite big_sepM_forall. f_equiv=> k.
    apply forall_intro=> -[x1 x2]. rewrite (forall_elim x1) (forall_elim x2).
    apply impl_intro_l, pure_elim_l.
    intros (?&?&[= <- <-]&?&?)%map_lookup_zip_with_Some.
    by rewrite !pure_True // !True_impl.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_impl Φ Ψ m1 m2 :
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) -∗
    □ (∀ k x1 x2,
      ⌜m1 !! k = Some x1⌝ → ⌜m2 !! k = Some x2⌝ → Φ k x1 x2 -∗ Ψ k x1 x2) -∗
    [∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2.
Proof.
    apply entails_wand.
    rewrite -(idemp bi_and (big_sepM2 _ _ _)) {1}big_sepM2_lookup_iff.
    apply pure_elim_l=> ?. rewrite big_sepM2_intro //.
    apply bi.wand_intro_l. rewrite -big_sepM2_sep. by setoid_rewrite wand_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_wand Φ Ψ m1 m2 :
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) -∗
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2 -∗ Ψ k y1 y2) -∗
    [∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2.
Proof.
    apply entails_wand, wand_intro_r. rewrite -big_sepM2_sep.
    setoid_rewrite wand_elim_r. done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_lookup_acc_impl {Φ m1 m2} i x1 x2 :
    m1 !! i = Some x1 →
    m2 !! i = Some x2 →
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) -∗
    (* We obtain [Φ] for [x1] and [x2] *)
    Φ i x1 x2 ∗
    (* We reobtain the bigop for a predicate [Ψ] selected by the user *)
    ∀ Ψ,
      □ (∀ k y1 y2,
        ⌜ m1 !! k = Some y1 ⌝ → ⌜ m2 !! k = Some y2 ⌝ → ⌜ k ≠ i ⌝ →
        Φ k y1 y2 -∗ Ψ k y1 y2) -∗
      Ψ i x1 x2 -∗
      [∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2.
Proof.
    intros. rewrite big_sepM2_delete //. apply entails_wand, sep_mono_r, forall_intro=> Ψ.
    apply wand_intro_r, wand_intro_l.
    rewrite (big_sepM2_delete Ψ m1 m2 i) //. apply sep_mono_r.
    eapply wand_apply; [apply wand_entails, big_sepM2_impl|apply sep_mono_r].
    f_equiv; f_equiv=> k; f_equiv=> y1; f_equiv=> y2.
    rewrite !impl_curry -!pure_and !lookup_delete_Some.
    do 2 f_equiv. intros ?; naive_solver.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_later_1 `{!BiAffine PROP} Φ m1 m2 :
    (▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
    ⊢ ◇ ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2).
Proof.
    rewrite !big_sepM2_alt later_and (timeless ⌜_⌝).
    rewrite big_sepM_later except_0_and.
    auto using and_mono_r, except_0_intro.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_later_2 Φ m1 m2 :
    ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2)
    ⊢ ▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
Proof.
    rewrite !big_sepM2_alt later_and -(later_intro ⌜_⌝).
    apply and_mono_r. by rewrite big_opM_commute.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_laterN_2 Φ n m1 m2 :
    ([∗ map] k↦x1;x2 ∈ m1;m2, ▷^n Φ k x1 x2)
    ⊢ ▷^n [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
Proof.
    induction n as [|n IHn]; first done.
    rewrite later_laterN -IHn -big_sepM2_later_2.
    apply big_sepM2_mono. eauto.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_sepM (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
    (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ1 k y1 ∗ Φ2 k y2) ⊣⊢
    ([∗ map] k↦y1 ∈ m1, Φ1 k y1) ∗ ([∗ map] k↦y2 ∈ m2, Φ2 k y2).
Proof.
    intros.
    rewrite -big_sepM_sep_zip // big_sepM2_alt_lookup pure_True // left_id //.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_sepM_2 (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
    (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
    ([∗ map] k↦y1 ∈ m1, Φ1 k y1) -∗
    ([∗ map] k↦y2 ∈ m2, Φ2 k y2) -∗
    [∗ map] k↦y1;y2 ∈ m1;m2, Φ1 k y1 ∗ Φ2 k y2.
Proof. intros. apply entails_wand, wand_intro_r. by rewrite big_sepM2_sepM. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_union_inv_l (Φ : K → A → B → PROP) m1 m2 m' :
    m1 ##ₘ m2 →
    ([∗ map] k↦x;y ∈ (m1 ∪ m2);m', Φ k x y)
    ⊢ ∃ m1' m2', ⌜m' = m1' ∪ m2'⌝ ∧ ⌜ m1' ##ₘ m2' ⌝ ∧
                 ([∗ map] k↦x;y ∈ m1;m1', Φ k x y) ∗
                 ([∗ map] k↦x;y ∈ m2;m2', Φ k x y).
Proof.
    revert m'. induction m1 as [|i x m1 ? IH] using map_ind;
      intros m' ?; decompose_map_disjoint.
    { rewrite -(exist_intro ∅) -(exist_intro m') !left_id_L.
      rewrite !pure_True //; last by apply map_disjoint_empty_l.
      rewrite big_sepM2_empty !left_id //. }
    rewrite -insert_union_l big_sepM2_delete_l; last by apply lookup_insert_eq.
    apply exist_elim=> y. apply pure_elim_l=> ?.
    rewrite delete_insert_id; last by apply lookup_union_None.
    rewrite IH //.
    rewrite sep_exist_l. eapply exist_elim=> m1'.
    rewrite sep_exist_l. eapply exist_elim=> m2'.
    rewrite comm. apply wand_elim_l', pure_elim_l=> Hm'. apply pure_elim_l=> ?.
    assert ((m1' ∪ m2') !! i = None) as [??]%lookup_union_None.
    { by rewrite -Hm' lookup_delete_eq. }
    apply wand_intro_l.
    rewrite -(exist_intro (<[i:=y]> m1')) -(exist_intro m2'). apply and_intro.
    { apply pure_intro. by rewrite -insert_union_l -Hm' insert_delete_id. }
    apply and_intro.
    { apply pure_intro. by apply map_disjoint_insert_l. }
    by rewrite big_sepM2_insert // -assoc.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_union_inv_r `{Countable K} {A B}
      (Φ : K → A → B → PROP) (m1 m2 : gmap K B) (m' : gmap K A) :
  m1 ##ₘ m2 →
  ([∗ map] k↦x;y ∈ m';(m1 ∪ m2), Φ k x y)
    ⊢ ∃ m1' m2', ⌜ m' = m1' ∪ m2' ⌝ ∧ ⌜ m1' ##ₘ m2' ⌝ ∧
               ([∗ map] k↦x;y ∈ m1';m1, Φ k x y) ∗
               ([∗ map] k↦x;y ∈ m2';m2, Φ k x y).
Proof.
  intros Hm. rewrite -(big_sepM2_flip Φ).
  rewrite (big_sepM2_union_inv_l (λ k (x : B) y, Φ k y x)) //.
  f_equiv=>n1. f_equiv=>n2. f_equiv.
  by rewrite -!(big_sepM2_flip Φ).
Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_sepM2_diag `{Countable K} {A} (Φ : K → A → A → PROP) (m : gmap K A) :
  ([∗ map] k↦y ∈ m, Φ k y y) ⊢
  ([∗ map] k↦y1;y2 ∈ m;m, Φ k y1 y2).
Proof.
  rewrite big_sepM2_alt. rewrite pure_True; last naive_solver. rewrite left_id.
  rewrite map_zip_diag big_sepM_fmap. done.
Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_ne_2 `{Countable K} (A B : ofe)
    (Φ Ψ : K → A → B → PROP) m1 m2 m1' m2' n :
  m1 ≡{n}≡ m1' → m2 ≡{n}≡ m2' →
  (∀ k y1 y1' y2 y2',
    m1 !! k = Some y1 → m1' !! k = Some y1' → y1 ≡{n}≡ y1' →
    m2 !! k = Some y2 → m2' !! k = Some y2' → y2 ≡{n}≡ y2' →
    Φ k y1 y2 ≡{n}≡ Ψ k y1' y2') →
  ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2)%I ≡{n}≡ ([∗ map] k ↦ y1;y2 ∈ m1';m2', Ψ k y1 y2)%I.
Proof.
  intros Hm1 Hm2 Hf. rewrite !big_sepM2_alt. f_equiv.
  { by rewrite Hm1 Hm2. }
  apply big_opM_ne_2; [by f_equiv|].
  intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some
    (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some [??]; naive_solver.
Qed.
(* iris/bi/big_op.v *)
(* The lemmas [big_sepS_mono], [big_sepS_ne] and [big_sepS_proper] are more
  generic than the instances as they also give [x ∈ X] in the premise. *)
Lemma big_sepS_mono Φ Ψ X :
    (∀ x, x ∈ X → Φ x ⊢ Ψ x) →
    ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ X, Ψ x.
Proof. intros. apply big_opS_gen_proper; apply _ || auto. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_ne Φ Ψ X n :
    (∀ x, x ∈ X → Φ x ≡{n}≡ Ψ x) →
    ([∗ set] x ∈ X, Φ x)%I ≡{n}≡ ([∗ set] x ∈ X, Ψ x)%I.
Proof. apply big_opS_ne. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_proper Φ Ψ X :
    (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) →
    ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ set] x ∈ X, Ψ x).
Proof. apply big_opS_proper. Qed.
(* iris/bi/big_op.v *)
(* No need to declare instances for non-expansiveness and properness, we
  get both from the generic [big_opS] instances. *)
Instance big_sepS_mono' :
    Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (@bi_sep PROP) (A:=A)).
Proof. intros f g Hf m ? <-. by apply big_sepS_mono. Qed.
(* iris/bi/big_op.v *)
Instance big_sepS_flip_mono' :
    Proper (pointwise_relation _ (flip (⊢)) ==> (=) ==> flip (⊢))
           (big_opS (@bi_sep PROP) (A:=A)).
Proof. solve_proper. Qed.
(* iris/bi/big_op.v *)
Instance big_sepS_empty_persistent Φ :
    Persistent ([∗ set] x ∈ ∅, Φ x).
Proof. rewrite big_opS_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_persistent Φ X :
    (∀ x, x ∈ X → Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
Proof. apply big_opS_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepS_persistent' Φ X :
    (∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
Proof. intros; apply big_sepS_persistent, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepS_empty_affine Φ : Affine ([∗ set] x ∈ ∅, Φ x).
Proof. rewrite big_opS_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_affine Φ X :
    (∀ x, x ∈ X → Affine (Φ x)) → Affine ([∗ set] x ∈ X, Φ x).
Proof. apply big_opS_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepS_affine' Φ X :
    (∀ x, Affine (Φ x)) → Affine ([∗ set] x ∈ X, Φ x).
Proof. intros; apply big_sepS_affine, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepS_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
    Timeless ([∗ set] x ∈ ∅, Φ x).
Proof. rewrite big_opS_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_timeless `{!Timeless (emp%I : PROP)} Φ X :
    (∀ x, x ∈ X → Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
Proof. apply big_opS_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepS_timeless' `{!Timeless (emp%I : PROP)} Φ X :
    (∀ x, Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
Proof. intros; apply big_sepS_timeless, _. Qed.
(* iris/bi/big_op.v *)
(* See comment above [big_sepM_subseteq] as for why the [Affine]
     instance is placed late. *)
Lemma big_sepS_subseteq Φ X Y `{!∀ x, Affine (Φ x)} :
    Y ⊆ X → ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Φ x.
Proof.
    intros ->%union_difference_L. rewrite big_opS_union; last set_solver.
    by rewrite sep_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_elements Φ X :
    ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ list] x ∈ elements X, Φ x).
Proof. by rewrite big_opS_elements. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ emp.
Proof. by rewrite big_opS_empty. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_empty' P `{!Affine P} Φ : P ⊢ [∗ set] x ∈ ∅, Φ x.
Proof. rewrite big_sepS_empty. apply: affine. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_emp X : ([∗ set] x ∈ X, emp) ⊣⊢@{PROP} emp.
Proof. by rewrite big_opS_unit. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_insert Φ X x :
    x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ∗ [∗ set] y ∈ X, Φ y).
Proof. apply big_opS_insert. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_fn_insert {B} (Ψ : A → B → PROP) f X x b :
    x ∉ X →
       ([∗ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y))
    ⊣⊢ (Ψ x b ∗ [∗ set] y ∈ X, Ψ y (f y)).
Proof. apply big_opS_fn_insert. Qed.
(* iris/bi/big_op.v *)
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_opS_fn_insert'. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_union Φ X Y :
    X ## Y →
    ([∗ set] y ∈ X ∪ Y, Φ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ Y, Φ y).
Proof. apply big_opS_union. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_delete Φ X x :
    x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y.
Proof. apply big_opS_delete. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_insert_2 {Φ X} x
    `{!TCOr (Affine (Φ x)) (Absorbing (Φ x))} :
    Φ x ⊢ ([∗ set] y ∈ X, Φ y) -∗ ([∗ set] y ∈ {[ x ]} ∪ X, Φ y).
Proof.
    apply wand_intro_r. destruct (decide (x ∈ X)); last first.
    { rewrite -big_sepS_insert //. }
    rewrite big_sepS_delete // assoc.
    rewrite (sep_elim_l (Φ x)) -big_sepS_insert; last set_solver.
    rewrite -union_difference_singleton_L //.
    replace ({[x]} ∪ X) with X by set_solver.
    auto.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_insert_2' {Φ X} x
    `{!TCOr (Affine (Φ x)) (Absorbing (Φ x))} :
    Φ x -∗ ([∗ set] y ∈ X, Φ y) -∗ ([∗ set] y ∈ X ∪ {[ x ]}, Φ y).
Proof. apply entails_wand. rewrite comm_L. by apply big_sepS_insert_2. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_union_2 {Φ} X Y
    `{!∀ x, TCOr (Affine (Φ x)) (Absorbing (Φ x))} :
    ([∗ set] y ∈ X, Φ y) -∗ ([∗ set] y ∈ Y, Φ y) -∗ ([∗ set] y ∈ X ∪ Y, Φ y).
Proof.
    apply entails_wand, wand_intro_r. induction X as [|x X ? IH] using set_ind_L.
    { by rewrite left_id_L big_sepS_empty left_id. }
    rewrite big_sepS_insert // -assoc IH -assoc_L.
    destruct (decide (x ∈ Y)).
    { replace ({[x]} ∪ (X ∪ Y)) with (X ∪ Y) by set_solver.
      rewrite (big_sepS_delete _ _ x); last set_solver.
      by rewrite assoc sep_elim_r. }
    by rewrite big_sepS_insert; last set_solver.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_delete_2 {Φ X} x :
    Affine (Φ x) →
    Φ x ⊢ ([∗ set] y ∈ X ∖ {[ x ]}, Φ y) -∗ [∗ set] y ∈ X, Φ y.
Proof.
    intros Haff. apply wand_intro_r. destruct (decide (x ∈ X)).
    { rewrite -big_sepS_delete //. }
    rewrite sep_elim_r.
    replace (X ∖ {[x]}) with X by set_solver.
    auto.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_elem_of Φ X x
    `{!TCOr (∀ y, Affine (Φ y)) (Absorbing (Φ x))} :
    x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x.
Proof.
    intros ?. rewrite big_sepS_delete //.
    destruct select (TCOr _ _); by rewrite sep_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_elem_of_acc Φ X x :
    x ∈ X →
    ([∗ set] y ∈ X, Φ y) ⊢ Φ x ∗ (Φ x -∗ ([∗ set] y ∈ X, Φ y)).
Proof.
    intros. rewrite big_sepS_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
Proof. apply big_opS_singleton. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_filter' (φ : A → Prop) `{∀ x, Decision (φ x)} Φ X :
    ([∗ set] y ∈ filter φ X, Φ y)
    ⊣⊢ ([∗ set] y ∈ X, if decide (φ y) then Φ y else emp).
Proof. apply: big_opS_filter'. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_filter `{!BiAffine PROP}
      (φ : A → Prop) `{∀ x, Decision (φ x)} Φ X :
    ([∗ set] y ∈ filter φ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜φ y⌝ → Φ y).
Proof. setoid_rewrite <-decide_emp. apply big_sepS_filter'. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_filter_acc' (φ : A → Prop) `{∀ y, Decision (φ y)} Φ X Y :
    (∀ y, y ∈ Y → φ y → y ∈ X) →
    ([∗ set] y ∈ X, Φ y) -∗
      ([∗ set] y ∈ Y, if decide (φ y) then Φ y else emp) ∗
      (([∗ set] y ∈ Y, if decide (φ y) then Φ y else emp) -∗ [∗ set] y ∈ X, Φ y).
Proof.
    intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter φ Y) X))
      as (Z&->&?); first set_solver.
    rewrite big_sepS_union // big_sepS_filter'.
    by apply entails_wand, sep_mono_r, wand_intro_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_filter_acc `{!BiAffine PROP}
      (φ : A → Prop) `{∀ y, Decision (φ y)} Φ X Y :
    (∀ y, y ∈ Y → φ y → y ∈ X) →
    ([∗ set] y ∈ X, Φ y) -∗
      ([∗ set] y ∈ Y, ⌜φ y⌝ → Φ y) ∗
      (([∗ set] y ∈ Y, ⌜φ y⌝ → Φ y) -∗ [∗ set] y ∈ X, Φ y).
Proof. intros. setoid_rewrite <-decide_emp. by apply big_sepS_filter_acc'. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_list_to_set Φ (l : list A) :
    NoDup l →
    ([∗ set] x ∈ list_to_set l, Φ x) ⊣⊢ [∗ list] x ∈ l, Φ x.
Proof. apply big_opS_list_to_set. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_sep Φ Ψ X :
    ([∗ set] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ X, Ψ y).
Proof. apply big_opS_op. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_sep_2 Φ Ψ X :
    ([∗ set] y ∈ X, Φ y) -∗
    ([∗ set] y ∈ X, Ψ y) -∗
    ([∗ set] y ∈ X, Φ y ∗ Ψ y).
Proof. apply entails_wand, wand_intro_r. rewrite big_sepS_sep //. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_and Φ Ψ X :
    ([∗ set] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ set] y ∈ X, Φ y) ∧ ([∗ set] y ∈ X, Ψ y).
Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_pure_1 (φ : A → Prop) X :
    ([∗ set] y ∈ X, ⌜φ y⌝) ⊢@{PROP} ⌜set_Forall φ X⌝.
Proof.
    induction X as [|x X ? IH] using set_ind_L.
    { apply pure_intro, set_Forall_empty. }
    rewrite big_sepS_insert // IH sep_and -pure_and.
    f_equiv=>-[Hx HX]. apply set_Forall_union.
    - apply set_Forall_singleton. done.
    - done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_affinely_pure_2 (φ : A → Prop) X :
    <affine> ⌜set_Forall φ X⌝ ⊢@{PROP} ([∗ set] y ∈ X, <affine> ⌜φ y⌝).
Proof.
    induction X as [|x X ? IH] using set_ind_L.
    { rewrite big_sepS_empty. apply affinely_elim_emp. }
    rewrite big_sepS_insert // -IH.
    rewrite -persistent_and_sep_1 -affinely_and -pure_and.
    f_equiv. f_equiv=>HX. split.
    - apply HX. set_solver+.
    - apply set_Forall_union_inv_2 in HX. done.
  Qed.
(* iris/bi/big_op.v *)
(* The general backwards direction requires [BiAffine] to cover the empty case. *)
Lemma big_sepS_pure `{!BiAffine PROP} (φ : A → Prop) X :
    ([∗ set] y ∈ X, ⌜φ y⌝) ⊣⊢@{PROP} ⌜set_Forall φ X⌝.
Proof.
    apply (anti_symm (⊢)); first by apply big_sepS_pure_1.
    rewrite -(affine_affinely ⌜_⌝%I).
    rewrite big_sepS_affinely_pure_2. by setoid_rewrite affinely_elim.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_persistently `{!BiAffine PROP} Φ X :
    <pers> ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, <pers> (Φ y).
Proof. apply (big_opS_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_intro Φ X :
    □ (∀ x, ⌜x ∈ X⌝ → Φ x) ⊢ [∗ set] x ∈ X, Φ x.
Proof.
    revert Φ. induction X as [|x X ? IH] using set_ind_L=> Φ.
    { by rewrite (affine (□ _)) big_sepS_empty. }
    rewrite intuitionistically_sep_dup big_sepS_insert //. f_equiv.
    - rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
      by rewrite intuitionistically_elim.
    - rewrite -IH. f_equiv. apply forall_mono=> y.
      apply impl_intro_l, pure_elim_l=> ?.
      by rewrite pure_True ?True_impl; last set_solver.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_forall `{!BiAffine PROP} Φ X :
    (∀ x, Persistent (Φ x)) →
    ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> x.
      apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepS_elem_of. }
    revert Φ HΦ. induction X as [|x X ? IH] using set_ind_L=> Φ HΦ.
    { rewrite big_sepS_empty. apply: affine. }
    rewrite big_sepS_insert // -persistent_and_sep_1. apply and_intro.
    - rewrite (forall_elim x) pure_True ?True_impl; last set_solver. done.
    - rewrite -IH. apply forall_mono=> y.
      apply impl_intro_l, pure_elim_l=> ?.
      by rewrite pure_True ?True_impl; last set_solver.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_impl Φ Ψ X :
    ([∗ set] x ∈ X, Φ x) -∗
    □ (∀ x, ⌜x ∈ X⌝ → Φ x -∗ Ψ x) -∗
    [∗ set] x ∈ X, Ψ x.
Proof.
    apply entails_wand, wand_intro_l. rewrite big_sepS_intro -big_sepS_sep.
    by setoid_rewrite wand_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_wand Φ Ψ X :
    ([∗ set] x ∈ X, Φ x) -∗
    ([∗ set] x ∈ X, Φ x -∗ Ψ x) -∗
    [∗ set] x ∈ X, Ψ x.
Proof.
    apply entails_wand, wand_intro_r. rewrite -big_sepS_sep.
    setoid_rewrite wand_elim_r. done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_elem_of_acc_impl {Φ X} x :
    x ∈ X →
    ([∗ set] y ∈ X, Φ y) -∗
    (* we get [Φ] for the element [x] *)
    Φ x ∗
    (* we reobtain the bigop for a predicate [Ψ] selected by the user *)
    ∀ Ψ,
      □ (∀ y, ⌜ y ∈ X ⌝ → ⌜ x ≠ y ⌝ → Φ y -∗ Ψ y) -∗
      Ψ x -∗
      [∗ set] y ∈ X, Ψ y.
Proof.
    intros. rewrite big_sepS_delete //. apply entails_wand, sep_mono_r, forall_intro=> Ψ.
    apply wand_intro_r, wand_intro_l.
    rewrite (big_sepS_delete Ψ X x) //. apply sep_mono_r.
    eapply wand_apply; [apply wand_entails, big_sepS_impl|apply sep_mono_r].
    f_equiv; f_equiv=> y. rewrite impl_curry -pure_and.
    do 2 f_equiv. intros ?; set_solver.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_dup P `{!Affine P} X :
    □ (P -∗ P ∗ P) -∗ P -∗ [∗ set] x ∈ X, P.
Proof.
    apply entails_wand, wand_intro_l. induction X as [|x X ? IH] using set_ind_L.
    { apply: big_sepS_empty'. }
    rewrite !big_sepS_insert //.
    rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
    rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_later `{!BiAffine PROP} Φ X :
    ▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y).
Proof. apply (big_opS_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_later_2 Φ X :
    ([∗ set] y ∈ X, ▷ Φ y) ⊢ ▷ ([∗ set] y ∈ X, Φ y).
Proof. by rewrite big_opS_commute. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_laterN `{!BiAffine PROP} Φ n X :
    ▷^n ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷^n Φ y).
Proof. apply (big_opS_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_laterN_2 Φ n X :
    ([∗ set] y ∈ X, ▷^n Φ y) ⊢ ▷^n ([∗ set] y ∈ X, Φ y).
Proof. by rewrite big_opS_commute. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_dom `{Countable K} {A} (Φ : K → PROP) (m : gmap K A) :
  ([∗ map] k↦_ ∈ m, Φ k) ⊣⊢ ([∗ set] k ∈ dom m, Φ k).
Proof. apply big_opM_dom. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_set_to_map `{Countable K} {A}
    (Φ : K → A → PROP) (X : gset K) (g : K → A) :
  ([∗ map] k↦a ∈ set_to_map g X, Φ k a) ⊣⊢ ([∗ set] k ∈ X, Φ k (g k)).
Proof. apply big_opM_set_to_map. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_gset_to_gmap `{Countable K} {A} (Φ : K → A → PROP) (X : gset K) c :
  ([∗ map] k↦a ∈ gset_to_gmap c X, Φ k a) ⊣⊢ ([∗ set] k ∈ X, Φ k c).
Proof. apply big_opM_gset_to_gmap. Qed.
(* iris/bi/big_op.v *)
(* The lemmas [big_sepMS_mono], [big_sepMS_ne] and [big_sepMS_proper] are more
  generic than the instances as they also give [l !! k = Some y] in the premise. *)
Lemma big_sepMS_mono Φ Ψ X :
    (∀ x, x ∈ X → Φ x ⊢ Ψ x) →
    ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ X, Ψ x.
Proof. intros. apply big_opMS_gen_proper; apply _ || auto. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_ne Φ Ψ X n :
    (∀ x, x ∈ X → Φ x ≡{n}≡ Ψ x) →
    ([∗ mset] x ∈ X, Φ x)%I ≡{n}≡ ([∗ mset] x ∈ X, Ψ x)%I.
Proof. apply big_opMS_ne. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_proper Φ Ψ X :
    (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) →
    ([∗ mset] x ∈ X, Φ x) ⊣⊢ ([∗ mset] x ∈ X, Ψ x).
Proof. apply big_opMS_proper. Qed.