From 373feb826723a4c23a0bbc54bbb932fba9d35f81 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 20 Mar 2018 13:46:43 +0100
Subject: [PATCH] teach framing about the intuitionistic modality

---
 theories/bi/derived_laws.v           |  6 ++++++
 theories/proofmode/class_instances.v | 23 +++++++++++++++++++++++
 theories/proofmode/classes.v         |  9 +++++++++
 3 files changed, 38 insertions(+)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index a730ed46b..b4ccbb622 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -980,6 +980,12 @@ Proof. rewrite /bi_intuitionistically affinely_elim //. Qed.
 Lemma intuitionistically_persistently_persistently P : □ <pers> P ⊣⊢ □ P.
 Proof. rewrite /bi_intuitionistically persistently_idemp //. Qed.
 
+Lemma intuitionistic_intuitionistically P :
+  Affine P → Persistent P → □ P ⊣⊢ P.
+Proof.
+  intros. apply (anti_symm _); first exact: intuitionistically_elim.
+  rewrite -{1}(affine_affinely P) {1}(persistent P) //.
+Qed.
 Lemma intuitionistically_affinely P : □ P ⊢ <affine> P.
 Proof.
   rewrite /bi_intuitionistically /bi_affinely. apply and_intro.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index c735d2460..20f14095d 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -991,6 +991,29 @@ Proof.
   rewrite -{1}(affine_affinely (â–¡ R)%I) affinely_sep_2 //.
 Qed.
 
+Global Instance make_intuitionistically_True :
+  @KnownMakeIntuitionistically PROP True emp | 0.
+Proof.
+  by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
+             intuitionistically_True_emp.
+Qed.
+Global Instance make_intuitionistically_intuitionistic P :
+  Affine P → Persistent P → KnownMakeIntuitionistically P P | 1.
+Proof.
+  intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically.
+  rewrite intuitionistic_intuitionistically //.
+Qed.
+Global Instance make_intuitionistically_default P :
+  MakeIntuitionistically P (â–¡ P) | 100.
+Proof. by rewrite /MakeIntuitionistically. Qed.
+
+Global Instance frame_intuitionistically R P Q Q' :
+  Frame true R P Q → MakeIntuitionistically Q Q' → Frame true R (□ P) Q'.
+Proof.
+  rewrite /Frame /MakeIntuitionistically=> <- <- /=.
+  rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
+Qed.
+
 Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
 Proof.
   by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 944fe397b..f2aa85a35 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -348,6 +348,15 @@ Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
 Arguments KnownMakeAffinely {_} _%I _%I.
 Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
 
+Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
+  make_intuitionistically : □ P ⊣⊢ Q.
+Arguments MakeIntuitionistically {_} _%I _%I.
+Hint Mode MakeIntuitionistically + - - : typeclass_instances.
+Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
+  known_make_intuitionistically :> MakeIntuitionistically P Q.
+Arguments KnownMakeIntuitionistically {_} _%I _%I.
+Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
+
 Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
   make_absorbingly : <absorb> P ⊣⊢ Q.
 Arguments MakeAbsorbingly {_} _%I _%I.
-- 
GitLab