From 7209226cbd6882ef5ee978b094d85e9e392e1c29 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Jan 2016 09:15:28 +0100
Subject: [PATCH] Invariants are AlwaysStable.

---
 iris/ownership.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/iris/ownership.v b/iris/ownership.v
index d439589c7..c49a46881 100644
--- a/iris/ownership.v
+++ b/iris/ownership.v
@@ -25,15 +25,14 @@ Proof.
   apply (_: Proper (_ ==> _) iProp_unfold), Later_contractive in HPQ.
   by unfold inv; rewrite HPQ.
 Qed.
-Lemma inv_duplicate i P : inv i P ≡ (inv i P ★ inv i P)%I.
-Proof.
-  by rewrite /inv -uPred.own_op Res_op
-    map_op_singleton agree_idempotent !(left_id _ _).
-Qed.
 Lemma always_inv i P : (□ inv i P)%I ≡ inv i P.
 Proof.
   by apply uPred.always_own; rewrite Res_unit !ra_unit_empty map_unit_singleton.
 Qed.
+Global Instance inv_always_stable i P : AlwaysStable (inv i P).
+Proof. by rewrite /AlwaysStable always_inv. Qed.
+Lemma inv_sep_dup i P : inv i P ≡ (inv i P ★ inv i P)%I.
+Proof. apply (uPred.always_sep_dup' _). Qed.
 
 (* physical state *)
 Lemma ownP_twice σ1 σ2 : (ownP σ1 ★ ownP σ2 : iProp Σ) ⊑ False.
-- 
GitLab