Updates that takes a step: ElimModal instance, and a more easy to use lemma [wp_fupd_step].

base_logic/lib/fancy_updates.v

@@ -222,4 +222,11 @@ Proof.
   iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
 Qed.
 
+Global Instance elim_modal_step_fupd E1 E2 E3 E4 P Q :
+  ElimModal (|={E1,E2}=>▷|={E2,E3}=> P) P
+            (|={E1,E2}=>▷|={E2,E4}=> Q) (|={E3,E4}=> Q).
+Proof.
+  iIntros "[A B]". iMod "A". iModIntro. iNext. iMod "A". by iApply "B".
+Qed.
+
 End step_fupd.

program_logic/weakestpre.v

@@ -206,17 +206,18 @@ Proof.
   iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
 Qed.
 
-Lemma wp_frame_step_l E1 E2 e Φ R :
+Lemma wp_fupd_step E1 E2 e P Φ :
   to_val e = None → E2 ⊆ E1 →
-  (|={E1,E2}▷=> R) ∗ WP e @ E2 {{ Φ }} ⊢ WP e @ E1 {{ v, R ∗ Φ v }}.
+  (|={E1,E2}▷=> P) -∗ WP e @ E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ E1 {{ Φ }}.
 Proof.
-  rewrite !wp_unfold /wp_pre. iIntros (??) "[HR [Hv|[_ H]]]".
+  rewrite !wp_unfold /wp_pre. iIntros (??) "HR [Hv|[_ H]]".
   { iDestruct "Hv" as (v) "[% Hv]"; simplify_eq. }
   iRight; iSplit; [done|]. iIntros (σ1) "Hσ".
   iMod "HR". iMod ("H" $! _ with "Hσ") as "[$ H]".
   iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! e2 σ2 efs with "[%]") as "($ & H & $)"; auto.
-  iMod "HR". iModIntro. iApply (wp_strong_mono E2 _ _ Φ); try iFrame; eauto.
+  iMod "HR". iModIntro. iApply (wp_strong_mono E2); first done.
+  iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
 Qed.
 
 Lemma wp_bind K `{!LanguageCtx Λ K} E e Φ :
@@ -261,6 +262,13 @@ Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.
 Lemma wp_frame_r E e Φ R : WP e @ E {{ Φ }} ∗ R ⊢ WP e @ E {{ v, Φ v ∗ R }}.
 Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.
 
+Lemma wp_frame_step_l E1 E2 e Φ R :
+  to_val e = None → E2 ⊆ E1 →
+  (|={E1,E2}▷=> R) ∗ WP e @ E2 {{ Φ }} ⊢ WP e @ E1 {{ v, R ∗ Φ v }}.
+Proof.
+  iIntros (??) "[Hu Hwp]". iApply (wp_fupd_step with "Hu"); try done.
+  iApply (wp_mono with "Hwp"). by iIntros (?) "$$".
+Qed.
 Lemma wp_frame_step_r E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
   WP e @ E2 {{ Φ }} ∗ (|={E1,E2}▷=> R) ⊢ WP e @ E1 {{ v, Φ v ∗ R }}.
@@ -316,6 +324,7 @@ Section proofmode_classes.
     ElimModal (|={E1,E2}=> P) P
             (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
+
 End proofmode_classes.
 
 Hint Extern 0 (atomic _) => assumption : typeclass_instances.

[Robbert]

Notice that this instance overlaps with elim_modal_fupd_fupd. Both seem to have the same (default) precedence, so which is picked, is kind of arbitrary.

[Jacques-Henri Jourdan]

Oh, indeed. Well, of course we want Coq to take this one if possible.

[Robbert]

But this one is strictly weaker: when inlining this proof, it will strip a later of any hypothesis. Using this instance, that won't happen.

[Jacques-Henri Jourdan]

Right. But then, what can we do? Would the right thing to do be implementing this logic in iNext?

[Ralf Jung]

Once you settled on sth., could you please add comments to the explicit priority assignments explaining the choice?

[Robbert]

I am not sure, the problem about this instance that once declared, there is no way back. The iMod tactic will always pick it, and there is no way of telling it to use the more basic one.

[Robbert]

One thing you can do is hide the updates that take a step behind a definition. Then when not unfolded, it will pick the elim_modal_step_fupd instance, and when unfolded it will pick the elim_modal_fupd_fupd instance.

Problem, however, is that by putting them in a definition you also need to declare Proper instances, and basically develop a whole theory for updates that take a step.

[Jacques-Henri Jourdan]

Yeah, I understand that. I already reverted my commit.

My point is that it is really annoying to do iMod; iNext; iMod to eliminate such a modality. And really, what's happening here is more or less just taking a step. So I wonder whether it would be possible to implement that in iNext.

[Robbert]

I see that having to do that is annoying.

At this moment, iNext is tied to removing (possible many) laters: it cannot do much else.

[Robbert]

Somewhat related, A thing that I notice having to do often is iMod foo; iModIntro. So maybe having a variant of iMod that executes the update and directly removes it from the goal would be of help?

[Jacques-Henri Jourdan]

Probably that would make some proofs simpler, yes. But I don't see how this is related to upds that take a step.

[Robbert]

That saves you one iModIntro in your proof.

[Robbert]

But how would you propose changing iNext to handle this?

[Ralf Jung]

Somewhat related, A thing that I notice having to do often is iMod foo; iModIntro. So maybe having a variant of iMod that executes the update and directly removes it from the goal would be of help?

If we had ssreflect-style introduction, that would work beautifully: iDestruct ("H" with "foo") => "[pattern] !>".

[Jacques-Henri Jourdan]

Oh nice. So what about iDestruct ("H" with "foo") as "[pattern] !>" ?

[Ralf Jung]

Ouch... mixing Coq syntax and ssreflect semantics?^^

[Jacques-Henri Jourdan]

But how would you propose changing iNext to handle this?

Instead of IntoLaterN, I would introduce a typeclass IntoLaterModal, with four parameters (and the same specification as ElimModal). The two first parameters would describe the goal before and after the application of the tactic, and the next two would describe the evolution of an hypothesis.

[Robbert]

Ouch... mixing Coq syntax and ssreflect semantics?^

That seems like a bad idea, so let's not do that.

[Robbert]

Instead of IntoLaterN, I would introduce a typeclass IntoLaterModal, with four parameters (and the same specification as ElimModal). The two first parameters would describe the goal before and after the application of the tactic, and the next two would describe the evolution of an hypothesis.

So, you are suggesting to generalize iNext so that it can introduce all kinds of modalities by stripping them from the hypotheses?

I am not sure how that would be supposed to work when dealing with fancy updates with masks. Consider having hypotheses H1 : |={E1,E2} P and H2 : |={E1,E2} P while having to prove H1 : |={E1,E4} P. Now, when saying iNext, the behavior becomes pretty non-deterministic, it can remove the update modality from either H1 or H2, but not both. So, which should it pick?

[Robbert]

Alright, we could in principle unify iNext and iModIntro by allowing them to introduce any modality and stripping all occurrences of all hypotheses. If you want to have a sane semantics, I think we can only do that for non-mask changing updates.

[Jacques-Henri Jourdan]

Yeah, indeed. Let's forget this for the moment.