Extend `iApply` to deal with pure goals
If I have a pure Coq lemma A → B
, I would like to be able to use it in the proof-mode to prove an Iris goal ⌜B⌝
(under an Iris context). Currently iApply
does not support this. Here is an example.
Lemma test {Σ} (A B : Prop) (P : iProp Σ) :
(A → B) → (P -∗ ⌜A⌝) → (P -∗ ⌜B⌝).
Proof.
iIntros (ab pa) "p".
(* what I would like to write directly: *)
Fail iApply ab. (* Tactic failure: iPoseProof: not a uPred. *)
(* what I need to write instead: *)
iApply (uPred.pure_mono _ _ ab).
iApply pa.
iExact "p".
Qed.
(tested with coq-iris dev.2018-04-10.0)