Merge branch 'robbert/iFrame_affine' into 'master'

More general instance for framing under `<affine>`

See merge request !522

CHANGELOG.md

@@ -45,6 +45,9 @@ With this release, we dropped support for Coq 8.9.
   if the result after framing is `True` or `emp`. In particular, it no longer
   removes `<affine>` if the result after framing is affine, and it no longer
   removes `□` if the result after framing is intuitionistic.
+* Allow framing below an `<affine>` modality if the hypothesis that is framed is
+  affine. (Previously, framing below `<affine>` was only possible if the
+  hypothesis that is framed resides in the intuitionistic context.)
 
 **Changes in `base_logic`:**
 

tests/proofmode.v

@@ -455,6 +455,13 @@ Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
 Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
 Proof. iIntros "H1 H2". by iFrame "H1". Qed.
 
+Lemma test_iFrame_affinely_1 P Q `{!Affine P} :
+  P -∗ <affine> Q -∗ <affine> (P ∗ Q).
+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_iAssert_modality P : ◇ False -∗ ▷ P.
 Proof.
   iIntros "HF".

theories/proofmode/frame_instances.v

@@ -204,11 +204,12 @@ Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_em
 Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
 Proof. by rewrite /MakeAffinely. Qed.
 
-Global Instance frame_affinely R P Q Q' :
-  Frame true R P Q → MakeAffinely Q Q' → Frame true R (<affine> P) Q'.
+Global Instance frame_affinely p R P Q Q' :
+  TCOr (TCEq p true) (Affine R) →
+  Frame p R P Q → MakeAffinely Q Q' → Frame p R (<affine> P) Q'.
 Proof.
-  rewrite /Frame /MakeAffinely=> <- <- /=.
-  rewrite -{1}(affine_affinely (□ R)%I) affinely_sep_2 //.
+  rewrite /Frame /MakeAffinely=> -[->|?] <- <- /=;
+    by rewrite -{1}(affine_affinely (_ R)%I) affinely_sep_2.
 Qed.
 
 Global Instance make_intuitionistically_emp :