Commit 9ee62b3a authored by Ralf Jung's avatar Ralf Jung
Browse files

rename: preserving for a partial order -> monotone

parent 9efcd541
......@@ -127,7 +127,7 @@ Proof.
- by split; simpl; rewrite ?cmra_core_l.
- by split; simpl; rewrite ?cmra_core_idemp.
- intros ??; rewrite! auth_included; intros [??].
by split; simpl; apply cmra_core_preserving.
by split; simpl; apply cmra_core_mono.
- assert ( n (a b1 b2 : A), b1 b2 {n} a b1 {n} a).
{ intros n a b1 b2 <-; apply cmra_includedN_l. }
intros n [[[a1|]|] b1] [[[a2|]|] b2];
......@@ -222,9 +222,9 @@ Instance auth_map_cmra_monotone {A B : ucmraT} (f : A → B) :
Proof.
split; try apply _.
- intros n [[[a|]|] b]; rewrite /= /cmra_validN /=; try
naive_solver eauto using includedN_preserving, validN_preserving.
naive_solver eauto using cmra_monotoneN, validN_preserving.
- by intros [x a] [y b]; rewrite !auth_included /=;
intros [??]; split; simpl; apply: included_preserving.
intros [??]; split; simpl; apply: cmra_monotone.
Qed.
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
CofeMor (auth_map f).
......
......@@ -48,7 +48,7 @@ Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
mixin_cmra_comm : Comm () ();
mixin_cmra_pcore_l x cx : pcore x = Some cx cx x x;
mixin_cmra_pcore_idemp x cx : pcore x = Some cx pcore cx Some cx;
mixin_cmra_pcore_preserving x y cx :
mixin_cmra_pcore_mono x y cx :
x y pcore x = Some cx cy, pcore y = Some cy cx cy;
mixin_cmra_validN_op_l n x y : {n} (x y) {n} x;
mixin_cmra_extend n x y1 y2 :
......@@ -113,9 +113,9 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_pcore_l _ (cmra_mixin A)). Qed.
Lemma cmra_pcore_idemp x cx : pcore x = Some cx pcore cx Some cx.
Proof. apply (mixin_cmra_pcore_idemp _ (cmra_mixin A)). Qed.
Lemma cmra_pcore_preserving x y cx :
Lemma cmra_pcore_mono x y cx :
x y pcore x = Some cx cy, pcore y = Some cy cx cy.
Proof. apply (mixin_cmra_pcore_preserving _ (cmra_mixin A)). Qed.
Proof. apply (mixin_cmra_pcore_mono _ (cmra_mixin A)). Qed.
Lemma cmra_validN_op_l n x y : {n} (x y) {n} x.
Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
Lemma cmra_extend n x y1 y2 :
......@@ -217,10 +217,10 @@ Class CMRADiscrete (A : cmraT) := {
Class CMRAMonotone {A B : cmraT} (f : A B) := {
cmra_monotone_ne n :> Proper (dist n ==> dist n) f;
validN_preserving n x : {n} x {n} f x;
included_preserving x y : x y f x f y
cmra_monotone x y : x y f x f y
}.
Arguments validN_preserving {_ _} _ {_} _ _ _.
Arguments included_preserving {_ _} _ {_} _ _ _.
Arguments cmra_monotone {_ _} _ {_} _ _ _.
(** * Properties **)
Section cmra.
......@@ -364,18 +364,18 @@ Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
Lemma cmra_included_r x y : y x y.
Proof. rewrite (comm op); apply cmra_included_l. Qed.
Lemma cmra_pcore_preserving' x y cx :
Lemma cmra_pcore_mono' x y cx :
x y pcore x Some cx cy, pcore y = Some cy cx cy.
Proof.
intros ? (cx'&?&Hcx)%equiv_Some_inv_r'.
destruct (cmra_pcore_preserving x y cx') as (cy&->&?); auto.
destruct (cmra_pcore_mono x y cx') as (cy&->&?); auto.
exists cy; by rewrite Hcx.
Qed.
Lemma cmra_pcore_preservingN' n x y cx :
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_preserving x (x z) cx')
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. }
......@@ -384,14 +384,14 @@ Proof.
Qed.
Lemma cmra_included_pcore x cx : pcore x = Some cx cx x.
Proof. exists x. by rewrite cmra_pcore_l. Qed.
Lemma cmra_preservingN_l n x y z : x {n} y z x {n} z y.
Lemma cmra_monoN_l n 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_preserving_l x y z : x y z x z y.
Lemma cmra_mono_l x y z : x y z x z y.
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
Lemma cmra_preservingN_r n x y z : x {n} y x z {n} y z.
Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
Lemma cmra_preserving_r x y z : x y x z y z.
Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
Lemma cmra_monoN_r n 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_r x y z : x y x z y z.
Proof. by intros; rewrite -!(comm _ z); apply cmra_mono_l. Qed.
Lemma cmra_included_dist_l n x1 x2 x1' :
x1 x2 x1' {n} x1 x2', x1' x2' x2' {n} x2.
......@@ -412,10 +412,10 @@ Section total_core.
Proof.
destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_idemp.
Qed.
Lemma cmra_core_preserving x y : x y core x core y.
Lemma cmra_core_mono x y : x y core x core y.
Proof.
intros; destruct (cmra_total x) as [cx Hcx].
destruct (cmra_pcore_preserving x y cx) as (cy&Hcy&?); auto.
destruct (cmra_pcore_mono x y cx) as (cy&Hcy&?); auto.
by rewrite /core /= Hcx Hcy.
Qed.
......@@ -461,10 +461,10 @@ Section total_core.
Proof.
split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
Qed.
Lemma cmra_core_preservingN n x y : x {n} y core x {n} core y.
Lemma cmra_core_monoN n x y : x {n} y core x {n} core y.
Proof.
intros [z ->].
apply cmra_included_includedN, cmra_core_preserving, cmra_included_l.
apply cmra_included_includedN, cmra_core_mono, cmra_included_l.
Qed.
End total_core.
......@@ -519,7 +519,7 @@ Section ucmra.
Global Instance cmra_unit_total : CMRATotal A.
Proof.
intros x. destruct (cmra_pcore_preserving' x ) as (cx&->&?);
intros x. destruct (cmra_pcore_mono' x ) as (cx&->&?);
eauto using ucmra_unit_least, (persistent ).
Qed.
End ucmra.
......@@ -538,7 +538,7 @@ Section cmra_total.
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_preserving : x y : A, x y core x core y).
Context (core_mono : x y : A, x y core x core y).
Context (validN_op_l : n (x y : A), {n} (x y) {n} x).
Context (extend : n (x y1 y2 : A),
{n} x x {n} y1 y2
......@@ -551,7 +551,7 @@ Section cmra_total.
- 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_preserving Hx. move: Hxy.
- intros x y cx Hxy%core_mono Hx. move: Hxy.
rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
Qed.
End cmra_total.
......@@ -565,16 +565,16 @@ Proof.
split.
- apply _.
- move=> n x Hx /=. by apply validN_preserving, validN_preserving.
- move=> x y Hxy /=. by apply included_preserving, included_preserving.
- move=> x y Hxy /=. by apply cmra_monotone, cmra_monotone.
Qed.
Section cmra_monotone.
Context {A B : cmraT} (f : A B) `{!CMRAMonotone f}.
Global Instance cmra_monotone_proper : Proper (() ==> ()) f := ne_proper _.
Lemma includedN_preserving n x y : x {n} y f x {n} f y.
Lemma cmra_monotoneN n x y : x {n} y f x {n} f y.
Proof.
intros [z ->].
apply cmra_included_includedN, (included_preserving f), cmra_included_l.
apply cmra_included_includedN, (cmra_monotone f), cmra_included_l.
Qed.
Lemma valid_preserving x : x f x.
Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
......@@ -677,7 +677,7 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
ra_comm : Comm () ();
ra_pcore_l x cx : pcore x = Some cx cx x x;
ra_pcore_idemp x cx : pcore x = Some cx pcore cx Some cx;
ra_pcore_preserving x y cx :
ra_pcore_mono x y cx :
x y pcore x = Some cx cy, pcore y = Some cy cx cy;
ra_valid_op_l x y : (x y) x
}.
......@@ -715,7 +715,7 @@ Section ra_total.
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_preserving : x y : A, x y core x core y).
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.
......@@ -725,7 +725,7 @@ Section ra_total.
- 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_preserving Hx. move: Hxy.
- intros x y cx Hxy%core_mono Hx. move: Hxy.
rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
Qed.
End ra_total.
......@@ -878,8 +878,8 @@ Section prod.
- 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_preserving (x.1) (y.1) (cx.1)) as (z1&?&?); auto.
destruct (cmra_pcore_preserving (x.2) (y.2) (cx.2)) as (z2&?&?); auto.
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 *.
......@@ -942,7 +942,7 @@ Proof.
split; first apply _.
- by intros n x [??]; split; simpl; apply validN_preserving.
- intros x y; rewrite !prod_included=> -[??] /=.
by split; apply included_preserving.
by split; apply cmra_monotone.
Qed.
Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
......@@ -1043,7 +1043,7 @@ Section option.
- intros mx my; setoid_rewrite option_included.
intros [->|(x&y&->&->&[?|?])]; simpl; eauto.
+ destruct (pcore x) as [cx|] eqn:?; eauto.
destruct (cmra_pcore_preserving x y cx) as (?&?&?); eauto 10.
destruct (cmra_pcore_mono x y cx) as (?&?&?); eauto 10.
+ destruct (pcore x) as [cx|] eqn:?; eauto.
destruct (cmra_pcore_proper x y cx) as (?&?&?); eauto 10.
- intros n [x|] [y|]; rewrite /validN /option_validN /=;
......@@ -1102,7 +1102,7 @@ Proof.
split; first apply _.
- intros n [x|] ?; rewrite /cmra_validN //=. by apply (validN_preserving f).
- intros mx my; rewrite !option_included.
intros [->|(x&y&->&->&[?|Hxy])]; simpl; eauto 10 using @included_preserving.
intros [->|(x&y&->&->&[?|Hxy])]; simpl; eauto 10 using @cmra_monotone.
right; exists (f x), (f y). by rewrite {4}Hxy; eauto.
Qed.
Program Definition optionURF (F : rFunctor) : urFunctor := {|
......
......@@ -202,10 +202,10 @@ Proof.
- intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=].
+ exists CsumBot. rewrite csum_included; eauto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_preserving a a' ca) as (ca'&->&?); auto.
destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto.
exists (Cinl ca'). rewrite csum_included; eauto 10.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_preserving b b' cb) as (cb'&->&?); auto.
destruct (cmra_pcore_mono b b' cb) as (cb'&->&?); auto.
exists (Cinr cb'). rewrite csum_included; eauto 10.
- intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
- intros n [a|b|] y1 y2 Hx Hx'.
......@@ -330,7 +330,7 @@ Proof.
- intros n [a|b|]; simpl; auto using validN_preserving.
- intros x y; rewrite !csum_included.
intros [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]; simpl;
eauto 10 using included_preserving.
eauto 10 using cmra_monotone.
Qed.
Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
......
......@@ -20,7 +20,7 @@ Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
mixin_dra_core_disjoint_l x : x core x x;
mixin_dra_core_l x : x core x x x;
mixin_dra_core_idemp x : x core (core x) core x;
mixin_dra_core_preserving x y :
mixin_dra_core_mono x y :
z, x y x y core (x y) core x z z core x z
}.
Structure draT := DRAT {
......@@ -78,9 +78,9 @@ Section dra_mixin.
Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
Lemma dra_core_idemp x : x core (core x) core x.
Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
Lemma dra_core_preserving x y :
Lemma dra_core_mono x y :
z, x y x y core (x y) core x z z core x z.
Proof. apply (mixin_dra_core_preserving _ (dra_mixin A)). Qed.
Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
End dra_mixin.
Record validity (A : draT) := Validity {
......@@ -166,7 +166,7 @@ Proof.
naive_solver eauto using dra_core_l, dra_core_disjoint_l.
- intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
- intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
destruct (dra_core_preserving x z) as (z'&Hz').
destruct (dra_core_mono x z) as (z'&Hz').
unshelve eexists (Validity z' (px py pz) _); [|split; simpl].
{ intros (?&?&?); apply Hz'; tauto. }
+ tauto.
......
......@@ -134,7 +134,7 @@ Proof.
- intros m i. by rewrite lookup_op lookup_core cmra_core_l.
- intros m i. by rewrite !lookup_core cmra_core_idemp.
- intros m1 m2; rewrite !lookup_included=> Hm i.
rewrite !lookup_core. by apply cmra_core_preserving.
rewrite !lookup_core. by apply cmra_core_mono.
- intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- intros n m m1 m2 Hm Hm12.
......@@ -399,7 +399,7 @@ Proof.
split; try apply _.
- by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _).
- intros m1 m2; rewrite !lookup_included=> Hm i.
by rewrite !lookup_fmap; apply: included_preserving.
by rewrite !lookup_fmap; apply: cmra_monotone.
Qed.
Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A gmapC K B).
......
......@@ -114,7 +114,7 @@ Section iprod_cmra.
- by intros f x; rewrite iprod_lookup_op iprod_lookup_core cmra_core_l.
- by intros f x; rewrite iprod_lookup_core cmra_core_idemp.
- intros f1 f2; rewrite !iprod_included_spec=> Hf x.
by rewrite iprod_lookup_core; apply cmra_core_preserving, Hf.
by rewrite iprod_lookup_core; apply cmra_core_mono, Hf.
- intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
- intros n f f1 f2 Hf Hf12.
set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
......@@ -282,7 +282,7 @@ Proof.
split; first apply _.
- intros n g Hg x; rewrite /iprod_map; apply (validN_preserving (f _)), Hg.
- intros g1 g2; rewrite !iprod_included_spec=> Hf x.
rewrite /iprod_map; apply (included_preserving _), Hf.
rewrite /iprod_map; apply (cmra_monotone _), Hf.
Qed.
Definition iprodC_map `{Finite A} {B1 B2 : A cofeT}
......
......@@ -187,7 +187,7 @@ Section cmra.
- intros l; rewrite list_equiv_lookup=> i.
by rewrite !list_lookup_core cmra_core_idemp.
- intros l1 l2; rewrite !list_lookup_included=> Hl i.
rewrite !list_lookup_core. by apply cmra_core_preserving.
rewrite !list_lookup_core. by apply cmra_core_mono.
- intros n l1 l2. rewrite !list_lookup_validN.
setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
- intros n l. induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Hl';
......@@ -374,7 +374,7 @@ Proof.
- intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
by apply (validN_preserving (fmap f : option A option B)).
- intros l1 l2. rewrite !list_lookup_included=> Hl i. rewrite !list_lookup_fmap.
by apply (included_preserving (fmap f : option A option B)).
by apply (cmra_monotone (fmap f : option A option B)).
Qed.
Program Definition listURF (F : urFunctor) : urFunctor := {|
......
......@@ -68,7 +68,7 @@ Qed.
Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
`{!CMRAMonotone f} (P : uPred M1) :
uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. naive_solver eauto using uPred_mono, includedN_preserving. Qed.
Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
Next Obligation. naive_solver eauto using uPred_closed, validN_preserving. Qed.
Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
......@@ -212,7 +212,7 @@ Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
Next Obligation.
intros M P Q n x1 x1' HPQ ? n3 x3 ???; simpl in *.
apply uPred_mono with (x1 x3);
eauto using cmra_validN_includedN, cmra_preservingN_r, cmra_includedN_le.
eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Qed.
Next Obligation. naive_solver. Qed.
Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
......@@ -223,7 +223,7 @@ Definition uPred_wand_eq :
Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (core x) |}.
Next Obligation.
intros M; naive_solver eauto using uPred_mono, @cmra_core_preservingN.
intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
Qed.
Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
......@@ -1038,7 +1038,7 @@ Qed.
Lemma always_ownM (a : M) : Persistent a uPred_ownM a uPred_ownM a.
Proof.
split=> n x /=; split; [by apply always_elim|unseal; intros Hx]; simpl.
rewrite -(persistent_core a). by apply cmra_core_preservingN.
rewrite -(persistent_core a). by apply cmra_core_monoN.
Qed.
Lemma ownM_something : True a, uPred_ownM a.
Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
......
......@@ -109,7 +109,7 @@ Proof.
- by intros ?; constructor; rewrite /= cmra_core_l.
- by intros ?; constructor; rewrite /= cmra_core_idemp.
- intros r1 r2; rewrite !res_included.
by intros (?&?&?); split_and!; apply cmra_core_preserving.
by intros (?&?&?); split_and!; apply cmra_core_mono.
- intros n r1 r2 (?&?&?);
split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
- intros n r r1 r2 (?&?&?) [???]; simpl in *.
......@@ -212,7 +212,7 @@ Proof.
split; first apply _.
- intros n r (?&?&?); split_and!; simpl; by try apply: validN_preserving.
- by intros r1 r2; rewrite !res_included;
intros (?&?&?); split_and!; simpl; try apply: included_preserving.
intros (?&?&?); split_and!; simpl; try apply: cmra_monotone.
Qed.
Definition resC_map {Λ} {A A' : cofeT} {M M' : ucmraT}
(f : A -n> A') (g : M -n> M') : resC Λ A M -n> resC Λ A' M' :=
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment