sts: define state in terms of states; prove states_fsa

program_logic/auth.v

@@ -108,7 +108,7 @@ Section auth.
     P ⊑ fsa E Q.
   Proof.
     rewrite /auth_ctx=>? HN Hinv Hinner.
-    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P}.
+    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
     apply wand_intro_l. rewrite assoc.
     rewrite (auth_opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
     apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
@@ -116,7 +116,7 @@ Section auth.
     (* Getting this wand eliminated is really annoying. *)
     rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
     rewrite wand_elim_r fsa_frame_l.
-    apply (fsa_mono_pvs fsa)=> b.
+    apply (fsa_mono_pvs fsa)=> v.
     rewrite sep_exist_l; apply exist_elim=> L.
     rewrite sep_exist_l; apply exist_elim=> Lv.
     rewrite sep_exist_l; apply exist_elim=> ?.

program_logic/sts.v

@@ -28,10 +28,9 @@ Section definitions.
   Definition inv  (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
     (∃ 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.
+    own i γ (sts_frag sts.(st) sts.(tok) S T)%I.
   Definition state (s : A) (T: set B) : iPropG Λ Σ :=
-    own i γ (sts_frag sts.(st) sts.(tok) (sts.up sts.(st) sts.(tok) s T) T).
+    states (up sts.(st) sts.(tok) s T) T.
   Definition ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
     invariants.inv N (inv φ).
 End definitions.
@@ -69,15 +68,15 @@ Section sts.
   Qed.
 
   Lemma opened E γ S T :
-    (▷ inv StsI sts γ φ ★ own StsI γ (sts_frag sts.(st) sts.(tok) S T))
+    (▷ inv StsI sts γ φ ★ states StsI sts γ 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 /inv /states. 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.
+    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.
@@ -91,9 +90,9 @@ Section sts.
   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')).
+    ⊑ pvs E E (▷ inv StsI sts γ φ ★ states StsI sts γ S' T').
   Proof.
-    intros Hstep Hin Hcl. rewrite /inv -(exist_intro s').
+    intros Hstep Hin Hcl. rewrite /inv /states -(exist_intro s').
     rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
     rewrite -pvs_frame_l. apply sep_mono; first done.
     rewrite -later_intro.
@@ -108,6 +107,37 @@ Section sts.
     - intros _. constructor. solve_elem_of-.
   Qed.
 
+  Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
+
+  Lemma states_fsa E N P (Q : V → iPropG Λ Σ) γ S T S' T' :
+    fsaV → closed sts.(st) sts.(tok) S' T' →
+    nclose N ⊆ E →
+    P ⊑ ctx StsI sts γ N φ →
+    P ⊑ (states StsI sts γ S T ★ ∀ s,
+          ■ (s ∈ S) ★ ▷ φ s -★
+          fsa (E ∖ nclose N) (λ x, ∃ s',
+            ■ (step sts.(st) sts.(tok) (s, T) (s', T') ∧ s' ∈ S') ★ ▷ φ s' ★
+            (states StsI sts γ S' T' -★ Q x))) →
+    P ⊑ fsa E Q.
+  Proof.
+    rewrite /ctx=>? Hcl HN Hinv Hinner.
+    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
+    apply wand_intro_l. rewrite assoc.
+    rewrite (opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
+    apply (fsa_strip_pvs fsa). apply exist_elim=>s.
+    rewrite (forall_elim s). rewrite [(▷_ ★ _)%I]comm.
+    (* Getting this wand eliminated is really annoying. *)
+    rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
+    rewrite wand_elim_r fsa_frame_l.
+    apply (fsa_mono_pvs fsa)=> v.
+    rewrite sep_exist_l; apply exist_elim=> s'.
+    rewrite comm -!assoc. apply const_elim_sep_l=>-[Hstep Hin].
+    rewrite assoc [(_ ★ (_ -★ _))%I]comm -assoc.
+    rewrite (closing (E ∖ N)) //; [].
+    rewrite pvs_frame_l. apply pvs_mono.
+    by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l.
+  Qed.
+
 End sts.
 
 End sts.