From 121a4a75e9041a9eaa84ccbe3d6b49f9d447993b Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Mon, 10 Oct 2016 18:00:11 +0200
Subject: [PATCH] Add PersistentP instances for own(S).

Initial proof by Jan-Oliver Kaiser, adapted by Robbert Krebbers.
---
 algebra/sts.v       | 5 +++++
 program_logic/sts.v | 4 ++++
 2 files changed, 9 insertions(+)

diff --git a/algebra/sts.v b/algebra/sts.v
index 6d7346321..290cbc225 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -376,6 +376,11 @@ Proof.
     eapply closed_steps, Hsup; first done. set_solver +Hs'.
 Qed.
 
+Global Instance sts_frag_peristent S : Persistent (sts_frag S ∅).
+Proof.
+  constructor; split=> //= [[??]]. by rewrite /dra.dra_core /= sts.up_closed.
+Qed.
+
 (** Inclusion *)
 (* This is surprisingly different from to_validity_included. I am not sure
    whether this is because to_validity_included is non-canonical, or this
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 5163df446..06c1f37ad 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -44,6 +44,10 @@ Section definitions.
   Proof. solve_proper. Qed.
   Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ).
   Proof. apply _. Qed.
+  Global Instance sts_own_peristent s : PersistentP (sts_own s ∅).
+  Proof. apply _. Qed.
+  Global Instance sts_ownS_peristent S : PersistentP (sts_ownS S ∅).
+  Proof. apply _. Qed.
 End definitions.
 
 Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
-- 
GitLab