(* iris/algebra/ofe.v *)
From iris.prelude Require Export prelude
From iris.prelude Require Import options
From iris.algebra Require Export stepindex

Local SetPrimitive Projections.

Local OpenScope sidx_scope.

Class Dist{SI : sidx} A := dist : SI → relation A.

Global HintMode Dist - ! : typeclass_instances.

Global Instance: Params (@dist) 4 := {}.

Global HintExtern 0 (_ ≡{_}≡ _) => reflexivity : core.

Global HintExtern 0 (_ ≡{_}≡ _) => symmetry; assumption : core.

Notation NonExpansivef := (∀ n, Proper (dist n ==> dist n) f).

Notation NonExpansive2f := (∀ n, Proper (dist n ==> dist n ==> dist n) f).

Notation NonExpansive3f :=
  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) f).

Notation NonExpansive4f :=
  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) f).
Tactic Notation "ofe_subst" ident(x) :=
  repeat match goal with
  | _ => progress simplify_eq/=
  | H : @dist ?SI ?A ?d ?n x _ |- _ => setoid_subst_aux (@dist SI A d n) x
  | H : @dist ?SI ?A ?d ?n _ x |- _ =>
    symmetry in H; setoid_subst_aux (@dist SI A d n) x
  end.
Tactic Notation "ofe_subst" :=
  repeat match goal with
  | _ => progress simplify_eq/=
  | H : @dist ?SI ?A ?d ?n ?x _ |- _ => setoid_subst_aux (@dist SI A d n) x
  | H : @dist ?SI ?A ?d ?n _ ?x |- _ =>
    symmetry in H; setoid_subst_aux (@dist SI A d n) x
  end.

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
}.

Structure ofe{SI : sidx} := Ofe {
  ofe_car :> Type;
  ofe_equiv : Equiv ofe_car;
  ofe_dist : Dist ofe_car;
  ofe_mixin : OfeMixin ofe_car
}.

Global ArgumentsOfe {_} _ {_ _} _.
Add Printing Constructor ofe.

Global HintExtern 0 (Equiv _) => refine (ofe_equiv _); shelve : typeclass_instances.

Global HintExtern 0 (Dist _) => refine (ofe_dist _); shelve : typeclass_instances.

Global Argumentsofe_car : simpl never.

Global Argumentsofe_equiv : simpl never.

Global Argumentsofe_dist : simpl never.

Global Argumentsofe_mixin : simpl never.

Definition ofe_mixin_of'{SI : sidx} A {Ac : ofe} (f : Ac → A) : OfeMixin Ac := ofe_mixin Ac.

Notation ofe_mixin_ofA :=
  ltac:(let H := eval hnf in (ofe_mixin_of' A id) in exact H) (only parsing).

Lemma equiv_distx y : x ≡ y ↔ ∀ n, x ≡{n}≡ y.
  Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.

Global Instancedist_equivalence n : Equivalence (@dist SI A _ n).
  Proof. apply (mixin_dist_equivalence _ (ofe_mixin A)). Qed.

Lemma dist_len m x y : x ≡{n}≡ y → m ≤ n → x ≡{m}≡ y.
  Proof. apply (mixin_dist_le _ (ofe_mixin A)). Qed.

Global HintExtern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.

Class Discrete{SI : sidx} {A : ofe} (x : A) :=
  discrete_0 y : x ≡{0ᵢ}≡ y → x ≡ y.

Global Argumentsdiscrete_0 {_ _} _ {_} _ _.

Global HintMode Discrete - + ! : typeclass_instances.

Global Instance: Params (@Discrete) 2 := {}.

Class OfeDiscrete{SI : sidx} (A : ofe) :=
  #[global] ofe_discrete_discrete (x : A) :: Discrete x.

Global HintMode OfeDiscrete - ! : typeclass_instances.

Record chain{SI : sidx} (A : ofe) := {
  chain_car :> SI → A;
  chain_cauchy n m: n ≤ m → chain_car m ≡{n}≡ chain_car n
}.

Global Argumentschain_car {_ _} _ _.

Global Argumentschain_cauchy {_ _} _ _ _ _.

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
}.

Global Argumentsbchain_car {_ _} _ _ _.

Global Argumentsbchain_cauchy {_ _} _ _ _ _ _.

Program Definitionchain_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.

Program Definitionbchain_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.

Notation ComplA := (chain A%type → A).

Notation BComplA := (∀ n, bchain A%type n → A).

Notation LBComplA := (∀ n, SIdx.limit n → bchain A%type n → A).

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;

Global Argumentscompl : simpl never.

Global Argumentslbcompl {_ _ _ _} : simpl never.

Global HintMode Cofe - ! : typeclass_instances.

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.

Program Definitionchain_const {SI : sidx} {A : ofe} (a : A) : chain A :=
  {| chain_car n := a |}.
Next Obligation. by intros SI A a n i _. Qed.

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.

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.

Program Definitionbchain_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.

Program Definitionbchain_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.

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.

Global Instanceofe_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.

Global Instancedist_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.

Global Instancedist_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.

Global Instancedist_proper_2 n x : Proper ((≡) ==> iff) (dist n x).
  Proof. by apply dist_proper. Qed.

Global InstanceDiscrete_proper : Proper ((≡) ==> iff) (@Discrete SI A).
  Proof. intros x y Hxy. rewrite /Discrete. by setoid_rewrite Hxy. Qed.

Lemma dist_ltn m x y : x ≡{n}≡ y → m < n → x ≡{m}≡ y.
  Proof. eauto using dist_le, SIdx.lt_le_incl. Qed.

Lemma dist_le'n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y.
  Proof. eauto using dist_le. Qed.

Lemma dist_Sn x y : x ≡{Sᵢ n}≡ y → x ≡{n}≡ y.
  Proof. intros H. eapply dist_lt; eauto using SIdx.lt_succ_diag_r. Qed.

Local Instancesof [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.

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.

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.

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.

Lemma discrete_iffn 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.

Lemma discrete_iff_0n x y `{!TCOr (Discrete x) (Discrete y)} :
    x ≡{0ᵢ}≡ y ↔ x ≡{n}≡ y.
  Proof. by rewrite -!discrete_iff. Qed.

Lemma discreten x y `{!TCOr (Discrete x) (Discrete y)} :
    x ≡{n}≡ y → x ≡ y.
  Proof. intros. eapply discrete_iff; done. Qed.

Global Instanceofe_discrete_subrelation `{!OfeDiscrete A} n :
    @SolveProperSubrelation A (dist n) (≡).
  Proof. intros ???. apply: discrete. done. Qed.

Global Instanceofe_leibniz_subrelation `{!OfeDiscrete A, !LeibnizEquiv A} n :
    @SolveProperSubrelation A (dist n) (=).
  Proof. intros ?? EQ. unfold_leibniz. apply (is_solve_proper_subrelation EQ). Qed.

Record dist_later{SI : sidx} `{!Dist A} (n : SI) (x y : A) : Prop :=
  { dist_later_lt : ∀ m, m < n → x ≡{m}≡ y }.

Global Instancedist_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.

Lemma dist_dist_latern x y : dist n x y → dist_later n x y.
  Proof. intros. split; eauto using dist_lt. Qed.

Lemma dist_later_dist_ltn m (x y : A) : m < n → dist_later n x y → dist m x y.
  Proof. intros ? H; by apply H. Qed.

Lemma dist_later_0x y : dist_later 0ᵢ x y.
  Proof. split. intros ? []%SIdx.nlt_0_r. Qed.

Lemma dist_later_Sn 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.

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.

Notation Contractivef := (∀ n, Proper (dist_later n ==> dist n) f).

Global Instanceconst_contractive {SI : sidx} {A B : ofe} (x : A) :
  Contractive (@const A B x).
Proof. by intros n y1 y2. Qed.

Local SetDefault Proof Using "Type*".
  Context {SI : sidx} {A B : ofe} (f : A → B) `{!Contractive f}.
  Implicit Types x y : A.

Lemma contractive_0x y : f x ≡{0ᵢ}≡ f y.
  Proof. by apply (_ : Contractive f), dist_later_0. Qed.

Lemma contractive_dist_later_distn x y : dist_later n x y → f x ≡{n}≡ f y.
  Proof. by apply (_ : Contractive f). Qed.

Lemma contractive_Sn x y : x ≡{n}≡ y → f x ≡{Sᵢ n}≡ f y.
  Proof. intros. by apply contractive_dist_later_dist, dist_later_S. Qed.

Global Instancecontractive_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.

Global Instancecontractive_proper : Proper ((≡) ==> (≡)) f | 100.
  Proof. apply (ne_proper _). Qed.

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.

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.

Ltac solve_contractive:=
  solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]).

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);
}.

Global HintMode LimitPreserving - + + ! : typeclass_instances.

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.

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.

Global Instancelimit_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.

Lemma limit_preserving_discreteP :
    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.

Lemma limit_preserving_andP1 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.

Lemma limit_preserving_implP1 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.

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.

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.

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.

