phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/big_op.v *)
Lemma big_orL_bind {B} (f : A → list B) (Φ : B → PROP) l :
    ([∨ list] y ∈ l ≫= f, Φ y) ⊣⊢ ([∨ list] x ∈ l, [∨ list] y ∈ f x, Φ y).
Proof. by rewrite big_opL_bind. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_or Φ Ψ l :
    ([∨ list] k↦x ∈ l, Φ k x ∨ Ψ k x)
    ⊣⊢ ([∨ list] k↦x ∈ l, Φ k x) ∨ ([∨ list] k↦x ∈ l, Ψ k x).
Proof. by rewrite big_opL_op. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_persistently Φ l :
    <pers> ([∨ list] k↦x ∈ l, Φ k x) ⊣⊢ [∨ list] k↦x ∈ l, <pers> (Φ k x).
Proof. apply (big_opL_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_exist Φ l :
    ([∨ list] k↦x ∈ l, Φ k x) ⊣⊢ (∃ k x, ⌜l !! k = Some x⌝ ∧ Φ k x).
Proof.
    apply (anti_symm _).
    { revert Φ. induction l as [|x l IH]=> Φ.
      { rewrite big_orL_nil. apply False_elim. }
      rewrite big_orL_cons. apply or_elim.
      - by rewrite -(exist_intro 0) -(exist_intro x) pure_True // left_id.
      - rewrite IH. apply exist_elim=> k. by rewrite -(exist_intro (S k)). }
    apply exist_elim=> k; apply exist_elim=> x. apply pure_elim_l=> ?.
    by apply: big_orL_intro.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_pure (φ : nat → A → Prop) l :
    ([∨ list] k↦x ∈ l, ⌜φ k x⌝) ⊣⊢@{PROP} ⌜∃ k x, l !! k = Some x ∧ φ k x⌝.
Proof.
    rewrite big_orL_exist.
    rewrite pure_exist. apply exist_proper=>k.
    rewrite pure_exist. apply exist_proper=>x.
    rewrite -pure_and. done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_sep_l P Φ l :
    P ∗ ([∨ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∨ list] k↦x ∈ l, P ∗ Φ k x).
Proof.
    rewrite !big_orL_exist sep_exist_l.
    f_equiv=> k. rewrite sep_exist_l. f_equiv=> x.
    by rewrite !persistent_and_affinely_sep_l !assoc (comm _ P).
 Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_sep_r Q Φ l :
    ([∨ list] k↦x ∈ l, Φ k x) ∗ Q ⊣⊢ ([∨ list] k↦x ∈ l, Φ k x ∗ Q).
Proof. setoid_rewrite (comm bi_sep). apply big_orL_sep_l. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_later Φ l :
    l ≠ [] →
    ▷ ([∨ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∨ list] k↦x ∈ l, ▷ Φ k x).
Proof. apply (big_opL_commute1 _). Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_laterN Φ n l :
    l ≠ [] →
    ▷^n ([∨ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∨ list] k↦x ∈ l, ▷^n Φ k x).
Proof. apply (big_opL_commute1 _). Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_zip_seq (Φ : nat * A → PROP) n len l :
    length l ≤ len →
    ([∨ list] ky ∈ zip (seq n len) l, Φ ky) ⊣⊢
    ([∨ list] k ↦ y ∈ l, Φ (n + k, y)).
Proof. apply big_opL_zip_seq. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_zip_seqZ (Φ : Z * A → PROP) n len l :
    length l ≤ len →
    ([∨ list] ky ∈ zip (seqZ n len) l, Φ ky) ⊣⊢
    ([∨ list] k ↦ y ∈ l, Φ ((n + k)%Z, y)).
Proof. apply big_opL_zip_seqZ. Qed.
(* iris/bi/big_op.v *)
(* The lemmas [big_sepM_mono], [big_sepM_ne] and [big_sepM_proper] are more
  generic than the instances as they also give [l !! k = Some y] in the premise. *)
Lemma big_sepM_mono Φ Ψ m :
    (∀ k x, m !! k = Some x → Φ k x ⊢ Ψ k x) →
    ([∗ map] k ↦ x ∈ m, Φ k x) ⊢ [∗ map] k ↦ x ∈ m, Ψ k x.
Proof. apply big_opM_gen_proper; apply _ || auto. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_ne Φ Ψ m n :
    (∀ k x, m !! k = Some x → Φ k x ≡{n}≡ Ψ k x) →
    ([∗ map] k ↦ x ∈ m, Φ k x)%I ≡{n}≡ ([∗ map] k ↦ x ∈ m, Ψ k x)%I.
Proof. apply big_opM_ne. Qed.
(* iris/bi/big_op.v *)
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. apply big_opM_proper. Qed.
(* iris/bi/big_op.v *)
(* No need to declare instances for non-expansiveness and properness, we
  get both from the generic [big_opM] instances. *)
Instance big_sepM_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
           (big_opM (@bi_sep PROP) (K:=K) (A:=A)).
Proof. intros f g Hf m ? <-. apply big_sepM_mono; intros; apply Hf. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM_flip_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ (flip (⊢))) ==> (=) ==> flip (⊢))
           (big_opM (@bi_sep PROP) (K:=K) (A:=A)).
