prove that we can always own an empty fragment of auth

algebra/cmra.v

@@ -378,6 +378,8 @@ Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1
 Proof.
   rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
 Qed.
+Lemma cmra_update_id x : x ~~> x.
+Proof. intro. auto. Qed.
 
 Section identity_updates.
   Context `{Empty A, !CMRAIdentity A}.

program_logic/auth.v

@@ -35,6 +35,10 @@ Section auth.
     by rewrite always_and_sep_l.
   Qed.
 
+  Lemma auth_empty γ E :
+    True ⊑ pvs E E (auth_own γ ∅).
+  Proof. by rewrite own_update_empty /auth_own. Qed.
+
   Context {Hφ : ∀ n, Proper (dist n ==> dist n) φ}.
 
   Lemma auth_opened E a γ :

program_logic/ghost_ownership.v

@@ -93,7 +93,7 @@ Proof.
     by rewrite -(exist_intro γ).
 Qed.
 
-Lemma own_updateP γ a P E :
+Lemma own_updateP P γ a E :
   a ~~>: P → own i γ a ⊑ pvs E E (∃ a', ■ P a' ∧ own i γ a').
 Proof.
   intros Ha.
@@ -105,7 +105,7 @@ Proof.
     rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
 Qed.
 
-Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} γ a P E :
+Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} P γ E :
   ∅ ~~>: P → True ⊑ pvs E E (∃ a, ■ P a ∧ own i γ a).
 Proof.
   intros Hemp.
@@ -119,7 +119,14 @@ Qed.
 
 Lemma own_update γ a a' E : a ~~> a' → own i γ a ⊑ pvs E E (own i γ a').
 Proof.
-  intros; rewrite (own_updateP _ _ (a' =)); last by apply cmra_update_updateP.
-  by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
+  intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
+  by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
+Qed.
+
+Lemma own_update_empty `{Empty A, !CMRAIdentity A} γ E :
+  True ⊑ pvs E E (own i γ ∅).
+Proof.
+  rewrite (own_updateP_empty (∅ =)); last by apply cmra_updateP_id.
+  apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
 Qed.
 End global.