phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/big_op.v *)
Lemma big_sepL_omap {B} (f : A → option B) (Φ : B → PROP) l :
    ([∗ list] y ∈ omap f l, Φ y) ⊣⊢ ([∗ list] y ∈ l, from_option Φ emp (f y)).
Proof. by rewrite big_opL_omap. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_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_sepL_sep Φ Ψ 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_sepL_sep_2 Φ Ψ l :
    ([∗ list] k↦x ∈ l, Φ k x) -∗
    ([∗ list] k↦x ∈ l, Ψ k x) -∗
    ([∗ list] k↦x ∈ l, Φ k x ∗ Ψ k x).
Proof. apply entails_wand, wand_intro_r. rewrite big_sepL_sep //. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_and Φ Ψ l :
    ([∗ list] k↦x ∈ l, Φ k x ∧ Ψ k x)
    ⊢ ([∗ list] k↦x ∈ l, Φ k x) ∧ ([∗ list] k↦x ∈ l, Ψ k x).
Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_pure_1 (φ : nat → A → Prop) l :
    ([∗ list] k↦x ∈ l, ⌜φ k x⌝) ⊢@{PROP} ⌜∀ k x, l !! k = Some x → φ k x⌝.
Proof.
    induction l as [|x l IH] using rev_ind.
    { apply pure_intro=>??. rewrite lookup_nil. done. }
    rewrite big_sepL_snoc // IH sep_and -pure_and.
    f_equiv=>-[Hl Hx] k y /lookup_app_Some =>-[Hy|[Hlen Hy]].
    - by apply Hl.
    - apply list_lookup_singleton_Some in Hy as [Hk ->].
      replace k with (length l) by lia. done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_affinely_pure_2 (φ : nat → A → Prop) l :
    <affine> ⌜∀ k x, l !! k = Some x → φ k x⌝ ⊢@{PROP} ([∗ list] k↦x ∈ l, <affine> ⌜φ k x⌝).
Proof.
    induction l as [|x l IH] using rev_ind.
    { rewrite big_sepL_nil. apply affinely_elim_emp. }
    rewrite big_sepL_snoc // -IH.
    rewrite -persistent_and_sep_1 -affinely_and -pure_and.
    f_equiv. f_equiv=>- Hlx. split.
    - intros k y Hy. apply Hlx. rewrite lookup_app Hy //.
    - apply Hlx. rewrite lookup_app lookup_ge_None_2 //.
      rewrite Nat.sub_diag //.
  Qed.
(* iris/bi/big_op.v *)
(* The general backwards direction requires [BiAffine] to cover the empty case. *)
Lemma big_sepL_pure `{!BiAffine PROP} (φ : nat → A → Prop) l :
    ([∗ list] k↦x ∈ l, ⌜φ k x⌝) ⊣⊢@{PROP} ⌜∀ k x, l !! k = Some x → φ k x⌝.
Proof.
    apply (anti_symm (⊢)); first by apply big_sepL_pure_1.
    rewrite -(affine_affinely ⌜_⌝).
    rewrite big_sepL_affinely_pure_2. by setoid_rewrite affinely_elim.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_persistently `{!BiAffine PROP} Φ 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_sepL_intro Φ l :
    □ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x) ⊢ [∗ list] k↦x ∈ l, Φ k x.
Proof.
    revert Φ. induction l as [|x l IH]=> Φ /=; [by apply (affine _)|].
    rewrite intuitionistically_sep_dup. f_equiv.
    - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
      by rewrite intuitionistically_elim.
    - rewrite -IH. f_equiv.
      apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_forall `{!BiAffine PROP} Φ l :
    (∀ k x, Persistent (Φ k x)) →
    ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! 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_sepL_lookup. }
    revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ /=.
    { apply: affine. }
    rewrite -persistent_and_sep_1. apply and_intro.
    - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl. done.
    - rewrite -IH. apply forall_intro => k. by rewrite (forall_elim (S k)).
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_impl Φ Ψ l :
    ([∗ list] k↦x ∈ l, Φ k x) -∗
    □ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗
    [∗ list] k↦x ∈ l, Ψ k x.
Proof.
    apply entails_wand, wand_intro_l. rewrite big_sepL_intro -big_sepL_sep.
    by setoid_rewrite wand_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_wand Φ Ψ l :
    ([∗ list] k↦x ∈ l, Φ k x) -∗
    ([∗ list] k↦x ∈ l, Φ k x -∗ Ψ k x) -∗
    [∗ list] k↦x ∈ l, Ψ k x.
Proof.
    apply entails_wand, wand_intro_r. rewrite -big_sepL_sep.
    setoid_rewrite wand_elim_r. done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_dup P `{!Affine P} l :
    □ (P -∗ P ∗ P) -∗ P -∗ [∗ list] k↦x ∈ l, P.