Proof. solve_proper. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM_empty_persistent Φ :
    Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
Proof. rewrite big_opM_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_persistent Φ m :
    (∀ k x, m !! k = Some x → Persistent (Φ k x)) →
    Persistent ([∗ map] k↦x ∈ m, Φ k x).
Proof. apply big_opM_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM_persistent' Φ m :
    (∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x).
Proof. intros; apply big_sepM_persistent, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM_empty_affine Φ :
    Affine ([∗ map] k↦x ∈ ∅, Φ k x).
Proof. rewrite big_opM_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_affine Φ m :
    (∀ k x, m !! k = Some x → Affine (Φ k x)) →
    Affine ([∗ map] k↦x ∈ m, Φ k x).
Proof. apply big_opM_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM_affine' Φ m :
    (∀ k x, Affine (Φ k x)) → Affine ([∗ map] k↦x ∈ m, Φ k x).
Proof. intros; apply big_sepM_affine, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
    Timeless ([∗ map] k↦x ∈ ∅, Φ k x).
Proof. rewrite big_opM_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
    (∀ k x, m !! k = Some x → Timeless (Φ k x)) →
    Timeless ([∗ map] k↦x ∈ m, Φ k x).
Proof. apply big_opM_closed; apply _. Qed.
(* iris/bi/big_op.v *)
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_sepM_timeless, _. Qed.
(* iris/bi/big_op.v *)
(* We place the [Affine] instance after [m1] and [m2], so that
     manually instantiating [m1] or [m2] in [iApply] does not also
     implicitly instantiate the [Affine] instance. If it gets
     instantiated too early, [Φ] is not known, and typeclass inference
     fails. *)
Lemma big_sepM_subseteq Φ m1 m2 `{!∀ k x, Affine (Φ k x)} :
    m2 ⊆ m1 → ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Φ k x.
Proof.
    intros ?. rewrite -(map_difference_union m2 m1) //.
    rewrite big_opM_union; last by apply map_disjoint_difference_r1.
    assert (∀ kx, Affine (uncurry Φ kx)) by (intros []; apply _).
    by rewrite sep_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ emp.
Proof. by rewrite big_opM_empty. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_empty' P `{!Affine P} Φ : P ⊢ [∗ map] k↦x ∈ ∅, Φ k x.
Proof. rewrite big_sepM_empty. apply: affine. Qed.
(* iris/bi/big_op.v *)
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. apply big_opM_insert. Qed.
(* iris/bi/big_op.v *)
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. apply big_opM_delete. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_insert_delete Φ m i x :
    ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y.
