Add a rule to alloocate an invariant and open it

Fixes #59
Proof entirely by @janno

theories/base_logic/lib/invariants.v

@@ -41,6 +41,33 @@ Proof.
   - rewrite /uPred_except_0; eauto.
 Qed.
 
+Lemma inv_alloc_open N E P :
+  ↑N ⊆ E → True ={E, E∖↑N}=∗ inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
+Proof.
+  rewrite inv_eq /inv_def fupd_eq /fupd_def.
+  iIntros (Sub) "[Hw HE]".
+  iMod (ownI_alloc_open (∈ ↑ N) P with "Hw") as (i) "(% & Hw & #Hi & HD)".
+  - intros Ef. exists (coPpick (↑ N ∖ coPset.of_gset Ef)).
+    rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
+    apply coPpick_elem_of=> Hfin.
+    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
+    apply of_gset_finite.
+  - iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I with "[HE]" as "(HEi & HEN\i & HE\N)".
+    { rewrite -?ownE_op; [|set_solver|set_solver].
+      rewrite assoc_L. rewrite <-!union_difference_L; try done; set_solver. }
+    iModIntro. rewrite /uPred_except_0. iRight. iFrame.
+    iSplitL "Hw HEi".
+    + by iApply "Hw".
+    + iSplitL "Hi"; [eauto|].
+      iIntros "HP [Hw HE\N]".
+      iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[? HEi]".
+      iModIntro. iRight. iFrame. iSplitL; [|done].
+      iCombine "HEi" "HEN\i" as "HEN".
+      iCombine "HEN" "HE\N" as "HE".
+      rewrite -?ownE_op; [|set_solver|set_solver].
+      rewrite <-!union_difference_L; try done; set_solver.
+Qed.
+
 Lemma inv_open E N P :
   ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
 Proof.

theories/base_logic/lib/wsat.v

@@ -142,4 +142,28 @@ Proof.
   iApply (big_sepM_insert _ I); first done.
   iFrame "HI". iLeft. by rewrite /ownD; iFrame.
 Qed.
+
+Lemma ownI_alloc_open φ P :
+  (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
+  wsat ==∗ ∃ i, ⌜φ i⌝ ∗ (ownE {[i]} -∗ wsat) ∗ ownI i P ∗ ownD {[i]}.
+Proof.
+  iIntros (Hfresh) "Hw". iDestruct "Hw" as (I) "[? HI]".
+  iMod (own_empty (gset_disjUR positive) disabled_name) as "HD".
+  iMod (own_updateP with "HD") as "HD".
+  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
+    intros E. destruct (Hfresh (E ∪ dom _ I))
+      as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
+  iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?).
+  iMod (own_update with "Hw") as "[Hw HiP]".
+  { eapply auth_update_alloc,
+     (alloc_singleton_local_update _ i (invariant_unfold P)); last done.
+    by rewrite /= lookup_fmap HIi. }
+  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
+  rewrite -/(ownD _). iFrame "HD".
+  iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
+  { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
+  iApply (big_sepM_insert _ I); first done.
+  iFrame "HI". by iRight.
+Qed.
+
 End wsat.