From d70b62f645a14389cc7fb65424e6448177276b98 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 5 Jan 2021 09:58:21 +0100 Subject: [PATCH] Use new class `IntoFUpd` in tactic `wp_value_head`. --- iris_heap_lang/proofmode.v | 31 +++++++++++++------------------ 1 file changed, 13 insertions(+), 18 deletions(-) diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v index a640e92d1..e29fe8490 100644 --- a/iris_heap_lang/proofmode.v +++ b/iris_heap_lang/proofmode.v @@ -59,31 +59,26 @@ Lemma tac_twp_value_nofupd `{!heapG Σ} Δ s E Φ v : envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]). Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed. -Lemma tac_wp_value `{!heapG Σ} Δ s E (Φ : val → iPropI Σ) v : - envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}). -Proof. rewrite envs_entails_eq=> ->. by rewrite wp_value_fupd. Qed. -Lemma tac_twp_value `{!heapG Σ} Δ s E (Φ : val → iPropI Σ) v : - envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]). -Proof. rewrite envs_entails_eq=> ->. by rewrite twp_value_fupd. Qed. +Lemma tac_wp_value `{!heapG Σ} Δ s E P (Φ : val → iPropI Σ) v : + IntoFUpd E P (Φ v) → + envs_entails Δ P → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}). +Proof. rewrite /IntoFUpd envs_entails_eq=> -> ->. by rewrite wp_value_fupd. Qed. +Lemma tac_twp_value `{!heapG Σ} Δ s E P (Φ : val → iPropI Σ) v : + IntoFUpd E P (Φ v) → + envs_entails Δ P → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]). +Proof. rewrite /IntoFUpd envs_entails_eq=> -> ->. by rewrite twp_value_fupd. Qed. (** Simplify the goal if it is [WP] of a value. - If the postcondition already allows a fupd, do not add a second one. - But otherwise, *do* add a fupd. This ensures that all the lemmas applied + The [IntoFUpd] class in the above tactics ensures that if the postcondition + already allows a fupd, no second one is added. + But otherwise, an fupd *is* added. This ensures that all the lemmas applied here are bidirectional, so we never will make a goal unprovable. *) Ltac wp_value_head := lazymatch goal with - | |- envs_entails _ (wp ?s ?E (Val _) (λ _, fupd ?E _ _)) => - eapply tac_wp_value_nofupd - | |- envs_entails _ (wp ?s ?E (Val _) (λ _, wp _ ?E _ _)) => - eapply tac_wp_value_nofupd | |- envs_entails _ (wp ?s ?E (Val _) _) => - eapply tac_wp_value - | |- envs_entails _ (twp ?s ?E (Val _) (λ _, fupd ?E _ _)) => - eapply tac_twp_value_nofupd - | |- envs_entails _ (twp ?s ?E (Val _) (λ _, twp _ ?E _ _)) => - eapply tac_twp_value_nofupd + notypeclasses refine (tac_wp_value _ _ _ _ _ _ _ _); [iSolveTC|] | |- envs_entails _ (twp ?s ?E (Val _) _) => - eapply tac_twp_value + notypeclasses refine (tac_twp_value _ _ _ _ _ _ _ _); [iSolveTC|] end. Ltac wp_finish := -- GitLab