Commit 2386287d authored by Robbert Krebbers's avatar Robbert Krebbers

Rename AlwaysStable into Persistent as suggested by Derek.

parent a26a3367
......@@ -303,10 +303,9 @@ Infix "↔" := uPred_iff : uPred_scope.
Class TimelessP {M} (P : uPred M) := timelessP : P (P False).
Arguments timelessP {_} _ {_}.
(* TODO: Derek suggested to call such assertions "persistent", which we now
do in the paper. *)
Class AlwaysStable {M} (P : uPred M) := always_stable : P P.
Arguments always_stable {_} _ {_}.
Class Persistent {M} (P : uPred M) := persistent : P P.
Arguments persistent {_} _ {_}.
Module uPred.
Definition unseal :=
......@@ -1121,49 +1120,53 @@ Proof.
Qed.
(* Always stable *)
Local Notation AS := AlwaysStable.
Global Instance const_always_stable φ : AS ( φ : uPred M)%I.
Proof. by rewrite /AlwaysStable always_const. Qed.
Global Instance always_always_stable P : AS ( P).
Global Instance const_persistent φ : Persistent ( φ : uPred M)%I.
Proof. by rewrite /Persistent always_const. Qed.
Global Instance always_persistent P : Persistent ( P).
Proof. by intros; apply always_intro'. Qed.
Global Instance and_always_stable P Q: AS P AS Q AS (P Q).
Proof. by intros; rewrite /AlwaysStable always_and; apply and_mono. Qed.
Global Instance or_always_stable P Q : AS P AS Q AS (P Q).
Proof. by intros; rewrite /AlwaysStable always_or; apply or_mono. Qed.
Global Instance sep_always_stable P Q: AS P AS Q AS (P Q).
Proof. by intros; rewrite /AlwaysStable always_sep; apply sep_mono. Qed.
Global Instance forall_always_stable {A} (Ψ : A uPred M) :
( x, AS (Ψ x)) AS ( x, Ψ x).
Proof. by intros; rewrite /AlwaysStable always_forall; apply forall_mono. Qed.
Global Instance exist_always_stable {A} (Ψ : A uPred M) :
( x, AS (Ψ x)) AS ( x, Ψ x).
Proof. by intros; rewrite /AlwaysStable always_exist; apply exist_mono. Qed.
Global Instance eq_always_stable {A : cofeT} (a b : A) : AS (a b : uPred M)%I.
Proof. by intros; rewrite /AlwaysStable always_eq. Qed.
Global Instance valid_always_stable {A : cmraT} (a : A) : AS ( a : uPred M)%I.
Proof. by intros; rewrite /AlwaysStable always_valid. Qed.
Global Instance later_always_stable P : AS P AS ( P).
Proof. by intros; rewrite /AlwaysStable always_later; apply later_mono. Qed.
Global Instance ownM_core_always_stable (a : M) : AS (uPred_ownM (core a)).
Proof. by rewrite /AlwaysStable always_ownM_core. Qed.
Global Instance default_always_stable {A} P (Ψ : A uPred M) (mx : option A) :
AS P ( x, AS (Ψ x)) AS (default P mx Ψ).
Global Instance and_persistent P Q :
Persistent P Persistent Q Persistent (P Q).
Proof. by intros; rewrite /Persistent always_and; apply and_mono. Qed.
Global Instance or_persistent P Q :
Persistent P Persistent Q Persistent (P Q).
Proof. by intros; rewrite /Persistent always_or; apply or_mono. Qed.
Global Instance sep_persistent P Q :
Persistent P Persistent Q Persistent (P Q).
Proof. by intros; rewrite /Persistent always_sep; apply sep_mono. Qed.
Global Instance forall_persistent {A} (Ψ : A uPred M) :
( x, Persistent (Ψ x)) Persistent ( x, Ψ x).
Proof. by intros; rewrite /Persistent always_forall; apply forall_mono. Qed.
Global Instance exist_persistent {A} (Ψ : A uPred M) :
( x, Persistent (Ψ x)) Persistent ( x, Ψ x).
Proof. by intros; rewrite /Persistent always_exist; apply exist_mono. Qed.
Global Instance eq_persistent {A : cofeT} (a b : A) :
Persistent (a b : uPred M)%I.
Proof. by intros; rewrite /Persistent always_eq. Qed.
Global Instance valid_persistent {A : cmraT} (a : A) :
Persistent ( a : uPred M)%I.
Proof. by intros; rewrite /Persistent always_valid. Qed.
Global Instance later_persistent P : Persistent P Persistent ( P).
Proof. by intros; rewrite /Persistent always_later; apply later_mono. Qed.
Global Instance ownM_core_persistent (a : M) : Persistent (uPred_ownM (core a)).
Proof. by rewrite /Persistent always_ownM_core. Qed.
Global Instance default_persistent {A} P (Ψ : A uPred M) (mx : option A) :
Persistent P ( x, Persistent (Ψ x)) Persistent (default P mx Ψ).
Proof. destruct mx; apply _. Qed.
(* Derived lemmas for always stable *)
Lemma always_always P `{!AlwaysStable P} : ( P) P.
Lemma always_always P `{!Persistent P} : ( P) P.
Proof. apply (anti_symm ()); auto using always_elim. Qed.
Lemma always_intro P Q `{!AlwaysStable P} : P Q P Q.
Lemma always_intro P Q `{!Persistent P} : P Q P Q.
Proof. rewrite -(always_always P); apply always_intro'. Qed.
Lemma always_and_sep_l P Q `{!AlwaysStable P} : (P Q) (P Q).
Lemma always_and_sep_l P Q `{!Persistent P} : (P Q) (P Q).
Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
Lemma always_and_sep_r P Q `{!AlwaysStable Q} : (P Q) (P Q).
Lemma always_and_sep_r P Q `{!Persistent Q} : (P Q) (P Q).
Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
Lemma always_sep_dup P `{!AlwaysStable P} : P (P P).
Lemma always_sep_dup P `{!Persistent P} : P (P P).
Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
Lemma always_entails_l P Q `{!AlwaysStable Q} : (P Q) P (Q P).
Lemma always_entails_l P Q `{!Persistent Q} : (P Q) P (Q P).
Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
Lemma always_entails_r P Q `{!AlwaysStable Q} : (P Q) P (P Q).
Lemma always_entails_r P Q `{!Persistent Q} : (P Q) P (P Q).
Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
End uPred_logic.
......
......@@ -29,9 +29,9 @@ Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ)
(at level 20, X at level 10, format "Π★{set X } Φ") : uPred_scope.
(** * Always stability for lists *)
Class AlwaysStableL {M} (Ps : list (uPred M)) :=
always_stableL : Forall AlwaysStable Ps.
Arguments always_stableL {_} _ {_}.
Class PersistentL {M} (Ps : list (uPred M)) :=
persistentL : Forall Persistent Ps.
Arguments persistentL {_} _ {_}.
Section big_op.
Context {M : cmraT}.
......@@ -216,20 +216,22 @@ Section gset.
End gset.
(* Always stable *)
Local Notation AS := AlwaysStable.
Local Notation ASL := AlwaysStableL.
Global Instance big_and_always_stable Ps : ASL Ps AS (Π Ps).
Global Instance big_and_persistent Ps : PersistentL Ps Persistent (Π Ps).
Proof. induction 1; apply _. Qed.
Global Instance big_sep_always_stable Ps : ASL Ps AS (Π★ Ps).
Global Instance big_sep_persistent Ps : PersistentL Ps Persistent (Π★ Ps).
Proof. induction 1; apply _. Qed.
Global Instance nil_always_stable : ASL (@nil (uPred M)).
Global Instance nil_persistent : PersistentL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_always_stable P Ps : AS P ASL Ps ASL (P :: Ps).
Global Instance cons_persistent P Ps :
Persistent P PersistentL Ps PersistentL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_always_stable Ps Ps' : ASL Ps ASL Ps' ASL (Ps ++ Ps').
Global Instance app_persistent Ps Ps' :
PersistentL Ps PersistentL Ps' PersistentL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.
Global Instance zip_with_always_stable {A B} (f : A B uPred M) xs ys :
( x y, AS (f x y)) ASL (zip_with f xs ys).
Proof. unfold ASL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed.
Global Instance zip_with_persistent {A B} (f : A B uPred M) xs ys :
( x y, Persistent (f x y)) PersistentL (zip_with f xs ys).
Proof.
unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
End big_op.
......@@ -50,8 +50,8 @@ Definition recv (l : loc) (R : iProp) : iProp :=
barrier_ctx γ l P sts_ownS γ (i_states i) {[ Change i ]}
saved_prop_own i Q (Q - R))%I.
Global Instance barrier_ctx_always_stable (γ : gname) (l : loc) (P : iProp) :
AlwaysStable (barrier_ctx γ l P).
Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp) :
Persistent (barrier_ctx γ l P).
Proof. apply _. Qed.
(* TODO: Figure out if this has a "Global" or "Local" effect.
......
......@@ -33,7 +33,7 @@ Section definitions.
Global Instance heap_inv_proper : Proper (() ==> ()) heap_inv.
Proof. solve_proper. Qed.
Global Instance heap_ctx_always_stable N : AlwaysStable (heap_ctx N).
Global Instance heap_ctx_persistent N : Persistent (heap_ctx N).
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque heap_ctx heap_mapsto.
......
......@@ -30,7 +30,7 @@ Section definitions.
Proof. solve_proper. Qed.
Global Instance auth_own_timeless a : TimelessP (auth_own a).
Proof. apply _. Qed.
Global Instance auth_ctx_always_stable N φ : AlwaysStable (auth_ctx N φ).
Global Instance auth_ctx_persistent N φ : Persistent (auth_ctx N φ).
Proof. apply _. Qed.
End definitions.
......
......@@ -54,8 +54,8 @@ Lemma own_valid_l γ a : own γ a ⊢ (✓ a ★ own γ a).
Proof. by rewrite comm -own_valid_r. Qed.
Global Instance own_timeless γ a : Timeless a TimelessP (own γ a).
Proof. unfold own; apply _. Qed.
Global Instance own_core_always_stable γ a : AlwaysStable (own γ (core a)).
Proof. by rewrite /AlwaysStable always_own_core. Qed.
Global Instance own_core_persistent γ a : Persistent (own γ (core a)).
Proof. by rewrite /Persistent always_own_core. Qed.
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
......
......@@ -23,7 +23,7 @@ Implicit Types Φ : val Λ → iProp Λ Σ.
Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
Proof. intros n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive. Qed.
Global Instance inv_always_stable N P : AlwaysStable (inv N P).
Global Instance inv_persistent N P : Persistent (inv N P).
Proof. rewrite /inv; apply _. Qed.
Lemma always_inv N P : ( inv N P) inv N P.
......
......@@ -30,8 +30,8 @@ Proof.
apply uPred.always_ownM.
by rewrite Res_core !cmra_core_unit map_core_singleton.
Qed.
Global Instance ownI_always_stable i P : AlwaysStable (ownI i P).
Proof. by rewrite /AlwaysStable always_ownI. Qed.
Global Instance ownI_persistent i P : Persistent (ownI i P).
Proof. by rewrite /Persistent always_ownI. Qed.
Lemma ownI_sep_dup i P : ownI i P (ownI i P ownI i P).
Proof. apply (uPred.always_sep_dup _). Qed.
......@@ -69,8 +69,8 @@ Lemma ownG_empty : True ⊢ (ownG ∅ : iProp Λ Σ).
Proof. apply uPred.ownM_empty. Qed.
Global Instance ownG_timeless m : Timeless m TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Global Instance ownG_core_always_stable m : AlwaysStable (ownG (core m)).
Proof. by rewrite /AlwaysStable always_ownG_core. Qed.
Global Instance ownG_core_persistent m : Persistent (ownG (core m)).
Proof. by rewrite /Persistent always_ownG_core. Qed.
(* inversion lemmas *)
Lemma ownI_spec n r i P :
......
......@@ -144,10 +144,10 @@ Lemma pvs_strip_pvs E P Q : P ⊢ (|={E}=> Q) → (|={E}=> P) ⊢ (|={E}=> Q).
Proof. move=>->. by rewrite pvs_trans'. Qed.
Lemma pvs_frame_l E1 E2 P Q : (P |={E1,E2}=> Q) (|={E1,E2}=> P Q).
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :
Lemma pvs_always_l E1 E2 P Q `{!Persistent P} :
(P |={E1,E2}=> Q) (|={E1,E2}=> P Q).
Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} :
Lemma pvs_always_r E1 E2 P Q `{!Persistent Q} :
((|={E1,E2}=> P) Q) (|={E1,E2}=> P Q).
Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
Lemma pvs_impl_l E1 E2 P Q : ( (P Q) (|={E1,E2}=> P)) (|={E1,E2}=> Q).
......
......@@ -20,9 +20,9 @@ Section saved_prop.
Implicit Types x y : F (iPropG Λ Σ).
Implicit Types γ : gname.
Global Instance saved_prop_always_stable γ x :
AlwaysStable (saved_prop_own γ x).
Proof. by rewrite /AlwaysStable always_own. Qed.
Global Instance saved_prop_persistent γ x :
Persistent (saved_prop_own γ x).
Proof. by rewrite /Persistent always_own. Qed.
Lemma saved_prop_alloc_strong N x (G : gset gname) :
True pvs N N ( γ, (γ G) saved_prop_own γ x).
......
......@@ -42,7 +42,7 @@ Section definitions.
Global Instance sts_ctx_proper N :
Proper (pointwise_relation _ () ==> ()) (sts_ctx N).
Proof. solve_proper. Qed.
Global Instance sts_ctx_always_stable N φ : AlwaysStable (sts_ctx N φ).
Global Instance sts_ctx_persistent N φ : Persistent (sts_ctx N φ).
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque sts_own sts_ownS sts_ctx.
......
......@@ -239,10 +239,10 @@ Proof.
rewrite (comm _ ( R)%I); setoid_rewrite (comm _ R).
apply wp_frame_step_r.
Qed.
Lemma wp_always_l E e Φ R `{!AlwaysStable R} :
Lemma wp_always_l E e Φ R `{!Persistent R} :
(R WP e @ E {{ Φ }}) WP e @ E {{ λ v, R Φ v }}.
Proof. by setoid_rewrite (always_and_sep_l _ _); rewrite wp_frame_l. Qed.
Lemma wp_always_r E e Φ R `{!AlwaysStable R} :
Lemma wp_always_r E e Φ R `{!Persistent R} :
(WP e @ E {{ Φ }} R) WP e @ E {{ λ v, Φ v R }}.
Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed.
Lemma wp_impl_l E e Φ Ψ :
......
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