Proof.
    apply entails_wand, wand_intro_l.
    induction l as [|x l IH]=> /=; first by apply: affine.
    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_sepL_delete Φ l i x :
    l !! i = Some x →
    ([∗ list] k↦y ∈ l, Φ k y) ⊣⊢
    Φ i x ∗ [∗ list] k↦y ∈ l, if decide (k = i) then emp else Φ k y.
Proof.
    intros. rewrite -(take_drop_middle l i x) // !big_sepL_app /= Nat.add_0_r.
    rewrite length_take_le; last eauto using lookup_lt_Some, Nat.lt_le_incl.
    rewrite decide_True // left_id.
    rewrite assoc -!(comm _ (Φ _ _)) -assoc. do 2 f_equiv.
    - apply big_sepL_proper=> k y Hk. apply lookup_lt_Some in Hk.
      rewrite length_take in Hk. by rewrite decide_False; last lia.
    - apply big_sepL_proper=> k y _. by rewrite decide_False; last lia.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_delete' `{!BiAffine PROP} Φ l i x :
    l !! i = Some x →
    ([∗ list] k↦y ∈ l, Φ k y) ⊣⊢ Φ i x ∗ [∗ list] k↦y ∈ l, ⌜ k ≠ i ⌝ → Φ k y.
Proof.
    intros. rewrite big_sepL_delete //. (do 2 f_equiv)=> k y.
    rewrite -decide_emp. by repeat case_decide.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_lookup_acc_impl {Φ l} i x :
    l !! i = Some x →
    ([∗ list] k↦y ∈ l, Φ k y) -∗
    (* We obtain [Φ] for [x] *)
    Φ i x ∗
    (* We reobtain the bigop for a predicate [Ψ] selected by the user *)
    ∀ Ψ,
      □ (∀ k y, ⌜ l !! k = Some y ⌝ → ⌜ k ≠ i ⌝ → Φ k y -∗ Ψ k y) -∗
      Ψ i x -∗
      [∗ list] k↦y ∈ l, Ψ k y.
Proof.
    intros. apply entails_wand.
    rewrite big_sepL_delete //. apply sep_mono_r, forall_intro=> Ψ.
    apply wand_intro_r, wand_intro_l.
    rewrite (big_sepL_delete Ψ l i x) //. apply sep_mono_r.
    eapply wand_apply; [apply wand_entails, big_sepL_impl|apply sep_mono_r].
    apply intuitionistically_intro', forall_intro=> k; apply forall_intro=> y.
    apply impl_intro_l, pure_elim_l=> ?; apply wand_intro_r.
    rewrite (forall_elim ) (forall_elim y) pure_True // left_id.
    destruct (decide _) as [->|]; [by apply: affine|].
    by rewrite pure_True //left_id intuitionistically_elim wand_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_replicate l P :
    [∗] replicate (length l) P ⊣⊢ [∗ list] y ∈ l, P.
Proof. induction l as [|x l]=> //=; by f_equiv. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_later `{!BiAffine PROP} Φ l :
    ▷ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷ Φ k x).
