phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/ofe.v *)
Instance dist_later_equivalence n : Equivalence (@dist_later SI A _ n).
Proof.
    split.
    - intros ?; by split.
    - intros ?? [H]; split; intros ??; by rewrite H.
    - intros ??? [H1] [H2]; split; intros ??; by rewrite H1 ?H2.
  Qed.
(* iris/algebra/ofe.v *)
Lemma dist_dist_later n x y : dist n x y → dist_later n x y.
Proof. intros. split; eauto using dist_lt. Qed.
(* iris/algebra/ofe.v *)
Lemma dist_later_dist_lt n m (x y : A) : m < n → dist_later n x y → dist m x y.
Proof. intros ? H; by apply H. Qed.
(* iris/algebra/ofe.v *)
Lemma dist_later_0 x y : dist_later 0ᵢ x y.
Proof. split. intros ? []%SIdx.nlt_0_r. Qed.
(* iris/algebra/ofe.v *)
Lemma dist_later_S n x y : x ≡{n}≡ y ↔ dist_later (Sᵢ n) x y.
Proof.
    split.
    - intros Hn; split; intros m Hm%SIdx.lt_succ_r. by eapply dist_le.
    - intros Hdist. by apply Hdist, SIdx.lt_succ_r.
  Qed.
(* iris/algebra/ofe.v *)
(* We don't actually need this lemma (as our tactics deal with this through
   other means), but technically speaking, this is the reason why
   pre-composing a non-expansive function to a contractive function
   preserves contractivity. *)
Lemma ne_dist_later {SI : sidx} {A B : ofe} (f : A → B) :
  NonExpansive f → ∀ n, Proper (dist_later n ==> dist_later n) f.
Proof. intros Hf ??? [H]; split; intros ??; by eapply Hf, H. Qed.
(* iris/algebra/ofe.v *)
Notation Contractive f
:= (∀ n, Proper (dist_later n ==> dist n) f).
(* iris/algebra/ofe.v *)
Instance const_contractive {SI : sidx} {A B : ofe} (x : A) :
  Contractive (@const A B x).
Proof. by intros n y1 y2. Qed.
(* iris/algebra/ofe.v *)
Lemma contractive_0 x y : f x ≡{0ᵢ}≡ f y.
Proof. by apply (_ : Contractive f), dist_later_0. Qed.
(* iris/algebra/ofe.v *)
Lemma contractive_dist_later_dist n x y : dist_later n x y → f x ≡{n}≡ f y.
Proof. by apply (_ : Contractive f). Qed.
(* iris/algebra/ofe.v *)
Lemma contractive_S n x y : x ≡{n}≡ y → f x ≡{Sᵢ n}≡ f y.
Proof. intros. by apply contractive_dist_later_dist, dist_later_S. Qed.
(* iris/algebra/ofe.v *)
Instance contractive_ne : NonExpansive f | 100.
Proof.
    intros n x y ?; eapply (dist_lt (Sᵢ n)), SIdx.lt_succ_diag_r.
    eapply contractive_dist_later_dist. split.
    intros ??%SIdx.lt_succ_r. by eapply dist_le.
  Qed.
(* iris/algebra/ofe.v *)
Instance contractive_proper : Proper ((≡) ==> (≡)) f | 100.
Proof. apply (ne_proper _). Qed.
(* iris/algebra/ofe.v *)
Lemma dist_pointwise_lt {SI : sidx} {A} {B : ofe} n m (f g : A → B):
  m < n →
  pointwise_relation A (dist_later n) f g →
  pointwise_relation A (dist m) f g.
