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