phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/auth.v *)
(* These lemma statements are a bit awkward as we cannot possibly extract a
  single witness for [b ≼ a] from validity, we have to make do with one witness
  per step-index, i.e., [∀ n, b ≼{n} a]. *)
Lemma auth_both_dfrac_valid dq a b :
    ✓ (●{dq} a ⋅ ◯ b) ↔  ✓ dq ∧ (∀ n, b ≼{n} a) ∧ ✓ a.
Proof.
    rewrite view_both_dfrac_valid. apply and_iff_compat_l. split.
    - intros Hrel. split.
      + intros n. by destruct (Hrel n).
      + apply cmra_valid_validN=> n. by destruct (Hrel n).
    - intros [Hincl Hval] n. split; [done|by apply cmra_valid_validN].
  Qed.
(* iris/algebra/auth.v *)
Lemma auth_both_valid a b :
    ✓ (● a ⋅ ◯ b) ↔ (∀ n, b ≼{n} a) ∧ ✓ a.
Proof. rewrite auth_both_dfrac_valid. split; [naive_solver|done]. Qed.
(* iris/algebra/auth.v *)
(* The reverse direction of the two lemmas below only holds if the camera is
  discrete. *)
Lemma auth_both_dfrac_valid_2 dq a b : ✓ dq → ✓ a → b ≼ a → ✓ (●{dq} a ⋅ ◯ b).
Proof.
    intros. apply auth_both_dfrac_valid.
    naive_solver eauto using cmra_included_includedN.
  Qed.
(* iris/algebra/auth.v *)
Lemma auth_both_valid_2 a b : ✓ a → b ≼ a → ✓ (● a ⋅ ◯ b).
Proof. intros ??. by apply auth_both_dfrac_valid_2. Qed.
(* iris/algebra/auth.v *)
Lemma auth_both_dfrac_valid_discrete `{!CmraDiscrete A} dq a b :
    ✓ (●{dq} a ⋅ ◯ b) ↔ ✓ dq ∧ b ≼ a ∧ ✓ a.
Proof.
    rewrite auth_both_dfrac_valid. setoid_rewrite <-cmra_discrete_included_iff.
    pose 0ᵢ. naive_solver.
  Qed.
(* iris/algebra/auth.v *)
Lemma auth_both_valid_discrete `{!CmraDiscrete A} a b :
    ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
Proof. rewrite auth_both_dfrac_valid_discrete. split; [naive_solver|done]. Qed.
(* iris/algebra/auth.v *)
(* Inclusion *)
Lemma auth_auth_dfrac_includedN n dq1 dq2 a1 a2 b :
    ●{dq1} a1 ≼{n} ●{dq2} a2 ⋅ ◯ b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2.
Proof. apply view_auth_dfrac_includedN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_dfrac_included dq1 dq2 a1 a2 b :
    ●{dq1} a1 ≼ ●{dq2} a2 ⋅ ◯ b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2.
Proof. apply view_auth_dfrac_included. Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_includedN n a1 a2 b :
    ● a1 ≼{n} ● a2 ⋅ ◯ b ↔ a1 ≡{n}≡ a2.
Proof. apply view_auth_includedN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_included a1 a2 b :
    ● a1 ≼ ● a2 ⋅ ◯ b ↔ a1 ≡ a2.
Proof. apply view_auth_included. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_includedN n dq a b1 b2 :
    ◯ b1 ≼{n} ●{dq} a ⋅ ◯ b2 ↔ b1 ≼{n} b2.
Proof. apply view_frag_includedN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_included dq a b1 b2 :
    ◯ b1 ≼ ●{dq} a ⋅ ◯ b2 ↔ b1 ≼ b2.
Proof. apply view_frag_included. Qed.
(* iris/algebra/auth.v *)
(* The weaker [auth_both_included] lemmas below are a consequence of the
  [auth_auth_included] and [auth_frag_included] lemmas above. *)