Proof. apply (big_opL_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_later_2 Φ l :
    ([∗ list] k↦x ∈ l, ▷ Φ k x) ⊢ ▷ [∗ list] k↦x ∈ l, Φ k x.
Proof. by rewrite (big_opL_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_laterN `{!BiAffine PROP} Φ n l :
    ▷^n ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷^n Φ k x).
Proof. apply (big_opL_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_laterN_2 Φ n l :
    ([∗ list] k↦x ∈ l, ▷^n Φ k x) ⊢ ▷^n [∗ list] k↦x ∈ l, Φ k x.
Proof. by rewrite (big_opL_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_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_sepL_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 *)
(* Some lemmas depend on the generalized versions of the above ones. *)
Lemma big_sepL_sep_zip_with {A B C} (f : A → B → C) (g1 : C → A) (g2 : C → B)
    (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
  (∀ x y, g1 (f x y) = x) →
  (∀ x y, g2 (f x y) = y) →
  length l1 = length l2 →
  ([∗ list] k↦xy ∈ zip_with f l1 l2, Φ1 k (g1 xy) ∗ Φ2 k (g2 xy)) ⊣⊢
  ([∗ list] k↦x ∈ l1, Φ1 k x) ∗ ([∗ list] k↦y ∈ l2, Φ2 k y).
Proof. apply big_opL_sep_zip_with. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_sep_zip {A B} (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
  length l1 = length l2 →
  ([∗ list] k↦xy ∈ zip l1 l2, Φ1 k xy.1 ∗ Φ2 k xy.2) ⊣⊢
  ([∗ list] k↦x ∈ l1, Φ1 k x) ∗ ([∗ list] k↦y ∈ l2, Φ2 k y).
Proof. apply big_opL_sep_zip. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_zip_with {A B C} (Φ : nat → A → PROP) f (l1 : list B) (l2 : list C) :
  ([∗ list] k↦x ∈ zip_with f l1 l2, Φ k x) ⊣⊢
  ([∗ list] k↦x ∈ l1, if l2 !! k is Some y then Φ k (f x y) else emp).
Proof.
  revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //=.
  - by rewrite big_sepL_emp left_id.
  - by rewrite IH.
Qed.
(* iris/bi/big_op.v *)
(* ** Big ops over two lists *)
Lemma big_sepL2_alt {A B} (Φ : nat → A → B → PROP) l1 l2 :
  ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2) ⊣⊢
  ⌜ length l1 = length l2 ⌝ ∧ [∗ list] k ↦ xy ∈ zip l1 l2, Φ k (xy.1) (xy.2).
Proof.
  apply (anti_symm _).
  - apply and_intro.
    + revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2] /=;
        auto using pure_intro, False_elim.
      rewrite IH sep_elim_r. apply pure_mono; auto.
    + revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2] /=;
        auto using pure_intro, False_elim.
      by rewrite IH.
  - apply pure_elim_l=> /Forall2_same_length Hl. revert Φ.
    induction Hl as [|x1 l1 x2 l2 _ _ IH]=> Φ //=. by rewrite -IH.
Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_nil Φ : ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2) ⊣⊢ emp.
Proof. done. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_nil' P `{!Affine P} Φ : P ⊢ [∗ list] k↦y1;y2 ∈ [];[], Φ k y1 y2.
Proof. apply: affine. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_nil_inv_l Φ l2 :
    ([∗ list] k↦y1;y2 ∈ []; l2, Φ k y1 y2) ⊢ ⌜l2 = []⌝.
Proof. destruct l2; simpl; auto using False_elim, pure_intro. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_nil_inv_r Φ l1 :
    ([∗ list] k↦y1;y2 ∈ l1; [], Φ k y1 y2) ⊢ ⌜l1 = []⌝.
Proof. destruct l1; simpl; auto using False_elim, pure_intro. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_cons Φ x1 x2 l1 l2 :
    ([∗ list] k↦y1;y2 ∈ x1 :: l1; x2 :: l2, Φ k y1 y2)
    ⊣⊢ Φ 0 x1 x2 ∗ [∗ list] k↦y1;y2 ∈ l1;l2, Φ (S k) y1 y2.
Proof. done. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_cons_inv_l Φ x1 l1 l2 :
    ([∗ list] k↦y1;y2 ∈ x1 :: l1; l2, Φ k y1 y2) ⊢
    ∃ x2 l2', ⌜ l2 = x2 :: l2' ⌝ ∧
              Φ 0 x1 x2 ∗ [∗ list] k↦y1;y2 ∈ l1;l2', Φ (S k) y1 y2.
Proof.
    destruct l2 as [|x2 l2]; simpl; auto using False_elim.
    by rewrite -(exist_intro x2) -(exist_intro l2) pure_True // left_id.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_cons_inv_r Φ x2 l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1; x2 :: l2, Φ k y1 y2) ⊢
    ∃ x1 l1', ⌜ l1 = x1 :: l1' ⌝ ∧
              Φ 0 x1 x2 ∗ [∗ list] k↦y1;y2 ∈ l1';l2, Φ (S k) y1 y2.
Proof.
    destruct l1 as [|x1 l1]; simpl; auto using False_elim.
    by rewrite -(exist_intro x1) -(exist_intro l1) pure_True // left_id.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_singleton Φ x1 x2 :
    ([∗ list] k↦y1;y2 ∈ [x1];[x2], Φ k y1 y2) ⊣⊢ Φ 0 x1 x2.
Proof. by rewrite /= right_id. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_length Φ l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2) ⊢ ⌜ length l1 = length l2 ⌝.
Proof. by rewrite big_sepL2_alt and_elim_l. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_fst_snd Φ l :
    ([∗ list] k↦y1;y2 ∈ l.*1; l.*2, Φ k y1 y2) ⊣⊢
    [∗ list] k ↦ xy ∈ l, Φ k (xy.1) (xy.2).
Proof.
    rewrite big_sepL2_alt !length_fmap.
    by rewrite pure_True // True_and zip_fst_snd.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_app Φ l1 l2 l1' l2' :
    ([∗ list] k↦y1;y2 ∈ l1; l1', Φ k y1 y2) ⊢
    ([∗ list] k↦y1;y2 ∈ l2; l2', Φ (length l1 + k) y1 y2) -∗
    ([∗ list] k↦y1;y2 ∈ l1 ++ l2; l1' ++ l2', Φ k y1 y2).
Proof.
    apply wand_intro_r. revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] /=.
    - by rewrite left_id.
    - rewrite left_absorb. apply False_elim.
    - rewrite left_absorb. apply False_elim.
    - by rewrite -assoc IH.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_app_inv_l Φ l1' l1'' l2 :
    ([∗ list] k↦y1;y2 ∈ l1' ++ l1''; l2, Φ k y1 y2) ⊢
    ∃ l2' l2'', ⌜ l2 = l2' ++ l2'' ⌝ ∧
                ([∗ list] k↦y1;y2 ∈ l1';l2', Φ k y1 y2) ∗
                ([∗ list] k↦y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2).
Proof.
    rewrite -(exist_intro (take (length l1') l2))
      -(exist_intro (drop (length l1') l2)) take_drop pure_True // left_id.
    revert Φ l2. induction l1' as [|x1 l1' IH]=> Φ -[|x2 l2] /=;
       [by rewrite left_id|by rewrite left_id|apply False_elim|].
    by rewrite IH -assoc.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_app_inv_r Φ l1 l2' l2'' :
    ([∗ list] k↦y1;y2 ∈ l1; l2' ++ l2'', Φ k y1 y2) ⊢
    ∃ l1' l1'', ⌜ l1 = l1' ++ l1'' ⌝ ∧
                ([∗ list] k↦y1;y2 ∈ l1';l2', Φ k y1 y2) ∗
                ([∗ list] k↦y1;y2 ∈ l1'';l2'', Φ (length l2' + k) y1 y2).
Proof.
    rewrite -(exist_intro (take (length l2') l1))
      -(exist_intro (drop (length l2') l1)) take_drop pure_True // left_id.
    revert Φ l1. induction l2' as [|x2 l2' IH]=> Φ -[|x1 l1] /=;
       [by rewrite left_id|by rewrite left_id|apply False_elim|].
    by rewrite IH -assoc.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_app_inv Φ l1 l2 l1' l2' :
    length l1 = length l1' ∨ length l2 = length l2' →
    ([∗ list] k↦y1;y2 ∈ l1 ++ l2; l1' ++ l2', Φ k y1 y2) ⊢
    ([∗ list] k↦y1;y2 ∈ l1; l1', Φ k y1 y2) ∗
    ([∗ list] k↦y1;y2 ∈ l2; l2', Φ (length l1 + k)%nat y1 y2).
Proof.
    revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] /= Hlen.
    - by rewrite left_id.
    - destruct Hlen as [[=]|Hlen]. rewrite big_sepL2_length Hlen /= length_app.
      apply pure_elim'; lia.
    - destruct Hlen as [[=]|Hlen]. rewrite big_sepL2_length -Hlen /= length_app.
      apply pure_elim'; lia.
    - by rewrite -assoc IH; last lia.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_app_same_length Φ l1 l2 l1' l2' :
    length l1 = length l1' ∨ length l2 = length l2' →
    ([∗ list] k↦y1;y2 ∈ l1 ++ l2; l1' ++ l2', Φ k y1 y2) ⊣⊢
    ([∗ list] k↦y1;y2 ∈ l1; l1', Φ k y1 y2) ∗
    ([∗ list] k↦y1;y2 ∈ l2; l2', Φ (length l1 + k)%nat y1 y2).
Proof.
    intros. apply (anti_symm _).
    - by apply big_sepL2_app_inv.
    - apply wand_elim_l', big_sepL2_app.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_snoc Φ x1 x2 l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1 ++ [x1]; l2 ++ [x2], Φ k y1 y2) ⊣⊢
    ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2) ∗ Φ (length l1) x1 x2.
Proof.
    rewrite big_sepL2_app_same_length; last by auto.
    by rewrite big_sepL2_singleton Nat.add_0_r.
  Qed.
(* iris/bi/big_op.v *)
(* The lemmas [big_sepL2_mono], [big_sepL2_ne] and [big_sepL2_proper] are more
  generic than the instances as they also give [li !! k = Some yi] in the premise. *)
Lemma big_sepL2_mono Φ Ψ l1 l2 :
    (∀ k y1 y2, l1 !! k = Some y1 → l2 !! k = Some y2 → Φ k y1 y2 ⊢ Ψ k y1 y2) →
    ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ [∗ list] k ↦ y1;y2 ∈ l1;l2, Ψ k y1 y2.
Proof.
    intros H. rewrite !big_sepL2_alt. f_equiv. apply big_sepL_mono=> k [y1 y2].
    rewrite lookup_zip_with=> ?; simplify_option_eq; auto.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_ne Φ Ψ l1 l2 n :
    (∀ k y1 y2, l1 !! k = Some y1 → l2 !! k = Some y2 → Φ k y1 y2 ≡{n}≡ Ψ k y1 y2) →
    ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)%I ≡{n}≡ ([∗ list] k ↦ y1;y2 ∈ l1;l2, Ψ k y1 y2)%I.
Proof.
    intros H. rewrite !big_sepL2_alt. f_equiv. apply big_sepL_ne=> k [y1 y2].
    rewrite lookup_zip_with=> ?; simplify_option_eq; auto.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_proper Φ Ψ l1 l2 :
    (∀ k y1 y2, l1 !! k = Some y1 → l2 !! k = Some y2 → Φ k y1 y2 ⊣⊢ Ψ k y1 y2) →
    ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) ⊣⊢ [∗ list] k ↦ y1;y2 ∈ l1;l2, Ψ k y1 y2.
Proof.
    intros; apply (anti_symm _);
      apply big_sepL2_mono; auto using equiv_entails_1_1, equiv_entails_1_2.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_proper_2 `{!Equiv A, !Equiv B} Φ Ψ l1 l2 l1' l2' :
    l1 ≡ l1' → l2 ≡ l2' →
    (∀ k y1 y1' y2 y2',
      l1 !! k = Some y1 → l1' !! k = Some y1' → y1 ≡ y1' →
      l2 !! k = Some y2 → l2' !! k = Some y2' → y2 ≡ y2' →
      Φ k y1 y2 ⊣⊢ Ψ k y1' y2') →
    ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) ⊣⊢ [∗ list] k ↦ y1;y2 ∈ l1';l2', Ψ k y1 y2.
Proof.
    intros Hl1 Hl2 Hf. rewrite !big_sepL2_alt. f_equiv.
    { do 2 f_equiv; by apply length_proper. }
    apply big_opL_proper_2; [by f_equiv|].
    intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%lookup_zip_with_Some
      (?&?&[=<- <-]&?&?)%lookup_zip_with_Some [??]; naive_solver.
  Qed.
(* iris/bi/big_op.v *)
Instance big_sepL2_ne' n :
    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (dist n)))
      ==> (=) ==> (=) ==> (dist n))
           (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_ne; intros; apply Hf. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL2_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢)))
      ==> (=) ==> (=) ==> (⊢))
           (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_mono; intros; apply Hf. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL2_flip_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (flip (⊢))))
            ==> (=) ==> (=) ==> flip (⊢))
           (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
Proof. solve_proper. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL2_proper' :
    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊣⊢)))
      ==> (=) ==> (=) ==> (⊣⊢))
           (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_proper; intros; apply Hf. Qed.
(* iris/bi/big_op.v *)
(* Shows that some property [P] is closed under [big_sepL2]. Examples of [P]
  are [Persistent], [Affine], [Timeless]. *)
Lemma big_sepL2_closed (P : PROP → Prop) Φ l1 l2 :
    P emp%I → P False%I →
    (∀ Q1 Q2, P Q1 → P Q2 → P (Q1 ∗ Q2)%I) →
    (∀ k x1 x2, l1 !! k = Some x1 → l2 !! k = Some x2 → P (Φ k x1 x2)) →
    P ([∗ list] k↦x1;x2 ∈ l1; l2, Φ k x1 x2)%I.
Proof.
    intros ?? Hsep. revert l2 Φ. induction l1 as [|x1 l1 IH]=> -[|x2 l2] Φ HΦ //=.
    apply Hsep; first by auto. apply IH=> k. apply (HΦ (S k)).
  Qed.
(* iris/bi/big_op.v *)
Instance big_sepL2_nil_persistent Φ :
    Persistent ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
Proof. simpl; apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_persistent Φ l1 l2 :
    (∀ k x1 x2, l1 !! k = Some x1 → l2 !! k = Some x2 → Persistent (Φ k x1 x2)) →
    Persistent ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
Proof. apply big_sepL2_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL2_persistent' Φ l1 l2 :
    (∀ k x1 x2, Persistent (Φ k x1 x2)) →
    Persistent ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
Proof. intros; apply big_sepL2_persistent, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL2_nil_affine Φ :
    Affine ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
Proof. simpl; apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_affine Φ l1 l2 :
    (∀ k x1 x2, l1 !! k = Some x1 → l2 !! k = Some x2 → Affine (Φ k x1 x2)) →
    Affine ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
Proof. apply big_sepL2_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL2_affine' Φ l1 l2 :
    (∀ k x1 x2, Affine (Φ k x1 x2)) →
    Affine ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
Proof. intros; apply big_sepL2_affine, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL2_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
    Timeless ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
Proof. simpl; apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_timeless `{!Timeless (emp%I : PROP)} Φ l1 l2 :
    (∀ k x1 x2, l1 !! k = Some x1 → l2 !! k = Some x2 → Timeless (Φ k x1 x2)) →
    Timeless ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
Proof. apply big_sepL2_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL2_timeless' `{!Timeless (emp%I : PROP)} Φ l1 l2 :
    (∀ k x1 x2, Timeless (Φ k x1 x2)) →
    Timeless ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
Proof. intros; apply big_sepL2_timeless, _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_insert_acc Φ l1 l2 i x1 x2 :
    l1 !! i = Some x1 → l2 !! i = Some x2 →
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢
    Φ i x1 x2 ∗ (∀ y1 y2, Φ i y1 y2 -∗ ([∗ list] k↦y1;y2 ∈ <[i:=y1]>l1;<[i:=y2]>l2, Φ k y1 y2)).
Proof.
    intros Hl1 Hl2. rewrite big_sepL2_alt. apply pure_elim_l=> Hl.
    rewrite {1}big_sepL_insert_acc; last by rewrite lookup_zip_with; simplify_option_eq.
    apply sep_mono_r. apply forall_intro => y1. apply forall_intro => y2.
    rewrite big_sepL2_alt !length_insert pure_True // left_id -insert_zip_with.
    by rewrite (forall_elim (y1, y2)).
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_lookup_acc Φ l1 l2 i x1 x2 :
    l1 !! i = Some x1 → l2 !! i = Some x2 →
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢
    Φ i x1 x2 ∗ (Φ i x1 x2 -∗ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)).
Proof.
    intros. rewrite {1}big_sepL2_insert_acc // (forall_elim x1) (forall_elim x2).
    by rewrite !list_insert_id.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_lookup Φ l1 l2 i x1 x2
    `{!TCOr (∀ j y1 y2, Affine (Φ j y1 y2)) (Absorbing (Φ i x1 x2))} :
    l1 !! i = Some x1 → l2 !! i = Some x2 →
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ Φ i x1 x2.
Proof.
    intros Hx1 Hx2. destruct select (TCOr _ _).
    - rewrite -(take_drop_middle l1 i x1) // -(take_drop_middle l2 i x2) //.
      apply lookup_lt_Some in Hx1. apply lookup_lt_Some in Hx2.
      rewrite big_sepL2_app_same_length /= 2?length_take; last lia.
      rewrite (_ : _ + 0 = i); last lia.
      rewrite sep_elim_r sep_elim_l //.
    - rewrite big_sepL2_lookup_acc // sep_elim_l //.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_lookup_l Φ l1 l2 i x1
    `{!TCOr (∀ j y1 y2, Affine (Φ j y1 y2)) (∀ x2, Absorbing (Φ i x1 x2))} :
    l1 !! i = Some x1 →
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)
    ⊢ ∃ x2, ⌜l2 !! i = Some x2⌝ ∧ Φ i x1 x2.
Proof.
    intros Hl1. destruct (l2 !! i) as [x2|] eqn:Hl2.
    { rewrite -(bi.exist_intro x2) bi.pure_True // left_id.
      apply big_sepL2_lookup; [|done..]. destruct select (TCOr _ _); apply _. }
    rewrite big_sepL2_length. apply bi.pure_elim'=> ?.
    apply lookup_lt_Some in Hl1. apply lookup_ge_None in Hl2. lia.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_lookup_r Φ l1 l2 i x2
    `{!TCOr (∀ j y1 y2, Affine (Φ j y1 y2)) (∀ x1, Absorbing (Φ i x1 x2))} :
    l2 !! i = Some x2 →
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)
    ⊢ ∃ x1, ⌜l1 !! i = Some x1⌝ ∧ Φ i x1 x2.
Proof.
    intros Hl2. destruct (l1 !! i) as [x1|] eqn:Hl1.
    { rewrite -(bi.exist_intro x1) bi.pure_True // left_id.
      apply big_sepL2_lookup; [|done..]. destruct select (TCOr _ _); apply _. }
    rewrite big_sepL2_length. apply bi.pure_elim'=> ?.
    apply lookup_lt_Some in Hl2. apply lookup_ge_None in Hl1. lia.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_fmap_l {A'} (f : A → A') (Φ : nat → A' → B → PROP) l1 l2 :
    ([∗ list] k↦y1;y2 ∈ f <$> l1; l2, Φ k y1 y2)
    ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k (f y1) y2).
Proof.
    rewrite !big_sepL2_alt length_fmap zip_with_fmap_l zip_with_zip big_sepL_fmap.
    by f_equiv; f_equiv=> k [??].
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_fmap_r {B'} (g : B → B') (Φ : nat → A → B' → PROP) l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1; g <$> l2, Φ k y1 y2)
    ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 (g y2)).
Proof.
    rewrite !big_sepL2_alt length_fmap zip_with_fmap_r zip_with_zip big_sepL_fmap.
    by f_equiv; f_equiv=> k [??].
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_reverse_2 (Φ : A → B → PROP) l1 l2 :
    ([∗ list] y1;y2 ∈ l1;l2, Φ y1 y2) ⊢ ([∗ list] y1;y2 ∈ reverse l1;reverse l2, Φ y1 y2).
Proof.
    revert l2. induction l1 as [|x1 l1 IH]; intros [|x2 l2]; simpl; auto using False_elim.
    rewrite !reverse_cons (comm bi_sep) IH.
    by rewrite (big_sepL2_app _ _ [x1] _ [x2]) big_sepL2_singleton wand_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_reverse (Φ : A → B → PROP) l1 l2 :
    ([∗ list] y1;y2 ∈ reverse l1;reverse l2, Φ y1 y2) ⊣⊢ ([∗ list] y1;y2 ∈ l1;l2, Φ y1 y2).
Proof. apply (anti_symm _); by rewrite big_sepL2_reverse_2 ?reverse_involutive. Qed.