...
  View open merge request
Commits (1)
......@@ -175,13 +175,10 @@ Hint Mode CmraTotal ! : typeclass_instances.
(** The function [core] returns a dummy when used on CMRAs without total
core. *)
Class Core (A : Type) := core : A A.
Hint Mode Core ! : typeclass_instances.
Definition core `{PCore A} (x : A) : A := default x (pcore x).
Arguments core _ _ _ /.
Instance: Params (@core) 2 := {}.
Instance core' `{PCore A} : Core A := λ x, default x (pcore x).
Arguments core' _ _ _ /.
(** * CMRAs with a unit element *)
Class Unit (A : Type) := ε : A.
Arguments ε {_ _}.
......@@ -258,6 +255,22 @@ Arguments cmra_morphism_pcore {_ _} _ {_} _.
Arguments cmra_morphism_op {_ _} _ {_} _ _.
(** * Properties **)
(** The [core] totalization is actually [Proper] as long as [PCore] is,
no matter whether it's with a CMRA or not. *)
Global Instance cmra_core_ne {A : ofeT} `{!PCore A} :
NonExpansive (@pcore A _) NonExpansive (@core A _).
Proof.
intros ? n x y Hxy. rewrite /core. f_equiv; first done.
by rewrite Hxy.
Qed.
Global Instance cmra_core_proper {A : Type} `{!Equiv A, !PCore A} :
Proper (() ==> ()) (@pcore A _) Proper (() ==> ()) (@core A _).
Proof.
intros Hprop x y Hxy. rewrite /core. f_equiv; first done.
eapply Hprop. done.
Qed.
Section cmra.
Context {A : cmraT}.
Implicit Types x y z : A.
......@@ -478,7 +491,7 @@ Section total_core.
Lemma cmra_pcore_core x : pcore x = Some (core x).
Proof.
rewrite /core /core'. destruct (cmra_total x) as [cx ->]. done.
rewrite /core. destruct (cmra_total x) as [cx ->]. done.
Qed.
Lemma cmra_core_l x : core x x x.
Proof.
......@@ -495,14 +508,6 @@ Section total_core.
by rewrite /core /= Hcx Hcy.
Qed.
Global Instance cmra_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 Instance cmra_core_proper : Proper (() ==> ()) (@core A _).
Proof. apply (ne_proper _). Qed.
Lemma cmra_core_r x : x core x x.
Proof. by rewrite (comm _ x) cmra_core_l. Qed.
Lemma cmra_core_dup x : core x core x core x.
......@@ -723,7 +728,7 @@ Section cmra_total.
Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
Context (total : x : A, is_Some (pcore x)).
Context (op_ne : x : A, NonExpansive (op x)).
Context (core_ne : NonExpansive (@core A _)).
Context (pcore_ne : NonExpansive (@pcore A _)).
Context (validN_ne : n, Proper (dist n ==> impl) (@validN A _ n)).
Context (valid_validN : (x : A), x n, {n} x).
Context (validN_S : n (x : A), {S n} x {n} x).
......@@ -739,8 +744,8 @@ Section cmra_total.
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 n x y ? Hcx%pcore_ne Hx; move: Hcx. rewrite Hx /= => Hcx.
destruct (pcore y); inversion Hcx; simplify_eq/=; 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.
......@@ -768,7 +773,7 @@ Section cmra_morphism.
Local Set Default Proof Using "Type*".
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.
Proof. unfold core. rewrite cmra_morphism_pcore. by destruct (pcore x). Qed.
Lemma cmra_morphism_monotone x y : x y f x f y.
Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
Lemma cmra_morphism_monotoneN n x y : x {n} y f x {n} f y.
......@@ -926,7 +931,7 @@ Section ra_total.
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 (pcore_proper: Proper (() ==> ()) (@pcore A _)).
Context (valid_proper : Proper (() ==> impl) (@valid A _)).
Context (op_assoc : Assoc () (@op A _)).
Context (op_comm : Comm () (@op A _)).
......@@ -937,8 +942,8 @@ Section ra_total.
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 y ? Hcx%pcore_proper Hx; move: Hcx. rewrite Hx /==>Hcx.
destruct (pcore y); inversion Hcx; simplify_eq/=; 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.
......@@ -954,7 +959,10 @@ Section unit.
Instance unit_pcore : PCore () := λ x, Some x.
Instance unit_op : Op () := λ x y, ().
Lemma unit_cmra_mixin : CmraMixin ().
Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
Proof. apply discrete_cmra_mixin, ra_total_mixin; try by eauto.
assert (Proper (equiv ==> equiv) (@pcore () _)). apply _.
Set Printing All.
Qed.
Canonical Structure unitR : cmraT := CmraT unit unit_cmra_mixin.
Instance unit_unit : Unit () := ().
......@@ -1020,7 +1028,7 @@ Section mnat.
Proof.
apply ra_total_mixin; try by eauto.
- solve_proper.
- solve_proper.
- intros x y Hxy. rewrite /core /pcore /= //.
- intros x y z. apply Nat.max_assoc.
- intros x y. apply Nat.max_comm.
- intros x. apply Max.max_idempotent.
......@@ -1143,7 +1151,7 @@ Section prod.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).
Proof.
rewrite /core /core' {1}/pcore /=.
rewrite /core {1}/pcore /=.
rewrite (cmra_pcore_core a) /= (cmra_pcore_core b). done.
Qed.
......
From iris.algebra Require Export cmra updates.
Set Default Proof Using "Type".
Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
Record DraMixin A `{Equiv A, PCore A, Disjoint A, Op A, Valid A} := {
(* setoids *)
mixin_dra_equivalence : Equivalence (@{A});
mixin_dra_op_proper : Proper ((@{A}) ==> () ==> ()) ();
mixin_dra_core_proper : Proper ((@{A}) ==> ()) core;
mixin_dra_pcore_proper : Proper ((@{A}) ==> ()) pcore;
mixin_dra_valid_proper : Proper ((@{A}) ==> impl) valid;
mixin_dra_disjoint_proper (x : A) : Proper (() ==> impl) (disjoint x);
(* validity *)
......@@ -29,7 +29,7 @@ Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
Structure draT := DraT {
dra_car :> Type;
dra_equiv : Equiv dra_car;
dra_core : Core dra_car;
dra_pcore : PCore dra_car;
dra_disjoint : Disjoint dra_car;
dra_op : Op dra_car;
dra_valid : Valid dra_car;
......@@ -38,13 +38,13 @@ Structure draT := DraT {
Arguments DraT _ {_ _ _ _ _} _.
Arguments dra_car : simpl never.
Arguments dra_equiv : simpl never.
Arguments dra_core : simpl never.
Arguments dra_pcore : simpl never.
Arguments dra_disjoint : simpl never.
Arguments dra_op : simpl never.
Arguments dra_valid : simpl never.
Arguments dra_mixin : simpl never.
Add Printing Constructor draT.
Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid.
Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
(** Lifting properties from the mixin *)
Section dra_mixin.
......@@ -54,8 +54,8 @@ Section dra_mixin.
Proof. apply (mixin_dra_equivalence _ (dra_mixin A)). Qed.
Global Instance dra_op_proper : Proper (() ==> () ==> ()) (@op A _).
Proof. apply (mixin_dra_op_proper _ (dra_mixin A)). Qed.
Global Instance dra_core_proper : Proper (() ==> ()) (@core A _).
Proof. apply (mixin_dra_core_proper _ (dra_mixin A)). Qed.
Global Instance dra_core_proper : Proper (() ==> ()) (@pcore A _).
Proof. apply (mixin_dra_pcore_proper _ (dra_mixin A)). Qed.
Global Instance dra_valid_proper : Proper (() ==> impl) (@valid A _).
Proof. apply (mixin_dra_valid_proper _ (dra_mixin A)). Qed.
Global Instance dra_disjoint_proper x : Proper (() ==> impl) (disjoint x).
......@@ -160,7 +160,8 @@ Proof.
- intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
split; intros (?&?&?); split_and!;
first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
- by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
- intros ?? [? Heq]; split; [done|]; simpl=>?. f_equiv; first by auto.
rewrite Heq; done.
- intros ?? [??]; naive_solver.
- intros [x px ?] [y py ?] [z pz ?]; split; simpl;
[intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
......
......@@ -896,11 +896,11 @@ Canonical Structure NO := leibnizO N.
Canonical Structure ZO := leibnizO Z.
(* Option *)
Instance option_dist `{Dist A} : Dist (option A) := λ n, option_Forall2 (dist n).
Section option.
Context {A : ofeT}.
Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
Lemma dist_option_Forall2 n mx my : mx {n} my option_Forall2 (dist n) mx my.
Lemma dist_option_Forall2 n (mx my : option A) : mx {n} my option_Forall2 (dist n) mx my.
Proof. done. Qed.
Definition option_ofe_mixin : OfeMixin (option A).
......