phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/mra.v *)
Lemma to_mra_rel_inj :
    Reflexive R →
    AntiSymm S R →
    Inj S (≡@{mra R}) (to_mra).
Proof.
    intros ?? a b Hab. move: (Hab a) (Hab b). rewrite !mra_below_to_mra.
    intros. apply (anti_symm R); naive_solver.
  Qed.
(* iris/algebra/mra.v *)
Instance to_mra_inj {SI : sidx} {A} {R : relation A} :
  Reflexive R →
  AntiSymm (=) R →
  Inj (=) (≡@{mra R}) (to_mra) | 0.
(* Lower cost than [to_mra_equiv_inj] *)
Proof. intros. by apply (to_mra_rel_inj (=)). Qed.
(* iris/algebra/mra.v *)
Instance to_mra_proper {SI : sidx} `{Equiv A} {R : relation A} :
  Reflexive (≡@{A}) →
  Proper ((≡) ==> (≡) ==> iff) R →
  Proper ((≡) ==> (≡@{mra R})) (to_mra).
Proof. intros. by apply (to_mra_rel_proper (≡)). Qed.
(* iris/algebra/mra.v *)
Instance to_mra_equiv_inj {SI : sidx} `{Equiv A} {R : relation A} :
  Reflexive R →
  AntiSymm (≡) R →
  Inj (≡) (≡@{mra R}) (to_mra) | 1.
Proof. intros. by apply (to_mra_rel_inj (≡)). Qed.
(* iris/algebra/numbers.v *)
Instance nat_valid_instance : Valid nat
:= λ x, True.
(* iris/algebra/numbers.v *)
Instance nat_validN_instance : ValidN nat
:= λ n x, True.
(* iris/algebra/numbers.v *)
Instance nat_pcore_instance : PCore nat
:= λ x, Some 0.
(* iris/algebra/numbers.v *)
Instance nat_op_instance : Op nat
:= plus.
(* iris/algebra/numbers.v *)
Definition nat_op x y : x ⋅ y = x + y
:= eq_refl.
(* iris/algebra/numbers.v *)
Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
Proof. by rewrite Nat.le_sum. Qed.
(* iris/algebra/numbers.v *)
Lemma nat_ra_mixin : RAMixin nat.
Proof.
    apply ra_total_mixin; try by eauto.
    - solve_proper.
    - intros x y z. apply Nat.add_assoc.
    - intros x y. apply Nat.add_comm.
    - by exists 0.
  Qed.
(* iris/algebra/numbers.v *)
Canonical natR : cmra
:= discreteR nat nat_ra_mixin.
(* iris/algebra/numbers.v *)
Instance nat_cmra_discrete : CmraDiscrete natR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/numbers.v *)
Instance nat_unit_instance : Unit nat
:= 0.
(* iris/algebra/numbers.v *)
Lemma nat_ucmra_mixin : UcmraMixin nat.
Proof. split; apply _ || done. Qed.
(* iris/algebra/numbers.v *)
Canonical natUR : ucmra
:= Ucmra nat nat_ucmra_mixin.
(* iris/algebra/numbers.v *)
Instance nat_cancelable (x : nat) : Cancelable x.
Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
(* iris/algebra/numbers.v *)
Lemma nat_local_update (x y x' y' : nat) :
    (** Morally [x - y = x' - y']: the difference between auth and frag must
    stay the same with this update. Written using [+] due to underflow. *)
    x + y' = x' + y → (x,y) ~l~> (x',y').
Proof.
    intros ??; apply local_update_unital_discrete=> z _.
    compute -[minus plus]; lia.
  Qed.
(* iris/algebra/numbers.v *)
(* This one has a higher precendence than [is_op_op] so we get a [+] instead
     of an [⋅]. *)