Definition bcompl: BCompl A := λ n c,
    match SIdx.case n with
    | inl (inl Hn') => inhabitant

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.

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.

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.

Record bfchainn := {
    bfchain_car :> bchain A n;
    bfchain_fixpoint p :
      p < n → f (bcompl n bfchain_car) ≡{p}≡ bcompl n bfchain_car;
  }.

Local Lemmabfchain_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.

Local ProgramDefinition 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.
  Next Obligation.
    intros n rec p Hp; simpl. rewrite (conv_bcompl _ _ Hp) /=.
    apply (contractive_dist_later_dist _); split=> p' Hp'. by apply rec.
  Qed.

Local Definitionfixpoint_bchain n : bfchain n :=
    Fix SIdx.lt_wf bfchain fixpoint_bchain_go n.

Local ProgramDefinition 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.

Local Definitionfixpoint_def : A := compl fixpoint_chain.

Local Definitionfixpoint_aux : seal (@fixpoint_def).
  Proof using Type. by eexists. Qed.

Definition fixpoint:= fixpoint_aux.(unseal).

Local Definitionfixpoint_unseal :
    @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).

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.

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.

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.

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.

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.

Definition fixpointK{SI : sidx} `{!Cofe A, !Inhabited A} k (f : A → A)
  `{!Contractive (Nat.iter k f)} := fixpoint (Nat.iter k f).

Local SetDefault Proof Using "Type*".
  Context {SI : sidx} {A : ofe} `{!Cofe A, !Inhabited A} (f : A → A) (k : nat).
  Context {f_contractive : Contractive (Nat.iter k f)} {f_ne : NonExpansive f}.

Local ExistingInstance f_proper.

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.

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.

Lemma fixpointK_nen : (∀ 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.

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.

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.

Local Definitionfixpoint_AB (x : A) : B := fixpoint (fB x).

Local Instancefixpoint_AB_contractive : Contractive fixpoint_AB.
  Proof.
    intros n x x' Hx; rewrite /fixpoint_AB.
    apply fixpoint_ne=> y. by f_contractive.
  Qed.

Local Definitionfixpoint_AA (x : A) : A := fA x (fixpoint_AB x).

Local Instancefixpoint_AA_contractive : Contractive fixpoint_AA.
  Proof using fA_contractive. solve_contractive. Qed.

Definition fixpoint_A: A := fixpoint fixpoint_AA.

Definition fixpoint_B: B := fixpoint_AB fixpoint_A.

Lemma fixpoint_A_unfold: fA fixpoint_A fixpoint_B ≡ fixpoint_A.
  Proof. by rewrite {2}/fixpoint_A (fixpoint_unfold _). Qed.

Lemma fixpoint_B_unfold: fB fixpoint_A fixpoint_B ≡ fixpoint_B.
  Proof. by rewrite {2}/fixpoint_B /fixpoint_AB (fixpoint_unfold _). Qed.

Local Instance: Proper ((≡) ==> (≡) ==> (≡)) fA.
  Proof using fA_contractive.
    apply ne_proper_2=> n x x' ? y y' ?. f_contractive; eauto using dist_lt.
  Qed.

Local Instance: Proper ((≡) ==> (≡) ==> (≡)) fB.
  Proof using fB_contractive.
    apply ne_proper_2=> n x x' ? y y' ?. f_contractive; eauto using dist_lt.
  Qed.

Lemma fixpoint_A_uniquep 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.

Lemma fixpoint_B_uniquep q : fA p q ≡ p → fB p q ≡ q → q ≡ fixpoint_B.
  Proof. intros. apply fixpoint_unique. by rewrite -fixpoint_A_unique. Qed.

Lemma fixpoint_A_nen :
    (∀ 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.

Lemma fixpoint_B_nen :
    (∀ 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.

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.

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.

Record ofe_mor{SI : sidx} (A B : ofe) : Type := OfeMor {
  ofe_mor_car :> A → B;
  ofe_mor_ne : NonExpansive ofe_mor_car
}.

Global ArgumentsOfeMor {_ _ _} _ {_}.
Add Printing Constructor ofe_mor.

Global ExistingInstance ofe_mor_ne.

Global Instanceofe_mor_proper (f : ofe_mor A B) : Proper ((≡) ==> (≡)) f.
  Proof. apply ne_proper, ofe_mor_ne. Qed.

Local Instanceofe_mor_equiv : Equiv (ofe_mor A B) := λ f g, ∀ x, f x ≡ g x.

Local Instanceofe_mor_dist : Dist (ofe_mor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.

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.
  Canonical Structure ofe_morO := Ofe (ofe_mor A B) ofe_mor_ofe_mixin.

Program Definitionofe_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.

Program Definitionofe_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.

Program Definitionofe_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.

Program Definitionofe_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.

Global ProgramInstance 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.
  Next Obligation.
    intros ? n Hn m Hm H x; simpl. rewrite (conv_lbcompl Hn) //=.
  Qed.
  Next Obligation.
    intros ? n Hn c1 c2 m Hc x; simpl. apply lbcompl_ne=> p Hp. apply Hc.
  Qed.

Global Instanceofe_mor_car_ne : NonExpansive2 (@ofe_mor_car SI A B).
  Proof. intros n f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.

Global Instanceofe_mor_car_proper :
    Proper ((≡) ==> (≡) ==> (≡)) (@ofe_mor_car SI A B) := ne_proper_2 _.

Lemma ofe_mor_ext(f g : ofe_mor A B) : f ≡ g ↔ ∀ x, f x ≡ g x.
  Proof. done. Qed.

Global Argumentsofe_morO {_} _ _.

Global Instanceofe_mor_inhabited {SI : sidx} {A B : ofe} `{Inhabited B} :
  Inhabited (A -n> B) := populate (λne _, inhabitant).

Definition cid{SI : sidx} {A: ofe} : A -n> A := OfeMor id.

Global Instance: Params (@cid) 2 := {}.

Definition cconst{SI : sidx} {A B : ofe} (x : B) : A -n> B := OfeMor (const x).

Global Instance: Params (@cconst) 3 := {}.

Definition ccompose{SI : sidx} {A B C: ofe}
  (f : B -n> C) (g : A -n> B) : A -n> C := OfeMor (f ∘ g).

Global Instance: Params (@ccompose) 4 := {}.
Infix "◎" := ccompose (at level 40, left associativity).

Global Instanceccompose_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.

Global Instanceccompose_proper {SI : sidx} {A B C: ofe} :
  Proper ((≡) ==> (≡) ==> (≡)) (@ccompose SI A B C).
Proof. apply ne_proper_2; apply _. Qed.

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.

Global Instanceofe_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.

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).

Global Instanceofe_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.

Local Instanceunit_dist : Dist unit := λ _ _ _, True.

Definition unit_ofe_mixin: OfeMixin unit.
  Proof. repeat split. Qed.
  Canonical Structure unitO : ofe := Ofe unit unit_ofe_mixin.

Global ProgramInstance unit_cofe : Cofe unitO :=
    { compl x := (); lbcompl _ _ _ := () }.
  Solve All Obligations with by repeat split.

Global Instanceunit_ofe_discrete : OfeDiscrete unitO.
  Proof. done. Qed.

Local InstanceEmpty_set_dist : Dist Empty_set := λ _ _ _, True.

Definition Empty_set_ofe_mixin: OfeMixin Empty_set.
  Proof. by repeat split. Qed.
  Canonical Structure Empty_setO : ofe := Ofe Empty_set Empty_set_ofe_mixin.

Global ProgramInstance Empty_set_cofe : Cofe Empty_setO :=
    {| compl c := c 0ᵢ; lbcompl n Hn c := c _ (SIdx.limit_lt_0 _ Hn) |}.
  Solve All Obligations with done.

Global InstanceEmpty_set_ofe_discrete : OfeDiscrete Empty_setO.
  Proof. done. Qed.

Local Instanceprod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).

Global Instancepair_ne :
    NonExpansive2 (@pair A B) := _.

Global Instancefst_ne : NonExpansive (@fst A B) := _.

Global Instancesnd_ne : NonExpansive (@snd A B) := _.

Definition prod_ofe_mixin: OfeMixin (A * B).
  Proof.
    split.
    - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
      rewrite !equiv_dist; naive_solver.
    - apply _.
    - by intros n m [x1 y1] [x2 y2] [??]; split; eapply dist_le.
  Qed.
  Canonical Structure prodO : ofe := Ofe (A * B) prod_ofe_mixin.

