strengthen STS to be able to take any number of steps at once

algebra/sts.v

@@ -29,6 +29,7 @@ Inductive step : relation (state sts * tokens sts) :=
      (* TODO: This asks for ⊥ on sets: T1 ⊥ T2 := T1 ∩ T2 ⊆ ∅. *)
      prim_step s1 s2 → tok s1 ∩ T1 ≡ ∅ → tok s2 ∩ T2 ≡ ∅ →
      tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2).
+Definition steps := rtc step.
 Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
   | Frame_step T1 T2 :
      T1 ∩ (tok s1 ∪ T) ≡ ∅ → step (s1,T1) (s2,T2) → frame_step T s1 s2.
@@ -105,6 +106,16 @@ Proof.
   - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
   - set_solver -Hstep Hs1 Hs2.
 Qed.
+Lemma steps_closed s1 s2 T1 T2 S Tf :
+  steps (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ∩ Tf ≡ ∅ →
+  tok s1 ∩ T1 ≡ ∅ → s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅.
+Proof.
+  remember (s1,T1) as sT1. remember (s2,T2) as sT2. intros Hsteps.
+  revert s1 T1 HeqsT1 s2 T2 HeqsT2.
+  induction Hsteps as [?|? [s' T'] ? Hstep Hsteps IH]; intros; subst.
+  - case: HeqsT2=>? ?. subst. done.
+  - eapply step_closed in Hstep; [|done..]. destruct_conjs. eauto.
+Qed.
 
 (** ** Properties of the closure operators *)
 Lemma elem_of_up s T : s ∈ up s T.
@@ -326,11 +337,22 @@ Lemma sts_op_auth_frag s S T :
 Proof.
   intros; split; [split|constructor; set_solver]; simpl.
   - intros (?&?&?); by apply closed_disjoint' with S.
-  - intros; split_and?. set_solver+. done. constructor; set_solver.
+  - intros; split_and?.
+    + set_solver+.
+    + done.
+    + constructor; set_solver.
 Qed.
 Lemma sts_op_auth_frag_up s T :
-  tok s ∩ T ≡ ∅ → sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
-Proof. intros; apply sts_op_auth_frag; auto using elem_of_up, closed_up. Qed.
+  sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
+Proof.
+  intros; split; [split|constructor; set_solver]; simpl.
+  - intros (?&?&?). apply closed_disjoint' with (up s T); first done.
+    apply elem_of_up.
+  - intros; split_and?.
+    + set_solver+.
+    + by apply closed_up.
+    + constructor; last set_solver. apply elem_of_up.
+Qed.
 
 Lemma sts_op_frag S1 S2 T1 T2 :
   T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
@@ -344,10 +366,10 @@ Qed.
 
 (** Frame preserving updates *)
 Lemma sts_update_auth s1 s2 T1 T2 :
-  step (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
+  steps (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
 Proof.
   intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
-  destruct (step_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto.
+  destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
   repeat (done || constructor).
 Qed.
 

algebra/upred.v

@@ -983,9 +983,9 @@ Lemma always_entails_r P Q `{!AlwaysStable Q} : (P ⊑ Q) → P ⊑ (P ★ Q).
 Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
 
 (* Derived lemmas that need a combination of the above *)
-Lemma löb_strong_sep P Q : (▷(P -★ Q) ★ P) ⊑ Q → P ⊑ Q.
+Lemma löb_strong_sep P Q : (P ★ ▷(P -★ Q)) ⊑ Q → P ⊑ Q.
 Proof.
-  move/wand_intro_r=>Hlöb. rewrite -[P](left_id True (∧))%I.
+  move/wand_intro_l=>Hlöb. rewrite -[P](left_id True (∧))%I.
   apply impl_elim_l'. apply: always_entails. apply löb_strong.
   rewrite left_id -always_wand_impl -always_later Hlöb. done.
 Qed.

program_logic/sts.v

@@ -103,7 +103,7 @@ Section sts.
   Qed.
 
   Lemma sts_closing E γ s T s' T' :
-    sts.step (s, T) (s', T') →
+    sts.steps (s, T) (s', T') →
     (▷ φ s' ★ own γ (sts_auth s T)) ⊑ (|={E}=> ▷ sts_inv γ φ ★ sts_own γ s' T').
   Proof.
     intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s').
@@ -112,7 +112,7 @@ Section sts.
     rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
     transitivity (|={E}=> own γ (sts_auth s' T'))%I.
     { by apply own_update, sts_update_auth. }
-    by rewrite -own_op sts_op_auth_frag_up; last by inversion_clear Hstep.
+    by rewrite -own_op sts_op_auth_frag_up.
   Qed.
 
   Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
@@ -123,7 +123,7 @@ Section sts.
     P ⊑ (sts_ownS γ S T ★ ∀ s,
           ■ (s ∈ S) ★ ▷ φ s -★
           fsa (E ∖ nclose N) (λ x, ∃ s' T',
-            ■ sts.step (s, T) (s', T') ★ ▷ φ s' ★
+            ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★
             (sts_own γ s' T' -★ Ψ x))) →
     P ⊑ fsa E Ψ.
   Proof.
@@ -152,7 +152,7 @@ Section sts.
     P ⊑ (sts_own γ s0 T ★ ∀ s,
           ■ (s ∈ sts.up s0 T) ★ ▷ φ s -★
           fsa (E ∖ nclose N) (λ x, ∃ s' T',
-            ■ (sts.step (s, T) (s', T')) ★ ▷ φ s' ★
+            ■ (sts.steps (s, T) (s', T')) ★ ▷ φ s' ★
             (sts_own γ s' T' -★ Ψ x))) →
     P ⊑ fsa E Ψ.
   Proof. apply sts_fsaS. Qed.