Simplify NA-inv protocol.

iris/base_logic/lib/na_invariants.v

@@ -24,8 +24,7 @@ Section defs.
     own p (CoPset E, GSet ∅).
 
   Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
-    ∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧
-         inv N (P ∗ own p (ε, GSet {[i]}) ∨ na_own p {[i]}).
+    ∃ i, inv N (P ∗ own p (ε, GSet {[i]}) ∨ na_own p (↑N)).
 End defs.
 
 Global Instance: Params (@na_inv) 3 := {}.
@@ -47,9 +46,8 @@ Section proofs.
 
   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".
-    iExists i. iSplit; first done. iApply (inv_iff with "HI").
-    iIntros "!> !>".
+    rewrite /na_inv. iIntros "(%i & HI) #HPQ".
+    iExists i. iApply (inv_iff with "HI"). iIntros "!> !>".
     iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
   Qed.
 
@@ -82,9 +80,8 @@ Section proofs.
     iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
     { apply prod_updateP'.
       - apply cmra_updateP_id, (reflexivity (R:=eq)).
-      - apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ (↑N:coPset)))=> Ef.
-        apply fresh_inv_name. }
-    simpl. iDestruct "Hm" as %(<- & i & -> & ?).
+      - apply gset_disj_alloc_empty_updateP'. }
+    simpl. iDestruct "Hm" as %(<- & i & ->).
     rewrite /na_inv.
     iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).
     iNext. iLeft. by iFrame.
@@ -95,10 +92,9 @@ Section proofs.
     na_inv p N P -∗ na_own p F ={E}=∗ ▷ P ∗ na_own p (F∖↑N) ∗
                        (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F).
   Proof.
-    rewrite /na_inv. iIntros (??) "#(%i & % & Hinv) Htoks".
+    rewrite /na_inv. iIntros (??) "#(%i & Hinv) Htoks".
     rewrite [F as X in na_own p X](union_difference_L (↑N) F) //.
-    rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..].
-    iDestruct "Htoks" as "[[Htoki $] $]".
+    rewrite ?na_own_union; [|set_solver..]. iDestruct "Htoks" as "[Htoki $]".
     iInv "Hinv" as "[[$ >Hdis]|>Htoki2]" "Hclose".
     - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
       iIntros "!> [HP $]".
@@ -106,7 +102,8 @@ Section proofs.
       + iCombine "Hdis Hdis2" gives %[_ Hval%gset_disj_valid_op].
         set_solver.
       + iSplitR "Hitok"; last by iFrame. eauto with iFrame.
-    - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
+    - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?.
+      destruct (fresh_inv_name ∅ N) as (? & _ & ?). set_solver.
   Qed.
 
   Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N := {}.