Global ProgramInstance prod_cofe `{!Cofe A, !Cofe B} : Cofe prodO := {
    compl c := (compl (chain_map fst c), compl (chain_map snd c));
    lbcompl n Hn c := (lbcompl Hn (bchain_map fst c), lbcompl Hn (bchain_map snd c))
  }.
  Next Obligation. split; simpl; rewrite conv_compl //. Qed.
  Next Obligation. split; simpl; rewrite conv_lbcompl //=. Qed.
  Next Obligation. split; simpl; apply lbcompl_ne=> ?? /=; f_equiv; auto. Qed.

Global Instanceprod_discrete (x : A * B) :
    Discrete (x.1) → Discrete (x.2) → Discrete x.
  Proof. by intros ???[??]; split; apply (discrete_0 _). Qed.

Global Instanceprod_ofe_discrete :
    OfeDiscrete A → OfeDiscrete B → OfeDiscrete prodO.
  Proof. intros ?? [??]; apply _. Qed.

Lemma pair_distn (a1 a2 : A) (b1 b2 : B) :
    (a1, b1) ≡{n}≡ (a2, b2) ↔ a1 ≡{n}≡ a2 ∧ b1 ≡{n}≡ b2.
  Proof. reflexivity. Qed.

Global ArgumentsprodO {_} _ _.

Global Instancepair_dist_inj {SI : sidx} {A B : ofe} n :
  Inj2 (≡{n}≡) (≡{n}≡) (≡{n}≡) (@pair A B) := _.

Global Instancecurry_ne {SI : sidx} {A B C : ofe} n :
  Proper (((≡{n}@{A*B}≡) ==> (≡{n}@{C}≡)) ==>
          (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) curry := _.

Global Instanceuncurry_ne {SI : sidx} {A B C : ofe} n :
  Proper (((≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) ==>
          (≡{n}@{A*B}≡) ==> (≡{n}@{C}≡)) uncurry := _.

Global Instancecurry3_ne {SI : sidx} {A B C D : ofe} n :
  Proper (((≡{n}@{A*B*C}≡) ==> (≡{n}@{D}≡)) ==>
          (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) curry3 := _.

Global Instanceuncurry3_ne {SI : sidx} {A B C D : ofe} n :
  Proper (((≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) ==>
          (≡{n}@{A*B*C}≡) ==> (≡{n}@{D}≡)) uncurry3 := _.

Global Instancecurry4_ne {SI : sidx} {A B C D E : ofe} n :
  Proper (((≡{n}@{A*B*C*D}≡) ==> (≡{n}@{E}≡)) ==>
          (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) curry4 := _.

Global Instanceuncurry4_ne {SI : sidx} {A B C D E : ofe} n :
  Proper (((≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) ==>
          (≡{n}@{A*B*C*D}≡) ==> (≡{n}@{E}≡)) uncurry4 := _.

Global TypeclassesOpaque prod_dist.

Global Instanceprod_map_ne {SI : sidx} {A A' B B' : ofe} n :
  Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
           dist n ==> dist n) (@prod_map A A' B B').
Proof. by intros f f' Hf g g' Hg ?? [??]; split; [apply Hf|apply Hg]. Qed.

Definition prodO_map{SI : sidx} {A A' B B'} (f : A -n> A') (g : B -n> B') :
  prodO A B -n> prodO A' B' := OfeMor (prod_map f g).

Global InstanceprodO_map_ne {SI : sidx} {A A' B B'} :
  NonExpansive2 (@prodO_map SI A A' B B').
Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.

Record oFunctor{SI : sidx} := OFunctor {
  oFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ofe;
  oFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    ((A2 -n> A1) * (B1 -n> B2)) → oFunctor_car A1 B1 -n> oFunctor_car A2 B2;
  oFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    NonExpansive (@oFunctor_map A1 _ A2 _ B1 _ B2 _);
  oFunctor_map_id `{!Cofe A, !Cofe B} (x : oFunctor_car A B) :
    oFunctor_map (cid,cid) x ≡ x;
  oFunctor_map_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
    oFunctor_map (f◎g, g'◎f') x ≡ oFunctor_map (g,g') (oFunctor_map (f,f') x)
}.

Global ExistingInstance oFunctor_map_ne.

Global Instance: Params (@oFunctor_map) 10 := {}.
Declare Scope oFunctor_scope.
Delimit Scope oFunctor_scope with OF.
Bind Scope oFunctor_scope with oFunctor.

Class oFunctorContractive{SI : sidx} (F : oFunctor) :=
  #[global] oFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} ::
    Contractive (@oFunctor_map SI F A1 _ A2 _ B1 _ B2 _).

Global HintMode oFunctorContractive - ! : typeclass_instances.

Definition oFunctor_apply{SI : sidx} (F : oFunctor) (A : ofe) `{!Cofe A} : ofe :=
  oFunctor_car F A A.

Program DefinitionoFunctor_oFunctor_compose {SI : sidx} (F1 F2 : oFunctor)
  `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} : oFunctor := {|
  oFunctor_car A _ B _ := oFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ 'fg :=
    oFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
|}.
Next Obligation.
  intros SI F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
  apply oFunctor_map_ne; split; apply oFunctor_map_ne; by split.
Qed.
Next Obligation.
  intros SI F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(oFunctor_map_id F1 x).
  apply equiv_dist=> n. apply oFunctor_map_ne.
  split=> y /=; by rewrite !oFunctor_map_id.
Qed.
Next Obligation.
  intros SI F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
  rewrite -oFunctor_map_compose. apply equiv_dist=> n. apply oFunctor_map_ne.
  split=> y /=; by rewrite !oFunctor_map_compose.
Qed.

Global InstanceoFunctor_oFunctor_compose_contractive_1 {SI : sidx} (F1 F2 : oFunctor)
    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
  oFunctorContractive F1 → oFunctorContractive (oFunctor_oFunctor_compose F1 F2).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
  f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
Qed.

Global InstanceoFunctor_oFunctor_compose_contractive_2 {SI : sidx} (F1 F2 : oFunctor)
    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
  oFunctorContractive F2 → oFunctorContractive (oFunctor_oFunctor_compose F1 F2).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
  f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
Qed.

