Commit ca3da7ca authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify CMRAMonotone.

It now also contains a non-expansiveness proof.
parent c2725b24
......@@ -97,11 +97,6 @@ Proof.
split; [|by intros ?; exists y].
by intros [z Hz]; rewrite Hz assoc agree_idemp.
Qed.
Lemma agree_includedN n (x y : agree A) : x {n} y y {n} x y.
Proof.
split; [|by intros ?; exists y].
by intros [z Hz]; rewrite Hz assoc agree_idemp.
Qed.
Lemma agree_op_inv n (x1 x2 : agree A) : {n} (x1 x2) x1 {n} x2.
Proof. intros Hxy; apply Hxy. Qed.
Lemma agree_valid_includedN n (x y : agree A) : {n} y x {n} y x {n} y.
......@@ -160,20 +155,20 @@ Proof. done. Qed.
Section agree_map.
Context {A B : cofeT} (f : A B) `{Hf: n, Proper (dist n ==> dist n) f}.
Global Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
Global Instance agree_map_proper :
Proper (() ==> ()) (agree_map f) := ne_proper _.
Instance agree_map_proper : Proper (() ==> ()) (agree_map f) := ne_proper _.
Lemma agree_map_ext (g : A B) x :
( x, f x g x) agree_map f x agree_map g x.
Proof. by intros Hfg; split; simpl; intros; rewrite ?Hfg. Qed.
Global Instance agree_map_monotone : CMRAMonotone (agree_map f).
Proof.
split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]].
intros n x y; rewrite !agree_includedN; intros Hy; rewrite Hy.
split; last done; split; simpl; last tauto.
by intros (?&?&Hxy); repeat split; intros;
try apply Hxy; try apply Hf; eauto using @agree_valid_le.
split; first apply _.
- by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx].
- intros x y; rewrite !agree_included=> ->.
split; last done; split; simpl; last tauto.
by intros (?&?&Hxy); repeat split; intros;
try apply Hxy; try apply Hf; eauto using @agree_valid_le.
Qed.
End agree_map.
......
......@@ -98,12 +98,6 @@ Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
Lemma auth_includedN n (x y : auth A) :
x {n} y authoritative x {n} authoritative y own x {n} own y.
Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
Lemma authoritative_validN n (x : auth A) : {n} x {n} authoritative x.
Proof. by destruct x as [[]]. Qed.
Lemma own_validN n (x : auth A) : {n} x {n} own x.
......@@ -212,7 +206,6 @@ Proof.
intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN.
by rewrite -(local_updateN L) // EQ -(local_updateN L) // -EQ.
Qed.
End cmra.
Arguments authRA : clear implicits.
......@@ -234,14 +227,13 @@ Proof.
intros f g Hf [??] [??] [??]; split; [by apply excl_map_cmra_ne|by apply Hf].
Qed.
Instance auth_map_cmra_monotone {A B : cmraT} (f : A B) :
( n, Proper (dist n ==> dist n) f)
CMRAMonotone f CMRAMonotone (auth_map f).
Proof.
split.
- by intros n [x a] [y b]; rewrite !auth_includedN /=;
intros [??]; split; simpl; apply: includedN_preserving.
- intros n [[a| |] b]; rewrite /= /cmra_validN;
naive_solver eauto using @includedN_preserving, @validN_preserving.
split; try apply _.
- intros n [[a| |] b]; rewrite /= /cmra_validN /=; try
naive_solver eauto using includedN_preserving, validN_preserving.
- by intros [x a] [y b]; rewrite !auth_included /=;
intros [??]; split; simpl; apply: included_preserving.
Qed.
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
CofeMor (auth_map f).
......
......@@ -142,8 +142,9 @@ Class CMRADiscrete (A : cmraT) : Prop := {
(** * Morphisms *)
Class CMRAMonotone {A B : cmraT} (f : A B) := {
includedN_preserving n x y : x {n} y f x {n} f y;
validN_preserving n x : {n} x {n} f x
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
}.
(** * Local updates *)
......@@ -430,26 +431,28 @@ End cmra.
(** * Properties about monotone functions *)
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
Proof. by split. Qed.
Proof. repeat split; by try apply _. Qed.
Instance cmra_monotone_compose {A B C : cmraT} (f : A B) (g : B C) :
CMRAMonotone f CMRAMonotone g CMRAMonotone (g f).
Proof.
split.
- move=> n x y Hxy /=. by apply includedN_preserving, includedN_preserving.
- apply _.
- move=> n x Hx /=. by apply validN_preserving, validN_preserving.
- move=> x y Hxy /=. by apply included_preserving, included_preserving.
Qed.
Section cmra_monotone.
Context {A B : cmraT} (f : A B) `{!CMRAMonotone f}.
Lemma included_preserving x y : x y f x f y.
Global Instance cmra_monotone_proper : Proper (() ==> ()) f := ne_proper _.
Lemma includedN_preserving n x y : x {n} y f x {n} f y.
Proof.
rewrite !cmra_included_includedN; eauto using includedN_preserving.
intros [z ->].
apply cmra_included_includedN, included_preserving, cmra_included_l.
Qed.
Lemma valid_preserving x : x f x.
Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.
(** * Transporting a CMRA equality *)
Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
eq_rect A id x _ H.
......@@ -607,8 +610,8 @@ Arguments prodRA : clear implicits.
Instance prod_map_cmra_monotone {A A' B B' : cmraT} (f : A A') (g : B B') :
CMRAMonotone f CMRAMonotone g CMRAMonotone (prod_map f g).
Proof.
split.
- intros n x y; rewrite !prod_includedN; intros [??]; simpl.
by split; apply includedN_preserving.
split; first apply _.
- by intros n x [??]; split; simpl; apply validN_preserving.
- intros x y; rewrite !prod_included=> -[??] /=.
by split; apply included_preserving.
Qed.
......@@ -27,6 +27,7 @@ Inductive excl_dist : Dist (excl A) :=
| ExclUnit_dist n : ExclUnit {n} ExclUnit
| ExclBot_dist n : ExclBot {n} ExclBot.
Existing Instance excl_dist.
Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A).
Proof. by constructor. Qed.
Global Instance Excl_proper : Proper (() ==> ()) (@Excl A).
......@@ -35,6 +36,7 @@ Global Instance Excl_inj : Inj (≡) (≡) (@Excl A).
Proof. by inversion_clear 1. Qed.
Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
Proof. by inversion_clear 1. Qed.
Program Definition excl_chain
(c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A :=
{| chain_car n := match c n return _ with Excl y => y | _ => x end |}.
......@@ -191,10 +193,10 @@ Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
Instance excl_map_cmra_monotone {A B : cofeT} (f : A B) :
( n, Proper (dist n ==> dist n) f) CMRAMonotone (excl_map f).
Proof.
split.
- intros n x y [z Hy]; exists (excl_map f z); rewrite Hy.
by destruct x, z; constructor.
split; try apply _.
- by intros n [a| |].
- intros x y [z Hy]; exists (excl_map f z); apply equiv_dist=> n.
move: Hy=> /equiv_dist /(_ n) ->; by destruct x, z.
Qed.
Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
CofeMor (excl_map f).
......
......@@ -231,8 +231,8 @@ Proof.
[exists (x y)|exists x]; eauto using cmra_included_l.
- intros (y&Hi&?); rewrite map_includedN_spec=>j.
destruct (decide (i = j)); simplify_map_eq.
+ by rewrite Hi; apply Some_Some_includedN, cmra_included_includedN.
+ apply None_includedN.
+ rewrite Hi. by apply (includedN_preserving _), cmra_included_includedN.
+ apply: cmra_empty_leastN.
Qed.
Lemma map_dom_op m1 m2 : dom (gset K) (m1 m2) dom _ m1 dom _ m2.
Proof.
......@@ -338,10 +338,10 @@ Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
Instance map_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A B)
`{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A gmap K B).
Proof.
split.
- intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
by rewrite !lookup_fmap; apply: includedN_preserving.
split; try apply _.
- by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
- intros m1 m2; rewrite !map_included_spec=> Hm i.
by rewrite !lookup_fmap; apply: included_preserving.
Qed.
Definition mapC_map `{Countable K} {A B} (f: A -n> B) : mapC K A -n> mapC K B :=
CofeMor (fmap f : mapC K A mapC K B).
......
......@@ -133,13 +133,6 @@ Section iprod_cmra.
- intros Hh; exists (g f)=> x; specialize (Hh x).
by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus.
Qed.
Lemma iprod_includedN_spec n (f g : iprod B) : f {n} g x, f x {n} g x.
Proof.
split.
- by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x).
- intros Hh; exists (g f)=> x; specialize (Hh x).
by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus'.
Qed.
Definition iprod_cmra_mixin : CMRAMixin (iprod B).
Proof.
......@@ -283,10 +276,10 @@ Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
Instance iprod_map_cmra_monotone {A} {B1 B2: A cmraT} (f : x, B1 x B2 x) :
( x, CMRAMonotone (f x)) CMRAMonotone (iprod_map f).
Proof.
split.
- intros n g1 g2; rewrite !iprod_includedN_spec=> Hf x.
rewrite /iprod_map; apply includedN_preserving, Hf.
split; first apply _.
- intros n g Hg x; rewrite /iprod_map; apply validN_preserving, Hg.
- intros g1 g2; rewrite !iprod_included_spec=> Hf x.
rewrite /iprod_map; apply included_preserving, Hf.
Qed.
Definition iprodC_map {A} {B1 B2 : A cofeT} (f : iprod (λ x, B1 x -n> B2 x)) :
......
......@@ -72,6 +72,8 @@ Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
Instance option_minus : Minus (option A) :=
difference_with (λ x y, Some (x y)).
Definition Some_op a b : Some (a b) = Some a Some b := eq_refl.
Lemma option_included (mx my : option A) :
mx my mx = None x y, mx = Some x my = Some y x y.
Proof.
......@@ -84,24 +86,6 @@ Proof.
- intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
by exists (Some z); constructor.
Qed.
Lemma option_includedN n (mx my : option A) :
mx {n} my mx = None x y, mx = Some x my = Some y x {n} y.
Proof.
split.
- intros [mz Hmz].
destruct mx as [x|]; [right|by left].
destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
cofe_subst; eauto using cmra_includedN_l.
- intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
by exists (Some z); constructor.
Qed.
Lemma None_includedN n (mx : option A) : None {n} mx.
Proof. rewrite option_includedN; auto. Qed.
Lemma Some_Some_includedN n (x y : A) : x {n} y Some x {n} Some y.
Proof. rewrite option_includedN; eauto 10. Qed.
Definition Some_op a b : Some (a b) = Some a Some b := eq_refl.
Definition option_cmra_mixin : CMRAMixin (option A).
Proof.
......@@ -140,6 +124,8 @@ Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionRA.
Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
(** Misc *)
Global Instance Some_cmra_monotone : CMRAMonotone Some.
Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed.
Lemma op_is_Some mx my : is_Some (mx my) is_Some mx is_Some my.
Proof.
destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
......@@ -192,10 +178,10 @@ Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
Instance option_fmap_cmra_monotone {A B : cmraT} (f: A B) `{!CMRAMonotone f} :
CMRAMonotone (fmap f : option A option B).
Proof.
split.
- intros n mx my; rewrite !option_includedN.
intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @includedN_preserving.
- by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving.
split; first apply _.
- intros n [x|] ?; rewrite /cmra_validN /=; by repeat apply validN_preserving.
- intros mx my; rewrite !option_included.
intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @included_preserving.
Qed.
Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
CofeMor (fmap f : optionC A optionC B).
......
......@@ -205,10 +205,10 @@ Qed.
Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) :
CMRAMonotone (@res_map Λ Σ _ _ f).
Proof.
split.
- by intros n r1 r2; rewrite !res_includedN;
intros (?&?&?); split_and!; simpl; try apply includedN_preserving.
split; first apply _.
- by intros n r (?&?&?); split_and!; simpl; try apply validN_preserving.
- by intros r1 r2; rewrite !res_included;
intros (?&?&?); split_and!; simpl; try apply included_preserving.
Qed.
Definition resC_map {Λ Σ A B} (f : A -n> B) : resC Λ Σ A -n> resC Λ Σ B :=
CofeMor (res_map f : resRA Λ Σ A resRA Λ Σ B).
......
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