Commit ae1ed016 authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Make core_id_local_update work with fraction

parent 213fc044
......@@ -207,6 +207,13 @@ Proof.
by move=> /agree_op_invN->; rewrite agree_idemp.
Lemma to_agree_includedN n a b : to_agree a {n}to_agree b a {n} b.
split; last by intros ->.
intros (x & Heq). destruct Heq as [_ Hincl].
by destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+.
Lemma to_agree_included a b : to_agree a to_agree b a b.
split; last by intros ->.
......@@ -385,11 +385,19 @@ Proof.
exact: cmra_update_op_l.
Lemma auth_update_core_id a b `{!CoreId b} :
b a a ~~> a b.
Lemma auth_update_core_id q a b `{!CoreId b} :
b a {q} a ~~> {q} a b.
intros Hincl. apply: auth_update_alloc.
rewrite -(left_id ε _ b). apply: core_id_local_update. done.
intros Heq%core_id_extract; last done. apply cmra_total_update.
move=> n [[[q' ag]|] bf1] [/= VL [a0 [Eq [[bf2 Ha] VL2]]]]; do 2 red; simpl in *.
+ split; first done.
exists a0. split; last split; try done. exists bf2.
assert (a {n} a0) as Eq2. { apply to_agree_includedN. exists ag. done. }
by rewrite left_id -Eq2 -assoc -comm Heq Eq2 Ha left_id.
+ split; first done. exists a0.
split; first done. split; last done. exists bf2.
apply (inj to_agree) in Eq.
by rewrite left_id -Eq -assoc -comm Heq Eq Ha left_id.
Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε) a b ~~> a'.
......@@ -59,14 +59,6 @@ Section updates.
destruct mz as [z|]; [|done]. by destruct (id_freeN_r n n x z).
Lemma core_id_local_update x y z `{!CoreId y} :
y x (x, z) ~l~> (x, z y).
intros Hincl n mf ? Heq; simpl in *; split; first done.
rewrite [x]core_id_extract // Heq. destruct mf as [f|]; last done.
simpl. rewrite -assoc [f y]comm assoc //.
Lemma local_update_discrete `{!CmraDiscrete A} (x y x' y' : A) :
(x,y) ~l~> (x',y') mz, x x y ? mz x' x' y' ? mz.
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