Program DefinitionconstOF {SI : sidx} (B : ofe) : oFunctor :=
  {| oFunctor_car A1 A2 _ _ := B; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
Solve Obligations with done.

Coercion constOF: ofe >-> oFunctor.

Global InstanceconstOF_contractive {SI : sidx} B : oFunctorContractive (constOF B).
Proof. rewrite /oFunctorContractive; apply _. Qed.

Program DefinitionidOF {SI : sidx} : oFunctor :=
  {| oFunctor_car A1 _ A2 _ := A2; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := f.2 |}.
Solve Obligations with done.

Program DefinitionprodOF {SI : sidx} (F1 F2 : oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := prodO (oFunctor_car F1 A B) (oFunctor_car F2 A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    prodO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
|}.
Next Obligation.
  intros ??? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodO_map_ne; apply oFunctor_map_ne.
Qed.
Next Obligation. by intros ? F1 F2 A ? B ? [??]; rewrite /= !oFunctor_map_id. Qed.
Next Obligation.
  intros ? F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
  by rewrite !oFunctor_map_compose.
Qed.

Global InstanceprodOF_contractive {SI : sidx} F1 F2 :
  oFunctorContractive F1 → oFunctorContractive F2 →
  oFunctorContractive (prodOF F1 F2).
Proof.
  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
    by apply prodO_map_ne; apply oFunctor_map_contractive.
Qed.

Program Definitionofe_morOF {SI : sidx} (F1 F2 : oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := oFunctor_car F1 B A -n> oFunctor_car F2 A B;
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    ofe_morO_map (oFunctor_map F1 (fg.2, fg.1)) (oFunctor_map F2 fg)
|}.
Next Obligation.
  intros ? F1 F2 A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
  apply ofe_morO_map_ne; apply oFunctor_map_ne; split; by apply Hfg.
Qed.
Next Obligation.
  intros ? F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !oFunctor_map_id.
  apply (ne_proper f). apply oFunctor_map_id.
Qed.
Next Obligation.
  intros ? F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [h ?] ?; simpl in *.
  rewrite -!oFunctor_map_compose. do 2 apply (ne_proper _). apply oFunctor_map_compose.
Qed.

Global Instanceofe_morOF_contractive {SI : sidx} F1 F2 :
  oFunctorContractive F1 → oFunctorContractive F2 →
  oFunctorContractive (ofe_morOF F1 F2).
Proof.
  intros ?? A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
  apply ofe_morO_map_ne; apply oFunctor_map_contractive;
    split; intros m Hlt; split; simpl.
  all: destruct Hfg as [Hfg]; destruct (Hfg m); auto.
Qed.

Local Instancesum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n).

Global Instanceinl_ne : NonExpansive (@inl A B) := _.

Global Instanceinr_ne : NonExpansive (@inr A B) := _.

Global Instanceinl_ne_inj n : Inj (dist n) (dist n) (@inl A B) := _.

Global Instanceinr_ne_inj n : Inj (dist n) (dist n) (@inr A B) := _.

Definition sum_ofe_mixin: OfeMixin (A + B).
  Proof.
    split.
    - intros x y; split=> Hx.
      + destruct Hx=> n; constructor; by apply equiv_dist.
      + destruct (Hx 0ᵢ); constructor; apply equiv_dist=> n; by apply (inj _).
    - apply _.
    - destruct 1; constructor; eapply dist_le; eauto.
  Qed.
  Canonical Structure sumO : ofe := Ofe (A + B) sum_ofe_mixin.

Program Definitioninl_chain (c : chain sumO) (a : A) : chain A :=
    {| chain_car n := match c n return _ with inl a' => a' | _ => a end |}.
  Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.

Program Definitioninr_chain (c : chain sumO) (b : B) : chain B :=
    {| chain_car n := match c n return _ with inr b' => b' | _ => b end |}.
  Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.

Definition sum_compl`{!Cofe A, !Cofe B} : Compl sumO := λ c,
    match c 0ᵢ with
    | inl a => inl (compl (inl_chain c a))
    | inr b => inr (compl (inr_chain c b))
    end.

Program Definitioninl_bchain {n} (c : bchain sumO n) (a : A) : bchain A n :=
    {| bchain_car n Hn := match c n Hn return _ with inl a' => a' | _ => a end |}.
  Next Obligation.
    intros n c a m p Hm Hp Hmp; simpl.
    by destruct (bchain_cauchy n c m p Hm Hp Hmp).
  Qed.

Program Definitioninr_bchain {n} (c : bchain sumO n) (b : B) : bchain B n :=
    {| bchain_car n Hn := match c n Hn return _ with inr b' => b' | _ => b end |}.
  Next Obligation.
    intros n c b m p Hm Hp Hmp; simpl.
    by destruct (bchain_cauchy n c m p Hm Hp Hmp).
  Qed.

Definition sum_lbcompl`{!Cofe A, !Cofe B} : LBCompl sumO := λ n Hn c,
    match c 0ᵢ (SIdx.limit_lt_0 _ Hn) with
    | inl a => inl (lbcompl Hn (inl_bchain c a))
    | inr b => inr (lbcompl Hn (inr_bchain c b))
    end.

Global ProgramInstance sum_cofe `{!Cofe A, !Cofe B} : Cofe sumO :=
    { compl := sum_compl; lbcompl := sum_lbcompl }.
  Next Obligation.
    intros ?? n c; rewrite /compl /sum_compl.
    oinversion (chain_cauchy c 0ᵢ n); first apply SIdx.le_0_l.
    - rewrite (conv_compl n (inl_chain c _)) /=. destruct (c n); naive_solver.
    - rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver.
  Qed.
  Next Obligation.
    intros ?? n Hn c m Hm; rewrite /sum_lbcompl.
    oinversion (bchain_cauchy n c 0ᵢ m (SIdx.limit_lt_0 _ Hn) Hm);
      first apply SIdx.le_0_l.
    - rewrite (conv_lbcompl Hn _ Hm) /=. destruct (c m _); naive_solver.
    - rewrite (conv_lbcompl Hn _ Hm) /=. destruct (c m _); naive_solver.
  Qed.
  Next Obligation.
    intros ?? n Hn c1 c2 m Hc. rewrite /sum_lbcompl.
    destruct (Hc 0ᵢ (SIdx.limit_lt_0 _ Hn));
      rewrite /= lbcompl_ne //=; intros p Hp; by destruct (Hc p Hp).
  Qed.

Global Instanceinl_discrete (x : A) : Discrete x → Discrete (inl x).
  Proof. inversion_clear 2; constructor; by apply (discrete_0 _). Qed.

Global Instanceinr_discrete (y : B) : Discrete y → Discrete (inr y).
  Proof. inversion_clear 2; constructor; by apply (discrete_0 _). Qed.

Global Instancesum_ofe_discrete :
    OfeDiscrete A → OfeDiscrete B → OfeDiscrete sumO.
  Proof. intros ?? [?|?]; apply _. Qed.

Global ArgumentssumO {_} _ _.

Global TypeclassesOpaque sum_dist.

Global Instancesum_map_ne {SI : sidx} {A A' B B' : ofe} n :
  Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
           dist n ==> dist n) (@sum_map A A' B B').
Proof.
  intros f f' Hf g g' Hg ??; destruct 1; constructor; [by apply Hf|by apply Hg].
Qed.

Definition sumO_map{SI : sidx} {A A' B B'} (f : A -n> A') (g : B -n> B') :
  sumO A B -n> sumO A' B' := OfeMor (sum_map f g).

Global InstancesumO_map_ne {SI : sidx} {A A' B B'} :
  NonExpansive2 (@sumO_map SI A A' B B').
Proof. intros n f f' Hf g g' Hg [?|?]; constructor; [apply Hf|apply Hg]. Qed.

Program DefinitionsumOF {SI : sidx} (F1 F2 : oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := sumO (oFunctor_car F1 A B) (oFunctor_car F2 A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    sumO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
|}.
Next Obligation.
  intros ??? A1 ? A2 ? B1 ? B2 ? n ???;
    by apply sumO_map_ne; apply oFunctor_map_ne.
Qed.
Next Obligation.
  by intros ? F1 F2 A ? B ? [?|?]; rewrite /= !oFunctor_map_id.
Qed.
Next Obligation.
  intros ? F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [?|?]; simpl;
    by rewrite !oFunctor_map_compose.
Qed.

Global InstancesumOF_contractive {SI : sidx} F1 F2 :
  oFunctorContractive F1 → oFunctorContractive F2 →
  oFunctorContractive (sumOF F1 F2).
Proof.
  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
    by apply sumO_map_ne; apply oFunctor_map_contractive.
Qed.

Local Instancediscrete_dist : Dist A := λ n x y, x ≡ y.

Definition discrete_ofe_mixin: OfeMixin A.
  Proof using Type*.
    split.
    - intros x y; split; [done|intros Hn; apply (Hn 0ᵢ)].
    - done.
    - done.
  Qed.

Global Instancediscrete_ofe_discrete : OfeDiscrete (Ofe A discrete_ofe_mixin).
  Proof. by intros x y. Qed.

Global ProgramInstance discrete_cofe : Cofe (Ofe A discrete_ofe_mixin) :=
    { compl c := c 0ᵢ; lbcompl n Hn c := c _ (SIdx.limit_lt_0 _ Hn) }.
  Next Obligation.
    intros n c; simpl. symmetry. apply (chain_cauchy c 0ᵢ n), SIdx.le_0_l.
  Qed.
  Next Obligation.
    intros n Hn c m Hm; simpl.
    symmetry; apply (bchain_cauchy n c 0ᵢ m), SIdx.le_0_l.
  Qed.
  Next Obligation. simpl; eauto. Qed.

Notation discreteOA := (Ofe A (discrete_ofe_mixin _)).

Notation leibnizOA := (Ofe A (@discrete_ofe_mixin _ _ equivL eq_equivalence)).

Notation discrete_ofe_equivalence_ofA := ltac:(
  match constr:(ofe_mixin_of A) with
  | discrete_ofe_mixin ?H => exact H
  end) (only parsing).

Global InstanceleibnizO_leibniz {SI : sidx} A  : LeibnizEquiv (leibnizO A).
Proof. by intros x y. Qed.

Local InstanceProp_equiv : Equiv Prop := iff.

Local InstanceProp_equivalence : Equivalence (≡@{Prop}) := _.
  Canonical Structure PropO := discreteO Prop.

Local Instanceoption_dist : Dist (option A) := λ n, option_Forall2 (dist n).

Lemma option_dist_Forall2n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
  Proof. done. Qed.

Definition option_ofe_mixin: OfeMixin (option A).
  Proof.
    split.
    - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
      intros Hxy; destruct (Hxy 0ᵢ); constructor; apply equiv_dist.
      by intros n; oinversion (Hxy n).
    - apply _.
    - destruct 1; constructor; by eapply dist_le.
  Qed.
  Canonical Structure optionO := Ofe (option A) option_ofe_mixin.

Global InstanceSome_ne : NonExpansive (@Some A).
  Proof. intros ????. by econstructor. Qed.

Global InstanceSome_dist_inj n : Inj (dist n) (dist n) (@Some A).
  Proof. by inversion_clear 1. Qed.

Program Definitionoption_chain (c : chain optionO) (x : A) : chain A :=
    {| chain_car n := default x (c n) |}.
  Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.

Definition option_compl`{!Cofe A} : Compl optionO := λ c,
    match c 0ᵢ with Some x => Some (compl (option_chain c x)) | None => None end.

Program Definitionoption_bchain n (c : bchain optionO n) (x : A) : bchain A n :=
    {| bchain_car n Hn := default x (c n Hn) |}.
  Next Obligation.
    intros n c x m p Hm Hp Hmp; simpl.
    by destruct (bchain_cauchy n c m p Hm Hp Hmp).
  Qed.

Definition option_lbcompl`{!Cofe A} : LBCompl optionO := λ n Hn c,
    match c _ (SIdx.limit_lt_0 _ Hn) with
    | Some x => Some (lbcompl Hn (option_bchain n c x))
    | None => None
    end.

Global ProgramInstance option_cofe `{!Cofe A} : Cofe optionO :=
    { compl := option_compl; lbcompl := option_lbcompl }.
  Next Obligation.
    intros ? n c. rewrite /compl /option_compl.
    oinversion (chain_cauchy c 0ᵢ n); [by apply SIdx.le_0_l|..]; f_equiv.
    rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver.
  Qed.
  Next Obligation.
    intros ? n Hn c m Hm. rewrite /lbcompl /option_lbcompl.
    oinversion (bchain_cauchy n c 0ᵢ m (SIdx.limit_lt_0 _ Hn) Hm);
      [by apply SIdx.le_0_l|..]; f_equiv.
    rewrite (conv_lbcompl _ _ Hm) /=. destruct (c m Hm); naive_solver.
  Qed.
  Next Obligation.
    intros ? n Hn c1 c2 m Hc. rewrite /lbcompl /option_lbcompl.
    destruct (Hc 0ᵢ (SIdx.limit_lt_0 _ Hn)); f_equiv.
    apply lbcompl_ne=> p Hp /=. by destruct (Hc p Hp).
  Qed.

Global Instanceoption_ofe_discrete : OfeDiscrete A → OfeDiscrete optionO.
  Proof. destruct 2; constructor; by apply (discrete_0 _). Qed.

Global Instanceis_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
  Proof. destruct 1; split; eauto. Qed.

Global Instancefrom_option_ne {B} (R : relation B) n :
    Proper ((dist (A:=A) n ==> R) ==> R ==> dist n ==> R) from_option.
  Proof. destruct 3; simpl; auto. Qed.

Global InstanceNone_discrete : Discrete (@None A).
  Proof. inversion_clear 1; constructor. Qed.

Global InstanceSome_discrete x : Discrete x → Discrete (Some x).
  Proof. by intros ?; inversion_clear 1; constructor; apply discrete_0. Qed.

Lemma dist_Nonen mx : mx ≡{n}≡ None ↔ mx = None.
  Proof. split; [by inversion_clear 1|by intros ->]. Qed.

Lemma dist_Somen x y : Some x ≡{n}≡ Some y ↔ x ≡{n}≡ y.
  Proof. split; [by inversion_clear 1 | by intros ->]. Qed.

Lemma dist_Some_inv_ln mx my x :
    mx ≡{n}≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡{n}≡ y.
  Proof. destruct 1; naive_solver. Qed.

Lemma dist_Some_inv_rn mx my y :
    mx ≡{n}≡ my → my = Some y → ∃ x, mx = Some x ∧ x ≡{n}≡ y.
  Proof. destruct 1; naive_solver. Qed.

Lemma dist_Some_inv_l'n my x : Some x ≡{n}≡ my → ∃ x', Some x' = my ∧ x ≡{n}≡ x'.
  Proof. intros ?%(dist_Some_inv_l _ _ _ x); naive_solver. Qed.

Lemma dist_Some_inv_r'n mx y : mx ≡{n}≡ Some y → ∃ y', mx = Some y' ∧ y ≡{n}≡ y'.
  Proof. intros ?%(dist_Some_inv_r _ _ _ y); naive_solver. Qed.

Global TypeclassesOpaque option_dist.

Global ArgumentsoptionO {_} _.

Global Instanceoption_fmap_ne {SI : sidx} {A B : ofe} n :
  Proper ((dist n ==> dist n) ==> (≡{n}@{option A}≡) ==> (≡{n}@{option B}≡)) fmap.
Proof. intros f f' Hf ?? []; constructor; auto. Qed.

Global Instanceoption_mbind_ne {SI : sidx} {A B : ofe} n :
  Proper ((dist n ==> dist n) ==> (≡{n}@{option A}≡) ==> (≡{n}@{option B}≡)) mbind.
Proof. destruct 2; simpl; auto. Qed.

Global Instanceoption_mjoin_ne {SI : sidx} {A : ofe} n :
  Proper (dist n ==> (≡{n}@{option A}≡)) mjoin.
Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.

Global Instanceoption_fmap_dist_inj {SI : sidx} {A B : ofe} (f : A → B) n :
  Inj (≡{n}≡) (≡{n}≡) f → Inj (≡{n}@{option A}≡) (≡{n}@{option B}≡) (fmap f).
Proof. apply option_fmap_inj. Qed.

Lemma fmap_Some_dist{SI : sidx}
    {A B : ofe} (f : A → B) (mx : option A) (y : B) n :
  f <$> mx ≡{n}≡ Some y ↔ ∃ x : A, mx = Some x ∧ y ≡{n}≡ f x.
Proof.
  split; [|by intros (x&->&->)].
  intros (?&?%fmap_Some&?)%dist_Some_inv_r'; naive_solver.
Qed.

Definition optionO_map{SI : sidx} {A B: ofe} (f : A -n> B) :
    optionO A -n> optionO B :=
  OfeMor (fmap f : optionO A → optionO B).

Global InstanceoptionO_map_ne {SI : sidx} (A B: ofe) :
  NonExpansive (@optionO_map SI A B).
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.

Program DefinitionoptionOF {SI : sidx} (F : oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := optionO (oFunctor_car F A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (oFunctor_map F fg)
|}.
Next Obligation.
  intros ? F A1 ? A2 ? B1 ? B2 ? n f g Hfg;
    by apply optionO_map_ne, oFunctor_map_ne.
Qed.
Next Obligation.
  intros ? F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
  apply option_fmap_equiv_ext=> y; apply oFunctor_map_id.
Qed.
Next Obligation.
  intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x.
  rewrite /= -option_fmap_compose.
  apply option_fmap_equiv_ext=> y; apply oFunctor_map_compose.
Qed.

Global InstanceoptionOF_contractive {SI : sidx} F :
  oFunctorContractive F → oFunctorContractive (optionOF F).
Proof.
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
    apply optionO_map_ne, oFunctor_map_contractive.
Qed.

Record later(A : Type) : Type := Next { later_car : A }.
Add Printing Constructor later.

Global ArgumentsNext {_} _.

Global Argumentslater_car {_} _.

Global Instance: Params (@Next) 1 := {}.

Local Instancelater_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.

Local Instancelater_dist : Dist (later A) := λ n x y,
    dist_later n (later_car x) (later_car y).

Definition later_ofe_mixin: OfeMixin (later A).
  Proof.
    split.
    - intros [x] [y]; unfold equiv, later_equiv; rewrite !equiv_dist.
      split; first by intros Hxy n; split; intros m Hm.
      intros H n. eapply (H (Sᵢ n)), SIdx.lt_succ_diag_r.
    - split; rewrite /dist /later_dist.
      + by intros [x].
      + by intros [x] [y].
      + by intros [x] [y] [z] ??; trans y.
    - intros n m [x] [y] Hxy ?; split; intros p Hp.
      by eapply Hxy, SIdx.lt_le_trans.
  Qed.
  Canonical Structure laterO : ofe := Ofe (later A) later_ofe_mixin.

Global InstanceNext_contractive : Contractive (@Next A).
  Proof. by intros n x y. Qed.

Global InstanceNext_inj n : Inj (dist_later n) (dist n) (@Next A).
  Proof. by intros x y H. Qed.

Lemma Next_uninjx : ∃ a, x ≡ Next a.
  Proof. by exists (later_car x). Qed.

Local Instancelater_car_anti_contractive n :
    Proper (dist n ==> dist_later n) later_car.
  Proof. move=> [x] [y] /= Hxy. done. Qed.

Program Definitionlater_chain (c : chain laterO) : chain A :=
    {| chain_car n := later_car (c (Sᵢ n)) |}.
  Next Obligation.
    intros c n i ?%SIdx.succ_le_mono.
    apply (chain_cauchy c (Sᵢ n)); eauto using SIdx.lt_succ_diag_r.
  Qed.

Program Definitionlater_limit_bchain {n} (c : bchain laterO n)
      (Hn : SIdx.limit n) : bchain A n :=
    {| bchain_car m Hm := later_car (c (Sᵢ m) _) |}.
  Next Obligation. intros n _ Hn. apply Hn. Qed.
  Next Obligation.
    intros n c Hn m p ???%SIdx.succ_le_mono; simpl.
    apply (bchain_cauchy n c (Sᵢ m) (Sᵢ p)); eauto using SIdx.lt_succ_diag_r.
  Qed.

Global ProgramInstance later_cofe `{!Cofe A} : Cofe laterO := {
    compl c := Next (compl (later_chain c));
    lbcompl n Hn c := Next (lbcompl Hn (later_limit_bchain c Hn))
  }.
  Next Obligation.
    intros ? n c; split; intros m Hm%SIdx.le_succ_l; simpl. rewrite conv_compl /=.
    symmetry; apply (chain_cauchy c (Sᵢ m) n); eauto using SIdx.lt_succ_diag_r.
  Qed.
  Next Obligation.
    intros ? n ? c m Hm; simpl; split; intros p Hp; simpl.
    rewrite (conv_lbcompl _ _ (transitivity Hp Hm)) /=.
    symmetry; eapply (bchain_cauchy n c (Sᵢ p)); eauto using SIdx.lt_succ_diag_r.
    by apply SIdx.le_succ_l.
  Qed.
  Next Obligation.
    intros ? n Hn c1 c2 m Hc; split; intros p Hp; simpl.
    apply lbcompl_ne=> q Hq; by apply Hc.
  Qed.

Lemma contractive_alt{B : ofe} (f : A → B) :
    Contractive f ↔ ∃ g : later A → B, NonExpansive g ∧ ∀ x, f x ≡ g (Next x).
  Proof.
    split.
    - intros Hf. exists (f ∘ later_car); split=> // n x y ?. by f_equiv.
    - intros (g&Hg&Hf) n x y Hxy. rewrite !Hf. by apply Hg.
  Qed.

Global ArgumentslaterO {_} _.

Definition later_map{A B} (f : A → B) (x : later A) : later B :=
  Next (f (later_car x)).

Global Instancelater_map_ne {SI : sidx} {A B : ofe} (f : A → B) n :
  Proper (dist_later n ==> dist_later n) f →
  Proper (dist n ==> dist n) (later_map f) | 0.
Proof.
  intros P [x] [y] H; rewrite /later_map //=.
  split; intros m Hm; apply P, Hm. apply H.
Qed.

Global Instancelater_map_ne' {SI : sidx} {A B : ofe} (f : A → B) :
  NonExpansive f → NonExpansive (later_map f).
Proof.
  intros ?? [x] [y] H. unfold later_map; simpl.
  split; intros ??; simpl. f_equiv. by apply H.
Qed.

Global Instancelater_map_proper {SI : sidx} {A B : ofe} (f : A → B) :
  Proper ((≡) ==> (≡)) f →
  Proper ((≡) ==> (≡)) (later_map f).
Proof. solve_proper. Qed.

Lemma later_map_Next{SI : sidx} {A B : ofe} (f : A → B) x :
  later_map f (Next x) = Next (f x).
Proof. done. Qed.

Lemma later_map_id{SI : sidx} {A} (x : later A) : later_map id x = x.
Proof. by destruct x. Qed.

Lemma later_map_compose{SI : sidx}
    {A B C} (f : A → B) (g : B → C) (x : later A) :
  later_map (g ∘ f) x = later_map g (later_map f x).
Proof. by destruct x. Qed.

Lemma later_map_ext{SI : sidx} {A B : ofe} (f g : A → B) x :
  (∀ x, f x ≡ g x) → later_map f x ≡ later_map g x.
Proof. destruct x; intros Hf; apply Hf. Qed.

Definition laterO_map{SI : sidx}
    {A B: ofe} (f : A -n> B) : laterO A -n> laterO B :=
  OfeMor (later_map f).

Global InstancelaterO_map_contractive {SI : sidx} (A B : ofe) :
  Contractive (@laterO_map SI A B).
Proof. intros n f g Hlater [x]; split; intros ??; simpl. by apply Hlater. Qed.

Program DefinitionlaterOF {SI : sidx} (F : oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := laterO (oFunctor_car F A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := laterO_map (oFunctor_map F fg)
|}.
Next Obligation.
  intros ? F A1 ? A2 ? B1 ? B2 ? n fg fg' ?.
  by apply (contractive_ne laterO_map), oFunctor_map_ne.
Qed.
Next Obligation.
  intros ? F A ? B ? x; simpl. rewrite -{2}(later_map_id x).
  apply later_map_ext=>y. by rewrite oFunctor_map_id.
Qed.
Next Obligation.
  intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -later_map_compose.
  apply later_map_ext=>y; apply oFunctor_map_compose.
Qed.

Global InstancelaterOF_contractive {SI : sidx} F : oFunctorContractive (laterOF F).
Proof.
  intros A1 ? A2 ? B1 ? B2 ? n fg fg' Hfg. apply laterO_map_contractive.
  split; intros ???; simpl. by eapply oFunctor_map_ne, Hfg.
Qed.

Definition discrete_fun{SI : sidx} {A} (B : A → ofe) := ∀ x : A, B x.

Local Instancediscrete_fun_equiv : Equiv (discrete_fun B) := λ f g, ∀ x, f x ≡ g x.

Local Instancediscrete_fun_dist : Dist (discrete_fun B) := λ n f g, ∀ x, f x ≡{n}≡ g x.

Definition discrete_fun_ofe_mixin: OfeMixin (discrete_fun 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 ? H x. by eapply dist_le.
  Qed.
  Canonical Structure discrete_funO := Ofe (discrete_fun B) discrete_fun_ofe_mixin.

Program Definitiondiscrete_fun_chain (c : chain discrete_funO)
    (x : A) : chain (B x) := {| chain_car n := c n x |}.
  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.

Program Definitiondiscrete_fun_bchain {n} (c : bchain discrete_funO n)
    (x : A) : bchain (B x) n := {| bchain_car n Hn := c n Hn x |}.
  Next Obligation. intros n c x m p Hm Hp Hmp. by apply (bchain_cauchy n c). Qed.

Global ProgramInstance discrete_fun_cofe `{!∀ x, Cofe (B x)} :
      Cofe discrete_funO := {
    compl c x := compl (discrete_fun_chain c x);
    lbcompl n Hn c x := lbcompl Hn (discrete_fun_bchain c x)
  }.
  Next Obligation. intros ? n c x. by apply conv_compl. Qed.
  Next Obligation. intros ? n Hn c m Hm x. by rewrite (conv_lbcompl _ _ Hm). Qed.
  Next Obligation.
    intros ? n Hn c1 c2 m Hc x. apply lbcompl_ne=> ?? /=. by apply Hc.
  Qed.

Global Instancediscrete_fun_lookup_discrete `{EqDecision A} f x :
    Discrete f → Discrete (f x).
  Proof.
    intros Hf y ?.
    set (g x' := if decide (x = x') is left H then eq_rect _ B y _ H else f x').
    trans (g x).
    { apply Hf=> x'. unfold g. by destruct (decide _) as [[]|]. }
    unfold g. destruct (decide _) as [Hx|]; last done.
    by rewrite (proof_irrel Hx eq_refl).
  Qed.

Global Argumentsdiscrete_funO {_ _} _.

Definition discrete_fun_map{SI : sidx} {A} {B1 B2 : A → ofe} (f : ∀ x, B1 x → B2 x)
  (g : discrete_fun B1) : discrete_fun B2 := λ x, f _ (g x).

Lemma discrete_fun_map_ext{SI : sidx} {A} {B1 B2 : A → ofe} (f1 f2 : ∀ x, B1 x → B2 x)
  (g : discrete_fun B1) :
  (∀ x, f1 x (g x) ≡ f2 x (g x)) → discrete_fun_map f1 g ≡ discrete_fun_map f2 g.
Proof. done. Qed.

Lemma discrete_fun_map_id{SI : sidx} {A} {B : A → ofe} (g : discrete_fun B) :
  discrete_fun_map (λ _, id) g = g.
Proof. done. Qed.

Lemma discrete_fun_map_compose{SI : sidx} {A} {B1 B2 B3 : A → ofe}
    (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : discrete_fun B1) :
  discrete_fun_map (λ x, f2 x ∘ f1 x) g = discrete_fun_map f2 (discrete_fun_map f1 g).
Proof. done. Qed.

Global Instancediscrete_fun_map_ne {SI : sidx} {A} {B1 B2 : A → ofe}
    (f : ∀ x, B1 x → B2 x) n :
  (∀ x, Proper (dist n ==> dist n) (f x)) →
  Proper (dist n ==> dist n) (discrete_fun_map f).
Proof. by intros ? y1 y2 Hy x; rewrite /discrete_fun_map (Hy x). Qed.

Definition discrete_funO_map{SI : sidx} {A} {B1 B2 : A → ofe}
    (f : discrete_fun (λ x, B1 x -n> B2 x)) :
  discrete_funO B1 -n> discrete_funO B2 := OfeMor (discrete_fun_map f).

Global Instancediscrete_funO_map_ne {SI : sidx} {A} {B1 B2 : A → ofe} :
  NonExpansive (@discrete_funO_map SI A B1 B2).
Proof. intros n f1 f2 Hf g x; apply Hf. Qed.

Program Definitiondiscrete_funOF {SI : sidx} {C} (F : C → oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := discrete_funO (λ c, oFunctor_car (F c) A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := discrete_funO_map (λ c, oFunctor_map (F c) fg)
|}.
Next Obligation.
  intros ? C F A1 ? A2 ? B1 ? B2 ? n ?? g.
  by apply discrete_funO_map_ne=>?; apply oFunctor_map_ne.
Qed.
Next Obligation.
  intros ? C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
  apply discrete_fun_map_ext=> y; apply oFunctor_map_id.
Qed.
Next Obligation.
  intros ? C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g.
  rewrite /= -discrete_fun_map_compose.
  apply discrete_fun_map_ext=>y; apply oFunctor_map_compose.
Qed.

Global Instancediscrete_funOF_contractive {SI : sidx} {C} (F : C → oFunctor) :
  (∀ c, oFunctorContractive (F c)) → oFunctorContractive (discrete_funOF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
  by apply discrete_funO_map_ne=>c; apply oFunctor_map_contractive.
Qed.

Lemma iso_ofe_mixin{SI : sidx}
  {A : ofe} {B : Type} `{!Equiv B, !Dist B} (g : B → A)
  (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
  (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2) : OfeMixin B.
Proof.
  split.
  - intros y1 y2. rewrite g_equiv. setoid_rewrite g_dist. apply equiv_dist.
  - split.
    + intros y. by apply g_dist.
    + intros y1 y2. by rewrite !g_dist.
    + intros y1 y2 y3. rewrite !g_dist. intros ??; etrans; eauto.
  - intros n m y1 y2. rewrite !g_dist. by eapply dist_le.
Qed.

Local ExistingInstance Hgne.
  Context (gf : ∀ x Hx, g (f x Hx) ≡ x).
  Context (Hlimit : ∀ c : chain B, P (compl (chain_map g c))).
  Context (Hblimit : ∀ n (Hn : SIdx.limit n) c, P (lbcompl Hn (bchain_map g c))).

Program Definitioniso_cofe_subtype : Cofe B := {|
    compl c := f (compl (chain_map g c)) _;
    lbcompl n Hn c := f (lbcompl Hn (bchain_map g c)) _
  |}.
  Next Obligation. apply Hlimit. Qed.
  Next Obligation. apply Hblimit. Qed.
  Next Obligation. intros n c; simpl. apply g_dist. by rewrite gf conv_compl. Qed.
  Next Obligation.
    intros n Hn c m Hm; simpl. apply g_dist. by rewrite gf (conv_lbcompl _ _ Hm).
  Qed.
  Next Obligation.
    intros n Hn c1 c2 m Hc; simpl. apply g_dist. rewrite !gf.
    apply lbcompl_ne=> ?? /=. by rewrite Hc.
  Qed.

Lemma iso_cofe_subtype'{SI : sidx} {A B : ofe} `{!Cofe A}
  (P : A → Prop) (f : ∀ x, P x → B) (g : B → A)
  (Pg : ∀ y, P (g y))
  (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
  (gf : ∀ x Hx, g (f x Hx) ≡ x)
  (Hlimit : LimitPreserving P) : Cofe B.
Proof. destruct Hlimit. apply: (iso_cofe_subtype P f g); eauto. Qed.

Definition iso_cofe{SI : sidx} {A B : ofe} `{!Cofe A} (f : A → B) (g : B → A)
  (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
  (gf : ∀ x, g (f x) ≡ x) : Cofe B.
Proof. by apply (iso_cofe_subtype (λ _, True) (λ x _, f x) g). Qed.

Local Instancesig_equiv : Equiv (sig P) := λ x1 x2, `x1 ≡ `x2.

Local Instancesig_dist : Dist (sig P) := λ n x1 x2, `x1 ≡{n}≡ `x2.

Definition sig_equiv_defx y : (x ≡ y) = (`x ≡ `y) := reflexivity _.

Definition sig_dist_defn x y : (x ≡{n}≡ y) = (`x ≡{n}≡ `y) := reflexivity _.

Lemma exist_nen a1 a2 (H1 : P a1) (H2 : P a2) :
    a1 ≡{n}≡ a2 → a1 ↾ H1 ≡{n}≡ a2 ↾ H2.
  Proof. done. Qed.

Global Instanceproj1_sig_ne : NonExpansive (@proj1_sig _ P).
  Proof. by intros n [a Ha] [b Hb] ?. Qed.

Definition sig_ofe_mixin: OfeMixin (sig P).
  Proof. by apply (iso_ofe_mixin proj1_sig). Qed.
  Canonical Structure sigO : ofe := Ofe (sig P) sig_ofe_mixin.

Global Instancesig_cofe `{!Cofe A, !LimitPreserving P} : Cofe sigO.
  Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig)=> //. by intros []. Qed.

Global Instancesig_discrete (x : sig P) :  Discrete (`x) → Discrete x.
  Proof. intros ? y. rewrite sig_dist_def sig_equiv_def. apply (discrete_0 _). Qed.

Global Instancesig_ofe_discrete : OfeDiscrete A → OfeDiscrete sigO.
  Proof. intros ??. apply _. Qed.

Global ArgumentssigO {_ _} _.

Local InstancesigT_dist : Dist (sigT P) := λ n x1 x2,
    ∃ Heq : projT1 x1 = projT1 x2, rew Heq in projT2 x1 ≡{n}≡ projT2 x2.

Local InstancesigT_equiv : Equiv (sigT P) := λ x1 x2,
    ∀ n, x1 ≡{n}≡ x2.

Definition sigT_equiv_eqx1 x2 : (x1 ≡ x2) ↔ ∀ n, x1 ≡{n}≡ x2 :=
      reflexivity _.

Definition sigT_dist_eqx1 x2 n : (x1 ≡{n}≡ x2) ↔
    ∃ Heq : projT1 x1 = projT1 x2, (rew Heq in projT2 x1) ≡{n}≡ projT2 x2 :=
      reflexivity _.

Definition sigT_dist_proj1n {x y} :
    x ≡{n}≡ y → projT1 x = projT1 y := proj1_ex.

Definition sigT_equiv_proj1{x y} :
    x ≡ y → projT1 x = projT1 y := λ H, proj1_ex (H 0ᵢ).

Definition sigT_ofe_mixin: OfeMixin (sigT P).
  Proof.
    split => // n.
    - split; hnf; setoid_rewrite sigT_dist_eq.
      + intros. by exists eq_refl.
      + move => [xa x] [ya y] /=. destruct 1 as [-> Heq].
        by exists eq_refl.
      + move => [xa x] [ya y] [za z] /=.
        destruct 1 as [-> Heq1].
        destruct 1 as [-> Heq2]. exists eq_refl => /=. by trans y.
    - setoid_rewrite sigT_dist_eq.
      move => m [xa x] [ya y] /=. destruct 1 as [-> Heq].
      exists eq_refl. eauto using dist_le.
  Qed.
  Canonical Structure sigTO : ofe := Ofe (sigT P) sigT_ofe_mixin.

Lemma sigT_equiv_eq_alt`{!∀ a b : A, ProofIrrel (a = b)} x1 x2 :
    x1 ≡ x2 ↔
    ∃ Heq : projT1 x1 = projT1 x2, rew Heq in projT2 x1 ≡ projT2 x2.
  Proof.
    setoid_rewrite equiv_dist. setoid_rewrite sigT_dist_eq. split => Heq.
    - move: (Heq 0ᵢ) => [H0eq1 _].
      exists H0eq1 => n. move: (Heq n) => [] Hneq1.
      by rewrite (proof_irrel H0eq1 Hneq1).
    - move: Heq => [Heq1 Heqn2] n. by exists Heq1.
  Qed.

Global InstanceprojT1_ne : NonExpansive (projT1 : sigTO → leibnizO A).
  Proof. solve_proper. Qed.

Global InstanceprojT1_proper : Proper ((≡) ==> (≡)) (projT1 : sigTO → leibnizO A).
  Proof. apply ne_proper, projT1_ne. Qed.

Lemma projT2_nen (x1 x2 : sigTO) (Heq : x1 ≡{n}≡ x2) :
    rew (sigT_dist_proj1 n Heq) in projT2 x1 ≡{n}≡ projT2 x2.
  Proof. by destruct Heq. Qed.

Lemma projT2_proper`{!∀ a b : A, ProofIrrel (a = b)} (x1 x2 : sigTO) (Heqs : x1 ≡ x2):
    rew (sigT_equiv_proj1 Heqs) in projT2 x1 ≡ projT2 x2.
  Proof.
    move: x1 x2 Heqs => [a1 x1] [a2 x2] Heqs.
    case: (proj1 (sigT_equiv_eq_alt _ _) Heqs) => /=. intros ->.
    rewrite (proof_irrel (sigT_equiv_proj1 Heqs) eq_refl) /=. done.
  Qed.

Lemma existT_nen {i1 i2} {v1 : P i1} {v2 : P i2} :
    ∀ (Heq : i1 = i2), (rew f_equal P Heq in v1 ≡{n}≡ v2) →
      existT i1 v1 ≡{n}≡ existT i2 v2.
  Proof. intros ->; simpl. exists eq_refl => /=. done. Qed.

Lemma existT_proper{i1 i2} {v1 : P i1} {v2 : P i2} :
    ∀ (Heq : i1 = i2), (rew f_equal P Heq in v1 ≡ v2) →
      existT i1 v1 ≡ existT i2 v2.
  Proof. intros Heq Heqv n. apply (existT_ne n Heq), equiv_dist, Heqv. Qed.

Global InstanceexistT_ne_2 a : NonExpansive (@existT A P a).
  Proof. move => ??? Heq. apply (existT_ne _ eq_refl Heq). Qed.

Global InstanceexistT_proper_2 a : Proper ((≡) ==> (≡)) (@existT A P a).
  Proof. apply ne_proper, _. Qed.
  Implicit Types c : chain sigTO.

Global InstancesigT_discrete x : Discrete (projT2 x) → Discrete x.
  Proof.
    move: x => [xa x] ? [ya y] [] /=; intros -> => /= Hxy n.
    exists eq_refl => /=. apply equiv_dist, (discrete_0 _), Hxy.
  Qed.

Global InstancesigT_ofe_discrete : (∀ a, OfeDiscrete (P a)) → OfeDiscrete sigTO.
  Proof. intros ??. apply _. Qed.

Lemma sigT_chain_const_proj1c n : projT1 (c n) = projT1 (c 0ᵢ).
  Proof.
    refine (sigT_dist_proj1 _ (chain_cauchy c 0ᵢ n _)). apply SIdx.le_0_l.
  Qed.

Lemma sigT_bchain_const_proj1n Hn (c: bchain sigTO n) m Hm :
    projT1 (c m Hm) = projT1 (c 0ᵢ Hn).
  Proof.
    refine (sigT_dist_proj1 _ (bchain_cauchy n c 0ᵢ m _ _ _)). apply SIdx.le_0_l.
  Qed.

Program Definitionchain_map_snd c : chain (P (projT1 (c 0ᵢ))) :=
      {| chain_car n := rew (sigT_chain_const_proj1 c n) in projT2 (c n) |}.
    Next Obligation.
      move => c n i Hle /=.

Definition sigT_compl: Compl sigTO := λ c,
      existT (projT1 (c 0ᵢ)) (compl (chain_map_snd c)).

Program Definitionbchain_map_snd n Hn (c : bchain sigTO n) :
        bchain (P (projT1 (c 0ᵢ Hn))) n :=
      {| bchain_car m Hm :=
        rew (sigT_bchain_const_proj1 n Hn c m Hm) in projT2 (c m Hm) |}.
    Next Obligation.
      move => n Hn c m p Hm Hp Hle /=.

Definition sigT_lbcompl: LBCompl sigTO := λ n Hn (c : bchain sigTO n),
      existT (projT1 (c _ (SIdx.limit_lt_0 _ Hn)))
             (lbcompl Hn (bchain_map_snd n (SIdx.limit_lt_0 _ Hn) c)).

Global ProgramInstance sigT_cofe : Cofe sigTO :=
      { compl := sigT_compl; lbcompl := sigT_lbcompl }.
    Next Obligation.
      intros n c. rewrite /sigT_compl sigT_dist_eq /=.
      exists (symmetry (sigT_chain_const_proj1 c n)).

Global ArgumentssigTO {_ _} _.

Program DefinitionsigT_map {P1 P2 : A → ofe} :
    discrete_funO (λ a, P1 a -n> P2 a) -n>
    sigTO P1 -n> sigTO P2 :=
    λne f xpx, existT _ (f _ (projT2 xpx)).
  Next Obligation.
    move => ?? f n [x px] [y py] [/= Heq]. destruct Heq; simpl.
    exists eq_refl => /=. by f_equiv.
  Qed.
  Next Obligation.
    move => ?? n f g Heq [x px] /=. exists eq_refl => /=. apply Heq.
  Qed.

Program DefinitionsigTOF (F : A → oFunctor) : oFunctor := {|
    oFunctor_car A CA B CB := sigTO (λ a, oFunctor_car (F a) A B);
    oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := sigT_map (λ a, oFunctor_map (F a) fg)
  |}.
  Next Obligation.
    repeat intro. exists eq_refl => /=. solve_proper.
  Qed.
  Next Obligation.
    simpl; intros. apply (existT_proper eq_refl), oFunctor_map_id.
  Qed.
  Next Obligation.
    simpl; intros. apply (existT_proper eq_refl), oFunctor_map_compose.
  Qed.

Global InstancesigTOF_contractive {F} :
    (∀ a, oFunctorContractive (F a)) → oFunctorContractive (sigTOF F).
  Proof.
    repeat intro. apply sigT_map => a. exact: oFunctor_map_contractive.
  Qed.

Global ArgumentssigTOF {_ _} _%_OF.

Record ofe_iso{SI : sidx} (A B : ofe) := OfeIso {
  ofe_iso_1 : A -n> B;
  ofe_iso_2 : B -n> A;
  ofe_iso_12 y : ofe_iso_1 (ofe_iso_2 y) ≡ y;
  ofe_iso_21 x : ofe_iso_2 (ofe_iso_1 x) ≡ x;
}.

Global ArgumentsOfeIso {_ _ _} _ _ _ _.

Global Argumentsofe_iso_1 {_ _ _} _.

Global Argumentsofe_iso_2 {_ _ _} _.

Global Argumentsofe_iso_12 {_ _ _} _ _.

Global Argumentsofe_iso_21 {_ _ _} _ _.

Local Instanceofe_iso_equiv : Equiv (ofe_iso A B) := λ I1 I2,
    ofe_iso_1 I1 ≡ ofe_iso_1 I2 ∧ ofe_iso_2 I1 ≡ ofe_iso_2 I2.

Local Instanceofe_iso_dist : Dist (ofe_iso A B) := λ n I1 I2,
    ofe_iso_1 I1 ≡{n}≡ ofe_iso_1 I2 ∧ ofe_iso_2 I1 ≡{n}≡ ofe_iso_2 I2.

Global Instanceofe_iso_1_ne : NonExpansive (ofe_iso_1 (A:=A) (B:=B)).
  Proof. by destruct 1. Qed.

Global Instanceofe_iso_2_ne : NonExpansive (ofe_iso_2 (A:=A) (B:=B)).
  Proof. by destruct 1. Qed.

Lemma ofe_iso_ofe_mixin: OfeMixin (ofe_iso A B).
  Proof. by apply (iso_ofe_mixin (λ I, (ofe_iso_1 I, ofe_iso_2 I))). Qed.
  Canonical Structure ofe_isoO : ofe := Ofe (ofe_iso A B) ofe_iso_ofe_mixin.

Global Instanceofe_iso_cofe `{!SIdxFinite SI}
    `{!Cofe A, !Cofe B} : Cofe ofe_isoO.
  Proof.
    apply (iso_cofe_subtype'
      (λ I : prodO (A -n> B) (B -n> A),
        (∀ y, I.1 (I.2 y) ≡ y) ∧ (∀ x, I.2 (I.1 x) ≡ x))
      (λ I HI, OfeIso (I.1) (I.2) (proj1 HI) (proj2 HI))
      (λ I, (ofe_iso_1 I, ofe_iso_2 I))); [by intros []|done..|].
    apply limit_preserving_and; apply limit_preserving_forall=> ?;
      apply limit_preserving_equiv; solve_proper.
  Qed.

Global Argumentsofe_isoO {_} _ _.

Program Definitioniso_ofe_refl {SI : sidx} {A: ofe} : ofe_iso A A :=
  OfeIso cid cid _ _.
Solve Obligations with done.

Definition iso_ofe_sym{SI : sidx} {A B : ofe} (I : ofe_iso A B) : ofe_iso B A :=
  OfeIso (ofe_iso_2 I) (ofe_iso_1 I) (ofe_iso_21 I) (ofe_iso_12 I).

Global Instanceiso_ofe_sym_ne {SI : sidx} {A B : ofe} :
  NonExpansive (iso_ofe_sym (A:=A) (B:=B)).
Proof. intros n I1 I2 []; split; simpl; by f_equiv. Qed.

Program Definitioniso_ofe_trans {SI : sidx} {A B C: ofe}
    (I : ofe_iso A B) (J : ofe_iso B C) : ofe_iso A C :=
  OfeIso (ofe_iso_1 J ◎ ofe_iso_1 I) (ofe_iso_2 I ◎ ofe_iso_2 J) _ _.
Next Obligation. intros ? A B C I J z; simpl. by rewrite !ofe_iso_12. Qed.
Next Obligation. intros ? A B C I J z; simpl. by rewrite !ofe_iso_21. Qed.

Global Instanceiso_ofe_trans_ne {SI : sidx} {A B C} :
  NonExpansive2 (iso_ofe_trans (A:=A) (B:=B) (C:=C)).
Proof. intros n I1 I2 [] J1 J2 []; split; simpl; by f_equiv. Qed.

Program Definitioniso_ofe_cong {SI : sidx} (F : oFunctor) `{!Cofe A, !Cofe B}
    (I : ofe_iso A B) : ofe_iso (oFunctor_apply F A) (oFunctor_apply F B) :=
  OfeIso (oFunctor_map F (ofe_iso_2 I, ofe_iso_1 I))
    (oFunctor_map F (ofe_iso_1 I, ofe_iso_2 I)) _ _.
Next Obligation.
  intros ? F A ? B ? I x. rewrite -oFunctor_map_compose -{2}(oFunctor_map_id F x).
  apply equiv_dist=> n.
  apply oFunctor_map_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
Qed.
Next Obligation.
  intros ? F A ? B ? I y. rewrite -oFunctor_map_compose -{2}(oFunctor_map_id F y).
  apply equiv_dist=> n.
  apply oFunctor_map_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
Qed.

Global Instanceiso_ofe_cong_ne {SI : sidx} (F : oFunctor) `{!Cofe A, !Cofe B} :
  NonExpansive (iso_ofe_cong F (A:=A) (B:=B)).
Proof. intros n I1 I2 []; split; simpl; by f_equiv. Qed.

Global Instanceiso_ofe_cong_contractive {SI : sidx}
    (F : oFunctor) `{!Cofe A, !Cofe B} :
  oFunctorContractive F → Contractive (iso_ofe_cong F (A:=A) (B:=B)).
Proof. intros ? n I1 I2 HI; split; simpl; f_contractive; by destruct HI. Qed.