Commit 121a4a75 authored by Janno's avatar Janno Committed by Robbert Krebbers

Add PersistentP instances for own(S).

Initial proof by Jan-Oliver Kaiser, adapted by Robbert Krebbers.
parent c7240c72
......@@ -376,6 +376,11 @@ Proof.
eapply closed_steps, Hsup; first done. set_solver +Hs'.
Global Instance sts_frag_peristent S : Persistent (sts_frag S ).
constructor; split=> //= [[??]]. by rewrite /dra.dra_core /= sts.up_closed.
(** 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
......@@ -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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment