Commit 2c6727dc by Robbert Krebbers

### Use Φ and Ψ for (value-) indexed uPreds/iProps.

```This avoids ambiguity with P and Q that we were using before for both
uPreds/iProps and indexed uPreds/iProps.```
parent 5e9653fb
 ... ... @@ -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 *) ... ...
 ... ... @@ -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. ... ...
 ... ... @@ -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. ... ...
 ... ... @@ -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.