proof.v 13.5 KB
 Robbert Krebbers committed Feb 24, 2016 1 ``````From prelude Require Import functions. `````` Ralf Jung committed Mar 06, 2016 2 3 ``````From algebra Require Import upred_big_op. From program_logic Require Import sts saved_prop tactics. `````` Robbert Krebbers committed Feb 24, 2016 4 5 ``````From heap_lang Require Export heap wp_tactics. From barrier Require Export barrier. `````` Ralf Jung committed Mar 05, 2016 6 ``````From barrier Require Import protocol. `````` Robbert Krebbers committed Feb 24, 2016 7 8 ``````Import uPred. `````` Ralf Jung committed Mar 06, 2016 9 ``````(** The CMRAs we need. *) `````` Robbert Krebbers committed Feb 24, 2016 10 11 12 ``````(* Not bundling heapG, as it may be shared with other users. *) Class barrierG Σ := BarrierG { barrier_stsG :> stsG heap_lang Σ sts; `````` Robbert Krebbers committed Mar 06, 2016 13 `````` barrier_savedPropG :> savedPropG heap_lang Σ laterCF; `````` Robbert Krebbers committed Feb 24, 2016 14 ``````}. `````` Ralf Jung committed Mar 06, 2016 15 ``````(** The Functors we need. *) `````` Robbert Krebbers committed Mar 06, 2016 16 ``````Definition barrierGF : rFunctors := [stsGF sts; agreeRF laterCF]. `````` Ralf Jung committed Mar 06, 2016 17 18 19 ``````(* Show and register that they match. *) Instance inGF_barrierG `{H : inGFs heap_lang Σ barrierGF} : barrierG Σ. Proof. destruct H as (?&?&?). split; apply _. Qed. `````` Robbert Krebbers committed Feb 24, 2016 20 21 22 `````` (** Now we come to the Iris part of the proof. *) Section proof. `````` Robbert Krebbers committed Mar 02, 2016 23 ``````Context {Σ : rFunctorG} `{!heapG Σ, !barrierG Σ}. `````` Robbert Krebbers committed Feb 24, 2016 24 25 26 ``````Context (heapN N : namespace). Local Notation iProp := (iPropG heap_lang Σ). `````` 27 ``````Definition ress (P : iProp) (I : gset gname) : iProp := `````` Robbert Krebbers committed Feb 24, 2016 28 `````` (∃ Ψ : gname → iProp, `````` Robbert Krebbers committed Mar 02, 2016 29 `````` ▷ (P -★ Π★{set I} Ψ) ★ Π★{set I} (λ i, saved_prop_own i (Next (Ψ i))))%I. `````` Robbert Krebbers committed Feb 24, 2016 30 31 `````` Coercion state_to_val (s : state) : val := `````` Robbert Krebbers committed Mar 02, 2016 32 `````` match s with State Low _ => #0 | State High _ => #1 end. `````` Robbert Krebbers committed Feb 24, 2016 33 34 ``````Arguments state_to_val !_ /. `````` 35 36 37 38 ``````Definition state_to_prop (s : state) (P : iProp) : iProp := match s with State Low _ => P | State High _ => True%I end. Arguments state_to_val !_ /. `````` Robbert Krebbers committed Feb 24, 2016 39 ``````Definition barrier_inv (l : loc) (P : iProp) (s : state) : iProp := `````` 40 `````` (l ↦ s ★ ress (state_to_prop s P) (state_I s))%I. `````` Robbert Krebbers committed Feb 24, 2016 41 42 43 44 45 46 47 48 49 50 `````` Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp := (■ (heapN ⊥ N) ★ heap_ctx heapN ★ sts_ctx γ N (barrier_inv l P))%I. Definition send (l : loc) (P : iProp) : iProp := (∃ γ, barrier_ctx γ l P ★ sts_ownS γ low_states {[ Send ]})%I. Definition recv (l : loc) (R : iProp) : iProp := (∃ γ P Q i, barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★ `````` Robbert Krebbers committed Mar 02, 2016 51 52 `````` saved_prop_own i (Next Q) ★ ▷ (Q -★ R))%I. `````` Ralf Jung committed Mar 06, 2016 53 54 55 56 57 58 59 60 ``````Global Instance barrier_ctx_always_stable (γ : gname) (l : loc) (P : iProp) : AlwaysStable (barrier_ctx γ l P). Proof. apply _. Qed. (* TODO: Figure out if this has a "Global" or "Local" effect. We want it to be Global. *) Typeclasses Opaque barrier_ctx send recv. `````` Robbert Krebbers committed Mar 02, 2016 61 ``````Implicit Types I : gset gname. `````` Robbert Krebbers committed Feb 24, 2016 62 63 `````` (** Setoids *) `````` 64 65 66 67 ``````Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress. Proof. solve_proper. Qed. Global Instance state_to_prop_ne n s : Proper (dist n ==> dist n) (state_to_prop s). `````` Ralf Jung committed Feb 25, 2016 68 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Feb 24, 2016 69 ``````Global Instance barrier_inv_ne n l : `````` Ralf Jung committed Feb 25, 2016 70 71 `````` Proper (dist n ==> eq ==> dist n) (barrier_inv l). Proof. solve_proper. Qed. `````` Robbert Krebbers committed Feb 24, 2016 72 ``````Global Instance barrier_ctx_ne n γ l : Proper (dist n ==> dist n) (barrier_ctx γ l). `````` Ralf Jung committed Mar 06, 2016 73 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Feb 24, 2016 74 ``````Global Instance send_ne n l : Proper (dist n ==> dist n) (send l). `````` Ralf Jung committed Feb 25, 2016 75 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Feb 24, 2016 76 ``````Global Instance recv_ne n l : Proper (dist n ==> dist n) (recv l). `````` Ralf Jung committed Feb 25, 2016 77 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Feb 24, 2016 78 79 `````` (** Helper lemmas *) `````` 80 ``````Lemma ress_split i i1 i2 Q R1 R2 P I : `````` Robbert Krebbers committed Feb 24, 2016 81 `````` i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 → `````` Robbert Krebbers committed Mar 02, 2016 82 83 `````` (saved_prop_own i2 (Next R2) ★ saved_prop_own i1 (Next R1) ★ saved_prop_own i (Next Q) ★ `````` 84 85 `````` (Q -★ R1 ★ R2) ★ ress P I) ⊑ ress P ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))). `````` Robbert Krebbers committed Feb 24, 2016 86 ``````Proof. `````` 87 `````` intros. rewrite /ress !sep_exist_l. apply exist_elim=>Ψ. `````` Robbert Krebbers committed Feb 24, 2016 88 89 90 91 `````` rewrite -(exist_intro (<[i1:=R1]> (<[i2:=R2]> Ψ))). rewrite [(Π★{set _} (λ _, saved_prop_own _ _))%I](big_sepS_delete _ I i) //. do 4 (rewrite big_sepS_insert; last set_solver). rewrite !fn_lookup_insert fn_lookup_insert_ne // !fn_lookup_insert. `````` Ralf Jung committed Mar 05, 2016 92 93 94 95 `````` set savedQ := _ i _. set savedΨ := _ i _. sep_split left: [savedQ; savedΨ; Q -★ _; ▷ (_ -★ Π★{set I} _)]%I. - rewrite !assoc saved_prop_agree later_equivI /=. strip_later. apply wand_intro_l. to_front [P; P -★ _]%I. rewrite wand_elim_r. `````` Robbert Krebbers committed Feb 24, 2016 96 `````` rewrite (big_sepS_delete _ I i) //. `````` Ralf Jung committed Mar 05, 2016 97 `````` sep_split right: [Π★{set _} _]%I. `````` Robbert Krebbers committed Feb 24, 2016 98 99 100 101 `````` + rewrite !assoc. eapply wand_apply_r'; first done. apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); last by eauto with I. rewrite eq_sym. eauto with I. `````` Ralf Jung committed Mar 05, 2016 102 103 104 `````` + apply big_sepS_mono; [done|] => j. rewrite elem_of_difference not_elem_of_singleton=> -[??]. by do 2 (rewrite fn_lookup_insert_ne; last naive_solver). `````` Robbert Krebbers committed Feb 24, 2016 105 106 107 108 `````` - rewrite !assoc [(saved_prop_own i2 _ ★ _)%I]comm; apply sep_mono_r. apply big_sepS_mono; [done|]=> j. rewrite elem_of_difference not_elem_of_singleton=> -[??]. by do 2 (rewrite fn_lookup_insert_ne; last naive_solver). `````` Robbert Krebbers committed Mar 02, 2016 109 ``````Qed. `````` Robbert Krebbers committed Feb 24, 2016 110 111 `````` (** Actual proofs *) `````` Ralf Jung committed Feb 28, 2016 112 ``````Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) : `````` Robbert Krebbers committed Feb 24, 2016 113 `````` heapN ⊥ N → `````` Ralf Jung committed Mar 02, 2016 114 `````` (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (%l)) `````` Ralf Jung committed Mar 04, 2016 115 `````` ⊑ #> newbarrier #() {{ Φ }}. `````` Robbert Krebbers committed Feb 24, 2016 116 ``````Proof. `````` Ralf Jung committed Feb 28, 2016 117 `````` intros HN. rewrite /newbarrier. wp_seq. `````` Robbert Krebbers committed Feb 24, 2016 118 119 120 121 `````` rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj. apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l. rewrite !assoc. apply pvs_wand_r. (* The core of this proof: Allocating the STS and the saved prop. *) `````` Robbert Krebbers committed Mar 06, 2016 122 `````` eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=laterCF) _ (Next P)). `````` Robbert Krebbers committed Feb 24, 2016 123 124 `````` rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l. apply exist_elim=>i. `````` Robbert Krebbers committed Mar 02, 2016 125 126 `````` trans (pvs ⊤ ⊤ (heap_ctx heapN ★ ▷ (barrier_inv l P (State Low {[ i ]})) ★ saved_prop_own i (Next P))). `````` Robbert Krebbers committed Feb 24, 2016 127 `````` - rewrite -pvs_intro. cancel [heap_ctx heapN]. `````` Robbert Krebbers committed Mar 02, 2016 128 `````` rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i (Next P)]. `````` 129 `````` rewrite /barrier_inv /ress -later_intro. cancel [l ↦ #0]%I. `````` Robbert Krebbers committed Feb 24, 2016 130 131 132 133 134 135 136 137 `````` rewrite -(exist_intro (const P)) /=. rewrite -[saved_prop_own _ _](left_id True%I (★)%I). by rewrite !big_sepS_singleton /= wand_diag -later_intro. - rewrite (sts_alloc (barrier_inv l P) ⊤ N); last by eauto. rewrite !pvs_frame_r !pvs_frame_l. rewrite pvs_trans'. apply pvs_strip_pvs. rewrite sep_exist_r sep_exist_l. apply exist_elim=>γ. rewrite /recv /send. rewrite -(exist_intro γ) -(exist_intro P). rewrite -(exist_intro P) -(exist_intro i) -(exist_intro γ). `````` Ralf Jung committed Mar 06, 2016 138 139 140 141 142 `````` rewrite always_and_sep_l wand_diag later_True right_id. rewrite [heap_ctx _]always_sep_dup [sts_ctx _ _ _]always_sep_dup. rewrite /barrier_ctx const_equiv // left_id. ecancel_pvs [saved_prop_own i _; heap_ctx _; heap_ctx _; sts_ctx _ _ _; sts_ctx _ _ _]. `````` Robbert Krebbers committed Feb 24, 2016 143 144 145 146 147 `````` rewrite (sts_own_weaken ⊤ _ _ (i_states i ∩ low_states) _ ({[ Change i ]} ∪ {[ Send ]})). + apply pvs_mono. rewrite -sts_ownS_op; eauto using i_states_closed, low_states_closed. set_solver. `````` Robbert Krebbers committed Feb 24, 2016 148 149 `````` + intros []; set_solver. + set_solver. `````` Robbert Krebbers committed Feb 24, 2016 150 151 152 153 `````` + auto using sts.closed_op, i_states_closed, low_states_closed. Qed. Lemma signal_spec l P (Φ : val → iProp) : `````` Ralf Jung committed Mar 04, 2016 154 `````` (send l P ★ P ★ Φ #()) ⊑ #> signal (%l) {{ Φ }}. `````` Robbert Krebbers committed Feb 24, 2016 155 156 157 158 159 160 ``````Proof. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r. apply exist_elim=>γ. rewrite -!assoc. apply const_elim_sep_l=>?. wp_let. (* I think some evars here are better than repeating *everything* *) eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl; eauto with I ndisj. `````` Ralf Jung committed Mar 06, 2016 161 `````` ecancel [sts_ownS γ _ _]. `````` Robbert Krebbers committed Feb 24, 2016 162 163 164 `````` apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc. apply const_elim_sep_l=>Hs. destruct p; last done. rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep. `````` Robbert Krebbers committed Mar 02, 2016 165 166 `````` eapply wp_store with (v' := #0); eauto with I ndisj. strip_later. cancel [l ↦ #0]%I. `````` Robbert Krebbers committed Feb 24, 2016 167 168 169 `````` apply wand_intro_l. rewrite -(exist_intro (State High I)). rewrite -(exist_intro ∅). rewrite const_equiv /=; last by eauto using signal_step. rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r. `````` Ralf Jung committed Mar 06, 2016 170 `````` sep_split right: [Φ _]; last first. `````` Robbert Krebbers committed Feb 24, 2016 171 172 `````` { apply wand_intro_l. eauto with I. } (* Now we come to the core of the proof: Updating from waiting to ress. *) `````` Ralf Jung committed Mar 06, 2016 173 174 175 `````` rewrite /ress sep_exist_r. apply exist_mono=>{Φ} Φ. ecancel [Π★{set I} (λ _, saved_prop_own _ _)]%I. strip_later. rewrite wand_True. eapply wand_apply_l'; eauto with I. `````` Robbert Krebbers committed Feb 24, 2016 176 177 178 ``````Qed. Lemma wait_spec l P (Φ : val → iProp) : `````` Ralf Jung committed Mar 04, 2016 179 `````` (recv l P ★ (P -★ Φ #())) ⊑ #> wait (%l) {{ Φ }}. `````` Robbert Krebbers committed Feb 24, 2016 180 181 182 183 184 185 ``````Proof. rename P into R. wp_rec. rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r. apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P. rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r. apply exist_elim=>i. rewrite -!assoc. apply const_elim_sep_l=>?. `````` Robbert Krebbers committed Mar 03, 2016 186 `````` wp_focus (! _)%E. `````` Robbert Krebbers committed Feb 24, 2016 187 188 189 `````` (* I think some evars here are better than repeating *everything* *) eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl; eauto with I ndisj. `````` Ralf Jung committed Mar 06, 2016 190 `````` ecancel [sts_ownS γ _ _]. `````` Robbert Krebbers committed Feb 24, 2016 191 192 193 194 `````` apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc. apply const_elim_sep_l=>Hs. rewrite {1}/barrier_inv =>/=. rewrite later_sep. eapply wp_load; eauto with I ndisj. `````` Ralf Jung committed Mar 06, 2016 195 `````` ecancel [▷ l ↦{_} _]%I. strip_later. `````` Robbert Krebbers committed Feb 24, 2016 196 197 198 199 200 201 202 203 204 205 `````` apply wand_intro_l. destruct p. { (* a Low state. The comparison fails, and we recurse. *) rewrite -(exist_intro (State Low I)) -(exist_intro {[ Change i ]}). rewrite [(■ sts.steps _ _ )%I]const_equiv /=; last by apply rtc_refl. rewrite left_id -[(▷ barrier_inv _ _ _)%I]later_intro {3}/barrier_inv. rewrite -!assoc. apply sep_mono_r, sep_mono_r, wand_intro_l. wp_op; first done. intros _. wp_if. rewrite !assoc. rewrite -always_wand_impl always_elim. rewrite -{2}pvs_wp. apply pvs_wand_r. rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro Q) -(exist_intro i). `````` Ralf Jung committed Mar 06, 2016 206 207 `````` rewrite const_equiv // left_id -later_intro. ecancel_pvs [heap_ctx _; saved_prop_own _ _; Q -★ _; R -★ _; sts_ctx _ _ _]%I. `````` Robbert Krebbers committed Feb 24, 2016 208 209 210 211 212 213 214 215 216 `````` apply sts_own_weaken; eauto using i_states_closed. } (* a High state: the comparison succeeds, and we perform a transition and return to the client *) rewrite [(_ ★ □ (_ → _ ))%I]sep_elim_l. rewrite -(exist_intro (State High (I ∖ {[ i ]}))) -(exist_intro ∅). change (i ∈ I) in Hs. rewrite const_equiv /=; last by eauto using wait_step. rewrite left_id -[(▷ barrier_inv _ _ _)%I]later_intro {2}/barrier_inv. rewrite -!assoc. apply sep_mono_r. rewrite /ress. `````` 217 `````` rewrite !sep_exist_r. apply exist_mono=>Ψ. `````` Ralf Jung committed Mar 06, 2016 218 219 220 221 222 223 `````` rewrite !(big_sepS_delete _ I i) //= !wand_True later_sep. ecancel [▷ Π★{set _} Ψ; Π★{set _} (λ _, saved_prop_own _ _)]%I. apply wand_intro_l. set savedΨ := _ i _. set savedQ := _ i _. to_front [savedΨ; savedQ]. rewrite saved_prop_agree later_equivI /=. wp_op; [|done]=> _. wp_if. rewrite !assoc. eapply wand_apply_r'; first done. eapply wand_apply_r'; first done. `````` 224 `````` apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); by eauto with I. `````` Robbert Krebbers committed Feb 24, 2016 225 226 ``````Qed. `````` Ralf Jung committed Mar 01, 2016 227 228 229 ``````Lemma recv_split E l P1 P2 : nclose N ⊆ E → recv l (P1 ★ P2) ⊑ |={E}=> recv l P1 ★ recv l P2. `````` Robbert Krebbers committed Feb 24, 2016 230 ``````Proof. `````` Ralf Jung committed Mar 01, 2016 231 232 `````` rename P1 into R1. rename P2 into R2. intros HN. rewrite {1}/recv /barrier_ctx. `````` Robbert Krebbers committed Feb 24, 2016 233 `````` apply exist_elim=>γ. rewrite sep_exist_r. apply exist_elim=>P. `````` Ralf Jung committed Mar 01, 2016 234 235 `````` apply exist_elim=>Q. apply exist_elim=>i. rewrite -!assoc. apply const_elim_sep_l=>?. rewrite -pvs_trans'. `````` Robbert Krebbers committed Feb 24, 2016 236 `````` (* I think some evars here are better than repeating *everything* *) `````` Ralf Jung committed Mar 01, 2016 237 `````` eapply pvs_mk_fsa, (sts_fsaS _ pvs_fsa) with (N0:=N) (γ0:=γ); simpl; `````` Robbert Krebbers committed Feb 24, 2016 238 `````` eauto with I ndisj. `````` Ralf Jung committed Mar 06, 2016 239 `````` ecancel [sts_ownS γ _ _]. `````` Robbert Krebbers committed Feb 24, 2016 240 `````` apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc. `````` Ralf Jung committed Mar 01, 2016 241 `````` apply const_elim_sep_l=>Hs. rewrite /pvs_fsa. `````` Robbert Krebbers committed Feb 24, 2016 242 `````` eapply sep_elim_True_l. `````` Robbert Krebbers committed Mar 02, 2016 243 `````` { eapply saved_prop_alloc_strong with (x := Next R1) (G := I). } `````` Robbert Krebbers committed Feb 24, 2016 244 245 246 `````` rewrite pvs_frame_r. apply pvs_strip_pvs. rewrite sep_exist_r. apply exist_elim=>i1. rewrite always_and_sep_l. rewrite -assoc. apply const_elim_sep_l=>Hi1. eapply sep_elim_True_l. `````` Robbert Krebbers committed Mar 02, 2016 247 `````` { eapply saved_prop_alloc_strong with (x := Next R2) (G := I ∪ {[ i1 ]}). } `````` Robbert Krebbers committed Feb 24, 2016 248 249 250 251 `````` rewrite pvs_frame_r. apply pvs_mono. rewrite sep_exist_r. apply exist_elim=>i2. rewrite always_and_sep_l. rewrite -assoc. apply const_elim_sep_l=>Hi2. rewrite ->not_elem_of_union, elem_of_singleton in Hi2. `````` 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 `````` destruct Hi2 as [Hi2 Hi12]. change (i ∈ I) in Hs. (* Update to new state. *) rewrite -(exist_intro (State p ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))))). rewrite -(exist_intro ({[Change i1 ]} ∪ {[ Change i2 ]})). rewrite [(■ sts.steps _ _)%I]const_equiv; last by eauto using split_step. rewrite left_id {1 3}/barrier_inv. (* FIXME ssreflect rewrite fails if there are evars around. Also, this is very slow because we don't have a proof mode. *) rewrite -(ress_split _ _ _ Q R1 R2); [|done..]. rewrite {1}[saved_prop_own i1 _]always_sep_dup. rewrite {1}[saved_prop_own i2 _]always_sep_dup !later_sep. rewrite -![(▷ saved_prop_own _ _)%I]later_intro. ecancel [▷ l ↦ _; saved_prop_own i1 _; saved_prop_own i2 _ ; ▷ ress _ _ ; ▷ (Q -★ _) ; saved_prop_own i _]%I. apply wand_intro_l. rewrite !assoc. rewrite /recv. rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R1) -(exist_intro i1). rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R2) -(exist_intro i2). `````` Ralf Jung committed Mar 06, 2016 268 269 270 271 272 273 274 275 276 `````` rewrite [heap_ctx _]always_sep_dup [sts_ctx _ _ _]always_sep_dup. rewrite /barrier_ctx const_equiv // left_id. ecancel_pvs [saved_prop_own i1 _; saved_prop_own i2 _; heap_ctx _; heap_ctx _; sts_ctx _ _ _; sts_ctx _ _ _]. rewrite !wand_diag later_True !right_id. rewrite -sts_ownS_op; eauto using i_states_closed. - apply sts_own_weaken; eauto using sts.closed_op, i_states_closed. set_solver. - set_solver. `````` Robbert Krebbers committed Feb 24, 2016 277 278 ``````Qed. `````` Ralf Jung committed Mar 01, 2016 279 ``````Lemma recv_weaken l P1 P2 : `````` Robbert Krebbers committed Feb 24, 2016 280 281 282 283 284 `````` (P1 -★ P2) ⊑ (recv l P1 -★ recv l P2). Proof. apply wand_intro_l. rewrite /recv. rewrite sep_exist_r. apply exist_mono=>γ. rewrite sep_exist_r. apply exist_mono=>P. rewrite sep_exist_r. apply exist_mono=>Q. rewrite sep_exist_r. apply exist_mono=>i. `````` Ralf Jung committed Mar 06, 2016 285 286 `````` ecancel [barrier_ctx _ _ _; sts_ownS _ _ _; saved_prop_own _ _]. strip_later. apply wand_intro_l. by rewrite !assoc wand_elim_r wand_elim_r. `````` Robbert Krebbers committed Feb 24, 2016 287 ``````Qed. `````` Ralf Jung committed Feb 29, 2016 288 289 290 291 `````` Lemma recv_mono l P1 P2 : P1 ⊑ P2 → recv l P1 ⊑ recv l P2. Proof. `````` Ralf Jung committed Mar 01, 2016 292 `````` intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken. `````` Ralf Jung committed Feb 29, 2016 293 294 ``````Qed. `````` Robbert Krebbers committed Feb 24, 2016 295 ``End proof.``