diff --git a/algebra/upred.v b/algebra/upred.v
index 02bfe8cb6f64a18254e3e869af3dd02d98595996..de250643affdc688097d79875f8435728f4d373f 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -124,11 +124,11 @@ Next Obligation.
Qed.
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
-Program Definition uPred_forall {M A} (P : A → uPred M) : uPred M :=
- {| uPred_holds n x := ∀ a, P a n x |}.
+Program Definition uPred_forall {M A} (Ψ : A → uPred M) : uPred M :=
+ {| uPred_holds n x := ∀ a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
-Program Definition uPred_exist {M A} (P : A → uPred M) : uPred M :=
- {| uPred_holds n x := ∃ a, P a n x |}.
+Program Definition uPred_exist {M A} (Ψ : A → uPred M) : uPred M :=
+ {| uPred_holds n x := ∃ a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_eq {M} {A : cofeT} (a1 a2 : A) : uPred M :=
@@ -299,10 +299,10 @@ Global Instance eq_proper (A : cofeT) :
Proper ((≡) ==> (≡) ==> (≡)) (@uPred_eq M A) := ne_proper_2 _.
Global Instance forall_ne A :
Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
-Proof. by intros n P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
+Proof. by intros n Ψ1 Ψ2 HΨ x n'; split; intros HP a; apply HΨ. Qed.
Global Instance forall_proper A :
Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_forall M A).
-Proof. by intros P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
+Proof. by intros Ψ1 Ψ2 HΨ x n'; split; intros HP a; apply HΨ. Qed.
Global Instance exists_ne A :
Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
Proof. by intros n P1 P2 HP x; split; intros [a ?]; exists a; apply HP. Qed.
@@ -359,20 +359,20 @@ Proof.
Qed.
Lemma impl_elim P Q R : P ⊑ (Q → R) → P ⊑ Q → P ⊑ R.
Proof. by intros HP HP' x n ??; apply HP with x n, HP'. Qed.
-Lemma forall_intro {A} P (Q : A → uPred M): (∀ a, P ⊑ Q a) → P ⊑ (∀ a, Q a).
-Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
-Lemma forall_elim {A} {P : A → uPred M} a : (∀ a, P a) ⊑ P a.
+Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊑ Ψ a) → P ⊑ (∀ a, Ψ a).
+Proof. by intros HPΨ x n ?? a; apply HPΨ. Qed.
+Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊑ Ψ a.
Proof. intros x n ? HP; apply HP. Qed.
-Lemma exist_intro {A} {P : A → uPred M} a : P a ⊑ (∃ a, P a).
+Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊑ (∃ a, Ψ a).
Proof. by intros x n ??; exists a. Qed.
-Lemma exist_elim {A} (P : A → uPred M) Q : (∀ a, P a ⊑ Q) → (∃ a, P a) ⊑ Q.
-Proof. by intros HPQ x n ? [a ?]; apply HPQ with a. Qed.
+Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊑ Q) → (∃ a, Φ a) ⊑ Q.
+Proof. by intros HΦΨ x n ? [a ?]; apply HΦΨ with a. Qed.
Lemma eq_refl {A : cofeT} (a : A) P : P ⊑ (a ≡ a).
Proof. by intros x n ??; simpl. Qed.
-Lemma eq_rewrite {A : cofeT} a b (Q : A → uPred M) P
- `{HQ:∀ n, Proper (dist n ==> dist n) Q} : P ⊑ (a ≡ b) → P ⊑ Q a → P ⊑ Q b.
+Lemma eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P
+ `{HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : P ⊑ (a ≡ b) → P ⊑ Ψ a → P ⊑ Ψ b.
Proof.
- intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
+ intros Hab Ha x n ??; apply HΨ with n a; auto. by symmetry; apply Hab with x.
Qed.
Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
True ⊑ (a ≡ b) → a ≡ b.
@@ -392,7 +392,7 @@ Lemma or_intro_l' P Q R : P ⊑ Q → P ⊑ (Q ∨ R).
Proof. intros ->; apply or_intro_l. Qed.
Lemma or_intro_r' P Q R : P ⊑ R → P ⊑ (Q ∨ R).
Proof. intros ->; apply or_intro_r. Qed.
-Lemma exist_intro' {A} P (Q : A → uPred M) a : P ⊑ Q a → P ⊑ (∃ a, Q a).
+Lemma exist_intro' {A} P (Ψ : A → uPred M) a : P ⊑ Ψ a → P ⊑ (∃ a, Ψ a).
Proof. intros ->; apply exist_intro. Qed.
Hint Resolve or_elim or_intro_l' or_intro_r'.
@@ -451,14 +451,14 @@ Proof.
intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
apply impl_elim with P; eauto.
Qed.
-Lemma forall_mono {A} (P Q : A → uPred M) :
- (∀ a, P a ⊑ Q a) → (∀ a, P a) ⊑ (∀ a, Q a).
+Lemma forall_mono {A} (Φ Ψ : A → uPred M) :
+ (∀ a, Φ a ⊑ Ψ a) → (∀ a, Φ a) ⊑ (∀ a, Ψ a).
Proof.
intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
Qed.
-Lemma exist_mono {A} (P Q : A → uPred M) :
- (∀ a, P a ⊑ Q a) → (∃ a, P a) ⊑ (∃ a, Q a).
-Proof. intros HP. apply exist_elim=> a; rewrite (HP a); apply exist_intro. Qed.
+Lemma exist_mono {A} (Φ Ψ : A → uPred M) :
+ (∀ a, Φ a ⊑ Ψ a) → (∃ a, Φ a) ⊑ (∃ a, Ψ a).
+Proof. intros HΦ. apply exist_elim=> a; rewrite (HΦ a); apply exist_intro. Qed.
Global Instance const_mono' : Proper (impl ==> (⊑)) (@uPred_const M).
Proof. intros φ1 φ2; apply const_mono. Qed.
Global Instance and_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_and M).
@@ -532,7 +532,7 @@ Proof.
Qed.
Lemma and_or_r P Q R : ((P ∨ Q) ∧ R)%I ≡ (P ∧ R ∨ Q ∧ R)%I.
Proof. by rewrite -!(comm _ R) and_or_l. Qed.
-Lemma and_exist_l {A} P (Q : A → uPred M) : (P ∧ ∃ a, Q a)%I ≡ (∃ a, P ∧ Q a)%I.
+Lemma and_exist_l {A} P (Ψ : A → uPred M) : (P ∧ ∃ a, Ψ a)%I ≡ (∃ a, P ∧ Ψ a)%I.
Proof.
apply (anti_symm (⊑)).
- apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
@@ -540,10 +540,9 @@ Proof.
- apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
by rewrite -(exist_intro a) and_elim_r.
Qed.
-Lemma and_exist_r {A} P (Q : A → uPred M) : ((∃ a, Q a) ∧ P)%I ≡ (∃ a, Q a ∧ P)%I.
+Lemma and_exist_r {A} P (Φ: A → uPred M) : ((∃ a, Φ a) ∧ P)%I ≡ (∃ a, Φ a ∧ P)%I.
Proof.
- rewrite -(comm _ P) and_exist_l.
- apply exist_proper=>a. by rewrite comm.
+ rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
Qed.
(* BI connectives *)
@@ -652,18 +651,18 @@ Proof.
Qed.
Lemma sep_or_r P Q R : ((P ∨ Q) ★ R)%I ≡ ((P ★ R) ∨ (Q ★ R))%I.
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
-Lemma sep_exist_l {A} P (Q : A → uPred M) : (P ★ ∃ a, Q a)%I ≡ (∃ a, P ★ Q a)%I.
+Lemma sep_exist_l {A} P (Ψ : A → uPred M) : (P ★ ∃ a, Ψ a)%I ≡ (∃ a, P ★ Ψ a)%I.
Proof.
intros; apply (anti_symm (⊑)).
- apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
by rewrite -(exist_intro a).
- apply exist_elim=> a; apply sep_mono; auto using exist_intro.
Qed.
-Lemma sep_exist_r {A} (P: A → uPred M) Q: ((∃ a, P a) ★ Q)%I ≡ (∃ a, P a ★ Q)%I.
+Lemma sep_exist_r {A} (Φ: A → uPred M) Q: ((∃ a, Φ a) ★ Q)%I ≡ (∃ a, Φ a ★ Q)%I.
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
-Lemma sep_forall_l {A} P (Q : A → uPred M) : (P ★ ∀ a, Q a) ⊑ (∀ a, P ★ Q a).
+Lemma sep_forall_l {A} P (Ψ : A → uPred M) : (P ★ ∀ a, Ψ a) ⊑ (∀ a, P ★ Ψ a).
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
-Lemma sep_forall_r {A} (P : A → uPred M) Q : ((∀ a, P a) ★ Q) ⊑ (∀ a, P a ★ Q).
+Lemma sep_forall_r {A} (Φ : A → uPred M) Q : ((∀ a, Φ a) ★ Q) ⊑ (∀ a, Φ a ★ Q).
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
(* Later *)
@@ -685,12 +684,12 @@ Lemma later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I.
Proof. by intros x [|n]; split. Qed.
Lemma later_or P Q : (▷ (P ∨ Q))%I ≡ (▷ P ∨ ▷ Q)%I.
Proof. intros x [|n]; simpl; tauto. Qed.
-Lemma later_forall {A} (P : A → uPred M) : (▷ ∀ a, P a)%I ≡ (∀ a, ▷ P a)%I.
+Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a)%I ≡ (∀ a, ▷ Φ a)%I.
Proof. by intros x [|n]. Qed.
-Lemma later_exist_1 {A} (P : A → uPred M) : (∃ a, ▷ P a) ⊑ (▷ ∃ a, P a).
+Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊑ (▷ ∃ a, Φ a).
Proof. by intros x [|[|n]]. Qed.
-Lemma later_exist `{Inhabited A} (P : A → uPred M) :
- (▷ ∃ a, P a)%I ≡ (∃ a, ▷ P a)%I.
+Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
+ (▷ ∃ a, Φ a)%I ≡ (∃ a, ▷ Φ a)%I.
Proof. intros x [|[|n]]; split; done || by exists inhabitant; simpl. Qed.
Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
Proof.
@@ -718,10 +717,10 @@ Lemma later_wand P Q : ▷ (P -★ Q) ⊑ (▷ P -★ ▷ Q).
Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
Lemma later_iff P Q : (▷ (P ↔ Q)) ⊑ (▷P ↔ ▷Q).
Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
-Lemma löb_all_1 {A} (P Q : A → uPred M) :
- (∀ a, (▷(∀ b, P b → Q b) ∧ P a) ⊑ Q a) → ∀ a, P a ⊑ Q a.
+Lemma löb_all_1 {A} (Φ Ψ : A → uPred M) :
+ (∀ a, (▷ (∀ b, Φ b → Ψ b) ∧ Φ a) ⊑ Ψ a) → ∀ a, Φ a ⊑ Ψ a.
Proof.
- intros Hlöb a. apply impl_entails. transitivity (∀ a, P a → Q a)%I; last first.
+ intros Hlöb a. apply impl_entails. transitivity (∀ a, Φ a → Ψ a)%I; last first.
{ by rewrite (forall_elim a). } clear a.
etransitivity; last by eapply löb.
apply impl_intro_l, forall_intro=>a. rewrite right_id. by apply impl_intro_r.
@@ -744,9 +743,9 @@ Lemma always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
Proof. done. Qed.
Lemma always_or P Q : (□ (P ∨ Q))%I ≡ (□ P ∨ □ Q)%I.
Proof. done. Qed.
-Lemma always_forall {A} (P : A → uPred M) : (□ ∀ a, P a)%I ≡ (∀ a, □ P a)%I.
+Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a)%I ≡ (∀ a, □ Ψ a)%I.
Proof. done. Qed.
-Lemma always_exist {A} (P : A → uPred M) : (□ ∃ a, P a)%I ≡ (∃ a, □ P a)%I.
+Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a)%I ≡ (∃ a, □ Ψ a)%I.
Proof. done. Qed.
Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊑ □ (P ★ Q).
Proof.
@@ -898,14 +897,14 @@ Proof.
apply HP, HPQ, uPred_weaken with x' (S n');
eauto 3 using cmra_validN_le, cmra_validN_op_r.
Qed.
-Global Instance forall_timeless {A} (P : A → uPred M) :
- (∀ x, TimelessP (P x)) → TimelessP (∀ x, P x).
-Proof. by setoid_rewrite timelessP_spec=>HP x n ?? a; apply HP. Qed.
-Global Instance exist_timeless {A} (P : A → uPred M) :
- (∀ x, TimelessP (P x)) → TimelessP (∃ x, P x).
+Global Instance forall_timeless {A} (Ψ : A → uPred M) :
+ (∀ x, TimelessP (Ψ x)) → TimelessP (∀ x, Ψ x).
+Proof. by setoid_rewrite timelessP_spec=> HΨ x n ?? a; apply HΨ. Qed.
+Global Instance exist_timeless {A} (Ψ : A → uPred M) :
+ (∀ x, TimelessP (Ψ x)) → TimelessP (∃ x, Ψ x).
Proof.
- by setoid_rewrite timelessP_spec=>HP x [|n] ?;
- [|intros [a ?]; exists a; apply HP].
+ by setoid_rewrite timelessP_spec=> HΨ x [|n] ?;
+ [|intros [a ?]; exists a; apply HΨ].
Qed.
Global Instance always_timeless P : TimelessP P → TimelessP (□ P).
Proof.
@@ -940,11 +939,11 @@ 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} (P : A → uPred M) :
- (∀ x, AS (P x)) → AS (∀ x, P x).
+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} (P : A → uPred M) :
- (∀ x, AS (P x)) → AS (∃ x, P x).
+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.
@@ -954,8 +953,8 @@ Global Instance later_always_stable P : AS P → AS (▷ P).
Proof. by intros; rewrite /AlwaysStable always_later; apply later_mono. Qed.
Global Instance ownM_unit_always_stable (a : M) : AS (uPred_ownM (unit a)).
Proof. by rewrite /AlwaysStable always_ownM_unit. Qed.
-Global Instance default_always_stable {A} P (Q : A → uPred M) (mx : option A) :
- AS P → (∀ x, AS (Q x)) → AS (default P mx Q).
+Global Instance default_always_stable {A} P (Ψ : A → uPred M) (mx : option A) :
+ AS P → (∀ x, AS (Ψ x)) → AS (default P mx Ψ).
Proof. destruct mx; apply _. Qed.
(* Derived lemmas for always stable *)
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index 5c8f4f055a4b2310c7c052472819591e16a1efa4..ae1dea030d45f256c6859cd6b27ef16fe94f9834 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -16,17 +16,17 @@ Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
(** * Other big ops *)
(** We use a type class to obtain overloaded notations *)
Definition uPred_big_sepM {M} `{Countable K} {A}
- (m : gmap K A) (P : K → A → uPred M) : uPred M :=
- uPred_big_sep (curry P <$> map_to_list m).
+ (m : gmap K A) (Φ : K → A → uPred M) : uPred M :=
+ uPred_big_sep (curry Φ <$> map_to_list m).
Instance: Params (@uPred_big_sepM) 6.
-Notation "'Π★{map' m } P" := (uPred_big_sepM m P)
- (at level 20, m at level 10, format "Π★{map m } P") : uPred_scope.
+Notation "'Π★{map' m } Φ" := (uPred_big_sepM m Φ)
+ (at level 20, m at level 10, format "Π★{map m } Φ") : uPred_scope.
Definition uPred_big_sepS {M} `{Countable A}
- (X : gset A) (P : A → uPred M) : uPred M := uPred_big_sep (P <$> elements X).
+ (X : gset A) (Φ : A → uPred M) : uPred M := uPred_big_sep (Φ <$> elements X).
Instance: Params (@uPred_big_sepS) 5.
-Notation "'Π★{set' X } P" := (uPred_big_sepS X P)
- (at level 20, X at level 10, format "Π★{set X } P") : uPred_scope.
+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)) :=
@@ -97,56 +97,56 @@ Proof. induction 1; simpl; auto with I. Qed.
Section gmap.
Context `{Countable K} {A : Type}.
Implicit Types m : gmap K A.
- Implicit Types P : K → A → uPred M.
+ Implicit Types Φ Ψ : K → A → uPred M.
- Lemma big_sepM_mono P Q m1 m2 :
- m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → P k x ⊑ Q k x) →
- (Π★{map m1} P) ⊑ (Π★{map m2} Q).
+ Lemma big_sepM_mono Φ Ψ m1 m2 :
+ m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊑ Ψ k x) →
+ (Π★{map m1} Φ) ⊑ (Π★{map m2} Ψ).
Proof.
- intros HX HP. transitivity (Π★{map m2} P)%I.
+ intros HX HΦ. transitivity (Π★{map m2} Φ)%I.
- by apply big_sep_contains, fmap_contains, map_to_list_contains.
- apply big_sep_mono', Forall2_fmap, Forall2_Forall.
- apply Forall_forall=> -[i x] ? /=. by apply HP, elem_of_map_to_list.
+ apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
Qed.
Global Instance big_sepM_ne m n :
Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
(uPred_big_sepM (M:=M) m).
Proof.
- intros P1 P2 HP. apply big_sep_ne, Forall2_fmap.
- apply Forall2_Forall, Forall_true=> -[i x]; apply HP.
+ intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
+ apply Forall2_Forall, Forall_true=> -[i x]; apply HΦ.
Qed.
Global Instance big_sepM_proper m :
Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡))
(uPred_big_sepM (M:=M) m).
Proof.
- intros P1 P2 HP; apply equiv_dist=> n.
- apply big_sepM_ne=> k x; apply equiv_dist, HP.
+ intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
+ apply big_sepM_ne=> k x; apply equiv_dist, HΦ.
Qed.
Global Instance big_sepM_mono' m :
Proper (pointwise_relation _ (pointwise_relation _ (⊑)) ==> (⊑))
(uPred_big_sepM (M:=M) m).
- Proof. intros P1 P2 HP. apply big_sepM_mono; intros; [done|apply HP]. Qed.
+ Proof. intros Φ1 Φ2 HΦ. apply big_sepM_mono; intros; [done|apply HΦ]. Qed.
- Lemma big_sepM_empty P : (Π★{map ∅} P)%I ≡ True%I.
+ Lemma big_sepM_empty Φ : (Π★{map ∅} Φ)%I ≡ True%I.
Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
- Lemma big_sepM_insert P (m : gmap K A) i x :
- m !! i = None → (Π★{map <[i:=x]> m} P)%I ≡ (P i x ★ Π★{map m} P)%I.
+ Lemma big_sepM_insert Φ (m : gmap K A) i x :
+ m !! i = None → (Π★{map <[i:=x]> m} Φ)%I ≡ (Φ i x ★ Π★{map m} Φ)%I.
Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
- Lemma big_sepM_singleton P i x : (Π★{map {[i := x]}} P)%I ≡ (P i x)%I.
+ Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ)%I ≡ (Φ i x)%I.
Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
by rewrite big_sepM_empty right_id.
Qed.
- Lemma big_sepM_sepM P Q m :
- (Π★{map m} (λ i x, P i x ★ Q i x))%I ≡ (Π★{map m} P ★ Π★{map m} Q)%I.
+ Lemma big_sepM_sepM Φ Ψ m :
+ (Π★{map m} (λ i x, Φ i x ★ Ψ i x))%I ≡ (Π★{map m} Φ ★ Π★{map m} Ψ)%I.
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
- by rewrite IH -!assoc (assoc _ (Q _ _)) [(Q _ _ ★ _)%I]comm -!assoc.
+ by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc.
Qed.
- Lemma big_sepM_later P m : (▷ Π★{map m} P)%I ≡ (Π★{map m} (λ i x, ▷ P i x))%I.
+ Lemma big_sepM_later Φ m : (▷ Π★{map m} Φ)%I ≡ (Π★{map m} (λ i x, ▷ Φ i x))%I.
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
@@ -158,56 +158,56 @@ End gmap.
Section gset.
Context `{Countable A}.
Implicit Types X : gset A.
- Implicit Types P : A → uPred M.
+ Implicit Types Φ : A → uPred M.
- Lemma big_sepS_mono P Q X Y :
- Y ⊆ X → (∀ x, x ∈ Y → P x ⊑ Q x) → (Π★{set X} P) ⊑ (Π★{set Y} Q).
+ Lemma big_sepS_mono Φ Ψ X Y :
+ Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊑ Ψ x) → (Π★{set X} Φ) ⊑ (Π★{set Y} Ψ).
Proof.
- intros HX HP. transitivity (Π★{set Y} P)%I.
+ intros HX HΦ. transitivity (Π★{set Y} Φ)%I.
- by apply big_sep_contains, fmap_contains, elements_contains.
- apply big_sep_mono', Forall2_fmap, Forall2_Forall.
- apply Forall_forall=> x ? /=. by apply HP, elem_of_elements.
+ apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
Qed.
Lemma big_sepS_ne X n :
Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
Proof.
- intros P1 P2 HP. apply big_sep_ne, Forall2_fmap.
- apply Forall2_Forall, Forall_true=> x; apply HP.
+ intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
+ apply Forall2_Forall, Forall_true=> x; apply HΦ.
Qed.
Lemma big_sepS_proper X :
Proper (pointwise_relation _ (≡) ==> (≡)) (uPred_big_sepS (M:=M) X).
Proof.
- intros P1 P2 HP; apply equiv_dist=> n.
- apply big_sepS_ne=> x; apply equiv_dist, HP.
+ intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
+ apply big_sepS_ne=> x; apply equiv_dist, HΦ.
Qed.
Lemma big_sepS_mono' X :
Proper (pointwise_relation _ (⊑) ==> (⊑)) (uPred_big_sepS (M:=M) X).
- Proof. intros P1 P2 HP. apply big_sepS_mono; naive_solver. Qed.
+ Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
- Lemma big_sepS_empty P : (Π★{set ∅} P)%I ≡ True%I.
+ Lemma big_sepS_empty Φ : (Π★{set ∅} Φ)%I ≡ True%I.
Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
- Lemma big_sepS_insert P X x :
- x ∉ X → (Π★{set {[ x ]} ∪ X} P)%I ≡ (P x ★ Π★{set X} P)%I.
+ Lemma big_sepS_insert Φ X x :
+ x ∉ X → (Π★{set {[ x ]} ∪ X} Φ)%I ≡ (Φ x ★ Π★{set X} Φ)%I.
Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
- Lemma big_sepS_delete P X x :
- x ∈ X → (Π★{set X} P)%I ≡ (P x ★ Π★{set X ∖ {[ x ]}} P)%I.
+ Lemma big_sepS_delete Φ X x :
+ x ∈ X → (Π★{set X} Φ)%I ≡ (Φ x ★ Π★{set X ∖ {[ x ]}} Φ)%I.
Proof.
intros. rewrite -big_sepS_insert; last set_solver.
by rewrite -union_difference_L; last set_solver.
Qed.
- Lemma big_sepS_singleton P x : (Π★{set {[ x ]}} P)%I ≡ (P x)%I.
+ Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ)%I ≡ (Φ x)%I.
Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
- Lemma big_sepS_sepS P Q X :
- (Π★{set X} (λ x, P x ★ Q x))%I ≡ (Π★{set X} P ★ Π★{set X} Q)%I.
+ Lemma big_sepS_sepS Φ Ψ X :
+ (Π★{set X} (λ x, Φ x ★ Ψ x))%I ≡ (Π★{set X} Φ ★ Π★{set X} Ψ)%I.
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
- by rewrite IH -!assoc (assoc _ (Q _)) [(Q _ ★ _)%I]comm -!assoc.
+ by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc.
Qed.
- Lemma big_sepS_later P X : (▷ Π★{set X} P)%I ≡ (Π★{set X} (λ x, ▷ P x))%I.
+ Lemma big_sepS_later Φ X : (▷ Π★{set X} Φ)%I ≡ (Π★{set X} (λ x, ▷ Φ x))%I.
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
diff --git a/barrier/barrier.v b/barrier/barrier.v
index 7369e888b08314491b176581337914651c770240..04029b444cf6ee36c43b6e0cf4099db5098c1c2a 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -123,12 +123,12 @@ Section proof.
(∃ γ, barrier_ctx γ l P ★ sts_ownS γ low_states {[ Send ]})%I.
Definition recv (l : loc) (R : iProp) : iProp :=
- (∃ γ (P Q : iProp) i, barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★
+ (∃ γ P Q i, barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★
saved_prop_own i Q ★ ▷(Q -★ R))%I.
- Lemma newchan_spec (P : iProp) (Q : val → iProp) :
- (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Q (LocV l))
- ⊑ wp ⊤ (newchan '()) Q.
+ Lemma newchan_spec (P : iProp) (Φ : val → iProp) :
+ (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (LocV l))
+ ⊑ wp ⊤ (newchan '()) Φ.
Proof.
rewrite /newchan. wp_rec. (* TODO: wp_seq. *)
rewrite -wp_pvs. wp> eapply wp_alloc; eauto with I ndisj.
@@ -177,8 +177,8 @@ Section proof.
rewrite !mkSet_elem_of /=. set_solver.
Qed.
- Lemma signal_spec l P (Q : val → iProp) :
- heapN ⊥ N → (send l P ★ P ★ Q '()) ⊑ wp ⊤ (signal (LocV l)) Q.
+ Lemma signal_spec l P (Φ : val → iProp) :
+ heapN ⊥ N → (send l P ★ P ★ Φ '()) ⊑ wp ⊤ (signal (LocV l)) Φ.
Proof.
intros Hdisj. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
@@ -201,19 +201,19 @@ Section proof.
apply sep_mono; last first.
{ apply wand_intro_l. eauto with I. }
(* Now we come to the core of the proof: Updating from waiting to ress. *)
- rewrite /waiting /ress sep_exist_l. apply exist_elim=>{Q} Q.
+ rewrite /waiting /ress sep_exist_l. apply exist_elim=>{Φ} Φ.
rewrite later_wand {1}(later_intro P) !assoc wand_elim_r.
rewrite big_sepS_later -big_sepS_sepS. apply big_sepS_mono'=>i.
- rewrite -(exist_intro (Q i)) comm. done.
+ rewrite -(exist_intro (Φ i)) comm. done.
Qed.
- Lemma wait_spec l P (Q : val → iProp) :
- heapN ⊥ N → (recv l P ★ (P -★ Q '())) ⊑ wp ⊤ (wait (LocV l)) Q.
+ Lemma wait_spec l P (Φ : val → iProp) :
+ heapN ⊥ N → (recv l P ★ (P -★ Φ '())) ⊑ wp ⊤ (wait (LocV l)) Φ.
Proof.
Abort.
- Lemma split_spec l P1 P2 Q :
- (recv l (P1 ★ P2) ★ (recv l P1 ★ recv l P2 -★ Q '())) ⊑ wp ⊤ Skip Q.
+ Lemma split_spec l P1 P2 Φ :
+ (recv l (P1 ★ P2) ★ (recv l P1 ★ recv l P2 -★ Φ '())) ⊑ wp ⊤ Skip Φ.
Proof.
Abort.
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index b834c31faf8d7f78bc3420125b000aa2e1e45312..202e9f9734ed1982903e81b47b2146072847035f 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -12,49 +12,49 @@ Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Section derived.
Context {Σ : iFunctor}.
-Implicit Types P : iProp heap_lang Σ.
-Implicit Types Q : val → iProp heap_lang Σ.
+Implicit Types P Q : iProp heap_lang Σ.
+Implicit Types Φ : val → iProp heap_lang Σ.
(** Proof rules for the sugar *)
-Lemma wp_lam' E x ef e v Q :
- to_val e = Some v → ▷ wp E (subst ef x v) Q ⊑ wp E (App (Lam x ef) e) Q.
+Lemma wp_lam' E x ef e v Φ :
+ to_val e = Some v → ▷ wp E (subst ef x v) Φ ⊑ wp E (App (Lam x ef) e) Φ.
Proof. intros. by rewrite -wp_rec' ?subst_empty. Qed.
-Lemma wp_let' E x e1 e2 v Q :
- to_val e1 = Some v → ▷ wp E (subst e2 x v) Q ⊑ wp E (Let x e1 e2) Q.
+Lemma wp_let' E x e1 e2 v Φ :
+ to_val e1 = Some v → ▷ wp E (subst e2 x v) Φ ⊑ wp E (Let x e1 e2) Φ.
Proof. apply wp_lam'. Qed.
-Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, ▷ wp E e2 Q) ⊑ wp E (Seq e1 e2) Q.
+Lemma wp_seq E e1 e2 Φ : wp E e1 (λ _, ▷ wp E e2 Φ) ⊑ wp E (Seq e1 e2) Φ.
Proof.
rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
by rewrite -wp_let' //= ?to_of_val ?subst_empty.
Qed.
-Lemma wp_skip E Q : ▷ (Q (LitV LitUnit)) ⊑ wp E Skip Q.
+Lemma wp_skip E Φ : ▷ (Φ (LitV LitUnit)) ⊑ wp E Skip Φ.
Proof. rewrite -wp_seq -wp_value // -wp_value //. Qed.
-Lemma wp_le E (n1 n2 : Z) P Q :
- (n1 ≤ n2 → P ⊑ ▷ Q (LitV $ LitBool true)) →
- (n2 < n1 → P ⊑ ▷ Q (LitV $ LitBool false)) →
- P ⊑ wp E (BinOp LeOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Q.
+Lemma wp_le E (n1 n2 : Z) P Φ :
+ (n1 ≤ n2 → P ⊑ ▷ Φ (LitV $ LitBool true)) →
+ (n2 < n1 → P ⊑ ▷ Φ (LitV $ LitBool false)) →
+ P ⊑ wp E (BinOp LeOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
Qed.
-Lemma wp_lt E (n1 n2 : Z) P Q :
- (n1 < n2 → P ⊑ ▷ Q (LitV $ LitBool true)) →
- (n2 ≤ n1 → P ⊑ ▷ Q (LitV $ LitBool false)) →
- P ⊑ wp E (BinOp LtOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Q.
+Lemma wp_lt E (n1 n2 : Z) P Φ :
+ (n1 < n2 → P ⊑ ▷ Φ (LitV $ LitBool true)) →
+ (n2 ≤ n1 → P ⊑ ▷ Φ (LitV $ LitBool false)) →
+ P ⊑ wp E (BinOp LtOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
Qed.
-Lemma wp_eq E (n1 n2 : Z) P Q :
- (n1 = n2 → P ⊑ ▷ Q (LitV $ LitBool true)) →
- (n1 ≠n2 → P ⊑ ▷ Q (LitV $ LitBool false)) →
- P ⊑ wp E (BinOp EqOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Q.
+Lemma wp_eq E (n1 n2 : Z) P Φ :
+ (n1 = n2 → P ⊑ ▷ Φ (LitV $ LitBool true)) →
+ (n1 ≠n2 → P ⊑ ▷ Φ (LitV $ LitBool false)) →
+ P ⊑ wp E (BinOp EqOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index ad9c649ac3020523a482eca26ee8c11c6731bf24..e52dadfd4d900cf043bf87eb83eaad241a990cc8 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -31,7 +31,8 @@ Notation "l ↦ v" := (heap_mapsto l v) (at level 20) : uPred_scope.
Section heap.
Context {Σ : iFunctorG}.
Implicit Types N : namespace.
- Implicit Types P : iPropG heap_lang Σ.
+ Implicit Types P Q : iPropG heap_lang Σ.
+ Implicit Types Φ : val → iPropG heap_lang Σ.
Implicit Types σ : state.
Implicit Types h g : heapRA.
@@ -95,11 +96,11 @@ Section heap.
Qed.
(** Weakest precondition *)
- Lemma wp_alloc N E e v P Q :
+ Lemma wp_alloc N E e v P Φ :
to_val e = Some v → nclose N ⊆ E →
P ⊑ heap_ctx N →
- P ⊑ (▷ ∀ l, l ↦ v -★ Q (LocV l)) →
- P ⊑ wp E (Alloc e) Q.
+ P ⊑ (▷ ∀ l, l ↦ v -★ Φ (LocV l)) →
+ P ⊑ wp E (Alloc e) Φ.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
transitivity (pvs E E (auth_own heap_name ∅ ★ P))%I.
@@ -122,16 +123,16 @@ Section heap.
apply later_intro.
Qed.
- Lemma wp_load N E l v P Q :
+ Lemma wp_load N E l v P Φ :
nclose N ⊆ E →
P ⊑ heap_ctx N →
- P ⊑ (▷ l ↦ v ★ ▷ (l ↦ v -★ Q v)) →
- P ⊑ wp E (Load (Loc l)) Q.
+ P ⊑ (▷ l ↦ v ★ ▷ (l ↦ v -★ Φ v)) →
+ P ⊑ wp E (Load (Loc l)) Φ.
Proof.
- rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPQ.
+ rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Excl v ]}; simpl; eauto with I.
- rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
+ rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
@@ -141,16 +142,16 @@ Section heap.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Qed.
- Lemma wp_store N E l v' e v P Q :
+ Lemma wp_store N E l v' e v P Φ :
to_val e = Some v → nclose N ⊆ E →
P ⊑ heap_ctx N →
- P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Q (LitV LitUnit))) →
- P ⊑ wp E (Store (Loc l) e) Q.
+ P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))) →
+ P ⊑ wp E (Store (Loc l) e) Φ.
Proof.
- rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPQ.
+ rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
with N heap_name {[ l := Excl v' ]}; simpl; eauto with I.
- rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
+ rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
@@ -161,17 +162,17 @@ Section heap.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
Qed.
- Lemma wp_cas_fail N E l v' e1 v1 e2 v2 P Q :
+ Lemma wp_cas_fail N E l v' e1 v1 e2 v2 P Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠v1 →
nclose N ⊆ E →
P ⊑ heap_ctx N →
- P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v' -★ Q (LitV (LitBool false)))) →
- P ⊑ wp E (Cas (Loc l) e1 e2) Q.
+ P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v' -★ Φ (LitV (LitBool false)))) →
+ P ⊑ wp E (Cas (Loc l) e1 e2) Φ.
Proof.
- rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPQ.
+ rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Excl v' ]}; simpl; eauto 10 with I.
- rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
+ rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
@@ -181,17 +182,17 @@ Section heap.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Qed.
- Lemma wp_cas_suc N E l e1 v1 e2 v2 P Q :
+ Lemma wp_cas_suc N E l e1 v1 e2 v2 P Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
nclose N ⊆ E →
P ⊑ heap_ctx N →
- P ⊑ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Q (LitV (LitBool true)))) →
- P ⊑ wp E (Cas (Loc l) e1 e2) Q.
+ P ⊑ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))) →
+ P ⊑ wp E (Cas (Loc l) e1 e2) Φ.
Proof.
- rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPQ.
+ rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
with N heap_name {[ l := Excl v1 ]}; simpl; eauto 10 with I.
- rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
+ rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) ?lookup_insert //.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index e716714dbf46c31159621b3bd72931593c3c6d8b..4fd62284b40503dc397b6ee0eb2818d6188dbb5a 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -9,25 +9,25 @@ Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
Section lifting.
Context {Σ : iFunctor}.
-Implicit Types P : iProp heap_lang Σ.
-Implicit Types Q : val → iProp heap_lang Σ.
+Implicit Types P Q : iProp heap_lang Σ.
+Implicit Types Φ : val → iProp heap_lang Σ.
Implicit Types K : ectx.
Implicit Types ef : option expr.
(** Bind. *)
-Lemma wp_bind {E e} K Q :
- wp E e (λ v, wp E (fill K (of_val v)) Q) ⊑ wp E (fill K e) Q.
+Lemma wp_bind {E e} K Φ :
+ wp E e (λ v, wp E (fill K (of_val v)) Φ) ⊑ wp E (fill K e) Φ.
Proof. apply weakestpre.wp_bind. Qed.
-Lemma wp_bindi {E e} Ki Q :
- wp E e (λ v, wp E (fill_item Ki (of_val v)) Q) ⊑ wp E (fill_item Ki e) Q.
+Lemma wp_bindi {E e} Ki Φ :
+ wp E e (λ v, wp E (fill_item Ki (of_val v)) Φ) ⊑ wp E (fill_item Ki e) Φ.
Proof. apply weakestpre.wp_bind. Qed.
(** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ e v Q :
+Lemma wp_alloc_pst E σ e v Φ :
to_val e = Some v →
- (ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
- ⊑ wp E (Alloc e) Q.
+ (ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l)))
+ ⊑ wp E (Alloc e) Φ.
Proof.
(* TODO RJ: This works around ssreflect bug #22. *)
intros. set (φ v' σ' ef := ∃ l,
@@ -42,42 +42,42 @@ Proof.
by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
Qed.
-Lemma wp_load_pst E σ l v Q :
+Lemma wp_load_pst E σ l v Φ :
σ !! l = Some v →
- (ownP σ ★ ▷ (ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
+ (ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊑ wp E (Load (Loc l)) Φ.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
last by intros; inv_step; eauto using to_of_val.
Qed.
-Lemma wp_store_pst E σ l e v v' Q :
+Lemma wp_store_pst E σ l e v v' Φ :
to_val e = Some v → σ !! l = Some v' →
- (ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Q (LitV LitUnit))) ⊑ wp E (Store (Loc l) e) Q.
+ (ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Φ (LitV LitUnit))) ⊑ wp E (Store (Loc l) e) Φ.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None)
?right_id //; last by intros; inv_step; eauto.
Qed.
-Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
+Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠v1 →
- (ownP σ ★ ▷ (ownP σ -★ Q (LitV $ LitBool false))) ⊑ wp E (Cas (Loc l) e1 e2) Q.
+ (ownP σ ★ ▷ (ownP σ -★ Φ (LitV $ LitBool false))) ⊑ wp E (Cas (Loc l) e1 e2) Φ.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None)
?right_id //; last by intros; inv_step; eauto.
Qed.
-Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
+Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
- (ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Q (LitV $ LitBool true)))
- ⊑ wp E (Cas (Loc l) e1 e2) Q.
+ (ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Φ (LitV $ LitBool true)))
+ ⊑ wp E (Cas (Loc l) e1 e2) Φ.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true) (<[l:=v2]>σ) None)
?right_id //; last by intros; inv_step; eauto.
Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork E e Q :
- (▷ Q (LitV LitUnit) ★ ▷ wp (Σ:=Σ) ⊤ e (λ _, True)) ⊑ wp E (Fork e) Q.
+Lemma wp_fork E e Φ :
+ (▷ Φ (LitV LitUnit) ★ ▷ wp (Σ:=Σ) ⊤ e (λ _, True)) ⊑ wp E (Fork e) Φ.
Proof.
rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
last by intros; inv_step; eauto.
@@ -86,70 +86,72 @@ Qed.
(* For the lemmas involving substitution, we only derive a preliminary version.
The final version is defined in substitution.v. *)
-Lemma wp_rec' E f x e1 e2 v Q :
+Lemma wp_rec' E f x e1 e2 v Φ :
to_val e2 = Some v →
- ▷ wp E (subst (subst e1 f (RecV f x e1)) x v) Q ⊑ wp E (App (Rec f x e1) e2) Q.
+ ▷ wp E (subst (subst e1 f (RecV f x e1)) x v) Φ ⊑ wp E (App (Rec f x e1) e2) Φ.
Proof.
intros. rewrite -(wp_lift_pure_det_step (App _ _)
(subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
intros; inv_step; eauto.
Qed.
-Lemma wp_un_op E op l l' Q :
+Lemma wp_un_op E op l l' Φ :
un_op_eval op l = Some l' →
- ▷ Q (LitV l') ⊑ wp E (UnOp op (Lit l)) Q.
+ ▷ Φ (LitV l') ⊑ wp E (UnOp op (Lit l)) Φ.
Proof.
intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
?right_id -?wp_value //; intros; inv_step; eauto.
Qed.
-Lemma wp_bin_op E op l1 l2 l' Q :
+Lemma wp_bin_op E op l1 l2 l' Φ :
bin_op_eval op l1 l2 = Some l' →
- ▷ Q (LitV l') ⊑ wp E (BinOp op (Lit l1) (Lit l2)) Q.
+ ▷ Φ (LitV l') ⊑ wp E (BinOp op (Lit l1) (Lit l2)) Φ.
Proof.
intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
?right_id -?wp_value //; intros; inv_step; eauto.
Qed.
-Lemma wp_if_true E e1 e2 Q : ▷ wp E e1 Q ⊑ wp E (If (Lit $ LitBool true) e1 e2) Q.
+Lemma wp_if_true E e1 e2 Φ :
+ ▷ wp E e1 Φ ⊑ wp E (If (Lit $ LitBool true) e1 e2) Φ.
Proof.
rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
?right_id //; intros; inv_step; eauto.
Qed.
-Lemma wp_if_false E e1 e2 Q : ▷ wp E e2 Q ⊑ wp E (If (Lit $ LitBool false) e1 e2) Q.
+Lemma wp_if_false E e1 e2 Φ :
+ ▷ wp E e2 Φ ⊑ wp E (If (Lit $ LitBool false) e1 e2) Φ.
Proof.
rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
?right_id //; intros; inv_step; eauto.
Qed.
-Lemma wp_fst E e1 v1 e2 v2 Q :
+Lemma wp_fst E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- ▷ Q v1 ⊑ wp E (Fst $ Pair e1 e2) Q.
+ ▷ Φ v1 ⊑ wp E (Fst $ Pair e1 e2) Φ.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
?right_id -?wp_value //; intros; inv_step; eauto.
Qed.
-Lemma wp_snd E e1 v1 e2 v2 Q :
+Lemma wp_snd E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- ▷ Q v2 ⊑ wp E (Snd $ Pair e1 e2) Q.
+ ▷ Φ v2 ⊑ wp E (Snd $ Pair e1 e2) Φ.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
?right_id -?wp_value //; intros; inv_step; eauto.
Qed.
-Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Q :
+Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0 →
- ▷ wp E (subst e1 x1 v0) Q ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Q.
+ ▷ wp E (subst e1 x1 v0) Φ ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Φ.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
(subst e1 x1 v0) None) ?right_id //; intros; inv_step; eauto.
Qed.
-Lemma wp_case_inr' E e0 v0 x1 e1 x2 e2 Q :
+Lemma wp_case_inr' E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0 →
- ▷ wp E (subst e2 x2 v0) Q ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Q.
+ ▷ wp E (subst e2 x2 v0) Φ ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Φ.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
(subst e2 x2 v0) None) ?right_id //; intros; inv_step; eauto.
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index 666040d211950ee88db7014bc82c5f590bdcdebd..4ea9afc6f887d71810032b7d714fb24807a57792 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -116,36 +116,36 @@ Qed.
(** * Weakest precondition rules *)
Section wp.
Context {Σ : iFunctor}.
-Implicit Types P : iProp heap_lang Σ.
-Implicit Types Q : val → iProp heap_lang Σ.
+Implicit Types P Q : iProp heap_lang Σ.
+Implicit Types Φ : val → iProp heap_lang Σ.
Hint Resolve to_of_val.
-Lemma wp_rec E e1 f x erec e2 v Q :
+Lemma wp_rec E e1 f x erec e2 v Φ :
e1 = Rec f x erec →
to_val e2 = Some v →
- ▷ wp E (gsubst (gsubst erec f e1) x e2) Q ⊑ wp E (App e1 e2) Q.
+ ▷ wp E (gsubst (gsubst erec f e1) x e2) Φ ⊑ wp E (App e1 e2) Φ.
Proof.
intros -> <-%of_to_val.
rewrite (gsubst_correct _ _ (RecV _ _ _)) gsubst_correct.
by apply wp_rec'.
Qed.
-Lemma wp_lam E x ef e v Q :
- to_val e = Some v → ▷ wp E (gsubst ef x e) Q ⊑ wp E (App (Lam x ef) e) Q.
+Lemma wp_lam E x ef e v Φ :
+ to_val e = Some v → ▷ wp E (gsubst ef x e) Φ ⊑ wp E (App (Lam x ef) e) Φ.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_lam'. Qed.
-Lemma wp_let E x e1 e2 v Q :
- to_val e1 = Some v → ▷ wp E (gsubst e2 x e1) Q ⊑ wp E (Let x e1 e2) Q.
+Lemma wp_let E x e1 e2 v Φ :
+ to_val e1 = Some v → ▷ wp E (gsubst e2 x e1) Φ ⊑ wp E (Let x e1 e2) Φ.
Proof. apply wp_lam. Qed.
-Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Q :
+Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0 →
- ▷ wp E (gsubst e1 x1 e0) Q ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Q.
+ ▷ wp E (gsubst e1 x1 e0) Φ ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Φ.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inl'. Qed.
-Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Q :
+Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0 →
- ▷ wp E (gsubst e2 x2 e0) Q ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Q.
+ ▷ wp E (gsubst e2 x2 e0) Φ ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Φ.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inr'. Qed.
End wp.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index f6558404b8e79dbde5e27ee942cfac1513938ec9..76fc530c8c18056756a65259981ed6d849ceafdd 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -24,9 +24,8 @@ End LangTests.
Section LiftingTests.
Context `{heapG Σ}.
Local Notation iProp := (iPropG heap_lang Σ).
-
- Implicit Types P : iProp.
- Implicit Types Q : val → iProp.
+ Implicit Types P Q : iPropG heap_lang Σ.
+ Implicit Types Φ : val → iPropG heap_lang Σ.
Definition heap_e : expr :=
let: "x" := ref '1 in "x" <- !"x" + '1;; !"x".
@@ -48,22 +47,22 @@ Section LiftingTests.
λ: "x",
if: "x" ≤ '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.
- Lemma FindPred_spec n1 n2 E Q :
- (■(n1 < n2) ∧ Q '(n2 - 1)) ⊑ wp E (FindPred 'n2 'n1) Q.
+ Lemma FindPred_spec n1 n2 E Φ :
+ (■(n1 < n2) ∧ Φ '(n2 - 1)) ⊑ wp E (FindPred 'n2 'n1) Φ.
Proof.
revert n1; apply löb_all_1=>n1.
rewrite (comm uPred_and (â– _)%I) assoc; apply const_elim_r=>?.
(* first need to do the rec to get a later *)
wp_rec>.
(* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
- rewrite ->(later_intro (Q _)); rewrite -!later_and; apply later_mono.
+ rewrite ->(later_intro (Φ _)); rewrite -!later_and; apply later_mono.
wp_rec. wp_bin_op. wp_rec. wp_bin_op=> ?; wp_if.
- rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
by rewrite left_id impl_elim_l.
- wp_value. assert (n1 = n2 - 1) as -> by omega; auto with I.
Qed.
- Lemma Pred_spec n E Q : ▷ Q (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Q.
+ Lemma Pred_spec n E Φ : ▷ Φ (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Φ.
Proof.
wp_rec>; apply later_mono; wp_bin_op=> ?; wp_if.
- wp_un_op. wp_bin_op.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 4453110f5db418f719aab178e0b8b63804763363..886b66dc4210a8fbd0dd85697b8d042e9f36ddef 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -10,64 +10,66 @@ Local Hint Extern 10 (✓{_} _) =>
Section adequacy.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types e : expr Λ.
-Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types P Q : iProp Λ Σ.
+Implicit Types Φ : val Λ → iProp Λ Σ.
+Implicit Types Φs : list (val Λ → iProp Λ Σ).
Implicit Types m : iGst Λ Σ.
Transparent uPred_holds.
-Notation wptp n := (Forall3 (λ e Q r, uPred_holds (wp ⊤ e Q) n r)).
-Lemma wptp_le Qs es rs n n' :
- ✓{n'} (big_op rs) → wptp n es Qs rs → n' ≤ n → wptp n' es Qs rs.
+Notation wptp n := (Forall3 (λ e Φ r, uPred_holds (wp ⊤ e Φ) n r)).
+Lemma wptp_le Φs es rs n n' :
+ ✓{n'} (big_op rs) → wptp n es Φs rs → n' ≤ n → wptp n' es Φs rs.
Proof. induction 2; constructor; eauto using uPred_weaken. Qed.
-Lemma nsteps_wptp Qs k n tσ1 tσ2 rs1 :
+Lemma nsteps_wptp Φs k n tσ1 tσ2 rs1 :
nsteps step k tσ1 tσ2 →
- 1 < n → wptp (k + n) (tσ1.1) Qs rs1 →
+ 1 < n → wptp (k + n) (tσ1.1) Φs rs1 →
wsat (k + n) ⊤ (tσ1.2) (big_op rs1) →
- ∃ rs2 Qs', wptp n (tσ2.1) (Qs ++ Qs') rs2 ∧ wsat n ⊤ (tσ2.2) (big_op rs2).
+ ∃ rs2 Φs', wptp n (tσ2.1) (Φs ++ Φs') rs2 ∧ wsat n ⊤ (tσ2.2) (big_op rs2).
Proof.
- intros Hsteps Hn; revert Qs rs1.
+ intros Hsteps Hn; revert Φs rs1.
induction Hsteps as [|k ?? tσ3 [e1 σ1 e2 σ2 ef t1 t2 ?? Hstep] Hsteps IH];
- simplify_eq/=; intros Qs rs.
+ simplify_eq/=; intros Φs rs.
{ by intros; exists rs, []; rewrite right_id_L. }
- intros (Qs1&?&rs1&?&->&->&?&
- (Q&Qs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?.
- destruct (wp_step_inv ⊤ ∅ Q e1 (k + n) (S (k + n)) σ1 r
+ intros (Φs1&?&rs1&?&->&->&?&
+ (Φ&Φs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?.
+ destruct (wp_step_inv ⊤ ∅ Φ e1 (k + n) (S (k + n)) σ1 r
(big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using values_stuck.
{ by rewrite right_id_L -big_op_cons Permutation_middle. }
destruct (Hwpstep e2 σ2 ef) as (r2&r2'&Hwsat&?&?); auto; clear Hwpstep.
revert Hwsat; rewrite big_op_app right_id_L=>Hwsat.
destruct ef as [e'|].
- - destruct (IH (Qs1 ++ Q :: Qs2 ++ [λ _, True%I])
- (rs1 ++ r2 :: rs2 ++ [r2'])) as (rs'&Qs'&?&?).
+ - destruct (IH (Φs1 ++ Φ :: Φs2 ++ [λ _, True%I])
+ (rs1 ++ r2 :: rs2 ++ [r2'])) as (rs'&Φs'&?&?).
{ apply Forall3_app, Forall3_cons,
Forall3_app, Forall3_cons, Forall3_nil; eauto using wptp_le. }
{ by rewrite -Permutation_middle /= (assoc (++))
(comm (++)) /= assoc big_op_app. }
- exists rs', ([λ _, True%I] ++ Qs'); split; auto.
- by rewrite (assoc _ _ _ Qs') -(assoc _ Qs1).
- - apply (IH (Qs1 ++ Q :: Qs2) (rs1 ++ r2 â‹… r2' :: rs2)).
+ exists rs', ([λ _, True%I] ++ Φs'); split; auto.
+ by rewrite (assoc _ _ _ Φs') -(assoc _ Φs1).
+ - apply (IH (Φs1 ++ Φ :: Φs2) (rs1 ++ r2 ⋅ r2' :: rs2)).
{ rewrite /option_list right_id_L.
apply Forall3_app, Forall3_cons; eauto using wptp_le.
apply uPred_weaken with r2 (k + n); eauto using cmra_included_l. }
by rewrite -Permutation_middle /= big_op_app.
Qed.
-Lemma ht_adequacy_steps P Q k n e1 t2 σ1 σ2 r1 :
- {{ P }} e1 @ ⊤ {{ Q }} →
+Lemma ht_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
+ {{ P }} e1 @ ⊤ {{ Φ }} →
nsteps step k ([e1],σ1) (t2,σ2) →
1 < n → wsat (k + n) ⊤ σ1 r1 →
P (k + n) r1 →
- ∃ rs2 Qs', wptp n t2 (Q :: Qs') rs2 ∧ wsat n ⊤ σ2 (big_op rs2).
+ ∃ rs2 Φs', wptp n t2 (Φ :: Φs') rs2 ∧ wsat n ⊤ σ2 (big_op rs2).
Proof.
- intros Hht ????; apply (nsteps_wptp [Q] k n ([e1],σ1) (t2,σ2) [r1]);
+ intros Hht ????; apply (nsteps_wptp [Φ] k n ([e1],σ1) (t2,σ2) [r1]);
rewrite /big_op ?right_id; auto.
constructor; last constructor.
apply Hht with r1 (k + n); eauto using cmra_included_unit.
eapply uPred.const_intro; eauto.
Qed.
-Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
+Lemma ht_adequacy_own Φ e1 t2 σ1 m σ2 :
✓m →
- {{ ownP σ1 ★ ownG m }} e1 @ ⊤ {{ Q }} →
+ {{ ownP σ1 ★ ownG m }} e1 @ ⊤ {{ Φ }} →
rtc step ([e1],σ1) (t2,σ2) →
- ∃ rs2 Qs', wptp 2 t2 (Q :: Qs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2).
+ ∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2).
Proof.
intros Hv ? [k ?]%rtc_nsteps.
eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
@@ -91,30 +93,30 @@ Proof.
apply wp_value_inv in Hwp; destruct (Hwp (big_op rs) 2 ∅ σ2) as [r' []]; auto.
by rewrite right_id_L.
Qed.
-Lemma ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2 :
+Lemma ht_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
✓ m →
- {{ ownP σ1 ★ ownG m }} e1 @ E {{ Q }} →
+ {{ ownP σ1 ★ ownG m }} e1 @ E {{ Φ }} →
rtc step ([e1], σ1) (t2, σ2) →
e2 ∈ t2 → to_val e2 = None → reducible e2 σ2.
Proof.
intros Hv ? Hs [i ?]%elem_of_list_lookup He.
- destruct (ht_adequacy_own Q e1 t2 σ1 m σ2) as (rs2&Qs&?&?); auto.
+ destruct (ht_adequacy_own Φ e1 t2 σ1 m σ2) as (rs2&Φs&?&?); auto.
{ by rewrite -(ht_mask_weaken E ⊤). }
- destruct (Forall3_lookup_l (λ e Q r, wp ⊤ e Q 2 r) t2
- (Q :: Qs) rs2 i e2) as (Q'&r2&?&?&Hwp); auto.
- destruct (wp_step_inv ⊤ ∅ Q' e2 1 2 σ2 r2 (big_op (delete i rs2)));
+ destruct (Forall3_lookup_l (λ e Φ r, wp ⊤ e Φ 2 r) t2
+ (Φ :: Φs) rs2 i e2) as (Φ'&r2&?&?&Hwp); auto.
+ destruct (wp_step_inv ⊤ ∅ Φ' e2 1 2 σ2 r2 (big_op (delete i rs2)));
rewrite ?right_id_L ?big_op_delete; auto.
Qed.
-Theorem ht_adequacy_safe E Q e1 t2 σ1 m σ2 :
+Theorem ht_adequacy_safe E Φ e1 t2 σ1 m σ2 :
✓ m →
- {{ ownP σ1 ★ ownG m }} e1 @ E {{ Q }} →
+ {{ ownP σ1 ★ ownG m }} e1 @ E {{ Φ }} →
rtc step ([e1], σ1) (t2, σ2) →
Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
Proof.
intros.
destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
- destruct (ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2) as (e3&σ3&ef&?);
+ destruct (ht_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2) as (e3&σ3&ef&?);
rewrite ?eq_None_not_Some; auto.
destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index be20490dad55259ee32ac17d7e06a61a22dda456..0ce603866f59e4bd4f79fb05601a7bc99dce6d20 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -97,7 +97,7 @@ Section auth.
(* Notice how the user has to prove that `bâ‹…a'` is valid at all
step-indices. However, since A is timeless, that should not be
a restriction. *)
- Lemma auth_fsa E N P (Q : V → iPropG Λ Σ) γ a :
+ Lemma auth_fsa E N P (Ψ : V → iPropG Λ Σ) γ a :
fsaV →
nclose N ⊆ E →
P ⊑ auth_ctx γ N φ →
@@ -105,8 +105,8 @@ Section auth.
■✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
■(Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
- (auth_own γ (L a) -★ Q x))) →
- P ⊑ fsa E Q.
+ (auth_own γ (L a) -★ Ψ x))) →
+ P ⊑ fsa E Ψ.
Proof.
rewrite /auth_ctx=>? HN Hinv Hinner.
eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
@@ -129,7 +129,7 @@ Section auth.
rewrite pvs_frame_l. apply pvs_mono.
by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l.
Qed.
- Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Q: V → iPropG Λ Σ) γ a :
+ Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Ψ : V → iPropG Λ Σ) γ a :
fsaV →
nclose N ⊆ E →
P ⊑ auth_ctx γ N φ →
@@ -137,8 +137,8 @@ Section auth.
■✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
fsa (E ∖ nclose N) (λ x,
■(Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
- (auth_own γ (L a) -★ Q x)))) →
- P ⊑ fsa E Q.
+ (auth_own γ (L a) -★ Ψ x)))) →
+ P ⊑ fsa E Ψ.
Proof.
intros ??? HP. eapply auth_fsa with N γ a; eauto.
rewrite HP; apply sep_mono; first done; apply forall_mono=> a'.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index af48ef24e0105ec424c576b330b034b92345110e..c1a52f2546db44a130a01caab51929f3c0a3c8a9 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,35 +1,35 @@
From program_logic Require Export weakestpre viewshifts.
Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
- (e : expr Λ) (Q : val Λ → iProp Λ Σ) : iProp Λ Σ := (□ (P → wp E e Q))%I.
+ (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := (□ (P → wp E e Φ))%I.
Instance: Params (@ht) 3.
-Notation "{{ P } } e @ E {{ Q } }" := (ht E P e Q)
- (at level 74, format "{{ P } } e @ E {{ Q } }") : uPred_scope.
-Notation "{{ P } } e @ E {{ Q } }" := (True ⊑ ht E P e Q)
- (at level 74, format "{{ P } } e @ E {{ Q } }") : C_scope.
+Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ)
+ (at level 74, format "{{ P } } e @ E {{ Φ } }") : uPred_scope.
+Notation "{{ P } } e @ E {{ Φ } }" := (True ⊑ ht E P e Φ)
+ (at level 74, format "{{ P } } e @ E {{ Φ } }") : C_scope.
Section hoare.
Context {Λ : language} {Σ : iFunctor}.
-Implicit Types P : iProp Λ Σ.
-Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types P Q : iProp Λ Σ.
+Implicit Types Φ Ψ : val Λ → iProp Λ Σ.
Implicit Types v : val Λ.
Import uPred.
Global Instance ht_ne E n :
Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (@ht Λ Σ E).
-Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
+Proof. by intros P P' HP e ? <- Φ Φ' HΦ; rewrite /ht HP; setoid_rewrite HΦ. Qed.
Global Instance ht_proper E :
Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (@ht Λ Σ E).
-Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
-Lemma ht_mono E P P' Q Q' e :
- P ⊑ P' → (∀ v, Q' v ⊑ Q v) → {{ P' }} e @ E {{ Q' }} ⊑ {{ P }} e @ E {{ Q }}.
+Proof. by intros P P' HP e ? <- Φ Φ' HΦ; rewrite /ht HP; setoid_rewrite HΦ. Qed.
+Lemma ht_mono E P P' Φ Φ' e :
+ P ⊑ P' → (∀ v, Φ' v ⊑ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊑ {{ P }} e @ E {{ Φ }}.
Proof. by intros; apply always_mono, impl_mono, wp_mono. Qed.
Global Instance ht_mono' E :
Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Λ Σ E).
-Proof. by intros P P' HP e ? <- Q Q' HQ; apply ht_mono. Qed.
+Proof. by intros P P' HP e ? <- Φ Φ' HΦ; apply ht_mono. Qed.
-Lemma ht_alt E P Q e : (P ⊑ wp E e Q) → {{ P }} e @ E {{ Q }}.
+Lemma ht_alt E P Φ e : (P ⊑ wp E e Φ) → {{ P }} e @ E {{ Φ }}.
Proof.
intros; rewrite -{1}always_const. apply (always_intro _ _), impl_intro_l.
by rewrite always_const right_id.
@@ -39,21 +39,21 @@ Lemma ht_val E v :
{{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
Proof. apply ht_alt. by rewrite -wp_value'; apply const_intro. Qed.
-Lemma ht_vs E P P' Q Q' e :
- ((P ={E}=> P') ∧ {{ P' }} e @ E {{ Q' }} ∧ ∀ v, Q' v ={E}=> Q v)
- ⊑ {{ P }} e @ E {{ Q }}.
+Lemma ht_vs E P P' Φ Φ' e :
+ ((P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ ∀ v, Φ' v ={E}=> Φ v)
+ ⊑ {{ P }} e @ E {{ Φ }}.
Proof.
apply (always_intro _ _), impl_intro_l.
rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
- rewrite -(pvs_wp E e Q) -(wp_pvs E e Q); apply pvs_mono, wp_mono=> v.
+ rewrite -(pvs_wp E e Φ) -(wp_pvs E e Φ); apply pvs_mono, wp_mono=> v.
by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
Qed.
-Lemma ht_atomic E1 E2 P P' Q Q' e :
+Lemma ht_atomic E1 E2 P P' Φ Φ' e :
E2 ⊆ E1 → atomic e →
- ((P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Q' }} ∧ ∀ v, Q' v ={E2,E1}=> Q v)
- ⊑ {{ P }} e @ E1 {{ Q }}.
+ ((P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ ∀ v, Φ' v ={E2,E1}=> Φ v)
+ ⊑ {{ P }} e @ E1 {{ Φ }}.
Proof.
intros ??; apply (always_intro _ _), impl_intro_l.
rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
@@ -62,9 +62,9 @@ Proof.
by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
Qed.
-Lemma ht_bind `{LanguageCtx Λ K} E P Q Q' e :
- ({{ P }} e @ E {{ Q }} ∧ ∀ v, {{ Q v }} K (of_val v) @ E {{ Q' }})
- ⊑ {{ P }} K e @ E {{ Q' }}.
+Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
+ ({{ P }} e @ E {{ Φ }} ∧ ∀ v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
+ ⊑ {{ P }} K e @ E {{ Φ' }}.
Proof.
intros; apply (always_intro _ _), impl_intro_l.
rewrite (assoc _ P) {1}/ht always_elim impl_elim_r.
@@ -72,37 +72,36 @@ Proof.
by rewrite (forall_elim v) /ht always_elim impl_elim_r.
Qed.
-Lemma ht_mask_weaken E1 E2 P Q e :
- E1 ⊆ E2 → {{ P }} e @ E1 {{ Q }} ⊑ {{ P }} e @ E2 {{ Q }}.
+Lemma ht_mask_weaken E1 E2 P Φ e :
+ E1 ⊆ E2 → {{ P }} e @ E1 {{ Φ }} ⊑ {{ P }} e @ E2 {{ Φ }}.
Proof. intros. by apply always_mono, impl_mono, wp_mask_frame_mono. Qed.
-Lemma ht_frame_l E P Q R e :
- {{ P }} e @ E {{ Q }} ⊑ {{ R ★ P }} e @ E {{ λ v, R ★ Q v }}.
+Lemma ht_frame_l E P Φ R e :
+ {{ P }} e @ E {{ Φ }} ⊑ {{ R ★ P }} e @ E {{ λ v, R ★ Φ v }}.
Proof.
apply always_intro', impl_intro_l.
rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
by rewrite wp_frame_l.
Qed.
-Lemma ht_frame_r E P Q R e :
- {{ P }} e @ E {{ Q }} ⊑ {{ P ★ R }} e @ E {{ λ v, Q v ★ R }}.
+Lemma ht_frame_r E P Φ R e :
+ {{ P }} e @ E {{ Φ }} ⊑ {{ P ★ R }} e @ E {{ λ v, Φ v ★ R }}.
Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
-Lemma ht_frame_later_l E P R e Q :
+Lemma ht_frame_later_l E P R e Φ :
to_val e = None →
- {{ P }} e @ E {{ Q }} ⊑ {{ ▷ R ★ P }} e @ E {{ λ v, R ★ Q v }}.
+ {{ P }} e @ E {{ Φ }} ⊑ {{ ▷ R ★ P }} e @ E {{ λ v, R ★ Φ v }}.
Proof.
intros; apply always_intro', impl_intro_l.
rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
by rewrite wp_frame_later_l //; apply wp_mono=>v; rewrite pvs_frame_l.
Qed.
-Lemma ht_frame_later_r E P R e Q :
+Lemma ht_frame_later_r E P Φ R e :
to_val e = None →
- {{ P }} e @ E {{ Q }} ⊑ {{ P ★ ▷ R }} e @ E {{ λ v, Q v ★ R }}.
+ {{ P }} e @ E {{ Φ }} ⊑ {{ P ★ ▷ R }} e @ E {{ λ v, Φ v ★ R }}.
Proof.
rewrite (comm _ _ (â–· R)%I); setoid_rewrite (comm _ _ R).
apply ht_frame_later_l.
Qed.
-
End hoare.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index 48100a9d90311939a7ef34cdcd5fce0299d82557..9ed65435153f745928f9a548d1febe3dca1f609f 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -2,29 +2,29 @@ From program_logic Require Export hoare lifting.
From program_logic Require Import ownership.
Import uPred.
-Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
- (default True%I ef (λ e, ht E P e Q))
- (at level 74, format "{{ P } } ef ?@ E {{ Q } }") : uPred_scope.
-Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
- (True ⊑ default True ef (λ e, ht E P e Q))
- (at level 74, format "{{ P } } ef ?@ E {{ Q } }") : C_scope.
+Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
+ (default True%I ef (λ e, ht E P e Φ))
+ (at level 74, format "{{ P } } ef ?@ E {{ Φ } }") : uPred_scope.
+Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
+ (True ⊑ default True ef (λ e, ht E P e Φ))
+ (at level 74, format "{{ P } } ef ?@ E {{ Φ } }") : C_scope.
Section lifting.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types e : expr Λ.
-Implicit Types P : iProp Λ Σ.
-Implicit Types R : val Λ → iProp Λ Σ.
+Implicit Types P Q R : iProp Λ Σ.
+Implicit Types Ψ : val Λ → iProp Λ Σ.
Lemma ht_lift_step E1 E2
- (φ : expr Λ → state Λ → option (expr Λ) → Prop) P P' Q1 Q2 R e1 σ1 :
+ (φ : expr Λ → state Λ → option (expr Λ) → Prop) P P' Φ1 Φ2 Ψ e1 σ1 :
E1 ⊆ E2 → to_val e1 = None →
reducible e1 σ1 →
(∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
((P ={E2,E1}=> ownP σ1 ★ ▷ P') ∧ ∀ e2 σ2 ef,
- (■φ e2 σ2 ef ★ ownP σ2 ★ P' ={E1,E2}=> Q1 e2 σ2 ef ★ Q2 e2 σ2 ef) ∧
- {{ Q1 e2 σ2 ef }} e2 @ E2 {{ R }} ∧
- {{ Q2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }})
- ⊑ {{ P }} e1 @ E2 {{ R }}.
+ (■φ e2 σ2 ef ★ ownP σ2 ★ P' ={E1,E2}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧
+ {{ Φ1 e2 σ2 ef }} e2 @ E2 {{ Ψ }} ∧
+ {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }})
+ ⊑ {{ P }} e1 @ E2 {{ Ψ }}.
Proof.
intros ?? Hsafe Hstep; apply (always_intro _ _), impl_intro_l.
rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
@@ -37,7 +37,7 @@ Proof.
rewrite (assoc _ _ P') -(assoc _ _ _ P') assoc.
rewrite {1}/vs -always_wand_impl always_elim wand_elim_r.
rewrite pvs_frame_r; apply pvs_mono.
- rewrite (comm _ (Q1 _ _ _)) -assoc (assoc _ (Q1 _ _ _)).
+ rewrite (comm _ (Φ1 _ _ _)) -assoc (assoc _ (Φ1 _ _ _)).
rewrite {1}/ht -always_wand_impl always_elim wand_elim_r.
rewrite assoc (comm _ _ (wp _ _ _)) -assoc.
apply sep_mono; first done.
@@ -73,14 +73,14 @@ Proof.
by rewrite -always_and_sep_r; apply and_intro; try apply const_intro.
Qed.
-Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1 :
+Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e1 :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
(∀ e2 ef,
- {{ ■φ e2 ef ★ P }} e2 @ E {{ Q }} ∧
+ {{ ■φ e2 ef ★ P }} e2 @ E {{ Ψ }} ∧
{{ ■φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }})
- ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Q }}.
+ ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
Proof.
intros ? Hsafe Hstep; apply (always_intro _ _), impl_intro_l.
rewrite -(wp_lift_pure_step E φ _ e1) //.
@@ -100,12 +100,12 @@ Proof.
Qed.
Lemma ht_lift_pure_det_step
- E (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1 e2 ef :
+ E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e1 e2 ef :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
- ({{ P }} e2 @ E {{ Q }} ∧ {{ P' }} ef ?@ ⊤ {{ λ _, True }})
- ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Q }}.
+ ({{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ λ _, True }})
+ ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
Proof.
intros ? Hsafe Hdet.
rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 0ea33451fde59f2a9080ac0dc0a4cc53bd28a4b2..559e4ba2b34ee8baeb62166c87cc00d3dcae7f68 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -18,6 +18,7 @@ Context {Λ : language} {Σ : iFunctor}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Λ Σ.
+Implicit Types Φ : val Λ → iProp Λ Σ.
Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
Proof. intros n ???. apply exists_ne=>i. by apply and_ne, ownI_contractive. Qed.
@@ -29,13 +30,11 @@ Lemma always_inv N P : (□ inv N P)%I ≡ inv N P.
Proof. by rewrite always_always. Qed.
(** Invariants can be opened around any frame-shifting assertion. *)
-Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}
- E N P (Q : A → iProp Λ Σ) R :
- fsaV →
- nclose N ⊆ E →
+Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ R :
+ fsaV → nclose N ⊆ E →
R ⊑ inv N P →
- R ⊑ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Q a)) →
- R ⊑ fsa E Q.
+ R ⊑ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Ψ a)) →
+ R ⊑ fsa E Ψ.
Proof.
intros ? HN Hinv Hinner.
rewrite -[R](idemp (∧)%I) {1}Hinv Hinner =>{Hinv Hinner R}.
@@ -58,15 +57,15 @@ Qed.
Lemma pvs_open_close E N P Q R :
nclose N ⊆ E →
R ⊑ inv N P →
- R ⊑ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q)) →
+ R ⊑ (▷ P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷ P ★ Q)) →
R ⊑ pvs E E Q.
Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
-Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) R :
+Lemma wp_open_close E e N P Φ R :
atomic e → nclose N ⊆ E →
R ⊑ inv N P →
- R ⊑ (▷ P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v)) →
- R ⊑ wp E e Q.
+ R ⊑ (▷ P -★ wp (E ∖ nclose N) e (λ v, ▷ P ★ Φ v)) →
+ R ⊑ wp E e Φ.
Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
Lemma inv_alloc N P : ▷ P ⊑ pvs N N (inv N P).
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index bd00e8cd4689ea0646e74bbf6e0e258a16694c71..c9b24371a66ef4a458d759e32cdf2da918edd403 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -12,19 +12,20 @@ Context {Λ : language} {Σ : iFunctor}.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
-Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types P Q : iProp Λ Σ.
+Implicit Types Φ : val Λ → iProp Λ Σ.
Transparent uPred_holds.
Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, True)))%I.
Lemma wp_lift_step E1 E2
- (φ : expr Λ → state Λ → option (expr Λ) → Prop) Q e1 σ1 :
+ (φ : expr Λ → state Λ → option (expr Λ) → Prop) Φ e1 σ1 :
E1 ⊆ E2 → to_val e1 = None →
reducible e1 σ1 →
(∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2 ef,
- (■φ e2 σ2 ef ∧ ownP σ2) -★ pvs E1 E2 (wp E2 e2 Q ★ wp_fork ef))
- ⊑ wp E2 e1 Q.
+ (■φ e2 σ2 ef ∧ ownP σ2) -★ pvs E1 E2 (wp E2 e2 Φ ★ wp_fork ef))
+ ⊑ wp E2 e1 Φ.
Proof.
intros ? He Hsafe Hstep r n ? Hvs; constructor; auto.
intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1')
@@ -40,11 +41,11 @@ Proof.
by exists r1', r2'; split_ands; [| |by intros ? ->].
Qed.
-Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Q e1 :
+Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
- (▷ ∀ e2 ef, ■φ e2 ef → wp E e2 Q ★ wp_fork ef) ⊑ wp E e1 Q.
+ (▷ ∀ e2 ef, ■φ e2 ef → wp E e2 Φ ★ wp_fork ef) ⊑ wp E e1 Φ.
Proof.
intros He Hsafe Hstep r n ? Hwp; constructor; auto.
intros rf k Ef σ1 ???; split; [done|]. destruct n as [|n]; first lia.
@@ -57,14 +58,14 @@ Qed.
Opaque uPred_holds.
Import uPred.
-Lemma wp_lift_atomic_step {E Q} e1
+Lemma wp_lift_atomic_step {E Φ} e1
(φ : val Λ → state Λ → option (expr Λ) → Prop) σ1 :
to_val e1 = None →
reducible e1 σ1 →
(∀ e2 σ2 ef,
prim_step e1 σ1 e2 σ2 ef → ∃ v2, to_val e2 = Some v2 ∧ φ v2 σ2 ef) →
- (ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■φ v2 σ2 ef ∧ ownP σ2 -★ Q v2 ★ wp_fork ef)
- ⊑ wp E e1 Q.
+ (ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■φ v2 σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
+ ⊑ wp E e1 Φ.
Proof.
intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, ∃ v2,
to_val e2 = Some v2 ∧ φ v2 σ2 ef) _ e1 σ1) //; [].
@@ -78,12 +79,12 @@ Proof.
by rewrite left_id wand_elim_r -(wp_value _ _ e2' v2').
Qed.
-Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 ef :
+Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
to_val e1 = None →
reducible e1 σ1 →
(∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
- (ownP σ1 ★ ▷ (ownP σ2 -★ Q v2 ★ wp_fork ef)) ⊑ wp E e1 Q.
+ (ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef)) ⊑ wp E e1 Φ.
Proof.
intros. rewrite -(wp_lift_atomic_step _ (λ v2' σ2' ef',
σ2 = σ2' ∧ v2 = v2' ∧ ef = ef') σ1) //; last naive_solver.
@@ -94,11 +95,11 @@ Proof.
apply const_elim_l=>-[-> [-> ->]] /=. by rewrite wand_elim_r.
Qed.
-Lemma wp_lift_pure_det_step {E Q} e1 e2 ef :
+Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
- ▷ (wp E e2 Q ★ wp_fork ef) ⊑ wp E e1 Q.
+ ▷ (wp E e2 Φ ★ wp_fork ef) ⊑ wp E e1 Φ.
Proof.
intros.
rewrite -(wp_lift_pure_step E (λ e2' ef', e2 = e2' ∧ ef = ef') _ e1) //=.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index b309e564fe7cd138e1dc3385fb623ad51456f9e6..9fb421ddd2ce062c6bf0bbc7bf6eb133fea3d590 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -148,9 +148,7 @@ Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P ∧ □ (P → Q)) ⊑ pvs E1 E2 Q.
Proof. by rewrite comm pvs_impl_l. Qed.
Lemma pvs_wand_l E1 E2 P Q R :
P ⊑ pvs E1 E2 Q → ((Q -★ R) ★ P) ⊑ pvs E1 E2 R.
-Proof.
- intros ->. rewrite pvs_frame_l. apply pvs_mono, wand_elim_l.
-Qed.
+Proof. intros ->. rewrite pvs_frame_l. apply pvs_mono, wand_elim_l. Qed.
Lemma pvs_wand_r E1 E2 P Q R :
P ⊑ pvs E1 E2 Q → (P ★ (Q -★ R)) ⊑ pvs E1 E2 R.
Proof. rewrite comm. apply pvs_wand_l. Qed.
@@ -195,34 +193,34 @@ End pvs.
into the postcondition, and composition witn mask-changing view shifts. *)
Notation FSA Λ Σ A := (coPset → (A → iProp Λ Σ) → iProp Λ Σ).
Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
- fsa_mask_frame_mono E1 E2 Q Q' :
- E1 ⊆ E2 → (∀ a, Q a ⊑ Q' a) → fsa E1 Q ⊑ fsa E2 Q';
- fsa_trans3 E Q : pvs E E (fsa E (λ a, pvs E E (Q a))) ⊑ fsa E Q;
- fsa_open_close E1 E2 Q :
- fsaV → E2 ⊆ E1 → pvs E1 E2 (fsa E2 (λ a, pvs E2 E1 (Q a))) ⊑ fsa E1 Q;
- fsa_frame_r E P Q : (fsa E Q ★ P) ⊑ fsa E (λ a, Q a ★ P)
+ fsa_mask_frame_mono E1 E2 Φ Ψ :
+ E1 ⊆ E2 → (∀ a, Φ a ⊑ Ψ a) → fsa E1 Φ ⊑ fsa E2 Ψ;
+ fsa_trans3 E Φ : pvs E E (fsa E (λ a, pvs E E (Φ a))) ⊑ fsa E Φ;
+ fsa_open_close E1 E2 Φ :
+ fsaV → E2 ⊆ E1 → pvs E1 E2 (fsa E2 (λ a, pvs E2 E1 (Φ a))) ⊑ fsa E1 Φ;
+ fsa_frame_r E P Φ : (fsa E Φ ★ P) ⊑ fsa E (λ a, Φ a ★ P)
}.
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
-Implicit Types Q : A → iProp Λ Σ.
+Implicit Types Φ Ψ : A → iProp Λ Σ.
-Lemma fsa_mono E Q Q' : (∀ a, Q a ⊑ Q' a) → fsa E Q ⊑ fsa E Q'.
+Lemma fsa_mono E Φ Ψ : (∀ a, Φ a ⊑ Ψ a) → fsa E Φ ⊑ fsa E Ψ.
Proof. apply fsa_mask_frame_mono; auto. Qed.
-Lemma fsa_mask_weaken E1 E2 Q : E1 ⊆ E2 → fsa E1 Q ⊑ fsa E2 Q.
+Lemma fsa_mask_weaken E1 E2 Φ : E1 ⊆ E2 → fsa E1 Φ ⊑ fsa E2 Φ.
Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
-Lemma fsa_frame_l E P Q : (P ★ fsa E Q) ⊑ fsa E (λ a, P ★ Q a).
+Lemma fsa_frame_l E P Φ : (P ★ fsa E Φ) ⊑ fsa E (λ a, P ★ Φ a).
Proof. rewrite comm fsa_frame_r. apply fsa_mono=>a. by rewrite comm. Qed.
-Lemma fsa_strip_pvs E P Q : P ⊑ fsa E Q → pvs E E P ⊑ fsa E Q.
+Lemma fsa_strip_pvs E P Φ : P ⊑ fsa E Φ → pvs E E P ⊑ fsa E Φ.
Proof.
move=>->. rewrite -{2}fsa_trans3.
apply pvs_mono, fsa_mono=>a; apply pvs_intro.
Qed.
-Lemma fsa_mono_pvs E Q Q' : (∀ a, Q a ⊑ pvs E E (Q' a)) → fsa E Q ⊑ fsa E Q'.
-Proof. intros. rewrite -[fsa E Q']fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
+Lemma fsa_mono_pvs E Φ Ψ : (∀ a, Φ a ⊑ pvs E E (Ψ a)) → fsa E Φ ⊑ fsa E Ψ.
+Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
End fsa.
-Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Q, pvs E E (Q ()).
+Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, pvs E E (Φ ()).
Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
Proof.
rewrite /pvs_fsa.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index eff7bea2f6588deb232ed8f72b1d91448f06226d..db5f5f9d2f05011256300d3214bec3fbddba5c5b 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -118,15 +118,15 @@ Section sts.
Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
- Lemma sts_fsaS E N P (Q : V → iPropG Λ Σ) γ S T :
+ Lemma sts_fsaS E N P (Ψ : V → iPropG Λ Σ) γ S T :
fsaV → nclose N ⊆ E →
P ⊑ sts_ctx γ N φ →
P ⊑ (sts_ownS γ S T ★ ∀ s,
■(s ∈ S) ★ ▷ φ s -★
fsa (E ∖ nclose N) (λ x, ∃ s' T',
■sts.step (s, T) (s', T') ★ ▷ φ s' ★
- (sts_own γ s' T' -★ Q x))) →
- P ⊑ fsa E Q.
+ (sts_own γ s' T' -★ Ψ x))) →
+ P ⊑ fsa E Ψ.
Proof.
rewrite /sts_ctx=>? HN Hinv Hinner.
eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
@@ -147,14 +147,14 @@ Section sts.
by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l.
Qed.
- Lemma sts_fsa E N P (Q : V → iPropG Λ Σ) γ s0 T :
+ Lemma sts_fsa E N P (Ψ : V → iPropG Λ Σ) γ s0 T :
fsaV → nclose N ⊆ E →
P ⊑ sts_ctx γ N φ →
P ⊑ (sts_own γ s0 T ★ ∀ s,
■(s ∈ sts.up s0 T) ★ ▷ φ s -★
fsa (E ∖ nclose N) (λ x, ∃ s' T',
■(sts.step (s, T) (s', T')) ★ ▷ φ s' ★
- (sts_own γ s' T' -★ Q x))) →
- P ⊑ fsa E Q.
+ (sts_own γ s' T' -★ Ψ x))) →
+ P ⊑ fsa E Ψ.
Proof. apply sts_fsaS. Qed.
End sts.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 995154be87856a8718e3f5ad0035f1035dfba565..19aabc83c4c9c666003b6afa85b16daff13b7b3f 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -9,37 +9,37 @@ Local Hint Extern 10 (✓{_} _) =>
| H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
end; solve_validN.
-Record wp_go {Λ Σ} (E : coPset) (Q Qfork : expr Λ → nat → iRes Λ Σ → Prop)
+Record wp_go {Λ Σ} (E : coPset) (Φ Φfork : expr Λ → nat → iRes Λ Σ → Prop)
(k : nat) (rf : iRes Λ Σ) (e1 : expr Λ) (σ1 : state Λ) := {
wf_safe : reducible e1 σ1;
wp_step e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef →
∃ r2 r2',
wsat k E σ2 (r2 ⋅ r2' ⋅ rf) ∧
- Q e2 k r2 ∧
- ∀ e', ef = Some e' → Qfork e' k r2'
+ Φ e2 k r2 ∧
+ ∀ e', ef = Some e' → Φfork e' k r2'
}.
CoInductive wp_pre {Λ Σ} (E : coPset)
- (Q : val Λ → iProp Λ Σ) : expr Λ → nat → iRes Λ Σ → Prop :=
- | wp_pre_value n r v : pvs E E (Q v) n r → wp_pre E Q (of_val v) n r
+ (Φ : val Λ → iProp Λ Σ) : expr Λ → nat → iRes Λ Σ → Prop :=
+ | wp_pre_value n r v : pvs E E (Φ v) n r → wp_pre E Φ (of_val v) n r
| wp_pre_step n r1 e1 :
to_val e1 = None →
(∀ rf k Ef σ1,
0 < k < n → E ∩ Ef = ∅ →
wsat (S k) (E ∪ Ef) σ1 (r1 ⋅ rf) →
- wp_go (E ∪ Ef) (wp_pre E Q)
+ wp_go (E ∪ Ef) (wp_pre E Φ)
(wp_pre ⊤ (λ _, True%I)) k rf e1 σ1) →
- wp_pre E Q e1 n r1.
+ wp_pre E Φ e1 n r1.
Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ)
- (Q : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Q e |}.
+ (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}.
Next Obligation.
- intros Λ Σ E e Q r1 r2 n Hwp Hr.
+ intros Λ Σ E e Φ r1 r2 n Hwp Hr.
destruct Hwp as [|n r1 e2 ? Hgo]; constructor; rewrite -?Hr; auto.
intros rf k Ef σ1 ?; rewrite -(dist_le _ _ _ _ Hr); naive_solver.
Qed.
Next Obligation.
- intros Λ Σ E e Q r1 r2 n1; revert Q E e r1 r2.
- induction n1 as [n1 IH] using lt_wf_ind; intros Q E e r1 r1' n2.
+ intros Λ Σ E e Φ r1 r2 n1; revert Φ E e r1 r2.
+ induction n1 as [n1 IH] using lt_wf_ind; intros Φ E e r1 r1' n2.
destruct 1 as [|n1 r1 e1 ? Hgo].
- constructor; eauto using uPred_weaken.
- intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???].
@@ -54,7 +54,7 @@ Instance: Params (@wp) 4.
Section wp.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P : iProp Λ Σ.
-Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types Φ : val Λ → iProp Λ Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Transparent uPred_holds.
@@ -62,10 +62,10 @@ Transparent uPred_holds.
Global Instance wp_ne E e n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
Proof.
- cut (∀ Q1 Q2, (∀ v, Q1 v ≡{n}≡ Q2 v) →
- ∀ r n', n' ≤ n → ✓{n'} r → wp E e Q1 n' r → wp E e Q2 n' r).
- { by intros help Q Q' HQ; split; apply help. }
- intros Q1 Q2 HQ r n'; revert e r.
+ cut (∀ Φ Ψ, (∀ v, Φ v ≡{n}≡ Ψ v) →
+ ∀ r n', n' ≤ n → ✓{n'} r → wp E e Φ n' r → wp E e Ψ n' r).
+ { by intros help Φ Ψ HΦΨ; split; apply help. }
+ intros Φ Ψ HΦΨ r n'; revert e r.
induction n' as [n' IH] using lt_wf_ind=> e r.
destruct 3 as [n' r v HpvsQ|n' r e1 ? Hgo].
{ constructor. by eapply pvs_ne, HpvsQ; eauto. }
@@ -78,12 +78,12 @@ Qed.
Global Instance wp_proper E e :
Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ E e).
Proof.
- by intros Q Q' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
+ by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Qed.
-Lemma wp_mask_frame_mono E1 E2 e Q1 Q2 :
- E1 ⊆ E2 → (∀ v, Q1 v ⊑ Q2 v) → wp E1 e Q1 ⊑ wp E2 e Q2.
+Lemma wp_mask_frame_mono E1 E2 e Φ Ψ :
+ E1 ⊆ E2 → (∀ v, Φ v ⊑ Ψ v) → wp E1 e Φ ⊑ wp E2 e Ψ.
Proof.
- intros HE HQ r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r.
+ intros HE HΦ r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r.
destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo].
{ constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. }
constructor; [done|]=> rf k Ef σ1 ???.
@@ -95,19 +95,19 @@ Proof.
exists r2, r2'; split_ands; [rewrite HE'|eapply IH|]; eauto.
Qed.
-Lemma wp_value_inv E Q v n r : wp E (of_val v) Q n r → pvs E E (Q v) n r.
+Lemma wp_value_inv E Φ v n r : wp E (of_val v) Φ n r → pvs E E (Φ v) n r.
Proof.
by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_eq.
Qed.
-Lemma wp_step_inv E Ef Q e k n σ r rf :
+Lemma wp_step_inv E Ef Φ e k n σ r rf :
to_val e = None → 0 < k < n → E ∩ Ef = ∅ →
- wp E e Q n r → wsat (S k) (E ∪ Ef) σ (r ⋅ rf) →
- wp_go (E ∪ Ef) (λ e, wp E e Q) (λ e, wp ⊤ e (λ _, True%I)) k rf e σ.
+ wp E e Φ n r → wsat (S k) (E ∪ Ef) σ (r ⋅ rf) →
+ wp_go (E ∪ Ef) (λ e, wp E e Φ) (λ e, wp ⊤ e (λ _, True%I)) k rf e σ.
Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
-Lemma wp_value' E Q v : Q v ⊑ wp E (of_val v) Q.
+Lemma wp_value' E Φ v : Φ v ⊑ wp E (of_val v) Φ.
Proof. by constructor; apply pvs_intro. Qed.
-Lemma pvs_wp E e Q : pvs E E (wp E e Q) ⊑ wp E e Q.
+Lemma pvs_wp E e Φ : pvs E E (wp E e Φ) ⊑ wp E e Φ.
Proof.
intros r n ? Hvs.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
@@ -117,24 +117,24 @@ Proof.
destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
eapply wp_step_inv with (S k) r'; eauto.
Qed.
-Lemma wp_pvs E e Q : wp E e (λ v, pvs E E (Q v)) ⊑ wp E e Q.
+Lemma wp_pvs E e Φ : wp E e (λ v, pvs E E (Φ v)) ⊑ wp E e Φ.
Proof.
- intros r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HQ.
+ intros r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
- { constructor; apply pvs_trans', (wp_value_inv _ (pvs E E ∘ Q)); auto. }
+ { constructor; apply pvs_trans', (wp_value_inv _ (pvs E E ∘ Φ)); auto. }
constructor; [done|]=> rf k Ef σ1 ???.
- destruct (wp_step_inv E Ef (pvs E E ∘ Q) e k n σ1 r rf) as [? Hstep]; auto.
+ destruct (wp_step_inv E Ef (pvs E E ∘ Φ) e k n σ1 r rf) as [? Hstep]; auto.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); auto.
exists r2, r2'; split_ands; [|apply (IH k)|]; auto.
Qed.
-Lemma wp_atomic E1 E2 e Q :
- E2 ⊆ E1 → atomic e → pvs E1 E2 (wp E2 e (λ v, pvs E2 E1 (Q v))) ⊑ wp E1 e Q.
+Lemma wp_atomic E1 E2 e Φ :
+ E2 ⊆ E1 → atomic e → pvs E1 E2 (wp E2 e (λ v, pvs E2 E1 (Φ v))) ⊑ wp E1 e Φ.
Proof.
intros ? He r n ? Hvs; constructor; eauto using atomic_not_val.
intros rf k Ef σ1 ???.
destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
- destruct (wp_step_inv E2 Ef (pvs E2 E1 ∘ Q) e k (S k) σ1 r' rf)
+ destruct (wp_step_inv E2 Ef (pvs E2 E1 ∘ Φ) e k (S k) σ1 r' rf)
as [Hsafe Hstep]; auto using atomic_not_val.
split; [done|]=> e2 σ2 ef ?.
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto.
@@ -146,7 +146,7 @@ Proof.
- by rewrite -assoc.
- constructor; apply pvs_intro; auto.
Qed.
-Lemma wp_frame_r E e Q R : (wp E e Q ★ R) ⊑ wp E e (λ v, Q v ★ R).
+Lemma wp_frame_r E e Φ R : (wp E e Φ ★ R) ⊑ wp E e (λ v, Φ v ★ R).
Proof.
intros r' n Hvalid (r&rR&Hr&Hwp&?); revert Hvalid.
rewrite Hr; clear Hr; revert e r Hwp.
@@ -163,8 +163,8 @@ Proof.
(comm _ rR) !assoc -(assoc _ _ rR).
- apply IH; eauto using uPred_weaken.
Qed.
-Lemma wp_frame_later_r E e Q R :
- to_val e = None → (wp E e Q ★ ▷ R) ⊑ wp E e (λ v, Q v ★ R).
+Lemma wp_frame_later_r E e Φ R :
+ to_val e = None → (wp E e Φ ★ ▷ R) ⊑ wp E e (λ v, Φ v ★ R).
Proof.
intros He r' n Hvalid (r&rR&Hr&Hwp&?); revert Hvalid; rewrite Hr; clear Hr.
destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
@@ -178,8 +178,8 @@ Proof.
- apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
eapply uPred_weaken with rR n; eauto.
Qed.
-Lemma wp_bind `{LanguageCtx Λ K} E e Q :
- wp E e (λ v, wp E (K (of_val v)) Q) ⊑ wp E (K e) Q.
+Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
+ wp E e (λ v, wp E (K (of_val v)) Φ) ⊑ wp E (K e) Φ.
Proof.
intros r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?.
destruct 1 as [|n r e ? Hgo]; [by apply pvs_wp|].
@@ -197,39 +197,39 @@ Qed.
(** * Derived rules *)
Opaque uPred_holds.
Import uPred.
-Lemma wp_mono E e Q1 Q2 : (∀ v, Q1 v ⊑ Q2 v) → wp E e Q1 ⊑ wp E e Q2.
+Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊑ Ψ v) → wp E e Φ ⊑ wp E e Ψ.
Proof. by apply wp_mask_frame_mono. Qed.
Global Instance wp_mono' E e :
Proper (pointwise_relation _ (⊑) ==> (⊑)) (@wp Λ Σ E e).
-Proof. by intros Q Q' ?; apply wp_mono. Qed.
-Lemma wp_strip_pvs E e P Q : P ⊑ wp E e Q → pvs E E P ⊑ wp E e Q.
+Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
+Lemma wp_strip_pvs E e P Φ : P ⊑ wp E e Φ → pvs E E P ⊑ wp E e Φ.
Proof. move=>->. by rewrite pvs_wp. Qed.
-Lemma wp_value E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
+Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊑ wp E e Φ.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
-Lemma wp_value_pvs E Q e v : to_val e = Some v → pvs E E (Q v) ⊑ wp E e Q.
+Lemma wp_value_pvs E Φ e v : to_val e = Some v → pvs E E (Φ v) ⊑ wp E e Φ.
Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
-Lemma wp_frame_l E e Q R : (R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).
+Lemma wp_frame_l E e Φ R : (R ★ wp E e Φ) ⊑ wp E e (λ v, R ★ Φ v).
Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
-Lemma wp_frame_later_l E e Q R :
- to_val e = None → (▷ R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).
+Lemma wp_frame_later_l E e Φ R :
+ to_val e = None → (▷ R ★ wp E e Φ) ⊑ wp E e (λ v, R ★ Φ v).
Proof.
rewrite (comm _ (â–· R)%I); setoid_rewrite (comm _ R).
apply wp_frame_later_r.
Qed.
-Lemma wp_always_l E e Q R `{!AlwaysStable R} :
- (R ∧ wp E e Q) ⊑ wp E e (λ v, R ∧ Q v).
+Lemma wp_always_l E e Φ R `{!AlwaysStable 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 Q R `{!AlwaysStable R} :
- (wp E e Q ∧ R) ⊑ wp E e (λ v, Q v ∧ R).
+Lemma wp_always_r E e Φ R `{!AlwaysStable 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 Q1 Q2 : ((□ ∀ v, Q1 v → Q2 v) ∧ wp E e Q1) ⊑ wp E e Q2.
+Lemma wp_impl_l E e Φ Ψ : ((□ ∀ v, Φ v → Ψ v) ∧ wp E e Φ) ⊑ wp E e Ψ.
Proof.
rewrite wp_always_l; apply wp_mono=> // v.
by rewrite always_elim (forall_elim v) impl_elim_l.
Qed.
-Lemma wp_impl_r E e Q1 Q2 : (wp E e Q1 ∧ □ ∀ v, Q1 v → Q2 v) ⊑ wp E e Q2.
+Lemma wp_impl_r E e Φ Ψ : (wp E e Φ ∧ □ ∀ v, Φ v → Ψ v) ⊑ wp E e Ψ.
Proof. by rewrite comm wp_impl_l. Qed.
-Lemma wp_mask_weaken E1 E2 e Q : E1 ⊆ E2 → wp E1 e Q ⊑ wp E2 e Q.
+Lemma wp_mask_weaken E1 E2 e Φ : E1 ⊆ E2 → wp E1 e Φ ⊑ wp E2 e Φ.
Proof. auto using wp_mask_frame_mono. Qed.
(** * Weakest-pre is a FSA. *)
@@ -237,6 +237,6 @@ Definition wp_fsa (e : expr Λ) : FSA Λ Σ (val Λ) := λ E, wp E e.
Global Instance wp_fsa_prf : FrameShiftAssertion (atomic e) (wp_fsa e).
Proof.
rewrite /wp_fsa; split; auto using wp_mask_frame_mono, wp_atomic, wp_frame_r.
- intros E Q. by rewrite -(pvs_wp E e Q) -(wp_pvs E e Q).
+ intros E Φ. by rewrite -(pvs_wp E e Φ) -(wp_pvs E e Φ).
Qed.
End wp.