Proof. apply big_opM_insert_delete. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_insert_2 Φ m i x
    `{!TCOr (∀ y, Affine (Φ i y)) (Absorbing (Φ i x))} :
    Φ i x ⊢ ([∗ map] k↦y ∈ m, Φ k y) -∗ [∗ map] k↦y ∈ <[i:=x]> m, Φ k y.
Proof.
    apply wand_intro_r. destruct (m !! i) as [y|] eqn:Hi; last first.
    { by rewrite -big_sepM_insert. }
    assert (TCOr (Affine (Φ i y)) (Absorbing (Φ i x))).
    { destruct select (TCOr _ _); apply _. }
    rewrite big_sepM_delete // assoc.
    rewrite (sep_elim_l (Φ i x)) -big_sepM_insert ?lookup_delete_eq //.
    by rewrite insert_delete_eq.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_lookup_acc Φ m i x :
    m !! i = Some x →
    ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x ∗ (Φ i x -∗ ([∗ map] k↦y ∈ m, Φ k y)).
Proof.
    intros. rewrite big_sepM_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_lookup Φ m i x
    `{!TCOr (∀ j y, Affine (Φ j y)) (Absorbing (Φ i x))} :
    m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x.
Proof.
    intros Hi. destruct select (TCOr _ _).
    - rewrite big_sepM_delete // sep_elim_l //.
    - rewrite big_sepM_lookup_acc // sep_elim_l //.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_lookup_dom (Φ : K → PROP) m i
    `{!TCOr (∀ j, Affine (Φ j)) (Absorbing (Φ i))} :
    is_Some (m !! i) → ([∗ map] k↦_ ∈ m, Φ k) ⊢ Φ i.
Proof. intros [x ?]. destruct select (TCOr _ _); by apply: big_sepM_lookup. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_singleton Φ i x : ([∗ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
Proof. by rewrite big_opM_singleton. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → PROP) m :
    ([∗ map] k↦y ∈ f <$> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, Φ k (f y)).
Proof. by rewrite big_opM_fmap. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_omap {B} (f : A → option B) (Φ : K → B → PROP) m :
    ([∗ map] k↦y ∈ omap f m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, from_option (Φ k) emp (f y)).
Proof. by rewrite big_opM_omap. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_insert_override Φ m i x x' :
    m !! i = Some x → (Φ i x ⊣⊢ Φ i x') →
    ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, Φ k y).
Proof. apply big_opM_insert_override. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_insert_override_1 Φ m i x x' :
    m !! i = Some x →
    ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y) ⊢
      (Φ i x' -∗ Φ i x) -∗ ([∗ map] k↦y ∈ m, Φ k y).
Proof.
    intros ?. apply wand_intro_l.
    rewrite -insert_delete_eq big_sepM_insert ?lookup_delete_eq //.
    by rewrite assoc wand_elim_l -big_sepM_delete.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_insert_override_2 Φ m i x x' :
    m !! i = Some x →
    ([∗ map] k↦y ∈ m, Φ k y) ⊢
      (Φ i x -∗ Φ i x') -∗ ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y).
Proof.
    intros ?. apply wand_intro_l.
    rewrite {1}big_sepM_delete //; rewrite assoc wand_elim_l.
    rewrite -insert_delete_eq big_sepM_insert ?lookup_delete_eq //.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_insert_acc Φ m i x :
    m !! i = Some x →
    ([∗ map] k↦y ∈ m, Φ k y) ⊢
      Φ i x ∗ (∀ x', Φ i x' -∗ ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y)).
Proof.
    intros ?. rewrite {1}big_sepM_delete //. apply sep_mono; [done|].
    apply forall_intro=> x'.
    rewrite -insert_delete_eq big_sepM_insert ?lookup_delete_eq //.
    by apply wand_intro_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → PROP) (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. apply big_opM_fn_insert. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_fn_insert' (Φ : K → PROP) 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_opM_fn_insert'. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_filter' (φ : K * A → Prop) `{∀ kx, Decision (φ kx)} Φ m :
    ([∗ map] k ↦ x ∈ filter φ m, Φ k x) ⊣⊢
    ([∗ map] k ↦ x ∈ m, if decide (φ (k, x)) then Φ k x else emp).