Proof. intros Hlt Hp a. by apply Hp. Qed.
(* iris/algebra/ofe.v *)
(* The tactic [f_contractive] can be used to prove contractiveness or
non-expansiveness of a function [f]. Inside of the proof of
contractiveness/non-expansiveness, if the current goal is
  [g x1 ... xn ≡{i}≡ g y1 ... yn]
for a contractive function [g] (that is used inside of the body of [f]),
then the tactic will try to find a suitable [Contractive] instance for [g]
and apply it. Currently, the tactic only supports one (i.e., [n = 1]) and
two (i.e., [n = 2]) arguments. As a result of applying the [Contractive]
instance for [g], one of the goals will be [dist_later i xi yi] and the tactic
will try to simplify or solve the goal. By simplify we mean that it will
turn hypotheses [dist_later] into [dist].

The tactic [f_contractive] is implemented using

1. [f_contractive_prepare] which looks up a [Contractive] looks at which
   function is being applied on both sides of a [dist], looks up the
   [Contractive] instance (or the equivalent for two arguments) and applies it.
2. [dist_later_intro] introduces the resulting goals with [dist_later n x y]. *)
Ltac f_contractive_prepare
:=
  match goal with
  | |- ?f _ ≡{_}≡ ?f _ => simple apply (_ : Proper (dist_later _ ==> dist _) f)
  | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (dist_later _ ==> _ ==> dist _) f)
  | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (_ ==> dist_later _ ==> dist _) f)
  end.
(* iris/algebra/ofe.v *)
Ltac solve_contractive
:=
  solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]).
(* iris/algebra/ofe.v *)
(* To perform induction over a fixpoint ([fixpoint_ind]) and to construct the
COFE over a Sigma type ([sig_cofe]) we need the predicate to be limit
preserving: if it holds for every element of a chain, it must hold for the
limit. *)
Class LimitPreserving {SI : sidx} `{!Cofe A} (P : A → Prop) : Prop
:= {
  limit_preserving_compl (c : chain A) :
    (∀ n, P (c n)) → P (compl c);
  limit_preserving_lbcompl n Hn (c : bchain A n) :
    (∀ m Hm, P (c m Hm)) → P (lbcompl Hn c);
}.
(* iris/algebra/ofe.v *)
(* These lemmas are not instances as they will never fire automatically...
  but they can still be helpful in proving things to be limit preserving. *)
Lemma limit_preserving_sidx_finite `{!SIdxFinite SI} P :
    LimitPreserving P ↔ ∀ c : chain A, (∀ n, P (c n)) → P (compl c).
Proof.
    split; [by destruct 1|]. intros Hcompl. split; [done|].
    intros n Hn. by destruct (SIdx.limit_finite n).
  Qed.
(* iris/algebra/ofe.v *)
Lemma limit_preserving_ext (P Q : A → Prop) :
    (∀ x, P x ↔ Q x) → LimitPreserving P → LimitPreserving Q.
Proof.
    intros HP [Hcompl Hlbcompl]. split.
    - intros c ?. apply HP, Hcompl=> n; by apply HP.
    - intros n Hn c HC. apply HP, Hlbcompl=> m Hm. by apply HP.
  Qed.
(* iris/algebra/ofe.v *)
Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _ : A, P).
Proof.
    split.
    - intros c HP. apply (HP 0ᵢ).
    - intros n [Hlim Hn] Hc HP. by apply (HP (Sᵢ 0ᵢ)), Hlim, SIdx.neq_0_lt_0.
  Qed.
(* iris/algebra/ofe.v *)
Lemma limit_preserving_discrete P :
    Proper (dist 0ᵢ ==> impl) P → LimitPreserving P.
Proof.
    intros HP. split.
    - intros c Hc. by rewrite (conv_compl 0ᵢ).
    - intros n Hn c HPc.
      rewrite (conv_lbcompl _ _ (SIdx.limit_lt_0 _ Hn)). apply HPc.
  Qed.
(* iris/algebra/ofe.v *)
Lemma limit_preserving_and P1 P2 :
    LimitPreserving P1 →
    LimitPreserving P2 →
    LimitPreserving (λ x, P1 x ∧ P2 x).
Proof.
    intros [Hcompl1 Hlbcompl1] [Hcompl2 Hlbcompl2]. split.
    - intros c Hc. split; [apply Hcompl1|apply Hcompl2]; apply Hc.
    - intros n Hn c Hc. split; [apply Hlbcompl1|apply Hlbcompl2]; apply Hc.
  Qed.
(* iris/algebra/ofe.v *)
Lemma limit_preserving_impl P1 P2 :
    Proper (dist 0ᵢ ==> impl) P1 →
    LimitPreserving P2 →
    LimitPreserving (λ x, P1 x → P2 x).
