Stripping laterN from pure propositions when proving laterN *without except-0*

I just proved that, for uniform predicates, when proving ▷^i Q, you can strip ▷^i from "Hfoo": ▷^i ⌜ P ⌝, for arbitrary uniform predicates. Statements:

(⌜ P ⌝ → ▷^i Q) ⊢ ▷^i ⌜ P ⌝ → ▷^i Q.

(⌜ P ⌝ → ▷ Q) ⊢ (▷ ⌜ P ⌝ → ▷ Q).

I needed this in my proof; could we add support for this in Iris? I'm not sending a MR because the code is far from ready for that.

Was this already possible? I didn't find how, and thought this would need some new variant of except-0 (an except-i modality).

• IPM suggested that wouldn't work — iDestruct "Hfoo" as "%" complains that Hfoo is not pure, even when the conclusion starts with ▷^i.

• The proof is by case distinction on the world: in worlds n < i, the conclusion is trivial, while in worlds n >= i, we have that ▷^i ⌜ P ⌝ → P. This must be done in the model.

My proof is easy for later, but laterN was trickier; I'm also not sure where this proof would go (since laterN is a derived connective, but the proof for laterN goes in the model).

I expect one could lift this lemma to wand as well (since ▷^i ⌜ P ⌝ is persistent, this shouldn't need going to the model).

• These lemmas are also a bit inconvenient to use; it's not clear that IntoPure supports such conditional tactics. A typical example, for hypothesis "Hlclw": ▷^i ⌜ nclosed_vl w 0 ⌝, is:

    iApply (strip_pure_laterN i with "[] Hlclw").
    iIntros (Hclw).

iRevert "Hlclw"; iApply strip_pure_wand_laterN; iIntros (Hclw) might also work, given a version for wand.

My proof script is:

From iris.base_logic Require Import base_logic lib.iprop.

Import uPred.

Section uPred_later_extra.
  Context `{M: ucmraT}.
  Implicit Types (Q: uPred M) (x: M).

  Lemma laterN_pure_id i n P x: i <= n →
    (▷^i uPred_pure_def P)%I n x → P.
  Proof.
    move => Hle H; induction i => //=.
    apply IHi; first lia.
    elim: i n Hle H {IHi} => [|i IHi] [|n] Hle;
      unseal => // H; first lia.
    apply IHi; first lia. by unseal.
  Qed.

  Lemma laterN_trivial i n Q x: i > n →
    (▷^i Q)%I n x.
  Proof.
    move: i => [|i] Hle. by lia.
    apply uPred_mono with i x; eauto with lia.
    elim: i {Hle}; by unseal.
  Qed.

  Lemma strip_pure_later P Q:
    (⌜ P ⌝ → ▷ Q) ⊢ (▷ ⌜ P ⌝ → ▷ Q).
  Proof.
    unseal; constructor => n x Hvx Hyp [|n'] // ?????.
    by apply Hyp.
  Qed.

  Lemma strip_pure_laterN i P Q:
    (⌜ P ⌝ → ▷^i Q) ⊢ ▷^i ⌜ P ⌝ → ▷^i Q.
  Proof.
    unseal; constructor => n x Hvx Hyp n' //= x' ?? Hvx' H.
    destruct (decide (i <= n')) as [Hle|Hge].
    - by eapply Hyp, laterN_pure_id.
    - by apply laterN_trivial; lia.
  Qed.
End uPred_later_extra.