Instance nat_is_op (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
Proof. done. Qed.
(* iris/algebra/numbers.v *)
(* ** Natural numbers with [max] as the operation. *)
Record max_nat
:= MaxNat { max_nat_car : nat }.
(* iris/algebra/numbers.v *)
Canonical max_natO {SI : sidx}
:= leibnizO max_nat.
(* iris/algebra/numbers.v *)
Instance max_nat_unit_instance : Unit max_nat
:= MaxNat 0.
(* iris/algebra/numbers.v *)
Instance max_nat_valid_instance : Valid max_nat
:= λ x, True.
(* iris/algebra/numbers.v *)
Instance max_nat_validN_instance : ValidN max_nat
:= λ n x, True.
(* iris/algebra/numbers.v *)
Instance max_nat_pcore_instance : PCore max_nat
:= Some.
(* iris/algebra/numbers.v *)
Instance max_nat_op_instance : Op max_nat
:= λ n m, MaxNat (max_nat_car n `max` max_nat_car m).
(* iris/algebra/numbers.v *)
Definition max_nat_op x y : MaxNat x ⋅ MaxNat y = MaxNat (x `max` y)
:= eq_refl.
(* iris/algebra/numbers.v *)
Lemma max_nat_included x y : x ≼ y ↔ max_nat_car x ≤ max_nat_car y.
Proof.
    split.
    - intros [z ->]. simpl. lia.
    - exists y. rewrite /op /max_nat_op_instance. rewrite Nat.max_r; last lia. by destruct y.
  Qed.
(* iris/algebra/numbers.v *)
Lemma max_nat_ra_mixin : RAMixin max_nat.
Proof.
    apply ra_total_mixin; apply _ || eauto.
    - intros [x] [y] [z]. repeat rewrite max_nat_op. by rewrite Nat.max_assoc.
    - intros [x] [y]. by rewrite max_nat_op Nat.max_comm.
    - intros [x]. by rewrite max_nat_op Nat.max_id.
  Qed.
(* iris/algebra/numbers.v *)
Canonical max_natR : cmra
:= discreteR max_nat max_nat_ra_mixin.
(* iris/algebra/numbers.v *)
Instance max_nat_cmra_discrete : CmraDiscrete max_natR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/numbers.v *)
Lemma max_nat_ucmra_mixin : UcmraMixin max_nat.
Proof. split; try apply _ || done. intros [x]. done. Qed.
(* iris/algebra/numbers.v *)
Canonical max_natUR : ucmra
:= Ucmra max_nat max_nat_ucmra_mixin.
(* iris/algebra/numbers.v *)
Instance max_nat_core_id (x : max_nat) : CoreId x.
Proof. by constructor. Qed.
(* iris/algebra/numbers.v *)
Lemma max_nat_local_update (x y x' : max_nat) :
    max_nat_car x ≤ max_nat_car x' → (x,y) ~l~> (x',x').
Proof.
    move: x y x' => [x] [y] [y'] /= ?.
    rewrite local_update_unital_discrete=> [[z]] _.
    rewrite 2!max_nat_op. intros [= ?].
    split; first done. apply f_equal. lia.
  Qed.
(* iris/algebra/numbers.v *)
Instance : IdemP (=@{max_nat}) (⋅).
Proof. intros [x]. rewrite max_nat_op. apply f_equal. lia. Qed.
(* iris/algebra/numbers.v *)
Instance max_nat_is_op (x y : nat) :
    IsOp (MaxNat (x `max` y)) (MaxNat x) (MaxNat y).
Proof. done. Qed.
(* iris/algebra/numbers.v *)
(* ** Natural numbers with [min] as the operation. *)
Record min_nat
:= MinNat { min_nat_car : nat }.
(* iris/algebra/numbers.v *)
Canonical min_natO {SI : sidx}
:= leibnizO min_nat.
(* iris/algebra/numbers.v *)
Instance min_nat_valid_instance : Valid min_nat
:= λ x, True.
(* iris/algebra/numbers.v *)
Instance min_nat_validN_instance : ValidN min_nat
:= λ n x, True.
(* iris/algebra/numbers.v *)
Instance min_nat_pcore_instance : PCore min_nat
:= Some.
(* iris/algebra/numbers.v *)
Instance min_nat_op_instance : Op min_nat
:= λ n m, MinNat (min_nat_car n `min` min_nat_car m).
(* iris/algebra/numbers.v *)
Definition min_nat_op_min x y : MinNat x ⋅ MinNat y = MinNat (x `min` y)
:= eq_refl.
(* iris/algebra/numbers.v *)
Lemma min_nat_included (x y : min_nat) : x ≼ y ↔ min_nat_car y ≤ min_nat_car x.
Proof.
    split.
    - intros [z ->]. simpl. lia.
    - exists y. rewrite /op /min_nat_op_instance. rewrite Nat.min_r; last lia. by destruct y.
  Qed.
