phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/cmra.v *)
Instance cmra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
Proof. apply (ne_proper _). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_r x : x ⋅ core x ≡ x.
Proof. by rewrite (comm _ x) cmra_core_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_dup x : core x ≡ core x ⋅ core x.
Proof. by rewrite -{3}(cmra_core_idemp x) cmra_core_r. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_validN n x : ✓{n} x → ✓{n} core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_valid x : ✓ x → ✓ core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
(* iris/algebra/cmra.v *)
Lemma core_id_total x : 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.
(* iris/algebra/cmra.v *)
Lemma core_id_core x `{!CoreId x} : core x ≡ x.
Proof. by apply core_id_total. Qed.
(* iris/algebra/cmra.v *)
(* Not an instance since TC search cannot solve the premise. *)
Lemma cmra_pcore_core_id x y : pcore x = Some y → CoreId y.
Proof. rewrite /CoreId. eauto using cmra_pcore_idemp. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_core_core_id x : CoreId (core x).
Proof. eapply cmra_pcore_core_id. rewrite cmra_pcore_core. done. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_included_core x : core x ≼ x.
Proof. by exists x; rewrite cmra_core_l. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_includedN_preorder n : PreOrder (@includedN SI A _ _ n).
Proof.
    split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
  Qed.
(* iris/algebra/cmra.v *)
Instance cmra_included_preorder : PreOrder (@included A _ _).
Proof.
    split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
  Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_monoN n x y : x ≼{n} y → core x ≼{n} core y.
Proof.
    intros [z ->].
    apply cmra_included_includedN, cmra_core_mono, cmra_included_l.
  Qed.
(* iris/algebra/cmra.v *)
(* ** Discrete *)
Lemma cmra_discrete_included_l x 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.
(* iris/algebra/cmra.v *)
Lemma cmra_discrete_included_r x y : Discrete y → x ≼{0ᵢ} y → x ≼ y.
Proof. intros ? [x' ?]. exists x'. by apply (discrete_0 y). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_op_discrete x1 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.
(* iris/algebra/cmra.v *)
(* ** Discrete *)
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.
(* iris/algebra/cmra.v *)
Lemma cmra_discrete_valid_iff_0 `{!CmraDiscrete A} n x : ✓{0ᵢ} x ↔ ✓{n} x.
Proof. by rewrite -!cmra_discrete_valid_iff. Qed.
(* iris/algebra/cmra.v *)
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.
(* iris/algebra/cmra.v *)
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.
(* iris/algebra/cmra.v *)
(* Cancelable elements *)
Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable SI A).
Proof. unfold Cancelable. intros x x' EQ. by setoid_rewrite EQ. Qed.
(* iris/algebra/cmra.v *)
Lemma cancelable x `{!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.
(* iris/algebra/cmra.v *)
Lemma discrete_cancelable x `{!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.
(* iris/algebra/cmra.v *)
Instance cancelable_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.
(* iris/algebra/cmra.v *)
Instance exclusive_cancelable (x : A) : Exclusive x → Cancelable x.
Proof. intros ? n z z' []%(exclusiveN_l _ x). Qed.
(* iris/algebra/cmra.v *)
(* Id-free elements *)
Instance id_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.
(* iris/algebra/cmra.v *)
Instance id_free_proper : Proper (equiv ==> iff) (@IdFree SI A).
Proof. by move=> P Q /equiv_dist /(_ 0ᵢ)=> ->. Qed.
(* iris/algebra/cmra.v *)
Lemma id_freeN_r n 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.
(* iris/algebra/cmra.v *)
Lemma id_freeN_l n n' x `{!IdFree x} y : ✓{n}x → y ⋅ x ≡{n'}≡ x → False.
Proof. rewrite comm. eauto using id_freeN_r. Qed.
(* iris/algebra/cmra.v *)
Lemma id_free_r x `{!IdFree x} y : ✓x → x ⋅ y ≡ x → False.
Proof. move=> /cmra_valid_validN ? /equiv_dist. eauto. Qed.
(* iris/algebra/cmra.v *)
Lemma id_free_l x `{!IdFree x} y : ✓x → y ⋅ x ≡ x → False.
Proof. rewrite comm. eauto using id_free_r. Qed.
(* iris/algebra/cmra.v *)
Lemma discrete_id_free x `{!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.
(* iris/algebra/cmra.v *)
Instance id_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.
(* iris/algebra/cmra.v *)
Instance id_free_op_l x y : IdFree x → Cancelable y → IdFree (x ⋅ y).
Proof. intros. rewrite comm. apply _. Qed.
(* iris/algebra/cmra.v *)
Instance exclusive_id_free x : Exclusive x → IdFree x.
Proof. intros ? z ? Hid. apply (exclusiveN_l 0ᵢ x z). by rewrite Hid. Qed.
(* iris/algebra/cmra.v *)
Lemma ucmra_unit_validN n : ✓{n} (ε:A).
Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
(* iris/algebra/cmra.v *)
Lemma ucmra_unit_leastN n x : ε ≼{n} x.
Proof. by exists x; rewrite left_id. Qed.
(* iris/algebra/cmra.v *)
Lemma ucmra_unit_least x : ε ≼ x.
Proof. by exists x; rewrite left_id. Qed.
(* iris/algebra/cmra.v *)
Instance ucmra_unit_right_id : RightId (≡) ε (@op A _).
Proof. by intros x; rewrite (comm op) left_id. Qed.
(* iris/algebra/cmra.v *)
Instance ucmra_unit_core_id : CoreId (ε:A).
Proof. apply ucmra_pcore_unit. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_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.
(* iris/algebra/cmra.v *)
Instance empty_cancelable : Cancelable (ε:A).
Proof. intros ???. by rewrite !left_id. Qed.
(* iris/algebra/cmra.v *)
(* For big ops *)
Lemma cmra_monoid : Monoid (@op A _) ε.
Proof. split; apply _. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_assoc_L : Assoc (=) (@op A _).
Proof. intros x y z. unfold_leibniz. by rewrite assoc. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_comm_L : Comm (=) (@op A _).
Proof. intros x y. unfold_leibniz. by rewrite comm. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_l_L x cx : pcore x = Some cx → cx ⋅ x = x.
Proof. unfold_leibniz. apply cmra_pcore_l'. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_idemp_L x cx : pcore x = Some cx → pcore cx = Some cx.
Proof. unfold_leibniz. apply cmra_pcore_idemp'. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_op_opM_assoc_L x y mz : (x ⋅ y) ⋅? mz = x ⋅ (y ⋅? mz).
Proof. unfold_leibniz. apply cmra_op_opM_assoc. Qed.
(* iris/algebra/cmra.v *)
(* ** Core *)
Lemma cmra_pcore_r_L x cx : pcore x = Some cx → x ⋅ cx = x.
Proof. unfold_leibniz. apply cmra_pcore_r'. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_pcore_dup_L x cx : pcore x = Some cx → cx = cx ⋅ cx.
Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.
(* iris/algebra/cmra.v *)
(* ** CoreId elements *)
Lemma core_id_dup_L x `{!CoreId x} : x = x ⋅ x.
Proof. unfold_leibniz. by apply core_id_dup. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_r_L x : x ⋅ core x = x.
Proof. unfold_leibniz. apply cmra_core_r. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_l_L x : core x ⋅ x = x.
Proof. unfold_leibniz. apply cmra_core_l. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_idemp_L x : core (core x) = core x.
Proof. unfold_leibniz. apply cmra_core_idemp. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_core_dup_L x : core x = core x ⋅ core x.
Proof. unfold_leibniz. apply cmra_core_dup. Qed.
(* iris/algebra/cmra.v *)
Lemma core_id_total_L x : CoreId x ↔ core x = x.
Proof. unfold_leibniz. apply core_id_total. Qed.
(* iris/algebra/cmra.v *)
Lemma core_id_core_L x `{!CoreId x} : core x = x.
Proof. by apply core_id_total_L. Qed.
(* iris/algebra/cmra.v *)
Instance ucmra_unit_left_id_L : LeftId (=) ε (@op A _).
Proof. intros x. unfold_leibniz. by rewrite left_id. Qed.
(* iris/algebra/cmra.v *)
Instance ucmra_unit_right_id_L : RightId (=) ε (@op A _).
Proof. intros x. unfold_leibniz. by rewrite right_id. Qed.
(* iris/algebra/cmra.v *)
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.
(* iris/algebra/cmra.v *)
(* * Properties about morphisms *)
Instance cmra_morphism_id {SI : sidx} {A : cmra} : CmraMorphism (@id A).
Proof.
  split => /=.
  - apply _.
  - done.
  - intros. by rewrite option_fmap_id.
  - done.
Qed.
(* iris/algebra/cmra.v *)
Instance cmra_morphism_proper {SI : sidx}
    {A B : cmra} (f : A → B) `{!CmraMorphism f} :
  Proper ((≡) ==> (≡)) f
