prove sts.opened; state sts.closing

program_logic/ghost_ownership.v

@@ -77,6 +77,8 @@ Proof.
 Qed.
 Lemma own_valid_r γ a : own i γ a ⊑ (own i γ a ★ ✓ a).
 Proof. apply (uPred.always_entails_r _ _), own_valid. Qed.
+Lemma own_valid_l γ a : own i γ a ⊑ (✓ a ★ own i γ a).
+Proof. by rewrite comm -own_valid_r. Qed.
 Global Instance own_timeless γ a : Timeless a → TimelessP (own i γ a).
 Proof. unfold own; apply _. Qed.
 

program_logic/sts.v

@@ -20,12 +20,13 @@ Arguments Sts : clear implicits.
 
 Class InG Λ Σ (i : gid) {A B} (sts : Sts A B) := {
   inG :> ghost_ownership.InG Λ Σ i (stsRA sts.(st) sts.(tok));
+  inh :> Inhabited A;
 }.
 
 Section definitions.
   Context {Λ Σ A B} (i : gid) (sts : Sts A B) `{!InG Λ Σ i sts} (γ : gname).
   Definition inv  (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
-    (∃ s, own i γ (sts_auth sts.(st) sts.(tok) s set_empty) ★ φ s)%I.
+    (∃ s, own i γ (sts_auth sts.(st) sts.(tok) s ∅) ★ φ s)%I.
   Definition states (S : set A) (T: set B) : iPropG Λ Σ :=
     (■ closed sts.(st) sts.(tok) S T ∧
      own i γ (sts_frag sts.(st) sts.(tok) S T))%I.
@@ -67,6 +68,33 @@ Section sts.
     by rewrite always_and_sep_l.
   Qed.
 
+  Lemma opened E γ S T :
+    (▷ inv StsI sts γ φ ★ own StsI γ (sts_frag sts.(st) sts.(tok) S T))
+      ⊑ pvs E E (∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own StsI γ (sts_auth sts.(st) sts.(tok) s T)).
+  Proof.
+    rewrite /inv. rewrite later_exist sep_exist_r. apply exist_elim=>s.
+    rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
+    rewrite -(exist_intro s).
+    rewrite [(_ ★ ▷φ _)%I]comm -!assoc -own_op -[(▷φ _ ★ _)%I]comm.
+    rewrite own_valid_l discrete_validI.
+    rewrite -!assoc. apply const_elim_sep_l=>-[? [Hcl Hdisj]]. simpl in Hdisj, Hcl.
+    inversion_clear Hdisj. rewrite const_equiv // left_id.
+    rewrite comm. apply sep_mono; first done.
+    apply equiv_spec, own_proper. split; first split; simpl.
+    - intros Hdisj. split_ands; first by solve_elem_of-.
+      + done.
+      + constructor; [done | solve_elem_of-].
+    - intros _. by eapply closed_disjoint.
+    - intros _. constructor. solve_elem_of-.
+  Qed.
+
+  Lemma closing E γ s T s' S' T' :
+    step sts.(st) sts.(tok) (s, T) (s', T') → s' ∈ S' → closed sts.(st) sts.(tok) S' T' →
+    (▷ φ 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.
+
 End sts.
 
 End sts.