Prove `<absorb> □ P ⊣⊢ <pers> P` and use it to refactor some stuff.

theories/bi/derived_laws.v

@@ -1113,10 +1113,24 @@ Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 Lemma persistent_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
 Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 
-Lemma persistent_absorbingly_affinely P `{!Persistent P} : P ⊢ <absorb> <affine> P.
+Lemma absorbingly_affinely_persistently P : <absorb> □ P ⊣⊢ <pers> P.
 Proof.
-  by rewrite {1}(persistent_persistently_2 P) -persistently_affinely
-             persistently_elim_absorbingly.
+  apply (anti_symm _).
+  - by rewrite affinely_elim absorbingly_persistently.
+  - rewrite -{1}(idemp bi_and (<pers> _)%I) persistently_and_affinely_sep_r.
+    by rewrite {1} (True_intro (<pers> _)%I).
+Qed.
+
+Lemma persistent_absorbingly_affinely_2 P `{!Persistent P} :
+  P ⊢ <absorb> <affine> P.
+Proof.
+  rewrite {1}(persistent P) -absorbingly_affinely_persistently.
+  by rewrite -{1}affinely_idemp affinely_persistently_elim.
+Qed.
+Lemma persistent_absorbingly_affinely P `{!Persistent P, !Absorbing P} :
+  <absorb> <affine> P ⊣⊢ P.
+Proof.
+  by rewrite -(persistent_persistently P) absorbingly_affinely_persistently.
 Qed.
 
 Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :

theories/proofmode/class_instances.v

@@ -106,7 +106,7 @@ Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
 Proof.
   rewrite /FromPure /IntoPure=> <- -> /=.
   rewrite pure_impl -impl_wand_2. apply bi.wand_intro_l.
-  rewrite {1}(persistent_absorbingly_affinely ⌜φ1⌝%I) absorbingly_sep_l
+  rewrite -{1}(persistent_absorbingly_affinely ⌜φ1⌝%I) absorbingly_sep_l
           bi.wand_elim_r absorbing //.
 Qed.
 
@@ -186,8 +186,9 @@ Global Instance from_pure_affinely_false P φ `{!Affine P} :
   FromPure false P φ → FromPure false (<affine> P) φ.
 Proof. rewrite /FromPure /= affine_affinely //. Qed.
 
-Global Instance from_pure_absorbingly P φ : FromPure true P φ → FromPure false (<absorb> P) φ.
-Proof. rewrite /FromPure=> <- /=. apply persistent_absorbingly_affinely, _. Qed.
+Global Instance from_pure_absorbingly P φ :
+  FromPure true P φ → FromPure false (<absorb> P) φ.
+Proof. rewrite /FromPure=> <- /=. by rewrite persistent_absorbingly_affinely. Qed.
 Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
   FromPure a P φ → FromPure a ⎡P⎤ φ.
 Proof. rewrite /FromPure=> <-. by rewrite embed_affinely_if embed_pure. Qed.

theories/proofmode/coq_tactics.v

@@ -590,7 +590,7 @@ Proof.
   - destruct HPQ.
     + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
       by apply pure_elim_l.
-    + rewrite (into_pure P) (persistent_absorbingly_affinely ⌜ _ ⌝%I) absorbingly_sep_lr.
+    + rewrite (into_pure P) -(persistent_absorbingly_affinely ⌜ _ ⌝%I) absorbingly_sep_lr.
       rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
 
@@ -612,8 +612,8 @@ Proof.
     + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
               (into_persistent _ P) wand_elim_r //.
     + rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
-      by rewrite {1}(persistent_absorbingly_affinely (<pers> _)%I)
-                 absorbingly_sep_l wand_elim_r HQ.
+      by rewrite -{1}absorbingly_affinely_persistently
+        absorbingly_sep_l wand_elim_r HQ.
 Qed.
 
 (** * Implication and wand *)
@@ -669,8 +669,8 @@ Proof.
   - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
             (into_persistent _ P) wand_elim_r //.
   - rewrite (_ : P = □?false P)%I // (into_persistent _ P).
-    by rewrite {1}(persistent_absorbingly_affinely (<pers> _)%I)
-               absorbingly_sep_l wand_elim_r HQ.
+    by rewrite -{1}absorbingly_affinely_persistently
+      absorbingly_sep_l wand_elim_r HQ.
 Qed.
 Lemma tac_wand_intro_pure Δ P φ Q R :
   FromWand R P Q →
@@ -681,7 +681,7 @@ Proof.
   rewrite /FromWand envs_entails_eq. intros <- ? HPQ HQ. apply wand_intro_l. destruct HPQ.
   - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
     by apply pure_elim_l.
-  - rewrite (into_pure P) (persistent_absorbingly_affinely ⌜ _ ⌝%I) absorbingly_sep_lr.
+  - rewrite (into_pure P) -(persistent_absorbingly_affinely ⌜ _ ⌝%I) absorbingly_sep_lr.
     rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
 Lemma tac_wand_intro_drop Δ P Q R :