show auth_update_core_id

theories/algebra/auth.v

@@ -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.
 

theories/algebra/cmra.v

@@ -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*".

theories/algebra/local_updates.v

@@ -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.