phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/big_op.v *)
Lemma big_opMS_commute `{Countable A} (h : M1 → M2)
      `{!MonoidHomomorphism o1 o2 R h} (f : A → M1) X :
    R (h ([^o1 mset] x ∈ X, f x)) ([^o2 mset] x ∈ X, h (f x)).
Proof.
    intros. induction X as [|x X IH] using gmultiset_ind.
    - by rewrite !big_opMS_empty monoid_homomorphism_unit.
    - by rewrite !big_opMS_disj_union !big_opMS_singleton monoid_homomorphism -IH.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_commute1 `{Countable A} (h : M1 → M2)
      `{!WeakMonoidHomomorphism o1 o2 R h} (f : A → M1) X :
    X ≠ ∅ → R (h ([^o1 mset] x ∈ X, f x)) ([^o2 mset] x ∈ X, h (f x)).
Proof.
    intros. induction X as [|x X IH] using gmultiset_ind; [done|].
    destruct (decide (X = ∅)) as [->|].
    - by rewrite !big_opMS_disj_union !big_opMS_singleton !big_opMS_empty !right_id.
    - by rewrite !big_opMS_disj_union !big_opMS_singleton monoid_homomorphism -IH //.
  Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_commute_L {A} (h : M1 → M2)
      `{!MonoidHomomorphism o1 o2 (≡) h} (f : nat → A → M1) l :
    h ([^o1 list] k↦x ∈ l, f k x) = ([^o2 list] k↦x ∈ l, h (f k x)).
Proof using Type*. unfold_leibniz. by apply big_opL_commute. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opL_commute1_L {A} (h : M1 → M2)
      `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : nat → A → M1) l :
    l ≠ [] → h ([^o1 list] k↦x ∈ l, f k x) = ([^o2 list] k↦x ∈ l, h (f k x)).
Proof using Type*. unfold_leibniz. by apply big_opL_commute1. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_commute_L `{Countable K} {A} (h : M1 → M2)
      `{!MonoidHomomorphism o1 o2 (≡) h} (f : K → A → M1) m :
    h ([^o1 map] k↦x ∈ m, f k x) = ([^o2 map] k↦x ∈ m, h (f k x)).
Proof using Type*. unfold_leibniz. by apply big_opM_commute. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opM_commute1_L `{Countable K} {A} (h : M1 → M2)
      `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : K → A → M1) m :
    m ≠ ∅ → h ([^o1 map] k↦x ∈ m, f k x) = ([^o2 map] k↦x ∈ m, h (f k x)).
