phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/ofe.v *)
Instance pair_ne :
    NonExpansive2 (@pair A B)
:= _.
(* iris/algebra/ofe.v *)
Instance fst_ne : NonExpansive (@fst A B)
:= _.
(* iris/algebra/ofe.v *)
Instance snd_ne : NonExpansive (@snd A B)
:= _.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
Canonical prodO : ofe
:= Ofe (A * B) prod_ofe_mixin.
(* iris/algebra/ofe.v *)
Instance 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.
(* iris/algebra/ofe.v *)
Instance prod_discrete (x : A * B) :
    Discrete (x.1) → Discrete (x.2) → Discrete x.
Proof. by intros ???[??]; split; apply (discrete_0 _). Qed.
(* iris/algebra/ofe.v *)
Instance prod_ofe_discrete :
    OfeDiscrete A → OfeDiscrete B → OfeDiscrete prodO.
Proof. intros ?? [??]; apply _. Qed.
(* iris/algebra/ofe.v *)
Lemma pair_dist n (a1 a2 : A) (b1 b2 : B) :
    (a1, b1) ≡{n}≡ (a2, b2) ↔ a1 ≡{n}≡ a2 ∧ b1 ≡{n}≡ b2.
Proof. reflexivity. Qed.
(* iris/algebra/ofe.v *)
(* Below we make [prod_dist] type class opaque, so we first lift all
instances *)
Instance pair_dist_inj {SI : sidx} {A B : ofe} n :
  Inj2 (≡{n}≡) (≡{n}≡) (≡{n}≡) (@pair A B)
