Make the behavior of `iSplit` on `P ∗ □ Q` consistent with that of `iDestruct`.

It now turns the goal into `P` and `<pers> Q`, which is dual to
`iDestruct`, which turns `P ∧ <pers> Q` into `P` and `□ Q`.

theories/proofmode/class_instances_bi.v

@@ -22,6 +22,11 @@ Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
 Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
 Global Instance into_absorbingly_absorbing P : Absorbing P → IntoAbsorbingly P P | 1.
 Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.
+Global Instance into_absorbingly_intuitionistically P :
+  IntoAbsorbingly (<pers> P) (□ P) | 0.
+Proof.
+  by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
+Qed.
 Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
 Proof. by rewrite /IntoAbsorbingly. Qed.
 
@@ -382,19 +387,18 @@ Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
 Proof. by rewrite /FromAnd. Qed.
 Global Instance from_and_sep_persistent_l P1 P1' P2 :
-  FromAffinely P1 P1' → Persistent P1' → FromAnd (P1 ∗ P2) P1' P2 | 9.
+  Persistent P1 → IntoAbsorbingly P1' P1 → FromAnd (P1 ∗ P2) P1' P2 | 9.
 Proof.
-  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_l_1.
+  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
+  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
+  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
 Qed.
 Global Instance from_and_sep_persistent_r P1 P2 P2' :
-  FromAffinely P2 P2' → Persistent P2' → FromAnd (P1 ∗ P2) P1 P2' | 10.
-Proof.
-  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_r_1.
-Qed.
-Global Instance from_and_sep_persistent P1 P2 :
-  Persistent P1 → Persistent P2 → FromAnd (P1 ∗ P2) P1 P2 | 11.
+  Persistent P2 → IntoAbsorbingly P2' P2 → FromAnd (P1 ∗ P2) P1 P2' | 10.
 Proof.
-  rewrite /FromAffinely /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
+  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
+  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
+  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
 Qed.
 
 Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.

theories/proofmode/classes.v

@@ -117,11 +117,14 @@ Arguments FromModal {_ _ _} _ _%I _%I _%I : simpl never.
 Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
 Hint Mode FromModal - + - - - ! - : typeclass_instances.
 
+(** The [FromAffinely P Q] class is used to add an [<affine>] modality to the
+proposition [Q].
+
+The input is [Q] and the output is [P]. *)
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : <affine> Q ⊢ P.
 Arguments FromAffinely {_} _%I _%I : simpl never.
 Arguments from_affinely {_} _%I _%I {_}.
-Hint Mode FromAffinely + ! - : typeclass_instances.
 Hint Mode FromAffinely + - ! : typeclass_instances.
 
 (** The [IntoAbsorbingly P Q] class is used to add an [<absorb>] modality to

theories/tests/proofmode.v

@@ -444,4 +444,20 @@ Lemma test_apply_affine_wand `{!BiPlainly PROP} (P : PROP) :
   P -∗ (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q).
 Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
 
+Lemma test_and_sep (P Q R : PROP) : P ∧ (Q ∗ □ R) ⊢ (P ∧ Q) ∗ □ R.
+Proof.
+  iIntros "H". repeat iSplit.
+  - iDestruct "H" as "[$ _]".
+  - iDestruct "H" as "[_ [$ _]]".
+  - iDestruct "H" as "[_ [_ #$]]".
+Qed.
+
+Lemma test_and_sep_2 (P Q R : PROP) `{!Persistent R, !Affine R} :
+  P ∧ (Q ∗ R) ⊢ (P ∧ Q) ∗ R.
+Proof.
+  iIntros "H". repeat iSplit.
+  - iDestruct "H" as "[$ _]".
+  - iDestruct "H" as "[_ [$ _]]".
+  - iDestruct "H" as "[_ [_ #$]]".
+Qed.
 End tests.