(* iris/algebra/numbers.v *)
Lemma min_nat_ra_mixin : RAMixin min_nat.
Proof.
    apply ra_total_mixin; apply _ || eauto.
    - intros [x] [y] [z]. repeat rewrite min_nat_op_min. by rewrite Nat.min_assoc.
    - intros [x] [y]. by rewrite min_nat_op_min Nat.min_comm.
    - intros [x]. by rewrite min_nat_op_min Nat.min_id.
  Qed.
(* iris/algebra/numbers.v *)
Canonical min_natR : cmra
:= discreteR min_nat min_nat_ra_mixin.
(* iris/algebra/numbers.v *)
Instance min_nat_cmra_discrete : CmraDiscrete min_natR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/numbers.v *)
Instance min_nat_core_id (x : min_nat) : CoreId x.
Proof. by constructor. Qed.
(* iris/algebra/numbers.v *)
Lemma min_nat_local_update (x y x' : min_nat) :
    min_nat_car x' ≤ min_nat_car x → (x,y) ~l~> (x',x').
Proof.
    move: x y x' => [x] [y] [x'] /= ?.
    rewrite local_update_discrete. move=> [[z]|] _ /=; last done.
    rewrite 2!min_nat_op_min. intros [= ?].
    split; first done. apply f_equal. lia.
  Qed.
(* iris/algebra/numbers.v *)
Instance : LeftAbsorb (=) (MinNat 0) (⋅).
Proof. done. Qed.
(* iris/algebra/numbers.v *)
Instance : RightAbsorb (=) (MinNat 0) (⋅).
Proof. intros [x]. by rewrite min_nat_op_min Nat.min_0_r. Qed.
(* iris/algebra/numbers.v *)
Instance : IdemP (=@{min_nat}) (⋅).
Proof. intros [x]. rewrite min_nat_op_min. apply f_equal. lia. Qed.
(* iris/algebra/numbers.v *)
Instance min_nat_is_op (x y : nat) :
    IsOp (MinNat (x `min` y)) (MinNat x) (MinNat y).
Proof. done. Qed.
(* iris/algebra/numbers.v *)
Instance pos_valid_instance : Valid positive
:= λ x, True.
(* iris/algebra/numbers.v *)
Instance pos_validN_instance : ValidN positive
:= λ n x, True.
(* iris/algebra/numbers.v *)
Instance pos_pcore_instance : PCore positive
:= λ x, None.
(* iris/algebra/numbers.v *)
Instance pos_op_instance : Op positive
:= Pos.add.
(* iris/algebra/numbers.v *)
Definition pos_op_add x y : x ⋅ y = (x + y)%positive
:= eq_refl.
(* iris/algebra/numbers.v *)
Lemma pos_included (x y : positive) : x ≼ y ↔ (x < y)%positive.
Proof. by rewrite Pos.lt_sum. Qed.
(* iris/algebra/numbers.v *)
Lemma pos_ra_mixin : RAMixin positive.
Proof.
    split; try by eauto.
    - by intros ??? ->.
    - intros ???. apply Pos.add_assoc.
    - intros ??. apply Pos.add_comm.
  Qed.
(* iris/algebra/numbers.v *)
Canonical positiveR : cmra
:= discreteR positive pos_ra_mixin.
(* iris/algebra/numbers.v *)
Instance pos_cmra_discrete : CmraDiscrete positiveR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/numbers.v *)
Instance pos_cancelable (x : positive) : Cancelable x.
Proof. intros n y z ??. by eapply Pos.add_reg_l, leibniz_equiv. Qed.
(* iris/algebra/numbers.v *)
Instance pos_id_free (x : positive) : IdFree x.
Proof.
    intros y ??. apply (Pos.add_no_neutral x y). rewrite Pos.add_comm.
    by apply leibniz_equiv.
  Qed.
