From stdpp Require Import countable fin_sets functions.
From iris.algebra Require Export big_op.
From iris.algebra Require Import list gmap.
From iris.bi Require Import derived_laws_later.
From iris.prelude Require Import options.
Import interface.bi derived_laws.bi derived_laws_later.bi.

Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
  (big_opL bi_sep (λ k x, P%I) l) : bi_scope.
Notation "'[∗' 'list]' x ∈ l , P" :=
  (big_opL bi_sep (λ _ x, P%I) l) : bi_scope.
Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps%I) : bi_scope.

Notation "'[∧' 'list]' k ↦ x ∈ l , P" :=
  (big_opL bi_and (λ k x, P%I) l) : bi_scope.
Notation "'[∧' 'list]' x ∈ l , P" :=
  (big_opL bi_and (λ _ x, P%I) l) : bi_scope.
Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps%I) : bi_scope.

Notation "'[∨' 'list]' k ↦ x ∈ l , P" :=
  (big_opL bi_or (λ k x, P%I) l) : bi_scope.
Notation "'[∨' 'list]' x ∈ l , P" :=
  (big_opL bi_or (λ _ x, P%I) l) : bi_scope.
Notation "'[∨]' Ps" := (big_opL bi_or (λ _ x, x) Ps%I) : bi_scope.

Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P%I) m) : bi_scope.
Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P%I) m) : bi_scope.

Notation "'[∧' 'map]' k ↦ x ∈ m , P" := (big_opM bi_and (λ k x, P) m) : bi_scope.
Notation "'[∧' 'map]' x ∈ m , P" := (big_opM bi_and (λ _ x, P) m) : bi_scope.

Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P%I) X) : bi_scope.

Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P%I) X) : bi_scope.

Fixpoint big_sepL2 {PROP : bi} {A B}
    (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) : PROP :=
  match l1, l2 with
  | [], [] ⇒ emp
  | x1 :: l1, x2 :: l2 ⇒ Φ 0 x1 x2 ∗ big_sepL2 (λ n, Φ (S n)) l1 l2
  | _, _ ⇒ False
  end%I.
Global Instance: Params (@big_sepL2) 3 := {}.
Global Arguments big_sepL2 {PROP A B} _ !_ !_ /.
Global Typeclasses Opaque big_sepL2.
Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
  (big_sepL2 (λ k x1 x2, P%I) l1 l2) : bi_scope.
Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" :=
  (big_sepL2 (λ _ x1 x2, P%I) l1 l2) : bi_scope.

