diff --git a/program_logic/invariants.v b/program_logic/invariants.v index 0035924cb739fab3581764be7445758b032c735b..a50eb388eec84475ba70af45b7b43680c8097a13 100644 --- a/program_logic/invariants.v +++ b/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.