(* iris/algebra/numbers.v *)
(* This one has a higher precendence than [is_op_op] so we get a [+] instead
     of an [⋅]. *)
Instance pos_is_op (x y : positive) : IsOp (x + y)%positive x y.
Proof. done. Qed.
(* iris/algebra/numbers.v *)
Instance Z_valid_instance : Valid Z
:= λ x, True.
(* iris/algebra/numbers.v *)
Instance Z_validN_instance : ValidN Z
:= λ n x, True.
(* iris/algebra/numbers.v *)
Instance Z_pcore_instance : PCore Z
:= λ x, Some 0.
(* iris/algebra/numbers.v *)
Instance Z_op_instance : Op Z
:= Z.add.
(* iris/algebra/numbers.v *)
Definition Z_op x y : x ⋅ y = x + y
:= eq_refl.
(* iris/algebra/numbers.v *)
Lemma Z_ra_mixin : RAMixin Z.
Proof.
    apply ra_total_mixin; try by eauto.
    - solve_proper.
    - intros x y z. apply Z.add_assoc.
    - intros x y. apply Z.add_comm.
    - by exists 0.
  Qed.
(* iris/algebra/numbers.v *)
Canonical ZR : cmra
:= discreteR Z Z_ra_mixin.
(* iris/algebra/numbers.v *)
Instance Z_cmra_discrete : CmraDiscrete ZR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/numbers.v *)
Instance Z_unit_instance : Unit Z
:= 0.
(* iris/algebra/numbers.v *)
Lemma Z_ucmra_mixin : UcmraMixin Z.
Proof. split; apply _ || done. Qed.
(* iris/algebra/numbers.v *)
Canonical ZUR : ucmra
:= Ucmra Z Z_ucmra_mixin.
(* iris/algebra/numbers.v *)
Instance Z_cancelable (x : Z) : Cancelable x.
Proof. by intros ???? ?%Z.add_cancel_l. Qed.
(* iris/algebra/numbers.v *)
(* The difference between auth and frag must stay the same with this update. *)
Lemma Z_local_update (x y x' y' : Z) :
    x - y = x' - y' → (x,y) ~l~> (x',y').
Proof.
    intros. rewrite local_update_unital_discrete=> z _.
    compute -[Z.sub Z.add]; lia.
  Qed.
(* iris/algebra/numbers.v *)
(* This one has a higher precendence than [is_op_op] so we get a [+] instead
     of an [⋅]. *)
Instance Z_is_op (n1 n2 : Z) : IsOp (n1 + n2) n1 n2.
Proof. done. Qed.
(* iris/algebra/numbers.v *)
(* ** Integers (positive and negative) with [Z.max] as the operation. *)
Record max_Z
:= MaxZ { max_Z_car : Z }.
(* iris/algebra/numbers.v *)
Canonical max_ZO {SI : sidx}
:= leibnizO max_Z.
(* iris/algebra/numbers.v *)
Instance max_Z_unit_instance : Unit max_Z
:= MaxZ 0.
(* iris/algebra/numbers.v *)
Instance max_Z_valid_instance : Valid max_Z
:= λ x, True.
(* iris/algebra/numbers.v *)
Instance max_Z_validN_instance : ValidN max_Z
:= λ n x, True.
(* iris/algebra/numbers.v *)
Instance max_Z_pcore_instance : PCore max_Z
:= Some.
(* iris/algebra/numbers.v *)
Instance max_Z_op_instance : Op max_Z
:= λ n m,
    MaxZ (max_Z_car n `max` max_Z_car m).
(* iris/algebra/numbers.v *)
Definition max_Z_op x y : MaxZ x ⋅ MaxZ y = MaxZ (x `max` y)
:= eq_refl.
(* iris/algebra/numbers.v *)
Lemma max_Z_included x y : x ≼ y ↔ max_Z_car x ≤ max_Z_car y.
Proof.
    split.
    - intros [z ->]. simpl. lia.
    - exists y. rewrite /op /max_Z_op_instance. rewrite Z.max_r; last lia.
      by destruct y.
  Qed.
