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

heap_lang/par.v

@@ -25,19 +25,15 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊑ #> par e {{ Φ }}.
 Proof.
-  intros. rewrite /par.
-  wp_focus e. etransitivity; last by eapply wp_value. wp_let.
-  (* FIXME: wp_proj should not spawn these goals. *)
-  wp_proj; eauto using to_of_val.
-  ewp eapply spawn_spec; eauto using to_of_val.
-  apply sep_mono_r. apply sep_mono_r.
-  apply forall_intro=>h. apply wand_intro_l. wp_let.
-  wp_proj; eauto using to_of_val.
+  intros. rewrite /par. ewp (by eapply wp_value). wp_let. wp_proj.
+  ewp (eapply spawn_spec; wp_done).
+  apply sep_mono_r, sep_mono_r.
+  apply forall_intro=>h. apply wand_intro_l. wp_let. wp_proj.
   wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. apply wp_mono=>v2. wp_let.
-  ewp eapply join_spec; eauto using to_of_val. apply sep_mono_r.
-  apply forall_intro=>v1. apply wand_intro_l. 
+  ewp (by eapply join_spec).
+  apply sep_mono_r, forall_intro=>v1; apply wand_intro_l.
   rewrite (forall_elim v1) (forall_elim v2). rewrite assoc wand_elim_r.
-  wp_let. eapply wp_value, to_val_Pair; eapply to_of_val.
+  wp_let. apply wp_value; wp_done.
 Qed.
 
 Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
@@ -46,8 +42,6 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊑ #> ParV e1 e2 {{ Φ }}.
 Proof.
-  intros. rewrite -par_spec //. apply sep_mono_r.
-  apply sep_mono; last apply sep_mono_l; by wp_seq.
+  intros. rewrite -par_spec //. repeat apply sep_mono; done || by wp_seq.
 Qed.
-
 End proof.

heap_lang/spawn.v