Local Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
    (Φ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : PROP :=
  ⌜ dom m1 = dom m2 ⌝ ∧ [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2.
Local Definition big_sepM2_aux : seal (@big_sepM2_def). Proof. by eexists. Qed.
Definition big_sepM2 := big_sepM2_aux.(unseal).
Global Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
Local Definition big_sepM2_unseal : @big_sepM2 = _ := big_sepM2_aux.(seal_eq).
Global Instance: Params (@big_sepM2) 6 := {}.
Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
  (big_sepM2 (λ k x1 x2, P%I) m1 m2) : bi_scope.
Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P" :=
  (big_sepM2 (λ _ x1 x2, P%I) m1 m2) : bi_scope.

Section big_op.
Context {PROP : bi}.
Implicit Types P Q : PROP.
Implicit Types Ps Qs : list PROP.
Implicit Types A : Type.

Section sep_list.
  Context {A : Type}.
  Implicit Types l : list A.
  Implicit Types Φ Ψ : nat → A → PROP.

  Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ emp.
  Proof. done. Qed.
  Lemma big_sepL_nil' P `{!Affine P} Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y.
  Proof. apply: affine. Qed.
  Lemma big_sepL_cons Φ x l :
    ([∗ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∗ [∗ list] k↦y ∈ l, Φ (S k) y.
  Proof. by rewrite big_opL_cons. Qed.
  Lemma big_sepL_singleton Φ x : ([∗ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x.
  Proof. by rewrite big_opL_singleton. Qed.
  Lemma big_sepL_app Φ l1 l2 :
    ([∗ list] k↦y ∈ l1 ++ l2, Φ k y)
    ⊣⊢ ([∗ list] k↦y ∈ l1, Φ k y) ∗ ([∗ list] k↦y ∈ l2, Φ (length l1 + k) y).
  Proof. by rewrite big_opL_app. Qed.
  Lemma big_sepL_snoc Φ l x :
    ([∗ list] k↦y ∈ l ++ [x], Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k y) ∗ Φ (length l) x.
  Proof. by rewrite big_opL_snoc. Qed.

  Lemma big_sepL_take_drop Φ l n :
    ([∗ list] k ↦ x ∈ l, Φ k x) ⊣⊢
    ([∗ list] k ↦ x ∈ take n l, Φ k x) ∗ ([∗ list] k ↦ x ∈ drop n l, Φ (n + k) x).
  Proof. by rewrite big_opL_take_drop. Qed.

  Lemma big_sepL_submseteq (Φ : A → PROP) `{!∀ x, Affine (Φ x)} l1 l2 :
    l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
  Proof.
    intros [l ->]%submseteq_Permutation. rewrite big_sepL_app.
    induction l as [|x l IH]; simpl; [by rewrite right_id|by rewrite sep_elim_r].
  Qed.

  Lemma big_sepL_mono Φ Ψ l :
    (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) →
    ([∗ list] k ↦ y ∈ l, Φ k y) ⊢ [∗ list] k ↦ y ∈ l, Ψ k y.
  Proof. apply big_opL_gen_proper; apply _. Qed.
  Lemma big_sepL_ne Φ Ψ l n :
    (∀ k y, l !! k = Some y → Φ k y ≡{n}≡ Ψ k y) →
    ([∗ list] k ↦ y ∈ l, Φ k y)%I ≡{n}≡ ([∗ list] k ↦ y ∈ l, Ψ k y)%I.
  Proof. apply big_opL_ne. Qed.
  Lemma big_sepL_proper Φ Ψ l :
    (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) →
    ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∗ list] k ↦ y ∈ l, Ψ k y).
  Proof. apply big_opL_proper. Qed.

  Global Instance big_sepL_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
           (big_opL (@bi_sep PROP) (A:=A)).
  Proof. intros f g Hf m ? <-. apply big_sepL_mono; intros; apply Hf. Qed.
  Global Instance big_sepL_id_mono' :
    Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_sep PROP) (λ _ P, P)).
  Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

  Global Instance big_sepL_nil_persistent Φ :
    Persistent ([∗ list] k↦x ∈ [], Φ k x).
  Proof. simpl; apply _. Qed.
  Lemma big_sepL_persistent Φ l :
    (∀ k x, l !! k = Some x → Persistent (Φ k x)) →
    Persistent ([∗ list] k↦x ∈ l, Φ k x).
  Proof. apply big_opL_closed; apply _. Qed.
  Global Instance big_sepL_persistent' Φ l :
    (∀ k x, Persistent (Φ k x)) → Persistent ([∗ list] k↦x ∈ l, Φ k x).
  Proof. intros; apply big_sepL_persistent, _. Qed.
  Global Instance big_sepL_persistent_id Ps :
    TCForall Persistent Ps → Persistent ([∗] Ps).
  Proof. induction 1; simpl; apply _. Qed.

  Global Instance big_sepL_nil_affine Φ :
    Affine ([∗ list] k↦x ∈ [], Φ k x).
  Proof. simpl; apply _. Qed.
  Lemma big_sepL_affine Φ l :
    (∀ k x, l !! k = Some x → Affine (Φ k x)) →
    Affine ([∗ list] k↦x ∈ l, Φ k x).
  Proof. apply big_opL_closed; apply _. Qed.
  Global Instance big_sepL_affine' Φ l :
    (∀ k x, Affine (Φ k x)) → Affine ([∗ list] k↦x ∈ l, Φ k x).
  Proof. intros. apply big_sepL_affine, _. Qed.
  Global Instance big_sepL_affine_id Ps : TCForall Affine Ps → Affine ([∗] Ps).
  Proof. induction 1; simpl; apply _. Qed.

  Global Instance big_sepL_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
    Timeless ([∗ list] k↦x ∈ [], Φ k x).
  Proof. simpl; apply _. Qed.
  Lemma big_sepL_timeless `{!Timeless (emp%I : PROP)} Φ l :
    (∀ k x, l !! k = Some x → Timeless (Φ k x)) →
    Timeless ([∗ list] k↦x ∈ l, Φ k x).
  Proof. apply big_opL_closed; apply _. Qed.
  Global Instance big_sepL_timeless' `{!Timeless (emp%I : PROP)} Φ l :
    (∀ k x, Timeless (Φ k x)) →
    Timeless ([∗ list] k↦x ∈ l, Φ k x).
  Proof. intros. apply big_sepL_timeless, _. Qed.
  Global Instance big_sepL_timeless_id `{!Timeless (emp%I : PROP)} Ps :
    TCForall Timeless Ps → Timeless ([∗] Ps).
  Proof. induction 1; simpl; apply _. Qed.

  Lemma big_sepL_emp l : ([∗ list] k↦y ∈ l, emp) ⊣⊢@{PROP} emp.
  Proof. by rewrite big_opL_unit. Qed.

  Lemma big_sepL_insert_acc Φ l i x :
    l !! i = Some x →
    ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x ∗ (∀ y, Φ i y -∗ ([∗ list] k↦y ∈ <[i:=y]>l, Φ k y)).
  Proof.
    intros Hli. assert (i ≤ length l) by eauto using lookup_lt_Some, Nat.lt_le_incl.
    rewrite -(take_drop_middle l i x) // big_sepL_app /=.
    rewrite Nat.add_0_r take_length_le //.
    rewrite assoc -!(comm _ (Φ _ _)) -assoc. apply sep_mono_r, forall_intro⇒ y.
    rewrite insert_app_r_alt ?take_length_le //.
    rewrite Nat.sub_diag /=. apply wand_intro_l.
    rewrite assoc !(comm _ (Φ _ _)) -assoc big_sepL_app /=.
    by rewrite Nat.add_0_r take_length_le.
  Qed.

  Lemma big_sepL_lookup_acc Φ l i x :
    l !! i = Some x →
    ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x ∗ (Φ i x -∗ ([∗ list] k↦y ∈ l, Φ k y)).
  Proof. intros. by rewrite {1}big_sepL_insert_acc // (forall_elim x) list_insert_id. Qed.

  Lemma big_sepL_lookup Φ l i x
    `{!TCOr (∀ j y, Affine (Φ j y)) (Absorbing (Φ i x))} :
    l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x.
  Proof.
    intros Hi. destruct select (TCOr _ _).
    - rewrite -(take_drop_middle l i x) // big_sepL_app /= take_length.
      apply lookup_lt_Some in Hi. rewrite (_ : _ + 0 = i); last lia.
      rewrite sep_elim_r sep_elim_l //.
    - rewrite big_sepL_lookup_acc // sep_elim_l //.
  Qed.

  Lemma big_sepL_elem_of (Φ : A → PROP) l x
    `{!TCOr (∀ y, Affine (Φ y)) (Absorbing (Φ x))} :
    x ∈ l → ([∗ list] y ∈ l, Φ y) ⊢ Φ x.
  Proof.
    intros [i ?]%elem_of_list_lookup.
    destruct select (TCOr _ _); by apply: big_sepL_lookup.
  Qed.

  Lemma big_sepL_fmap {B} (f : A → B) (Φ : nat → B → PROP) l :
    ([∗ list] k↦y ∈ f <$> l, Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k (f y)).
  Proof. by rewrite big_opL_fmap. Qed.

  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.

  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.

  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.

  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.

  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.

  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.
  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.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  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 take_length_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 take_length in Hk. by rewrite decide_False; last lia.
    - apply big_sepL_proper⇒ k y _. by rewrite decide_False; last lia.
  Qed.
  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.

  Lemma big_sepL_lookup_acc_impl {Φ l} i x :
    l !! i = Some x →
    ([∗ list] k↦y ∈ l, Φ k y) -∗
    
    Φ i x ∗
    
    ∀ Ψ,
      □ (∀ 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.

  Lemma big_sepL_replicate l P :
    [∗] replicate (length l) P ⊣⊢ [∗ list] y ∈ l, P.
  Proof. induction l as [|x l]=> //=; by f_equiv. Qed.

  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.
  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.

  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.
  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.
End sep_list.

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.

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.

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.

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.

Section sep_list2.
  Context {A B : Type}.
  Implicit Types Φ Ψ : nat → A → B → PROP.

  Lemma big_sepL2_nil Φ : ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2) ⊣⊢ emp.
  Proof. done. Qed.
  Lemma big_sepL2_nil' P `{!Affine P} Φ : P ⊢ [∗ list] k↦y1;y2 ∈ [];[], Φ k y1 y2.
  Proof. apply: affine. Qed.
  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.
  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.

  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.
  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.
  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.

  Lemma big_sepL2_singleton Φ x1 x2 :
    ([∗ list] k↦y1;y2 ∈ [x1];[x2], Φ k y1 y2) ⊣⊢ Φ 0 x1 x2.
  Proof. by rewrite /= right_id. Qed.

  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.

  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 !fmap_length.
    by rewrite pure_True // True_and zip_fst_snd.
  Qed.

  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.
  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.
  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.
  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 /= app_length.
      apply pure_elim'; lia.
    - destruct Hlen as [[=]|Hlen]. rewrite big_sepL2_length -Hlen /= app_length.
      apply pure_elim'; lia.
    - by rewrite -assoc IH; last lia.
  Qed.
  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.

  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.