:= ne_proper _.
(* iris/algebra/cmra.v *)
Instance cmra_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.
(* iris/algebra/cmra.v *)
Lemma cmra_morphism_core x : f (core x) ≡ core (f x).
Proof. unfold core. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_morphism_mono x y : x ≼ y → f x ≼ f y.
Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_morphism_monoN n x y : x ≼{n} y → f x ≼{n} f y.
Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_morphism_valid x : ✓ x → ✓ f x.
Proof. rewrite !cmra_valid_validN; eauto using cmra_morphism_validN. Qed.
(* iris/algebra/cmra.v *)
(* COFE → CMRA Functors *)
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)
}.
(* iris/algebra/cmra.v *)
Instance : Params (@rFunctor_map) 10
:= {}.
(* iris/algebra/cmra.v *)
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 _).
(* iris/algebra/cmra.v *)
Definition rFunctor_apply {SI : sidx} (F: rFunctor) (A: ofe) `{!Cofe A} : cmra
:=
  rFunctor_car F A A.
(* iris/algebra/cmra.v *)
Definition rFunctor_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.
(* iris/algebra/cmra.v *)
Instance rFunctor_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.
(* iris/algebra/cmra.v *)
Definition rFunctor_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.
(* iris/algebra/cmra.v *)
Instance rFunctor_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.
(* iris/algebra/cmra.v *)
Instance rFunctor_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.
(* iris/algebra/cmra.v *)
Definition constRF {SI : sidx} (B : cmra) : rFunctor
:=
  {| rFunctor_car A1 _ A2 _ := B; rFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
(* iris/algebra/cmra.v *)
Coercion constRF : cmra >-> rFunctor.
(* iris/algebra/cmra.v *)
Instance constRF_contractive {SI : sidx} B : rFunctorContractive (constRF B).
Proof. rewrite /rFunctorContractive; apply _. Qed.
(* iris/algebra/cmra.v *)
(* COFE → UCMRA Functors *)
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)
}.
(* iris/algebra/cmra.v *)
Instance : Params (@urFunctor_map) 10
:= {}.
(* iris/algebra/cmra.v *)
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 _).
(* iris/algebra/cmra.v *)
Definition urFunctor_apply {SI : sidx} (F: urFunctor) (A: ofe) `{!Cofe A} : ucmra
:=
  urFunctor_car F A A.
