Merge branch 'feat-na-own-empty' into 'master'

add lemmas for na_own p ∅

See merge request iris/iris!1044

CHANGELOG.md

@@ -3,6 +3,13 @@ way the logic is used on paper.  We also document changes in the Coq
 development; every API-breaking change should be listed, but not every new
 lemma.
 
+## Iris master
+
+**Changes in `base_logic`:**
+
+* Add lemma `na_own_empty` and persistence instance for `na_own p ∅` for
+  non-atomic invariant tokens. (by Benjamin Peters)
+
 ## Iris 4.2.0 (2024-04-12)
 
 The highlights of this release are:

iris/base_logic/lib/na_invariants.v

@@ -45,6 +45,9 @@ Section proofs.
   Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
   Proof. rewrite /na_inv; apply _. Qed.
 
+  Global Instance na_own_empty_persistent p : Persistent (na_own p ∅).
+  Proof. rewrite /na_own; apply _. Qed.
+
   Lemma na_inv_iff p N P Q : na_inv p N P -∗ ▷ □ (P ↔ Q) -∗ na_inv p N Q.
   Proof.
     rewrite /na_inv. iIntros "(%i & % & HI) #HPQ".
@@ -109,6 +112,9 @@ Section proofs.
     - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
   Qed.
 
+  Lemma na_own_empty p : ⊢ |==> na_own p ∅.
+  Proof. apply: own_unit. Qed.
+
   Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N := {}.
 
   Global Instance into_acc_na p F E N P :