Simpler specifications for pre_bin_op

theories/c_translation/derived.v

@@ -58,6 +58,33 @@ Section derived.
       iApply ("HΦ" with "[$Hl] [$Hr]").
   Qed.
 
+  Lemma a_pre_bin_op_spec' R Φ Ψ1 Ψ2 e1 e2 op v l :
+    l ↦C v -∗
+    AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗
+    ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ⌜v1 = #l⌝ ∗
+          ∃ w, ⌜bin_op_eval op v v2 = Some w⌝
+          ∗ (l ↦C[LLvl] w -∗ Φ v)) -∗
+    AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
+  Proof.
+    iIntros "Hl He1 He2 HΦ".
+    iApply (a_pre_bin_op_spec with "He1 He2 [-]").
+    iNext. iIntros (v1 v2) "HΨ1 HΨ2 $".
+    iDestruct ("HΦ" with "HΨ1 HΨ2") as (->) "HΦ".
+    iDestruct "HΦ" as (w ?) "HΦ".
+    iExists _,_,_; iFrame. eauto.
+  Qed.
+
+  Lemma a_pre_incr R Φ e1 l (z : Z) :
+    l ↦C #z -∗
+    AWP e1 @ R {{ v, ⌜v = #l⌝ ∗ (l ↦C[LLvl] #(z+1) -∗ Φ #z) }} -∗
+    AWP e1 +=ᶜ ♯1 @ R {{ Φ }}.
+  Proof.
+    iIntros "Hl He1".
+    iApply (a_pre_bin_op_spec' _ _ _ (λ v, ⌜v = #1⌝)%I with "Hl He1 [] [-]").
+    { iApply awp_ret. by wp_value_head. }
+    iNext. iIntros (v1 v2) "[% HΦ] %". simplify_eq/=. eauto.
+  Qed.
+
   Lemma a_move_spec (s t :loc) (v w: val) R Φ :
     s ↦C v ∗ t ↦C w ∗ (t ↦C w -∗ s ↦C[LLvl] w -∗ Φ w) -∗
     awp (a_store (a_ret #s) (a_load (a_ret #t))) R Φ.

theories/tests/test1.v

@@ -147,4 +147,13 @@ Section test.
     repeat iSplit; eauto.
   Qed.
 
+  Lemma inc_test2 (l : loc) (z0 : Z) R:
+    l ↦C #z0 -∗
+    AWP ♯l +=ᶜ ♯1 @ R {{ v, ⌜v = #z0⌝ ∧ l ↦C[LLvl] #(z0+1) }}.
+  Proof.
+    iIntros "Hl".
+    iApply (a_pre_incr with "Hl").
+    iApply awp_ret; wp_value_head. iSplit; eauto.
+  Qed.
+
 End test.