Commit cfb00b3e authored by Robbert Krebbers's avatar Robbert Krebbers

CMRAs with partial cores.

Based on an idea and WIP commits of J-H. Jourdan: the core of a CMRA
A is now a partial function A → option A.

TODO: define sum CMRA
TODO: remove one shot CMRA and define it in terms of sum
parent 4195e15c
Pipeline #1173 passed with stage
......@@ -60,7 +60,7 @@ Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := x;
agree_is_valid n := agree_is_valid x n agree_is_valid y n x {n} y |}.
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
Instance agree_core : Core (agree A) := id.
Instance agree_pcore : PCore (agree A) := Some.
Instance: Comm () (@op (agree A) _).
Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
......@@ -106,11 +106,11 @@ Qed.
Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof.
split; try (apply _ || done).
apply cmra_total_mixin; try apply _ || by eauto.
- intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
rewrite -(Hx n'); last auto.
symmetry; apply dist_le with n; try apply Hx; auto.
- intros x; apply agree_idemp.
- intros x. apply agree_idemp.
- by intros n x y [(?&?&?) ?].
- intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
+ by rewrite agree_idemp.
......@@ -119,8 +119,10 @@ Qed.
Canonical Structure agreeR : cmraT :=
CMRAT (agree A) agree_cofe_mixin agree_cmra_mixin.
Global Instance agree_total : CMRATotal agreeR.
Proof. rewrite /CMRATotal; eauto. Qed.
Global Instance agree_persistent (x : agree A) : Persistent x.
Proof. done. Qed.
Proof. by constructor. Qed.
Program Definition to_agree (x : A) : agree A :=
{| agree_car n := x; agree_is_valid n := True |}.
......
......@@ -3,18 +3,18 @@ From iris.algebra Require Import upred.
Local Arguments valid _ _ !_ /.
Local Arguments validN _ _ _ !_ /.
Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
Record auth (A : Type) := Auth { authoritative : option (excl A); own : A }.
Add Printing Constructor auth.
Arguments Auth {_} _ _.
Arguments authoritative {_} _.
Arguments own {_} _.
Notation "◯ a" := (Auth ExclUnit a) (at level 20).
Notation "● a" := (Auth (Excl a) ) (at level 20).
Notation "◯ a" := (Auth None a) (at level 20).
Notation "● a" := (Auth (Excl' a) ) (at level 20).
(* COFE *)
Section cofe.
Context {A : cofeT}.
Implicit Types a : excl A.
Implicit Types a : option (excl A).
Implicit Types b : A.
Implicit Types x y : auth A.
......@@ -72,20 +72,20 @@ Implicit Types x y : auth A.
Instance auth_valid : Valid (auth A) := λ x,
match authoritative x with
| Excl a => ( n, own x {n} a) a
| ExclUnit => own x
| ExclBot => False
| Excl' a => ( n, own x {n} a) a
| None => own x
| ExclBot' => False
end.
Global Arguments auth_valid !_ /.
Instance auth_validN : ValidN (auth A) := λ n x,
match authoritative x with
| Excl a => own x {n} a {n} a
| ExclUnit => {n} own x
| ExclBot => False
| Excl' a => own x {n} a {n} a
| None => {n} own x
| ExclBot' => False
end.
Global Arguments auth_validN _ !_ /.
Instance auth_core : Core (auth A) := λ x,
Auth (core (authoritative x)) (core (own x)).
Instance auth_pcore : PCore (auth A) := λ x,
Some (Auth (core (authoritative x)) (core (own x))).
Instance auth_op : Op (auth A) := λ x y,
Auth (authoritative x authoritative y) (own x own y).
......@@ -96,20 +96,21 @@ Proof.
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.
Proof. by destruct x as [[[]|]]. Qed.
Lemma own_validN n (x : auth A) : {n} x {n} own x.
Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed.
Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
Lemma auth_cmra_mixin : CMRAMixin (auth A).
Proof.
split.
apply cmra_total_mixin.
- eauto.
- by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- intros n [x a] [y b] [Hx Ha]; simpl in *;
destruct Hx; intros ?; cofe_subst; auto.
- intros [[] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
- intros n [x a] [y b] [Hx Ha]; simpl in *.
destruct Hx as [?? Hx|]; first destruct Hx; intros ?; cofe_subst; auto.
- intros [[[?|]|] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
naive_solver eauto using O.
- intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
- intros n [[[]|] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
- by split; simpl; rewrite assoc.
- by split; simpl; rewrite comm.
- by split; simpl; rewrite ?cmra_core_l.
......@@ -118,7 +119,7 @@ Proof.
by split; simpl; apply cmra_core_preserving.
- 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];
intros n [[[a1|]|] b1] [[[a2|]|] b2];
naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
- intros n x y1 y2 ? [??]; simpl in *.
destruct (cmra_extend n (authoritative x) (authoritative y1)
......@@ -127,12 +128,12 @@ Proof.
as (b&?&?&?); auto using own_validN.
by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
Qed.
Canonical Structure authR :=
CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
Canonical Structure authR := CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
Global Instance auth_cmra_discrete : CMRADiscrete A CMRADiscrete authR.
Proof.
split; first apply _.
intros [[] ?]; rewrite /= /cmra_valid /cmra_validN /=; auto.
intros [[[?|]|] ?]; rewrite /= /cmra_valid /cmra_validN /=; auto.
- setoid_rewrite <-cmra_discrete_included_iff.
rewrite -cmra_discrete_valid_iff. tauto.
- by rewrite -cmra_discrete_valid_iff.
......@@ -145,6 +146,7 @@ Proof.
- apply (@ucmra_unit_valid A).
- by intros x; constructor; rewrite /= left_id.
- apply _.
- do 2 constructor; simpl; apply (persistent_core _).
Qed.
Canonical Structure authUR :=
UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
......@@ -155,22 +157,23 @@ Lemma auth_equivI {M} (x y : auth A) :
Proof. by uPred.unseal. Qed.
Lemma auth_validI {M} (x : auth A) :
( x) ⊣⊢ (match authoritative x with
| Excl a => ( b, a own x b) a
| ExclUnit => own x
| ExclBot => False
| Excl' a => ( b, a own x b) a
| None => own x
| ExclBot' => False
end : uPred M).
Proof. uPred.unseal. by destruct x as [[]]. Qed.
Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
Lemma auth_frag_op a b : (a b) a b.
Proof. done. Qed.
Lemma auth_both_op a b : Auth (Excl a) b a b.
Lemma auth_both_op a b : Auth (Excl' a) b a b.
Proof. by rewrite /op /auth_op /= left_id. Qed.
Lemma auth_update a a' b b' :
( n af, {n} a a {n} a' af b {n} b' af {n} b)
a a' ~~> b b'.
Proof.
move=> Hab n [[?| |] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
intros Hab; apply cmra_total_update.
move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
destruct (Hab n (bf1 bf2)) as [Ha' ?]; auto.
{ by rewrite Ha left_id assoc. }
split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done].
......@@ -209,25 +212,29 @@ Arguments authUR : clear implicits.
(* Functor *)
Definition auth_map {A B} (f : A B) (x : auth A) : auth B :=
Auth (excl_map f (authoritative x)) (f (own x)).
Auth (excl_map f <$> authoritative x) (f (own x)).
Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
Proof. by destruct x; rewrite /auth_map excl_map_id. Qed.
Proof. by destruct x as [[[]|]]. Qed.
Lemma auth_map_compose {A B C} (f : A B) (g : B C) (x : auth A) :
auth_map (g f) x = auth_map g (auth_map f x).
Proof. by destruct x; rewrite /auth_map excl_map_compose. Qed.
Proof. by destruct x as [[[]|]]. Qed.
Lemma auth_map_ext {A B : cofeT} (f g : A B) x :
( x, f x g x) auth_map f x auth_map g x.
Proof. constructor; simpl; auto using excl_map_ext. Qed.
Instance auth_map_cmra_ne {A B : cofeT} n :
Proof.
constructor; simpl; auto.
apply option_fmap_setoid_ext=> a; by apply excl_map_ext.
Qed.
Instance auth_map_ne {A B : cofeT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
Proof.
intros f g Hf [??] [??] [??]; split; [by apply excl_map_cmra_ne|by apply Hf].
intros f g Hf [??] [??] [??]; split; simpl in *; [|by apply Hf].
apply option_fmap_ne; [|done]=> x y ?; by apply excl_map_ne.
Qed.
Instance auth_map_cmra_monotone {A B : ucmraT} (f : A B) :
CMRAMonotone f CMRAMonotone (auth_map f).
Proof.
split; try apply _.
- intros n [[a| |] b]; rewrite /= /cmra_validN /=; try
- 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.
......@@ -235,7 +242,7 @@ Qed.
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
CofeMor (auth_map f).
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.
Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
Program Definition authURF (F : urFunctor) : urFunctor := {|
urFunctor_car A B := authUR (urFunctor_car F A B);
......
This diff is collapsed.
......@@ -88,6 +88,8 @@ Section cofe_mixin.
Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
End cofe_mixin.
Hint Extern 1 (_ {_} _) => apply equiv_dist; assumption.
(** Discrete COFEs and Timeless elements *)
(* TODO: On paper, We called these "discrete elements". I think that makes
more sense. *)
......@@ -151,8 +153,7 @@ Section cofe.
Qed.
Lemma timeless_iff n (x : A) `{!Timeless x} y : x y x {n} y.
Proof.
split; intros; [by apply equiv_dist|].
apply (timeless _), dist_le with n; auto with lia.
split; intros; auto. apply (timeless _), dist_le with n; auto with lia.
Qed.
End cofe.
......@@ -569,6 +570,9 @@ Section option.
Proof. destruct 1; split; eauto. Qed.
Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
Proof. by inversion_clear 1. Qed.
Global Instance from_option_ne {B} (R : relation B) (f : A B) n :
Proper (dist n ==> R) f Proper (R ==> dist n ==> R) (from_option f).
Proof. destruct 3; simpl; auto. Qed.
Global Instance None_timeless : Timeless (@None A).
Proof. inversion_clear 1; constructor. Qed.
......@@ -592,14 +596,9 @@ End option.
Typeclasses Opaque option_dist.
Arguments optionC : clear implicits.
Instance from_option_ne {A B : cofeT} (f : A B) n :
Proper (dist n ==> dist n) f
Proper (dist n ==> dist n ==> dist n) (from_option f).
Proof. destruct 3; simpl; auto. Qed.
Instance option_fmap_ne {A B : cofeT} (f : A B) n:
Proper (dist n ==> dist n) f Proper (dist n==>dist n) (fmap (M:=option) f).
Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
Instance option_fmap_ne {A B : cofeT} n:
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
Proof. intros f f' Hf ?? []; constructor; auto. Qed.
Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
CofeMor (fmap f : optionC A optionC B).
Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
......
......@@ -2,7 +2,7 @@ From iris.algebra Require Export cmra.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments core _ _ !_ /.
Local Arguments pcore _ _ !_ /.
(* This is isomorphic to option, but has a very different RA structure. *)
Inductive dec_agree (A : Type) : Type :=
......@@ -26,19 +26,19 @@ Instance dec_agree_op : Op (dec_agree A) := λ x y,
| DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
| _, _ => DecAgreeBot
end.
Instance dec_agree_core : Core (dec_agree A) := id.
Instance dec_agree_pcore : PCore (dec_agree A) := Some.
Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
Proof.
split.
- apply _.
- apply _.
- intros x y cx ? [=<-]; eauto.
- apply _.
- intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|] ? [=<-]; by repeat (simplify_eq/= || case_match).
- intros [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|]; by repeat (simplify_eq/= || case_match).
- by intros [?|] [?|] ?.
- intros [?|] [?|] ?? [=<-]; eauto.
- by intros [?|] [?|] ?.
Qed.
......@@ -47,7 +47,7 @@ Canonical Structure dec_agreeR : cmraT :=
(* Some properties of this CMRA *)
Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
Proof. done. Qed.
Proof. by constructor. Qed.
Lemma dec_agree_ne a b : a b DecAgree a DecAgree b = DecAgreeBot.
Proof. intros. by rewrite /= decide_False. Qed.
......
......@@ -142,8 +142,8 @@ Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Lemma validity_valid_car_valid z : z validity_car z.
Proof. apply validity_prf. Qed.
Hint Resolve validity_valid_car_valid.
Program Instance validity_core : Core (validity A) := λ x,
Validity (core (validity_car x)) ( x) _.
Program Instance validity_pcore : PCore (validity A) := λ x,
Some (Validity (core (validity_car x)) ( x) _).
Solve Obligations with naive_solver eauto using dra_core_valid.
Program Instance validity_op : Op (validity A) := λ x y,
Validity (validity_car x validity_car y)
......@@ -152,7 +152,7 @@ Solve Obligations with naive_solver eauto using dra_op_valid.
Definition validity_ra_mixin : RAMixin (validity A).
Proof.
split.
apply ra_total_mixin; first eauto.
- intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
split; intros (?&?&?); split_and!;
first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
......@@ -176,6 +176,9 @@ Qed.
Canonical Structure validityR : cmraT :=
discreteR (validity A) validity_ra_mixin.
Global Instance validity_cmra_total : CMRATotal validityR.
Proof. rewrite /CMRATotal; eauto. Qed.
Lemma validity_update x y :
( c, x c validity_car x c y validity_car y c) x ~~> y.
Proof.
......
......@@ -5,11 +5,13 @@ Local Arguments valid _ _ !_ /.
Inductive excl (A : Type) :=
| Excl : A excl A
| ExclUnit : excl A
| ExclBot : excl A.
Arguments Excl {_} _.
Arguments ExclUnit {_}.
Arguments ExclBot {_}.
Notation Excl' x := (Some (Excl x)).
Notation ExclBot' := (Some ExclBot).
Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
match x with Excl a => Some a | _ => None end.
......@@ -21,12 +23,10 @@ Implicit Types x y : excl A.
(* Cofe *)
Inductive excl_equiv : Equiv (excl A) :=
| Excl_equiv a b : a b Excl a Excl b
| ExclUnit_equiv : ExclUnit ExclUnit
| ExclBot_equiv : ExclBot ExclBot.
Existing Instance excl_equiv.
Inductive excl_dist : Dist (excl A) :=
| Excl_dist a b n : a {n} b Excl a {n} Excl b
| ExclUnit_dist n : ExclUnit {n} ExclUnit
| ExclBot_dist n : ExclBot {n} ExclBot.
Existing Instance excl_dist.
......@@ -67,43 +67,31 @@ Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
Global Instance Excl_timeless a : Timeless a Timeless (Excl a).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
Proof. by inversion_clear 1; constructor. Qed.
Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Proof. by inversion_clear 1; constructor. Qed.
(* CMRA *)
Instance excl_valid : Valid (excl A) := λ x,
match x with Excl _ | ExclUnit => True | ExclBot => False end.
match x with Excl _ => True | ExclBot => False end.
Instance excl_validN : ValidN (excl A) := λ n x,
match x with Excl _ | ExclUnit => True | ExclBot => False end.
Instance excl_core : Core (excl A) := λ _, ExclUnit.
Instance excl_op : Op (excl A) := λ x y,
match x, y with
| Excl a, ExclUnit | ExclUnit, Excl a => Excl a
| ExclUnit, ExclUnit => ExclUnit
| _, _=> ExclBot
end.
match x with Excl _ => True | ExclBot => False end.
Instance excl_pcore : PCore (excl A) := λ _, None.
Instance excl_op : Op (excl A) := λ x y, ExclBot.
Lemma excl_cmra_mixin : CMRAMixin (excl A).
Proof.
split.
split; try discriminate.
- by intros n []; destruct 1; constructor.
- constructor.
- by destruct 1; intros ?.
- intros x; split. done. by move=> /(_ 0).
- intros n [?| |]; simpl; auto with lia.
- by intros [?| |] [?| |] [?| |]; constructor.
- by intros [?| |] [?| |]; constructor.
- by intros [?| |]; constructor.
- constructor.
- by intros [?| |] [?| |]; exists ExclUnit.
- by intros n [?| |] [?| |].
- intros n [?|]; simpl; auto with lia.
- by intros [?|] [?|] [?|]; constructor.
- by intros [?|] [?|]; constructor.
- by intros n [?|] [?|].
- intros n x y1 y2 ? Hx.
by exists match y1, y2 with
| Excl a1, Excl a2 => (Excl a1, Excl a2)
| ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot)
| ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
end; destruct y1, y2; inversion_clear Hx; repeat constructor.
Qed.
Canonical Structure exclR :=
......@@ -112,57 +100,49 @@ Canonical Structure exclR :=
Global Instance excl_cmra_discrete : Discrete A CMRADiscrete exclR.
Proof. split. apply _. by intros []. Qed.
Instance excl_empty : Empty (excl A) := ExclUnit.
Lemma excl_ucmra_mixin : UCMRAMixin (excl A).
Proof. split. done. by intros []. apply _. Qed.
Canonical Structure exclUR :=
UCMRAT (excl A) excl_cofe_mixin excl_cmra_mixin excl_ucmra_mixin.
Lemma excl_validN_inv_l n x a : {n} (Excl a x) x = .
Proof. by destruct x. Qed.
Lemma excl_validN_inv_r n x a : {n} (x Excl a) x = .
Proof. by destruct x. Qed.
Lemma Excl_includedN n a x : {n} x Excl a {n} x x {n} Excl a.
Proof.
intros Hvalid; split; [|by intros ->].
intros [z ?]; cofe_subst. by rewrite (excl_validN_inv_l n z a).
Qed.
(** Internalized properties *)
Lemma excl_equivI {M} (x y : excl A) :
(x y) ⊣⊢ (match x, y with
| Excl a, Excl b => a b
| ExclUnit, ExclUnit | ExclBot, ExclBot => True
| ExclBot, ExclBot => True
| _, _ => False
end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma excl_validI {M} (x : excl A) :
( x) ⊣⊢ (if x is ExclBot then False else True : uPred M).
x ⊣⊢ (if x is ExclBot then False else True : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** ** Local updates *)
Global Instance excl_local_update y :
LocalUpdate (λ x, if x is Excl _ then y else False) (λ _, y).
Proof. split. apply _. by destruct y; intros n [a| |] [b'| |]. Qed.
Proof. split. apply _. by destruct y; intros n [a|] [b'|]. Qed.
(** Updates *)
Lemma excl_update a y : y Excl a ~~> y.
Proof. destruct y; by intros ?? [?| |]. Qed.
Proof. destruct y=> ? n [z|]; eauto. Qed.
Lemma excl_updateP (P : excl A Prop) a y : y P y Excl a ~~>: P.
Proof. intros ?? n z ?; exists y. by destruct y, z as [?| |]. Qed.
Proof. destruct y=> ?? n [z|]; eauto. Qed.
(** Option excl *)
Lemma excl_validN_inv_l n mx a : {n} (Excl' a mx) mx = None.
Proof. by destruct mx. Qed.
Lemma excl_validN_inv_r n mx a : {n} (mx Excl' a) mx = None.
Proof. by destruct mx. Qed.
Lemma Excl_includedN n a mx : {n} mx Excl' a {n} mx mx {n} Excl' a.
Proof.
intros Hvalid; split; [|by intros ->].
intros [z ?]; cofe_subst. by rewrite (excl_validN_inv_l n z a).
Qed.
End excl.
Arguments exclC : clear implicits.
Arguments exclR : clear implicits.
Arguments exclUR : clear implicits.
(* Functor *)
Definition excl_map {A B} (f : A B) (x : excl A) : excl B :=
match x with
| Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
end.
match x with Excl a => Excl (f a) | ExclBot => ExclBot end.
Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
Proof. by destruct x. Qed.
Lemma excl_map_compose {A B C} (f : A B) (g : B C) (x : excl A) :
......@@ -171,14 +151,14 @@ Proof. by destruct x. Qed.
Lemma excl_map_ext {A B : cofeT} (f g : A B) x :
( x, f x g x) excl_map f x excl_map g x.
Proof. by destruct x; constructor. Qed.
Instance excl_map_cmra_ne {A B : cofeT} n :
Instance excl_map_ne {A B : cofeT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
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; try apply _.
- by intros n [a| |].
- 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.
......@@ -187,9 +167,9 @@ Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
Program Definition exclURF (F : cFunctor) : urFunctor := {|
urFunctor_car A B := (exclUR (cFunctor_car F A B) : ucmraT);
urFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
Program Definition exclRF (F : cFunctor) : rFunctor := {|
rFunctor_car A B := (exclR (cFunctor_car F A B));
rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
|}.
Next Obligation.
intros F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
......@@ -203,8 +183,8 @@ Next Obligation.
apply excl_map_ext=>y; apply cFunctor_compose.
Qed.
Instance exclURF_contractive F :
cFunctorContractive F urFunctorContractive (exclURF F).
Instance exclRF_contractive F :
cFunctorContractive F rFunctorContractive (exclRF F).
Proof.
intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
Qed.
This diff is collapsed.
......@@ -93,14 +93,14 @@ Context `{Countable K} {A : cmraT}.
Implicit Types m : gmap K A.
Instance gmap_op : Op (gmap K A) := merge op.
Instance gmap_core : Core (gmap K A) := fmap core.
Instance gmap_pcore : PCore (gmap K A) := λ m, Some (omap pcore m).
Instance gmap_valid : Valid (gmap K A) := λ m, i, (m !! i).
Instance gmap_validN : ValidN (gmap K A) := λ n m, i, {n} (m !! i).
Lemma lookup_op m1 m2 i : (m1 m2) !! i = m1 !! i m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_core m i : core m !! i = core (m !! i).
Proof. by apply lookup_fmap. Qed.
Proof. by apply lookup_omap. Qed.
Lemma lookup_included (m1 m2 : gmap K A) : m1 m2 i, m1 !! i m2 !! i.
Proof.
......@@ -120,20 +120,21 @@ Qed.
Lemma gmap_cmra_mixin : CMRAMixin (gmap K A).
Proof.
split.
- by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
- by intros n m1 m2 Hm i; rewrite !lookup_core (Hm i).
- by intros n m1 m2 Hm ? i; rewrite -(Hm i).
apply cmra_total_mixin.
- eauto.
- intros n m1 m2 m3 Hm i; by rewrite !lookup_op (Hm i).
- intros n m1 m2 Hm i; by rewrite !lookup_core (Hm i).
- intros n m1 m2 Hm ? i; by rewrite -(Hm i).
- intros m; split.
+ by intros ? n i; apply cmra_valid_validN.
+ intros Hm i; apply cmra_valid_validN=> n; apply Hm.
- intros n m Hm i; apply cmra_validN_S, Hm.
- by intros m1 m2 m3 i; rewrite !lookup_op assoc.
- by intros m1 m2 i; rewrite !lookup_op comm.
- by intros m i; rewrite lookup_op !lookup_core cmra_core_l.
- by intros m i; rewrite !lookup_core cmra_core_idemp.
- intros x y; rewrite !lookup_included; intros Hm i.
by rewrite !lookup_core; apply cmra_core_preserving.
- 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.
- 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.
......@@ -164,6 +165,7 @@ Proof.
- by intros i; rewrite lookup_empty.
- by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- apply gmap_empty_timeless.
- constructor=> i. by rewrite lookup_omap lookup_empty.
Qed.
Canonical Structure gmapUR :=
UCMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin gmap_ucmra_mixin.
......@@ -201,42 +203,51 @@ Lemma singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
Lemma insert_singleton_opN n m i x :
m !! i = None m !! i {n} Some (core x) <[i:=x]> m {n} {[ i := x ]} m.
m !! i = None <[i:=x]> m {n} {[ i := x ]} m.
Proof.
intros Hi j; destruct (decide (i = j)) as [->|];
[|by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id].
rewrite lookup_op lookup_insert lookup_singleton.
by destruct Hi as [->| ->]; constructor; rewrite ?cmra_core_r.
intros Hi j; destruct (decide (i = j)) as [->|].
- by rewrite lookup_op lookup_insert lookup_singleton Hi right_id.
- by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id.
Qed.
Lemma insert_singleton_op m i x :
m !! i = None m !! i Some (core x) <[i:=x]> m {[ i := x ]} m.
Lemma insert_singleton_op m i x : m !! i = None <[i:=x]> m {[ i := x ]} m.
Proof. rewrite !equiv_dist; naive_solver eauto using insert_singleton_opN. Qed.