Commit d0276a67 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename some old occurences of always stable into persistent.

parent 7952bca4
...@@ -957,7 +957,7 @@ Proof. intros P Q; apply later_mono. Qed. ...@@ -957,7 +957,7 @@ Proof. intros P Q; apply later_mono. Qed.
Global Instance later_flip_mono' : Global Instance later_flip_mono' :
Proper (flip () ==> flip ()) (@uPred_later M). Proper (flip () ==> flip ()) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed. Proof. intros P Q; apply later_mono. Qed.
Lemma later_True : ( True) True. Lemma later_True : True True.
Proof. apply (anti_symm ()); auto using later_intro. Qed. Proof. apply (anti_symm ()); auto using later_intro. Qed.
Lemma later_impl P Q : (P Q) ( P Q). Lemma later_impl P Q : (P Q) ( P Q).
Proof. Proof.
...@@ -969,7 +969,7 @@ Lemma later_exist `{Inhabited A} (Φ : A → uPred M) : ...@@ -969,7 +969,7 @@ Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
Proof. apply: anti_symm; eauto using later_exist', later_exist_1. Qed. Proof. apply: anti_symm; eauto using later_exist', later_exist_1. Qed.
Lemma later_wand P Q : (P - Q) ( P - Q). Lemma later_wand P Q : (P - Q) ( P - Q).
Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed. Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
Lemma later_iff P Q : ( (P Q)) ( P Q). Lemma later_iff P Q : (P Q) ( P Q).
Proof. by rewrite /uPred_iff later_and !later_impl. Qed. Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
Lemma löb_strong P Q : (P Q) Q P Q. Lemma löb_strong P Q : (P Q) Q P Q.
Proof. Proof.
...@@ -1119,7 +1119,7 @@ Proof. ...@@ -1119,7 +1119,7 @@ Proof.
cmra_timeless_included_l; eauto using cmra_validN_le. cmra_timeless_included_l; eauto using cmra_validN_le.
Qed. Qed.
(* Always stable *) (* Persistence *)
Global Instance const_persistent φ : PersistentP ( φ : uPred M)%I. Global Instance const_persistent φ : PersistentP ( φ : uPred M)%I.
Proof. by rewrite /PersistentP always_const. Qed. Proof. by rewrite /PersistentP always_const. Qed.
Global Instance always_persistent P : PersistentP ( P). Global Instance always_persistent P : PersistentP ( P).
...@@ -1153,7 +1153,7 @@ Global Instance default_persistent {A} P (Ψ : A → uPred M) (mx : option A) : ...@@ -1153,7 +1153,7 @@ Global Instance default_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
PersistentP P ( x, PersistentP (Ψ x)) PersistentP (default P mx Ψ). PersistentP P ( x, PersistentP (Ψ x)) PersistentP (default P mx Ψ).
Proof. destruct mx; apply _. Qed. Proof. destruct mx; apply _. Qed.
(* Derived lemmas for always stable *) (* Derived lemmas for persistence *)
Lemma always_always P `{!PersistentP P} : ( P) P. Lemma always_always P `{!PersistentP P} : ( P) P.
Proof. apply (anti_symm ()); auto using always_elim. Qed. Proof. apply (anti_symm ()); auto using always_elim. Qed.
Lemma always_intro P Q `{!PersistentP P} : P Q P Q. Lemma always_intro P Q `{!PersistentP P} : P Q P Q.
......
...@@ -28,17 +28,18 @@ Instance: Params (@uPred_big_sepS) 5. ...@@ -28,17 +28,18 @@ Instance: Params (@uPred_big_sepS) 5.
Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ) Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ)
(at level 20, X at level 10, format "Π★{set X } Φ") : uPred_scope. (at level 20, X at level 10, format "Π★{set X } Φ") : uPred_scope.
(** * Always stability for lists *) (** * Persistence of lists of uPreds *)
Class PersistentL {M} (Ps : list (uPred M)) := Class PersistentL {M} (Ps : list (uPred M)) :=
persistentL : Forall PersistentP Ps. persistentL : Forall PersistentP Ps.
Arguments persistentL {_} _ {_}. Arguments persistentL {_} _ {_}.
(** * Properties *)
Section big_op. Section big_op.
Context {M : cmraT}. Context {M : cmraT}.
Implicit Types Ps Qs : list (uPred M). Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type. Implicit Types A : Type.
(* Big ops *) (** ** Big ops over lists *)
Global Instance big_and_proper : Proper (() ==> ()) (@uPred_big_and M). Global Instance big_and_proper : Proper (() ==> ()) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M). Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M).
...@@ -91,7 +92,7 @@ Proof. induction 1; simpl; auto with I. Qed. ...@@ -91,7 +92,7 @@ Proof. induction 1; simpl; auto with I. Qed.
Lemma big_sep_elem_of Ps P : P Ps Π★ Ps P. Lemma big_sep_elem_of Ps P : P Ps Π★ Ps P.
Proof. induction 1; simpl; auto with I. Qed. Proof. induction 1; simpl; auto with I. Qed.
(* Big ops over finite maps *) (** ** Big ops over finite maps *)
Section gmap. Section gmap.
Context `{Countable K} {A : Type}. Context `{Countable K} {A : Type}.
Implicit Types m : gmap K A. Implicit Types m : gmap K A.
...@@ -152,7 +153,7 @@ Section gmap. ...@@ -152,7 +153,7 @@ Section gmap.
Qed. Qed.
End gmap. End gmap.
(* Big ops over finite sets *) (** ** Big ops over finite sets *)
Section gset. Section gset.
Context `{Countable A}. Context `{Countable A}.
Implicit Types X : gset A. Implicit Types X : gset A.
...@@ -213,7 +214,7 @@ Section gset. ...@@ -213,7 +214,7 @@ Section gset.
Qed. Qed.
End gset. End gset.
(* Always stable *) (** ** Persistence *)
Global Instance big_and_persistent Ps : PersistentL Ps PersistentP (Π Ps). Global Instance big_and_persistent Ps : PersistentL Ps PersistentP (Π Ps).
Proof. induction 1; apply _. Qed. Proof. induction 1; apply _. Qed.
Global Instance big_sep_persistent Ps : PersistentL Ps PersistentP (Π★ Ps). Global Instance big_sep_persistent Ps : PersistentL Ps PersistentP (Π★ Ps).
......
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