teach framing about the intuitionistic modality

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.

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

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.