Proof. apply: big_opM_filter'. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_filter `{!BiAffine PROP}
      (φ : K * A → Prop) `{∀ kx, Decision (φ kx)} Φ m :
    ([∗ map] k ↦ x ∈ filter φ m, Φ k x) ⊣⊢
    ([∗ map] k ↦ x ∈ m, ⌜φ (k, x)⌝ → Φ k x).
Proof. setoid_rewrite <-decide_emp. apply big_sepM_filter'. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_union Φ m1 m2 :
    m1 ##ₘ m2 →
    ([∗ map] k↦y ∈ m1 ∪ m2, Φ k y)
    ⊣⊢ ([∗ map] k↦y ∈ m1, Φ k y) ∗ ([∗ map] k↦y ∈ m2, Φ k y).
Proof. apply big_opM_union. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_sep Φ Ψ m :
    ([∗ map] k↦x ∈ m, Φ k x ∗ Ψ k x)
    ⊣⊢ ([∗ map] k↦x ∈ m, Φ k x) ∗ ([∗ map] k↦x ∈ m, Ψ k x).
Proof. apply big_opM_op. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_sep_2 Φ Ψ m :
    ([∗ map] k↦x ∈ m, Φ k x) -∗
    ([∗ map] k↦x ∈ m, Ψ k x) -∗
    ([∗ map] k↦x ∈ m, Φ k x ∗ Ψ k x).
Proof. apply entails_wand, wand_intro_r. rewrite big_sepM_sep //. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_and Φ Ψ m :
    ([∗ map] k↦x ∈ m, Φ k x ∧ Ψ k x)
    ⊢ ([∗ map] k↦x ∈ m, Φ k x) ∧ ([∗ map] k↦x ∈ m, Ψ k x).
Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_pure_1 (φ : K → A → Prop) m :
    ([∗ map] k↦x ∈ m, ⌜φ k x⌝) ⊢@{PROP} ⌜map_Forall φ m⌝.
Proof.
    induction m as [|k x m ? IH] using map_ind.
    { apply pure_intro, map_Forall_empty. }
    rewrite big_sepM_insert // IH sep_and -pure_and.
    by rewrite -map_Forall_insert.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_affinely_pure_2 (φ : K → A → Prop) m :
    <affine> ⌜map_Forall φ m⌝ ⊢@{PROP} ([∗ map] k↦x ∈ m, <affine> ⌜φ k x⌝).
Proof.
    induction m as [|k x m ? IH] using map_ind.
    { rewrite big_sepM_empty. apply affinely_elim_emp. }
    rewrite big_sepM_insert // -IH.
    by rewrite -persistent_and_sep_1 -affinely_and -pure_and map_Forall_insert.
  Qed.
(* iris/bi/big_op.v *)
(* The general backwards direction requires [BiAffine] to cover the empty case. *)
Lemma big_sepM_pure `{!BiAffine PROP} (φ : K → A → Prop) m :
    ([∗ map] k↦x ∈ m, ⌜φ k x⌝) ⊣⊢@{PROP} ⌜map_Forall φ m⌝.
Proof.
    apply (anti_symm (⊢)); first by apply big_sepM_pure_1.
    rewrite -(affine_affinely ⌜_⌝).
    rewrite big_sepM_affinely_pure_2. by setoid_rewrite affinely_elim.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_persistently `{!BiAffine PROP} Φ m :
    (<pers> ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢ ([∗ map] k↦x ∈ m, <pers> (Φ k x)).
Proof. apply (big_opM_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_intro Φ m :
    □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x) ⊢ [∗ map] k↦x ∈ m, Φ k x.
Proof.
    revert Φ. induction m as [|i x m ? IH] using map_ind=> Φ.
    { by rewrite (affine (□ _)) big_sepM_empty. }
    rewrite big_sepM_insert // intuitionistically_sep_dup. f_equiv.
    - rewrite (forall_elim i) (forall_elim x) lookup_insert_eq.
      by rewrite pure_True // True_impl intuitionistically_elim.
    - rewrite -IH. f_equiv. apply forall_mono=> k; apply forall_mono=> y.
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
      by rewrite pure_True // True_impl.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_forall `{!BiAffine PROP} Φ m :
    (∀ k x, Persistent (Φ k x)) →
    ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x).
Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
      apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepM_lookup. }
    revert Φ HΦ. induction m as [|i x m ? IH] using map_ind=> Φ HΦ.
    { rewrite big_sepM_empty. apply: affine. }
    rewrite big_sepM_insert // -persistent_and_sep_1. apply and_intro.
    - rewrite (forall_elim i) (forall_elim x) lookup_insert_eq.
      by rewrite pure_True // True_impl.
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
      by rewrite pure_True // True_impl.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_impl Φ Ψ m :
    ([∗ map] k↦x ∈ m, Φ k x) -∗
    □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗
    [∗ map] k↦x ∈ m, Ψ k x.