:= _.
(* iris/algebra/ofe.v *)
Instance curry_ne {SI : sidx} {A B C : ofe} n :
  Proper (((≡{n}@{A*B}≡) ==> (≡{n}@{C}≡)) ==>
          (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) curry
:= _.
(* iris/algebra/ofe.v *)
Instance uncurry_ne {SI : sidx} {A B C : ofe} n :
  Proper (((≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) ==>
          (≡{n}@{A*B}≡) ==> (≡{n}@{C}≡)) uncurry
:= _.
(* iris/algebra/ofe.v *)
Instance curry3_ne {SI : sidx} {A B C D : ofe} n :
  Proper (((≡{n}@{A*B*C}≡) ==> (≡{n}@{D}≡)) ==>
          (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) curry3
:= _.
(* iris/algebra/ofe.v *)
Instance uncurry3_ne {SI : sidx} {A B C D : ofe} n :
  Proper (((≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) ==>
          (≡{n}@{A*B*C}≡) ==> (≡{n}@{D}≡)) uncurry3
:= _.
(* iris/algebra/ofe.v *)
Instance curry4_ne {SI : sidx} {A B C D E : ofe} n :
  Proper (((≡{n}@{A*B*C*D}≡) ==> (≡{n}@{E}≡)) ==>
          (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) curry4
:= _.
(* iris/algebra/ofe.v *)
Instance uncurry4_ne {SI : sidx} {A B C D E : ofe} n :
  Proper (((≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡) ==> (≡{n}≡)) ==>
          (≡{n}@{A*B*C*D}≡) ==> (≡{n}@{E}≡)) uncurry4
:= _.
(* iris/algebra/ofe.v *)
Instance prod_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.
(* iris/algebra/ofe.v *)
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).
(* iris/algebra/ofe.v *)
Instance prodO_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.
(* iris/algebra/ofe.v *)
(* * COFE → OFE Functors *)
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)
}.
(* iris/algebra/ofe.v *)
Instance : Params (@oFunctor_map) 10
:= {}.
(* iris/algebra/ofe.v *)
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 _).
(* iris/algebra/ofe.v *)
(* Not a coercion due to the [Cofe] type class argument, and to avoid
ambiguous coercion paths, see https://gitlab.mpi-sws.org/iris/iris/issues/240. *)
Definition oFunctor_apply {SI : sidx} (F : oFunctor) (A : ofe) `{!Cofe A} : ofe
:=
  oFunctor_car F A A.
(* iris/algebra/ofe.v *)
Definition oFunctor_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.
(* iris/algebra/ofe.v *)
Instance oFunctor_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.
(* iris/algebra/ofe.v *)
Instance oFunctor_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.
(* iris/algebra/ofe.v *)
Definition constOF {SI : sidx} (B : ofe) : oFunctor
:=
  {| oFunctor_car A1 A2 _ _ := B; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
(* iris/algebra/ofe.v *)
Coercion constOF : ofe >-> oFunctor.
(* iris/algebra/ofe.v *)
Instance constOF_contractive {SI : sidx} B : oFunctorContractive (constOF B).
Proof. rewrite /oFunctorContractive; apply _. Qed.
(* iris/algebra/ofe.v *)
Definition idOF {SI : sidx} : oFunctor
:=
  {| oFunctor_car A1 _ A2 _ := A2; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := f.2 |}.
(* iris/algebra/ofe.v *)
Notation "∙"
:= idOF : oFunctor_scope.
(* iris/algebra/ofe.v *)
Definition prodOF {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.
(* iris/algebra/ofe.v *)
Notation "F1 * F2"
:= (prodOF F1%OF F2%OF) : oFunctor_scope.
(* iris/algebra/ofe.v *)
Instance prodOF_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.
(* iris/algebra/ofe.v *)
Definition ofe_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.
(* iris/algebra/ofe.v *)
Notation "F1 -n> F2"
:= (ofe_morOF F1%OF F2%OF) : oFunctor_scope.
(* iris/algebra/ofe.v *)
Instance ofe_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.
(* iris/algebra/ofe.v *)
Instance sum_dist : Dist (A + B)
:= λ n, sum_relation (dist n) (dist n).
(* iris/algebra/ofe.v *)
Instance inl_ne : NonExpansive (@inl A B)
:= _.
(* iris/algebra/ofe.v *)
Instance inr_ne : NonExpansive (@inr A B)
:= _.
(* iris/algebra/ofe.v *)
Instance inl_ne_inj n : Inj (dist n) (dist n) (@inl A B)
:= _.
(* iris/algebra/ofe.v *)
Instance inr_ne_inj n : Inj (dist n) (dist n) (@inr A B)
:= _.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
Canonical sumO : ofe
:= Ofe (A + B) sum_ofe_mixin.
(* iris/algebra/ofe.v *)
(* The [compl] operator for sums is tricky. We are are given a [chain (A + B)]
  and need to turn it into a [chain A] or [chain B] to use the [compl] operation
  on [A] and [B], respectively. A priori it seems that a [chain (A + B)] might
  contain [inl] and [inr] elements in a mixed fashion, but this is not the case.
  Once we have inspected the first element [c 0ᵢ] and established it is an [inl]
  or [inr], we know the whole chain contains [inl] or [inr] elements.

  Encoding this knowledge using dependent types is annoying, hence the functions
  [inl_chain] and [inr_chain] take a default value [a] and [b] to handle the
  impossible [inr] and [inl] cases. The function [sum_compl] only calls
  [inl_chain] if the first element is [inl a], so it can easily supply such a
  default (and similar for [inr]). In the proofs of [sum_cofe] we show that
  these cases cannot occur. *)
Definition inl_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.
(* iris/algebra/ofe.v *)
Definition inr_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.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
(* The definition of [bcompl] follows the same pattern as [compl] with the
  caveat that we need to show that [0ᵢ] is below [n] (for which we use
  [SIdx.limit_lt_0]). *)
Definition inl_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.
(* iris/algebra/ofe.v *)
Definition inr_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.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
Instance 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.
(* iris/algebra/ofe.v *)
Instance inl_discrete (x : A) : Discrete x → Discrete (inl x).
Proof. inversion_clear 2; constructor; by apply (discrete_0 _). Qed.
(* iris/algebra/ofe.v *)
Instance inr_discrete (y : B) : Discrete y → Discrete (inr y).
Proof. inversion_clear 2; constructor; by apply (discrete_0 _). Qed.
(* iris/algebra/ofe.v *)
Instance sum_ofe_discrete :
    OfeDiscrete A → OfeDiscrete B → OfeDiscrete sumO.
Proof. intros ?? [?|?]; apply _. Qed.
(* iris/algebra/ofe.v *)
Instance sum_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.
(* iris/algebra/ofe.v *)
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).
(* iris/algebra/ofe.v *)
Instance sumO_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.
(* iris/algebra/ofe.v *)
Definition sumOF {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.
(* iris/algebra/ofe.v *)
Notation "F1 + F2"
:= (sumOF F1%OF F2%OF) : oFunctor_scope.
(* iris/algebra/ofe.v *)
Instance sumOF_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.
(* iris/algebra/ofe.v *)
Instance discrete_dist : Dist A
:= λ n x y, x ≡ y.
(* iris/algebra/ofe.v *)
Definition discrete_ofe_mixin : OfeMixin A.
Proof using Type*.
    split.
    - intros x y; split; [done|intros Hn; apply (Hn 0ᵢ)].
    - done.
    - done.
  Qed.
(* iris/algebra/ofe.v *)
Instance discrete_ofe_discrete : OfeDiscrete (Ofe A discrete_ofe_mixin).
Proof. by intros x y. Qed.
(* iris/algebra/ofe.v *)
Instance 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.
(* iris/algebra/ofe.v *)
(* The combinator [discreteO A] lifts an existing [Equiv A] instance into a
discrete OFE. *)
Notation discreteO A
:= (Ofe A (discrete_ofe_mixin _)).
(* iris/algebra/ofe.v *)
(* The combinator [leibnizO A] lifts Leibniz equality [=] into a discrete OFE.
The implementation forces the [Equivalence] proof to be [eq_equivalence] so that
Coq does not accidentally use another one, like [ofe_equivalence], in the case of
aliases. See also https://gitlab.mpi-sws.org/iris/iris/issues/299 *)
Notation leibnizO A
:= (Ofe A (@discrete_ofe_mixin _ _ equivL eq_equivalence)).
(* iris/algebra/ofe.v *)
(* In order to define a discrete CMRA with carrier [A] (in the file [cmra.v])
we need to determine the [Equivalence A] proof that was used to construct the
OFE instance of [A] (note that this proof is not the same as the one we obtain
via [ofe_equivalence]).

We obtain the proof of [Equivalence A] by inferring the canonical OFE mixin
using [ofe_mixin_of A], and then check whether it is indeed a discrete OFE. This
will fail if no OFE, or an OFE other than the discrete OFE, was registered. *)
Notation discrete_ofe_equivalence_of A
:= ltac:(
  match constr:(ofe_mixin_of A) with
  | discrete_ofe_mixin ?H => exact H
  end) (only parsing).
(* iris/algebra/ofe.v *)
Instance leibnizO_leibniz {SI : sidx} A  : LeibnizEquiv (leibnizO A).
Proof. by intros x y. Qed.
(* iris/algebra/ofe.v *)
(* * Basic Coq types *)
Canonical boolO {SI : sidx} : ofe
:= leibnizO bool.
(* iris/algebra/ofe.v *)
Canonical natO {SI : sidx} : ofe
:= leibnizO nat.
(* iris/algebra/ofe.v *)
Canonical positiveO {SI : sidx} : ofe
:= leibnizO positive.
(* iris/algebra/ofe.v *)
Canonical NO {SI : sidx} : ofe
:= leibnizO N.
(* iris/algebra/ofe.v *)
Canonical ZO {SI : sidx} : ofe
:= leibnizO Z.
(* iris/algebra/ofe.v *)
Instance Prop_equiv : Equiv Prop
:= iff.
(* iris/algebra/ofe.v *)
Instance Prop_equivalence : Equivalence (≡@{Prop})
:= _.
(* iris/algebra/ofe.v *)
Canonical PropO
:= discreteO Prop.
(* iris/algebra/ofe.v *)
Instance option_dist : Dist (option A)
:= λ n, option_Forall2 (dist n).
(* iris/algebra/ofe.v *)
Lemma option_dist_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
Proof. done. Qed.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
Canonical optionO
:= Ofe (option A) option_ofe_mixin.
(* iris/algebra/ofe.v *)
Instance Some_ne : NonExpansive (@Some A).
Proof. intros ????. by econstructor. Qed.
(* iris/algebra/ofe.v *)
Instance Some_dist_inj n : Inj (dist n) (dist n) (@Some A).
Proof. by inversion_clear 1. Qed.
(* iris/algebra/ofe.v *)
Definition option_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.
(* iris/algebra/ofe.v *)
Definition option_compl `{!Cofe A} : Compl optionO
:= λ c,
    match c 0ᵢ with Some x => Some (compl (option_chain c x)) | None => None end.
(* iris/algebra/ofe.v *)
Definition option_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.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
Instance 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.
(* iris/algebra/ofe.v *)
Instance option_ofe_discrete : OfeDiscrete A → OfeDiscrete optionO.
Proof. destruct 2; constructor; by apply (discrete_0 _). Qed.
(* iris/algebra/ofe.v *)
Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
Proof. destruct 1; split; eauto. Qed.
(* iris/algebra/ofe.v *)
Instance from_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.
(* iris/algebra/ofe.v *)
Instance None_discrete : Discrete (@None A).
Proof. inversion_clear 1; constructor. Qed.
(* iris/algebra/ofe.v *)
Instance Some_discrete x : Discrete x → Discrete (Some x).
Proof. by intros ?; inversion_clear 1; constructor; apply discrete_0. Qed.
(* iris/algebra/ofe.v *)
Lemma dist_None n mx : mx ≡{n}≡ None ↔ mx = None.
Proof. split; [by inversion_clear 1|by intros ->]. Qed.
(* iris/algebra/ofe.v *)
Lemma dist_Some n x y : Some x ≡{n}≡ Some y ↔ x ≡{n}≡ y.
Proof. split; [by inversion_clear 1 | by intros ->]. Qed.
(* iris/algebra/ofe.v *)
Lemma dist_Some_inv_l n mx my x :
    mx ≡{n}≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡{n}≡ y.
Proof. destruct 1; naive_solver. Qed.
(* iris/algebra/ofe.v *)
Lemma dist_Some_inv_r n mx my y :
    mx ≡{n}≡ my → my = Some y → ∃ x, mx = Some x ∧ x ≡{n}≡ y.
Proof. destruct 1; naive_solver. Qed.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
Instance option_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.
(* iris/algebra/ofe.v *)
Instance option_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.
(* iris/algebra/ofe.v *)
Instance option_mjoin_ne {SI : sidx} {A : ofe} n :
  Proper (dist n ==> (≡{n}@{option A}≡)) mjoin.
Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
(* iris/algebra/ofe.v *)
Instance option_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.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
Definition optionO_map {SI : sidx} {A B: ofe} (f : A -n> B) :
    optionO A -n> optionO B
:=
  OfeMor (fmap f : optionO A → optionO B).
(* iris/algebra/ofe.v *)
Instance optionO_map_ne {SI : sidx} (A B: ofe) :
  NonExpansive (@optionO_map SI A B).
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
(* iris/algebra/ofe.v *)
Definition optionOF {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.
(* iris/algebra/ofe.v *)
Instance optionOF_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.
(* iris/algebra/ofe.v *)
(* Note that the projection [later_car] is not non-expansive (see also the
lemma [later_car_anti_contractive] below), so it cannot be used in the logic.
If you need to get a witness out, you should use the lemma [Next_uninj]
instead. *)
Record later (A : Type) : Type
:= Next { later_car : A }.
(* iris/algebra/ofe.v *)
Instance : Params (@Next) 1
:= {}.
(* iris/algebra/ofe.v *)
Instance later_equiv : Equiv (later A)
:= λ x y, later_car x ≡ later_car y.
(* iris/algebra/ofe.v *)
Instance later_dist : Dist (later A)
:= λ n x y,
    dist_later n (later_car x) (later_car y).
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
Canonical laterO : ofe
:= Ofe (later A) later_ofe_mixin.
(* iris/algebra/ofe.v *)
Instance Next_contractive : Contractive (@Next A).
Proof. by intros n x y. Qed.
(* iris/algebra/ofe.v *)
Instance Next_inj n : Inj (dist_later n) (dist n) (@Next A).
Proof. by intros x y H. Qed.
(* iris/algebra/ofe.v *)
Lemma Next_uninj x : ∃ a, x ≡ Next a.
Proof. by exists (later_car x). Qed.
(* iris/algebra/ofe.v *)
Instance later_car_anti_contractive n :
    Proper (dist n ==> dist_later n) later_car.
Proof. move=> [x] [y] /= Hxy. done. Qed.
(* iris/algebra/ofe.v *)
Definition later_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.
(* iris/algebra/ofe.v *)
Definition later_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.