`iApply` does not use `FromAssumption` for goal matching
From iris.proofmode Require Import tactics.
Typeclasses eauto := debug.
Lemma foo {PROP : bi} (P Q : PROP) :
(P -∗ □ Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
Lemma bar {PROP : bi} (P : PROP) (Q : nat → PROP) :
(P -∗ ∀ n, Q n) -∗ Q 10.
Proof.
iIntros "H".
Fail iApply "H".
iApply ("H" with "[]").
Admitted.
When using iApply
in combination with the with
clause, it will first iSpecialize
and then use iApply
, which in these examples turns to the degenerate case of iExact
. The iExact
tactic uses FromAssumption
to deal with minor mismatches between the hypothesis and the goal. For example, it will eliminate ∀s and modalities (like □).
When using iApply
without the with
clause, it will launch a search using IntoWand
where the goal with unified with the conclusion of the lemma. If there's a mismatch (like the ones above), it will fail.
The problem is the instance:
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
Here, Q
should match exactly. I tried strengtening it to:
Global Instance into_wand_wand p q P Q P' Q' :
FromAssumption q P P' →
FromAssumption (p && q) Q' Q →
IntoWand p q (P' -∗ Q') P Q.
However, that causes other problems: in some cases the above instance will be triggered instead of instances like into_wand_bupd_args
causing the following to go wrong:
Lemma fooz `{!BiBUpd PROP} (P Q : PROP) :
(P -∗ Q) -∗ |==> Q.
Proof.
iIntros "H".
iApply "H". (* should be [|==> P], but will be [P] with the new [into_wand_wand] *)
This issue came up in practice Simuliris.