Commit 00db32d1 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Don't create `<pers>` modalities in `iSplit` when the BI is affine.

parent 480bc071
...@@ -23,7 +23,7 @@ Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed. ...@@ -23,7 +23,7 @@ Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
Global Instance into_absorbingly_absorbing P : Absorbing P IntoAbsorbingly P P | 1. Global Instance into_absorbingly_absorbing P : Absorbing P IntoAbsorbingly P P | 1.
Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed. Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.
Global Instance into_absorbingly_intuitionistically P : Global Instance into_absorbingly_intuitionistically P :
IntoAbsorbingly (<pers> P) ( P) | 0. IntoAbsorbingly (<pers> P) ( P) | 2.
Proof. Proof.
by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently. by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
Qed. Qed.
......
...@@ -460,4 +460,10 @@ Proof. ...@@ -460,4 +460,10 @@ Proof.
- iDestruct "H" as "[_ [$ _]]". - iDestruct "H" as "[_ [$ _]]".
- iDestruct "H" as "[_ [_ #$]]". - iDestruct "H" as "[_ [_ #$]]".
Qed. Qed.
Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q : P Q P Q.
Proof.
iIntros "[??]". iSplit; last done.
lazymatch goal with |- coq_tactics.envs_entails _ ( P) => done end.
Qed.
End tests. End tests.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment