Use new class `IntoFUpd` in tactic `wp_value_head`.

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 :=