Lemma auth_both_dfrac_includedN n dq1 dq2 a1 a2 b1 b2 :
    ●{dq1} a1 ⋅ ◯ b1 ≼{n} ●{dq2} a2 ⋅ ◯ b2 ↔
      (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
Proof. apply view_both_dfrac_includedN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_both_dfrac_included dq1 dq2 a1 a2 b1 b2 :
    ●{dq1} a1 ⋅ ◯ b1 ≼ ●{dq2} a2 ⋅ ◯ b2 ↔
      (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2 ∧ b1 ≼ b2.
Proof. apply view_both_dfrac_included. Qed.
(* iris/algebra/auth.v *)
Lemma auth_both_includedN n a1 a2 b1 b2 :
    ● a1 ⋅ ◯ b1 ≼{n} ● a2 ⋅ ◯ b2 ↔ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
Proof. apply view_both_includedN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_both_included a1 a2 b1 b2 :
    ● a1 ⋅ ◯ b1 ≼ ● a2 ⋅ ◯ b2 ↔ a1 ≡ a2 ∧ b1 ≼ b2.
Proof. apply view_both_included. Qed.
(* iris/algebra/auth.v *)
(* Updates *)
Lemma auth_update a b a' b' :
    (a,b) ~l~> (a',b') → ● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b'.
Proof.
    intros Hup. apply view_update=> n bf [[bf' Haeq] Hav].
    destruct (Hup n (Some (bf ⋅ bf'))); simpl in *; [done|by rewrite assoc|].
    split; [|done]. exists bf'. by rewrite -assoc.
  Qed.
(* iris/algebra/auth.v *)
Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a' ⋅ ◯ b'.
Proof. intros. rewrite -(right_id _ _ (● a)). by apply auth_update. Qed.
(* iris/algebra/auth.v *)
Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε) → ● a ⋅ ◯ b ~~> ● a'.
Proof. intros. rewrite -(right_id _ _ (● a')). by apply auth_update. Qed.
(* iris/algebra/auth.v *)
Lemma auth_update_auth a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a'.
Proof.
    intros. etrans; first exact: auth_update_alloc.
    exact: cmra_update_op_l.
  Qed.
(* iris/algebra/auth.v *)
Lemma auth_update_auth_persist dq a : ●{dq} a ~~> ●□ a.
Proof. apply view_update_auth_persist. Qed.
(* iris/algebra/auth.v *)
Lemma auth_updateP_auth_unpersist a : ●□ a ~~>: λ k, ∃ q, k = ●{#q} a.
Proof. apply view_updateP_auth_unpersist. Qed.
(* iris/algebra/auth.v *)
Lemma auth_updateP_both_unpersist a b : ●□ a ⋅ ◯ b ~~>: λ k, ∃ q, k = ●{#q} a ⋅ ◯ b.
Proof. apply view_updateP_both_unpersist. Qed.
(* iris/algebra/auth.v *)
Lemma auth_update_dfrac_alloc dq a b `{!CoreId b} :
    b ≼ a → ●{dq} a ~~> ●{dq} a ⋅ ◯ b.
Proof.
    intros Ha%(core_id_extract _ _). apply view_update_dfrac_alloc=> n bf [??].
    split; [|done]. rewrite Ha (comm _ a). by apply cmra_monoN_l.
  Qed.
(* iris/algebra/auth.v *)
Lemma auth_local_update a b0 b1 a' b0' b1' :
    (b0, b1) ~l~> (b0', b1') → b0' ≼ a' → ✓ a' →
    (● a ⋅ ◯ b0, ● a ⋅ ◯ b1) ~l~> (● a' ⋅ ◯ b0', ● a' ⋅ ◯ b1').
Proof.
    intros. apply view_local_update; [done|]=> n [??]. split.
    - by apply cmra_included_includedN.
    - by apply cmra_valid_validN.
  Qed.
(* iris/algebra/auth.v *)
(* * Functor *)
Definition authURF {SI : sidx} (F : urFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
|}.
Next Obligation.
  intros ? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
  apply viewO_map_ne; by apply urFunctor_map_ne.
Qed.
(* iris/algebra/auth.v *)
Instance authURF_contractive {SI : sidx} F :
  urFunctorContractive F → urFunctorContractive (authURF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
  apply viewO_map_ne; by apply urFunctor_map_contractive.
Qed.
(* iris/algebra/auth.v *)
Definition authRF {SI : sidx} (F : urFunctor) : rFunctor
:= {|
  rFunctor_car A _ B _ := authR (urFunctor_car F A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
|}.
(* iris/algebra/auth.v *)
Instance authRF_contractive {SI : sidx} F :
  urFunctorContractive F → rFunctorContractive (authRF F).
Proof. apply authURF_contractive. Qed.
(* iris/algebra/big_op.v *)
(* * Big ops over lists *)
Fixpoint big_opL {SI : sidx} {M : ofe}
    (o : M → M → M) `{!MonoidOps o u} {A} (f : nat → A → M) (xs : list A) : M
:=
  match xs with
  | [] => u
  | x :: xs => o (f 0 x) (big_opL o (λ n, f (S n)) xs)
  end.
(* iris/algebra/big_op.v *)
Instance : Params (@big_opL) 6
:= {}.
(* iris/algebra/big_op.v *)
Notation "'[^' o 'list]' k ↦ x ∈ l , P"
:= (big_opL o (λ k x, P) l)
  (at level 200, o at level 1, l at level 200, k, x at level 1, right associativity,
   format "[^ o  list]  k ↦ x  ∈  l ,  P") : stdpp_scope.
(* iris/algebra/big_op.v *)
Notation "'[^' o 'list]' x ∈ l , P"
:= (big_opL o (λ _ x, P) l)
  (at level 200, o at level 1, l at level 200, x at level 1, right associativity,
   format "[^ o  list]  x  ∈  l ,  P") : stdpp_scope.
(* iris/algebra/big_op.v *)
Definition big_opM_def {SI : sidx} {M : ofe}
  {o : M → M → M} `{!MonoidOps o u} `{Countable K} {A} (f : K → A → M)
  (m : gmap K A) : M
:= big_opL o (λ _, uncurry f) (map_to_list m).
(* iris/algebra/big_op.v *)
Definition big_opM_aux : seal (@big_opM_def).
Proof. by eexists. Qed.
(* iris/algebra/big_op.v *)
Definition big_opM
:= big_opM_aux.(unseal).
(* iris/algebra/big_op.v *)
Definition big_opM_unseal :
  @big_opM = @big_opM_def
:= big_opM_aux.(seal_eq).
(* iris/algebra/big_op.v *)
Instance : Params (@big_opM) 9
:= {}.
(* iris/algebra/big_op.v *)
Notation "'[^' o 'map]' k ↦ x ∈ m , P"
:= (big_opM o (λ k x, P) m)
  (at level 200, o at level 1, m at level 200, k, x at level 1, right associativity,
   format "[^  o  map]  k ↦ x  ∈  m ,  P") : stdpp_scope.
(* iris/algebra/big_op.v *)
Notation "'[^' o 'map]' x ∈ m , P"
:= (big_opM o (λ _ x, P) m)
  (at level 200, o at level 1, m at level 200, x at level 1, right associativity,
   format "[^ o  map]  x  ∈  m ,  P") : stdpp_scope.
(* iris/algebra/big_op.v *)
Definition big_opS_def {SI : sidx} {M : ofe}
  {o : M → M → M} `{!MonoidOps o u} `{Countable A} (f : A → M)
  (X : gset A) : M
:= big_opL o (λ _, f) (elements X).
(* iris/algebra/big_op.v *)
Definition big_opS_aux : seal (@big_opS_def).
Proof. by eexists. Qed.
(* iris/algebra/big_op.v *)
Definition big_opS
:= big_opS_aux.(unseal).
(* iris/algebra/big_op.v *)
Definition big_opS_unseal :
  @big_opS = @big_opS_def
:= big_opS_aux.(seal_eq).
(* iris/algebra/big_op.v *)
Instance : Params (@big_opS) 8
:= {}.
(* iris/algebra/big_op.v *)
Notation "'[^' o 'set]' x ∈ X , P"
:= (big_opS o (λ x, P) X)
  (at level 200, o at level 1, X at level 200, x at level 1, right associativity,
   format "[^ o  set]  x  ∈  X ,  P") : stdpp_scope.
(* iris/algebra/big_op.v *)
Definition big_opMS_def {SI : sidx} {M : ofe}
  {o : M → M → M} `{!MonoidOps o u} `{Countable A} (f : A → M)
  (X : gmultiset A) : M
:= big_opL o (λ _, f) (elements X).
(* iris/algebra/big_op.v *)
Definition big_opMS_aux : seal (@big_opMS_def).
Proof. by eexists. Qed.
(* iris/algebra/big_op.v *)
Definition big_opMS
:= big_opMS_aux.(unseal).
(* iris/algebra/big_op.v *)
Definition big_opMS_unseal :
  @big_opMS = @big_opMS_def
:= big_opMS_aux.(seal_eq).
(* iris/algebra/big_op.v *)
Instance : Params (@big_opMS) 9
:= {}.
(* iris/algebra/big_op.v *)
Notation "'[^' o 'mset]' x ∈ X , P"
:= (big_opMS o (λ x, P) X)
  (at level 200, o at level 1, X at level 200, x at level 1, right associativity,
   format "[^ o  mset]  x  ∈  X ,  P") : stdpp_scope.
(* iris/algebra/big_op.v *)
Lemma big_opL_nil f : ([^o list] k↦y ∈ [], f k y) = u.
Proof. done. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_cons f x l :
    ([^o list] k↦y ∈ x :: l, f k y) = f 0 x `o` [^o list] k↦y ∈ l, f (S k) y.
Proof. done. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_singleton f x : ([^o list] k↦y ∈ [x], f k y) ≡ f 0 x.
Proof. by rewrite /= right_id. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_app f l1 l2 :
    ([^o list] k↦y ∈ l1 ++ l2, f k y)
    ≡ ([^o list] k↦y ∈ l1, f k y) `o` ([^o list] k↦y ∈ l2, f (length l1 + k) y).
Proof.
    revert f. induction l1 as [|x l1 IH]=> f /=; first by rewrite left_id.
    by rewrite IH assoc.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_snoc f l x :
    ([^o list] k↦y ∈ l ++ [x], f k y) ≡ ([^o list] k↦y ∈ l, f k y) `o` f (length l) x.
Proof. rewrite big_opL_app big_opL_singleton Nat.add_0_r //. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_unit l : ([^o list] k↦y ∈ l, u) ≡@{M} u.
Proof. induction l; rewrite /= ?left_id //. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_take_drop Φ l n :
    ([^o list] k ↦ x ∈ l, Φ k x) ≡
    ([^o list] k ↦ x ∈ take n l, Φ k x) `o` ([^o list] k ↦ x ∈ drop n l, Φ (n + k) x).
Proof.
    rewrite -{1}(take_drop n l) big_opL_app length_take.
    destruct (decide (length l ≤ n)).
    - rewrite drop_ge //=.
    - rewrite Nat.min_l //=; lia.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_gen_proper_2 {B} (R : relation M) f (g : nat → B → M)
        l1 (l2 : list B) :
    R u u →
    Proper (R ==> R ==> R) o →
    (∀ k,
      match l1 !! k, l2 !! k with
      | Some y1, Some y2 => R (f k y1) (g k y2)
      | None, None => True
      | _, _ => False
      end) →
    R ([^o list] k ↦ y ∈ l1, f k y) ([^o list] k ↦ y ∈ l2, g k y).
Proof.
    intros ??. revert l2 f g. induction l1 as [|x1 l1 IH]=> -[|x2 l2] //= f g Hfg.
    - by specialize (Hfg 0).
    - by specialize (Hfg 0).
    - f_equiv; [apply (Hfg 0)|]. apply IH. intros k. apply (Hfg (S k)).
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_gen_proper R f g l :
    Reflexive R →
    Proper (R ==> R ==> R) o →
    (∀ k y, l !! k = Some y → R (f k y) (g k y)) →
    R ([^o list] k ↦ y ∈ l, f k y) ([^o list] k ↦ y ∈ l, g k y).
Proof.
    intros. apply big_opL_gen_proper_2; [done..|].
    intros k. destruct (l !! k) eqn:?; auto.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_ext f g l :
    (∀ k y, l !! k = Some y → f k y = g k y) →
    ([^o list] k ↦ y ∈ l, f k y) = [^o list] k ↦ y ∈ l, g k y.
Proof. apply big_opL_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_permutation (f : A → M) l1 l2 :
    l1 ≡ₚ l2 → ([^o list] x ∈ l1, f x) ≡ ([^o list] x ∈ l2, f x).
Proof.
    induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
    - by rewrite IH.
    - by rewrite !assoc (comm _ (f x)).
    - by etrans.
  Qed.
(* iris/algebra/big_op.v *)
Instance big_opL_permutation' (f : A → M) :
    Proper ((≡ₚ) ==> (≡)) (big_opL o (λ _, f)).
Proof. intros xs1 xs2. apply big_opL_permutation. Qed.
(* iris/algebra/big_op.v *)
(* The lemmas [big_opL_ne] and [big_opL_proper] are more generic than the
  instances as they also give [l !! k = Some y] in the premise. *)
Lemma big_opL_ne f g l n :
    (∀ k y, l !! k = Some y → f k y ≡{n}≡ g k y) →
    ([^o list] k ↦ y ∈ l, f k y) ≡{n}≡ ([^o list] k ↦ y ∈ l, g k y).
Proof. apply big_opL_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_proper f g l :
    (∀ k y, l !! k = Some y → f k y ≡ g k y) →
    ([^o list] k ↦ y ∈ l, f k y) ≡ ([^o list] k ↦ y ∈ l, g k y).
Proof. apply big_opL_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
(* The version [big_opL_proper_2] with [≡] for the list arguments can only be
  used if there is a setoid on [A]. The version for [dist n] can be found in
  [algebra.list]. We do not define this lemma as a [Proper] instance, since
  [f_equiv] will then use sometimes use this one, and other times
  [big_opL_proper'], depending on whether a setoid on [A] exists. *)
Lemma big_opL_proper_2 `{!Equiv A} f g l1 l2 :
    l1 ≡ l2 →
    (∀ k y1 y2,
      l1 !! k = Some y1 → l2 !! k = Some y2 → y1 ≡ y2 → f k y1 ≡ g k y2) →
    ([^o list] k ↦ y ∈ l1, f k y) ≡ ([^o list] k ↦ y ∈ l2, g k y).
Proof.
    intros Hl Hf. apply big_opL_gen_proper_2; try (apply _ || done).
    (* FIXME (Coq #14441) unnecessary type annotation *)
    intros k. assert (l1 !! k ≡@{option A} l2 !! k) as Hlk by (by f_equiv).
    destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
  Qed.
(* iris/algebra/big_op.v *)
Instance big_opL_ne' n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (=) ==> dist n)
           (big_opL o (A:=A)).
Proof. intros f f' Hf l ? <-. apply big_opL_ne; intros; apply Hf. Qed.
(* iris/algebra/big_op.v *)
Instance big_opL_proper' :
    Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (=) ==> (≡))
           (big_opL o (A:=A)).
Proof. intros f f' Hf l ? <-. apply big_opL_proper; intros; apply Hf. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_consZ_l (f : Z → A → M) x l :
    ([^o list] k↦y ∈ x :: l, f k y) = f 0 x `o` [^o list] k↦y ∈ l, f (1 + k)%Z y.
Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_consZ_r (f : Z → A → M) x l :
    ([^o list] k↦y ∈ x :: l, f k y) = f 0 x `o` [^o list] k↦y ∈ l, f (k + 1)%Z y.
Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_fmap {B} (h : A → B) (f : nat → B → M) l :
    ([^o list] k↦y ∈ h <$> l, f k y) ≡ ([^o list] k↦y ∈ l, f k (h y)).
Proof. revert f. induction l as [|x l IH]=> f; csimpl=> //. by rewrite IH. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_omap {B} (h : A → option B) (f : B → M) l :
    ([^o list] y ∈ omap h l, f y) ≡ ([^o list] y ∈ l, from_option f u (h y)).
Proof.
    revert f. induction l as [|x l IH]=> f //; csimpl.
    case_match; csimpl; by rewrite IH // left_id.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_zip_seq (f : nat * A → M) n len l :
    length l ≤ len →
    ([^o list] ky ∈ zip (seq n len) l, f ky) ≡
    ([^o list] k ↦ y ∈ l, f (n + k, y)).
Proof.
    intros Hlen. induction l as [|x l IH] in n, len, Hlen |- *; simpl.
    { by rewrite zip_nil_r. }
    destruct len as [| len]; simpl in *; first lia.
    rewrite Nat.add_0_r IH; last lia.
    by setoid_rewrite Nat.add_succ_r.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_op f g l :
    ([^o list] k↦x ∈ l, f k x `o` g k x)
    ≡ ([^o list] k↦x ∈ l, f k x) `o` ([^o list] k↦x ∈ l, g k x).
Proof.
    revert f g; induction l as [|x l IH]=> f g /=; first by rewrite left_id.
    by rewrite IH -!assoc (assoc _ (g _ _)) [(g _ _ `o` _)]comm -!assoc.
  Qed.
(* iris/algebra/big_op.v *)
(* Shows that some property [P] is closed under [big_opL]. Examples of [P]
  are [Persistent], [Affine], [Timeless]. *)
Lemma big_opL_closed (P : M → Prop) f l :
    P u →
    (∀ x y, P x → P y → P (x `o` y)) →
    (∀ k x, l !! k = Some x → P (f k x)) →
    P ([^o list] k↦x ∈ l, f k x).
Proof.
    intros Hunit Hop. revert f. induction l as [|x l IH]=> f Hf /=; [done|].
    apply Hop; first by auto. apply IH=> k. apply (Hf (S k)).
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_zip_seqZ {A} (f : Z * A → M) n len l :
  length l ≤ len →
  ([^o list] ky ∈ zip (seqZ n len) l, f ky) ≡
  ([^o list] k ↦ y ∈ l, f ((n + k)%Z, y)).
Proof.
  intros Hlen. rewrite /seqZ -{1}(list_fmap_id l) -prod_map_zip.
  rewrite big_opL_fmap big_opL_zip_seq; last lia.
  f_equiv=> i x /=. by rewrite Z.add_comm.
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_bind {A B} (h : A → list B) (f : B → M) l :
  ([^o list] y ∈ l ≫= h, f y) ≡ ([^o list] x ∈ l, [^o list] y ∈ h x, f y).
Proof.
  revert f. induction l as [|x l IH]=> f; csimpl=> //. by rewrite big_opL_app IH.
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_sep_zip_with {A B C} (f : A → B → C) (g1 : C → A) (g2 : C → B)
    (h1 : nat → A → M) (h2 : nat → B → M) l1 l2 :
  (∀ x y, g1 (f x y) = x) →
  (∀ x y, g2 (f x y) = y) →
  length l1 = length l2 →
  ([^o list] k↦xy ∈ zip_with f l1 l2, h1 k (g1 xy) `o` h2 k (g2 xy)) ≡
  ([^o list] k↦x ∈ l1, h1 k x) `o` ([^o list] k↦y ∈ l2, h2 k y).
Proof.
  intros Hlen Hg1 Hg2. rewrite big_opL_op.
  rewrite -(big_opL_fmap g1) -(big_opL_fmap g2).
  rewrite fmap_zip_with_r; [|auto with lia..].
  by rewrite fmap_zip_with_l; [|auto with lia..].
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_sep_zip {A B} (h1 : nat → A → M) (h2 : nat → B → M) l1 l2 :
  length l1 = length l2 →
  ([^o list] k↦xy ∈ zip l1 l2, h1 k xy.1 `o` h2 k xy.2) ≡
  ([^o list] k↦x ∈ l1, h1 k x) `o` ([^o list] k↦y ∈ l2, h2 k y).
Proof. by apply big_opL_sep_zip_with. Qed.
(* iris/algebra/big_op.v *)
(* ** Big ops over finite maps *)
Lemma big_opM_empty `{Countable K} {B} (f : K → B → M) :
  ([^o map] k↦x ∈ ∅, f k x) = u.
Proof. by rewrite big_opM_unseal /big_opM_def map_to_list_empty. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_insert `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x :
  m !! i = None →
  ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ m, f k y.
Proof. intros ?. by rewrite big_opM_unseal /big_opM_def map_to_list_insert. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_delete `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x :
  m !! i = Some x →
  ([^o map] k↦y ∈ m, f k y) ≡ f i x `o` [^o map] k↦y ∈ delete i m, f k y.
Proof.
  intros. rewrite -big_opM_insert ?lookup_delete_eq //.
  by rewrite insert_delete_id.
Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_gen_proper_2 {B} (R : relation M) f (g : K → B → M)
        m1 (m2 : gmap K B) :
    subrelation (≡) R → Equivalence R →
    Proper (R ==> R ==> R) o →
    (∀ k,
      match m1 !! k, m2 !! k with
      | Some y1, Some y2 => R (f k y1) (g k y2)
      | None, None => True
      | _, _ => False
      end) →
    R ([^o map] k ↦ x ∈ m1, f k x) ([^o map] k ↦ x ∈ m2, g k x).
Proof.
    intros HR ??. revert m2 f g.
    induction m1 as [|k x1 m1 Hm1k IH] using map_ind=> m2 f g Hfg.
    { destruct m2 as [|k x2 m2 _ _] using map_ind.
      { rewrite !big_opM_empty. by apply HR. }
      generalize (Hfg k). by rewrite lookup_empty lookup_insert_eq. }
    generalize (Hfg k). rewrite lookup_insert_eq.
    destruct (m2 !! k) as [x2|] eqn:Hm2k; [intros Hk|done].
    etrans; [by apply HR, big_opM_insert|].
    etrans; [|by symmetry; apply HR, big_opM_delete].
    f_equiv; [done|]. apply IH=> k'. destruct (decide (k = k')) as [->|?].
    - by rewrite lookup_delete_eq Hm1k.
    - generalize (Hfg k'). rewrite lookup_insert_ne // lookup_delete_ne //.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_gen_proper R f g m :
    Reflexive R →
    Proper (R ==> R ==> R) o →
    (∀ k x, m !! k = Some x → R (f k x) (g k x)) →
    R ([^o map] k ↦ x ∈ m, f k x) ([^o map] k ↦ x ∈ m, g k x).
Proof.
    intros ?? Hf. rewrite big_opM_unseal. apply (big_opL_gen_proper R); auto.
    intros k [i x] ?%list_elem_of_lookup_2. by apply Hf, elem_of_map_to_list.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_ext f g m :
    (∀ k x, m !! k = Some x → f k x = g k x) →
    ([^o map] k ↦ x ∈ m, f k x) = ([^o map] k ↦ x ∈ m, g k x).
Proof. apply big_opM_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
(* The lemmas [big_opM_ne] and [big_opM_proper] are more generic than the
  instances as they also give [m !! k = Some y] in the premise. *)
Lemma big_opM_ne f g m n :
    (∀ k x, m !! k = Some x → f k x ≡{n}≡ g k x) →
    ([^o map] k ↦ x ∈ m, f k x) ≡{n}≡ ([^o map] k ↦ x ∈ m, g k x).
Proof. apply big_opM_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_proper f g m :
    (∀ k x, m !! k = Some x → f k x ≡ g k x) →
    ([^o map] k ↦ x ∈ m, f k x) ≡ ([^o map] k ↦ x ∈ m, g k x).
Proof. apply big_opM_gen_proper; apply _. Qed.
(* iris/algebra/big_op.v *)
(* The version [big_opM_proper_2] with [≡] for the map arguments can only be
  used if there is a setoid on [A]. The version for [dist n] can be found in
  [algebra.gmap]. We do not define this lemma as a [Proper] instance, since
  [f_equiv] will then use sometimes use this one, and other times
  [big_opM_proper'], depending on whether a setoid on [A] exists. *)
Lemma big_opM_proper_2 `{!Equiv A} f g m1 m2 :
    m1 ≡ m2 →
    (∀ k y1 y2,
      m1 !! k = Some y1 → m2 !! k = Some y2 → y1 ≡ y2 → f k y1 ≡ g k y2) →
    ([^o map] k ↦ y ∈ m1, f k y) ≡ ([^o map] k ↦ y ∈ m2, g k y).
Proof.
    intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
    (* FIXME (Coq #14441) unnecessary type annotation *)
    intros k. assert (m1 !! k ≡@{option A} m2 !! k) as Hlk by (by f_equiv).
    destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
  Qed.
(* iris/algebra/big_op.v *)
Instance big_opM_ne' n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (=) ==> dist n)
           (big_opM o (K:=K) (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opM_ne; intros; apply Hf. Qed.
(* iris/algebra/big_op.v *)
Instance big_opM_proper' :
    Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (=) ==> (≡))
           (big_opM o (K:=K) (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opM_proper; intros; apply Hf. Qed.
(* iris/algebra/big_op.v *)
(* FIXME: This lemma could be generalized from [≡] to [=], but that breaks
  [setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opM_map_to_list f m :
    ([^o map] k↦x ∈ m, f k x) ≡ [^o list] xk ∈ map_to_list m, f (xk.1) (xk.2).
Proof. rewrite big_opM_unseal. apply big_opL_proper'; [|done]. by intros ? [??]. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_list_to_map f l :
    NoDup l.*1 →
    ([^o map] k↦x ∈ list_to_map l, f k x) ≡ [^o list] xk ∈ l, f (xk.1) (xk.2).
Proof.
    intros. rewrite big_opM_map_to_list.
    by apply big_opL_permutation, map_to_list_to_map.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_singleton f i x : ([^o map] k↦y ∈ {[i:=x]}, f k y) ≡ f i x.
Proof.
    rewrite -insert_empty big_opM_insert/=; last eauto using lookup_empty.
    by rewrite big_opM_empty right_id.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_unit m : ([^o map] k↦y ∈ m, u) ≡@{M} u.
Proof.
    by induction m using map_ind; rewrite /= ?big_opM_insert ?left_id // big_opM_unseal.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_fmap {B} (h : A → B) (f : K → B → M) m :
    ([^o map] k↦y ∈ h <$> m, f k y) ≡ ([^o map] k↦y ∈ m, f k (h y)).
Proof.
    rewrite big_opM_unseal /big_opM_def map_to_list_fmap big_opL_fmap.
    by apply big_opL_proper=> ? [??].
  Qed.