From 10de2067d88b658ca7de9414a9ad6de49fbaba5f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Feb 2016 15:41:42 +0100
Subject: [PATCH] prove sts.opening

---
 program_logic/sts.v | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/program_logic/sts.v b/program_logic/sts.v
index 893606f76..d732966ca 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -93,7 +93,20 @@ Section sts.
     (▷ φ s' ★ own StsI γ (sts_auth sts.(st) sts.(tok) s T))
     ⊑ pvs E E (▷ inv StsI sts γ φ ★ own StsI γ (sts_frag sts.(st) sts.(tok) S' T')).
   Proof.
-  Abort.
+    intros Hstep Hin Hcl. rewrite /inv -(exist_intro s').
+    rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
+    rewrite -pvs_frame_l. apply sep_mono; first done.
+    rewrite -later_intro.
+    transitivity (pvs E E (own StsI γ (sts_auth sts.(st) sts.(tok) s' T'))).
+    { by apply own_update, sts_update. }
+    apply pvs_mono. rewrite -own_op. apply equiv_spec, own_proper.
+    split; first split; simpl.
+    - intros _. by eapply closed_disjoint.
+    - intros ?. split_ands; first by solve_elem_of-.
+      + done.
+      + constructor; [done | solve_elem_of-].
+    - intros _. constructor. solve_elem_of-.
+  Qed.
 
 End sts.
 
-- 
GitLab