Stronger Invariant Allocation Rules

Allocating Iris invariants currently combines allocating and closing the invariant. I see no reason to do that other than it being somewhat convenient for 80% of the use cases. Here's a stronger invariant allocation rule that we need for our GPS work. This is not (yet) a pull request for - just a copy of my local file. But I wanted to dump this here so that you guys can discuss if you want it in Iris.

From iris.base_logic.lib Require Export own wsat.
From iris.prelude Require Export coPset.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.

From iris.base_logic.lib Require Export fancy_updates namespaces.
From iris.base_logic.lib Require Import wsat invariants.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics coq_tactics intro_patterns.

Section wsat.
Import invG.
Context `{invG Σ}.
Implicit Types P : iProp Σ.

Lemma ownI_alloc_strong φ 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.

Section invariants.
Import uPred.
Context `{invG Σ}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Σ.

Lemma ownE_proper : Proper ((≡) ==> (≡)) ownE.
Proof.
  rewrite /ownE => ? ? Eq. f_equiv. f_equiv. by apply leibniz_equiv.
Qed.

Lemma inv_alloc_strong 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_strong (∈ ↑ 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 ownE_proper; [done|].
      rewrite assoc. rewrite <-!union_difference; 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 ownE_proper; [done|].
      rewrite <-!union_difference; set_solver.
Qed.
End invariants.