Commit 83c9c1c1 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'big_rename' into 'master'

Fix some longstanding renaming issues

See merge request FP/iris-coq!63
parents d9417f9a 2a92f265
......@@ -131,7 +131,7 @@ Proof.
- destruct (elem_of_agree x1); naive_solver.
Qed.
Definition agree_cmra_mixin : CMRAMixin (agree A).
Definition agree_cmra_mixin : CmraMixin (agree A).
Proof.
apply cmra_total_mixin; try apply _ || by eauto.
- intros n x; rewrite !agree_validN_def; eauto using dist_S.
......@@ -142,19 +142,19 @@ Proof.
+ by rewrite agree_idemp.
+ by move: Hval; rewrite Hx; move=> /agree_op_invN->; rewrite agree_idemp.
Qed.
Canonical Structure agreeR : cmraT := CMRAT (agree A) agree_cmra_mixin.
Canonical Structure agreeR : cmraT := CmraT (agree A) agree_cmra_mixin.
Global Instance agree_total : CMRATotal agreeR.
Proof. rewrite /CMRATotal; eauto. Qed.
Global Instance agree_persistent (x : agree A) : Persistent x.
Global Instance agree_cmra_total : CmraTotal agreeR.
Proof. rewrite /CmraTotal; eauto. Qed.
Global Instance agree_core_id (x : agree A) : CoreId x.
Proof. by constructor. Qed.
Global Instance agree_discrete : Discrete A CMRADiscrete agreeR.
Global Instance agree_cmra_discrete : OfeDiscrete A CmraDiscrete agreeR.
Proof.
intros HD. split.
- intros x y [H H'] n; split=> a; setoid_rewrite <-(timeless_iff_0 _ _); auto.
- intros x y [H H'] n; split=> a; setoid_rewrite <-(discrete_iff_0 _ _); auto.
- intros x; rewrite agree_validN_def=> Hv n. apply agree_validN_def=> a b ??.
apply timeless_iff_0; auto.
apply discrete_iff_0; auto.
Qed.
Program Definition to_agree (a : A) : agree A :=
......@@ -267,7 +267,7 @@ Section agree_map.
- intros (a&->&?). exists (f a). rewrite -Hfg; eauto.
Qed.
Global Instance agree_map_morphism : CMRAMorphism (agree_map f).
Global Instance agree_map_morphism : CmraMorphism (agree_map f).
Proof using Hf.
split; first apply _.
- intros n x. rewrite !agree_validN_def=> Hv b b' /=.
......
......@@ -49,10 +49,10 @@ Proof.
(λ x, (authoritative x, auth_own x))); by repeat intro.
Qed.
Global Instance Auth_timeless a b :
Timeless a Timeless b Timeless (Auth a b).
Proof. by intros ?? [??] [??]; split; apply: timeless. Qed.
Global Instance auth_discrete : Discrete A Discrete authC.
Global Instance Auth_discrete a b :
Discrete a Discrete b Discrete (Auth a b).
Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
Global Instance auth_ofe_discrete : OfeDiscrete A OfeDiscrete authC.
Proof. intros ? [??]; apply _. Qed.
Global Instance auth_leibniz : LeibnizEquiv A LeibnizEquiv (auth A).
Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
......@@ -113,7 +113,7 @@ Proof.
destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN.
Qed.
Lemma auth_valid_discrete `{CMRADiscrete A} x :
Lemma auth_valid_discrete `{CmraDiscrete A} x :
x match authoritative x with
| Excl' a => auth_own x a a
| None => auth_own x
......@@ -125,18 +125,18 @@ Proof.
Qed.
Lemma auth_validN_2 n a b : {n} ( a b) b {n} a {n} a.
Proof. by rewrite auth_validN_eq /= left_id. Qed.
Lemma auth_valid_discrete_2 `{CMRADiscrete A} a b : ( a b) b a a.
Lemma auth_valid_discrete_2 `{CmraDiscrete A} a b : ( a b) b a a.
Proof. by rewrite auth_valid_discrete /= left_id. Qed.
Lemma authoritative_valid x : x authoritative x.
Proof. by destruct x as [[[]|]]. Qed.
Lemma auth_own_valid `{CMRADiscrete A} x : x auth_own x.
Lemma auth_own_valid `{CmraDiscrete A} x : x auth_own x.
Proof.
rewrite auth_valid_discrete.
destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
Qed.
Lemma auth_cmra_mixin : CMRAMixin (auth A).
Lemma auth_cmra_mixin : CmraMixin (auth A).
Proof.
apply cmra_total_mixin.
- eauto.
......@@ -166,9 +166,9 @@ Proof.
as (b1&b2&?&?&?); auto using auth_own_validN.
by exists (Auth ea1 b1), (Auth ea2 b2).
Qed.
Canonical Structure authR := CMRAT (auth A) auth_cmra_mixin.
Canonical Structure authR := CmraT (auth A) auth_cmra_mixin.
Global Instance auth_cmra_discrete : CMRADiscrete A CMRADiscrete authR.
Global Instance auth_cmra_discrete : CmraDiscrete A CmraDiscrete authR.
Proof.
split; first apply _.
intros [[[?|]|] ?]; rewrite auth_valid_eq auth_validN_eq /=; auto.
......@@ -178,17 +178,17 @@ Proof.
Qed.
Instance auth_empty : Unit (auth A) := Auth ε ε.
Lemma auth_ucmra_mixin : UCMRAMixin (auth A).
Lemma auth_ucmra_mixin : UcmraMixin (auth A).
Proof.
split; simpl.
- rewrite auth_valid_eq /=. apply ucmra_unit_valid.
- by intros x; constructor; rewrite /= left_id.
- do 2 constructor; simpl; apply (persistent_core _).
- do 2 constructor; simpl; apply (core_id_core _).
Qed.
Canonical Structure authUR := UCMRAT (auth A) auth_ucmra_mixin.
Canonical Structure authUR := UcmraT (auth A) auth_ucmra_mixin.
Global Instance auth_frag_persistent a : Persistent a Persistent ( a).
Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.
Global Instance auth_frag_core_id a : CoreId a CoreId ( a).
Proof. do 2 constructor; simpl; auto. by apply core_id_core. Qed.
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
......@@ -274,7 +274,7 @@ Proof.
apply option_fmap_ne; [|done]=> x y ?; by apply excl_map_ne.
Qed.
Instance auth_map_cmra_morphism {A B : ucmraT} (f : A B) :
CMRAMorphism f CMRAMorphism (auth_map f).
CmraMorphism f CmraMorphism (auth_map f).
Proof.
split; try apply _.
- intros n [[[a|]|] b]; rewrite !auth_validN_eq; try
......
......@@ -41,7 +41,7 @@ Hint Extern 0 (_ ≼{_} _) => reflexivity.
Section mixin.
Local Set Primitive Projections.
Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
Record CmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
(* setoids *)
mixin_cmra_op_ne (x : A) : NonExpansive (op x);
mixin_cmra_pcore_ne n x y cx :
......@@ -65,7 +65,7 @@ Section mixin.
End mixin.
(** Bundeled version *)
Structure cmraT := CMRAT' {
Structure cmraT := CmraT' {
cmra_car :> Type;
cmra_equiv : Equiv cmra_car;
cmra_dist : Dist cmra_car;
......@@ -74,14 +74,14 @@ Structure cmraT := CMRAT' {
cmra_valid : Valid cmra_car;
cmra_validN : ValidN cmra_car;
cmra_ofe_mixin : OfeMixin cmra_car;
cmra_mixin : CMRAMixin cmra_car;
cmra_mixin : CmraMixin cmra_car;
_ : Type
}.
Arguments CMRAT' _ {_ _ _ _ _ _} _ _ _.
(* Given [m : CMRAMixin A], the notation [CMRAT A m] provides a smart
Arguments CmraT' _ {_ _ _ _ _ _} _ _ _.
(* Given [m : CmraMixin A], the notation [CmraT A m] provides a smart
constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
the type [A], so that it does not have to be given manually. *)
Notation CMRAT A m := (CMRAT' A (ofe_mixin_of A%type) m A) (only parsing).
Notation CmraT A m := (CmraT' A (ofe_mixin_of A%type) m A) (only parsing).
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
......@@ -100,7 +100,7 @@ Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
Coercion cmra_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeC.
Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac A) : CMRAMixin Ac := cmra_mixin Ac.
Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac A) : CmraMixin Ac := cmra_mixin Ac.
Notation cmra_mixin_of A :=
ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).
......@@ -142,11 +142,11 @@ Definition opM {A : cmraT} (x : A) (my : option A) :=
match my with Some y => x y | None => x end.
Infix "⋅?" := opM (at level 50, left associativity) : C_scope.
(** * Persistent elements *)
Class Persistent {A : cmraT} (x : A) := persistent : pcore x Some x.
Arguments persistent {_} _ {_}.
Hint Mode Persistent + ! : typeclass_instances.
Instance: Params (@Persistent) 1.
(** * CoreId elements *)
Class CoreId {A : cmraT} (x : A) := core_id : pcore x Some x.
Arguments core_id {_} _ {_}.
Hint Mode CoreId + ! : typeclass_instances.
Instance: Params (@CoreId) 1.
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : {0} (x y) False.
......@@ -171,8 +171,8 @@ Instance: Params (@IdFree) 1.
(** * CMRAs whose core is total *)
(** The function [core] may return a dummy when used on CMRAs without total
core. *)
Class CMRATotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
Hint Mode CMRATotal ! : typeclass_instances.
Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
Hint Mode CmraTotal ! : typeclass_instances.
Class Core (A : Type) := core : A A.
Hint Mode Core ! : typeclass_instances.
......@@ -185,13 +185,13 @@ Arguments core' _ _ _ /.
Class Unit (A : Type) := ε : A.
Arguments ε {_ _}.
Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
mixin_ucmra_unit_valid : ε;
mixin_ucmra_unit_left_id : LeftId () ε ();
mixin_ucmra_pcore_unit : pcore ε Some ε
}.
Structure ucmraT := UCMRAT' {
Structure ucmraT := UcmraT' {
ucmra_car :> Type;
ucmra_equiv : Equiv ucmra_car;
ucmra_dist : Dist ucmra_car;
......@@ -201,13 +201,13 @@ Structure ucmraT := UCMRAT' {
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;
ucmra_cmra_mixin : CmraMixin ucmra_car;
ucmra_mixin : UcmraMixin ucmra_car;
_ : Type;
}.
Arguments UCMRAT' _ {_ _ _ _ _ _ _} _ _ _ _.
Notation UCMRAT A m :=
(UCMRAT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m A) (only parsing).
Arguments UcmraT' _ {_ _ _ _ _ _ _} _ _ _ _.
Notation UcmraT A m :=
(UcmraT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m A) (only parsing).
Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
......@@ -223,7 +223,7 @@ Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
Coercion ucmra_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeC.
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
CMRAT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A) A.
CmraT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A) A.
Canonical Structure ucmra_cmraR.
(** Lifting properties from the mixin *)
......@@ -239,14 +239,14 @@ Section ucmra_mixin.
End ucmra_mixin.
(** * Discrete CMRAs *)
Class CMRADiscrete (A : cmraT) := {
cmra_discrete :> Discrete A;
Class CmraDiscrete (A : cmraT) := {
cmra_discrete_ofe_discrete :> OfeDiscrete A;
cmra_discrete_valid (x : A) : {0} x x
}.
Hint Mode CMRADiscrete ! : typeclass_instances.
Hint Mode CmraDiscrete ! : typeclass_instances.
(** * Morphisms *)
Class CMRAMorphism {A B : cmraT} (f : A B) := {
Class CmraMorphism {A B : cmraT} (f : A B) := {
cmra_morphism_ne :> NonExpansive f;
cmra_morphism_validN n x : {n} x {n} f x;
cmra_morphism_pcore x : pcore (f x) f <$> pcore x;
......@@ -316,7 +316,7 @@ Proof. destruct 2; by ofe_subst. Qed.
Global Instance cmra_opM_proper : Proper (() ==> () ==> ()) (@opM A).
Proof. destruct 2; by setoid_subst. Qed.
Global Instance Persistent_proper : Proper (() ==> iff) (@Persistent A).
Global Instance CoreId_proper : Proper (() ==> iff) (@CoreId A).
Proof. solve_proper. Qed.
Global Instance Exclusive_proper : Proper (() ==> iff) (@Exclusive A).
Proof. intros x y Hxy. rewrite /Exclusive. by setoid_rewrite Hxy. Qed.
......@@ -361,8 +361,8 @@ Proof.
intros Hv Hx%cmra_pcore_l. move: Hv; rewrite -Hx. apply cmra_valid_op_l.
Qed.
(** ** Persistent elements *)
Lemma persistent_dup x `{!Persistent x} : x x x.
(** ** CoreId elements *)
Lemma core_id_dup x `{!CoreId x} : x x x.
Proof. by apply cmra_pcore_dup' with x. Qed.
(** ** Exclusive elements *)
......@@ -464,7 +464,7 @@ Qed.
(** ** Total core *)
Section total_core.
Local Set Default Proof Using "Type*".
Context `{CMRATotal A}.
Context `{CmraTotal A}.
Lemma cmra_core_l x : core x x x.
Proof.
......@@ -498,19 +498,19 @@ Section total_core.
Lemma cmra_core_valid x : x core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
Lemma persistent_total x : Persistent x core x x.
Lemma core_id_total x : CoreId x core x x.
Proof.
split; [intros; by rewrite /core /= (persistent x)|].
rewrite /Persistent /core /=.
split; [intros; by rewrite /core /= (core_id x)|].
rewrite /CoreId /core /=.
destruct (cmra_total x) as [? ->]. by constructor.
Qed.
Lemma persistent_core x `{!Persistent x} : core x x.
Proof. by apply persistent_total. Qed.
Lemma core_id_core x `{!CoreId x} : core x x.
Proof. by apply core_id_total. Qed.
Global Instance cmra_core_persistent x : Persistent (core x).
Global Instance cmra_core_core_id x : CoreId (core x).
Proof.
destruct (cmra_total x) as [cx Hcx].
rewrite /Persistent /core /= Hcx /=. eauto using cmra_pcore_idemp.
rewrite /CoreId /core /= Hcx /=. eauto using cmra_pcore_idemp.
Qed.
Lemma cmra_included_core x : core x x.
......@@ -530,34 +530,34 @@ Section total_core.
Qed.
End total_core.
(** ** Timeless *)
Lemma cmra_timeless_included_l x y : Timeless x {0} y x {0} y x y.
(** ** 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 (timeless x z).
by exists z'; rewrite Hy (discrete x z).
Qed.
Lemma cmra_timeless_included_r x y : Timeless y x {0} y x y.
Proof. intros ? [x' ?]. exists x'. by apply (timeless y). Qed.
Lemma cmra_op_timeless x1 x2 :
(x1 x2) Timeless x1 Timeless x2 Timeless (x1 x2).
Lemma cmra_discrete_included_r x y : Discrete y x {0} y x y.
Proof. intros ? [x' ?]. exists x'. by apply (discrete y). Qed.
Lemma cmra_op_discrete x1 x2 :
(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. by apply cmra_valid_validN. }
by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
by rewrite Hz' (discrete x1 y1) // (discrete x2 y2).
Qed.
(** ** Discrete *)
Lemma cmra_discrete_valid_iff `{CMRADiscrete A} n x : x {n} x.
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 with lia.
Qed.
Lemma cmra_discrete_included_iff `{Discrete A} n x y : x y x {n} y.
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 ->%(timeless_iff _ _)]; eauto using cmra_included_l.
intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
Qed.
(** Cancelable elements *)
......@@ -565,9 +565,9 @@ Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
Proof. unfold Cancelable. intros x x' EQ. by setoid_rewrite EQ. Qed.
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.
Lemma discrete_cancelable x `{CMRADiscrete A}:
Lemma discrete_cancelable x `{CmraDiscrete A}:
( y z, (x y) x y x z y z) Cancelable x.
Proof. intros ????. rewrite -!timeless_iff -cmra_discrete_valid_iff. auto. Qed.
Proof. intros ????. rewrite -!discrete_iff -cmra_discrete_valid_iff. auto. Qed.
Global Instance cancelable_op x y :
Cancelable x Cancelable y Cancelable (x y).
Proof.
......@@ -595,9 +595,11 @@ Lemma id_free_r x `{!IdFree x} y : ✓x → x ⋅ y ≡ x → False.
Proof. move=> /cmra_valid_validN ? /equiv_dist. eauto. Qed.
Lemma id_free_l x `{!IdFree x} y : x y x x False.
Proof. rewrite comm. eauto using id_free_r. Qed.
Lemma discrete_id_free x `{CMRADiscrete A}:
Lemma discrete_id_free x `{CmraDiscrete A}:
( y, x x y x False) IdFree x.
Proof. repeat intro. eauto using cmra_discrete_valid, cmra_discrete, timeless. Qed.
Proof.
intros Hx y ??. apply (Hx y), (discrete _); eauto using cmra_discrete_valid.
Qed.
Global 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) ?.
......@@ -622,13 +624,13 @@ Section ucmra.
Proof. by exists x; rewrite left_id. Qed.
Global Instance ucmra_unit_right_id : RightId () ε (@op A _).
Proof. by intros x; rewrite (comm op) left_id. Qed.
Global Instance ucmra_unit_persistent : Persistent (ε:A).
Global Instance ucmra_unit_core_id : CoreId (ε:A).
Proof. apply ucmra_pcore_unit. Qed.
Global Instance cmra_unit_total : CMRATotal A.
Global Instance cmra_unit_cmra_total : CmraTotal A.
Proof.
intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?);
eauto using ucmra_unit_least, (persistent (ε:A)).
eauto using ucmra_unit_least, (core_id (ε:A)).
Qed.
Global Instance empty_cancelable : Cancelable (ε:A).
Proof. intros ???. by rewrite !left_id. Qed.
......@@ -637,7 +639,7 @@ Section ucmra.
Global Instance cmra_monoid : Monoid (@op A _) := {| monoid_unit := ε |}.
End ucmra.
Hint Immediate cmra_unit_total.
Hint Immediate cmra_unit_cmra_total.
(** * Properties about CMRAs with Leibniz equality *)
Section cmra_leibniz.
......@@ -664,13 +666,13 @@ Section cmra_leibniz.
Lemma cmra_pcore_dup_L x cx : pcore x = Some cx cx = cx cx.
Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.
(** ** Persistent elements *)
Lemma persistent_dup_L x `{!Persistent x} : x = x x.
Proof. unfold_leibniz. by apply persistent_dup. Qed.
(** ** CoreId elements *)
Lemma core_id_dup_L x `{!CoreId x} : x = x x.
Proof. unfold_leibniz. by apply core_id_dup. Qed.
(** ** Total core *)
Section total_core.
Context `{CMRATotal A}.
Context `{CmraTotal A}.
Lemma cmra_core_r_L x : x core x = x.
Proof. unfold_leibniz. apply cmra_core_r. Qed.
......@@ -680,10 +682,10 @@ Section cmra_leibniz.
Proof. unfold_leibniz. apply cmra_core_idemp. Qed.
Lemma cmra_core_dup_L x : core x = core x core x.
Proof. unfold_leibniz. apply cmra_core_dup. Qed.
Lemma persistent_total_L x : Persistent x core x = x.
Proof. unfold_leibniz. apply persistent_total. Qed.
Lemma persistent_core_L x `{!Persistent x} : core x = x.
Proof. by apply persistent_total_L. Qed.
Lemma core_id_total_L x : CoreId x core x = x.
Proof. unfold_leibniz. apply core_id_total. Qed.
Lemma core_id_core_L x `{!CoreId x} : core x = x.
Proof. by apply core_id_total_L. Qed.
End total_core.
End cmra_leibniz.
......@@ -716,7 +718,7 @@ Section cmra_total.
Context (extend : n (x y1 y2 : A),
{n} x x {n} y1 y2
z1 z2, x z1 z2 z1 {n} y1 z2 {n} y2).
Lemma cmra_total_mixin : CMRAMixin A.
Lemma cmra_total_mixin : CmraMixin A.
Proof using Type*.
split; auto.
- intros n x y ? Hcx%core_ne Hx; move: Hcx. rewrite /core /= Hx /=.
......@@ -730,12 +732,12 @@ Section cmra_total.
End cmra_total.
(** * Properties about morphisms *)
Instance cmra_morphism_id {A : cmraT} : CMRAMorphism (@id A).
Instance cmra_morphism_id {A : cmraT} : CmraMorphism (@id A).
Proof. split=>//=. apply _. intros. by rewrite option_fmap_id. Qed.
Instance cmra_morphism_proper {A B : cmraT} (f : A B) `{!CMRAMorphism f} :
Instance cmra_morphism_proper {A B : cmraT} (f : A B) `{!CmraMorphism f} :
Proper (() ==> ()) f := ne_proper _.
Instance cmra_morphism_compose {A B C : cmraT} (f : A B) (g : B C) :
CMRAMorphism f CMRAMorphism g CMRAMorphism (g f).
CmraMorphism f CmraMorphism g CmraMorphism (g f).
Proof.
split.
- apply _.
......@@ -746,7 +748,7 @@ Qed.
Section cmra_morphism.
Local Set Default Proof Using "Type*".
Context {A B : cmraT} (f : A B) `{!CMRAMorphism f}.
Context {A B : cmraT} (f : A B) `{!CmraMorphism f}.
Lemma cmra_morphism_core x : core (f x) f (core x).
Proof. unfold core, core'. rewrite cmra_morphism_pcore. by destruct (pcore x). Qed.
Lemma cmra_morphism_monotone x y : x y f x f y.
......@@ -769,7 +771,7 @@ Structure rFunctor := RFunctor {
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
rFunctor_map (fg, g'f') x rFunctor_map (g,g') (rFunctor_map (f,f') x);
rFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
CMRAMorphism (rFunctor_map fg)
CmraMorphism (rFunctor_map fg)
}.
Existing Instances rFunctor_ne rFunctor_mor.
Instance: Params (@rFunctor_map) 5.
......@@ -802,7 +804,7 @@ Structure urFunctor := URFunctor {
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
urFunctor_map (fg, g'f') x urFunctor_map (g,g') (urFunctor_map (f,f') x);
urFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
CMRAMorphism (urFunctor_map fg)
CmraMorphism (urFunctor_map fg)
}.
Existing Instances urFunctor_ne urFunctor_mor.
Instance: Params (@urFunctor_map) 5.
......@@ -843,9 +845,9 @@ Section cmra_transport.
Proof. by destruct H. Qed.
Lemma cmra_transport_valid x : T x x.
Proof. by destruct H. Qed.
Global Instance cmra_transport_timeless x : Timeless x Timeless (T x).
Global Instance cmra_transport_discrete x : Discrete x Discrete (T x).
Proof. by destruct H. Qed.
Global Instance cmra_transport_persistent x : Persistent x Persistent (T x).
Global Instance cmra_transport_core_id x : CoreId x CoreId (T x).
Proof. by destruct H. Qed.
End cmra_transport.
......@@ -874,7 +876,7 @@ Section discrete.
Existing Instances discrete_dist.
Instance discrete_validN : ValidN A := λ n x, x.
Definition discrete_cmra_mixin : CMRAMixin A.
Definition discrete_cmra_mixin : CmraMixin A.
Proof.
destruct ra_mix; split; try done.
- intros x; split; first done. by move=> /(_ 0).
......@@ -882,15 +884,15 @@ Section discrete.
Qed.
Instance discrete_cmra_discrete :
CMRADiscrete (CMRAT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin A).
CmraDiscrete (CmraT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin A).
Proof. split. apply _. done. Qed.
End discrete.
(** A smart constructor for the discrete RA over a carrier [A]. It uses
[discrete_ofe_equivalence_of A] to make sure the same [Equivalence] proof is
[ofe_discrete_equivalence_of A] to make sure the same [Equivalence] proof is
used as when constructing the OFE. *)
Notation discreteR A ra_mix :=
(CMRAT A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
(CmraT A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
(only parsing).
Section ra_total.
......@@ -925,18 +927,18 @@ Section unit.
Instance unit_validN : ValidN () := λ n x, True.
Instance unit_pcore : PCore () := λ x, Some x.
Instance unit_op : Op () := λ x y, ().