iApply strips some modalities, but not monotonically
Here's a minimized inconsistent behavior and a possible fix via an instance. I suspect that instance is missing by design, but I can't tell what the design is, even tho I can read Hint Mode — see #139.
(I also realize that such instances must appear for either all or none of the monotonic modalities).
From iris.proofmode Require Import tactics.
From iris.bi Require Import bi.
Import bi.
Section sbi_instances.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
(* Here [iApply] works. *)
Lemma foo0 P : □ P -∗ P.
Proof. iIntros "H". iApply "H". Qed.
(* But here it fails! *)
Lemma foo1 P : ▷ □ P -∗ ▷ P.
Proof. iIntros "H". Fail iApply "H". iNext. iApply "H". Qed.
(* Here's a possible fix, but I'm unsure whether it respects the interplay of
FromAssumption, KnownLFromAssumption and KnownRFromAssumption,
as it is not fully documented.
Should I add this for both KnownLFromAssumption and KnownRFromAssumption? *)
Global Instance from_assumption_later_later p P Q :
FromAssumption p P Q → FromAssumption p (▷ P) (▷ Q)%I.
Proof.
rewrite /KnownRFromAssumption /FromAssumption
later_intuitionistically_if_2 => ->. exact: later_mono.
Qed.
Lemma foo P : ▷ □ P -∗ ▷ P.
Proof. iIntros "H". iApply "H". Qed.
End sbi_instances.