Proof using Type*. unfold_leibniz. by apply big_opM_commute1. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_commute_L `{Countable A} (h : M1 → M2)
      `{!MonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
    h ([^o1 set] x ∈ X, f x) = ([^o2 set] x ∈ X, h (f x)).
Proof using Type*. unfold_leibniz. by apply big_opS_commute. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opS_commute1_L `{ Countable A} (h : M1 → M2)
      `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
    X ≠ ∅ → h ([^o1 set] x ∈ X, f x) = ([^o2 set] x ∈ X, h (f x)).
Proof using Type*. intros. rewrite <-leibniz_equiv_iff. by apply big_opS_commute1. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_commute_L `{Countable A} (h : M1 → M2)
      `{!MonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
    h ([^o1 mset] x ∈ X, f x) = ([^o2 mset] x ∈ X, h (f x)).
Proof using Type*. unfold_leibniz. by apply big_opMS_commute. Qed.
(* iris/algebra/big_op.v *)
Lemma big_opMS_commute1_L `{Countable A} (h : M1 → M2)
      `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
    X ≠ ∅ → h ([^o1 mset] x ∈ X, f x) = ([^o2 mset] x ∈ X, h (f x)).
Proof using Type*. intros. rewrite <-leibniz_equiv_iff. by apply big_opMS_commute1. Qed.
(* iris/algebra/cmra.v *)
Class PCore (A : Type)
:= pcore : A → option A.
(* iris/algebra/cmra.v *)
Instance : Params (@pcore) 2
:= {}.
(* iris/algebra/cmra.v *)
Class Op (A : Type)
:= op : A → A → A.
(* iris/algebra/cmra.v *)
Instance : Params (@op) 2
:= {}.
(* iris/algebra/cmra.v *)
Notation "(⋅)"
:= op (only parsing) : stdpp_scope.
(* iris/algebra/cmra.v *)
(* The inclusion quantifies over [A], not [option A].  This means we do not get
   reflexivity.  However, if we used [option A], the following would no longer
   hold:
     x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2
   If you need the reflexive closure of the inclusion relation, you can use
   [Some a ≼ Some b]. There are various [Some_included] lemmas that help
   deal with propositions of this shape. *)
Definition included {A} `{!Equiv A, !Op A} (x y : A)
:= ∃ z, y ≡ x ⋅ z.
(* iris/algebra/cmra.v *)
Notation "(≼)"
:= included (only parsing) : stdpp_scope.
(* iris/algebra/cmra.v *)
Instance : Params (@included) 3
:= {}.
(* iris/algebra/cmra.v *)
(* [opM] is used in some lemma statements where [A] has not yet been shown to
be a CMRA, so we define it directly in terms of [Op]. *)
Definition opM `{!Op A} (x : A) (my : option A)
:=
  match my with Some y => x ⋅ y | None => x end.
(* iris/algebra/cmra.v *)
Class ValidN {SI : sidx} (A : Type)
:= validN : SI → A → Prop.
(* iris/algebra/cmra.v *)
Instance : Params (@validN) 4
:= {}.
(* iris/algebra/cmra.v *)
Notation "✓{ n } x"
:= (validN n x)
  (at level 20, n at next level, format "✓{ n }  x").
(* iris/algebra/cmra.v *)
Class Valid (A : Type)
:= valid : A → Prop.
(* iris/algebra/cmra.v *)
Instance : Params (@valid) 2
:= {}.
(* iris/algebra/cmra.v *)
Notation "✓ x"
:= (valid x) (at level 20, right associativity) : stdpp_scope.
(* iris/algebra/cmra.v *)
Definition includedN {SI : sidx} `{!Dist A, Op A} (n : SI) (x y : A)
:=
  ∃ z, y ≡{n}≡ x ⋅ z.
(* iris/algebra/cmra.v *)
Notation "x ≼{ n } y"
:= (includedN n x y)
  (at level 70, n at next level, format "x  ≼{ n }  y") : stdpp_scope.
(* iris/algebra/cmra.v *)
Instance : Params (@includedN) 5
:= {}.
(* iris/algebra/cmra.v *)
Record CmraMixin {SI : sidx} A
      `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A}
:= {
    (* setoids *)
    mixin_cmra_op_ne (x : A) : NonExpansive (op x);
    mixin_cmra_pcore_ne n (x y : A) cx :
      x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
    mixin_cmra_validN_ne n : Proper (dist (A := A) n ==> impl) (validN n);
    (* valid *)
    mixin_cmra_valid_validN (x : A) : ✓ x ↔ ∀ n, ✓{n} x;
    mixin_cmra_validN_le n n' (x : A) : ✓{n} x → n' ≤ n → ✓{n'} x;
    (* monoid *)
    mixin_cmra_assoc : Assoc (≡@{A}) (⋅);
    mixin_cmra_comm : Comm (≡@{A}) (⋅);
    mixin_cmra_pcore_l (x : A) cx : pcore x = Some cx → cx ⋅ x ≡ x;
    mixin_cmra_pcore_idemp (x : A) cx : pcore x = Some cx → pcore cx ≡ Some cx;
    mixin_cmra_pcore_mono (x y : A) cx :
      x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
    mixin_cmra_validN_op_l n (x y : A) : ✓{n} (x ⋅ y) → ✓{n} x;
    mixin_cmra_extend n (x y1 y2 : A) :
      ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
      { z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }
  }.
(* iris/algebra/cmra.v *)
(* Bundled version *)
Structure cmra {SI : sidx}
:= Cmra' {
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_dist : Dist cmra_car;
  cmra_pcore : PCore cmra_car;
  cmra_op : Op cmra_car;
  cmra_valid : Valid cmra_car;
  cmra_validN : ValidN cmra_car;
  cmra_ofe_mixin : OfeMixin cmra_car;
  cmra_mixin : CmraMixin cmra_car;
}.
(* iris/algebra/cmra.v *)
(* Given [m : CmraMixin A], the notation [Cmra A m] provides a smart
constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
the type [A], so that it does not have to be given manually. *)
Notation Cmra A m
:= (Cmra' A (ofe_mixin_of A%type) m) (only parsing).
(* iris/algebra/cmra.v *)
Coercion cmra_ofeO {SI : sidx} (A : cmra) : ofe
:= Ofe A (cmra_ofe_mixin A).
(* iris/algebra/cmra.v *)
Canonical cmra_ofeO.
(* iris/algebra/cmra.v *)
Definition cmra_mixin_of' {SI : sidx} A {Ac : cmra}
  (f : Ac → A) : CmraMixin Ac
:= cmra_mixin Ac.
(* iris/algebra/cmra.v *)
Notation cmra_mixin_of A
:=
  ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).
(* iris/algebra/cmra.v *)
Instance cmra_op_ne (x : A) : NonExpansive (op x).
Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_ne n x y cx :
    x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy.
Proof. apply (mixin_cmra_pcore_ne _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN _ A _ n).
Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x.
Proof. apply (mixin_cmra_validN_le _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Instance cmra_assoc : Assoc (≡) (@op A _).
Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Instance cmra_comm : Comm (≡) (@op A _).
Proof. apply (mixin_cmra_comm _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x.
Proof. apply (mixin_cmra_pcore_l _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx.
Proof. apply (mixin_cmra_pcore_idemp _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_mono x y cx :
    x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
Proof. apply (mixin_cmra_pcore_mono _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_extend n x y1 y2 :
    ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
    { z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }.
Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
(* * CoreId elements *)
Class CoreId {SI : sidx} {A : cmra} (x : A)
:= core_id : pcore x ≡ Some x.
(* iris/algebra/cmra.v *)
Instance : Params (@CoreId) 2
:= {}.
(* iris/algebra/cmra.v *)
(* * Exclusive elements (i.e., elements that cannot have a frame). *)
Class Exclusive {SI : sidx} {A : cmra} (x : A)
:=
  exclusive0_l y : ✓{0ᵢ} (x ⋅ y) → False.
(* iris/algebra/cmra.v *)
Instance : Params (@Exclusive) 2
:= {}.
(* iris/algebra/cmra.v *)
(* * Cancelable elements. *)
Class Cancelable {SI : sidx} {A : cmra} (x : A)
:=
  cancelableN n y z : ✓{n} (x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.
(* iris/algebra/cmra.v *)
Instance : Params (@Cancelable) 2
:= {}.
(* iris/algebra/cmra.v *)
(* * Identity-free elements. *)
Class IdFree {SI : sidx} {A : cmra} (x : A)
:=
  id_free0_r y : ✓{0ᵢ} x → x ⋅ y ≡{0ᵢ}≡ x → False.
(* iris/algebra/cmra.v *)
Instance : Params (@IdFree) 2
:= {}.
(* iris/algebra/cmra.v *)
(* * CMRAs whose core is total *)
Class CmraTotal {SI : sidx} (A : cmra)
:=
  cmra_total (x : A) : is_Some (pcore x).
(* iris/algebra/cmra.v *)
(* The function [core] returns a dummy when used on CMRAs without total
core. We only ever use this for [CmraTotal] CMRAs, but it is more convenient
to not require that proof to be able to call this function. *)
Definition core {A} `{!PCore A} (x : A) : A
:= default x (pcore x).
(* iris/algebra/cmra.v *)
Instance : Params (@core) 2
:= {}.
(* iris/algebra/cmra.v *)
(* * CMRAs with a unit element *)
Class Unit (A : Type)
:= ε : A.
(* iris/algebra/cmra.v *)
Record UcmraMixin {SI : sidx} A
    `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !Unit A}
:= {
  mixin_ucmra_unit_valid : ✓ (ε : A);
  mixin_ucmra_unit_left_id : LeftId (≡@{A}) ε (⋅);
  mixin_ucmra_pcore_unit : pcore ε ≡@{option A} Some ε
}.
(* iris/algebra/cmra.v *)
Structure ucmra {SI : sidx}
:= Ucmra' {
  ucmra_car :> Type;
  ucmra_equiv : Equiv ucmra_car;
  ucmra_dist : Dist ucmra_car;
  ucmra_pcore : PCore ucmra_car;
  ucmra_op : Op ucmra_car;
  ucmra_valid : Valid ucmra_car;
  ucmra_validN : ValidN ucmra_car;
  ucmra_unit : Unit ucmra_car;
  ucmra_ofe_mixin : OfeMixin ucmra_car;
  ucmra_cmra_mixin : CmraMixin ucmra_car;
  ucmra_mixin : UcmraMixin ucmra_car;
}.
(* iris/algebra/cmra.v *)
Notation Ucmra A m
:=
  (Ucmra' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
(* iris/algebra/cmra.v *)
Coercion ucmra_ofeO {SI : sidx} (A : ucmra) : ofe
:= Ofe A (ucmra_ofe_mixin A).
(* iris/algebra/cmra.v *)
Canonical ucmra_ofeO.
(* iris/algebra/cmra.v *)
Coercion ucmra_cmraR {SI : sidx} (A : ucmra) : cmra
:=
  Cmra' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
(* iris/algebra/cmra.v *)
Canonical ucmra_cmraR.
(* iris/algebra/cmra.v *)
Lemma ucmra_unit_valid : ✓ (ε : A).
Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Instance ucmra_unit_left_id : LeftId (≡) ε (@op A _).
Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
Lemma ucmra_pcore_unit : pcore (ε:A) ≡ Some ε.
Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
(* iris/algebra/cmra.v *)
(* * Discrete CMRAs *)
Class CmraDiscrete {SI : sidx} (A : cmra)
:= {
  #[global] cmra_discrete_ofe_discrete :: OfeDiscrete A;
  cmra_discrete_valid (x : A) : ✓{0ᵢ} x → ✓ x
}.
(* iris/algebra/cmra.v *)
(* * Morphisms *)
Class CmraMorphism {SI : sidx} {A B : cmra} (f : A → B)
:= {
  #[global] cmra_morphism_ne :: NonExpansive f;
  cmra_morphism_validN n x : ✓{n} x → ✓{n} f x;
  cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
  cmra_morphism_op x y : f (x ⋅ y) ≡ f x ⋅ f y
}.
(* iris/algebra/cmra.v *)
(* ** Setoids *)
Instance cmra_pcore_ne' : NonExpansive (@pcore A _).
Proof.
  intros n x y Hxy. destruct (pcore x) as [cx|] eqn:?.
  { destruct (cmra_pcore_ne n x y cx) as (cy&->&->); auto. }
  destruct (pcore y) as [cy|] eqn:?; auto.
  destruct (cmra_pcore_ne n y x cy) as (cx&?&->); simplify_eq/=; auto.
Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_proper x y cx :
  x ≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡ cy.
Proof.
  intros. destruct (cmra_pcore_ne 0ᵢ x y cx) as (cy&?&?); auto.
  exists cy; split; [done|apply equiv_dist=> n].
  destruct (cmra_pcore_ne n x y cx) as (cy'&?&?); naive_solver.
Qed.
(* iris/algebra/cmra.v *)
Instance cmra_pcore_proper' : Proper ((≡) ==> (≡)) (@pcore A _).
Proof. apply (ne_proper _). Qed.
(* iris/algebra/cmra.v *)
Instance cmra_op_ne' : NonExpansive2 (@op A _).
Proof. intros n x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
(* iris/algebra/cmra.v *)
Instance cmra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
Proof. apply (ne_proper_2 _). Qed.
(* iris/algebra/cmra.v *)
Instance cmra_validN_ne' n : Proper (dist n ==> iff) (@validN SI A _ n) | 1.
Proof. by split; apply cmra_validN_ne. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_validN_proper n : Proper ((≡) ==> iff) (@validN SI A _ n) | 1.
Proof. by intros x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_valid_proper : Proper ((≡) ==> iff) (@valid A _).
Proof.
  intros x y Hxy; rewrite !cmra_valid_validN.
  by split=> ? n; [rewrite -Hxy|rewrite Hxy].
Qed.
(* iris/algebra/cmra.v *)
Instance cmra_includedN_ne n :
  Proper (dist n ==> dist n ==> iff) (@includedN SI A _ _ n) | 1.
Proof.
  intros x x' Hx y y' Hy.
  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
(* iris/algebra/cmra.v *)
Instance cmra_includedN_proper n :
  Proper ((≡) ==> (≡) ==> iff) (@includedN SI A _ _ n) | 1.
Proof.
  intros x x' Hx y y' Hy; revert Hx Hy; rewrite !equiv_dist=> Hx Hy.
  by rewrite (Hx n) (Hy n).
Qed.
(* iris/algebra/cmra.v *)
Instance cmra_included_proper :
  Proper ((≡) ==> (≡) ==> iff) (@included A _ _) | 1.
Proof.
  intros x x' Hx y y' Hy.
  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
(* iris/algebra/cmra.v *)
Instance cmra_opM_ne : NonExpansive2 (@opM A _).
Proof. destruct 2; by ofe_subst. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_opM_proper : Proper ((≡) ==> (≡) ==> (≡)) (@opM A _).
Proof. destruct 2; by setoid_subst. Qed.
(* iris/algebra/cmra.v *)
Instance CoreId_proper : Proper ((≡) ==> iff) (@CoreId SI A).
Proof. solve_proper. Qed.
(* iris/algebra/cmra.v *)
Instance Exclusive_proper : Proper ((≡) ==> iff) (@Exclusive SI A).
Proof. intros x y Hxy. rewrite /Exclusive. by setoid_rewrite Hxy. Qed.
(* iris/algebra/cmra.v *)
Instance Cancelable_proper : Proper ((≡) ==> iff) (@Cancelable SI A).
Proof. intros x y Hxy. rewrite /Cancelable. by setoid_rewrite Hxy. Qed.
(* iris/algebra/cmra.v *)
Instance IdFree_proper : Proper ((≡) ==> iff) (@IdFree SI A).
Proof. intros x y Hxy. rewrite /IdFree. by setoid_rewrite Hxy. Qed.
(* iris/algebra/cmra.v *)
(* ** Op *)
Lemma cmra_op_opM_assoc x y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz).
Proof. destruct mz; by rewrite /= -?assoc. Qed.
(* iris/algebra/cmra.v *)
(* ** Validity *)
Lemma cmra_validN_lt n n' x : ✓{n} x → n' < n → ✓{n'} x.
Proof. eauto using cmra_validN_le, SIdx.lt_le_incl. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_validN_op_r n x y : ✓{n} (x ⋅ y) → ✓{n} y.
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.
(* iris/algebra/cmra.v *)
(* ** Core *)
Lemma cmra_pcore_l' x cx : pcore x ≡ Some cx → cx ⋅ x ≡ x.
Proof. intros (cx'&?&<-)%Some_equiv_eq. by apply cmra_pcore_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_r x cx : pcore x = Some cx → x ⋅ cx ≡ x.
Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_r' x cx : pcore x ≡ Some cx → x ⋅ cx ≡ x.
Proof. intros (cx'&?&<-)%Some_equiv_eq. by apply cmra_pcore_r. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_idemp' x cx : pcore x ≡ Some cx → pcore cx ≡ Some cx.
Proof. intros (cx'&?&<-)%Some_equiv_eq. eauto using cmra_pcore_idemp. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_dup x cx : pcore x = Some cx → cx ≡ cx ⋅ cx.
Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_dup' x cx : pcore x ≡ Some cx → cx ≡ cx ⋅ cx.
Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp'. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_validN n x cx : ✓{n} x → pcore x = Some cx → ✓{n} cx.
Proof.
  intros Hvx Hx%cmra_pcore_l. move: Hvx; rewrite -Hx. apply cmra_validN_op_l.
Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_valid x cx : ✓ x → pcore x = Some cx → ✓ cx.
Proof.
  intros Hv Hx%cmra_pcore_l. move: Hv; rewrite -Hx. apply cmra_valid_op_l.
Qed.
(* iris/algebra/cmra.v *)
(* ** Exclusive elements *)
Lemma exclusiveN_l n x `{!Exclusive x} y : ✓{n} (x ⋅ y) → False.
Proof. intros. by eapply (exclusive0_l x y), cmra_validN_le, SIdx.le_0_l. Qed.
(* iris/algebra/cmra.v *)
Lemma exclusiveN_r n x `{!Exclusive x} y : ✓{n} (y ⋅ x) → False.
Proof. rewrite comm. by apply exclusiveN_l. Qed.
(* iris/algebra/cmra.v *)
Lemma exclusive_l x `{!Exclusive x} y : ✓ (x ⋅ y) → False.
Proof. by move /cmra_valid_validN /(_ 0ᵢ) /exclusive0_l. Qed.
(* iris/algebra/cmra.v *)
Lemma exclusive_r x `{!Exclusive x} y : ✓ (y ⋅ x) → False.
Proof. rewrite comm. by apply exclusive_l. Qed.
(* iris/algebra/cmra.v *)
Lemma exclusiveN_opM n x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None.
Proof. destruct my as [y|]; last done. move=> /(exclusiveN_l _ x) []. Qed.
(* iris/algebra/cmra.v *)
Lemma exclusive_includedN n x `{!Exclusive x} y : x ≼{n} y → ✓{n} y → False.
Proof. intros [? ->]. by apply exclusiveN_l. Qed.
(* iris/algebra/cmra.v *)
Lemma exclusive_included x `{!Exclusive x} y : x ≼ y → ✓ y → False.
Proof. intros [? ->]. by apply exclusive_l. Qed.
(* iris/algebra/cmra.v *)
(* ** Order *)
Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.
Proof. intros [z ->]. by exists z. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_includedN_trans n : Transitive (@includedN SI A _ _ n).
Proof.
  intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). by rewrite assoc -Hy -Hz.
Qed.
(* iris/algebra/cmra.v *)
Instance cmra_included_trans: Transitive (@included A _ _).
Proof.
  intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). by rewrite assoc -Hy -Hz.
Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_valid_included x y : ✓ y → x ≼ y → ✓ x.
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_valid_op_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_validN_includedN n x y : ✓{n} y → x ≼{n} y → ✓{n} x.
Proof. intros Hyv [z ?]; ofe_subst y; eauto using cmra_validN_op_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_validN_included n x y : ✓{n} y → x ≼ y → ✓{n} x.
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_includedN_le n m x y : x ≼{n} y → m ≤ n → x ≼{m} y.
Proof. by intros [z Hz] H; exists z; eapply dist_le. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_includedN_S n x y : x ≼{Sᵢ n} y → x ≼{n} y.
Proof. intros ?. by eapply cmra_includedN_le, SIdx.le_succ_diag_r. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_includedN_l n x y : x ≼{n} x ⋅ y.
Proof. by exists y. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_included_l x y : x ≼ x ⋅ y.
Proof. by exists y. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_includedN_r n x y : y ≼{n} x ⋅ y.
Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_included_r x y : y ≼ x ⋅ y.
Proof. rewrite (comm op); apply cmra_included_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_mono' x y cx :
  x ≼ y → pcore x ≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
Proof.
  intros ? (cx'&?&Hcx)%Some_equiv_eq.
  destruct (cmra_pcore_mono x y cx') as (cy&->&?); auto.
  exists cy; by rewrite -Hcx.
Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_monoN' n x y cx :
  x ≼{n} y → pcore x ≡{n}≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼{n} cy.
Proof.
  intros [z Hy] (cx'&?&Hcx)%dist_Some_inv_r'.
  destruct (cmra_pcore_mono x (x ⋅ z) cx')
    as (cy&Hxy&?); auto using cmra_included_l.
  assert (pcore y ≡{n}≡ Some cy) as (cy'&?&Hcy')%dist_Some_inv_r'.
  { by rewrite Hy Hxy. }
  exists cy'; split; first done.
  rewrite Hcx -Hcy'; auto using cmra_included_includedN.
Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_included_pcore x cx : pcore x = Some cx → cx ≼ x.
Proof. exists x. by rewrite cmra_pcore_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_monoN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_mono_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_monoN_r n x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z.
Proof. by intros; rewrite -!(comm _ z); apply cmra_monoN_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_mono_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
Proof. by intros; rewrite -!(comm _ z); apply cmra_mono_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_monoN n x1 x2 y1 y2 : x1 ≼{n} y1 → x2 ≼{n} y2 → x1 ⋅ x2 ≼{n} y1 ⋅ y2.
Proof. intros; etrans; eauto using cmra_monoN_l, cmra_monoN_r. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_mono x1 x2 y1 y2 : x1 ≼ y1 → x2 ≼ y2 → x1 ⋅ x2 ≼ y1 ⋅ y2.
Proof. intros; etrans; eauto using cmra_mono_l, cmra_mono_r. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_monoN' n :
  Proper (includedN n ==> includedN n ==> includedN n) (@op A _).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_monoN. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_mono' :
  Proper (included ==> included ==> included) (@op A _).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_mono. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_included_dist_l n x1 x2 x1' :
  x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2.
Proof.
  intros [z Hx2] Hx1; exists (x1' ⋅ z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Qed.
(* iris/algebra/cmra.v *)
(* ** CoreId elements *)
Lemma core_id_dup x `{!CoreId x} : x ≡ x ⋅ x.
Proof. by apply cmra_pcore_dup' with x. Qed.
(* iris/algebra/cmra.v *)
Lemma core_id_extract x y `{!CoreId x} :
  x ≼ y → y ≡ y ⋅ x.
Proof.
  intros ?.
  destruct (cmra_pcore_mono' x y x) as (cy & Hcy & [x' Hx']); [done|exact: core_id|].
  rewrite -(cmra_pcore_r y) //. rewrite Hx' -!assoc. f_equiv.
  rewrite [x' ⋅ x]comm assoc -core_id_dup. done.
Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_core x : pcore x = Some (core x).
Proof.
    rewrite /core. destruct (cmra_total x) as [cx ->]. done.
  Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_l x : core x ⋅ x ≡ x.
Proof.
    destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_l.
  Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_idemp x : core (core x) ≡ core x.
Proof.
    destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_idemp.
  Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_mono x y : x ≼ y → core x ≼ core y.
Proof.
    intros; destruct (cmra_total x) as [cx Hcx].
    destruct (cmra_pcore_mono x y cx) as (cy&Hcy&?); auto.
    by rewrite /core /= Hcx Hcy.
  Qed.
(* iris/algebra/cmra.v *)
Instance cmra_core_ne : NonExpansive (@core A _).
Proof.
    intros n x y Hxy. destruct (cmra_total x) as [cx Hcx].
    by rewrite /core /= -Hxy Hcx.
  Qed.