(* iris/algebra/cmra.v *)
Definition urFunctor_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.
(* iris/algebra/cmra.v *)
Instance urFunctor_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.
(* iris/algebra/cmra.v *)
Definition urFunctor_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.
(* iris/algebra/cmra.v *)
Instance urFunctor_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.
(* iris/algebra/cmra.v *)
Instance urFunctor_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.
(* iris/algebra/cmra.v *)
Definition constURF {SI : sidx} (B : ucmra) : urFunctor
:=
  {| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
(* iris/algebra/cmra.v *)
Coercion constURF : ucmra >-> urFunctor.
(* iris/algebra/cmra.v *)
Instance constURF_contractive {SI : sidx} B :
  urFunctorContractive (constURF B).
Proof. rewrite /urFunctorContractive; apply _. Qed.
(* iris/algebra/cmra.v *)
(* * Transporting a CMRA equality *)
Definition cmra_transport {SI : sidx} {A B : cmra} (H : A = B) (x : A) : B
:=
  eq_rect A id x _ H.
(* iris/algebra/cmra.v *)
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.
(* iris/algebra/cmra.v *)
Notation T
:= (cmra_transport H).
(* iris/algebra/cmra.v *)
Instance cmra_transport_ne : NonExpansive T.
Proof. by intros ???; destruct H. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_transport_proper : Proper ((≡) ==> (≡)) T.
Proof. by intros ???; destruct H. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_transport_op x y : T (x ⋅ y) = T x ⋅ T y.
Proof. by destruct H. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_transport_core x : T (core x) = core (T x).
Proof. by destruct H. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_transport_validN n x : ✓{n} T x ↔ ✓{n} x.
Proof. by destruct H. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_transport_valid x : ✓ T x ↔ ✓ x.
Proof. by destruct H. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_transport_discrete x : Discrete x → Discrete (T x).
Proof. by destruct H. Qed.
(* iris/algebra/cmra.v *)
Instance cmra_transport_core_id x : CoreId x → CoreId (T x).
Proof. by destruct H. Qed.
(* iris/algebra/cmra.v *)
(* ** Discrete CMRA *)
Record RAMixin A `{Equiv A, PCore A, Op A, Valid A}
:= {
  (* setoids *)
  ra_op_proper (x : A) : Proper ((≡) ==> (≡)) (op x);
  ra_core_proper (x y : A) cx :
    x ≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡ cy;
  ra_validN_proper : Proper ((≡@{A}) ==> impl) valid;
  (* monoid *)
  ra_assoc : Assoc (≡@{A}) (⋅);
  ra_comm : Comm (≡@{A}) (⋅);
  ra_pcore_l (x : A) cx : pcore x = Some cx → cx ⋅ x ≡ x;
  ra_pcore_idemp (x : A) cx : pcore x = Some cx → pcore cx ≡ Some cx;
  ra_pcore_mono (x y : A) cx :
    x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
  ra_valid_op_l (x y : A) : ✓ (x ⋅ y) → ✓ x
}.
(* iris/algebra/cmra.v *)
Instance discrete_validN_instance : ValidN A
:= λ n x, ✓ x.
(* iris/algebra/cmra.v *)
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.
(* iris/algebra/cmra.v *)
Instance discrete_cmra_discrete :
    CmraDiscrete (Cmra' A (discrete_ofe_mixin Heq) discrete_cmra_mixin).
Proof. split; first apply _. done. Qed.
(* iris/algebra/cmra.v *)
(* A smart constructor for the discrete RA over a carrier [A]. It uses
[ofe_discrete_equivalence_of A] to make sure the same [Equivalence] proof is
used as when constructing the OFE. *)
Notation discreteR A ra_mix
:=
  (Cmra A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
  (only parsing).
(* iris/algebra/cmra.v *)
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.
(* iris/algebra/cmra.v *)
Instance unit_valid_instance : Valid ()
:= λ x, True.
(* iris/algebra/cmra.v *)
Instance unit_validN_instance : ValidN ()
:= λ n x, True.
(* iris/algebra/cmra.v *)
Instance unit_pcore_instance : PCore ()
:= λ x, Some x.
(* iris/algebra/cmra.v *)
Instance unit_op_instance : Op ()
:= λ x y, ().
(* iris/algebra/cmra.v *)
Lemma unit_cmra_mixin : CmraMixin ().
Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
(* iris/algebra/cmra.v *)
Canonical unitR : cmra
:= Cmra unit unit_cmra_mixin.
(* iris/algebra/cmra.v *)
Instance unit_unit_instance : Unit ()
:= ().
(* iris/algebra/cmra.v *)
Lemma unit_ucmra_mixin : UcmraMixin ().
Proof. done. Qed.
(* iris/algebra/cmra.v *)
Canonical unitUR : ucmra
:= Ucmra unit unit_ucmra_mixin.
(* iris/algebra/cmra.v *)
Instance unit_cmra_discrete : CmraDiscrete unitR.
Proof. done. Qed.
(* iris/algebra/cmra.v *)
Instance unit_core_id (x : ()) : CoreId x.
Proof. by constructor. Qed.
(* iris/algebra/cmra.v *)
Instance unit_cancelable (x : ()) : Cancelable x.
Proof. by constructor. Qed.
(* iris/algebra/cmra.v *)
Instance Empty_set_valid_instance : Valid Empty_set
:= λ x, False.
(* iris/algebra/cmra.v *)
Instance Empty_set_validN_instance : ValidN Empty_set
:= λ n x, False.
(* iris/algebra/cmra.v *)
Instance Empty_set_pcore_instance : PCore Empty_set
:= λ x, Some x.
(* iris/algebra/cmra.v *)
Instance Empty_set_op_instance : Op Empty_set
:= λ x y, x.
(* iris/algebra/cmra.v *)
Lemma Empty_set_cmra_mixin : CmraMixin Empty_set.
Proof. apply discrete_cmra_mixin, ra_total_mixin; by (intros [] || done). Qed.
(* iris/algebra/cmra.v *)
Canonical Empty_setR : cmra
:= Cmra Empty_set Empty_set_cmra_mixin.
(* iris/algebra/cmra.v *)
Instance Empty_set_cmra_discrete : CmraDiscrete Empty_setR.
Proof. done. Qed.
(* iris/algebra/cmra.v *)
Instance Empty_set_core_id (x : Empty_set) : CoreId x.
Proof. by constructor. Qed.
(* iris/algebra/cmra.v *)
Instance Empty_set_cancelable (x : Empty_set) : Cancelable x.
Proof. by constructor. Qed.
(* iris/algebra/cmra.v *)
Instance prod_op_instance : Op (A * B)
:= λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
(* iris/algebra/cmra.v *)
Instance prod_pcore_instance : PCore (A * B)
:= λ x,
    c1 ← pcore (x.1); c2 ← pcore (x.2); Some (c1, c2).
(* iris/algebra/cmra.v *)
Instance prod_valid_instance : Valid (A * B)
:= λ x, ✓ x.1 ∧ ✓ x.2.
(* iris/algebra/cmra.v *)
Instance prod_validN_instance : ValidN (A * B)
:= λ n x, ✓{n} x.1 ∧ ✓{n} x.2.