From 5c535b85b0d661ad9edcf5fb943226b51e8403df Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 13 Jun 2021 11:55:05 +0200
Subject: [PATCH] add lemmas 'intuitionistic' and 'intuitionistically_intro'

---
 iris/bi/derived_laws.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index fc8d8955d..7d0b04d51 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1431,9 +1431,19 @@ Proof. by rewrite -(persistent_persistently P) persistently_and_sep_assoc. Qed.
 Lemma impl_wand_2 P `{!Persistent P} Q : (P -∗ Q) ⊢ P → Q.
 Proof. apply impl_intro_l. by rewrite persistent_and_sep_1 wand_elim_r. Qed.
 
+(** We don't have a [Intuitionistic] typeclass, but if we did, this
+would be its only field. *)
+Lemma intuitionistic P `{!Persistent P, !Affine P} : P ⊢ □ P.
+Proof. rewrite intuitionistic_intuitionistically. done. Qed.
+
 Section persistent_bi_absorbing.
   Context `{BiAffine PROP}.
 
+  Lemma intuitionistically_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
+  Proof.
+    intros HP. rewrite (persistent P) HP intuitionistically_into_persistently //.
+  Qed.
+
   Lemma persistent_and_sep P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
     P ∧ Q ⊣⊢ P ∗ Q.
   Proof.
-- 
GitLab