Commit f230165b authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso Committed by Robbert Krebbers
Browse files
parent 58c1caae
...@@ -548,6 +548,13 @@ Global Instance big_sepMS_plain `{BiAffine PROP, Countable A} (Φ : A → PROP) ...@@ -548,6 +548,13 @@ Global Instance big_sepMS_plain `{BiAffine PROP, Countable A} (Φ : A → PROP)
( x, Plain (Φ x)) Plain ([ mset] x X, Φ x). ( x, Plain (Φ x)) Plain ([ mset] x X, Φ x).
Proof. rewrite big_opMS_eq. apply _. Qed. Proof. rewrite big_opMS_eq. apply _. Qed.
Global Instance plainly_timeless P `{!BiPlainlyExist PROP} :
Timeless P Timeless ( P).
Proof.
intros. rewrite /Timeless /bi_except_0 later_plainly_1.
by rewrite (timeless P) /bi_except_0 plainly_or {1}plainly_elim.
Qed.
(* Interaction with equality *) (* Interaction with equality *)
Section internal_eq. Section internal_eq.
Context `{!BiInternalEq PROP}. Context `{!BiInternalEq PROP}.
...@@ -604,6 +611,13 @@ Section prop_ext. ...@@ -604,6 +611,13 @@ Section prop_ext.
(λ Q, (True - Q))%I ltac:(shelve)); last solve_proper. (λ Q, (True - Q))%I ltac:(shelve)); last solve_proper.
by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl. by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
Qed. Qed.
(* This proof uses [BiPlainlyExist] and [BiLöb] via [plainly_timeless] and
[wand_timeless]. *)
Global Instance internal_eq_timeless `{!BiPlainlyExist PROP, !BiLöb PROP}
`{!Timeless P} `{!Timeless Q} :
Timeless (PROP := PROP) (P Q).
Proof. rewrite prop_ext. apply _. Qed.
End prop_ext. End prop_ext.
(* Interaction with ▷ *) (* Interaction with ▷ *)
...@@ -629,12 +643,6 @@ Proof. induction n; apply _. Qed. ...@@ -629,12 +643,6 @@ Proof. induction n; apply _. Qed.
Global Instance except_0_plain P : Plain P Plain ( P). Global Instance except_0_plain P : Plain P Plain ( P).
Proof. rewrite /bi_except_0; apply _. Qed. Proof. rewrite /bi_except_0; apply _. Qed.
Global Instance plainly_timeless P `{!BiPlainlyExist PROP} :
Timeless P Timeless ( P).
Proof.
intros. rewrite /Timeless /bi_except_0 later_plainly_1.
by rewrite (timeless P) /bi_except_0 plainly_or {1}plainly_elim.
Qed.
End plainly_derived. End plainly_derived.
(* When declared as an actual instance, [plain_persistent] will cause (* When declared as an actual instance, [plain_persistent] will cause
......
Supports Markdown
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