phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/algebra.v *)
(* Derived lemma: If two [x y : agree O] compose to some [to_agree a],
      they are internally equal, and also equal to the [to_agree a].

      Empirically, [x ⋅ y ≡ to_agree a] appears often when agreement comes up
      in CMRA validity terms, especially when [view]s are involved. The desired
      simplification [x ≡ y ∧ y ≡ to_agree a] is also not straightforward to
      derive, so we have a special lemma to handle this common case. *)
Lemma agree_op_equiv_to_agreeI x y a :
      x ⋅ y ≡ to_agree a ⊢ x ≡ y ∧ y ≡ to_agree a.
Proof.
      assert (x ⋅ y ≡ to_agree a ⊢ x ≡ y) as Hxy_equiv.
      { rewrite -(agree_op_invI x y) internal_eq_sym.
        apply: (internal_eq_rewrite' _ _ (λ o, ✓ o)%I); [solve_proper|done|].
        rewrite -(bi.absorbing_absorbingly (✓ _)).
        rewrite -to_agree_validI bi.absorbingly_emp_True. apply bi.True_intro. }
      apply bi.and_intro; first done.
      rewrite -{1}(idemp bi_and (_ ≡ _)%I) {1}Hxy_equiv. apply bi.impl_elim_l'.
      apply: (internal_eq_rewrite' _ _
        (λ y', x ⋅ y' ≡ to_agree a → y' ≡ to_agree a)%I); [solve_proper|done|].
      rewrite agree_idemp. apply bi.impl_refl.
    Qed.
(* iris/bi/algebra.v *)
Lemma agree_includedI (x y : agree A) : x ≼ y ⊣⊢ y ≡ x ⋅ y.
Proof. sbi_unfold=> n. apply agree_includedN. Qed.
(* iris/bi/algebra.v *)
Lemma to_agree_includedI a b : to_agree a ≼ to_agree b ⊣⊢ a ≡ b.
Proof. sbi_unfold=> n. apply: to_agree_includedN. Qed.
(* iris/bi/algebra.v *)
Lemma csum_equivI (x y : csum A B) :
      x ≡ y ⊣⊢ match x, y with
                          | Cinl a, Cinl a' => a ≡ a'
                          | Cinr b, Cinr b' => b ≡ b'
                          | CsumInvalid, CsumInvalid => True
                          | _, _ => False
                          end.
Proof.
      sbi_unfold; split; [by destruct 1|destruct x, y; by repeat constructor].
    Qed.
(* iris/bi/algebra.v *)
Lemma csum_validI (x : csum A B) :
      ✓ x ⊣⊢ match x with
                        | Cinl a => ✓ a
                        | Cinr b => ✓ b
                        | CsumInvalid => False
                        end.
Proof. by sbi_unfold. Qed.
(* iris/bi/algebra.v *)
Lemma csum_includedI (sx sy : csum A B) :
      sx ≼ sy ⊣⊢ match sx, sy with
                 | Cinl x, Cinl y => x ≼ y
                 | Cinr x, Cinr y => x ≼ y
                 | _, CsumInvalid => True
                 | _, _ => False
                 end.
Proof.
      sbi_unfold=> n; destruct sx, sy; rewrite ?csum_includedN; naive_solver.
    Qed.
(* iris/bi/algebra.v *)
Lemma view_both_dfrac_validI_1 (relI : siProp) dq a b :
      (∀ n, rel n a b → siProp_holds relI n) →
      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
Proof.
      intros. sbi_unfold=> n. rewrite view_both_dfrac_validN. naive_solver.
    Qed.
(* iris/bi/algebra.v *)
Lemma view_both_dfrac_validI_2 (relI : siProp) dq a b :
      (∀ n, siProp_holds relI n → rel n a b) →
      ⌜✓dq⌝ ∧ <si_pure> relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
Proof.
      intros. sbi_unfold=> n. rewrite view_both_dfrac_validN. naive_solver.
    Qed.
(* iris/bi/algebra.v *)
Lemma view_both_dfrac_validI (relI : siProp) dq a b :
      (∀ n, rel n a b ↔ siProp_holds relI n) →
      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
Proof.
      intros. apply (anti_symm _);
        [apply view_both_dfrac_validI_1|apply view_both_dfrac_validI_2]; naive_solver.
    Qed.
(* iris/bi/algebra.v *)
Lemma view_both_validI_1 (relI : siProp) a b :
      (∀ n, rel n a b → siProp_holds relI n) →
      ✓ (●V a ⋅ ◯V b : view rel) ⊢ <si_pure> relI.
Proof. intros. by rewrite view_both_dfrac_validI_1 // bi.and_elim_r. Qed.
(* iris/bi/algebra.v *)
Lemma view_both_validI_2 (relI : siProp) a b :
      (∀ n, siProp_holds relI n → rel n a b) →
      <si_pure> relI ⊢ ✓ (●V a ⋅ ◯V b : view rel).
Proof.
      intros. rewrite -view_both_dfrac_validI_2 //.
      apply bi.and_intro; [|done]. by apply bi.pure_intro.
    Qed.
(* iris/bi/algebra.v *)
Lemma view_both_validI (relI : siProp) a b :
      (∀ n, rel n a b ↔ siProp_holds relI n) →
      ✓ (●V a ⋅ ◯V b : view rel) ⊣⊢ <si_pure> relI.
Proof.
      intros. apply (anti_symm _);
        [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
    Qed.
(* iris/bi/algebra.v *)
Lemma view_auth_dfrac_validI (relI : siProp) dq a :
      (∀ n, siProp_holds relI n ↔ rel n a ε) →
      ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
Proof.
      intros. rewrite -(right_id ε op (●V{dq} a)). by apply view_both_dfrac_validI.
    Qed.
(* iris/bi/algebra.v *)
Lemma view_auth_validI (relI : siProp) a :
      (∀ n, siProp_holds relI n ↔ rel n a ε) →
      ✓ (●V a : view rel) ⊣⊢ <si_pure> relI.
Proof. intros. rewrite -(right_id ε op (●V a)). by apply view_both_validI. Qed.
(* iris/bi/algebra.v *)
Lemma view_frag_validI (relI : siProp) b :
      (∀ n, siProp_holds relI n ↔ ∃ a, rel n a b) →
      ✓ (◯V b : view rel) ⊣⊢ <si_pure> relI.
Proof. intros Hrel. sbi_unfold=> n. by rewrite Hrel. Qed.
(* iris/bi/algebra.v *)
Lemma auth_auth_dfrac_validI dq a : ✓ (●{dq} a) ⊣⊢ ⌜✓dq⌝ ∧ ✓ a.
Proof. sbi_unfold=> n. apply auth_auth_dfrac_validN. Qed.
(* iris/bi/algebra.v *)
Lemma auth_auth_validI a : ✓ (● a) ⊣⊢ ✓ a.
Proof. sbi_unfold=> n. apply auth_auth_validN. Qed.
(* iris/bi/algebra.v *)
Lemma auth_auth_dfrac_op_validI dq1 dq2 a1 a2 :
      ✓ (●{dq1} a1 ⋅ ●{dq2} a2) ⊣⊢ ✓ (dq1 ⋅ dq2) ∧ (a1 ≡ a2) ∧ ✓ a1.
Proof. sbi_unfold=> n. apply auth_auth_dfrac_op_validN. Qed.
(* iris/bi/algebra.v *)
Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢ ✓ a.
Proof. sbi_unfold=> n. apply auth_frag_validN. Qed.
(* iris/bi/algebra.v *)
Lemma auth_both_dfrac_validI dq a b :
      ✓ (●{dq} a ⋅ ◯ b) ⊣⊢ ⌜✓dq⌝ ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
Proof.  sbi_unfold=> n. apply auth_both_dfrac_validN. Qed.
(* iris/bi/algebra.v *)
Lemma auth_both_validI a b :
      ✓ (● a ⋅ ◯ b) ⊣⊢ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
Proof. sbi_unfold=> n. apply auth_both_validN. Qed.
(* iris/bi/algebra.v *)
Lemma excl_auth_agreeI a b : ✓ (●E a ⋅ ◯E b) ⊢ (a ≡ b).
Proof. sbi_unfold=> n. apply excl_auth_agreeN. Qed.
(* iris/bi/algebra.v *)
Lemma dfrac_agree_validI dq a : ✓ (to_dfrac_agree dq a) ⊣⊢ ⌜✓ dq⌝.
Proof. sbi_unfold=> n. rewrite /to_dfrac_agree pair_validN. naive_solver. Qed.
(* iris/bi/algebra.v *)
Lemma dfrac_agree_validI_2 dq1 dq2 a b :
      ✓ (to_dfrac_agree dq1 a ⋅ to_dfrac_agree dq2 b) ⊣⊢ ⌜✓ (dq1 ⋅ dq2)⌝ ∧ (a ≡ b).
Proof.
      rewrite prod_validI /= internal_cmra_valid_discrete to_agree_op_validI //.
    Qed.
(* iris/bi/algebra.v *)
Lemma frac_agree_validI q a : ✓ (to_frac_agree q a) ⊣⊢ ⌜(q ≤ 1)%Qp⌝.
Proof.
      rewrite dfrac_agree_validI dfrac_valid_own //.
    Qed.
(* iris/bi/algebra.v *)
Lemma frac_agree_validI_2 q1 q2 a b :
      ✓ (to_frac_agree q1 a ⋅ to_frac_agree q2 b) ⊣⊢ ⌜(q1 + q2 ≤ 1)%Qp⌝ ∧ (a ≡ b).
Proof.
      rewrite dfrac_agree_validI_2 dfrac_valid_own //.
    Qed.
(* iris/bi/algebra.v *)
Lemma gmap_view_both_dfrac_validI dp m k dq v :
      ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ⊣⊢
      ∃ v' dq', ⌜✓ dp⌝ ∧ ⌜m !! k = Some v'⌝ ∧ ✓ (dq', v') ∧
                Some (dq, v) ≼ Some (dq', v').
Proof. sbi_unfold=> n. apply: gmap_view_both_dfrac_validN. Qed.
(* iris/bi/algebra.v *)
Lemma gmap_view_both_validI m dp k v :
      ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k (DfracOwn 1) v) ⊣⊢
      ⌜ ✓ dp ⌝ ∧ ✓ v ∧ m !! k ≡ Some v.
Proof. sbi_unfold=> n. apply gmap_view_both_validN. Qed.
(* iris/bi/algebra.v *)
Lemma gmap_view_both_validI_total `{!CmraTotal V} dp m k dq v :
      ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ⊢
      ∃ v', ⌜✓ dp ⌝ ∧ ⌜ ✓ dq⌝ ∧ ⌜m !! k = Some v'⌝ ∧ ✓ v' ∧ v ≼ v'.
Proof. sbi_unfold=> n. apply: gmap_view_both_dfrac_validN_total. Qed.
(* iris/bi/algebra.v *)
Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
      ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢
      ⌜✓ (dq1 ⋅ dq2)⌝ ∧ ✓ (v1 ⋅ v2).
Proof. sbi_unfold=> n. apply gmap_view_frag_op_validN. Qed.
(* iris/bi/ascii.v *)
Notation "P |- Q"
:= (P ⊢ Q)
  (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "P '|-@{' PROP } Q"
:= (P ⊢@{PROP} Q)
  (at level 99, Q at level 200, right associativity, only parsing)
  : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "(|-)"
:= (⊢) (only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "'(|-@{' PROP } )"
:= (⊢@{PROP}) (only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "|- Q"
:= (⊢ Q%I) (at level 20, Q at level 200, only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "'|-@{' PROP } Q"
:= (⊢@{PROP} Q) (at level 20, Q at level 200, only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
(* Work around parsing issues: see [notation.v] for details. *)
Notation "'(|-@{' PROP } Q )"
:= (⊢@{PROP} Q) (only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "P -|- Q"
:= (P ⊣⊢ Q) (at level 95, no associativity, only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "P '-|-@{' PROP } Q"
:= (P ⊣⊢@{PROP} Q)
  (at level 95, no associativity, only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "(-|-)"
:= (⊣⊢) (only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "'(-|-@{' PROP } )"
:= (⊣⊢@{PROP}) (only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "P -* Q"
:= (P ⊢ Q)%stdpp
  (at level 99, Q at level 200, right associativity, only parsing)
  : stdpp_scope.
(* iris/bi/ascii.v *)
(* FIXME: Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope. *)
Notation "P /\ Q"
:= (P ∧ Q)%I (only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "(/\)"
:= bi_and (only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "P \/ Q"
:= (P ∨ Q)%I (only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "(\/)"
:= bi_or (only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "P -> Q"
:= (P → Q)%I (only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "~ P"
:= (P → False)%I (only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "P ** Q"
:= (P ∗ Q)%I
  (at level 80, right associativity, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "(**)"
:= bi_sep (only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "P -* Q"
:= (P -∗ Q)%I
  (at level 99, Q at level 200, right associativity, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
(* ∀ x .. y , P *)
Notation "'forall' x .. y , P"
:=
  (bi_forall (fun x => .. (bi_forall (fun y => P%I)) ..))
  (at level 200, x binder, right associativity, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
(* ∃ x .. y , P *)
Notation "'exists' x .. y , P"
:=
  (bi_exist (fun x => .. (bi_exist (fun y => P%I)) ..))
  (at level 200, x binder, right associativity, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "|> P"
:= (▷ P)%I
  (at level 20, right associativity, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "|>? p P"
:= (▷?p P)%I (at level 20, p at level 9, P at level 20,
   only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "|>^ n P"
:= (▷^n P)%I (at level 20, n at level 9, P at level 20,
   only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "P <-> Q"
:= (P ↔ Q)%I
  (at level 95, no associativity, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "P *-* Q"
:= (P ∗-∗ Q)%I
  (at level 95, no associativity, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "'<#>' P"
:= (□ P)%I
  (at level 20, right associativity, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "'<#>?' p P"
:= (□?p P)%I (at level 20, p at level 9, P at level 20,
   right associativity, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "'<except_0>' P"
:= (◇ P)%I
  (at level 20, right associativity, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "mP -*? Q"
:= (mP -∗? Q)%I
  (at level 99, Q at level 200, right associativity, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "P ==* Q"
:= (P ==∗ Q)%stdpp
  (at level 99, Q at level 200, only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "P ==* Q"
:= (P ==∗ Q)%I
  (at level 99, Q at level 200, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "P ={ E1 , E2 }=* Q"
:= (P ={E1,E2}=∗ Q)%I
  (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "P ={ E1 , E2 }=* Q"
:= (P ={E1,E2}=∗ Q)
  (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "P ={ E }=* Q"
:= (P ={E}=∗ Q)%I
  (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "P ={ E }=* Q"
:= (P ={E}=∗ Q)
  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope
.
(* iris/bi/ascii.v *)
Notation "P ={ E1 } [ E2 ]|>=* Q"
:= (P ={E1}[E2]▷=∗ Q)
  (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "P ={ E1 } [ E2 ]|>=* Q"
:= (P ={E1}[E2]▷=∗ Q)%I
  (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "|={ E }|>=> Q"
:= (|={E}▷=> Q)%I
  (at level 20, E at level 50, Q at level 200, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "P ={ E }|>=* Q"
:= (P ={E}▷=∗ Q)%I
  (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
(* iris/bi/ascii.v *)
Notation "|={ E1 } [ E2 ]|>=>^ n Q"
:= (|={E1}[E2]▷=>^n Q)%I
  (at level 20, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
  : bi_scope.
(* iris/bi/ascii.v *)
Notation "P ={ E1 } [ E2 ]|>=*^ n Q"
:= (P ={E1}[E2]▷=∗^n Q)%I
  (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
   : stdpp_scope.
(* iris/bi/ascii.v *)
Notation "P ={ E1 } [ E2 ]|>=*^ n Q"
:= (P ={E1}[E2]▷=∗^n Q)%I
  (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
  : bi_scope.
(* iris/bi/big_op.v *)
(* Notations for unary variants *)
Notation big_sepL
:= (big_opL bi_sep) (only parsing).
(* iris/bi/big_op.v *)
Notation "'[∗' 'list]' k ↦ x ∈ l , P"
:= (big_sepL (λ k x, P%I) l) : bi_scope.
(* iris/bi/big_op.v *)
Notation "'[∗' 'list]' x ∈ l , P"
:= (big_sepL (λ _ x, P%I) l) : bi_scope.
(* iris/bi/big_op.v *)
Notation "'[∗]' Ps"
:= (big_sepL (λ _ x, x) Ps%I) : bi_scope.
(* iris/bi/big_op.v *)
Notation big_andL
:= (big_opL bi_and) (only parsing).
(* iris/bi/big_op.v *)
Notation "'[∧' 'list]' k ↦ x ∈ l , P"
:= (big_andL (λ k x, P%I) l) : bi_scope.
(* iris/bi/big_op.v *)
Notation "'[∧' 'list]' x ∈ l , P"
:= (big_andL (λ _ x, P%I) l) : bi_scope.
(* iris/bi/big_op.v *)
Notation "'[∧]' Ps"
:= (big_andL (λ _ x, x) Ps%I) : bi_scope.
(* iris/bi/big_op.v *)
Notation big_orL
:= (big_opL bi_or) (only parsing).
(* iris/bi/big_op.v *)
Notation "'[∨' 'list]' k ↦ x ∈ l , P"
:= (big_orL (λ k x, P%I) l) : bi_scope.
(* iris/bi/big_op.v *)
Notation "'[∨' 'list]' x ∈ l , P"
:= (big_orL (λ _ x, P%I) l) : bi_scope.
(* iris/bi/big_op.v *)
Notation "'[∨]' Ps"
:= (big_orL (λ _ x, x) Ps%I) : bi_scope.
(* iris/bi/big_op.v *)
Notation big_sepM
:= (big_opM bi_sep) (only parsing).
(* iris/bi/big_op.v *)
Notation "'[∗' 'map]' k ↦ x ∈ m , P"
:= (big_sepM (λ k x, P%I) m) : bi_scope.
(* iris/bi/big_op.v *)
Notation "'[∗' 'map]' x ∈ m , P"
:= (big_sepM (λ _ x, P%I) m) : bi_scope.
(* iris/bi/big_op.v *)
Notation big_andM
:= (big_opM bi_and) (only parsing).
(* iris/bi/big_op.v *)
Notation "'[∧' 'map]' k ↦ x ∈ m , P"
:= (big_andM (λ k x, P) m) : bi_scope.
(* iris/bi/big_op.v *)
Notation "'[∧' 'map]' x ∈ m , P"
:= (big_andM (λ _ x, P) m) : bi_scope.
(* iris/bi/big_op.v *)
Notation big_sepS
:= (big_opS bi_sep) (only parsing).
(* iris/bi/big_op.v *)
Notation "'[∗' 'set]' x ∈ X , P"
:= (big_sepS (λ x, P%I) X) : bi_scope.
(* iris/bi/big_op.v *)
Notation big_sepMS
:= (big_opMS bi_sep) (only parsing).
(* iris/bi/big_op.v *)
Notation "'[∗' 'mset]' x ∈ X , P"
:= (big_sepMS (λ x, P%I) X) : bi_scope.
(* iris/bi/big_op.v *)
(* A version of the separating big operator that ranges over two lists. This
version also ensures that both lists have the same length. Although this version
can be defined in terms of the unary using a [zip] (see [big_sepL2_alt]), we do
not define it that way to get better computational behavior (for [simpl]). *)
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.
(* iris/bi/big_op.v *)
Instance : Params (@big_sepL2) 3
:= {}.
(* iris/bi/big_op.v *)
Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P"
:=
  (big_sepL2 (λ k x1 x2, P%I) l1 l2) : bi_scope.
(* iris/bi/big_op.v *)
Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P"
:=
  (big_sepL2 (λ _ x1 x2, P%I) l1 l2) : bi_scope.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
Definition big_sepM2_aux : seal (@big_sepM2_def).
Proof. by eexists. Qed.
(* iris/bi/big_op.v *)
Definition big_sepM2
:= big_sepM2_aux.(unseal).
(* iris/bi/big_op.v *)
Definition big_sepM2_unseal : @big_sepM2 = _
:= big_sepM2_aux.(seal_eq).
(* iris/bi/big_op.v *)
Instance : Params (@big_sepM2) 6
:= {}.
(* iris/bi/big_op.v *)
Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P"
:=
  (big_sepM2 (λ k x1 x2, P%I) m1 m2) : bi_scope.
(* iris/bi/big_op.v *)
Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P"
:=
  (big_sepM2 (λ _ x1 x2, P%I) m1 m2) : bi_scope.
(* iris/bi/big_op.v *)
Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ emp.
Proof. done. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_nil' P `{!Affine P} Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y.
Proof. apply: affine. Qed.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
Lemma big_sepL_singleton Φ x : ([∗ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x.
Proof. by rewrite big_opL_singleton. Qed.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
(* The lemmas [big_sepL_mono], [big_sepL_ne] and [big_sepL_proper] are more
  generic than the instances as they also give [l !! k = Some y] in the premise. *)
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.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
(* No need to declare instances for non-expansiveness and properness, we
  get both from the generic [big_opL] instances. *)
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.
(* iris/bi/big_op.v *)
Instance big_sepL_flip_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ (flip (⊢))) ==> (=) ==> flip (⊢))
           (big_opL (@bi_sep PROP) (A:=A)).
Proof. solve_proper. Qed.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
Instance big_sepL_nil_persistent Φ :
    Persistent ([∗ list] k↦x ∈ [], Φ k x).
Proof. simpl; apply _. Qed.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
Instance big_sepL_persistent' Φ l :
    (∀ k x, Persistent (Φ k x)) → Persistent ([∗ list] k↦x ∈ l, Φ k x).
Proof. intros; apply big_sepL_persistent, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL_persistent_id Ps :
    TCForall Persistent Ps → Persistent ([∗] Ps).
Proof. induction 1; simpl; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL_nil_affine Φ :
    Affine ([∗ list] k↦x ∈ [], Φ k x).
Proof. simpl; apply _. Qed.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
Instance big_sepL_affine' Φ l :
    (∀ k x, Affine (Φ k x)) → Affine ([∗ list] k↦x ∈ l, Φ k x).
Proof. intros. apply big_sepL_affine, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL_affine_id Ps : TCForall Affine Ps → Affine ([∗] Ps).
Proof. induction 1; simpl; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepL_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
    Timeless ([∗ list] k↦x ∈ [], Φ k x).
Proof. simpl; apply _. Qed.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
Instance big_sepL_timeless_id `{!Timeless (emp%I : PROP)} Ps :
    TCForall Timeless Ps → Timeless ([∗] Ps).
Proof. induction 1; simpl; apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_emp l : ([∗ list] k↦y ∈ l, emp) ⊣⊢@{PROP} emp.
Proof. by rewrite big_opL_unit. Qed.
(* iris/bi/big_op.v *)
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 length_take_le //.
    rewrite assoc -!(comm _ (Φ _ _)) -assoc. apply sep_mono_r, forall_intro=> y.
    rewrite insert_app_r_alt ?length_take_le //.
    rewrite Nat.sub_diag /=. apply wand_intro_l.
    rewrite assoc !(comm _ (Φ _ _)) -assoc big_sepL_app /=.
    by rewrite Nat.add_0_r length_take_le.
  Qed.
(* iris/bi/big_op.v *)
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.
(* iris/bi/big_op.v *)
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 /= length_take.
      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.
(* iris/bi/big_op.v *)
Lemma big_sepL_elem_of_acc (Φ : A → PROP) l x :
    x ∈ l → ([∗ list] y ∈ l, Φ y) ⊢ Φ x ∗ (Φ x -∗ ([∗ list] y ∈ l, Φ y)).
Proof.
    intros [i ?]%list_elem_of_lookup.
    by apply: big_sepL_lookup_acc.
  Qed.
(* iris/bi/big_op.v *)
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 ?]%list_elem_of_lookup.
    destruct select (TCOr _ _); by apply: big_sepL_lookup.
  Qed.
(* iris/bi/big_op.v *)
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.