From 7c9f06f7645c58b65f14f68c3ea5f6f8fc8a7464 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 24 Jan 2018 16:23:21 +0100
Subject: [PATCH] Show that non-atomic invariants are closed under logical
 equivalence.

---
 theories/base_logic/lib/na_invariants.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index e6ab08fbe..2e736737e 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -43,6 +43,14 @@ Section proofs.
   Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
   Proof. rewrite /na_inv; apply _. Qed.
 
+  Lemma na_inv_iff p N P Q : ▷ □ (P ↔ Q) -∗ na_inv p N P -∗ na_inv p N Q.
+  Proof.
+    iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
+    iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
+    iNext. iAlways. iSplit; (iIntros "[[? Ho]|?]";
+      [iLeft; iFrame "Ho"; by iApply "HPQ"|by iRight]).
+  Qed.
+
   Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
   Proof. by apply own_alloc. Qed.
 
-- 
GitLab