From 3cebc8a15941da4f4ee1f8b31517ee7fd308943a Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 10 Aug 2021 14:19:02 +0200
Subject: [PATCH] na_invariants: deduplicate proof of fresh_inv_name

---
 iris/base_logic/lib/na_invariants.v | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index f94042796..d59861a89 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -80,12 +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))).
-        intros Ef. exists (coPpick (↑ N ∖ gset_to_coPset Ef)).
-        rewrite -elem_of_gset_to_coPset comm -elem_of_difference.
-        apply coPpick_elem_of=> Hfin.
-        eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
-        apply gset_to_coPset_finite. }
+      - apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ (↑N:coPset)))=> Ef.
+        apply fresh_inv_name. }
     simpl. iDestruct "Hm" as %(<- & i & -> & ?).
     rewrite /na_inv.
     iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).
-- 
GitLab