Proof.
    intros HP1 [Hcompl Hlbcompl]. split.
    - intros c Hc HP1c. apply Hcompl=> n. eapply Hc, HP1, HP1c.
      apply dist_le with n, SIdx.le_0_l. apply conv_compl.
    - intros n Hn c Hc HP1c. apply Hlbcompl=> m Hm. eapply Hc, HP1, HP1c.
      apply dist_le with m, SIdx.le_0_l. apply conv_lbcompl.
  Qed.
(* iris/algebra/ofe.v *)
(* This is strictly weaker than the [_impl] variant, but sometimes automation
  is better at proving [Proper] for [iff] than for [impl]. *)
Lemma limit_preserving_impl' P1 P2 :
    Proper (dist 0ᵢ ==> iff) P1 →
    LimitPreserving P2 →
    LimitPreserving (λ x, P1 x → P2 x).
Proof.
    intros HP1. apply limit_preserving_impl. intros ???.
    apply iff_impl_subrelation. by apply HP1.
  Qed.
(* iris/algebra/ofe.v *)
Lemma limit_preserving_forall {B} (P : B → A → Prop) :
    (∀ y, LimitPreserving (P y)) →
    LimitPreserving (λ x, ∀ y, P y x).
Proof.
    intros Hlim. split.
    - intros c Hc y. by apply Hlim.
    - intros n Hn c Hc y. by apply Hlim.
  Qed.
(* iris/algebra/ofe.v *)
(* We need [SIdxFinite] because [compl_bchain_map] does not hold for [≡],
  only for a bounded [≡{m}≡]. *)
Lemma limit_preserving_equiv `{!SIdxFinite SI} `{!Cofe B} (f g : A → B) :
    NonExpansive f → NonExpansive g → LimitPreserving (λ x, f x ≡ g x).
Proof.
    intros Hf Hg. apply limit_preserving_sidx_finite=> c Hfg.
    apply equiv_dist=> n. by rewrite -!compl_chain_map !conv_compl /= Hfg.
  Qed.
