From 7f14dcb3d49527adcd8d874ebf8016ab36d6603c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 6 Jun 2021 12:54:20 +0200
Subject: [PATCH] prove laterable_alt

---
 iris/bi/lib/laterable.v | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 477ed933f..968f678fb 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -90,7 +90,7 @@ Section instances.
   (** A wrapper to obtain a weaker, laterable form of any assertion.
      Alternatively: the modality corresponding to [Laterable].
      The â—‡ is required to make [make_laterable_intro'] hold.
-   TODO: Can we define [Laterable] in terms of this? *)
+   TODO: Define [Laterable] in terms of this (see [laterable_alt] below). *)
   Definition make_laterable (Q : PROP) : PROP :=
     ∃ P, ▷ P ∗ □ (▷ P -∗ ◇ Q).
 
@@ -191,6 +191,14 @@ Section instances.
     - iApply make_laterable_intro'.
   Qed.
 
+  Lemma laterable_alt Q :
+    Laterable Q ↔ (Q -∗ make_laterable Q).
+  Proof.
+    split.
+    - intros ?. apply make_laterable_intro'. done.
+    - intros ?. done.
+  Qed.
+
   (** * Proofmode integration *)
   Global Instance into_laterable_laterable P :
     Laterable P →
-- 
GitLab