(* iris/algebra/numbers.v *)
Lemma max_Z_ra_mixin : RAMixin max_Z.
Proof.
    apply ra_total_mixin; apply _ || eauto.
    - intros [x] [y] [z]. repeat rewrite max_Z_op. by rewrite Z.max_assoc.
    - intros [x] [y]. by rewrite max_Z_op Z.max_comm.
    - intros [x]. by rewrite max_Z_op Z.max_id.
  Qed.
(* iris/algebra/numbers.v *)
Canonical max_ZR : cmra
:= discreteR max_Z max_Z_ra_mixin.
(* iris/algebra/numbers.v *)
Instance max_Z_cmra_total : CmraTotal max_ZR.
Proof. intros x. eauto. Qed.
(* iris/algebra/numbers.v *)
Instance max_Z_cmra_discrete : CmraDiscrete max_ZR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/numbers.v *)
Instance max_Z_core_id (x : max_Z) : CoreId x.
Proof. by constructor. Qed.
(* iris/algebra/numbers.v *)
Lemma max_Z_local_update (x y x' : max_Z) :
    max_Z_car x ≤ max_Z_car x' → (x,y) ~l~> (x',x').
Proof.
    move: x y x' => [x] [y] [y'] /= ?.
    rewrite local_update_discrete=> [[[z]|]] //= _ [?].
    split; first done. rewrite max_Z_op. f_equal. lia.
  Qed.
(* iris/algebra/numbers.v *)
Instance : IdemP (=@{max_Z}) (⋅).
Proof. intros [x]. rewrite max_Z_op. apply f_equal. lia. Qed.
(* iris/algebra/numbers.v *)
Instance max_Z_is_op (x y : nat) :
    IsOp (MaxZ (x `max` y)) (MaxZ x) (MaxZ y).
Proof. done. Qed.
(* iris/algebra/ofe.v *)
(* Unbundled version *)
Class Dist {SI : sidx} A
:= dist : SI → relation A.
(* iris/algebra/ofe.v *)
Instance : Params (@dist) 4
:= {}.
(* iris/algebra/ofe.v *)
Notation "x ≡{ n }≡ y"
:= (dist n x y)
  (at level 70, n at next level, format "x  ≡{ n }≡  y").
(* iris/algebra/ofe.v *)
Notation "x ≡{ n }@{ A }≡ y"
:= (dist (A:=A) n x y)
  (at level 70, n at next level, only parsing).
(* iris/algebra/ofe.v *)
Notation "(≡{ n }≡)"
:= (dist n) (only parsing).
(* iris/algebra/ofe.v *)
Notation "(≡{ n }@{ A }≡)"
:= (dist (A:=A) n) (only parsing).
(* iris/algebra/ofe.v *)
Notation "( x ≡{ n }≡.)"
:= (dist n x) (only parsing).
(* iris/algebra/ofe.v *)
Notation "(.≡{ n }≡ y )"
:= (λ x, x ≡{n}≡ y) (only parsing).
(* iris/algebra/ofe.v *)
Notation NonExpansive f
:= (∀ n, Proper (dist n ==> dist n) f).
(* iris/algebra/ofe.v *)
Notation NonExpansive2 f
:= (∀ n, Proper (dist n ==> dist n ==> dist n) f).
(* iris/algebra/ofe.v *)
Notation NonExpansive3 f
:=
  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) f).
(* iris/algebra/ofe.v *)
Notation NonExpansive4 f
:=
  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) f).
