Remove more laters in rules for opening timeless invariants.

examples/one_shot.v

@@ -68,13 +68,13 @@ Proof.
       rewrite (own_update); (* FIXME: canonical structures are not working *)
         last by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)).
       rewrite pvs_frame_l; apply pvs_mono, sep_intro_True_r; eauto with I.
-      rewrite -later_intro /one_shot_inv -or_intro_r -(exist_intro n).
+      rewrite /one_shot_inv -or_intro_r -(exist_intro n).
       solve_sep_entails.
     + rewrite sep_exist_l; apply exist_elim=>m.
       eapply wp_cas_fail with (v':=InjRV #m) (q:=1%Qp);
         rewrite /= ?to_of_val; eauto with I ndisj; strip_later.
       ecancel [l ↦ _]%I; apply wand_intro_l, sep_intro_True_r; eauto with I.
-      rewrite -later_intro /one_shot_inv -or_intro_r -(exist_intro m).
+      rewrite /one_shot_inv -or_intro_r -(exist_intro m).
       solve_sep_entails.
   - apply: always_intro. wp_seq.
     wp_focus (Load (%l))%I.
@@ -92,7 +92,7 @@ Proof.
     rewrite !sep_exist_l; apply exist_elim=> w.
     eapply wp_load with (q:=1%Qp) (v:=w); eauto with I ndisj.
     rewrite -later_intro; cancel [l ↦ w]%I.
-    rewrite -later_intro; apply wand_intro_l; rewrite -later_intro.
+    rewrite -later_intro; apply wand_intro_l.
     trans (heap_ctx heapN ★ inv N (one_shot_inv γ l) ★ one_shot_inv γ l ★
       (w = InjLV #0 ∨ (∃ n : Z, w = InjRV #n ★ own γ (Shot (DecAgree n)))))%I.
     { cancel [heap_ctx heapN]. rewrite !sep_or_l; apply or_elim.
@@ -130,7 +130,7 @@ Proof.
       rewrite (True_intro (heap_ctx heapN)) left_id.
       rewrite -own_op own_valid_l one_shot_validI Shot_op /= discrete_valid.
       rewrite -assoc. apply const_elim_sep_l=> /dec_agree_op_inv [->].
-      rewrite dec_agree_idemp -later_intro. apply sep_intro_True_r.
+      rewrite dec_agree_idemp. apply sep_intro_True_r.
       { rewrite /one_shot_inv -or_intro_r -(exist_intro m). solve_sep_entails. }
       wp_case; fold of_val. wp_let. rewrite -wp_assert'.
       wp_op; by eauto using later_intro with I.

program_logic/invariants.v

@@ -55,12 +55,13 @@ Lemma inv_fsa_timeless {A} (fsa : FSA Λ Σ A)
     `{!FrameShiftAssertion fsaV fsa} E N P `{!TimelessP P} Ψ R :
   fsaV → nclose N ⊆ E →
   R ⊢ inv N P →
-  R ⊢ (P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Ψ a)) →
+  R ⊢ (P -★ fsa (E ∖ nclose N) (λ a, P ★ Ψ a)) →
   R ⊢ fsa E Ψ.
 Proof.
   intros ??? HR. eapply inv_fsa, wand_intro_l; eauto.
   trans (|={E ∖ N}=> P ★ R)%I; first by rewrite pvs_timeless pvs_frame_r.
-  apply (fsa_strip_pvs _). by rewrite HR wand_elim_r.
+  apply (fsa_strip_pvs _). rewrite HR wand_elim_r.
+  apply: fsa_mono=> v. by rewrite -later_intro.
 Qed.
 
 (* Derive the concrete forms for pvs and wp, because they are useful. *)
@@ -74,7 +75,7 @@ Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
 Lemma pvs_inv_timeless E N P `{!TimelessP P} Q R :
   nclose N ⊆ E →
   R ⊢ inv N P →
-  R ⊢ (P -★ |={E ∖ nclose N}=> (▷ P ★ Q)) →
+  R ⊢ (P -★ |={E ∖ nclose N}=> (P ★ Q)) →
   R ⊢ (|={E}=> Q).
 Proof. intros. by apply: (inv_fsa_timeless pvs_fsa). Qed.
 
@@ -87,7 +88,7 @@ Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
 Lemma wp_inv_timeless E e N P `{!TimelessP P} Φ R :
   atomic e → nclose N ⊆ E →
   R ⊢ inv N P →
-  R ⊢ (P -★ WP e @ E ∖ nclose N {{ λ v, ▷ P ★ Φ v }}) →
+  R ⊢ (P -★ WP e @ E ∖ nclose N {{ λ v, P ★ Φ v }}) →
   R ⊢ WP e @ E {{ Φ }}.
 Proof. intros. by apply: (inv_fsa_timeless (wp_fsa e)). Qed.