From b6d1946d4cf3b02bc2390b2396ed690c95257ef6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 18 Jun 2020 13:39:48 +0200
Subject: [PATCH] Add make_laterable_mono

---
 theories/bi/lib/laterable.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/bi/lib/laterable.v b/theories/bi/lib/laterable.v
index b1245dd5f..77ac15310 100644
--- a/theories/bi/lib/laterable.v
+++ b/theories/bi/lib/laterable.v
@@ -84,6 +84,12 @@ Section instances.
     iExists P. iFrame. iIntros "!> HP". iApply "HQ". iApply "HQ1". done.
   Qed.
 
+  Lemma make_laterable_mono Q1 Q2 :
+    (Q1 ⊢ Q2) → (make_laterable Q1 ⊢ make_laterable Q2).
+  Proof.
+    intros HQ12. iApply make_laterable_wand. rewrite HQ12. by iIntros "!# ?".
+  Qed.
+
   Global Instance make_laterable_laterable Q :
     Laterable (make_laterable Q).
   Proof.
@@ -97,6 +103,8 @@ Section instances.
     iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]". by iApply "HQ".
   Qed.
 
+  (** Written internally (as an entailment of wands) to reflect
+      that persistent assertions can be kept unchanged. *)
   Lemma make_laterable_intro P Q :
     Laterable P →
     □ (◇ P -∗ Q) -∗ P -∗ make_laterable Q.
-- 
GitLab