phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/big_op.v *)
Lemma big_andM_empty Φ : ([∧ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True.
Proof. by rewrite big_opM_empty. Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_empty' P Φ : P ⊢ [∧ map] k↦x ∈ ∅, Φ k x.
Proof. rewrite big_andM_empty. apply: True_intro. Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_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_andM_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_andM_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_andM_insert_2 Φ m i x :
    Φ i x ∧ ([∧ map] k↦y ∈ m, Φ k y) ⊢ [∧ map] k↦y ∈ <[i:=x]> m, Φ k y.
Proof.
    rewrite big_andM_insert_delete.
    destruct (m !! i) eqn:Hi; [ | by rewrite delete_id ].
    rewrite big_andM_delete //. apply and_mono_r, and_elim_r.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_lookup Φ m i x :
    m !! i = Some x → ([∧ map] k↦y ∈ m, Φ k y) ⊢ Φ i x.
Proof.
    intros. rewrite -(insert_id m i x) // big_andM_insert_delete. apply and_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_lookup_dom (Φ : K → PROP) m i :
    is_Some (m !! i) → ([∧ map] k↦_ ∈ m, Φ k) ⊢ Φ i.
Proof. intros [x ?]. by eapply (big_andM_lookup (λ i x, Φ i)). Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_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_andM_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_andM_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) True (f y)).
Proof. by rewrite big_opM_omap. Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_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_andM_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_andM_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 True).
Proof. apply: big_opM_filter'. Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_filter (φ : 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_bi_True. apply big_andM_filter'. Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_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_andM_and Φ Ψ 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_andM_persistently Φ 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_andM_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=> Φ.
    { rewrite big_andM_empty. apply: True_intro. }
    rewrite big_andM_insert //. apply and_intro.
    - rewrite (forall_elim i) (forall_elim x) lookup_insert_eq.
      by rewrite pure_True // True_impl.
    - rewrite -IH. apply forall_intro=> k. apply forall_intro=> x'.
      rewrite (forall_elim k) (forall_elim x').
      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_andM_forall Φ m :
    ([∧ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x).
Proof.
    intros. apply (anti_symm _); [| by rewrite -big_andM_intro].
    apply forall_intro=> k; apply forall_intro=> x.
    apply impl_intro_l, pure_elim_l=> ?; by apply: big_andM_lookup.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_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.
    rewrite -big_andM_forall -big_andM_and.
    by setoid_rewrite bi.impl_elim_r.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_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_andM_insert // IH -pure_and.
    by rewrite -map_Forall_insert.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_pure_2 (φ : K → A → Prop) m :
    ⌜map_Forall φ m⌝ ⊢@{PROP} ([∧ map] k↦x ∈ m, ⌜φ k x⌝).
Proof.
    rewrite big_andM_forall pure_forall_1. f_equiv=>k.
    rewrite pure_forall_1. f_equiv=>x. apply pure_impl_1.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_pure (φ : K → A → Prop) m :
    ([∧ map] k↦x ∈ m, ⌜φ k x⌝) ⊣⊢@{PROP} ⌜map_Forall φ m⌝.
Proof.
    apply (anti_symm (⊢)); [ by apply big_andM_pure_1 | by apply big_andM_pure_2].
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andM_later Φ 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_andM_laterN Φ 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_andM_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_andM_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_andM_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 *)
(* ** Big ops over two maps *)
Lemma big_sepM2_alt `{Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
  ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊣⊢
  ⌜ dom m1 = dom m2 ⌝ ∧ [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2.
Proof. by rewrite big_sepM2_unseal. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_alt_lookup (Φ : K → A → B → PROP) m1 m2 :
    ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊣⊢
    ⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝ ∧
    [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2.
Proof. rewrite big_sepM2_alt set_eq. by setoid_rewrite elem_of_dom. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_lookup_iff Φ m1 m2 :
    ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊢
    ⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝.
Proof. by rewrite big_sepM2_alt_lookup and_elim_l. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_dom Φ m1 m2 :
    ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊢
    ⌜ dom m1 = dom m2 ⌝.
Proof. by rewrite big_sepM2_alt and_elim_l. Qed.
(* iris/bi/big_op.v *)
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.
    rewrite !big_sepM2_alt. apply and_proper; [apply pure_proper; naive_solver |].
    rewrite -map_zip_with_flip map_zip_with_map_zip big_sepM_fmap.
    apply big_sepM_proper. by intros k [b a].
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_empty Φ : ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2) ⊣⊢ emp.
Proof.
    rewrite big_sepM2_alt map_zip_with_empty big_sepM_empty pure_True ?left_id //.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_empty' P `{!Affine P} Φ : P ⊢ [∗ map] k↦y1;y2 ∈ ∅;∅, Φ k y1 y2.
Proof. rewrite big_sepM2_empty. apply: affine. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_empty_l m1 Φ : ([∗ map] k↦y1;y2 ∈ m1; ∅, Φ k y1 y2) ⊢ ⌜m1 = ∅⌝.
Proof.
    rewrite big_sepM2_dom dom_empty_L.
    apply pure_mono, dom_empty_iff_L.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_empty_r m2 Φ : ([∗ map] k↦y1;y2 ∈ ∅; m2, Φ k y1 y2) ⊢ ⌜m2 = ∅⌝.
Proof.
    rewrite big_sepM2_dom dom_empty_L.
    apply pure_mono=>?. eapply dom_empty_iff_L. eauto.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_insert Φ m1 m2 i x1 x2 :
    m1 !! i = None → m2 !! i = None →
    ([∗ 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_alt -map_insert_zip_with.
    rewrite big_sepM_insert;
      last by rewrite map_lookup_zip_with Hm1.
    rewrite !persistent_and_affinely_sep_l /=.
    rewrite sep_assoc (sep_comm _ (Φ _ _ _)) -sep_assoc.
    repeat apply sep_proper=>//.
    apply affinely_proper, pure_proper. rewrite !dom_insert_L.
    apply not_elem_of_dom in Hm1. apply not_elem_of_dom in Hm2. set_solver.
  Qed.
(* iris/bi/big_op.v *)
(* The lemmas [big_sepM2_mono], [big_sepM2_ne] and [big_sepM2_proper] are more
  generic than the instances as they also give [mi !! k = Some yi] in the premise. *)
Lemma big_sepM2_mono Φ Ψ m1 m2 :
    (∀ 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_alt.
    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.
    destruct (m2 !! k) as [y2|]; simpl; last done.
    intros ?; simplify_eq. by apply Hm1m2.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_ne Φ Ψ m1 m2 n :
    (∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some 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 Hm1m2. rewrite !big_sepM2_alt.
    f_equiv. apply big_sepM_ne=> k [x1 x2]. rewrite map_lookup_zip_with.
    specialize (Hm1m2 k x1 x2).
    destruct (m1 !! k) as [y1|]; last done.
    destruct (m2 !! k) as [y2|]; simpl; last done.
    intros ?; simplify_eq. by apply Hm1m2.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_proper Φ Ψ m1 m2 :
    (∀ 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; apply (anti_symm _);
      apply big_sepM2_mono; auto using equiv_entails_1_1, equiv_entails_1_2.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_proper_2 `{!Equiv A, !Equiv B} Φ Ψ m1 m2 m1' m2' :
    m1 ≡ m1' → m2 ≡ m2' →
    (∀ k y1 y1' y2 y2',
      m1 !! k = Some y1 → m1' !! k = Some y1' → y1 ≡ y1' →
      m2 !! k = Some y2 → m2' !! k = Some y2' → y2 ≡ 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 Hm1 Hm2 Hf. rewrite !big_sepM2_alt. f_equiv.
    { by rewrite Hm1 Hm2. }
    apply big_opM_proper_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 *)
Instance big_sepM2_ne' n :
    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (dist n)))
      ==> (=) ==> (=) ==> (dist n))
           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_ne; intros; apply Hf. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM2_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢)))
      ==> (=) ==> (=) ==> (⊢)) (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_mono; intros; apply Hf. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM2_flip_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (flip (⊢))))
            ==> (=) ==> (=) ==> flip (⊢))
           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
Proof. solve_proper. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM2_proper' :
    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊣⊢)))
            ==> (=) ==> (=) ==> (⊣⊢))
           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_proper; intros; apply Hf. Qed.
(* iris/bi/big_op.v *)
(* Shows that some property [P] is closed under [big_sepM2]. Examples of [P]
  are [Persistent], [Affine], [Timeless]. *)
Lemma big_sepM2_closed (P : PROP → Prop) Φ m1 m2 :
    Proper ((≡) ==> iff) P →
    P emp%I → P False%I →
    (∀ Q1 Q2, P Q1 → P Q2 → P (Q1 ∗ Q2)%I) →
    (∀ k x1 x2, m1 !! k = Some x1 → m2 !! k = Some x2 → P (Φ k x1 x2)) →
    P ([∗ map] k↦x1;x2 ∈ m1; m2, Φ k x1 x2)%I.
Proof.
    intros ??? Hsep HΦ.
    rewrite big_sepM2_alt. destruct (decide (dom m1 = dom m2)).
    - rewrite pure_True // left_id. apply big_opM_closed; [done..|].
      intros k [x1 x2] Hk. rewrite map_lookup_zip_with in Hk.
      simplify_option_eq; auto.
    - by rewrite pure_False // left_absorb.
  Qed.
(* iris/bi/big_op.v *)
Instance big_sepM2_empty_persistent Φ :
    Persistent ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
Proof. rewrite big_sepM2_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_persistent Φ m1 m2 :
    (∀ k x1 x2, m1 !! k = Some x1 → m2 !! k = Some x2 → Persistent (Φ k x1 x2)) →
    Persistent ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
Proof. apply big_sepM2_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM2_persistent' Φ m1 m2 :
    (∀ k x1 x2, Persistent (Φ k x1 x2)) →
    Persistent ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
Proof. intros; apply big_sepM2_persistent, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM2_empty_affine Φ :
    Affine ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
Proof. rewrite big_sepM2_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_affine Φ m1 m2 :
    (∀ k x1 x2, m1 !! k = Some x1 → m2 !! k = Some x2 → Affine (Φ k x1 x2)) →
    Affine ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
Proof. apply big_sepM2_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM2_affine' Φ m1 m2 :
    (∀ k x1 x2, Affine (Φ k x1 x2)) →
    Affine ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
Proof. intros; apply big_sepM2_affine, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM2_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
    Timeless ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
Proof. rewrite big_sepM2_alt map_zip_with_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_timeless `{!Timeless (emp%I : PROP)} Φ m1 m2 :
    (∀ k x1 x2, m1 !! k = Some x1 → m2 !! k = Some x2 → Timeless (Φ k x1 x2)) →
    Timeless ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
Proof. apply big_sepM2_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepM2_timeless' `{!Timeless (emp%I : PROP)} Φ m1 m2 :
    (∀ k x1 x2, Timeless (Φ k x1 x2)) →
    Timeless ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
Proof. intros; apply big_sepM2_timeless, _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_delete Φ m1 m2 i x1 x2 :
    m1 !! i = Some x1 → m2 !! i = Some x2 →
    ([∗ 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_alt=> Hx1 Hx2.
    rewrite !persistent_and_affinely_sep_l /=.
    rewrite sep_assoc (sep_comm  (Φ _ _ _)) -sep_assoc.
    apply sep_proper.
    - apply affinely_proper, pure_proper. rewrite !dom_delete_L.
      apply elem_of_dom_2 in Hx1; apply elem_of_dom_2 in Hx2. set_unfold.
      apply base.forall_proper=> k. destruct (decide (k = i)); naive_solver.
    - rewrite -map_delete_zip_with.
      apply (big_sepM_delete (λ i xx, Φ i xx.1 xx.2) (map_zip m1 m2) i (x1,x2)).
      by rewrite map_lookup_zip_with Hx1 Hx2.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_delete_l Φ m1 m2 i x1 :
    m1 !! i = Some x1 →
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
    ⊣⊢ ∃ x2, ⌜m2 !! i = Some x2⌝ ∧
            (Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2).
Proof.
    intros Hm1. apply (anti_symm _).
    - rewrite big_sepM2_alt_lookup. apply pure_elim_l=> Hm.
      assert (is_Some (m2 !! i)) as [x2 Hm2].
      { apply Hm. by econstructor. }
      rewrite -(exist_intro x2).
      rewrite big_sepM2_alt_lookup (big_sepM_delete _ _ i (x1,x2)) /=;
        last by rewrite map_lookup_zip_with Hm1 Hm2.
      rewrite pure_True // left_id.
      f_equiv. apply and_intro.
      + apply pure_intro=> k. by rewrite !lookup_delete_is_Some Hm.
      + by rewrite -map_delete_zip_with.
    - apply exist_elim=> x2. apply pure_elim_l=> ?.
      by rewrite -big_sepM2_delete.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_delete_r Φ m1 m2 i x2 :
    m2 !! i = Some x2 →
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
    ⊣⊢ ∃ x1, ⌜m1 !! i = Some x1⌝ ∧
            (Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2).
Proof.
    intros Hm2. apply (anti_symm _).
    - rewrite big_sepM2_alt_lookup.
      apply pure_elim_l=> Hm.
      assert (is_Some (m1 !! i)) as [x1 Hm1].
      { apply Hm. by econstructor. }
      rewrite -(exist_intro x1).
      rewrite big_sepM2_alt_lookup (big_sepM_delete _ _ i (x1,x2)) /=;
        last by rewrite map_lookup_zip_with Hm1 Hm2.
      rewrite pure_True // left_id.
      f_equiv. apply and_intro.
      + apply pure_intro=> k. by rewrite !lookup_delete_is_Some Hm.
      + by rewrite -map_delete_zip_with.
    - apply exist_elim=> x1. apply pure_elim_l=> ?.
      by rewrite -big_sepM2_delete.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_insert_delete Φ m1 m2 i x1 x2 :
    ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
    ⊣⊢ Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2.
Proof.
    rewrite -(insert_delete_eq m1) -(insert_delete_eq m2).
    apply big_sepM2_insert; by rewrite lookup_delete_eq.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_insert_acc Φ m1 m2 i x1 x2 :
    m1 !! i = Some x1 → m2 !! i = Some x2 →
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢
    Φ i x1 x2 ∗ (∀ x1' x2', Φ i x1' x2' -∗
        ([∗ map] k↦y1;y2 ∈ <[i:=x1']>m1;<[i:=x2']>m2, Φ k y1 y2)).
Proof.
    intros ??. rewrite {1}big_sepM2_delete //. apply sep_mono; [done|].
    apply forall_intro=> x1'. apply forall_intro=> x2'.
    rewrite -(insert_delete_eq m1) -(insert_delete_eq m2)
      big_sepM2_insert ?lookup_delete_eq //.
    by apply wand_intro_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_insert_2 Φ m1 m2 i x1 x2
    `{!TCOr (∀ x y, Affine (Φ i x y)) (Absorbing (Φ i x1 x2))} :
    Φ i x1 x2 -∗
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) -∗
    ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2).
Proof.
    rewrite !big_sepM2_alt.
    assert (TCOr (∀ x, Affine (Φ i x.1 x.2)) (Absorbing (Φ i x1 x2))).
    { destruct select (TCOr _ _); apply _. }
    apply entails_wand, wand_intro_r.
    rewrite !persistent_and_affinely_sep_l /=.
    rewrite (sep_comm  (Φ _ _ _)) -sep_assoc. apply sep_mono.
    { apply affinely_mono, pure_mono. rewrite !dom_insert_L. set_solver. }
    rewrite (big_sepM_insert_2 (λ k xx, Φ k xx.1 xx.2) (map_zip m1 m2) i (x1, x2)).
    rewrite map_insert_zip_with. apply wand_elim_r.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_lookup_acc Φ m1 m2 i x1 x2 :
    m1 !! i = Some x1 → m2 !! i = Some x2 →
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢
    Φ i x1 x2 ∗ (Φ i x1 x2 -∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)).
Proof.
    intros Hm1 Hm2. etrans; first apply big_sepM2_insert_acc=>//.
    apply sep_mono_r. rewrite (forall_elim x1) (forall_elim x2).
    rewrite !insert_id //.
 Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_lookup Φ m1 m2 i x1 x2
    `{!TCOr (∀ j y1 y2, Affine (Φ j y1 y2)) (Absorbing (Φ i x1 x2))} :
    m1 !! i = Some x1 → m2 !! i = Some x2 →
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢ Φ i x1 x2.
Proof.
    intros Hx1 Hx2. destruct select (TCOr _ _).
    - rewrite big_sepM2_delete // sep_elim_l //.
    - rewrite big_sepM2_lookup_acc // sep_elim_l //.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_lookup_l Φ m1 m2 i x1
    `{!TCOr (∀ j y1 y2, Affine (Φ j y1 y2)) (∀ x2, Absorbing (Φ i x1 x2))} :
    m1 !! i = Some x1 →
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
    ⊢ ∃ x2, ⌜m2 !! i = Some x2⌝ ∧ Φ i x1 x2.
Proof.
    intros Hm1. rewrite big_sepM2_delete_l //.
    f_equiv=> x2. destruct select (TCOr _ _); by rewrite sep_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_lookup_r Φ m1 m2 i x2
    `{!TCOr (∀ j y1 y2, Affine (Φ j y1 y2)) (∀ x1, Absorbing (Φ i x1 x2))} :
    m2 !! i = Some x2 →
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
    ⊢ ∃ x1, ⌜m1 !! i = Some x1⌝ ∧ Φ i x1 x2.
Proof.
    intros Hm2. rewrite big_sepM2_delete_r //.
    f_equiv=> x1. destruct select (TCOr _ _); by rewrite sep_elim_l.
  Qed.
(* iris/bi/big_op.v *)
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_alt.
    rewrite map_zip_with_singleton big_sepM_singleton.
    apply (anti_symm _).
    - apply and_elim_r.
    - rewrite <- (left_id True%I (∧)%I (Φ i x1 x2)).
      apply and_mono=> //. apply pure_mono=> _. set_solver.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_fst_snd Φ m :
    ([∗ map] k↦y1;y2 ∈ fst <$> m; snd <$> m, Φ k y1 y2) ⊣⊢
    [∗ map] k ↦ xy ∈ m, Φ k (xy.1) (xy.2).
Proof.
    rewrite big_sepM2_alt. rewrite !dom_fmap_L.
    by rewrite pure_True // True_and map_zip_fst_snd.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_fmap {A' B'} (f : A → A') (g : B → B') (Φ : K → A' → B' → PROP) m1 m2 :
    ([∗ 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_alt. by rewrite map_fmap_zip !dom_fmap_L big_sepM_fmap.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_fmap_l {A'} (f : A → A') (Φ : K → A' → B → PROP) m1 m2 :
    ([∗ map] k↦y1;y2 ∈ f <$> m1; m2, Φ k y1 y2)
    ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k (f y1) y2).
Proof. rewrite -{1}(map_fmap_id m2). apply big_sepM2_fmap. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_fmap_r {B'} (g : B → B') (Φ : K → A → B' → PROP) m1 m2 :
    ([∗ map] k↦y1;y2 ∈ m1; g <$> m2, Φ k y1 y2)
    ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 (g y2)).
Proof. rewrite -{1}(map_fmap_id m1). apply big_sepM2_fmap. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_sep Φ Ψ m1 m2 :
    ([∗ 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_alt.
    rewrite -{1}(idemp bi_and ⌜ dom m1 = dom m2 ⌝%I).
    rewrite -assoc.
    rewrite !persistent_and_affinely_sep_l /=.
    rewrite -assoc. apply sep_proper=>//.
    rewrite assoc (comm _ _ (<affine> _)%I) -assoc.
    apply sep_proper=>//. apply big_sepM_sep.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_sep_2 Φ Ψ m1 m2 :
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) -∗
    ([∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2) -∗
    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2 ∗ Ψ k y1 y2).
Proof. apply entails_wand, wand_intro_r. rewrite big_sepM2_sep //. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_and Φ Ψ m1 m2 :
    ([∗ 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. auto using and_intro, big_sepM2_mono, and_elim_l, and_elim_r. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM2_pure_1 (φ : K → A → B → Prop) m1 m2 :
    ([∗ map] k↦y1;y2 ∈ m1;m2, ⌜φ k y1 y2⌝) ⊢@{PROP}
      ⌜∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → φ k y1 y2⌝.
Proof.
    rewrite big_sepM2_alt.
    rewrite big_sepM_pure_1 -pure_and.
    f_equiv=>-[Hdom Hforall] k y1 y2 Hy1 Hy2.
    eapply (Hforall k (y1, y2)). clear Hforall.
    apply map_lookup_zip_with_Some. naive_solver.
  Qed.