Rules for opening timeless invariants.

program_logic/invariants.v

@@ -51,6 +51,17 @@ Proof.
   rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id.
   apply pvs_mask_frame'; set_solver.
 Qed.
+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 ⊢ 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.
+Qed.
 
 (* Derive the concrete forms for pvs and wp, because they are useful. *)
 
@@ -60,6 +71,12 @@ Lemma pvs_inv E N P Q R :
   R ⊢ (▷ P -★ |={E ∖ nclose N}=> (▷ P ★ Q)) →
   R ⊢ (|={E}=> Q).
 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 ⊢ (|={E}=> Q).
+Proof. intros. by apply: (inv_fsa_timeless pvs_fsa). Qed.
 
 Lemma wp_inv E e N P Φ R :
   atomic e → nclose N ⊆ E →
@@ -67,6 +84,12 @@ Lemma wp_inv E e N P Φ R :
   R ⊢ (▷ P -★ WP e @ E ∖ nclose N {{ λ v, ▷ P ★ Φ v }}) →
   R ⊢ WP e @ E {{ Φ }}.
 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 ⊢ WP e @ E {{ Φ }}.
+Proof. intros. by apply: (inv_fsa_timeless (wp_fsa e)). Qed.
 
 Lemma inv_alloc N E P : nclose N ⊆ E → ▷ P ⊢ |={E}=> inv N P.
 Proof.