make affinely_True_emp more useful, and make absorbingly lemmas consistent

iris/bi/derived_laws.v

@@ -672,7 +672,7 @@ Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
 Lemma affinely_exist {A} (Φ : A → PROP) : <affine> (∃ a, Φ a) ⊣⊢ ∃ a, <affine> (Φ a).
 Proof. by rewrite /bi_affinely and_exist_l. Qed.
 
-Lemma affinely_True_emp : <affine> True ⊣⊢ <affine> emp.
+Lemma affinely_True_emp : <affine> True ⊣⊢ emp.
 Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed.
 
 Lemma affinely_and_l P Q : <affine> P ∧ Q ⊣⊢ <affine> (P ∧ Q).
@@ -708,6 +708,8 @@ Proof.
   apply (anti_symm _), absorbingly_intro.
   apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto.
 Qed.
+Lemma absorbingly_True : <absorb> True ⊣⊢ True.
+Proof. apply absorbingly_pure. Qed.
 Lemma absorbingly_or P Q : <absorb> (P ∨ Q) ⊣⊢ <absorb> P ∨ <absorb> Q.
 Proof. by rewrite /bi_absorbingly sep_or_l. Qed.
 Lemma absorbingly_and_1 P Q : <absorb> (P ∧ Q) ⊢ <absorb> P ∧ <absorb> Q.
@@ -719,8 +721,8 @@ Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.
 
 Lemma absorbingly_sep P Q : <absorb> (P ∗ Q) ⊣⊢ <absorb> P ∗ <absorb> Q.
 Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed.
-Lemma absorbingly_True_emp : <absorb> True ⊣⊢ <absorb> emp.
-Proof. by rewrite absorbingly_pure /bi_absorbingly right_id. Qed.
+Lemma absorbingly_emp_True : <absorb> emp ⊣⊢ True.
+Proof. rewrite /bi_absorbingly right_id //. Qed.
 Lemma absorbingly_wand P Q : <absorb> (P -∗ Q) ⊢ <absorb> P -∗ <absorb> Q.
 Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed.
 
@@ -734,7 +736,7 @@ Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
 Lemma affinely_absorbingly_elim `{!BiPositive PROP} P : <affine> <absorb> P ⊣⊢ <affine> P.
 Proof.
   apply (anti_symm _), affinely_mono, absorbingly_intro.
-  by rewrite /bi_absorbingly affinely_sep affinely_True_emp affinely_emp left_id.
+  by rewrite /bi_absorbingly affinely_sep affinely_True_emp left_id.
 Qed.
 
 (* Affine and absorbing propositions *)
@@ -1072,7 +1074,7 @@ Qed.
 Lemma intuitionistically_emp : □ emp ⊣⊢ emp.
 Proof.
   by rewrite /bi_intuitionistically -persistently_True_emp persistently_pure
-             affinely_True_emp affinely_emp.
+             affinely_True_emp.
 Qed.
 Lemma intuitionistically_False : □ False ⊣⊢ False.
 Proof. by rewrite /bi_intuitionistically persistently_pure affinely_False. Qed.

iris/proofmode/class_instances.v

@@ -64,7 +64,7 @@ Proof. by rewrite /FromAffinely. Qed.
 
 (** IntoAbsorbingly *)
 Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
-Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
+Proof. by rewrite /IntoAbsorbingly -absorbingly_emp_True. 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 :
@@ -184,7 +184,7 @@ Global Instance into_pure_pure_wand `{!BiPureForall PROP} a (φ1 φ2 : Prop) P1
 Proof.
   rewrite /FromPure /IntoPure=> <- -> /=. rewrite pure_impl.
   apply impl_intro_l, pure_elim_l=> ?. rewrite (pure_True φ1) //.
-  by rewrite -affinely_affinely_if affinely_True_emp affinely_emp left_id.
+  by rewrite -affinely_affinely_if affinely_True_emp left_id.
 Qed.
 
 Global Instance into_pure_affinely P φ : IntoPure P φ → IntoPure (<affine> P) φ.

iris/proofmode/coq_tactics.v

@@ -149,7 +149,7 @@ Lemma tac_pure_intro Δ Q φ a :
   envs_entails Δ Q.
 Proof.
   intros ???. rewrite envs_entails_unseal -(from_pure a Q). destruct a; simpl.
-  - by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp affinely_emp.
+  - by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp.
   - by apply pure_intro.
 Qed.
 
@@ -176,7 +176,7 @@ Lemma tac_pure_revert Δ φ P Q :
   (φ → envs_entails Δ Q).
 Proof.
   rewrite /FromAffinely envs_entails_unseal. intros <- -> ?.
-  by rewrite pure_True // affinely_True_emp affinely_emp left_id.
+  by rewrite pure_True // affinely_True_emp left_id.
 Qed.
 
 (** * Intuitionistic *)
@@ -391,7 +391,7 @@ Proof.
   rewrite envs_entails_unseal=> ?????. rewrite envs_simple_replace_singleton_sound //=.
   rewrite -intuitionistically_if_idemp (into_wand q true) /=.
   rewrite -(from_pure a P1) pure_True //.
-  rewrite -affinely_affinely_if affinely_True_emp affinely_emp.
+  rewrite -affinely_affinely_if affinely_True_emp.
   by rewrite intuitionistically_emp left_id wand_elim_r.
 Qed.
 

iris/proofmode/frame_instances.v

@@ -209,7 +209,7 @@ Qed.
 Global Instance make_affinely_emp : @KnownMakeAffinely PROP emp emp | 0.
 Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_emp. Qed.
 Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
-Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_emp. Qed.
+Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
 Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
 Proof. by rewrite /MakeAffinely. Qed.
 
@@ -249,7 +249,7 @@ Qed.
 Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
 Proof.
   by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
-     -absorbingly_True_emp absorbingly_pure.
+     -absorbingly_emp_True.
 Qed.
 Global Instance make_absorbingly_True : @KnownMakeAbsorbingly PROP True True | 0.
 Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbingly_pure. Qed.