wp_apply: bad errors when the term is not found or the lemma is used wrong
Consider this test case:
From iris.algebra Require Import excl frac_auth numbers.
From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Import lib.token lib.invariants lib.own.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation adequacy lib.par.
From iris.prelude Require Import options.
Definition newlock : val. Admitted.
Definition acquire : val. Admitted.
Definition release : val. Admitted.
Section test.
Context `{!heapGS_gen hlc Σ}.
Notation iProp := (iProp Σ).
Context (newlock_spec : ∀ R, {{{ R }}} newlock #() {{{ RET #(); True }}}).
Context (acquire_spec : ∀ R, {{{ R }}} acquire #() {{{ RET #(); True }}}).
Lemma test (P : iProp) :
P -∗ WP newlock #() {{ _, True }}.
Proof.
iIntros "HP".
Fail wp_apply acquire_spec.
Fail wp_apply (newlock_spec True%I with "HP").
Both of these wp_apply
fail by just saying "No applicable tactic", which is a pretty bad user experience.
The first should fail saying something about "acquire" not having been found in the goal.
The second should fail the same way iApply (newlock_spec True%I with "HP")
fails in that situation:
iSpecialize: cannot instantiate (True -∗ ▷ (True -∗ ?Goal #()) -∗ WP newlock #() {{ v, ?Goal v }})%I with P.