Stripping laterN from pure propositions when proving laterN *without except0*
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 except0 (an excepti modality).

IPM suggested that wouldn't work —
iDestruct "Hfoo" as "%"
complains thatHfoo
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 worldsn >= 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 [HleHge].
 by eapply Hyp, laterN_pure_id.
 by apply laterN_trivial; lia.
Qed.
End uPred_later_extra.