GitLab

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.