(* iris/algebra/cmra.v *)
From stdpp Require Import finite
From iris.algebra Require Export ofe monoid
From iris.prelude Require Import options

Local SetPrimitive Projections.

Local OpenScope sidx_scope.

Class PCore(A : Type) := pcore : A → option A.

Global HintMode PCore ! : typeclass_instances.

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

Class Op(A : Type) := op : A → A → A.

Global HintMode Op ! : typeclass_instances.

Global Instance: Params (@op) 2 := {}.
Infix "⋅" := op (at level 50, left associativity) : stdpp_scope.

Definition included{A} `{!Equiv A, !Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
Infix "≼" := included (at level 70) : stdpp_scope.

Global HintExtern 0 (_ ≼ _) => reflexivity : core.

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

Definition opM`{!Op A} (x : A) (my : option A) :=
  match my with Some y => x ⋅ y | None => x end.
Infix "⋅?" := opM (at level 50, left associativity) : stdpp_scope.

Class ValidN{SI : sidx} (A : Type) := validN : SI → A → Prop.

Global HintMode ValidN - ! : typeclass_instances.

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

Class Valid(A : Type) := valid : A → Prop.

Global HintMode Valid ! : typeclass_instances.

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

Definition includedN{SI : sidx} `{!Dist A, Op A} (n : SI) (x y : A) :=
  ∃ z, y ≡{n}≡ x ⋅ z.

Global Instance: Params (@includedN) 5 := {}.

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

Record CmraMixin{SI : sidx} A
      `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A} := {

Structure cmra{SI : sidx} := Cmra' {
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_dist : Dist cmra_car;
  cmra_pcore : PCore cmra_car;
  cmra_op : Op cmra_car;
  cmra_valid : Valid cmra_car;
  cmra_validN : ValidN cmra_car;
  cmra_ofe_mixin : OfeMixin cmra_car;
  cmra_mixin : CmraMixin cmra_car;
}.

Global ArgumentsCmra' {_} _ {_ _ _ _ _ _} _ _.

