Commit 90f773c0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Prove that from_option is timeless.

parent ce32b224
...@@ -794,6 +794,9 @@ Proof. ...@@ -794,6 +794,9 @@ Proof.
apply except_0_mono. rewrite internal_eq_sym. apply except_0_mono. rewrite internal_eq_sym.
apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto. apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto.
Qed. Qed.
Global Instance from_option_timeless {A} P (Ψ : A uPred M) (mx : option A) :
( x, TimelessP (Ψ x)) TimelessP P TimelessP (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.
(* Persistence *) (* Persistence *)
Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I. Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
......
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