Better `Make*` instances that clean up redundant modalities in the spine of a frame.

tests/proofmode.v

@@ -325,6 +325,45 @@ Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
 Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} :
   P -∗ Q -∗ <affine> (P ∗ Q).
 Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_affinely_3 P Q :
+  □ P -∗ <affine> Q -∗ <affine> (<pers> P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_affinely_4 P Q `{!BiPositive PROP, !Affine P} :
+  <affine> P -∗ <affine> Q -∗ <affine> (<absorb> P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+
+Lemma test_iFrame_intuitionistically_1 P Q `{!Persistent P} :
+  <affine> P -∗ □ Q -∗ □ (P ∗ Q).
+Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_intuitionistically_2 P Q `{!Persistent P, !Affine P} :
+  P -∗ □ Q -∗ □ (P ∗ Q).
+Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_intuitionistically_3 P Q :
+  □ P -∗ □ Q -∗ □ (<pers> P ∗ Q).
+Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed.
+
+Lemma test_iFrame_absorbingly_1 P Q `{!Absorbing P, !Persistent P} :
+  P -∗ Q -∗ <absorb> (P ∧ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_absorbingly_2 P Q :
+  <pers> P -∗ Q -∗ <absorb> (□ P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_absorbingly_3 P Q `{!Absorbing P, !Persistent P} :
+  P -∗ Q -∗ True ∗ (P ∧ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_absorbingly_4 P Q :
+  <pers> P -∗ Q -∗ True ∗ (□ P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+
+Lemma test_iFrame_persistently_1 P Q `{!Persistent P} :
+  <absorb> P -∗ □ Q -∗ <pers> (P ∗ Q).
+Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_persistently_2 P Q `{!Persistent P, !Absorbing P} :
+  P -∗ □ Q -∗ <pers> (P ∗ Q).
+Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_persistently_3 P Q :
+  <pers> P -∗ □ Q -∗ <pers> (□ P ∗ Q).
+Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed.
 
 Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
 Proof.

theories/proofmode/frame_instances.v

@@ -66,10 +66,12 @@ Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
 Proof. apply left_id, _. Qed.
 Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
 Proof. apply right_id, _. Qed.
-Global Instance make_sep_true_l P : Absorbing P → KnownLMakeSep True P P.
-Proof. intros. apply True_sep, _. Qed.
-Global Instance make_sep_true_r P : Absorbing P → KnownRMakeSep P True P.
-Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed.
+Global Instance make_sep_true_l P1 P2 :
+  MakeAbsorbingly P1 P2 → KnownLMakeSep True P1 P2.
+Proof. by rewrite /MakeAbsorbingly /KnownLMakeSep /MakeSep=> <-. Qed.
+Global Instance make_sep_true_r P1 P2 :
+  MakeAbsorbingly P1 P2 → KnownRMakeSep P1 True P2.
+Proof. rewrite /MakeAbsorbingly /KnownRMakeSep /MakeSep=> <-. by rewrite comm. Qed.
 Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
 Proof. by rewrite /MakeSep. Qed.
 
@@ -124,10 +126,10 @@ Global Instance make_and_true_l P : KnownLMakeAnd True P P.
 Proof. apply left_id, _. Qed.
 Global Instance make_and_true_r P : KnownRMakeAnd P True P.
 Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
-Global Instance make_and_emp_l P : Affine P → KnownLMakeAnd emp P P.
-Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd emp_and. Qed.
-Global Instance make_and_emp_r P : Affine P → KnownRMakeAnd P emp P.
-Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed.
+Global Instance make_and_emp_l P1 P2 : MakeAffinely P1 P2 → KnownLMakeAnd emp P1 P2.
+Proof. by rewrite /MakeAffinely /KnownLMakeAnd /MakeAnd=> <-. Qed.
+Global Instance make_and_emp_r P1 P2 : MakeAffinely P1 P2 → KnownRMakeAnd P1 emp P2.
+Proof. rewrite /MakeAffinely /KnownRMakeAnd /MakeAnd=> <-. by rewrite comm. Qed.
 Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. by rewrite /MakeAnd. Qed.
 
@@ -188,8 +190,17 @@ Proof.
   by rewrite assoc (comm _ P1) -assoc wand_elim_r.
 Qed.
 
+(** * Affinely *)
 Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
 Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_emp. Qed.
+Global Instance make_affinely_persistently P : KnownMakeAffinely (<pers> P) (□ P) | 0.
+Proof. by rewrite /KnownMakeAffinely /MakeAffinely. Qed.
+Global Instance make_affinely_absorbingly P1 P2 :
+  BiPositive PROP → MakeAffinely P1 P2 → KnownMakeAffinely (<absorb> P1) P2 | 0.
+Proof.
+  rewrite /KnownMakeAffinely /MakeAffinely=> ? <-.
+  by rewrite affinely_absorbingly_elim.
+Qed.
 Global Instance make_affinely_affine P : Affine P → KnownMakeAffinely P P | 1.
 Proof. intros. by rewrite /KnownMakeAffinely /MakeAffinely affine_affinely. Qed.
 Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
@@ -203,17 +214,21 @@ Proof.
     by rewrite -{1}(affine_affinely (_ R)%I) affinely_sep_2.
 Qed.
 
+(** * Intuitionistically *)
 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.
+(** The instance below also turns [<pers> P] into [□ P] *)
+Global Instance make_intuitionistically_intuitionistic P1 P2 :
+  Persistent P1 → MakeAffinely P1 P2 → KnownMakeIntuitionistically P1 P2 | 1.
 Proof.
-  intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically.
-  rewrite intuitionistic_intuitionistically //.
+  rewrite /MakeAffinely /KnownMakeIntuitionistically
+    /MakeIntuitionistically=> ? <-. apply (anti_symm _).
+  - apply intuitionistically_affinely.
+  - by rewrite {1}(persistent P1).
 Qed.
 Global Instance make_intuitionistically_default P :
   MakeIntuitionistically P (□ P) | 100.
@@ -226,14 +241,31 @@ Proof.
   rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
 Qed.
 
+(** * Absorbingly *)
 Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
 Proof.
   by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
      -absorbingly_True_emp absorbingly_pure.
 Qed.
-(* Note: there is no point in having an instance `Absorbing P → MakeAbsorbingly P P`
-because framing will never turn a proposition that is not absorbing into
-something that is absorbing. *)
+Global Instance make_absorbingly_affinely P1 P2 :
+  Persistent P1 → MakeAbsorbingly P1 P2 →
+  KnownMakeAbsorbingly (<affine> P1) P2 | 0.
+Proof.
+  rewrite /KnownMakeAbsorbingly /MakeAbsorbingly=> ? <-. apply (anti_symm _).
+  - by rewrite affinely_elim.
+  - by rewrite -(absorbingly_idemp (<affine> _))%I -persistent_absorbingly_affinely_2.
+Qed.
+Global Instance make_absorbingly_absorbing P :
+  Absorbing P → KnownMakeAbsorbingly P P | 1.
+Proof.
+  intros. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbing_absorbingly.
+Qed.
+(** The instance [make_absorbingly_intuitionistically] should be used after
+[make_absorbingly_absorbing], otherwise it will also turn [□] modalities into
+[<pers>] modalities if the BI is affine. *)
+Global Instance make_absorbingly_intuitionistically P :
+  KnownMakeAbsorbingly (□ P) (<pers> P) | 2.
+Proof. apply absorbingly_intuitionistically_into_persistently. Qed.
 Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
 Proof. by rewrite /MakeAbsorbingly. Qed.
 
@@ -243,6 +275,7 @@ Proof.
   rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
 Qed.
 
+(** * Persistently *)
 Global Instance make_persistently_true : @KnownMakePersistently PROP True True.
 Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.
 Global Instance make_persistently_emp : @KnownMakePersistently PROP emp True.
@@ -250,6 +283,15 @@ Proof.
   by rewrite /KnownMakePersistently /MakePersistently
      -persistently_True_emp persistently_pure.
 Qed.
+(** The instance below also turns [□ P] into [<pers> P]. *)
+Global Instance make_persistently_persistent_absorbing P1 P2 :
+  Persistent P1 → MakeAbsorbingly P1 P2 → KnownMakePersistently P1 P2 | 1.
+Proof.
+  rewrite /MakeAbsorbingly /KnownMakePersistently
+    /MakePersistently=> ? <-. apply (anti_symm _).
+  - apply persistently_into_absorbingly.
+  - by rewrite {1}(persistent P1) absorbingly_elim_persistently.
+Qed.
 Global Instance make_persistently_default P :
   MakePersistently P (<pers> P) | 100.
 Proof. by rewrite /MakePersistently. Qed.