Proof.
    apply entails_wand, wand_intro_l. rewrite big_sepM_intro -big_sepM_sep.
    by setoid_rewrite wand_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_wand Φ Ψ m :
    ([∗ map] k↦x ∈ m, Φ k x) -∗
    ([∗ map] k↦x ∈ m, Φ k x -∗ Ψ k x) -∗
    [∗ map] k↦x ∈ m, Ψ k x.
Proof.
    apply entails_wand, wand_intro_r. rewrite -big_sepM_sep.
    setoid_rewrite wand_elim_r. done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_dup P `{!Affine P} m :
    □ (P -∗ P ∗ P) -∗ P -∗ [∗ map] k↦x ∈ m, P.
Proof.
    apply entails_wand, wand_intro_l. induction m as [|i x m ? IH] using map_ind.
    { apply: big_sepM_empty'. }
    rewrite !big_sepM_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_sepM_lookup_acc_impl {Φ m} i x :
    m !! i = Some x →
    ([∗ map] k↦y ∈ m, Φ k y) -∗
    (* We obtain [Φ] for [x] *)
    Φ i x ∗
    (* We reobtain the bigop for a predicate [Ψ] selected by the user *)
    ∀ Ψ,
      □ (∀ k y, ⌜ m !! k = Some y ⌝ → ⌜ k ≠ i ⌝ → Φ k y -∗ Ψ k y) -∗
      Ψ i x -∗
      [∗ map] k↦y ∈ m, Ψ k y.
Proof.
    intros. rewrite big_sepM_delete //. apply entails_wand, sep_mono_r, forall_intro=> Ψ.
    apply wand_intro_r, wand_intro_l.
    rewrite (big_sepM_delete Ψ m i x) //. apply sep_mono_r.
    eapply wand_apply; [apply wand_entails, big_sepM_impl|apply sep_mono_r].
    f_equiv; f_equiv=> k; f_equiv=> y.
    rewrite impl_curry -pure_and lookup_delete_Some.
    do 2 f_equiv. intros ?; naive_solver.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_later `{!BiAffine PROP} Φ m :
    ▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x).
Proof. apply (big_opM_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_later_2 Φ m :
    ([∗ map] k↦x ∈ m, ▷ Φ k x) ⊢ ▷ [∗ map] k↦x ∈ m, Φ k x.
Proof. by rewrite big_opM_commute. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_laterN `{!BiAffine PROP} Φ n m :
    ▷^n ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷^n Φ k x).
Proof. apply (big_opM_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_laterN_2 Φ n m :
    ([∗ map] k↦x ∈ m, ▷^n Φ k x) ⊢ ▷^n [∗ map] k↦x ∈ m, Φ k x.
Proof. by rewrite big_opM_commute. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_map_to_list Φ m :
    ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ list] xk ∈ map_to_list m, Φ (xk.1) (xk.2).
Proof. apply big_opM_map_to_list. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_list_to_map Φ l :
    NoDup l.*1 →
    ([∗ map] k↦x ∈ list_to_map l, Φ k x) ⊣⊢ [∗ list] xk ∈ l, Φ (xk.1) (xk.2).
Proof. apply big_opM_list_to_map. Qed.
(* iris/bi/big_op.v *)
(* Some lemmas depend on the generalized versions of the above ones. *)
Lemma big_sepM_sep_zip_with `{Countable K} {A B C}
    (f : A → B → C) (g1 : C → A) (g2 : C → B)
    (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) 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)) →
  ([∗ map] k↦xy ∈ map_zip_with f m1 m2, Φ1 k (g1 xy) ∗ Φ2 k (g2 xy)) ⊣⊢
  ([∗ map] k↦x ∈ m1, Φ1 k x) ∗ ([∗ map] k↦y ∈ m2, Φ2 k y).
