register make_laterable as modality

iris/bi/lib/atomic.v

@@ -75,7 +75,7 @@ Section definition.
   Proof.
     constructor.
     - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
-      iApply (make_laterable_wand with "[] AU").
+      iApply (make_laterable_intuitionistic_wand with "[] AU").
       iIntros "!> AA". iApply (atomic_acc_wand with "[HP12] AA").
       iSplit; last by eauto. iApply "HP12".
     - intros ??. solve_proper.
@@ -256,7 +256,7 @@ Section lemmas.
     iIntros (Heo) "HAU".
     iApply (greatest_fixpoint_coind _ (λ _, atomic_update_def Eo1 Ei α β Φ)); last done.
     iIntros "!> *". rewrite {1}/atomic_update_def /= greatest_fixpoint_unfold.
-    iApply make_laterable_wand. iIntros "!>".
+    iApply make_laterable_intuitionistic_wand. iIntros "!>".
     iApply atomic_acc_mask_weaken. done.
   Qed.
 
@@ -267,7 +267,7 @@ Section lemmas.
   Proof using Type*.
     rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros "HUpd".
     iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd".
-    iApply make_laterable_elim. done.
+    iDestruct (make_laterable_elim with "HUpd") as ">?". done.
   Qed.
 
   (* This lets you eliminate atomic updates with iMod. *)
@@ -301,7 +301,7 @@ Section lemmas.
     rewrite atomic_update_eq {1}/atomic_update_def /=.
     iIntros (??? HAU) "[#HP HQ]".
     iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!>" ([]) "HQ".
-    iApply (make_laterable_intro Q with "[] HQ"). iIntros "!> >HQ".
+    iApply (make_laterable_intro Q with "[] HQ"). iIntros "!> HQ".
     iApply HAU. by iFrame.
   Qed.
 

iris/bi/lib/laterable.v

@@ -75,10 +75,11 @@ Section instances.
     Laterable ([∗] Ps).
   Proof. induction 2; simpl; apply _. Qed.
 
-  (* A wrapper to obtain a weaker, laterable form of any assertion.
-     Alternatively: the modality corresponding to [Laterable]. *)
+  (** A wrapper to obtain a weaker, laterable form of any assertion.
+     Alternatively: the modality corresponding to [Laterable].
+   TODO: Can we define [Laterable] in terms of this? *)
   Definition make_laterable (Q : PROP) : PROP :=
-    (∃ P, ▷ P ∗ □ (▷ P -∗ Q))%I.
+    (∃ P, ▷ P ∗ □ (▷ P -∗ ◇ Q))%I.
 
   Global Instance make_laterable_ne : NonExpansive make_laterable.
   Proof. solve_proper. Qed.
@@ -93,6 +94,18 @@ Section instances.
     (Q1 ⊢ Q2) → (make_laterable Q1 ⊢ make_laterable Q2).
   Proof. by intros ->. Qed.
 
+  Lemma make_laterable_sep Q1 Q2 :
+    make_laterable Q1 ∗ make_laterable Q2 -∗ make_laterable (Q1 ∗ Q2).
+  Proof.
+    iIntros "[HQ1 HQ2]".
+    iDestruct "HQ1" as (P1) "[HP1 #HQ1]".
+    iDestruct "HQ2" as (P2) "[HP2 #HQ2]".
+    iExists (P1 ∗ P2)%I. iFrame. iIntros "!# [HP1 HP2]".
+    iDestruct ("HQ1" with "HP1") as ">$".
+    iDestruct ("HQ2" with "HP2") as ">$".
+    done.
+  Qed.
+
   (** A stronger version of [make_laterable_mono] that lets us keep laterable
   resources. We cannot keep arbitrary resources since that would let us "frame
   in" non-laterable things. *)
@@ -100,10 +113,20 @@ Section instances.
     make_laterable (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
   Proof.
     iIntros "HQ HQ1".
-    iDestruct "HQ" as (Q1') "[HQ1' #HQ]".
-    iDestruct "HQ1" as (P) "[HP #HQ1]".
-    iExists (Q1' ∗ P)%I. iFrame. iIntros "!> [HQ1' HP]".
-    iApply ("HQ" with "HQ1'"). iApply "HQ1". done.
+    iDestruct (make_laterable_sep with "[$HQ $HQ1 //]") as "HQ".
+    iApply make_laterable_mono; last done.
+    by rewrite bi.wand_elim_l.
+  Qed.
+
+  (** A variant of the above for keeping arbitrary intuitionistic resources.
+      Sadly, this is not implied by the above for non-affine BIs. *)
+  Lemma make_laterable_intuitionistic_wand Q1 Q2 :
+    □ (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
+  Proof.
+    iIntros "#HQ HQ1". iDestruct "HQ1" as (P) "[HP #HQ1]".
+    iExists P. iFrame. iIntros "!> HP".
+    iDestruct ("HQ1" with "HP") as "{HQ1} >HQ1".
+    iModIntro. iApply "HQ". done.
   Qed.
 
   Global Instance make_laterable_laterable Q :
@@ -114,7 +137,7 @@ Section instances.
   Qed.
 
   Lemma make_laterable_elim Q :
-    make_laterable Q -∗ Q.
+    make_laterable Q -∗ ◇ Q.
   Proof.
     iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]". by iApply "HQ".
   Qed.
@@ -123,12 +146,35 @@ Section instances.
       that persistent assertions can be kept unchanged. *)
   Lemma make_laterable_intro P Q :
     Laterable P →
-    □ (◇ P -∗ Q) -∗ P -∗ make_laterable Q.
+    □ (P -∗ Q) -∗ P -∗ make_laterable Q.
   Proof.
     iIntros (?) "#HQ HP".
     iDestruct (laterable with "HP") as (P') "[HP' #HPi]". iExists P'.
-    iFrame. iIntros "!> HP'". iApply "HQ". iApply "HPi". done.
+    iFrame. iIntros "!> HP'".
+    iDestruct ("HPi" with "HP'") as ">HP". iModIntro.
+    iApply "HQ". done.
   Qed.
+  Lemma make_laterable_intro' Q :
+    Laterable Q →
+    Q -∗ make_laterable Q.
+  Proof.
+    intros ?. iApply make_laterable_intro. iIntros "!# $".
+  Qed.
+
+  (** We need PROP to be affine as otherwise [emp] is not [Laterable]. *)
+  Lemma modality_make_laterable_mixin `{!BiAffine PROP} :
+    modality_mixin make_laterable MIEnvId (MIEnvForall Laterable).
+  Proof.
+    split; simpl; eauto using make_laterable_intro', make_laterable_mono,
+      make_laterable_sep with typeclass_instances.
+  Qed.
+
+  Definition modality_make_laterable `{!BiAffine PROP} :=
+    Modality _ modality_make_laterable_mixin.
+
+  Global Instance from_modal_make_laterable `{!BiAffine PROP} P :
+    FromModal modality_make_laterable (make_laterable P) (make_laterable P) P.
+  Proof. by rewrite /FromModal. Qed.
 
 End instances.