From 5f98a0bfce6a8572c4dd210ec7c15fe66f2c0a3a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 18 Jun 2020 15:16:58 +0200
Subject: [PATCH] Add Proper mono instances for make_laterable
---
theories/bi/lib/laterable.v | 17 +++++++++++------
1 file changed, 11 insertions(+), 6 deletions(-)
diff --git a/theories/bi/lib/laterable.v b/theories/bi/lib/laterable.v
index 77ac15310..7983c6fb6 100644
--- a/theories/bi/lib/laterable.v
+++ b/theories/bi/lib/laterable.v
@@ -76,7 +76,18 @@ Section instances.
Global Instance make_laterable_ne : NonExpansive make_laterable.
Proof. solve_proper. Qed.
Global Instance make_laterable_proper : Proper ((≡) ==> (≡)) make_laterable := ne_proper _.
+ Global Instance make_laterable_mono' : Proper ((⊢) ==> (⊢)) make_laterable.
+ Proof. solve_proper. Qed.
+ Global Instance make_laterable_flip_mono' :
+ Proper (flip (⊢) ==> flip (⊢)) make_laterable.
+ Proof. solve_proper. Qed.
+
+ Lemma make_laterable_mono Q1 Q2 :
+ (Q1 ⊢ Q2) → (make_laterable Q1 ⊢ make_laterable Q2).
+ Proof. by intros ->. Qed.
+ (** A stronger version of [make_laterable_mono] that lets us keep persistent
+ resources. *)
Lemma make_laterable_wand Q1 Q2 :
□ (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
Proof.
@@ -84,12 +95,6 @@ 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.
--
GitLab