(* iris/algebra/ofe.v *)
Record OfeMixin {SI : sidx} A `{Equiv A, !Dist A}
:= {
  mixin_equiv_dist (x y : A) : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
  mixin_dist_equivalence n : Equivalence (@dist SI A _ n);
  mixin_dist_le n m (x y : A) : x ≡{n}≡ y → m ≤ n → x ≡{m}≡ y
}.
(* iris/algebra/ofe.v *)
(* Bundled version *)
Structure ofe {SI : sidx}
:= Ofe {
  ofe_car :> Type;
  ofe_equiv : Equiv ofe_car;
  ofe_dist : Dist ofe_car;
  ofe_mixin : OfeMixin ofe_car
}.
(* iris/algebra/ofe.v *)
(* When declaring instances of subclasses of OFE (like CMRAs and unital CMRAs)
we need Coq to *infer* the canonical OFE instance of a given type and take the
mixin out of it. This makes sure we do not use two different OFE instances in
different places (see for example the constructors [Cmra] and [Ucmra] in the
file [cmra.v].)

In order to infer the OFE instance, we use the definition [ofe_mixin_of'] which
is inspired by the [clone] trick in ssreflect. It works as follows, when type
checking [@ofe_mixin_of' A ?Ac id] Coq faces a unification problem:

  ofe_car ?Ac  ~  A

which will resolve [?Ac] to the canonical OFE instance corresponding to [A]. The
definition [@ofe_mixin_of' A ?Ac id] will then provide the corresponding mixin.
Note that type checking of [ofe_mixin_of' A id] will fail when [A] does not have
a canonical OFE instance.

The notation [ofe_mixin_of A] that we define on top of [ofe_mixin_of' A id]
hides the [id] and normalizes the mixin to head normal form. The latter is to
ensure that we do not end up with redundant canonical projections to the mixin,
i.e. them all being of the shape [ofe_mixin_of' A id]. *)
Definition ofe_mixin_of' {SI : sidx} A {Ac : ofe} (f : Ac → A) : OfeMixin Ac
:= ofe_mixin Ac.
(* iris/algebra/ofe.v *)
Notation ofe_mixin_of A
:=
  ltac:(let H := eval hnf in (ofe_mixin_of' A id) in exact H) (only parsing).
(* iris/algebra/ofe.v *)
Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y.
Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
(* iris/algebra/ofe.v *)
Instance dist_equivalence n : Equivalence (@dist SI A _ n).
Proof. apply (mixin_dist_equivalence _ (ofe_mixin A)). Qed.
(* iris/algebra/ofe.v *)
Lemma dist_le n m x y : x ≡{n}≡ y → m ≤ n → x ≡{m}≡ y.
Proof. apply (mixin_dist_le _ (ofe_mixin A)). Qed.
(* iris/algebra/ofe.v *)
(* Discrete OFEs and discrete OFE elements *)
Class Discrete {SI : sidx} {A : ofe} (x : A)
:=
  discrete_0 y : x ≡{0ᵢ}≡ y → x ≡ y.
(* iris/algebra/ofe.v *)
Instance : Params (@Discrete) 2
:= {}.
(* iris/algebra/ofe.v *)
Class OfeDiscrete {SI : sidx} (A : ofe)
:=
  #[global] ofe_discrete_discrete (x : A) :: Discrete x.
(* iris/algebra/ofe.v *)
(* A (converging) "chain" is a sequence of type [A] such that from the n-th
position onwards, everything is n-equal. *)
Record chain {SI : sidx} (A : ofe)
:= {
  chain_car :> SI → A;
  chain_cauchy n m: n ≤ m → chain_car m ≡{n}≡ chain_car n
}.
(* iris/algebra/ofe.v *)
(* A "bounded chain" up to step index [n] is similar to a "chain", except that
the sequence has length [n], i.e., it is only defined for indices strictly less
than [n]. *)
Record bchain {SI : sidx} (A : ofe) (n : SI)
:= {
  bchain_car :> ∀ m, m < n → A;
  bchain_cauchy m p Hm Hp : m ≤ p → bchain_car p Hp ≡{m}≡ bchain_car m Hm
}.
(* iris/algebra/ofe.v *)
Definition chain_map {SI : sidx} {A B : ofe} (f : A → B)
    `{NonExpansive f} (c : chain A) : chain B :=
  {| chain_car n := f (c n) |}.
