From 0b860f2a26a0b193345c9a703c8a133d087fefe4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Nov 2019 16:10:59 +0100
Subject: [PATCH] Simplify definition of invariant model.

Due to the new semantic invariants (!319) we no longer need to
close the model (i.e. `inv_def`) to be contractive, the semantic
invariant definition (i.e. `inv`) is already contractive.
---
 theories/base_logic/lib/invariants.v | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 6671535a2..d5d637e48 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -25,21 +25,18 @@ Section inv.
 
   (** ** Internal model of invariants *)
   Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ :=
-    (∃ i P', ⌜i ∈ (↑N:coPset)⌝ ∧ ▷ □ (P' ↔ P) ∧ ownI i P')%I.
+    (∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧ ownI i P)%I.
 
   Lemma own_inv_open E N P :
     ↑N ⊆ E → own_inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
   Proof.
-    rewrite uPred_fupd_eq /uPred_fupd_def.
-    iDestruct 1 as (i P') "(Hi & #HP' & #HiP)".
+    rewrite uPred_fupd_eq /uPred_fupd_def. iDestruct 1 as (i) "[Hi #HiP]".
     iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
     rewrite {1 4}(union_difference_L (↑ N) E) // ownE_op; last set_solver.
     rewrite {1 5}(union_difference_L {[ i ]} (↑ N)) // ownE_op; last set_solver.
     iIntros "(Hw & [HE $] & $) !> !>".
-    iDestruct (ownI_open i with "[$Hw $HE $HiP]") as "($ & HP & HD)".
-    iDestruct ("HP'" with "HP") as "$".
-    iIntros "HP [Hw $] !> !>". iApply (ownI_close _ P'). iFrame "HD Hw HiP".
-    iApply "HP'". iFrame.
+    iDestruct (ownI_open i with "[$Hw $HE $HiP]") as "($ & $ & HD)".
+    iIntros "HP [Hw $] !> !>". iApply (ownI_close _ P). by iFrame.
   Qed.
 
   Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ (↑N:coPset).
@@ -56,7 +53,7 @@ Section inv.
     rewrite uPred_fupd_eq. iIntros "HP [Hw $]".
     iMod (ownI_alloc (.∈ (↑N : coPset)) P with "[$HP $Hw]")
       as (i ?) "[$ ?]"; auto using fresh_inv_name.
-    do 2 iModIntro. iExists i, P. rewrite -(iff_refl True%I). auto.
+    do 2 iModIntro. iExists i. auto.
   Qed.
 
   Lemma own_inv_alloc_open N E P :
@@ -71,7 +68,7 @@ Section inv.
       rewrite assoc_L -!union_difference_L //. set_solver. }
     do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw".
     iSplitL "Hi".
-    { iExists i, P. rewrite -(iff_refl True%I). auto. }
+    { iExists i. auto. }
     iIntros "HP [Hw HE\N]".
     iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[$ HEi]".
     do 2 iModIntro. iSplitL; [|done].
-- 
GitLab