strengthen sts_alloc and auth_alloc

heap_lang/heap.v

@@ -67,7 +67,8 @@ Section heap.
     ownP σ ⊑ pvs N N (∃ (_ : heapG Σ), heap_ctx N ∧ Π★{map σ} heap_mapsto).
   Proof.
     rewrite -{1}(from_to_heap σ). etransitivity.
-    { apply (auth_alloc (ownP ∘ of_heap) N (to_heap σ)), to_heap_valid. }
+    { rewrite [ownP _]later_intro.
+      apply (auth_alloc (ownP ∘ of_heap) N (to_heap σ)), to_heap_valid. }
     apply pvs_mono, exist_elim=> γ.
     rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
     induction σ as [|l v σ Hl IH] using map_ind.

program_logic/auth.v

@@ -42,17 +42,17 @@ Section auth.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
 
   Lemma auth_alloc N a :
-    ✓ a → φ a ⊑ pvs N N (∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
+    ✓ a → ▷ φ a ⊑ pvs N N (∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
   Proof.
     intros Ha. eapply sep_elim_True_r.
     { by eapply (own_alloc (Auth (Excl a) a) N). }
     rewrite pvs_frame_l. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     transitivity (▷ auth_inv γ φ ★ auth_own γ a)%I.
-    { rewrite /auth_inv -later_intro -(exist_intro a).
+    { rewrite /auth_inv -(exist_intro a) later_sep.
       rewrite const_equiv // left_id.
-      rewrite [(_ ★ φ _)%I]comm -assoc. apply sep_mono; first done.
-      rewrite /auth_own -own_op auth_both_op. done. }
+      rewrite [(_ ★ ▷ φ _)%I]comm -assoc. apply sep_mono; first done.
+      rewrite -later_intro /auth_own -own_op auth_both_op. done. }
     rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
     by rewrite always_and_sep_l.
   Qed.

program_logic/sts.v

@@ -64,7 +64,7 @@ Section sts.
   Proof. intros. by apply own_update, sts_update_frag_up. Qed.
 
   Lemma sts_alloc N s :
-    φ s ⊑ pvs N N (∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
+    ▷ φ s ⊑ pvs N N (∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
   Proof.
     eapply sep_elim_True_r.
     { apply (own_alloc (sts_auth s (⊤ ∖ sts.tok s)) N).
@@ -72,9 +72,9 @@ Section sts.
     rewrite pvs_frame_l. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     transitivity (▷ sts_inv γ φ ★ sts_own γ s (⊤ ∖ sts.tok s))%I.
-    { rewrite /sts_inv -later_intro -(exist_intro s).
-      rewrite [(_ ★ φ _)%I]comm -assoc. apply sep_mono_r.
-      by rewrite -own_op sts_op_auth_frag_up; last solve_elem_of. }
+    { rewrite /sts_inv -(exist_intro s) later_sep.
+      rewrite [(_ ★ ▷ φ _)%I]comm -assoc. apply sep_mono_r.
+      by rewrite -later_intro -own_op sts_op_auth_frag_up; last solve_elem_of. }
     rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
     by rewrite always_and_sep_l.
   Qed.