Next Obligation. by intros SI A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
(* iris/algebra/ofe.v *)
Definition bchain_map {SI : sidx} {A B : ofe} (f : A → B)
    `{NonExpansive f} {n} (c : bchain A n) : bchain B n :=
  {| bchain_car m Hm := f (c m Hm) |}.
Next Obligation.
  by intros SI A B f Hf n c m p ? Hm Hp; apply Hf, bchain_cauchy.
Qed.
(* iris/algebra/ofe.v *)
(* These notations [Compl] and [LBCompl] are convenient to define instances
(e.g., [ofe_mor_compl] without having to repeat the type. The notation [BCompl]
will be used as the type for [bcompl], completing [bchain] with an arbitrary
bound [n]. *)
Notation Compl A
:= (chain A%type → A).
(* iris/algebra/ofe.v *)
Notation BCompl A
:= (∀ n, bchain A%type n → A).
(* iris/algebra/ofe.v *)
Notation LBCompl A
:= (∀ n, SIdx.limit n → bchain A%type n → A).
(* iris/algebra/ofe.v *)
Class Cofe {SI : sidx} (A : ofe)
:= {
  compl : Compl A;
  lbcompl : LBCompl A;
  conv_compl n c : compl c ≡{n}≡ c n;
  conv_lbcompl {n} Hn (c : bchain A n) {m} Hm : lbcompl n Hn c ≡{m}≡ c m Hm;
  (** The bounded limit operation is non-expansive: for chains agreeing up to
  the limit index, the bounded limits agree *)
  lbcompl_ne n {Hn} (c1 c2 : bchain A n) m :
    (∀ p (Hp : p < n), c1 p Hp ≡{m}≡ c2 p Hp) →
    lbcompl n Hn c1 ≡{m}≡ lbcompl n Hn c2
}.
(* iris/algebra/ofe.v *)
Lemma compl_chain_map {SI : sidx} `{!Cofe A, !Cofe B} (f : A → B) c
    `(!NonExpansive f) :
  compl (chain_map f c) ≡ f (compl c).
Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
(* iris/algebra/ofe.v *)
Definition chain_const {SI : sidx} {A : ofe} (a : A) : chain A :=
  {| chain_car n := a |}.
Next Obligation. by intros SI A a n i _. Qed.
(* iris/algebra/ofe.v *)
Lemma compl_chain_const {SI : sidx} `{!Cofe A} (a : A) :
  compl (chain_const a) ≡ a.
Proof. apply equiv_dist=> n. by rewrite conv_compl. Qed.
(* iris/algebra/ofe.v *)
Lemma compl_bchain_map {SI : sidx} `{!Cofe A, !Cofe B} (f : A → B)
    n Hn (c : bchain A n) `(!NonExpansive f) m :
  m < n → lbcompl Hn (bchain_map f c) ≡{m}≡ f (lbcompl Hn c).
Proof. intros Hm. by rewrite !(conv_lbcompl _ _ Hm). Qed.
(* iris/algebra/ofe.v *)
Definition bchain_const {SI : sidx} {A : ofe} (a : A) n : bchain A n :=
  {| bchain_car m _ := a |}.
Next Obligation. by intros SI A a n m p Hm Hp Hle. Qed.
(* iris/algebra/ofe.v *)
Definition bchain_le {SI : sidx} `{!Cofe A} {n}
    (c : bchain A n) {m} (Hm : m ≤ n) : bchain A m :=
  {| bchain_car m' Hm' := c m' (SIdx.lt_le_trans _ _ _ Hm' Hm) |}.
Next Obligation.
  intros SI A ? n c m Hm p1 p2 Hp Hp1 Hp2; simpl. by apply (bchain_cauchy n c).
Qed.
(* iris/algebra/ofe.v *)
Lemma lbcompl_bchain_le {SI : sidx} `{!Cofe A} n Hn m Hm (Hmn : m ≤ n)
    (c : bchain A n) p :
  p < m → lbcompl Hm (bchain_le c Hmn) ≡{p}≡ lbcompl Hn c.
Proof.
  intros Hp. rewrite (conv_lbcompl _ _ Hp).
  rewrite conv_lbcompl. by rewrite /bchain_le /=.
Qed.
(* iris/algebra/ofe.v *)
Instance ofe_equivalence : Equivalence ((≡) : relation A).
Proof.
    split.
    - by intros x; rewrite equiv_dist.
    - by intros x y; rewrite !equiv_dist.
    - by intros x y z; rewrite !equiv_dist; intros; trans y.
  Qed.
(* iris/algebra/ofe.v *)
Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist SI A _ n).
Proof.
    intros x1 x2 ? y1 y2 ?; split; intros.
    - by trans x1; [|trans y1].
    - by trans x2; [|trans y2].
  Qed.
