From 3e84ca431c0a5ba928e541aea05e3ecbe1ba4c4e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 Mar 2023 15:46:42 +0100
Subject: [PATCH] Prove that invariants are "except 0".
---
iris/base_logic/lib/invariants.v | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index d3f82d3eb..017795a34 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -161,7 +161,16 @@ Section inv.
iIntros "!> [HP HQ]". by iApply "HcloseQ".
Qed.
+ Lemma except_0_inv N P : ◇ inv N P ⊢ inv N P.
+ Proof.
+ rewrite inv_unseal /inv_def. iIntros "#H !>" (E ?).
+ iMod "H". by iApply "H".
+ Qed.
+
(** ** Proof mode integration *)
+ Global Instance is_except_0_inv N P : IsExcept0 (inv N P).
+ Proof. apply except_0_inv. Qed.
+
Global Instance into_inv_inv N P : IntoInv (inv N P) N := {}.
Global Instance into_acc_inv N P E:
--
GitLab