Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

docs/derived.tex

@@ -176,8 +176,8 @@ The following rules can be derived for Hoare triples.
   {\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask]}
 \and
 \inferH{Ht-frame-step}
-  {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot}
-  {\hoare{\prop * \later\propC}{\expr}{\Ret\val. \propB * \propC}[\mask]}
+  {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot \and \mask_2 \subseteq \mask_2 \\\\ \propC_1 \vs[\mask_1][\mask_2] \later\propC_2 \and \propC_2 \vs[\mask_2][\mask_1] \propC_3}
+  {\hoare{\prop * \propC_1}{\expr}{\Ret\val. \propB * \propC_3}[\mask \uplus \mask_1]}
 \and
 \inferH{Ht-atomic}
   {\prop \vs[\mask \uplus \mask'][\mask] \prop' \\

docs/logic.tex

@@ -584,8 +584,8 @@ This is entirely standard.
 {}{\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
 
 \infer[wp-frame-step]
-{\toval(\expr) = \bot}
-{\later\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
+{\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}
+{\wpre\expr[\mask]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\mask \uplus \mask_1]{\Ret\var.\propB*\prop}}
 
 \infer[wp-bind]
 {\text{$\lctx$ is a context}}

heap_lang/lifting.v

@@ -28,12 +28,13 @@ Lemma wp_alloc_pst E σ e v Φ :
   (▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l)))
   ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
+  iIntros {?}  "[HP HΦ]".
   (* TODO: This works around ssreflect bug #22. *)
-  intros. set (φ (e' : expr []) σ' ef := ∃ l,
+  set (φ (e' : expr []) σ' ef := ∃ l,
     ef = None ∧ e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
-  rewrite -(wp_lift_atomic_head_step (Alloc e) φ σ) // /φ;
-    last (by intros; inv_head_step; eauto 8); last (by simpl; eauto).
-  iIntros  "[$ HΦ] >"; iIntros {v2 σ2 ef} "[% HP]".
+  iApply (wp_lift_atomic_head_step (Alloc e) φ σ); try (by simpl; eauto);
+    [by intros; subst φ; inv_head_step; eauto 8|].
+  iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]".
   (* FIXME: I should not have to refer to "H0". *)
   destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
   iSplit; last done. iApply "HΦ"; by iSplit.