(* iris/algebra/ofe.v *)
Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist SI A _ n).
Proof.
    by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
  Qed.
(* iris/algebra/ofe.v *)
Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x).
Proof. by apply dist_proper. Qed.
(* iris/algebra/ofe.v *)
Instance Discrete_proper : Proper ((≡) ==> iff) (@Discrete SI A).
Proof. intros x y Hxy. rewrite /Discrete. by setoid_rewrite Hxy. Qed.
(* iris/algebra/ofe.v *)
Lemma dist_lt n m x y : x ≡{n}≡ y → m < n → x ≡{m}≡ y.
Proof. eauto using dist_le, SIdx.lt_le_incl. Qed.
(* iris/algebra/ofe.v *)
Lemma dist_le' n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y.
Proof. eauto using dist_le. Qed.
(* iris/algebra/ofe.v *)
Lemma dist_S n x y : x ≡{Sᵢ n}≡ y → x ≡{n}≡ y.
Proof. intros H. eapply dist_lt; eauto using SIdx.lt_succ_diag_r. Qed.
(* iris/algebra/ofe.v *)
(* [ne_proper] and [ne_proper_2] are not instances to improve efficiency of
  type class search during setoid rewriting.
  Local Instances of [NonExpansive{,2}] are hence accompanied by instances of
  [Proper] built using these lemmas. *)
Lemma ne_proper {B : ofe} (f : A → B) `{!NonExpansive f} :
    Proper ((≡) ==> (≡)) f.
Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
(* iris/algebra/ofe.v *)
Lemma ne_proper_2 {B C : ofe} (f : A → B → C) `{!NonExpansive2 f} :
    Proper ((≡) ==> (≡) ==> (≡)) f.
Proof.
     unfold Proper, respectful; setoid_rewrite equiv_dist.
     by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
  Qed.
(* iris/algebra/ofe.v *)
Lemma conv_compl_le `{!Cofe A} n m (c : chain A) : n ≤ m → compl c ≡{n}≡ c m.
Proof.
    transitivity (c n); first by rewrite conv_compl.
    symmetry. by rewrite chain_cauchy.
  Qed.
(* iris/algebra/ofe.v *)
Lemma conv_compl_S `{!Cofe A} n (c : chain A) : compl c ≡{n}≡ c (Sᵢ n).
Proof. apply conv_compl_le, SIdx.le_succ_diag_r. Qed.
(* iris/algebra/ofe.v *)
Lemma discrete_iff n x y `{!TCOr (Discrete x) (Discrete y)} :
    x ≡ y ↔ x ≡{n}≡ y.
Proof.
    split; intros; [by auto|].
    destruct select (TCOr _ _); [|symmetry];
      apply (discrete_0 _), dist_le with n; eauto using SIdx.le_0_l.
  Qed.
(* iris/algebra/ofe.v *)
Lemma discrete_iff_0 n x y `{!TCOr (Discrete x) (Discrete y)} :
    x ≡{0ᵢ}≡ y ↔ x ≡{n}≡ y.
Proof. by rewrite -!discrete_iff. Qed.
(* iris/algebra/ofe.v *)
Lemma discrete n x y `{!TCOr (Discrete x) (Discrete y)} :
    x ≡{n}≡ y → x ≡ y.
Proof. intros. eapply discrete_iff; done. Qed.
(* iris/algebra/ofe.v *)
Instance ofe_discrete_subrelation `{!OfeDiscrete A} n :
    @SolveProperSubrelation A (dist n) (≡).
Proof. intros ???. apply: discrete. done. Qed.
(* iris/algebra/ofe.v *)
Instance ofe_leibniz_subrelation `{!OfeDiscrete A, !LeibnizEquiv A} n :
    @SolveProperSubrelation A (dist n) (=).
Proof. intros ?? EQ. unfold_leibniz. apply (is_solve_proper_subrelation EQ). Qed.
(* iris/algebra/ofe.v *)
(* Defined as a record to avoid eager unfolding. *)
Record dist_later {SI : sidx} `{!Dist A} (n : SI) (x y : A) : Prop
:=
  { dist_later_lt : ∀ m, m < n → x ≡{m}≡ y }.