Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0

barrier/lifting.v

@@ -21,21 +21,14 @@ Lemma wp_alloc_pst E σ e v Q :
   (ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
        ⊑ wp E (Alloc e) Q.
 Proof.
-  intros.
-  (* FIXME RJ: ssreflect rewrite does not work. *)
-  rewrite <-(wp_lift_atomic_step (Alloc e)
-    (λ v' σ', ∃ l, v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None) σ)=> //;
-    last first.
-  { (* TODO RJ: Somehow automation used to kill all this...?? *)
-    intros. inv_step. eexists; split_ands; try done; [].
-    eexists; done. }
+  intros. set (φ v' σ' := ∃ l, v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
+  rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
+    last by intros; inv_step; eauto 10.
   apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2; apply forall_intro=>σ2.
-  apply wand_intro_l.
+  apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
   rewrite always_and_sep_l' -associative -always_and_sep_l'.
   apply const_elim_l=>-[l [-> [-> ?]]].
-  rewrite (forall_elim l) const_equiv //.
-  by rewrite left_id wand_elim_r.
+  by rewrite (forall_elim l) const_equiv // left_id wand_elim_r.
 Qed.
 
 Lemma wp_load_pst E σ l v Q :