Commit 57e5d1ed authored by Robbert's avatar Robbert

Merge branch 'ralf/auth-core-id' into 'master'

show auth_update_core_id

See merge request !282
parents 4832f461 1a15694e
Pipeline #18026 passed with stage
in 14 minutes and 2 seconds
......@@ -362,8 +362,17 @@ Proof.
exists a'. split; [done|]. split; [|done]. exists bf2.
by rewrite left_id -assoc.
Qed.
Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b') a ~~> a' b'.
Proof. intros. rewrite -(right_id _ _ ( a)). by apply auth_update. Qed.
Lemma auth_update_core_id a b `{!CoreId b} :
b a a ~~> a b.
Proof.
intros Hincl. apply: auth_update_alloc.
rewrite -(left_id ε _ b). apply: core_id_local_update. done.
Qed.
Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε) a b ~~> a'.
Proof. intros. rewrite -(right_id _ _ ( a')). by apply auth_update. Qed.
......
......@@ -362,10 +362,6 @@ Proof.
intros Hv Hx%cmra_pcore_l. move: Hv; rewrite -Hx. apply cmra_valid_op_l.
Qed.
(** ** CoreId elements *)
Lemma core_id_dup x `{!CoreId x} : x x x.
Proof. by apply cmra_pcore_dup' with x. Qed.
(** ** Exclusive elements *)
Lemma exclusiveN_l n x `{!Exclusive x} y : {n} (x y) False.
Proof. intros. eapply (exclusive0_l x y), cmra_validN_le; eauto with lia. Qed.
......@@ -462,6 +458,19 @@ Proof.
by rewrite Hx1 Hx2.
Qed.
(** ** CoreId elements *)
Lemma core_id_dup x `{!CoreId x} : x x x.
Proof. by apply cmra_pcore_dup' with x. Qed.
Lemma core_id_extract x y `{!CoreId x} :
x y y y x.
Proof.
intros ?.
destruct (cmra_pcore_mono' x y x) as (cy & Hcy & [x' Hx']); [done|exact: core_id|].
rewrite -(cmra_pcore_r y) //. rewrite Hx' -!assoc. f_equiv.
rewrite [x' x]comm assoc -core_id_dup. done.
Qed.
(** ** Total core *)
Section total_core.
Local Set Default Proof Using "Type*".
......
......@@ -59,6 +59,14 @@ Section updates.
destruct mz as [z|]; [|done]. by destruct (id_freeN_r n n x z).
Qed.
Lemma core_id_local_update x y z `{!CoreId y} :
y x (x, z) ~l~> (x, z y).
Proof.
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 //.
Qed.
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.
Proof.
......
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