@@ -53,14 +53,11 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
   (heap_ctx heapN ★ #> f #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ (%l))
   ⊑ #> spawn e {{ Φ }}.
 Proof.
-  intros Hval Hdisj. rewrite /spawn.
-  (* TODO: Make this more convenient. *)
-  wp_focus e. etransitivity; last by eapply wp_value. wp_let.
-  (* FIXME: can we change the ewp notation so that the parentheses become unnecessary? *)
-  (ewp eapply wp_alloc); eauto with I. strip_later.
+  intros Hval Hdisj. rewrite /spawn. ewp (by eapply wp_value). wp_let.
+  wp eapply wp_alloc; eauto with I.
   apply forall_intro=>l. apply wand_intro_l. wp_let.
   rewrite (forall_elim l). eapply sep_elim_True_l.
-  { eapply (own_alloc (Excl ())). done. }
+  { by eapply (own_alloc (Excl ())). }
   rewrite !pvs_frame_r. eapply wp_strip_pvs. rewrite !sep_exist_r.
   apply exist_elim=>γ.
   (* TODO: Figure out a better way to say "I want to establish ▷ spawn_inv". *)
@@ -68,7 +65,7 @@ Proof.
          own γ (Excl ()) ★ ▷ (spawn_inv γ l Ψ))%I.
   { ecancel [ #> _ {{ _ }}; _ -★ _; heap_ctx _; own _ _]%I.
     rewrite -later_intro /spawn_inv -(exist_intro (InjLV #0)).
-    cancel [l ↦ InjLV #0]%I. apply or_intro_l'. by rewrite const_equiv. }
+    cancel [l ↦ InjLV #0]%I. by apply or_intro_l', const_intro. }
   rewrite (inv_alloc N) // !pvs_frame_l. eapply wp_strip_pvs.
   ewp eapply wp_fork. rewrite [heap_ctx _]always_sep_dup [inv _ _]always_sep_dup.
   sep_split left: [_ -★ _; inv _ _; own _ _; heap_ctx _]%I.
@@ -104,7 +101,7 @@ Proof.
   cancel [l ↦ lv]%I. rewrite sep_or_r. apply or_elim.
   - (* Case 1 : nothing sent yet, we wait. *)
     rewrite -or_intro_l. apply const_elim_sep_l=>-> {lv}.
-    do 2 rewrite const_equiv // left_id. wp_case; eauto.
+    do 2 rewrite const_equiv // left_id. wp_case.
     wp_seq. rewrite -always_wand_impl always_elim.
     rewrite !assoc. eapply wand_apply_r'; first done.
     rewrite -(exist_intro γ). solve_sep_entails.
@@ -115,8 +112,7 @@ Proof.
       rewrite [(heap_ctx _ ★ _)%I]sep_elim_r !assoc. rewrite -own_op own_valid_l.
       rewrite -!assoc discrete_valid. apply const_elim_sep_l=>-[]. }
     rewrite -or_intro_r. ecancel [own _ _].
-    wp_case; eauto using to_of_val.
-    wp_let. etransitivity; last by eapply wp_value, to_of_val.
+    wp_case. wp_let. ewp (eapply wp_value; wp_done).
     rewrite (forall_elim v). rewrite !assoc. eapply wand_apply_r'; eauto with I.
 Qed.
 

heap_lang/wp_tactics.v

@@ -21,6 +21,8 @@ Ltac wp_finish :=
   | _ => idtac
   end in simpl; intros_revert go.
 
+Ltac wp_done := rewrite -/of_val /= ?to_of_val; fast_done.
+
 Tactic Notation "wp_rec" ">" :=
   löb ltac:(
     (* Find the redex and apply wp_rec *)
@@ -30,9 +32,7 @@ Tactic Notation "wp_rec" ">" :=
       match eval hnf in e' with App ?e1 _ =>
 (* hnf does not reduce through an of_val *)
 (*      match eval hnf in e1 with Rec _ _ _ => *)
-      wp_bind K; etrans;
-         [|eapply wp_rec'; repeat rewrite /= to_of_val; fast_done];
-         simpl_subst; wp_finish
+      wp_bind K; etrans; [|eapply wp_rec'; wp_done]; simpl_subst; wp_finish
 (*      end *) end)
      end).
 Tactic Notation "wp_rec" := wp_rec>; try strip_later.
@@ -42,9 +42,7 @@ Tactic Notation "wp_lam" ">" :=
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with App ?e1 _ =>
 (*    match eval hnf in e1 with Rec BAnon _ _ => *)
-    wp_bind K; etrans;
-       [|eapply wp_lam; repeat (fast_done || rewrite /= to_of_val)];
-       simpl_subst; wp_finish
+    wp_bind K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
 (*    end *) end)
   end.
 Tactic Notation "wp_lam" := wp_lam>; try strip_later.
@@ -73,10 +71,8 @@ Tactic Notation "wp_proj" ">" :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
-    | Fst _ =>
-       wp_bind K; etrans; [|eapply wp_fst; try fast_done]; wp_finish
-    | Snd _ =>
-       wp_bind K; etrans; [|eapply wp_snd; try fast_done]; wp_finish
+    | Fst _ => wp_bind K; etrans; [|eapply wp_fst; wp_done]; wp_finish
+    | Snd _ => wp_bind K; etrans; [|eapply wp_snd; wp_done]; wp_finish
     end)
   end.
 Tactic Notation "wp_proj" := wp_proj>; try strip_later.
@@ -95,8 +91,9 @@ Tactic Notation "wp_case" ">" :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with Case _ _ _ =>
-    wp_bind K;
-    etrans; [|eapply wp_case_inl || eapply wp_case_inr]; wp_finish
+      wp_bind K;
+      etrans; [|first[eapply wp_case_inl; wp_done|eapply wp_case_inr; wp_done]];
+      wp_finish
     end)
   end.
 Tactic Notation "wp_case" := wp_case>; try strip_later.