(* iris/algebra/ofe.v *)
Definition bcompl : BCompl A
:= λ n c,
    match SIdx.case n with
    | inl (inl Hn') => inhabitant
    (* If the chain ends in a non-zero non-limit ordinal, we can just take the
    last element as the limit. *)
    | inl (inr (m ↾ Hm)) => c m (SIdx.lt_succ_diag_r' _ _ Hm)
    | inr Hlim => lbcompl Hlim c
    end.
(* iris/algebra/ofe.v *)
Lemma conv_bcompl {n} (c : bchain A n) m Hm : bcompl n c ≡{m}≡ c m Hm.
Proof.
    rewrite /bcompl. destruct (SIdx.case _) as [[->|[m' ->]]|?]; simpl.
    - by destruct (SIdx.nlt_0_r m).
    - by apply bchain_cauchy, SIdx.lt_succ_r.
    - apply conv_lbcompl.
  Qed.
(* iris/algebra/ofe.v *)
Lemma bcompl_ne {n} (c1 c2 : bchain A n) m :
    (∀ p (Hp : p < n), c1 p Hp ≡{m}≡ c2 p Hp) →
    bcompl n c1 ≡{m}≡ bcompl n c2.
Proof.
    intros Hc. rewrite /bcompl. destruct (SIdx.case _) as [[?|[m' ->]]|?]; simpl.
    - done.
    - apply Hc.
    - by apply lbcompl_ne.
  Qed.
(* iris/algebra/ofe.v *)
Lemma limit_preserving_bcompl (P : A → Prop) n (c : bchain A n) :
    n ≠ 0ᵢ ∨ P inhabitant →
    LimitPreserving P →
    (∀ m Hm, P (c m Hm)) → P (bcompl n c).
Proof.
    intros H0 [Hcompl Hlbcompl] HP. rewrite /bcompl.
    destruct (SIdx.case _) as [[?|[m' ->]]|?]; naive_solver.
  Qed.
(* iris/algebra/ofe.v *)
(* Note that [bfchain] is a private implementation detail, but Coq does not
  allow us to make records [Local]. *)
Record bfchain n
:= {
    bfchain_car :> bchain A n;
    bfchain_fixpoint p :
      p < n → f (bcompl n bfchain_car) ≡{p}≡ bcompl n bfchain_car;
  }.
(* iris/algebra/ofe.v *)
Lemma bfchain_chain_unique {n m} (c1 : bfchain n) (c2 : bfchain m) p :
    p < n → p < m → bcompl n c1 ≡{p}≡ bcompl m c2.
Proof using Type*.
    intros Hn Hm. induction (SIdx.lt_wf p) as [p _ IH].
    rewrite -(bfchain_fixpoint _ c2) // -(bfchain_fixpoint _ c1) //.
    apply (contractive_dist_later_dist _); split=> p' Hp'.
    apply IH; [done|by etrans..].
  Qed.
(* iris/algebra/ofe.v *)
Definition fixpoint_bchain_go n
      (rec : ∀ m, m < n → bfchain m) : bfchain n :=
    {| bfchain_car := {| bchain_car m' Hm' := f (bcompl m' (rec _ Hm')) |} |}.
Next Obligation.
    intros n rec m m' Hmn Hmn' Hm; simpl.
    apply (contractive_dist_later_dist _); split=> p Hp.
    apply bfchain_chain_unique; eauto using SIdx.lt_le_trans.
  Qed.
(* iris/algebra/ofe.v *)
(* We obtain a bounded fixpoint chain for every index [n] by index recursion.
  In the recursive case, we construct a new chain up to [n] by taking,
  for any [m < n], the limit of the [m]-th chain before applying [f] to it. *)
Definition fixpoint_bchain n : bfchain n
:=
    Fix SIdx.lt_wf bfchain fixpoint_bchain_go n.
(* iris/algebra/ofe.v *)
(* We obtain a final full chain by repeating this construction for every [n],
     using the bounded chains computed before. *)
Definition fixpoint_chain : chain A :=
    {| chain_car n := f (bcompl n (fixpoint_bchain n)) |}.
Next Obligation.
    intros n m [Hnm| ->]%SIdx.le_lteq; simpl; [|done].
    apply (contractive_dist_later_dist _); split=> p Hp.
    apply bfchain_chain_unique; [by etrans|done].
  Qed.
(* iris/algebra/ofe.v *)
Definition fixpoint_def : A
:= compl fixpoint_chain.
(* iris/algebra/ofe.v *)
Definition fixpoint_aux : seal (@fixpoint_def).
Proof using Type. by eexists. Qed.
(* iris/algebra/ofe.v *)
Definition fixpoint
:= fixpoint_aux.(unseal).
(* iris/algebra/ofe.v *)
Definition fixpoint_unseal :
    @fixpoint = @fixpoint_def
:= fixpoint_aux.(seal_eq).
(* iris/algebra/ofe.v *)
(* This lemma does not work well with [rewrite]; we usually define a specific
  unfolding lemma for each fixpoint and then [apply fixpoint_unfold] in the
  proof of that unfolding lemma. *)
Lemma fixpoint_unfold : fixpoint ≡ f fixpoint.
Proof.
    apply equiv_dist=> n. rewrite fixpoint_unseal /fixpoint_def /=.
    rewrite !conv_compl /fixpoint_chain /=.
    apply (contractive_dist_later_dist _); split=> p Hp.
    by rewrite bfchain_fixpoint.
  Qed.
(* iris/algebra/ofe.v *)
Lemma fixpoint_unique (x : A) : x ≡ f x → x ≡ fixpoint f.
Proof.
    rewrite !equiv_dist=> Hx n. induction (SIdx.lt_wf n) as [n _ IH].
    rewrite Hx fixpoint_unfold. f_contractive; eauto.
  Qed.
(* iris/algebra/ofe.v *)
Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
    (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
Proof.
    intros Hfg. induction (SIdx.lt_wf n) as [n _ IH].
    rewrite (fixpoint_unfold f) (fixpoint_unfold g) -Hfg.
    f_contractive. apply IH; eauto using dist_lt.
  Qed.
(* iris/algebra/ofe.v *)
Lemma fixpoint_proper (g : A → A) `{!Contractive g} :
    (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
(* iris/algebra/ofe.v *)
Lemma fixpoint_ind (P : A → Prop) :
    Proper ((≡) ==> impl) P →
    (∃ x, P x) →
    (∀ x, P x → P (f x)) →
    LimitPreserving P →
    P (fixpoint f).
Proof.
    intros HP [x Hx] Hf Hlim. eapply HP.
    { eapply fixpoint_unique, (@fixpoint_unfold _ _ _ (populate x) f). }
    rewrite fixpoint_unseal /fixpoint_def. apply Hlim=> m /=.
    apply Hf. rewrite /fixpoint_bchain /Fix.
    generalize (SIdx.lt_wf m). revert m. fix IH 2=> m acc.
    apply limit_preserving_bcompl; [auto..|].
    intros m' Hm'. destruct acc as [acc]; simpl. apply Hf, IH.
  Qed.
(* iris/algebra/ofe.v *)
(* Fixpoint of [f] when [f^k] is contractive. * *)
Definition fixpointK {SI : sidx} `{!Cofe A, !Inhabited A} k (f : A → A)
  `{!Contractive (Nat.iter k f)}
:= fixpoint (Nat.iter k f).
(* iris/algebra/ofe.v *)
(* Note than f_ne is crucial here:  there are functions f such that f^2 is contractive,
     but f is not non-expansive.
     Consider for example f: SPred → SPred (where SPred is "downclosed sets of natural numbers").
     Define f (using informative excluded middle) as follows:
     f(N) = N  (where N is the set of all natural numbers)
     f({0, ..., n}) = {0, ... n-1}  if n is even (so n-1 is at least -1, in which case we return the empty set)
     f({0, ..., n}) = {0, ..., n+2} if n is odd
     In other words, if we consider elements of SPred as ordinals, then we decreaste odd finite
     ordinals by 1 and increase even finite ordinals by 2.
     f is not non-expansive:  Consider f({0}) = ∅ and f({0,1}) = f({0,1,2,3}).
     The arguments are clearly 0-equal, but the results are not.

     Now consider g := f^2. We have
     g(N) = N
     g({0, ..., n}) = {0, ... n+1}  if n is even
     g({0, ..., n}) = {0, ..., n+4} if n is odd
     g is contractive.  All outputs contain 0, so they are all 0-equal.
     Now consider two n-equal inputs. We have to show that the outputs are n+1-equal.
     Either they both do not contain n in which case they have to be fully equal and
     hence so are the results.  Or else they both contain n, so the results will
     both contain n+1, so the results are n+1-equal. *)
Let f_proper : Proper ((≡) ==> (≡)) f
:= ne_proper f.
(* iris/algebra/ofe.v *)
Lemma fixpointK_unfold : fixpointK k f ≡ f (fixpointK k f).
Proof.
    symmetry. rewrite /fixpointK. apply fixpoint_unique.
    by rewrite -Nat.iter_succ_r Nat.iter_succ -fixpoint_unfold.
  Qed.
(* iris/algebra/ofe.v *)
Lemma fixpointK_unique (x : A) : x ≡ f x → x ≡ fixpointK k f.
Proof.
    intros Hf. apply fixpoint_unique. clear f_contractive.
    induction k as [|k' IH]=> //=. by rewrite -IH.
  Qed.
(* iris/algebra/ofe.v *)
Lemma fixpointK_ne n : (∀ z, f z ≡{n}≡ g z) → fixpointK k f ≡{n}≡ fixpointK k g.
Proof.
      rewrite /fixpointK=> Hfg /=. apply fixpoint_ne=> z.
      clear f_contractive g_contractive.
      induction k as [|k' IH]=> //=. by rewrite IH Hfg.
    Qed.
(* iris/algebra/ofe.v *)
Lemma fixpointK_proper : (∀ z, f z ≡ g z) → fixpointK k f ≡ fixpointK k g.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpointK_ne. Qed.
(* iris/algebra/ofe.v *)
Lemma fixpointK_ind (P : A → Prop) :
    Proper ((≡) ==> impl) P →
    (∃ x, P x) → (∀ x, P x → P (f x)) →
    LimitPreserving P →
    P (fixpointK k f).
Proof.
    intros. rewrite /fixpointK. apply fixpoint_ind; eauto.
    intros; apply Nat.iter_ind; auto.
  Qed.
(* iris/algebra/ofe.v *)
Definition fixpoint_AB (x : A) : B
:= fixpoint (fB x).
(* iris/algebra/ofe.v *)
Instance fixpoint_AB_contractive : Contractive fixpoint_AB.
Proof.
    intros n x x' Hx; rewrite /fixpoint_AB.
    apply fixpoint_ne=> y. by f_contractive.
  Qed.
(* iris/algebra/ofe.v *)
Definition fixpoint_AA (x : A) : A
:= fA x (fixpoint_AB x).
(* iris/algebra/ofe.v *)
Instance fixpoint_AA_contractive : Contractive fixpoint_AA.
Proof using fA_contractive. solve_contractive. Qed.
(* iris/algebra/ofe.v *)
Definition fixpoint_A : A
:= fixpoint fixpoint_AA.
(* iris/algebra/ofe.v *)
Definition fixpoint_B : B
:= fixpoint_AB fixpoint_A.
(* iris/algebra/ofe.v *)
Lemma fixpoint_A_unfold : fA fixpoint_A fixpoint_B ≡ fixpoint_A.
Proof. by rewrite {2}/fixpoint_A (fixpoint_unfold _). Qed.
(* iris/algebra/ofe.v *)
Lemma fixpoint_B_unfold : fB fixpoint_A fixpoint_B ≡ fixpoint_B.
Proof. by rewrite {2}/fixpoint_B /fixpoint_AB (fixpoint_unfold _). Qed.
(* iris/algebra/ofe.v *)
Instance : Proper ((≡) ==> (≡) ==> (≡)) fA.
Proof using fA_contractive.
    apply ne_proper_2=> n x x' ? y y' ?. f_contractive; eauto using dist_lt.
  Qed.
(* iris/algebra/ofe.v *)
Instance : Proper ((≡) ==> (≡) ==> (≡)) fB.
Proof using fB_contractive.
    apply ne_proper_2=> n x x' ? y y' ?. f_contractive; eauto using dist_lt.
  Qed.
(* iris/algebra/ofe.v *)
Lemma fixpoint_A_unique p q : fA p q ≡ p → fB p q ≡ q → p ≡ fixpoint_A.
Proof.
    intros HfA HfB. rewrite -HfA. apply fixpoint_unique. rewrite /fixpoint_AA.
    f_equiv=> //. apply fixpoint_unique. by rewrite HfA HfB.
  Qed.
(* iris/algebra/ofe.v *)
Lemma fixpoint_B_unique p q : fA p q ≡ p → fB p q ≡ q → q ≡ fixpoint_B.
Proof. intros. apply fixpoint_unique. by rewrite -fixpoint_A_unique. Qed.
(* iris/algebra/ofe.v *)
Lemma fixpoint_A_ne n :
    (∀ x y, fA x y ≡{n}≡ fA' x y) → (∀ x y, fB x y ≡{n}≡ fB' x y) →
    fixpoint_A fA fB ≡{n}≡ fixpoint_A fA' fB'.
Proof.
    intros HfA HfB. apply fixpoint_ne=> z.
    rewrite /fixpoint_AA /fixpoint_AB HfA. f_equiv. by apply fixpoint_ne.
  Qed.
(* iris/algebra/ofe.v *)
Lemma fixpoint_B_ne n :
    (∀ x y, fA x y ≡{n}≡ fA' x y) → (∀ x y, fB x y ≡{n}≡ fB' x y) →
    fixpoint_B fA fB ≡{n}≡ fixpoint_B fA' fB'.
Proof.
    intros HfA HfB. apply fixpoint_ne=> z. rewrite HfB. f_contractive.
    apply fixpoint_A_ne; eauto using dist_lt.
  Qed.
(* iris/algebra/ofe.v *)
Lemma fixpoint_A_proper :
    (∀ x y, fA x y ≡ fA' x y) → (∀ x y, fB x y ≡ fB' x y) →
    fixpoint_A fA fB ≡ fixpoint_A fA' fB'.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_A_ne. Qed.
(* iris/algebra/ofe.v *)
Lemma fixpoint_B_proper :
    (∀ x y, fA x y ≡ fA' x y) → (∀ x y, fB x y ≡ fB' x y) →
    fixpoint_B fA fB ≡ fixpoint_B fA' fB'.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_B_ne. Qed.
(* iris/algebra/ofe.v *)
(* Non-expansive function space *)
Record ofe_mor {SI : sidx} (A B : ofe) : Type
:= OfeMor {
  ofe_mor_car :> A → B;
  ofe_mor_ne : NonExpansive ofe_mor_car
}.
(* iris/algebra/ofe.v *)
Notation "'λne' x .. y , t"
:=
  (@OfeMor _ _ _ (λ x, .. (@OfeMor _ _ _ (λ y, t) _) ..) _)
  (at level 200, x binder, y binder, right associativity).
(* iris/algebra/ofe.v *)
Instance ofe_mor_proper (f : ofe_mor A B) : Proper ((≡) ==> (≡)) f.
Proof. apply ne_proper, ofe_mor_ne. Qed.
(* iris/algebra/ofe.v *)
Instance ofe_mor_equiv : Equiv (ofe_mor A B)
:= λ f g, ∀ x, f x ≡ g x.
(* iris/algebra/ofe.v *)
Instance ofe_mor_dist : Dist (ofe_mor A B)
:= λ n f g, ∀ x, f x ≡{n}≡ g x.
(* iris/algebra/ofe.v *)
Definition ofe_mor_ofe_mixin : OfeMixin (ofe_mor A B).
Proof.
    split.
    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
      intros Hfg k; apply equiv_dist=> n; apply Hfg.
    - intros n; split.
      + by intros f x.
      + by intros f g ? x.
      + by intros f g h ?? x; trans (g x).
    - intros n m f g ? x ?; eauto using dist_le.
  Qed.
(* iris/algebra/ofe.v *)
Canonical ofe_morO
:= Ofe (ofe_mor A B) ofe_mor_ofe_mixin.
(* iris/algebra/ofe.v *)
Definition ofe_mor_chain (c : chain ofe_morO)
    (x : A) : chain B := {| chain_car n := c n x |}.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
(* iris/algebra/ofe.v *)
Definition ofe_mor_compl `{!Cofe B} : Compl ofe_morO := λ c,
    {| ofe_mor_car x := compl (ofe_mor_chain c x) |}.
Next Obligation.
    intros ? c n x y Hx. by rewrite (conv_compl n (ofe_mor_chain c x))
      (conv_compl n (ofe_mor_chain c y)) /= Hx.
  Qed.
(* iris/algebra/ofe.v *)
Definition ofe_mor_bchain {n}
      (c : bchain ofe_morO n) (x : A) : bchain B n :=
    {| bchain_car n Hn := c n Hn x |}.
Next Obligation. intros n c x m Hm i ??. by apply (bchain_cauchy n c). Qed.
(* iris/algebra/ofe.v *)
Definition ofe_mor_lbcompl `{!Cofe B} : LBCompl ofe_morO := λ n Hn c,
    {| ofe_mor_car x := lbcompl Hn (ofe_mor_bchain c x) |}.
Next Obligation.
    intros ? n Hn c m x y Hx. apply lbcompl_ne=> p ?.
    rewrite /ofe_mor_bchain /=. by rewrite Hx.
  Qed.
(* iris/algebra/ofe.v *)
Instance ofe_mor_cofe `{!Cofe B} : Cofe ofe_morO :=
    {| compl := ofe_mor_compl; lbcompl := ofe_mor_lbcompl |}.
Next Obligation. intros ? n c x; simpl. by rewrite conv_compl. Qed.
(* iris/algebra/ofe.v *)
Instance ofe_mor_car_ne : NonExpansive2 (@ofe_mor_car SI A B).
Proof. intros n f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
(* iris/algebra/ofe.v *)
Instance ofe_mor_car_proper :
    Proper ((≡) ==> (≡) ==> (≡)) (@ofe_mor_car SI A B)
:= ne_proper_2 _.
(* iris/algebra/ofe.v *)
Lemma ofe_mor_ext (f g : ofe_mor A B) : f ≡ g ↔ ∀ x, f x ≡ g x.
Proof. done. Qed.
(* iris/algebra/ofe.v *)
Notation "A -n> B"
:=
  (ofe_morO A B) (at level 99, B at level 200, right associativity).
(* iris/algebra/ofe.v *)
Instance ofe_mor_inhabited {SI : sidx} {A B : ofe} `{Inhabited B} :
  Inhabited (A -n> B)
:= populate (λne _, inhabitant).
(* iris/algebra/ofe.v *)
(* Identity and composition and constant function *)
Definition cid {SI : sidx} {A: ofe} : A -n> A
:= OfeMor id.
(* iris/algebra/ofe.v *)
Instance : Params (@cid) 2
:= {}.
(* iris/algebra/ofe.v *)
Definition cconst {SI : sidx} {A B : ofe} (x : B) : A -n> B
:= OfeMor (const x).
(* iris/algebra/ofe.v *)
Instance : Params (@cconst) 3
:= {}.
(* iris/algebra/ofe.v *)
Definition ccompose {SI : sidx} {A B C: ofe}
  (f : B -n> C) (g : A -n> B) : A -n> C
:= OfeMor (f ∘ g).
(* iris/algebra/ofe.v *)
Instance : Params (@ccompose) 4
:= {}.
(* iris/algebra/ofe.v *)
Instance ccompose_ne {SI : sidx} {A B C: ofe} :
  NonExpansive2 (@ccompose SI A B C).
Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
(* iris/algebra/ofe.v *)
Instance ccompose_proper {SI : sidx} {A B C: ofe} :
  Proper ((≡) ==> (≡) ==> (≡)) (@ccompose SI A B C).
Proof. apply ne_proper_2; apply _. Qed.
(* iris/algebra/ofe.v *)
(* Function space maps *)
Definition ofe_mor_map {SI : sidx} {A A' B B': ofe}
    (f : A' -n> A) (g : B -n> B') (h : A -n> B) : A' -n> B'
:=
  g ◎ h ◎ f.
(* iris/algebra/ofe.v *)
Instance ofe_mor_map_ne {SI : sidx} {A A' B B': ofe} :
  NonExpansive3 (@ofe_mor_map SI A A' B B').
Proof. intros n ??? ??? ???. by repeat apply ccompose_ne. Qed.
(* iris/algebra/ofe.v *)
Definition ofe_morO_map {SI : sidx} {A A' B B': ofe}
    (f : A' -n> A) (g : B -n> B') : (A -n> B) -n> (A' -n>  B')
:=
  OfeMor (ofe_mor_map f g).
(* iris/algebra/ofe.v *)
Instance ofe_morO_map_ne {SI : sidx} {A A' B B': ofe} :
  NonExpansive2 (@ofe_morO_map SI A A' B B').
Proof.
  intros n f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
  by repeat apply ccompose_ne.
Qed.
(* iris/algebra/ofe.v *)
Instance unit_dist : Dist unit
:= λ _ _ _, True.
(* iris/algebra/ofe.v *)
Definition unit_ofe_mixin : OfeMixin unit.
Proof. repeat split. Qed.
(* iris/algebra/ofe.v *)
Canonical unitO : ofe
:= Ofe unit unit_ofe_mixin.
(* iris/algebra/ofe.v *)
Instance unit_cofe : Cofe unitO
:=
    { compl x := (); lbcompl _ _ _ := () }.
(* iris/algebra/ofe.v *)
Instance unit_ofe_discrete : OfeDiscrete unitO.
Proof. done. Qed.
(* iris/algebra/ofe.v *)
Instance Empty_set_dist : Dist Empty_set
:= λ _ _ _, True.
(* iris/algebra/ofe.v *)
Definition Empty_set_ofe_mixin : OfeMixin Empty_set.
Proof. by repeat split. Qed.
(* iris/algebra/ofe.v *)
Canonical Empty_setO : ofe
:= Ofe Empty_set Empty_set_ofe_mixin.
(* iris/algebra/ofe.v *)
Instance Empty_set_cofe : Cofe Empty_setO
:=
    {| compl c := c 0ᵢ; lbcompl n Hn c := c _ (SIdx.limit_lt_0 _ Hn) |}.
(* iris/algebra/ofe.v *)
Instance Empty_set_ofe_discrete : OfeDiscrete Empty_setO.
Proof. done. Qed.
(* iris/algebra/ofe.v *)
Instance prod_dist : Dist (A * B)
:= λ n, prod_relation (dist n) (dist n).