Skip to content

GitLab

Commit b4567fbd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Rename `always` → `persistently` (the persistent modality).

parent 0ad1d2bd
Show whitespace changes
Inline Side-by-side
Showing with 311 additions and 310 deletions
theories/base_logic/base_logic.v
View file @ b4567fbd
......@@ -11,7 +11,7 @@ End uPred.
Hint Resolve pure_intro.
Hint Resolve or_elim or_intro_l' or_intro_r' : I.
Hint Resolve and_intro and_elim_l' and_elim_r' : I.
Hint Resolve always_mono : I.
Hint Resolve persistently_mono : I.
Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
Hint Immediate True_intro False_elim : I.
Hint Immediate iff_refl internal_eq_refl' : I.
theories/base_logic/big_op.v
View file @ b4567fbd
......@@ -117,11 +117,11 @@ Section list.
▷^n ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷^n Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_always Φ l :
Lemma big_sepL_persistently Φ l :
(□ [∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □ Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_always_if p Φ l :
Lemma big_sepL_persistently_if p Φ l :
□?p ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □?p Φ k x).
Proof. apply (big_opL_commute _). Qed.
......@@ -134,7 +134,7 @@ Section list.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepL_lookup. }
revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ.
{ rewrite big_sepL_nil; auto with I. }
rewrite big_sepL_cons. rewrite -always_and_sep_l; apply and_intro.
rewrite big_sepL_cons. rewrite -persistently_and_sep_l; apply and_intro.
- by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
- rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
Qed.
......@@ -143,10 +143,10 @@ Section list.
□ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ list] k↦x ∈ l, Φ k x)
⊢ [∗ list] k↦x ∈ l, Ψ k x.
Proof.
rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
setoid_rewrite always_impl; setoid_rewrite always_pure.
rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?.
by rewrite -always_wand_impl always_elim wand_elim_l.
by rewrite -persistently_wand_impl persistently_elim wand_elim_l.
Qed.
Global Instance big_sepL_nil_persistent Φ :
......@@ -307,11 +307,11 @@ Section gmap.
▷^n ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷^n Φ k x).
Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM_always Φ m :
Lemma big_sepM_persistently Φ m :
(□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x).
Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM_always_if p Φ m :
Lemma big_sepM_persistently_if p Φ m :
□?p ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □?p Φ k x).
Proof. apply (big_opM_commute _). Qed.
......@@ -323,7 +323,7 @@ Section gmap.
{ apply forall_intro=> k; apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
rewrite big_sepM_insert // -always_and_sep_l. apply and_intro.
rewrite big_sepM_insert // -persistently_and_sep_l. apply and_intro.
- rewrite (forall_elim i) (forall_elim x) lookup_insert.
by rewrite pure_True // True_impl.
- rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
......@@ -336,10 +336,10 @@ Section gmap.
□ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ map] k↦x ∈ m, Φ k x)
⊢ [∗ map] k↦x ∈ m, Ψ k x.
Proof.
rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
setoid_rewrite always_impl; setoid_rewrite always_pure.
rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
by rewrite -always_wand_impl always_elim wand_elim_l.
by rewrite -persistently_wand_impl persistently_elim wand_elim_l.
Qed.
Global Instance big_sepM_empty_persistent Φ :
......@@ -460,10 +460,10 @@ Section gset.
▷^n ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷^n Φ y).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_always Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y).
Lemma big_sepS_persistently Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_always_if q Φ X :
Lemma big_sepS_persistently_if q Φ X :
□?q ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □?q Φ y).
Proof. apply (big_opS_commute _). Qed.
......@@ -475,7 +475,7 @@ Section gset.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
induction X as [|x X ? IH] using collection_ind_L.
{ rewrite big_sepS_empty; auto. }
rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
rewrite big_sepS_insert // -persistently_and_sep_l. apply and_intro.
- by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
- rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
by rewrite pure_True ?True_impl; last set_solver.
......@@ -484,10 +484,10 @@ Section gset.
Lemma big_sepS_impl Φ Ψ X :
□ (∀ x, ⌜x ∈ X⌝ → Φ x → Ψ x) ∧ ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ X, Ψ x.
Proof.
rewrite always_and_sep_l always_forall.
setoid_rewrite always_impl; setoid_rewrite always_pure.
rewrite persistently_and_sep_l persistently_forall.
setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
by rewrite -always_wand_impl always_elim wand_elim_l.
by rewrite -persistently_wand_impl persistently_elim wand_elim_l.
Qed.
Global Instance big_sepS_empty_persistent Φ : Persistent ([∗ set] x ∈ ∅, Φ x).
......@@ -571,10 +571,10 @@ Section gmultiset.
▷^n ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷^n Φ y).
Proof. apply (big_opMS_commute _). Qed.
Lemma big_sepMS_always Φ X : □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y).
Lemma big_sepMS_persistently Φ X : □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y).
Proof. apply (big_opMS_commute _). Qed.
Lemma big_sepMS_always_if q Φ X :
Lemma big_sepMS_persistently_if q Φ X :
□?q ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □?q Φ y).
Proof. apply (big_opMS_commute _). Qed.
......
theories/base_logic/derived.v
View file @ b4567fbd
......@@ -16,11 +16,11 @@ Notation "▷? p P" := (uPred_laterN (Nat.b2n p) P)
(at level 20, p at level 9, P at level 20,
format "▷? p P") : uPred_scope.
Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
Definition uPred_persistently_if {M} (p : bool) (P : uPred M) : uPred M :=
(if p then □ P else P)%I.
Instance: Params (@uPred_always_if) 2.
Arguments uPred_always_if _ !_ _/.
Notation "□? p P" := (uPred_always_if p P)
Instance: Params (@uPred_persistently_if) 2.
Arguments uPred_persistently_if _ !_ _/.
Notation "□? p P" := (uPred_persistently_if p P)
(at level 20, p at level 9, P at level 20, format "□? p P").
Definition uPred_except_0 {M} (P : uPred M) : uPred M := ▷ False ∨ P.
......@@ -472,105 +472,105 @@ Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a,
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
(* Always derived *)
Hint Resolve always_mono always_elim.
Global Instance always_mono' : Proper ((⊢) ==> (⊢)) (@uPred_always M).
Proof. intros P Q; apply always_mono. Qed.
Global Instance always_flip_mono' :
Proper (flip (⊢) ==> flip (⊢)) (@uPred_always M).
Proof. intros P Q; apply always_mono. Qed.
Hint Resolve persistently_mono persistently_elim.
Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@uPred_persistently M).
Proof. intros P Q; apply persistently_mono. Qed.
Global Instance persistently_flip_mono' :
Proper (flip (⊢) ==> flip (⊢)) (@uPred_persistently M).
Proof. intros P Q; apply persistently_mono. Qed.
Lemma always_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
Proof. intros <-. apply always_idemp_2. Qed.
Lemma always_idemp P : □ □ P ⊣⊢ □ P.
Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
Lemma persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
Proof. intros <-. apply persistently_idemp_2. Qed.
Lemma persistently_idemp P : □ □ P ⊣⊢ □ P.
Proof. apply (anti_symm _); auto using persistently_idemp_2. Qed.
Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
Lemma persistently_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
Proof.
apply (anti_symm _); auto.
apply pure_elim'=> Hφ.
trans (∀ x : False, □ True : uPred M)%I; [by apply forall_intro|].
rewrite always_forall_2. auto using always_mono, pure_intro.
rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
Qed.
Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
Lemma persistently_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
Proof.
apply (anti_symm _); auto using always_forall_2.
apply (anti_symm _); auto using persistently_forall_2.
apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
Lemma persistently_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
Proof.
apply (anti_symm _); auto using always_exist_1.
apply (anti_symm _); auto using persistently_exist_1.
apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
Lemma always_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
Proof. rewrite !and_alt always_forall. by apply forall_proper=> -[]. Qed.
Lemma always_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
Proof. rewrite !or_alt always_exist. by apply exist_proper=> -[]. Qed.
Lemma always_impl P Q : □ (P → Q) ⊢ □ P → □ Q.
Lemma persistently_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed.
Lemma persistently_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
Lemma persistently_impl P Q : □ (P → Q) ⊢ □ P → □ Q.
Proof.
apply impl_intro_l; rewrite -always_and.
apply always_mono, impl_elim with P; auto.
apply impl_intro_l; rewrite -persistently_and.
apply persistently_mono, impl_elim with P; auto.
Qed.
Lemma always_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
Lemma persistently_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
Proof.
apply (anti_symm (⊢)); auto using always_elim.
apply (anti_symm (⊢)); auto using persistently_elim.
apply (internal_eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
{ intros n; solve_proper. }
rewrite -(internal_eq_refl a) always_pure; auto.
rewrite -(internal_eq_refl a) persistently_pure; auto.
Qed.
Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed.
Lemma always_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
Lemma always_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
Proof. by rewrite -always_and_sep_l' idemp. Qed.
Lemma persistently_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
Proof. apply (anti_symm (⊢)); auto using persistently_and_sep_l_1. Qed.
Lemma persistently_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
Proof. by rewrite !(comm _ P) persistently_and_sep_l'. Qed.
Lemma persistently_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
Proof. by rewrite -persistently_and_sep_l' idemp. Qed.
Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
Lemma persistently_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
Proof.
apply (anti_symm (⊢)); auto.
rewrite -{1}always_idemp always_and always_and_sep_l'; auto.
rewrite -{1}persistently_idemp persistently_and persistently_and_sep_l'; auto.
Qed.
Lemma always_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
Lemma persistently_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
Proof. by rewrite -persistently_and_sep -persistently_and_sep_l' persistently_and. Qed.
Lemma always_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
Lemma always_wand_impl P Q : □ (P -∗ Q) ⊣⊢ □ (P → Q).
Lemma persistently_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed.
Lemma persistently_wand_impl P Q : □ (P -∗ Q) ⊣⊢ □ (P → Q).
Proof.
apply (anti_symm (⊢)); [|by rewrite -impl_wand].
apply always_intro', impl_intro_r.
by rewrite always_and_sep_l' always_elim wand_elim_l.
apply persistently_intro', impl_intro_r.
by rewrite persistently_and_sep_l' persistently_elim wand_elim_l.
Qed.
Lemma wand_impl_always P Q : ((□ P) -∗ Q) ⊣⊢ ((□ P) → Q).
Lemma wand_impl_persistently P Q : ((□ P) -∗ Q) ⊣⊢ ((□ P) → Q).
Proof.
apply (anti_symm (⊢)); [|by rewrite -impl_wand].
apply impl_intro_l. by rewrite always_and_sep_l' wand_elim_r.
apply impl_intro_l. by rewrite persistently_and_sep_l' wand_elim_r.
Qed.
Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
Lemma persistently_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
Proof. intros; rewrite -persistently_and_sep_l'; auto. Qed.
Lemma persistently_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
Proof. intros; rewrite -persistently_and_sep_r'; auto. Qed.
Lemma always_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.
Lemma persistently_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite persistently_later IH. Qed.
Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □ (P ∗ R → Q).
Proof.
apply (anti_symm (⊢)).
- rewrite -(right_id True%I uPred_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
apply sep_mono_r. rewrite -always_pure. apply always_mono, impl_intro_l.
apply sep_mono_r. rewrite -persistently_pure. apply persistently_mono, impl_intro_l.
by rewrite wand_elim_r right_id.
- apply exist_elim=> R. apply wand_intro_l. rewrite assoc -always_and_sep_r'.
by rewrite always_elim impl_elim_r.
- apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r'.
by rewrite persistently_elim impl_elim_r.
Qed.
Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □ (P ∧ R -∗ Q).
Proof.
apply (anti_symm (⊢)).
- rewrite -(right_id True%I uPred_and (P → Q)%I) -(exist_intro (P → Q)%I).
apply and_mono_r. rewrite -always_pure. apply always_mono, wand_intro_l.
apply and_mono_r. rewrite -persistently_pure. apply persistently_mono, wand_intro_l.
by rewrite impl_elim_r right_id.
- apply exist_elim=> R. apply impl_intro_l. rewrite assoc always_and_sep_r'.
by rewrite always_elim wand_elim_r.
- apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r'.
by rewrite persistently_elim wand_elim_r.
Qed.
(* Later derived *)
......@@ -671,33 +671,33 @@ Qed.
Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.
(* Conditional always *)
Global Instance always_if_ne p : NonExpansive (@uPred_always_if M p).
(* Conditional persistently *)
Global Instance persistently_if_ne p : NonExpansive (@uPred_persistently_if M p).
Proof. solve_proper. Qed.
Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
Global Instance persistently_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_persistently_if M p).
Proof. solve_proper. Qed.
Global Instance always_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M p).
Global Instance persistently_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_persistently_if M p).
Proof. solve_proper. Qed.
Lemma always_if_elim p P : □?p P ⊢ P.
Proof. destruct p; simpl; auto using always_elim. Qed.
Lemma always_elim_if p P : □ P ⊢ □?p P.
Proof. destruct p; simpl; auto using always_elim. Qed.
Lemma always_if_pure p φ : □?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
Proof. destruct p; simpl; auto using always_pure. Qed.
Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
Proof. destruct p; simpl; auto using always_and. Qed.
Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
Proof. destruct p; simpl; auto using always_or. Qed.
Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
Proof. destruct p; simpl; auto using always_exist. Qed.
Lemma always_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
Proof. destruct p; simpl; auto using always_sep. Qed.
Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
Proof. destruct p; simpl; auto using always_later. Qed.
Lemma always_if_laterN p n P : □?p ▷^n P ⊣⊢ ▷^n □?p P.
Proof. destruct p; simpl; auto using always_laterN. Qed.
Lemma persistently_if_elim p P : □?p P ⊢ P.
Proof. destruct p; simpl; auto using persistently_elim. Qed.
Lemma persistently_elim_if p P : □ P ⊢ □?p P.
Proof. destruct p; simpl; auto using persistently_elim. Qed.
Lemma persistently_if_pure p φ : □?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
Proof. destruct p; simpl; auto using persistently_pure. Qed.
Lemma persistently_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
Proof. destruct p; simpl; auto using persistently_and. Qed.
Lemma persistently_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
Proof. destruct p; simpl; auto using persistently_or. Qed.
Lemma persistently_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
Proof. destruct p; simpl; auto using persistently_exist. Qed.
Lemma persistently_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
Proof. destruct p; simpl; auto using persistently_sep. Qed.
Lemma persistently_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
Proof. destruct p; simpl; auto using persistently_later. Qed.
Lemma persistently_if_laterN p n P : □?p ▷^n P ⊣⊢ ▷^n □?p P.
Proof. destruct p; simpl; auto using persistently_laterN. Qed.
(* True now *)
Global Instance except_0_ne : NonExpansive (@uPred_except_0 M).
......@@ -727,7 +727,7 @@ Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q.
Proof.
rewrite /uPred_except_0. apply (anti_symm _).
- apply or_elim; last by auto.
by rewrite -!or_intro_l -always_pure -always_later -always_sep_dup'.
by rewrite -!or_intro_l -persistently_pure -persistently_later -persistently_sep_dup'.
- rewrite sep_or_r sep_elim_l sep_or_l; auto.
Qed.
Lemma except_0_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
......@@ -743,20 +743,20 @@ Proof.
Qed.
Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
Proof. by rewrite /uPred_except_0 -later_or False_or. Qed.
Lemma except_0_always P : ◇ □ P ⊣⊢ □ ◇ P.
Proof. by rewrite /uPred_except_0 always_or always_later always_pure. Qed.
Lemma except_0_always_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
Proof. destruct p; simpl; auto using except_0_always. Qed.
Lemma except_0_persistently P : ◇ □ P ⊣⊢ □ ◇ P.
Proof. by rewrite /uPred_except_0 persistently_or persistently_later persistently_pure. Qed.
Lemma except_0_persistently_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
Proof. destruct p; simpl; auto using except_0_persistently. Qed.
Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
(* Own and valid derived *)
Lemma always_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
Lemma persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
Proof.
intros; apply (anti_symm _); first by apply:always_elim.
by rewrite {1}always_ownM_core core_id_core.
intros; apply (anti_symm _); first by apply:persistently_elim.
by rewrite {1}persistently_ownM_core core_id_core.
Qed.
Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
......@@ -764,10 +764,10 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
Proof. apply (anti_symm _); first by auto. apply ownM_unit. Qed.
Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
Lemma persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
Proof.
intros; apply (anti_symm _); first by apply:always_elim.
apply:always_cmra_valid_1.
intros; apply (anti_symm _); first by apply:persistently_elim.
apply:persistently_cmra_valid_1.
Qed.
(** * Derived rules *)
......@@ -823,8 +823,8 @@ Proof.
apply or_mono, wand_intro_l; first done.
rewrite -{2}(löb Q); apply impl_intro_l.
rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
rewrite -(always_pure) -always_later always_and_sep_l'.
by rewrite assoc (comm _ _ P) -assoc -always_and_sep_l' impl_elim_r wand_elim_r.
rewrite -(persistently_pure) -persistently_later persistently_and_sep_l'.
by rewrite assoc (comm _ _ P) -assoc -persistently_and_sep_l' impl_elim_r wand_elim_r.
Qed.
Global Instance forall_timeless {A} (Ψ : A → uPred M) :
(∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
......@@ -842,9 +842,9 @@ Proof.
- rewrite /uPred_except_0; auto.
- apply exist_elim=> x. rewrite -(exist_intro x); auto.
Qed.
Global Instance always_timeless P : Timeless P → Timeless (□ P).
Proof. intros; rewrite /Timeless except_0_always -always_later; auto. Qed.
Global Instance always_if_timeless p P : Timeless P → Timeless (□?p P).
Global Instance persistently_timeless P : Timeless P → Timeless (□ P).
Proof. intros; rewrite /Timeless except_0_persistently -persistently_later; auto. Qed.
Global Instance persistently_if_timeless p P : Timeless P → Timeless (□?p P).
Proof. destruct p; apply _. Qed.
Global Instance eq_timeless {A : ofeT} (a b : A) :
Discrete a → Timeless (a ≡ b : uPred M)%I.
......@@ -867,71 +867,71 @@ Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → uPred
NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
Lemma always_always P `{!Persistent P} : □ P ⊣⊢ P.
Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
Lemma always_if_always p P `{!Persistent P} : □?p P ⊣⊢ P.
Proof. destruct p; simpl; auto using always_always. Qed.
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 `{!Persistent P} : P ∧ Q ⊣⊢ P ∗ Q.
Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
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 `{!Persistent P} : P ⊣⊢ P ∗ P.
Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
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 `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
Lemma always_impl_wand P `{!Persistent P} Q : (P → Q) ⊣⊢ (P -∗ Q).
Lemma persistently_persistently P `{!Persistent P} : □ P ⊣⊢ P.
Proof. apply (anti_symm (⊢)); auto using persistently_elim. Qed.
Lemma persistently_if_persistently p P `{!Persistent P} : □?p P ⊣⊢ P.
Proof. destruct p; simpl; auto using persistently_persistently. Qed.
Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
Proof. rewrite -(persistently_persistently P); apply persistently_intro'. Qed.
Lemma persistently_and_sep_l P Q `{!Persistent P} : P ∧ Q ⊣⊢ P ∗ Q.
Proof. by rewrite -(persistently_persistently P) persistently_and_sep_l'. Qed.
Lemma persistently_and_sep_r P Q `{!Persistent Q} : P ∧ Q ⊣⊢ P ∗ Q.
Proof. by rewrite -(persistently_persistently Q) persistently_and_sep_r'. Qed.
Lemma persistently_sep_dup P `{!Persistent P} : P ⊣⊢ P ∗ P.
Proof. by rewrite -(persistently_persistently P) -persistently_sep_dup'. Qed.
Lemma persistently_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
Proof. by rewrite -(persistently_persistently Q); apply persistently_entails_l'. Qed.
Lemma persistently_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
Proof. by rewrite -(persistently_persistently Q); apply persistently_entails_r'. Qed.
Lemma persistently_impl_wand P `{!Persistent P} Q : (P → Q) ⊣⊢ (P -∗ Q).
Proof.
apply (anti_symm _); auto using impl_wand.
apply impl_intro_l. by rewrite always_and_sep_l wand_elim_r.
apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r.
Qed.
(* Persistence *)
Global Instance pure_persistent φ : Persistent (⌜φ⌝ : uPred M)%I.
Proof. by rewrite /Persistent always_pure. Qed.
Proof. by rewrite /Persistent persistently_pure. Qed.
Global Instance pure_impl_persistent φ Q :
Persistent Q → Persistent (⌜φ⌝ → Q)%I.
Proof.
rewrite /Persistent pure_impl_forall always_forall. auto using forall_mono.
rewrite /Persistent pure_impl_forall persistently_forall. auto using forall_mono.
Qed.
Global Instance pure_wand_persistent φ Q :
Persistent Q → Persistent (⌜φ⌝ -∗ Q)%I.
Proof.
rewrite /Persistent -always_impl_wand pure_impl_forall always_forall.
rewrite /Persistent -persistently_impl_wand pure_impl_forall persistently_forall.
auto using forall_mono.
Qed.
Global Instance always_persistent P : Persistent (□ P).
Proof. by intros; apply always_intro'. Qed.
Global Instance persistently_persistent P : Persistent (□ P).