Proof. apply big_opM_sep_zip_with. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_sep_zip `{Countable K} {A B}
    (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
  (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
  ([∗ map] k↦xy ∈ map_zip m1 m2, Φ1 k xy.1 ∗ Φ2 k xy.2) ⊣⊢
  ([∗ map] k↦x ∈ m1, Φ1 k x) ∗ ([∗ map] k↦y ∈ m2, Φ2 k y).
Proof. apply big_opM_sep_zip. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_impl_strong `{Countable K} {A B}
    (Φ : K → A → PROP) (Ψ : K → B → PROP) (m1 : gmap K A) (m2 : gmap K B) :
  ([∗ map] k↦x ∈ m1, Φ k x) ⊢
  □ (∀ (k : K) (y : B),
    (if m1 !! k is Some x then Φ k x else emp) -∗
    ⌜m2 !! k = Some y⌝ →
    Ψ k y) -∗
  ([∗ map] k↦y ∈ m2, Ψ k y) ∗
  ([∗ map] k↦x ∈ filter (λ '(k, _), m2 !! k = None) m1, Φ k x).
Proof.
  apply wand_intro_r.
  revert m1. induction m2 as [|i y m ? IH] using map_ind=> m1.
  { rewrite big_sepM_empty left_id sep_elim_l.
    rewrite map_filter_id //. }
  rewrite big_sepM_insert; last done.
  rewrite intuitionistically_sep_dup.
  rewrite assoc. rewrite (comm _ _ (□ _))%I.
  rewrite {1}intuitionistically_elim {1}(forall_elim i) {1}(forall_elim y).
  rewrite lookup_insert_eq pure_True // left_id.
  destruct (m1 !! i) as [x|] eqn:Hx.
  - rewrite big_sepM_delete; last done.
    rewrite assoc assoc wand_elim_l -2!assoc. apply sep_mono_r.
    assert (filter (λ '(k, _), <[i:=y]> m !! k = None) m1
          = filter (λ '(k, _), m !! k = None) (delete i m1)) as ->.
    { apply map_filter_strong_ext_1=> k z.
      rewrite lookup_insert_None lookup_delete_Some. naive_solver. }
    rewrite -IH. do 2 f_equiv. f_equiv=> k. f_equiv=> z.
    apply wand_intro_r. apply impl_intro_l, pure_elim_l=> ?.
    assert (i ≠ k) by congruence.
    rewrite lookup_insert_ne // pure_True // left_id.
    rewrite lookup_delete_ne // wand_elim_l //.
  - rewrite left_id -assoc. apply sep_mono_r.
    assert (filter (λ '(k, _), <[i:=y]> m !! k = None) m1
          = filter (λ '(k, _), m !! k = None) m1) as ->.
    { apply map_filter_strong_ext_1=> k z.
      rewrite lookup_insert_None. naive_solver. }
    rewrite -IH. do 2 f_equiv. f_equiv=> k. f_equiv=> z.
    apply wand_intro_r. apply impl_intro_l, pure_elim_l=> ?.
    rewrite lookup_insert_ne; last congruence.
    rewrite pure_True // left_id // wand_elim_l //.
Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_impl_dom_subseteq `{Countable K} {A B}
    (Φ : K → A → PROP) (Ψ : K → B → PROP) (m1 : gmap K A) (m2 : gmap K B) :
  dom m2 ⊆ dom m1 →
  ([∗ map] k↦x ∈ m1, Φ k x) -∗
  □ (∀ (k : K) (x : A) (y : B),
      ⌜m1 !! k = Some x⌝ → ⌜m2 !! k = Some y⌝ →
      Φ k x -∗ Ψ k y) -∗
  ([∗ map] k↦y ∈ m2, Ψ k y) ∗
  ([∗ map] k↦x ∈ filter (λ '(k, _), m2 !! k = None) m1, Φ k x).
Proof.
  intros. apply entails_wand. rewrite big_sepM_impl_strong.
  apply wand_mono; last done. f_equiv. f_equiv=> k. apply forall_intro=> y.
  apply wand_intro_r, impl_intro_l, pure_elim_l=> Hlm2.
  destruct (m1 !! k) as [x|] eqn:Hlm1.
  - rewrite (forall_elim x) (forall_elim y).
    do 2 rewrite pure_True // left_id //. apply wand_elim_l.
  - apply elem_of_dom_2 in Hlm2. apply not_elem_of_dom in Hlm1.
    set_solver.
Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_kmap `{Countable K1, Countable K2} {A}
    (h : K1 → K2) `{!Inj (=) (=) h} (Φ : K2 → A → PROP) (m : gmap K1 A) :
  ([∗ map] k2 ↦ y ∈ kmap h m, Φ k2 y) ⊣⊢ ([∗ map] k1 ↦ y ∈ m, Φ (h k1) y).
Proof. by apply big_opM_kmap. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_map_seq {A} (Φ : nat → A → PROP) (start : nat) (l : list A) :
  ([∗ map] k ↦ x ∈ map_seq start l, Φ k x) ⊣⊢
  ([∗ list] i ↦ x ∈ l, Φ (start + i) x).
Proof. apply big_opM_map_seq. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_map_seqZ {A} (Φ : Z → A → PROP) (start : Z) (l : list A) :
  ([∗ map] k ↦ x ∈ map_seqZ start l, Φ k x) ⊣⊢
  ([∗ list] i ↦ x ∈ l, Φ (start + i)%Z x).
Proof. apply big_opM_map_seqZ. Qed.
(* iris/bi/big_op.v *)
(* The lemmas [big_andM_mono], [big_andM_ne] and [big_andM_proper] are more
  generic than the instances as they also give [l !! k = Some y] in the premise. *)
Lemma big_andM_mono Φ Ψ m :
    (∀ k x, m !! k = Some x → Φ k x ⊢ Ψ k x) →
    ([∧ map] k ↦ x ∈ m, Φ k x) ⊢ [∧ map] k ↦ x ∈ m, Ψ k x.
Proof. apply big_opM_gen_proper; apply _ || auto. Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_ne Φ Ψ m n :
    (∀ k x, m !! k = Some x → Φ k x ≡{n}≡ Ψ k x) →
    ([∧ map] k ↦ x ∈ m, Φ k x)%I ≡{n}≡ ([∧ map] k ↦ x ∈ m, Ψ k x)%I.
Proof. apply big_opM_ne. Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_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. apply big_opM_proper. Qed.
(* iris/bi/big_op.v *)
(* No need to declare instances for non-expansiveness and properness, we
  get both from the generic [big_opM] instances. *)
Instance big_andM_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
           (big_opM (@bi_and PROP) (K:=K) (A:=A)).
Proof. intros f g Hf m ? <-. apply big_andM_mono; intros; apply Hf. Qed.
(* iris/bi/big_op.v *)
Instance big_andM_empty_persistent Φ :
    Persistent ([∧ map] k↦x ∈ ∅, Φ k x).
Proof. rewrite big_opM_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_persistent Φ m :
    (∀ k x, m !! k = Some x → Persistent (Φ k x)) →
    Persistent ([∧ map] k↦x ∈ m, Φ k x).
Proof. apply big_opM_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_andM_persistent' Φ m :
    (∀ k x, Persistent (Φ k x)) → Persistent ([∧ map] k↦x ∈ m, Φ k x).
Proof. intros; apply big_andM_persistent, _. Qed.
(* iris/bi/big_op.v *)
Instance big_andM_empty_timeless Φ :
    Timeless ([∧ map] k↦x ∈ ∅, Φ k x).
Proof. rewrite big_opM_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_timeless Φ m :
    (∀ k x, m !! k = Some x → Timeless (Φ k x)) →
    Timeless ([∧ map] k↦x ∈ m, Φ k x).
Proof. apply big_opM_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_andM_timeless' Φ m :
    (∀ k x, Timeless (Φ k x)) → Timeless ([∧ map] k↦x ∈ m, Φ k x).
Proof. intros; apply big_andM_timeless, _. Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_subseteq Φ m1 m2 :
    m2 ⊆ m1 → ([∧ map] k ↦ x ∈ m1, Φ k x) ⊢ [∧ map] k ↦ x ∈ m2, Φ k x.
Proof.
    intros ?. rewrite -(map_difference_union m2 m1) //.
    rewrite big_opM_union; last by apply map_disjoint_difference_r1.
    by rewrite and_elim_l.
  Qed.