proof.v 14.2 KB
Newer Older
 Robbert Krebbers committed Feb 24, 2016 1 2 3 4 5 ``````From prelude Require Import functions. From algebra Require Import upred_big_op upred_tactics. From program_logic Require Import sts saved_prop. 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 9 10 11 12 ``````Import uPred. (** The monoids we need. *) (* Not bundling heapG, as it may be shared with other users. *) Class barrierG Σ := BarrierG { barrier_stsG :> stsG heap_lang Σ sts; `````` Robbert Krebbers committed Mar 02, 2016 13 `````` barrier_savedPropG :> savedPropG heap_lang Σ idCF; `````` Robbert Krebbers committed Feb 24, 2016 14 ``````}. `````` Robbert Krebbers committed Mar 02, 2016 15 ``````Definition barrierGF : rFunctors := [stsGF sts; agreeRF idCF]. `````` Robbert Krebbers committed Feb 24, 2016 16 17 `````` Instance inGF_barrierG `````` Robbert Krebbers committed Mar 02, 2016 18 `````` `{inGF heap_lang Σ (stsGF sts), inGF heap_lang Σ (agreeRF idCF)} : barrierG Σ. `````` Robbert Krebbers committed Feb 24, 2016 19 20 21 22 ``````Proof. split; apply _. Qed. (** 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 53 `````` saved_prop_own i (Next Q) ★ ▷ (Q -★ R))%I. Implicit Types I : gset gname. `````` Robbert Krebbers committed Feb 24, 2016 54 55 `````` (** Setoids *) `````` 56 57 58 59 ``````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 60 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Feb 24, 2016 61 ``````Global Instance barrier_inv_ne n l : `````` Ralf Jung committed Feb 25, 2016 62 63 `````` Proper (dist n ==> eq ==> dist n) (barrier_inv l). Proof. solve_proper. Qed. `````` Robbert Krebbers committed Feb 24, 2016 64 ``````Global Instance barrier_ctx_ne n γ l : Proper (dist n ==> dist n) (barrier_ctx γ l). `````` Ralf Jung committed Feb 25, 2016 65 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Feb 24, 2016 66 ``````Global Instance send_ne n l : Proper (dist n ==> dist n) (send l). `````` Ralf Jung committed Feb 25, 2016 67 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Feb 24, 2016 68 ``````Global Instance recv_ne n l : Proper (dist n ==> dist n) (recv l). `````` Ralf Jung committed Feb 25, 2016 69 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Feb 24, 2016 70 71 `````` (** Helper lemmas *) `````` 72 ``````Lemma ress_split i i1 i2 Q R1 R2 P I : `````` Robbert Krebbers committed Feb 24, 2016 73 `````` i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 → `````` Robbert Krebbers committed Mar 02, 2016 74 75 `````` (saved_prop_own i2 (Next R2) ★ saved_prop_own i1 (Next R1) ★ saved_prop_own i (Next Q) ★ `````` 76 77 `````` (Q -★ R1 ★ R2) ★ ress P I) ⊑ ress P ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))). `````` Robbert Krebbers committed Feb 24, 2016 78 ``````Proof. `````` 79 `````` intros. rewrite /ress !sep_exist_l. apply exist_elim=>Ψ. `````` Robbert Krebbers committed Feb 24, 2016 80 81 82 83 `````` 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 84 85 86 87 `````` 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 88 `````` rewrite (big_sepS_delete _ I i) //. `````` Ralf Jung committed Mar 05, 2016 89 `````` sep_split right: [Π★{set _} _]%I. `````` Robbert Krebbers committed Feb 24, 2016 90 91 92 93 `````` + 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 94 95 96 `````` + 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 97 98 99 100 `````` - 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 101 ``````Qed. `````` Robbert Krebbers committed Feb 24, 2016 102 103 `````` (** Actual proofs *) `````` Ralf Jung committed Feb 28, 2016 104 ``````Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) : `````` Robbert Krebbers committed Feb 24, 2016 105 `````` heapN ⊥ N → `````` Ralf Jung committed Mar 02, 2016 106 `````` (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (%l)) `````` Ralf Jung committed Mar 04, 2016 107 `````` ⊑ #> newbarrier #() {{ Φ }}. `````` Robbert Krebbers committed Feb 24, 2016 108 ``````Proof. `````` Ralf Jung committed Feb 28, 2016 109 `````` intros HN. rewrite /newbarrier. wp_seq. `````` Robbert Krebbers committed Feb 24, 2016 110 111 112 113 `````` 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 02, 2016 114 `````` eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=idCF) _ (Next P)). `````` Robbert Krebbers committed Feb 24, 2016 115 116 `````` rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l. apply exist_elim=>i. `````` Robbert Krebbers committed Mar 02, 2016 117 118 `````` trans (pvs ⊤ ⊤ (heap_ctx heapN ★ ▷ (barrier_inv l P (State Low {[ i ]})) ★ saved_prop_own i (Next P))). `````` Robbert Krebbers committed Feb 24, 2016 119 `````` - rewrite -pvs_intro. cancel [heap_ctx heapN]. `````` Robbert Krebbers committed Mar 02, 2016 120 `````` rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i (Next P)]. `````` 121 `````` rewrite /barrier_inv /ress -later_intro. cancel [l ↦ #0]%I. `````` Robbert Krebbers committed Feb 24, 2016 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 `````` 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 γ). (* This is even more annoying than usually, since rewrite sometimes unfolds stuff... *) rewrite [barrier_ctx _ _ _]lock !assoc [(_ ★ locked (barrier_ctx _ _ _))%I]comm !assoc -lock. rewrite -always_sep_dup. (* TODO: This is cancelling below a pvs. *) rewrite [barrier_ctx _ _ _]lock always_and_sep_l -!assoc assoc -lock. rewrite -pvs_frame_l. rewrite /barrier_ctx const_equiv // left_id. apply sep_mono_r. rewrite [(saved_prop_own _ _ ★ _)%I]comm !assoc. rewrite -pvs_frame_r. apply sep_mono_l. rewrite -assoc [(▷ _ ★ _)%I]comm assoc -pvs_frame_r. eapply sep_elim_True_r; last eapply sep_mono_l. { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. } 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 147 148 `````` + intros []; set_solver. + set_solver. `````` Robbert Krebbers committed Feb 24, 2016 149 150 151 152 `````` + 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 153 `````` (send l P ★ P ★ Φ #()) ⊑ #> signal (%l) {{ Φ }}. `````` Robbert Krebbers committed Feb 24, 2016 154 155 156 157 158 159 160 161 162 163 ``````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. rewrite !assoc [(_ ★ sts_ownS _ _ _)%I]comm -!assoc. apply sep_mono_r. 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 164 165 `````` eapply wp_store with (v' := #0); eauto with I ndisj. strip_later. cancel [l ↦ #0]%I. `````` Robbert Krebbers committed Feb 24, 2016 166 167 168 169 170 171 172 `````` 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. rewrite !assoc [(_ ★ P)%I]comm !assoc -2!assoc. 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. *) `````` 173 174 `````` rewrite /ress sep_exist_l. apply exist_mono=>{Φ} Φ. rewrite later_wand {1}(later_intro P) !assoc wand_elim_r /= wand_True //. `````` Robbert Krebbers committed Feb 24, 2016 175 176 177 ``````Qed. Lemma wait_spec l P (Φ : val → iProp) : `````` Ralf Jung committed Mar 04, 2016 178 `````` (recv l P ★ (P -★ Φ #())) ⊑ #> wait (%l) {{ Φ }}. `````` Robbert Krebbers committed Feb 24, 2016 179 180 181 182 183 184 ``````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 185 `````` wp_focus (! _)%E. `````` Robbert Krebbers committed Feb 24, 2016 186 187 188 189 190 191 192 193 `````` (* I think some evars here are better than repeating *everything* *) eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl; eauto with I ndisj. rewrite !assoc [(_ ★ sts_ownS _ _ _)%I]comm -!assoc. apply sep_mono_r. 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. `````` Robbert Krebbers committed Feb 25, 2016 194 `````` rewrite -!assoc. apply sep_mono_r. strip_later. `````` Robbert Krebbers committed Feb 24, 2016 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 `````` 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). rewrite !assoc. do 3 (rewrite -pvs_frame_r; apply sep_mono; last (try apply later_intro; reflexivity)). rewrite [(_ ★ heap_ctx _)%I]comm -!assoc. rewrite const_equiv // left_id -pvs_frame_l. apply sep_mono_r. rewrite comm -pvs_frame_l. apply sep_mono_r. 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. `````` 219 220 221 222 `````` rewrite !sep_exist_r. apply exist_mono=>Ψ. rewrite !(big_sepS_delete _ I i) // [(_ ★ Π★{set _} _)%I]comm -!assoc. rewrite /= !wand_True later_sep. ecancel [▷ Π★{set _} _; Π★{set _} (λ _, saved_prop_own _ _)]%I. `````` Robbert Krebbers committed Feb 24, 2016 223 224 `````` apply wand_intro_l. rewrite [(heap_ctx _ ★ _)%I]sep_elim_r. rewrite [(sts_own _ _ _ ★ _)%I]sep_elim_r [(sts_ctx _ _ _ ★ _)%I]sep_elim_r. `````` 225 `````` rewrite [(saved_prop_own _ _ ★ _ ★ _)%I]assoc. `````` Robbert Krebbers committed Mar 02, 2016 226 `````` rewrite saved_prop_agree later_equivI /=. `````` 227 `````` wp_op; [|done]=> _. wp_if. rewrite !assoc. `````` Robbert Krebbers committed Feb 24, 2016 228 `````` eapply wand_apply_r; [done..|]. eapply wand_apply_r; [done..|]. `````` 229 `````` apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); by eauto with I. `````` Robbert Krebbers committed Feb 24, 2016 230 231 ``````Qed. `````` Ralf Jung committed Mar 01, 2016 232 233 234 ``````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 235 ``````Proof. `````` Ralf Jung committed Mar 01, 2016 236 237 `````` rename P1 into R1. rename P2 into R2. intros HN. rewrite {1}/recv /barrier_ctx. `````` Robbert Krebbers committed Feb 24, 2016 238 `````` apply exist_elim=>γ. rewrite sep_exist_r. apply exist_elim=>P. `````` Ralf Jung committed Mar 01, 2016 239 240 `````` apply exist_elim=>Q. apply exist_elim=>i. rewrite -!assoc. apply const_elim_sep_l=>?. rewrite -pvs_trans'. `````` Robbert Krebbers committed Feb 24, 2016 241 `````` (* I think some evars here are better than repeating *everything* *) `````` Ralf Jung committed Mar 01, 2016 242 `````` eapply pvs_mk_fsa, (sts_fsaS _ pvs_fsa) with (N0:=N) (γ0:=γ); simpl; `````` Robbert Krebbers committed Feb 24, 2016 243 244 245 `````` eauto with I ndisj. rewrite !assoc [(_ ★ sts_ownS _ _ _)%I]comm -!assoc. apply sep_mono_r. apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc. `````` Ralf Jung committed Mar 01, 2016 246 `````` apply const_elim_sep_l=>Hs. rewrite /pvs_fsa. `````` Robbert Krebbers committed Feb 24, 2016 247 `````` eapply sep_elim_True_l. `````` Robbert Krebbers committed Mar 02, 2016 248 `````` { eapply saved_prop_alloc_strong with (x := Next R1) (G := I). } `````` Robbert Krebbers committed Feb 24, 2016 249 250 251 `````` 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 252 `````` { eapply saved_prop_alloc_strong with (x := Next R2) (G := I ∪ {[ i1 ]}). } `````` Robbert Krebbers committed Feb 24, 2016 253 254 255 256 `````` 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. `````` 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 `````` 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). do 2 rewrite !(assoc (★)%I) [(_ ★ sts_ownS _ _ _)%I]comm. rewrite -!assoc. rewrite [(sts_ownS _ _ _ ★ _ ★ _)%I]assoc. rewrite -pvs_frame_r. apply sep_mono. - 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. - rewrite const_equiv // !left_id. rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup. rewrite !wand_diag -!later_intro. solve_sep_entails. `````` Robbert Krebbers committed Feb 24, 2016 283 284 ``````Qed. `````` Ralf Jung committed Mar 01, 2016 285 ``````Lemma recv_weaken l P1 P2 : `````` Robbert Krebbers committed Feb 24, 2016 286 287 288 289 290 291 292 293 294 `````` (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. rewrite -!assoc. apply sep_mono_r, sep_mono_r, sep_mono_r, sep_mono_r, sep_mono_r. rewrite (later_intro (P1 -★ _)%I) -later_sep. apply later_mono. apply wand_intro_l. by rewrite !assoc wand_elim_r wand_elim_r. Qed. `````` Ralf Jung committed Feb 29, 2016 295 296 297 298 `````` Lemma recv_mono l P1 P2 : P1 ⊑ P2 → recv l P1 ⊑ recv l P2. Proof. `````` Ralf Jung committed Mar 01, 2016 299 `````` intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken. `````` Ralf Jung committed Feb 29, 2016 300 301 ``````Qed. `````` Robbert Krebbers committed Feb 24, 2016 302 ``End proof.``