un-curry "par"; add wp_tactics for case and projections

heap_lang/par.v

@@ -3,12 +3,12 @@ From heap_lang Require Import wp_tactics notation.
 Import uPred.
 
 Definition par : val :=
-  λ: "f1" "f2", let: "handle" := ^spawn '"f1" in
-                let: "v2" := '"f2" #() in
-                let: "v1" := ^join '"handle" in
-                Pair '"v1" '"v2".
-Notation Par e1 e2 := (^par (λ: <>, e1) (λ: <>, e2))%E.
-Notation ParV e1 e2 := (par (λ: <>, e1) (λ: <>, e2))%E.
+  λ: "fs", let: "handle" := ^spawn (Fst '"fs") in
+           let: "v2" := Snd '"fs" #() in
+           let: "v1" := ^join '"handle" in
+           Pair '"v1" '"v2".
+Notation Par e1 e2 := (^par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
+Notation ParV e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
 (* We want both par and par^ to print like this. *)
 Infix "||" := ParV : expr_scope.
 Infix "||" := Par : expr_scope.
@@ -18,21 +18,21 @@ Context {Σ : rFunctorG} `{!heapG Σ, !spawnG Σ}.
 Context (heapN N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
 
-Lemma par_spec (Ψ1 Ψ2 : val → iProp) e1 e2 (f1 f2 : val) (Φ : val → iProp) :
-  heapN ⊥ N → to_val e1 = Some f1 → to_val e2 = Some f2 →
-  (* TODO like in spawn.v -- wp about e or f? *)
-  (heap_ctx heapN ★ #> e1 #() {{ Ψ1 }} ★ #> e2 #() {{ Ψ2 }} ★
+Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
+  heapN ⊥ N → to_val e = Some (PairV f1 f2) →
+  (heap_ctx heapN ★ #> f1 #() {{ Ψ1 }} ★ #> f2 #() {{ Ψ2 }} ★
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ Φ (PairV v1 v2))
-  ⊑ #> par e1 e2 {{ Φ }}.
+  ⊑ #> par e {{ Φ }}.
 Proof.
   intros. rewrite /par.
-  wp_focus e1. etransitivity; last by eapply wp_value. wp_let.
-  wp_focus e2. etransitivity; last by eapply wp_value. wp_let.
+  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. rewrite (of_to_val e1) //. apply sep_mono_r.
+  apply sep_mono_r. apply sep_mono_r.
   apply forall_intro=>h. apply wand_intro_l. wp_let.
-  wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. rewrite (of_to_val e2) //.
-  apply wp_mono=>v2. wp_let.
+  wp_proj; eauto using to_of_val.
+  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. wp_let.
   etransitivity; last by (eapply wp_value, to_val_Pair; eapply to_of_val).

heap_lang/spawn.v

@@ -45,8 +45,7 @@ Proof. solve_proper. Qed.
 Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
   to_val e = Some f →
   heapN ⊥ N →
-  (* TODO: Not sure whether the wp should be about [e] or [f]. Both work. *)
-  (heap_ctx heapN ★ #> e #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ (%l))
+  (heap_ctx heapN ★ #> f #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ (%l))
   ⊑ #> spawn e {{ Φ }}.
 Proof.
   intros Hval Hdisj. rewrite /spawn.
@@ -60,7 +59,7 @@ Proof.
   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". *)
-  trans (heap_ctx heapN ★ #> e #() {{ Ψ }} ★ (join_handle l Ψ -★ Φ (%l)%V) ★
+  trans (heap_ctx heapN ★ #> f #() {{ Ψ }} ★ (join_handle l Ψ -★ Φ (%l)%V) ★
          own γ (Excl ()) ★ ▷ (spawn_inv γ l Ψ))%I.
   { ecancel [ #> _ {{ _ }}; _ -★ _; heap_ctx _; own _ _]%I.
     rewrite -later_intro /spawn_inv -(exist_intro (InjLV #0)).
@@ -101,7 +100,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. (ewp eapply wp_case_inl); eauto.
+    do 2 rewrite const_equiv // left_id. wp_case; eauto.
     wp_seq. rewrite -always_wand_impl always_elim.
     rewrite !assoc. eapply wand_apply_r'; first done.
     rewrite -(exist_intro γ). solve_sep_entails.
@@ -112,7 +111,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 _ _].
-    (ewp apply: wp_case_inr); eauto using to_of_val.
+    wp_case; eauto using to_of_val.
     wp_let. etransitivity; last by eapply wp_value, to_of_val.
     rewrite (forall_elim v). rewrite !assoc. eapply wand_apply_r'; eauto with I.
 Qed.

heap_lang/wp_tactics.v

@@ -62,23 +62,45 @@ Tactic Notation "wp_op" ">" :=
     | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
     | BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish
     | BinOp _ _ _ =>
-       wp_bind K; etrans; [|fast_by eapply wp_bin_op]; wp_finish
+       wp_bind K; etrans; [|eapply wp_bin_op; try fast_done]; wp_finish
     | UnOp _ _ =>
-       wp_bind K; etrans; [|fast_by eapply wp_un_op]; wp_finish
+       wp_bind K; etrans; [|eapply wp_un_op; try fast_done]; wp_finish
     end)
   end.
 Tactic Notation "wp_op" := wp_op>; try strip_later.
 
+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
+    end)
+  end.
+Tactic Notation "wp_proj" := wp_proj>; try strip_later.
+
 Tactic Notation "wp_if" ">" :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with If _ _ _ =>
     wp_bind K;
-    etrans; [|apply wp_if_true || apply wp_if_false]; wp_finish
+    etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
     end)
   end.
 Tactic Notation "wp_if" := wp_if>; try strip_later.
 
+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
+    end)
+  end.
+Tactic Notation "wp_case" := wp_case>; try strip_later.
+
 Tactic Notation "wp_focus" open_constr(efoc) :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>