Notation CmraA m := (Cmra' A (ofe_mixin_of A%type) m) (only parsing).

Global Argumentscmra_car : simpl never.

Global Argumentscmra_equiv : simpl never.

Global Argumentscmra_dist : simpl never.

Global Argumentscmra_pcore : simpl never.

Global Argumentscmra_op : simpl never.

Global Argumentscmra_valid : simpl never.

Global Argumentscmra_validN : simpl never.

Global Argumentscmra_ofe_mixin : simpl never.

Global Argumentscmra_mixin : simpl never.
Add Printing Constructor cmra.

Global HintExtern 0 (PCore _) => refine (cmra_pcore _); shelve : typeclass_instances.

Global HintExtern 0 (Op _) => refine (cmra_op _); shelve : typeclass_instances.

Global HintExtern 0 (Valid _) => refine (cmra_valid _); shelve : typeclass_instances.

Global HintExtern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_instances.

Coercion cmra_ofeO{SI : sidx} (A : cmra) : ofe := Ofe A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeO.

Global Strategyexpand [cmra_ofeO cmra_equiv cmra_dist cmra_pcore cmra_op
                        cmra_valid cmra_validN cmra_ofe_mixin cmra_mixin].

Definition cmra_mixin_of'{SI : sidx} A {Ac : cmra}
  (f : Ac → A) : CmraMixin Ac := cmra_mixin Ac.

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

Global Instancecmra_op_ne (x : A) : NonExpansive (op x).
  Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.

Lemma cmra_pcore_nen x y cx :
    x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy.
  Proof. apply (mixin_cmra_pcore_ne _ (cmra_mixin A)). Qed.

Global Instancecmra_validN_ne n : Proper (dist n ==> impl) (@validN _ A _ n).
  Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.

Lemma cmra_valid_validNx : ✓ x ↔ ∀ n, ✓{n} x.
  Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.

Lemma cmra_validN_len n' x : ✓{n} x → n' ≤ n → ✓{n'} x.
  Proof. apply (mixin_cmra_validN_le _ (cmra_mixin A)). Qed.

Global Instancecmra_assoc : Assoc (≡) (@op A _).
  Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed.

Global Instancecmra_comm : Comm (≡) (@op A _).
  Proof. apply (mixin_cmra_comm _ (cmra_mixin A)). Qed.

Lemma cmra_pcore_lx cx : pcore x = Some cx → cx ⋅ x ≡ x.
  Proof. apply (mixin_cmra_pcore_l _ (cmra_mixin A)). Qed.

Lemma cmra_pcore_idempx cx : pcore x = Some cx → pcore cx ≡ Some cx.
  Proof. apply (mixin_cmra_pcore_idemp _ (cmra_mixin A)). Qed.

Lemma cmra_pcore_monox y cx :
    x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
  Proof. apply (mixin_cmra_pcore_mono _ (cmra_mixin A)). Qed.

Lemma cmra_validN_op_ln x y : ✓{n} (x ⋅ y) → ✓{n} x.
  Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.

Lemma cmra_extendn x y1 y2 :
    ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
    { z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }.
  Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.

Class CoreId{SI : sidx} {A : cmra} (x : A) := core_id : pcore x ≡ Some x.

Global Argumentscore_id {_ _} _ {_}.

Global HintMode CoreId - + ! : typeclass_instances.

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

Class Exclusive{SI : sidx} {A : cmra} (x : A) :=
  exclusive0_l y : ✓{0ᵢ} (x ⋅ y) → False.

Global Argumentsexclusive0_l {_ _} _ {_} _ _.

Global HintMode Exclusive - + ! : typeclass_instances.

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

Class Cancelable{SI : sidx} {A : cmra} (x : A) :=
  cancelableN n y z : ✓{n} (x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.

Global ArgumentscancelableN {_ _} _ {_} _ _ _ _.

Global HintMode Cancelable - + ! : typeclass_instances.

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

Class IdFree{SI : sidx} {A : cmra} (x : A) :=
  id_free0_r y : ✓{0ᵢ} x → x ⋅ y ≡{0ᵢ}≡ x → False.

Global Argumentsid_free0_r {_ _} _ {_} _ _.

Global HintMode IdFree - + ! : typeclass_instances.

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

Class CmraTotal{SI : sidx} (A : cmra) :=
  cmra_total (x : A) : is_Some (pcore x).

Global HintMode CmraTotal - ! : typeclass_instances.

Definition core{A} `{!PCore A} (x : A) : A := default x (pcore x).

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

Class Unit(A : Type) := ε : A.

Global HintMode Unit ! : typeclass_instances.

Global Argumentsε {_ _}.

Record UcmraMixin{SI : sidx} A
    `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !Unit A} := {
  mixin_ucmra_unit_valid : ✓ (ε : A);
  mixin_ucmra_unit_left_id : LeftId (≡@{A}) ε (⋅);
  mixin_ucmra_pcore_unit : pcore ε ≡@{option A} Some ε
}.
#[projections(primitive=no)]

Structure ucmra{SI : sidx} := Ucmra' {
  ucmra_car :> Type;
  ucmra_equiv : Equiv ucmra_car;
  ucmra_dist : Dist ucmra_car;
  ucmra_pcore : PCore ucmra_car;
  ucmra_op : Op ucmra_car;
  ucmra_valid : Valid ucmra_car;
  ucmra_validN : ValidN ucmra_car;
  ucmra_unit : Unit ucmra_car;
  ucmra_ofe_mixin : OfeMixin ucmra_car;
  ucmra_cmra_mixin : CmraMixin ucmra_car;
  ucmra_mixin : UcmraMixin ucmra_car;
}.

Global ArgumentsUcmra' {_} _ {_ _ _ _ _ _ _} _ _ _.

Notation UcmraA m :=
  (Ucmra' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).

Global Argumentsucmra_car : simpl never.

Global Argumentsucmra_equiv : simpl never.

Global Argumentsucmra_dist : simpl never.

Global Argumentsucmra_pcore : simpl never.

Global Argumentsucmra_op : simpl never.

Global Argumentsucmra_valid : simpl never.

Global Argumentsucmra_validN : simpl never.

Global Argumentsucmra_ofe_mixin : simpl never.

Global Argumentsucmra_cmra_mixin : simpl never.

Global Argumentsucmra_mixin : simpl never.
Add Printing Constructor ucmra.

Global HintExtern 0 (Unit _) => refine (ucmra_unit _); shelve : typeclass_instances.

Coercion ucmra_ofeO{SI : sidx} (A : ucmra) : ofe := Ofe A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeO.

Coercion ucmra_cmraR{SI : sidx} (A : ucmra) : cmra :=
  Cmra' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
Canonical Structure ucmra_cmraR.

Global Strategyexpand [ucmra_cmraR ucmra_ofeO ucmra_equiv ucmra_dist ucmra_pcore
                        ucmra_op ucmra_valid ucmra_validN ucmra_unit
                        ucmra_ofe_mixin ucmra_cmra_mixin].

Lemma ucmra_unit_valid: ✓ (ε : A).
  Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.

Global Instanceucmra_unit_left_id : LeftId (≡) ε (@op A _).
  Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.

Lemma ucmra_pcore_unit: pcore (ε:A) ≡ Some ε.
  Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.

Class CmraDiscrete{SI : sidx} (A : cmra) := {
  #[global] cmra_discrete_ofe_discrete :: OfeDiscrete A;
  cmra_discrete_valid (x : A) : ✓{0ᵢ} x → ✓ x
}.

Global HintMode CmraDiscrete - ! : typeclass_instances.

Class CmraMorphism{SI : sidx} {A B : cmra} (f : A → B) := {
  #[global] cmra_morphism_ne :: NonExpansive f;
  cmra_morphism_validN n x : ✓{n} x → ✓{n} f x;
  cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
  cmra_morphism_op x y : f (x ⋅ y) ≡ f x ⋅ f y
}.

Global HintMode CmraMorphism - - - ! : typeclass_instances.

Global Argumentscmra_morphism_validN {_ _ _} _ {_} _ _ _.

Global Argumentscmra_morphism_pcore {_ _ _} _ {_} _.

Global Argumentscmra_morphism_op {_ _ _} _ {_} _ _.

Global Instancecmra_pcore_ne' : NonExpansive (@pcore A _).
Proof.
  intros n x y Hxy. destruct (pcore x) as [cx|] eqn:?.
  { destruct (cmra_pcore_ne n x y cx) as (cy&->&->); auto. }
  destruct (pcore y) as [cy|] eqn:?; auto.
  destruct (cmra_pcore_ne n y x cy) as (cx&?&->); simplify_eq/=; auto.
Qed.

Lemma cmra_pcore_properx y cx :
  x ≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡ cy.
Proof.
  intros. destruct (cmra_pcore_ne 0ᵢ x y cx) as (cy&?&?); auto.
  exists cy; split; [done|apply equiv_dist=> n].
  destruct (cmra_pcore_ne n x y cx) as (cy'&?&?); naive_solver.
Qed.

Global Instancecmra_pcore_proper' : Proper ((≡) ==> (≡)) (@pcore A _).
Proof. apply (ne_proper _). Qed.

Global Instancecmra_op_ne' : NonExpansive2 (@op A _).
Proof. intros n x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.

Global Instancecmra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
Proof. apply (ne_proper_2 _). Qed.

Global Instancecmra_validN_ne' n : Proper (dist n ==> iff) (@validN SI A _ n) | 1.
Proof. by split; apply cmra_validN_ne. Qed.

Global Instancecmra_validN_proper n : Proper ((≡) ==> iff) (@validN SI A _ n) | 1.
Proof. by intros x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.

Global Instancecmra_valid_proper : Proper ((≡) ==> iff) (@valid A _).
Proof.
  intros x y Hxy; rewrite !cmra_valid_validN.
  by split=> ? n; [rewrite -Hxy|rewrite Hxy].
Qed.

Global Instancecmra_includedN_ne n :
  Proper (dist n ==> dist n ==> iff) (@includedN SI A _ _ n) | 1.
Proof.
  intros x x' Hx y y' Hy.
  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.

Global Instancecmra_includedN_proper n :
  Proper ((≡) ==> (≡) ==> iff) (@includedN SI A _ _ n) | 1.
Proof.
  intros x x' Hx y y' Hy; revert Hx Hy; rewrite !equiv_dist=> Hx Hy.
  by rewrite (Hx n) (Hy n).
Qed.

Global Instancecmra_included_proper :
  Proper ((≡) ==> (≡) ==> iff) (@included A _ _) | 1.
Proof.
  intros x x' Hx y y' Hy.
  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.

Global Instancecmra_opM_ne : NonExpansive2 (@opM A _).
Proof. destruct 2; by ofe_subst. Qed.

Global Instancecmra_opM_proper : Proper ((≡) ==> (≡) ==> (≡)) (@opM A _).
Proof. destruct 2; by setoid_subst. Qed.

Global InstanceCoreId_proper : Proper ((≡) ==> iff) (@CoreId SI A).
Proof. solve_proper. Qed.

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

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

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

Lemma cmra_op_opM_assocx y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz).
Proof. destruct mz; by rewrite /= -?assoc. Qed.

Lemma cmra_validN_ltn n' x : ✓{n} x → n' < n → ✓{n'} x.
Proof. eauto using cmra_validN_le, SIdx.lt_le_incl. Qed.

Lemma cmra_valid_op_lx y : ✓ (x ⋅ y) → ✓ x.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed.

Lemma cmra_validN_op_rn x y : ✓{n} (x ⋅ y) → ✓{n} y.
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.

Lemma cmra_valid_op_rx y : ✓ (x ⋅ y) → ✓ y.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.

Lemma cmra_pcore_l'x cx : pcore x ≡ Some cx → cx ⋅ x ≡ x.
Proof. intros (cx'&?&<-)%Some_equiv_eq. by apply cmra_pcore_l. Qed.

Lemma cmra_pcore_rx cx : pcore x = Some cx → x ⋅ cx ≡ x.
Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed.

Lemma cmra_pcore_r'x cx : pcore x ≡ Some cx → x ⋅ cx ≡ x.
Proof. intros (cx'&?&<-)%Some_equiv_eq. by apply cmra_pcore_r. Qed.

Lemma cmra_pcore_idemp'x cx : pcore x ≡ Some cx → pcore cx ≡ Some cx.
Proof. intros (cx'&?&<-)%Some_equiv_eq. eauto using cmra_pcore_idemp. Qed.

Lemma cmra_pcore_dupx cx : pcore x = Some cx → cx ≡ cx ⋅ cx.
Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.

Lemma cmra_pcore_dup'x cx : pcore x ≡ Some cx → cx ≡ cx ⋅ cx.
Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp'. Qed.

Lemma cmra_pcore_validNn x cx : ✓{n} x → pcore x = Some cx → ✓{n} cx.
Proof.
  intros Hvx Hx%cmra_pcore_l. move: Hvx; rewrite -Hx. apply cmra_validN_op_l.
Qed.

Lemma cmra_pcore_validx cx : ✓ x → pcore x = Some cx → ✓ cx.
Proof.
  intros Hv Hx%cmra_pcore_l. move: Hv; rewrite -Hx. apply cmra_valid_op_l.
Qed.

Lemma exclusiveN_ln x `{!Exclusive x} y : ✓{n} (x ⋅ y) → False.
Proof. intros. by eapply (exclusive0_l x y), cmra_validN_le, SIdx.le_0_l. Qed.

Lemma exclusiveN_rn x `{!Exclusive x} y : ✓{n} (y ⋅ x) → False.
Proof. rewrite comm. by apply exclusiveN_l. Qed.

Lemma exclusive_lx `{!Exclusive x} y : ✓ (x ⋅ y) → False.
Proof. by move /cmra_valid_validN /(_ 0ᵢ) /exclusive0_l. Qed.

Lemma exclusive_rx `{!Exclusive x} y : ✓ (y ⋅ x) → False.
Proof. rewrite comm. by apply exclusive_l. Qed.

Lemma exclusiveN_opMn x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None.
Proof. destruct my as [y|]; last done. move=> /(exclusiveN_l _ x) []. Qed.

Lemma exclusive_includedNn x `{!Exclusive x} y : x ≼{n} y → ✓{n} y → False.
Proof. intros [? ->]. by apply exclusiveN_l. Qed.

Lemma exclusive_includedx `{!Exclusive x} y : x ≼ y → ✓ y → False.
Proof. intros [? ->]. by apply exclusive_l. Qed.

Lemma cmra_included_includedNn x y : x ≼ y → x ≼{n} y.
Proof. intros [z ->]. by exists z. Qed.

Global Instancecmra_includedN_trans n : Transitive (@includedN SI A _ _ n).
Proof.
  intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). by rewrite assoc -Hy -Hz.
Qed.

Global Instancecmra_included_trans: Transitive (@included A _ _).
Proof.
  intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). by rewrite assoc -Hy -Hz.
Qed.

Lemma cmra_valid_includedx y : ✓ y → x ≼ y → ✓ x.
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_valid_op_l. Qed.

Lemma cmra_validN_includedNn x y : ✓{n} y → x ≼{n} y → ✓{n} x.
Proof. intros Hyv [z ?]; ofe_subst y; eauto using cmra_validN_op_l. Qed.

Lemma cmra_validN_includedn x y : ✓{n} y → x ≼ y → ✓{n} x.
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.

Lemma cmra_includedN_len m x y : x ≼{n} y → m ≤ n → x ≼{m} y.
Proof. by intros [z Hz] H; exists z; eapply dist_le. Qed.

Lemma cmra_includedN_Sn x y : x ≼{Sᵢ n} y → x ≼{n} y.
Proof. intros ?. by eapply cmra_includedN_le, SIdx.le_succ_diag_r. Qed.

Lemma cmra_includedN_ln x y : x ≼{n} x ⋅ y.
Proof. by exists y. Qed.

Lemma cmra_included_lx y : x ≼ x ⋅ y.
Proof. by exists y. Qed.

Lemma cmra_includedN_rn x y : y ≼{n} x ⋅ y.
Proof. rewrite (comm op); apply cmra_includedN_l. Qed.

Lemma cmra_included_rx y : y ≼ x ⋅ y.
Proof. rewrite (comm op); apply cmra_included_l. Qed.

Lemma cmra_pcore_mono'x y cx :
  x ≼ y → pcore x ≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
Proof.
  intros ? (cx'&?&Hcx)%Some_equiv_eq.
  destruct (cmra_pcore_mono x y cx') as (cy&->&?); auto.
  exists cy; by rewrite -Hcx.
Qed.

Lemma cmra_pcore_monoN'n x y cx :
  x ≼{n} y → pcore x ≡{n}≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼{n} cy.
Proof.
  intros [z Hy] (cx'&?&Hcx)%dist_Some_inv_r'.
  destruct (cmra_pcore_mono x (x ⋅ z) cx')
    as (cy&Hxy&?); auto using cmra_included_l.
  assert (pcore y ≡{n}≡ Some cy) as (cy'&?&Hcy')%dist_Some_inv_r'.
  { by rewrite Hy Hxy. }
  exists cy'; split; first done.
  rewrite Hcx -Hcy'; auto using cmra_included_includedN.
Qed.

Lemma cmra_included_pcorex cx : pcore x = Some cx → cx ≼ x.
Proof. exists x. by rewrite cmra_pcore_l. Qed.

Lemma cmra_monoN_ln x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.

Lemma cmra_mono_lx y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.

Lemma cmra_monoN_rn x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z.
Proof. by intros; rewrite -!(comm _ z); apply cmra_monoN_l. Qed.

Lemma cmra_mono_rx y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
Proof. by intros; rewrite -!(comm _ z); apply cmra_mono_l. Qed.

Lemma cmra_monoNn x1 x2 y1 y2 : x1 ≼{n} y1 → x2 ≼{n} y2 → x1 ⋅ x2 ≼{n} y1 ⋅ y2.
Proof. intros; etrans; eauto using cmra_monoN_l, cmra_monoN_r. Qed.

Lemma cmra_monox1 x2 y1 y2 : x1 ≼ y1 → x2 ≼ y2 → x1 ⋅ x2 ≼ y1 ⋅ y2.
Proof. intros; etrans; eauto using cmra_mono_l, cmra_mono_r. Qed.

Global Instancecmra_monoN' n :
  Proper (includedN n ==> includedN n ==> includedN n) (@op A _).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_monoN. Qed.

Global Instancecmra_mono' :
  Proper (included ==> included ==> included) (@op A _).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_mono. Qed.

Lemma cmra_included_dist_ln x1 x2 x1' :
  x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2.
Proof.
  intros [z Hx2] Hx1; exists (x1' ⋅ z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Qed.

Lemma core_id_dupx `{!CoreId x} : x ≡ x ⋅ x.
Proof. by apply cmra_pcore_dup' with x. Qed.

Lemma core_id_extractx y `{!CoreId x} :
  x ≼ y → y ≡ y ⋅ x.
Proof.
  intros ?.
  destruct (cmra_pcore_mono' x y x) as (cy & Hcy & [x' Hx']); [done|exact: core_id|].
  rewrite -(cmra_pcore_r y) //. rewrite Hx' -!assoc. f_equiv.
  rewrite [x' ⋅ x]comm assoc -core_id_dup. done.
Qed.

Local SetDefault Proof Using "Type*".
  Context `{!CmraTotal A}.

Lemma cmra_pcore_corex : pcore x = Some (core x).
  Proof.
    rewrite /core. destruct (cmra_total x) as [cx ->]. done.
  Qed.

Lemma cmra_core_lx : core x ⋅ x ≡ x.
  Proof.
    destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_l.
  Qed.

Lemma cmra_core_idempx : core (core x) ≡ core x.
  Proof.
    destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_idemp.
  Qed.

Lemma cmra_core_monox y : x ≼ y → core x ≼ core y.
  Proof.
    intros; destruct (cmra_total x) as [cx Hcx].
    destruct (cmra_pcore_mono x y cx) as (cy&Hcy&?); auto.
    by rewrite /core /= Hcx Hcy.
  Qed.

Global Instancecmra_core_ne : NonExpansive (@core A _).
  Proof.
    intros n x y Hxy. destruct (cmra_total x) as [cx Hcx].
    by rewrite /core /= -Hxy Hcx.
  Qed.

Global Instancecmra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
  Proof. apply (ne_proper _). Qed.

Lemma cmra_core_rx : x ⋅ core x ≡ x.
  Proof. by rewrite (comm _ x) cmra_core_l. Qed.

Lemma cmra_core_dupx : core x ≡ core x ⋅ core x.
  Proof. by rewrite -{3}(cmra_core_idemp x) cmra_core_r. Qed.

Lemma cmra_core_validNn x : ✓{n} x → ✓{n} core x.
  Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.

Lemma cmra_core_validx : ✓ x → ✓ core x.
  Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.

Lemma core_id_totalx : CoreId x ↔ core x ≡ x.
  Proof.
    split; [intros; by rewrite /core /= (core_id x)|].
    rewrite /CoreId /core /=.
    destruct (cmra_total x) as [? ->]. by constructor.
  Qed.

Lemma core_id_corex `{!CoreId x} : core x ≡ x.
  Proof. by apply core_id_total. Qed.

Lemma cmra_pcore_core_idx y : pcore x = Some y → CoreId y.
  Proof. rewrite /CoreId. eauto using cmra_pcore_idemp. Qed.

Global Instancecmra_core_core_id x : CoreId (core x).
  Proof. eapply cmra_pcore_core_id. rewrite cmra_pcore_core. done. Qed.

Lemma cmra_included_corex : core x ≼ x.
  Proof. by exists x; rewrite cmra_core_l. Qed.

Global Instancecmra_includedN_preorder n : PreOrder (@includedN SI A _ _ n).
  Proof.
    split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
  Qed.

Global Instancecmra_included_preorder : PreOrder (@included A _ _).
  Proof.
    split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
  Qed.

Lemma cmra_core_monoNn x y : x ≼{n} y → core x ≼{n} core y.
  Proof.
    intros [z ->].
    apply cmra_included_includedN, cmra_core_mono, cmra_included_l.
  Qed.

Lemma cmra_discrete_included_lx y : Discrete x → ✓{0ᵢ} y → x ≼{0ᵢ} y → x ≼ y.
Proof.
  intros ?? [x' ?].
  destruct (cmra_extend 0ᵢ y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
  by exists z'; rewrite Hy (discrete_0 x z).
Qed.

Lemma cmra_discrete_included_rx y : Discrete y → x ≼{0ᵢ} y → x ≼ y.
Proof. intros ? [x' ?]. exists x'. by apply (discrete_0 y). Qed.

Lemma cmra_op_discretex1 x2 :
  ✓{0ᵢ} (x1 ⋅ x2) → Discrete x1 → Discrete x2 → Discrete (x1 ⋅ x2).
Proof.
  intros ??? z Hz.
  destruct (cmra_extend 0ᵢ z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
  { rewrite -?Hz. done. }
  by rewrite Hz' (discrete_0 x1 y1) // (discrete_0 x2 y2).
Qed.

Lemma cmra_discrete_valid_iff`{!CmraDiscrete A} n x : ✓ x ↔ ✓{n} x.
Proof.
  split; first by rewrite cmra_valid_validN.
  eauto using cmra_discrete_valid, cmra_validN_le, SIdx.le_0_l.
Qed.

Lemma cmra_discrete_valid_iff_0`{!CmraDiscrete A} n x : ✓{0ᵢ} x ↔ ✓{n} x.
Proof. by rewrite -!cmra_discrete_valid_iff. Qed.

Lemma cmra_discrete_included_iff`{!OfeDiscrete A} n x y : x ≼ y ↔ x ≼{n} y.
Proof.
  split; first by apply cmra_included_includedN.
  intros [z ->%(discrete_iff _ _ _)]; eauto using cmra_included_l.
Qed.

Lemma cmra_discrete_included_iff_0`{!OfeDiscrete A} n x y : x ≼{0ᵢ} y ↔ x ≼{n} y.
Proof. by rewrite -!cmra_discrete_included_iff. Qed.

Global Instancecancelable_proper : Proper (equiv ==> iff) (@Cancelable SI A).
Proof. unfold Cancelable. intros x x' EQ. by setoid_rewrite EQ. Qed.

Lemma cancelablex `{!Cancelable x} y z : ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z.
Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.

Lemma discrete_cancelablex `{!CmraDiscrete A}:
  (∀ y z, ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z) → Cancelable x.
Proof. intros ????. rewrite -!discrete_iff -cmra_discrete_valid_iff. auto. Qed.

Global Instancecancelable_op x y :
  Cancelable x → Cancelable y → Cancelable (x ⋅ y).
Proof.
  intros ?? n z z' ??. apply (cancelableN y), (cancelableN x).
  - eapply cmra_validN_op_r. by rewrite assoc.
  - by rewrite assoc.
  - by rewrite !assoc.
Qed.

Global Instanceexclusive_cancelable (x : A) : Exclusive x → Cancelable x.
Proof. intros ? n z z' []%(exclusiveN_l _ x). Qed.

Global Instanceid_free_ne n : Proper (dist n ==> iff) (@IdFree SI A).
Proof.
  intros x x' EQ%(dist_le _ 0ᵢ); [|apply SIdx.le_0_l]. rewrite /IdFree.
  split=> y ?; (rewrite -EQ || rewrite EQ); eauto.
Qed.

Global Instanceid_free_proper : Proper (equiv ==> iff) (@IdFree SI A).
Proof. by move=> P Q /equiv_dist /(_ 0ᵢ)=> ->. Qed.

Lemma id_freeN_rn n' x `{!IdFree x} y : ✓{n}x → x ⋅ y ≡{n'}≡ x → False.
Proof. eauto using cmra_validN_le, dist_le, SIdx.le_0_l. Qed.

Lemma id_freeN_ln n' x `{!IdFree x} y : ✓{n}x → y ⋅ x ≡{n'}≡ x → False.
Proof. rewrite comm. eauto using id_freeN_r. Qed.

Lemma id_free_rx `{!IdFree x} y : ✓x → x ⋅ y ≡ x → False.
Proof. move=> /cmra_valid_validN ? /equiv_dist. eauto. Qed.

Lemma id_free_lx `{!IdFree x} y : ✓x → y ⋅ x ≡ x → False.
Proof. rewrite comm. eauto using id_free_r. Qed.

Lemma discrete_id_freex `{!CmraDiscrete A}:
  (∀ y, ✓ x → x ⋅ y ≡ x → False) → IdFree x.
Proof.
  intros Hx y ??. apply (Hx y), (discrete_0 _); eauto using cmra_discrete_valid.
Qed.

Global Instanceid_free_op_r x y : IdFree y → Cancelable x → IdFree (x ⋅ y).
Proof.
  intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
  eapply (id_free0_r y); [by eapply cmra_validN_op_r |symmetry; eauto].
Qed.

Global Instanceid_free_op_l x y : IdFree x → Cancelable y → IdFree (x ⋅ y).
Proof. intros. rewrite comm. apply _. Qed.

Global Instanceexclusive_id_free x : Exclusive x → IdFree x.
Proof. intros ? z ? Hid. apply (exclusiveN_l 0ᵢ x z). by rewrite Hid. Qed.

Global HintExtern 0 (?a ≼ ?a ⋅ _) => apply: cmra_included_l : core.

Global HintExtern 0 (?a ≼ _ ⋅ ?a) => apply: cmra_included_r : core.

Lemma ucmra_unit_validNn : ✓{n} (ε:A).
  Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.

Lemma ucmra_unit_leastNn x : ε ≼{n} x.
  Proof. by exists x; rewrite left_id. Qed.

Lemma ucmra_unit_leastx : ε ≼ x.
  Proof. by exists x; rewrite left_id. Qed.

Global Instanceucmra_unit_right_id : RightId (≡) ε (@op A _).
  Proof. by intros x; rewrite (comm op) left_id. Qed.

Global Instanceucmra_unit_core_id : CoreId (ε:A).
  Proof. apply ucmra_pcore_unit. Qed.

Global Instancecmra_unit_cmra_total : CmraTotal A.
  Proof.
    intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?); [..|by eauto].
    - apply ucmra_unit_least.
    - apply (core_id _).
  Qed.

Global Instanceempty_cancelable : Cancelable (ε:A).
  Proof. intros ???. by rewrite !left_id. Qed.

Lemma cmra_monoid: Monoid (@op A _) ε.
  Proof. split; apply _. Qed.

Global HintExtern 0 (Monoid _ _) => refine cmra_monoid; shelve : typeclass_instances.

Global HintImmediate cmra_unit_cmra_total : core.

Global HintExtern 0 (ε ≼ _) => apply: ucmra_unit_least : core.

Local SetDefault Proof Using "Type*".
  Context {SI : sidx} {A : cmra} `{!LeibnizEquiv A}.
  Implicit Types x y : A.

Global Instancecmra_assoc_L : Assoc (=) (@op A _).
  Proof. intros x y z. unfold_leibniz. by rewrite assoc. Qed.

Global Instancecmra_comm_L : Comm (=) (@op A _).
  Proof. intros x y. unfold_leibniz. by rewrite comm. Qed.

Lemma cmra_pcore_l_Lx cx : pcore x = Some cx → cx ⋅ x = x.
  Proof. unfold_leibniz. apply cmra_pcore_l'. Qed.

Lemma cmra_pcore_idemp_Lx cx : pcore x = Some cx → pcore cx = Some cx.
  Proof. unfold_leibniz. apply cmra_pcore_idemp'. Qed.

Lemma cmra_op_opM_assoc_Lx y mz : (x ⋅ y) ⋅? mz = x ⋅ (y ⋅? mz).
  Proof. unfold_leibniz. apply cmra_op_opM_assoc. Qed.

Lemma cmra_pcore_r_Lx cx : pcore x = Some cx → x ⋅ cx = x.
  Proof. unfold_leibniz. apply cmra_pcore_r'. Qed.

Lemma cmra_pcore_dup_Lx cx : pcore x = Some cx → cx = cx ⋅ cx.
  Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.

Lemma core_id_dup_Lx `{!CoreId x} : x = x ⋅ x.
  Proof. unfold_leibniz. by apply core_id_dup. Qed.

Lemma cmra_core_r_Lx : x ⋅ core x = x.
    Proof. unfold_leibniz. apply cmra_core_r. Qed.

Lemma cmra_core_l_Lx : core x ⋅ x = x.
    Proof. unfold_leibniz. apply cmra_core_l. Qed.

Lemma cmra_core_idemp_Lx : core (core x) = core x.
    Proof. unfold_leibniz. apply cmra_core_idemp. Qed.

Lemma cmra_core_dup_Lx : core x = core x ⋅ core x.
    Proof. unfold_leibniz. apply cmra_core_dup. Qed.

Lemma core_id_total_Lx : CoreId x ↔ core x = x.
    Proof. unfold_leibniz. apply core_id_total. Qed.

Lemma core_id_core_Lx `{!CoreId x} : core x = x.
    Proof. by apply core_id_total_L. Qed.

Local SetDefault Proof Using "Type*".
  Context {SI : sidx} {A : ucmra} `{!LeibnizEquiv A}.
  Implicit Types x y z : A.

Global Instanceucmra_unit_left_id_L : LeftId (=) ε (@op A _).
  Proof. intros x. unfold_leibniz. by rewrite left_id. Qed.

Global Instanceucmra_unit_right_id_L : RightId (=) ε (@op A _).
  Proof. intros x. unfold_leibniz. by rewrite right_id. Qed.

Lemma cmra_total_mixin: CmraMixin A.
  Proof using Type*.
    split; auto.
    - intros n x y ? Hcx%core_ne Hx; move: Hcx. rewrite /core /= Hx /=.
      case (total y)=> [cy ->]; eauto.
    - intros x cx Hcx. move: (core_l x). by rewrite /core /= Hcx.
    - intros x cx Hcx. move: (core_idemp x). rewrite /core /= Hcx /=.
      case (total cx)=>[ccx ->]; by constructor.
    - intros x y cx Hxy%core_mono Hx. move: Hxy.
      rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
  Qed.

Global Instancecmra_morphism_id {SI : sidx} {A : cmra} : CmraMorphism (@id A).
Proof.
  split => /=.
  - apply _.
  - done.
  - intros. by rewrite option_fmap_id.
  - done.
Qed.

Global Instancecmra_morphism_proper {SI : sidx}
    {A B : cmra} (f : A → B) `{!CmraMorphism f} :
  Proper ((≡) ==> (≡)) f := ne_proper _.

Global Instancecmra_morphism_compose {SI : sidx}
    {A B C : cmra} (f : A → B) (g : B → C) :
  CmraMorphism f → CmraMorphism g → CmraMorphism (g ∘ f).
Proof.
  split.
  - apply _.
  - move=> n x Hx /=. by apply cmra_morphism_validN, cmra_morphism_validN.
  - move=> x /=. by rewrite option_fmap_compose !cmra_morphism_pcore.
  - move=> x y /=. by rewrite !cmra_morphism_op.
Qed.

Local SetDefault Proof Using "Type*".
  Context {SI : sidx} {A B : cmra} (f : A → B) `{!CmraMorphism f}.

Lemma cmra_morphism_corex : f (core x) ≡ core (f x).
  Proof. unfold core. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.

Lemma cmra_morphism_monotonex y : x ≼ y → f x ≼ f y.
  Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.

Lemma cmra_morphism_monotoneNn x y : x ≼{n} y → f x ≼{n} f y.
  Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.

Lemma cmra_morphism_validx : ✓ x → ✓ f x.
  Proof. rewrite !cmra_valid_validN; eauto using cmra_morphism_validN. Qed.

Record rFunctor{SI : sidx} := RFunctor {
  rFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, cmra;
  rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
  rFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    NonExpansive (@rFunctor_map A1 _ A2 _ B1 _ B2 _);
  rFunctor_map_id `{!Cofe A, !Cofe B} (x : rFunctor_car A B) :
    rFunctor_map (cid,cid) x ≡ x;
  rFunctor_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 :
    rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
  rFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
      (fg : (A2 -n> A1) * (B1 -n> B2)) :
    CmraMorphism (rFunctor_map fg)
}.

Global ExistingInstances rFunctor_map_ne rFunctor_mor.

Global Instance: Params (@rFunctor_map) 10 := {}.
Declare Scope rFunctor_scope.
Delimit Scope rFunctor_scope with RF.
Bind Scope rFunctor_scope with rFunctor.

Class rFunctorContractive{SI : sidx} (F : rFunctor) :=
  #[global] rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} ::
    Contractive (@rFunctor_map SI F A1 _ A2 _ B1 _ B2 _).

Global HintMode rFunctorContractive - ! : typeclass_instances.

Definition rFunctor_apply{SI : sidx} (F: rFunctor) (A: ofe) `{!Cofe A} : cmra :=
  rFunctor_car F A A.

Program DefinitionrFunctor_to_oFunctor {SI : sidx} (F: rFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := rFunctor_car F A B;
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := rFunctor_map F fg
|}.
Next Obligation.
  intros ? F A ? B ? x. simpl in *. apply rFunctor_map_id.
Qed.
Next Obligation.
  intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
  apply rFunctor_map_compose.
Qed.

Global InstancerFunctor_to_oFunctor_contractive {SI : sidx} F :
  rFunctorContractive F → oFunctorContractive (rFunctor_to_oFunctor F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg. apply rFunctor_map_contractive. done.
Qed.

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

Global InstancerFunctor_oFunctor_compose_contractive_1
    {SI : sidx} (F1 : rFunctor) (F2 : oFunctor)
    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
  rFunctorContractive F1 → rFunctorContractive (rFunctor_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 InstancerFunctor_oFunctor_compose_contractive_2
    {SI : sidx} (F1 : rFunctor) (F2 : oFunctor)
    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
  oFunctorContractive F2 → rFunctorContractive (rFunctor_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 DefinitionconstRF {SI : sidx} (B : cmra) : rFunctor :=
  {| rFunctor_car A1 _ A2 _ := B; rFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
Solve Obligations with done.

Coercion constRF: cmra >-> rFunctor.

Global InstanceconstRF_contractive {SI : sidx} B : rFunctorContractive (constRF B).
Proof. rewrite /rFunctorContractive; apply _. Qed.

Record urFunctor{SI : sidx} := URFunctor {
  urFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ucmra;
  urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
  urFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
    NonExpansive (@urFunctor_map A1 _ A2 _ B1 _ B2 _);
  urFunctor_map_id `{!Cofe A, !Cofe B} (x : urFunctor_car A B) :
    urFunctor_map (cid,cid) x ≡ x;
  urFunctor_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 :
    urFunctor_map (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x);
  urFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
      (fg : (A2 -n> A1) * (B1 -n> B2)) :
    CmraMorphism (urFunctor_map fg)
}.

Global ExistingInstances urFunctor_map_ne urFunctor_mor.

Global Instance: Params (@urFunctor_map) 10 := {}.
Declare Scope urFunctor_scope.
Delimit Scope urFunctor_scope with URF.
Bind Scope urFunctor_scope with urFunctor.

Class urFunctorContractive{SI : sidx} (F : urFunctor) :=
  #[global] urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} ::
    Contractive (@urFunctor_map SI F A1 _ A2 _ B1 _ B2 _).

Global HintMode urFunctorContractive - ! : typeclass_instances.

Definition urFunctor_apply{SI : sidx} (F: urFunctor) (A: ofe) `{!Cofe A} : ucmra :=
  urFunctor_car F A A.

Program DefinitionurFunctor_to_rFunctor {SI : sidx} (F: urFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := urFunctor_car F A B;
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := urFunctor_map F fg
|}.
Next Obligation.
  intros ? F A ? B ? x. simpl in *. apply urFunctor_map_id.
Qed.
Next Obligation.
  intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
  apply urFunctor_map_compose.
Qed.

Global InstanceurFunctor_to_rFunctor_contractive {SI : sidx} F :
  urFunctorContractive F → rFunctorContractive (urFunctor_to_rFunctor F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg. apply urFunctor_map_contractive. done.
Qed.

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

Global InstanceurFunctor_oFunctor_compose_contractive_1
    {SI : sidx} (F1 : urFunctor) (F2 : oFunctor)
    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
  urFunctorContractive F1 → urFunctorContractive (urFunctor_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 InstanceurFunctor_oFunctor_compose_contractive_2
    {SI : sidx} (F1 : urFunctor) (F2 : oFunctor)
    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
  oFunctorContractive F2 → urFunctorContractive (urFunctor_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 DefinitionconstURF {SI : sidx} (B : ucmra) : urFunctor :=
  {| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
Solve Obligations with done.

Coercion constURF: ucmra >-> urFunctor.

Global InstanceconstURF_contractive {SI : sidx} B :
  urFunctorContractive (constURF B).
Proof. rewrite /urFunctorContractive; apply _. Qed.

Definition cmra_transport{SI : sidx} {A B : cmra} (H : A = B) (x : A) : B :=
  eq_rect A id x _ H.

Lemma cmra_transport_trans{SI : sidx} {A B C : cmra} (H1 : A = B) (H2 : B = C) x :
  cmra_transport H2 (cmra_transport H1 x) = cmra_transport (eq_trans H1 H2) x.
Proof. by destruct H2. Qed.

Notation T:= (cmra_transport H).

Global Instancecmra_transport_ne : NonExpansive T.
  Proof. by intros ???; destruct H. Qed.

Global Instancecmra_transport_proper : Proper ((≡) ==> (≡)) T.
  Proof. by intros ???; destruct H. Qed.

Lemma cmra_transport_opx y : T (x ⋅ y) = T x ⋅ T y.
  Proof. by destruct H. Qed.

Lemma cmra_transport_corex : T (core x) = core (T x).
  Proof. by destruct H. Qed.

Lemma cmra_transport_validNn x : ✓{n} T x ↔ ✓{n} x.
  Proof. by destruct H. Qed.

Lemma cmra_transport_validx : ✓ T x ↔ ✓ x.
  Proof. by destruct H. Qed.

Global Instancecmra_transport_discrete x : Discrete x → Discrete (T x).
  Proof. by destruct H. Qed.

Global Instancecmra_transport_core_id x : CoreId x → CoreId (T x).
  Proof. by destruct H. Qed.

Record RAMixinA `{Equiv A, PCore A, Op A, Valid A} := {

Local SetDefault Proof Using "Type*".
  Context {SI : sidx} `{!Equiv A, !PCore A, !Op A, !Valid A}.
  Context (Heq : @Equivalence A (≡)).
  Context (ra_mix : RAMixin A).
  Existing Instances discrete_dist.

Local Instancediscrete_validN_instance : ValidN A := λ n x, ✓ x.

Definition discrete_cmra_mixin: CmraMixin A.
  Proof.
    destruct ra_mix; split; try done.
    - intros x; split; first done. by move=> /(_ 0ᵢ).
    - intros n x y1 y2 ??; by exists y1, y2.
  Qed.

Local Instancediscrete_cmra_discrete :
    CmraDiscrete (Cmra' A (discrete_ofe_mixin Heq) discrete_cmra_mixin).
  Proof. split; first apply _. done. Qed.

Notation discreteRA ra_mix :=
  (Cmra A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
  (only parsing).

Local SetDefault Proof Using "Type*".
  Context A `{Equiv A, PCore A, Op A, Valid A}.
  Context (total : ∀ x : A, is_Some (pcore x)).
  Context (op_proper : ∀ x : A, Proper ((≡) ==> (≡)) (op x)).
  Context (core_proper: Proper ((≡) ==> (≡)) (@core A _)).
  Context (valid_proper : Proper ((≡) ==> impl) (@valid A _)).
  Context (op_assoc : Assoc (≡) (@op A _)).
  Context (op_comm : Comm (≡) (@op A _)).
  Context (core_l : ∀ x : A, core x ⋅ x ≡ x).
  Context (core_idemp : ∀ x : A, core (core x) ≡ core x).
  Context (core_mono : ∀ x y : A, x ≼ y → core x ≼ core y).
  Context (valid_op_l : ∀ x y : A, ✓ (x ⋅ y) → ✓ x).

Lemma ra_total_mixin: RAMixin A.
  Proof.
    split; auto.
    - intros x y ? Hcx%core_proper Hx; move: Hcx. rewrite /core /= Hx /=.
      case (total y)=> [cy ->]; eauto.
    - intros x cx Hcx. move: (core_l x). by rewrite /core /= Hcx.
    - intros x cx Hcx. move: (core_idemp x). rewrite /core /= Hcx /=.
      case (total cx)=>[ccx ->]; by constructor.
    - intros x y cx Hxy%core_mono Hx. move: Hxy.
      rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
  Qed.

Local Instanceunit_valid_instance : Valid () := λ x, True.

Local Instanceunit_validN_instance : ValidN () := λ n x, True.

Local Instanceunit_pcore_instance : PCore () := λ x, Some x.

Local Instanceunit_op_instance : Op () := λ x y, ().

Lemma unit_cmra_mixin: CmraMixin ().
  Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
  Canonical Structure unitR : cmra := Cmra unit unit_cmra_mixin.

Local Instanceunit_unit_instance : Unit () := ().

Lemma unit_ucmra_mixin: UcmraMixin ().
  Proof. done. Qed.
  Canonical Structure unitUR : ucmra := Ucmra unit unit_ucmra_mixin.

Global Instanceunit_cmra_discrete : CmraDiscrete unitR.
  Proof. done. Qed.

Global Instanceunit_core_id (x : ()) : CoreId x.
  Proof. by constructor. Qed.

Global Instanceunit_cancelable (x : ()) : Cancelable x.
  Proof. by constructor. Qed.

Local InstanceEmpty_set_valid_instance : Valid Empty_set := λ x, False.

Local InstanceEmpty_set_validN_instance : ValidN Empty_set := λ n x, False.

Local InstanceEmpty_set_pcore_instance : PCore Empty_set := λ x, Some x.

Local InstanceEmpty_set_op_instance : Op Empty_set := λ x y, x.

Lemma Empty_set_cmra_mixin: CmraMixin Empty_set.
  Proof. apply discrete_cmra_mixin, ra_total_mixin; by (intros [] || done). Qed.
  Canonical Structure Empty_setR : cmra := Cmra Empty_set Empty_set_cmra_mixin.

Global InstanceEmpty_set_cmra_discrete : CmraDiscrete Empty_setR.
  Proof. done. Qed.

Global InstanceEmpty_set_core_id (x : Empty_set) : CoreId x.
  Proof. by constructor. Qed.

Global InstanceEmpty_set_cancelable (x : Empty_set) : Cancelable x.
  Proof. by constructor. Qed.

Local Argumentspcore _ _ !_ /.

Local Argumentscmra_pcore _ !_/.

Local Instanceprod_op_instance : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).

Local Instanceprod_pcore_instance : PCore (A * B) := λ x,
    c1 ← pcore (x.1); c2 ← pcore (x.2); Some (c1, c2).

Local Argumentsprod_pcore_instance !_ /.

Local Instanceprod_valid_instance : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.

Local Instanceprod_validN_instance : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.

Lemma prod_pcore_Some(x cx : A * B) :
    pcore x = Some cx ↔ pcore (x.1) = Some (cx.1) ∧ pcore (x.2) = Some (cx.2).
  Proof. destruct x, cx; by intuition simplify_option_eq. Qed.

Lemma prod_pcore_Some'(x cx : A * B) :
    pcore x ≡ Some cx ↔ pcore (x.1) ≡ Some (cx.1) ∧ pcore (x.2) ≡ Some (cx.2).
  Proof.
    split; [by intros (cx'&[-> ->]%prod_pcore_Some&<-)%Some_equiv_eq|].
    rewrite {3}/pcore /prod_pcore_instance.
    intros [Hx1 Hx2]; inversion_clear Hx1; simpl; inversion_clear Hx2.
    by constructor.
  Qed.

Lemma prod_included(x y : A * B) : x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
  Proof.
    split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
    intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
  Qed.

Lemma prod_includedN(x y : A * B) n : x ≼{n} y ↔ x.1 ≼{n} y.1 ∧ x.2 ≼{n} y.2.
  Proof.
    split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
    intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
  Qed.

Definition prod_cmra_mixin: CmraMixin (A * B).
  Proof.
    split; try apply _.
    - by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
    - intros n x y cx; setoid_rewrite prod_pcore_Some=> -[??] [??].
      destruct (cmra_pcore_ne n (x.1) (y.1) (cx.1)) as (z1&->&?); auto.
      destruct (cmra_pcore_ne n (x.2) (y.2) (cx.2)) as (z2&->&?); auto.
      exists (z1,z2); repeat constructor; auto.
    - by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
    - intros x; split.
      + intros [??] n; split; by apply cmra_valid_validN.
      + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
    - intros n m x [??]; split; by eapply cmra_validN_le.
    - by split; rewrite /= assoc.
    - by split; rewrite /= comm.
    - intros x y [??]%prod_pcore_Some;
        constructor; simpl; eauto using cmra_pcore_l.
    - intros x y; rewrite prod_pcore_Some prod_pcore_Some'.
      naive_solver eauto using cmra_pcore_idemp.
    - intros x y cx; rewrite prod_included prod_pcore_Some=> -[??] [??].
      destruct (cmra_pcore_mono (x.1) (y.1) (cx.1)) as (z1&?&?); auto.
      destruct (cmra_pcore_mono (x.2) (y.2) (cx.2)) as (z2&?&?); auto.
      exists (z1,z2). by rewrite prod_included prod_pcore_Some.
    - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
    - intros n x y1 y2 [??] [??]; simpl in *.
      destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z11&z12&?&?&?); auto.
      destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z21&z22&?&?&?); auto.
      by exists (z11,
...

Lemma pair_op(a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').
  Proof. done. Qed.

Lemma pair_valid(a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
  Proof. done. Qed.

Lemma pair_validN(a : A) (b : B) n : ✓{n} (a, b) ↔ ✓{n} a ∧ ✓{n} b.
  Proof. done. Qed.

Lemma pair_included(a a' : A) (b b' : B) :
    (a, b) ≼ (a', b') ↔ a ≼ a' ∧ b ≼ b'.
  Proof. apply prod_included. Qed.

Lemma pair_includedN(a a' : A) (b b' : B) n :
    (a, b) ≼{n} (a', b') ↔ a ≼{n} a' ∧ b ≼{n} b'.
  Proof. apply prod_includedN. Qed.

Lemma pair_pcore(a : A) (b : B) :
    pcore (a, b) = c1 ← pcore a; c2 ← pcore b; Some (c1, c2).
  Proof. done. Qed.

Lemma pair_core`{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
    core (a, b) = (core a, core b).
  Proof.
    rewrite /core {1}/pcore /=.
    rewrite (cmra_pcore_core a) /= (cmra_pcore_core b). done.
  Qed.

Global Instanceprod_cmra_total : CmraTotal A → CmraTotal B → CmraTotal prodR.
  Proof.
    intros H1 H2 [a b]. destruct (H1 a) as [ca ?], (H2 b) as [cb ?].
    exists (ca,cb); by simplify_option_eq.
  Qed.

Global Instanceprod_cmra_discrete :
    CmraDiscrete A → CmraDiscrete B → CmraDiscrete prodR.
  Proof. split; [apply _|]. by intros ? []; split; apply cmra_discrete_valid. Qed.

Lemma pair_core_idx y :
    CoreId x → CoreId y → CoreId (x,y).
  Proof. by rewrite /CoreId prod_pcore_Some'. Qed.

Global Instancepair_exclusive_l x y : Exclusive x → Exclusive (x,y).
  Proof. by intros ?[][?%exclusive0_l]. Qed.

Global Instancepair_exclusive_r x y : Exclusive y → Exclusive (x,y).
  Proof. by intros ?[][??%exclusive0_l]. Qed.

Global Instancepair_cancelable x y :
    Cancelable x → Cancelable y → Cancelable (x,y).
  Proof. intros ???[][][][]. constructor; simpl in *; by eapply cancelableN. Qed.

Global Instancepair_id_free_l x y : IdFree x → IdFree (x,y).
  Proof. move=> Hx [a b] [? _] [/=? _]. apply (Hx a); eauto. Qed.

Global Instancepair_id_free_r x y : IdFree y → IdFree (x,y).
  Proof. move=> Hy [a b] [_ ?] [_ /=?]. apply (Hy b); eauto. Qed.

Global HintExtern 4 (CoreId _) =>
  notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.

Global ArgumentsprodR {_} _ _.

Local Instanceprod_unit_instance `{Unit A, Unit B} : Unit (A * B) := (ε, ε).

Lemma prod_ucmra_mixin: UcmraMixin (A * B).
  Proof.
    split.
    - split; apply ucmra_unit_valid.
    - by split; rewrite /=left_id.
    - rewrite prod_pcore_Some'; split; apply (core_id _).
  Qed.
  Canonical Structure prodUR := Ucmra (prod A B) prod_ucmra_mixin.

Lemma pair_split(a : A) (b : B) : (a, b) ≡ (a, ε) ⋅ (ε, b).
  Proof. by rewrite -pair_op left_id right_id. Qed.

Lemma pair_split_L`{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
    (x, y) = (x, ε) ⋅ (ε, y).
  Proof. unfold_leibniz. apply pair_split. Qed.

Lemma pair_op_1(a a': A) : (a ⋅ a', ε) ≡@{A*B} (a, ε) ⋅ (a', ε).
  Proof. by rewrite -pair_op ucmra_unit_left_id. Qed.

Lemma pair_op_1_L`{!LeibnizEquiv A, !LeibnizEquiv B} (a a': A) :
    (a ⋅ a', ε) =@{A*B} (a, ε) ⋅ (a', ε).
  Proof. unfold_leibniz. apply pair_op_1. Qed.

Lemma pair_op_2(b b': B) : (ε, b ⋅ b') ≡@{A*B} (ε, b) ⋅ (ε, b').
  Proof. by rewrite -pair_op ucmra_unit_left_id. Qed.

Lemma pair_op_2_L`{!LeibnizEquiv A, !LeibnizEquiv B} (b b': B) :
    (ε, b ⋅ b') =@{A*B} (ε, b) ⋅ (ε, b').
  Proof. unfold_leibniz. apply pair_op_2. Qed.

Global ArgumentsprodUR {_} _ _.

Global Instanceprod_map_cmra_morphism
    {SI : sidx} {A A' B B' : cmra} (f : A → A') (g : B → B') :
  CmraMorphism f → CmraMorphism g → CmraMorphism (prod_map f g).
Proof.
  split; first apply _.
  - by intros n x [??]; split; simpl; apply cmra_morphism_validN.
  - intros [x1 x2]. rewrite /= !pair_pcore /=.
    pose proof (Hf := cmra_morphism_pcore f (x1)).
    destruct (pcore (f (x1))), (pcore (x1)); inv Hf=>//=.
    pose proof (Hg := cmra_morphism_pcore g (x2)).
    destruct (pcore (g (x2))), (pcore (x2)); inv Hg=>//=.
    by setoid_subst.
  - intros. by rewrite /prod_map /= !cmra_morphism_op.
Qed.

Program DefinitionprodRF {SI : sidx} (F1 F2 : rFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    prodO_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
|}.
Next Obligation.
  intros ? F1 F2 A1 ? A2 ? B1 ? B2 ? n ???.
  by apply prodO_map_ne; apply rFunctor_map_ne.
Qed.
Next Obligation. by intros ? F1 F2 A ? B ? [??]; rewrite /= !rFunctor_map_id. Qed.
Next Obligation.
  intros ? F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
  by rewrite !rFunctor_map_compose.
Qed.

Global InstanceprodRF_contractive {SI : sidx} F1 F2 :
  rFunctorContractive F1 → rFunctorContractive F2 →
  rFunctorContractive (prodRF F1 F2).
Proof.
  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
    by apply prodO_map_ne; apply rFunctor_map_contractive.
Qed.

Program DefinitionprodURF {SI : sidx} (F1 F2 : urFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    prodO_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
|}.
Next Obligation.
  intros ? F1 F2 A1 ? A2 ? B1 ? B2 ? n ???.
  by apply prodO_map_ne; apply urFunctor_map_ne.
Qed.
Next Obligation. by intros ? F1 F2 A ? B ? [??]; rewrite /= !urFunctor_map_id. Qed.
Next Obligation.
  intros ? F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
  by rewrite !urFunctor_map_compose.
Qed.

Global InstanceprodURF_contractive {SI : sidx} F1 F2 :
  urFunctorContractive F1 → urFunctorContractive F2 →
  urFunctorContractive (prodURF F1 F2).
Proof.
  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
    by apply prodO_map_ne; apply urFunctor_map_contractive.
Qed.

Local Argumentscore _ _ !_ /.

Local Argumentspcore _ _ !_ /.

Local Instanceoption_valid_instance : Valid (option A) := λ ma,
    match ma with Some a => ✓ a | None => True end.

Local Instanceoption_validN_instance : ValidN (option A) := λ n ma,
    match ma with Some a => ✓{n} a | None => True end.

Local Instanceoption_pcore_instance : PCore (option A) := λ ma,
    Some (ma ≫= pcore).

Local Argumentsoption_pcore_instance !_ /.

Local Instanceoption_op_instance : Op (option A) :=
    union_with (λ a b, Some (a ⋅ b)).

Definition Some_valida : ✓ Some a ↔ ✓ a := reflexivity _.

Definition Some_validNa n : ✓{n} Some a ↔ ✓{n} a := reflexivity _.

Definition Some_opa b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl.

Lemma Some_core`{!CmraTotal A} a : Some (core a) = core (Some a).
  Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.

Lemma pcore_Somea : pcore (Some a) = Some (pcore a).
  Proof. done. Qed.

Lemma Some_op_opMa ma : Some a ⋅ ma = Some (a ⋅? ma).
  Proof. by destruct ma. Qed.

Lemma option_includedma mb :
    ma ≼ mb ↔ ma = None ∨ ∃ a b, ma = Some a ∧ mb = Some b ∧ (a ≡ b ∨ a ≼ b).
  Proof.
    split.
    - intros [mc Hmc].
      destruct ma as [a|]; [right|by left].
      destruct mb as [b|]; [exists a, b|destruct mc; inversion_clear Hmc].
      destruct mc as [c|]; inversion_clear Hmc; split_and?; auto;
        setoid_subst; eauto.
    - intros [->|(a&b&->&->&[Hc|[c Hc]])].
      + exists mb. by destruct mb.
      + exists None; by constructor.
      + exists (Some c); by constructor.
  Qed.

Lemma option_included_total`{!CmraTotal A} ma mb :
    ma ≼ mb ↔ ma = None ∨ ∃ a b, ma = Some a ∧ mb = Some b ∧ a ≼ b.
  Proof.
    rewrite option_included. split; last naive_solver.
    intros [->|(a&b&->&->&[Hab|?])]; [by eauto| |by eauto 10].
    right. exists a, b. by rewrite {3}Hab.
  Qed.

Lemma option_includedNn ma mb :
    ma ≼{n} mb ↔ ma = None ∨
                 ∃ x y, ma = Some x ∧ mb = Some y ∧ (x ≡{n}≡ y ∨ x ≼{n} y).
  Proof.
    split.
    - intros [mc Hmc].
      destruct ma as [a|]; [right|by left].
      destruct mb as [b|]; [exists a, b|destruct mc; inversion_clear Hmc].
      destruct mc as [c|]; inversion_clear Hmc; split_and?; auto;
        ofe_subst; eauto using cmra_includedN_l.
    - intros [->|(a&y&->&->&[Hc|[c Hc]])].
      + exists mb. by destruct mb.
      + exists None; by constructor.
      + exists (Some c); by constructor.
  Qed.

Lemma option_includedN_total`{!CmraTotal A} n ma mb :
    ma ≼{n} mb ↔ ma = None ∨ ∃ a b, ma = Some a ∧ mb = Some b ∧ a ≼{n} b.
  Proof.
    rewrite option_includedN. split; last naive_solver.
    intros [->|(a&b&->&->&[Hab|?])]; [by eauto| |by eauto 10].
    right. exists a, b. by rewrite {3}Hab.
  Qed.

Lemma option_cmra_mixin: CmraMixin (option A).
  Proof.
    apply cmra_total_mixin.
    - eauto.
    - by intros [a|] n; destruct 1; constructor; ofe_subst.
    - destruct 1; by ofe_subst.
    - by destruct 1; rewrite /validN /option_validN_instance //=; ofe_subst.
    - intros [a|]; [apply cmra_valid_validN|done].
    - intros n m [a|];
        unfold validN, option_validN_instance; eauto using cmra_validN_le.
    - intros [a|] [b|] [c|]; constructor; rewrite ?assoc; auto.
    - intros [a|] [b|]; constructor; rewrite 1?comm; auto.
    - intros [a|]; simpl; auto.
      destruct (pcore a) as [ca|] eqn:?; constructor; eauto using cmra_pcore_l.
    - intros [a|]; simpl; auto.
      destruct (pcore a) as [ca|] eqn:?; simpl; eauto using cmra_pcore_idemp.
    - intros ma mb; setoid_rewrite option_included.
      intros [->|(a&b&->&->&[?|?])]; simpl; eauto.
      + destruct (pcore a) as [ca|] eqn:?; eauto.
        destruct (cmra_pcore_proper a b ca) as (?&?&?); eauto 10.
      + destruct (pcore a) as [ca|] eqn:?; eauto.
        destruct (cmra_pcore_mono a b ca) as (?&?&?); eauto 10.
    - intros n [a|] [b|]; rewrite /validN /option_validN_instance /=;
        eauto using cmra_validN_op_l.
    - intros n ma mb1 mb2.
      destruct ma as [a|], mb1 as [b1|], mb2 as [b2|]; intros Hx Hx';
        (try by exfalso; inversion Hx'); (try (apply (inj Some) in Hx')).
      + destruct (cmra_extend n a b1 b2) as (c1&c2&?&?&?); auto.
        by exists (Some c1), (Some c2); repeat constructor.
      + by exists (Some a)
...

Global Instanceoption_cmra_discrete : CmraDiscrete A → CmraDiscrete optionR.
  Proof. split; [apply _|]. by intros [a|]; [apply (cmra_discrete_valid a)|]. Qed.

Local Instanceoption_unit_instance : Unit (option A) := None.

Lemma option_ucmra_mixin: UcmraMixin optionR.
  Proof. split; [done|  |done]. by intros []. Qed.
  Canonical Structure optionUR := Ucmra (option A) option_ucmra_mixin.

Lemma op_Nonema mb : ma ⋅ mb = None ↔ ma = None ∧ mb = None.
  Proof. destruct ma, mb; naive_solver. Qed.

Lemma op_is_Somema mb : is_Some (ma ⋅ mb) ↔ is_Some ma ∨ is_Some mb.
  Proof. rewrite -!not_eq_None_Some op_None. destruct ma, mb; naive_solver. Qed.

Global Instanceop_None_left_id : LeftId (=) None (@op (option A) _).
  Proof. intros [a|]; done. Qed.

Global Instanceop_None_right_id : RightId (=) None (@op (option A) _).
  Proof. intros [a|]; done. Qed.

Lemma cmra_opM_opM_assoca mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? (mb ⋅ mc).
  Proof. destruct mb, mc; by rewrite /= -?assoc. Qed.

Lemma cmra_opM_opM_assoc_L`{!LeibnizEquiv A} a mb mc :
    a ⋅? mb ⋅? mc = a ⋅? (mb ⋅ mc).
  Proof. unfold_leibniz. apply cmra_opM_opM_assoc. Qed.

Lemma cmra_opM_opM_swapa mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? mc ⋅? mb.
  Proof. by rewrite !cmra_opM_opM_assoc (comm _ mb). Qed.

Lemma cmra_opM_opM_swap_L`{!LeibnizEquiv A} a mb mc :
    a ⋅? mb ⋅? mc = a ⋅? mc ⋅? mb.
  Proof. by rewrite !cmra_opM_opM_assoc_L (comm_L _ mb). Qed.

Lemma cmra_opM_fmap_Somema1 ma2 : ma1 ⋅? (Some <$> ma2) = ma1 ⋅ ma2.
  Proof. by destruct ma1, ma2. Qed.

Global InstanceSome_core_id a : CoreId a → CoreId (Some a).
  Proof. by constructor. Qed.

Global Instanceoption_core_id ma : (∀ x : A, CoreId x) → CoreId ma.
  Proof. intros. destruct ma; apply _. Qed.

Lemma exclusiveN_Some_ln a `{!Exclusive a} mb :
    ✓{n} (Some a ⋅ mb) → mb = None.
  Proof. destruct mb; last done. move=> /(exclusiveN_l _ a) []. Qed.

Lemma exclusiveN_Some_rn a `{!Exclusive a} mb :
    ✓{n} (mb ⋅ Some a) → mb = None.
  Proof. rewrite comm. by apply exclusiveN_Some_l. Qed.

Lemma exclusive_Some_la `{!Exclusive a} mb : ✓ (Some a ⋅ mb) → mb = None.
  Proof. destruct mb; last done. move=> /(exclusive_l a) []. Qed.

Lemma exclusive_Some_ra `{!Exclusive a} mb : ✓ (mb ⋅ Some a) → mb = None.
  Proof. rewrite comm. by apply exclusive_Some_l. Qed.

Lemma Some_includedNn a b : Some a ≼{n} Some b ↔ a ≡{n}≡ b ∨ a ≼{n} b.
  Proof. rewrite option_includedN; naive_solver. Qed.

Lemma Some_includedN_1n a b : Some a ≼{n} Some b → a ≡{n}≡ b ∨ a ≼{n} b.
  Proof. rewrite Some_includedN. auto. Qed.

Lemma Some_includedN_2n a b : a ≡{n}≡ b ∨ a ≼{n} b → Some a ≼{n} Some b.
  Proof. rewrite Some_includedN. auto. Qed.

Lemma Some_includedN_monon a b : a ≼{n} b → Some a ≼{n} Some b.
  Proof. rewrite Some_includedN. auto. Qed.

Lemma Some_includedN_refln a b : a ≡{n}≡ b → Some a ≼{n} Some b.
  Proof. rewrite Some_includedN. auto. Qed.

Lemma Some_includedN_is_Somen x mb : Some x ≼{n} mb → is_Some mb.
  Proof. rewrite option_includedN. naive_solver. Qed.

Lemma Some_includeda b : Some a ≼ Some b ↔ a ≡ b ∨ a ≼ b.
  Proof. rewrite option_included; naive_solver. Qed.

Lemma Some_included_1a b : Some a ≼ Some b → a ≡ b ∨ a ≼ b.
  Proof. rewrite Some_included. auto. Qed.

Lemma Some_included_2a b : a ≡ b ∨ a ≼ b → Some a ≼ Some b.
  Proof. rewrite Some_included. auto. Qed.

Lemma Some_included_monoa b : a ≼ b → Some a ≼ Some b.
  Proof. rewrite Some_included. auto. Qed.

Lemma Some_included_refla b : a ≡ b → Some a ≼ Some b.
  Proof. rewrite Some_included. auto. Qed.

Lemma Some_included_is_Somex mb : Some x ≼ mb → is_Some mb.
  Proof. rewrite option_included. naive_solver. Qed.

Lemma Some_includedN_opMn a b : Some a ≼{n} Some b ↔ ∃ mc, b ≡{n}≡ a ⋅? mc.
  Proof.
    rewrite /includedN. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
  Qed.

Lemma Some_included_opMa b : Some a ≼ Some b ↔ ∃ mc, b ≡ a ⋅? mc.
  Proof.
    rewrite /included. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
  Qed.

Lemma cmra_validN_Some_includedNn a b : ✓{n} a → Some b ≼{n} Some a → ✓{n} b.
  Proof. apply: (cmra_validN_includedN _ (Some _) (Some _)). Qed.

Lemma cmra_valid_Some_includeda b : ✓ a → Some b ≼ Some a → ✓ b.
  Proof. apply: (cmra_valid_included (Some _) (Some _)). Qed.

Lemma Some_includedN_total`{!CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
  Proof. rewrite Some_includedN. split; [|by eauto]. by intros [->|?]. Qed.

Lemma Some_included_total`{!CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
  Proof. rewrite Some_included. split; [|by eauto]. by intros [->|?]. Qed.

Lemma Some_includedN_exclusiven a `{!Exclusive a} b :
    Some a ≼{n} Some b → ✓{n} b → a ≡{n}≡ b.
  Proof. move=> /Some_includedN [//|/exclusive_includedN]; tauto. Qed.

Lemma Some_included_exclusivea `{!Exclusive a} b :
    Some a ≼ Some b → ✓ b → a ≡ b.
  Proof. move=> /Some_included [//|/exclusive_included]; tauto. Qed.

Lemma is_Some_includedNn ma mb : ma ≼{n} mb → is_Some ma → is_Some mb.
  Proof. rewrite -!not_eq_None_Some option_includedN. naive_solver. Qed.

Lemma is_Some_includedma mb : ma ≼ mb → is_Some ma → is_Some mb.
  Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed.

Global Instancecancelable_Some a :
    IdFree a → Cancelable a → Cancelable (Some a).
  Proof.
    intros Hirr ? n [b|] [c|] ? EQ; inversion_clear EQ.
    - constructor. by apply (cancelableN a).
    - destruct (Hirr b); [|eauto using dist_le, SIdx.le_0_l].
      by eapply (cmra_validN_op_l 0ᵢ a b), (cmra_validN_le n), SIdx.le_0_l.
    - destruct (Hirr c); [|symmetry; eauto using dist_le, SIdx.le_0_l].
      by eapply (cmra_validN_le n), SIdx.le_0_l.
    - done.
  Qed.

Global Instanceoption_cancelable (ma : option A) :
    (∀ a : A, IdFree a) → (∀ a : A, Cancelable a) → Cancelable ma.
  Proof. destruct ma; apply _. Qed.

Global ArgumentsoptionR {_} _.

Global ArgumentsoptionUR {_} _.

Lemma Some_pair_includedNn a1 a2 b1 b2 :
    Some (a1,b1) ≼{n} Some (a2,b2) → Some a1 ≼{n} Some a2 ∧ Some b1 ≼{n} Some b2.
  Proof. rewrite !Some_includedN. intros [[??]|[??]%prod_includedN]; eauto. Qed.

Lemma Some_pair_includedN_ln a1 a2 b1 b2 :
    Some (a1,b1) ≼{n} Some (a2,b2) → Some a1 ≼{n} Some a2.
  Proof. intros. eapply Some_pair_includedN. done. Qed.

Lemma Some_pair_includedN_rn a1 a2 b1 b2 :
    Some (a1,b1) ≼{n} Some (a2,b2) → Some b1 ≼{n} Some b2.
  Proof. intros. eapply Some_pair_includedN. done. Qed.

Lemma Some_pair_includedN_total_1`{!CmraTotal A} n a1 a2 b1 b2 :
    Some (a1,b1) ≼{n} Some (a2,b2) → a1 ≼{n} a2 ∧ Some b1 ≼{n} Some b2.
  Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ a1). Qed.

Lemma Some_pair_includedN_total_2`{!CmraTotal B} n a1 a2 b1 b2 :
    Some (a1,b1) ≼{n} Some (a2,b2) → Some a1 ≼{n} Some a2 ∧ b1 ≼{n} b2.
  Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ b1). Qed.

Lemma Some_pair_includeda1 a2 b1 b2 :
    Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2 ∧ Some b1 ≼ Some b2.
  Proof. rewrite !Some_included. intros [[??]|[??]%prod_included]; eauto. Qed.

Lemma Some_pair_included_la1 a2 b1 b2 :
    Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2.
  Proof. intros. eapply Some_pair_included. done. Qed.

Lemma Some_pair_included_ra1 a2 b1 b2 :
    Some (a1,b1) ≼ Some (a2,b2) → Some b1 ≼ Some b2.
  Proof. intros. eapply Some_pair_included. done. Qed.

Lemma Some_pair_included_total_1`{!CmraTotal A} a1 a2 b1 b2 :
    Some (a1,b1) ≼ Some (a2,b2) → a1 ≼ a2 ∧ Some b1 ≼ Some b2.
  Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total a1). Qed.

Lemma Some_pair_included_total_2`{!CmraTotal B} a1 a2 b1 b2 :
    Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2 ∧ b1 ≼ b2.
  Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.

Lemma option_fmap_mono{SI : sidx} {A B : cmra} (f : A → B) (ma mb : option A) :
  Proper ((≡) ==> (≡)) f →
  (∀ a b, a ≼ b → f a ≼ f b) →
  ma ≼ mb → f <$> ma ≼ f <$> mb.
Proof.
  intros ??. rewrite !option_included; intros [->|(a&b&->&->&?)]; naive_solver.
Qed.

Global Instanceoption_fmap_cmra_morphism {SI : sidx}
    {A B : cmra} (f: A → B) `{!CmraMorphism f} :
  CmraMorphism (fmap f : option A → option B).
Proof.
  split; first apply _.
  - intros n [a|] ?; rewrite /cmra_validN //=. by apply (cmra_morphism_validN f).
  - move=> [a|] //. by apply Some_proper, cmra_morphism_pcore.
  - move=> [a|] [b|] //=. by rewrite (cmra_morphism_op f).
Qed.

Program DefinitionoptionURF {SI : sidx} (F : rFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := optionUR (rFunctor_car F A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
|}.
Next Obligation.
  intros ? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
  by apply optionO_map_ne, rFunctor_map_ne.
Qed.
Next Obligation.
  intros ? F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
  apply option_fmap_equiv_ext=>y; apply rFunctor_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 rFunctor_map_compose.
Qed.

Global InstanceoptionURF_contractive {SI : sidx} F :
  rFunctorContractive F → urFunctorContractive (optionURF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
  by apply optionO_map_ne, rFunctor_map_contractive.
Qed.

Program DefinitionoptionRF {SI : sidx} (F : rFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := optionR (rFunctor_car F A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
|}.
Solve Obligations with apply @optionURF.

Global InstanceoptionRF_contractive {SI : sidx} F :
  rFunctorContractive F → rFunctorContractive (optionRF F).
Proof. apply optionURF_contractive. Qed.

Local Instancediscrete_fun_op_instance : Op (discrete_fun B) := λ f g x,
    f x ⋅ g x.

Local Instancediscrete_fun_pcore_instance : PCore (discrete_fun B) := λ f,
    Some (λ x, core (f x)).

Local Instancediscrete_fun_valid_instance : Valid (discrete_fun B) := λ f,
    ∀ x, ✓ f x.

Local Instancediscrete_fun_validN_instance : ValidN (discrete_fun B) := λ n f,
    ∀ x, ✓{n} f x.

Definition discrete_fun_lookup_opf g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.

Definition discrete_fun_lookup_coref x : (core f) x = core (f x) := eq_refl.

Lemma discrete_fun_included_spec_1(f g : discrete_fun B) x : f ≼ g → f x ≼ g x.
  Proof.
    by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op_instance (Hh x).
  Qed.

Lemma discrete_fun_included_spec`{Finite A} (f g : discrete_fun B) :
    f ≼ g ↔ ∀ x, f x ≼ g x.
  Proof.
    split; [by intros; apply discrete_fun_included_spec_1|].
    intros [h ?]%finite_choice; by exists h.
  Qed.

Lemma discrete_fun_cmra_mixin: CmraMixin (discrete_fun B).
  Proof.
    apply cmra_total_mixin.
    - eauto.
    - intros n f1 f2 f3 Hf x. by rewrite discrete_fun_lookup_op (Hf x).
    - intros n f1 f2 Hf x. by rewrite discrete_fun_lookup_core (Hf x).
    - intros n f1 f2 Hf ? x. by rewrite -(Hf x).
    - intros g; split.
      + intros Hg n i; apply cmra_valid_validN, Hg.
      + intros Hg i; apply cmra_valid_validN=> n; apply Hg.
    - intros n n' f Hf ? x. eauto using cmra_validN_le.
    - intros f1 f2 f3 x. by rewrite discrete_fun_lookup_op assoc.
    - intros f1 f2 x. by rewrite discrete_fun_lookup_op comm.
    - intros f x.
      by rewrite discrete_fun_lookup_op discrete_fun_lookup_core cmra_core_l.
    - intros f x. by rewrite discrete_fun_lookup_core cmra_core_idemp.
    - intros f1 f2 Hf12. exists (core f2)=>x. rewrite discrete_fun_lookup_op.
      apply (discrete_fun_included_spec_1 _ _ x), (cmra_core_mono (f1 x)) in Hf12.
      rewrite !discrete_fun_lookup_core. destruct Hf12 as [? ->].
      rewrite assoc -cmra_core_dup //.
    - intros n f1 f2 Hf x. apply cmra_validN_op_l with (f2 x), Hf.
    - intros n f f1 f2 Hf Hf12.
      assert (FUN := λ x, cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
      exists (λ x, projT1 (FUN x)), (λ x, proj1_sig (projT2 (FUN x))).
      split; [|split]=>x; [rewrite discrete_fun_lookup_op| |];
        by destruct (FUN x) as (?&?&?&?&?).
  Qed.
  Canonical Structure discrete_funR :=
    Cmra (discrete_fun B) discrete_fun_cmra_mixin.

Local Instancediscrete_fun_unit_instance : Unit (discrete_fun B) := λ x, ε.

Definition discrete_fun_lookup_emptyx : ε x = ε := eq_refl.

Lemma discrete_fun_ucmra_mixin: UcmraMixin (discrete_fun B).
  Proof.
    split.
    - intros x. apply ucmra_unit_valid.
    - intros f x. by rewrite discrete_fun_lookup_op left_id.
    - constructor=> x. apply core_id_core, _.
  Qed.
  Canonical Structure discrete_funUR :=
    Ucmra (discrete_fun B) discrete_fun_ucmra_mixin.

Global Instancediscrete_fun_unit_discrete :
    (∀ i, Discrete (ε : B i)) → Discrete (ε : discrete_fun B).
  Proof. intros ? f Hf x. by apply: discrete. Qed.

Global Argumentsdiscrete_funR {_ _} _.

Global Argumentsdiscrete_funUR {_ _} _.

Global Instancediscrete_fun_map_cmra_morphism
    {SI : sidx} {A} {B1 B2 : A → ucmra} (f : ∀ x, B1 x → B2 x) :
  (∀ x, CmraMorphism (f x)) → CmraMorphism (discrete_fun_map f).
Proof.
  split; first apply _.
  - intros n g Hg x. rewrite /discrete_fun_map.
    apply (cmra_morphism_validN (f _)), Hg.
  - intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
  - intros g1 g2 i.
    by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op.
Qed.

Program Definitiondiscrete_funURF
    {SI : sidx} {C} (F : C → urFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := discrete_funUR (λ c, urFunctor_car (F c) A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    discrete_funO_map (λ c, urFunctor_map (F c) fg)
|}.
Next Obligation.
  intros ? C F A1 ? A2 ? B1 ? B2 ? n ?? g.
  by apply discrete_funO_map_ne=>?; apply urFunctor_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 urFunctor_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 urFunctor_map_compose.
Qed.

Global Instancediscrete_funURF_contractive {SI : sidx} {C} (F : C → urFunctor) :
  (∀ c, urFunctorContractive (F c)) → urFunctorContractive (discrete_funURF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
  by apply discrete_funO_map_ne=> c; apply urFunctor_map_contractive.
Qed.

Lemma inj_cmra_mixin_restrict_validity{SI : sidx} {A : cmra} {B : ofe}
  `{!PCore B, !Op B, !Valid B, !ValidN B}
  (f : A → option B) (g : B → A)

Lemma iso_cmra_mixin_restrict_validity{SI : sidx} {A : cmra} {B : ofe}
  `{!PCore B, !Op B, !Valid B, !ValidN B}
  (f : A → B) (g : B → A)

Lemma iso_cmra_mixin{SI : sidx} {A : cmra} {B : ofe}
  `{!PCore B, !Op B, !Valid B, !ValidN B}
  (f : A → B) (g : B → A)