Commit 0f2f51ba authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Jacques-Henri Jourdan

The bare modality is also persistent.

parent e896ce1a
......@@ -1182,8 +1182,6 @@ Global Instance pure_persistent φ : Persistent (⌜φ⌝%I : PROP).
Proof. by rewrite /Persistent persistently_pure. Qed.
Global Instance emp_persistent : Persistent (emp%I : PROP).
Proof. rewrite /Persistent. apply persistently_emp_intro. Qed.
Global Instance persistently_persistent P : Persistent ( P).
Proof. by rewrite /Persistent persistently_idemp. Qed.
Global Instance and_persistent P Q :
Persistent P Persistent Q Persistent (P Q).
Proof. intros. by rewrite /Persistent persistently_and -!persistent. Qed.
......@@ -1217,6 +1215,11 @@ Global Instance sep_persistent P Q :
Persistent P Persistent Q Persistent (P Q).
Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.
Global Instance persistently_persistent P : Persistent ( P).
Proof. by rewrite /Persistent persistently_idemp. Qed.
Global Instance bare_persistent P : Persistent P Persistent ( P).
Proof. rewrite /bi_bare. apply _. Qed.
Global Instance from_option_persistent {A} P (Ψ : A PROP) (mx : option A) :
( x, Persistent (Ψ x)) Persistent P Persistent (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.
......
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