awp_apply tactic.

theories/c_translation/monad.v

@@ -66,6 +66,16 @@ End a_wp.
 Section a_wp_rules.
   Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapG Σ}.
 
+  Lemma a_wp_awp R Φ Ψ e : awp e R Φ -∗ (∀ v : val, awp v R Φ -∗ Ψ v) -∗ WP e {{ Ψ }}.
+  Proof.
+    iIntros "Hwp H". iApply (wp_wand with "Hwp").
+    iIntros (v) "Hwp". iApply "H". by iApply wp_value'.
+  Qed.
+
+  Lemma wp_awp_bind R Φ K e :
+    WP e {{ v, awp (fill K (of_val v)) R Φ }} ⊢ awp (fill K e) R Φ.
+  Proof. by apply: wp_bind. Qed.
+
   Lemma awp_ret e R Φ :
     WP e {{ Φ }} -∗ awp (a_ret e) R Φ.
   Proof.

theories/c_translation/proofmode.v

@@ -4,6 +4,30 @@ From iris_c.lib Require Import locking_heap mset flock.
 From iris_c.c_translation Require Export monad lifting.
 From iris.proofmode Require Import coq_tactics.
 
+Lemma tac_awp_bind `{locking_heapG Σ, heapG Σ, flockG Σ} K Δ R Φ e f :
+  f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
+  envs_entails Δ (WP e {{ v, awp (f (of_val v)) R Φ }})%I →
+  envs_entails Δ (awp (fill K e) R Φ).
+Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_awp_bind. Qed.
+
+Ltac awp_bind_core K :=
+  lazymatch eval hnf in K with
+  | [] => idtac
+  | _ => eapply (tac_awp_bind K); [simpl; reflexivity|lazy beta]
+  end.
+
+Tactic Notation "awp_apply" open_constr(lem) :=
+  iPoseProofCore lem as false true (fun H =>
+    lazymatch goal with
+    | |- envs_entails _ (awp ?e ?R ?Q) =>
+      reshape_expr e ltac:(fun K e' =>
+        awp_bind_core K; iApplyHyp H; try iNext (*; try wp_expr_simpl*) ) ||
+      lazymatch iTypeOf H with
+      | Some (_,?P) => fail "awp_apply: cannot apply" P
+      end
+    | _ => fail "awp_apply: not a 'awp'"
+    end).
+
 Lemma tac_awp_pure `{locking_heapG Σ, heapG Σ, flockG Σ} Δ Δ' K e1 e2 e φ R Φ :
   e = fill K e1 →
   PureExec φ e1 e2 →

theories/c_translation/translation.v

@@ -85,23 +85,14 @@ Section proofs.
       { rewrite -bi.big_sepM_insert_override; eauto. }
   Qed.
 
-  Lemma a_fill R Ψ Φ K e :
-    awp e R Ψ -∗
-    (∀ v : val, awp v R Ψ -∗ awp (fill K (of_val v)) R Φ) -∗
-    awp (fill K e) R Φ.
-  Proof.
-    iIntros "Hwp H". iApply wp_bind. iApply (wp_wand with "Hwp").
-    iIntros (v) "Hwp". iApply "H". iApply wp_value'. done.
-  Qed.
-
   Lemma a_sequence_spec R Φ (e1 e2 : expr) :
     AsVal e2 →
     awp e1 R (λ v, U (awp (e2 v) R Φ)) -∗
     awp (a_seq_bind e1 e2) R Φ.
   Proof.
     iIntros ([v2 <-%of_to_val]) "H".
-    iApply (a_fill _ _ _ [AppRCtx a_seq_bind; AppLCtx v2] with "H").
-    iIntros (v) "H /=". rewrite /a_seq_bind. awp_lam. awp_lam.
+    awp_apply (a_wp_awp with "H"); iIntros (v) "H".
+    rewrite /a_seq_bind /=. do 2 awp_lam.
     iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H".
     awp_lam. iApply awp_bind. iApply a_seq_spec.
     iModIntro. by awp_lam.
@@ -179,19 +170,11 @@ Section proofs.
     awp (a_store e1 e2) R Φ.
   Proof.
     iIntros "H1 H2 HΦ".
-    iApply (a_fill _ _ _ [AppRCtx a_store; AppLCtx e2] with "H1").
-    iIntros (v) "H1 /=".
-    rewrite /a_store. awp_lam.
-    iApply (a_fill _ _ _ [AppRCtx (LamV "x2" (
-(a_bind (λ: "vv", a_atomic_env (λ: "env", (mset_add (Fst "vv")) "env";; Fst "vv" <- Snd "vv";; Snd "vv")))
-     ((a_par v) "x2")
-)%E)] with "H2"). simpl. iIntros (v2) "H2". awp_lam.
-iApply awp_bind. iApply (awp_par with "H1 H2"). iNext.
-iIntros (w1 w2) "H1 H2".
-iDestruct "H1" as (l ->) "H1".
- iNext. awp_lam. clear v.
-iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]".
-
+    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
+    awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
+    iApply awp_bind. iApply (awp_par with "H1 H2").
+    iIntros "!>" (w1 w2) "H1 H2 !>". iDestruct "H1" as (l ->) "H1". awp_lam.
+    iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]".
     iApply awp_atomic_env.
     iIntros (env) "Henv HR".
     rewrite {2}/env_inv.