Strengthen `awp_par` and the store/binop/load rules

theories/c_translation/derived.v

@@ -35,7 +35,7 @@ Section derived.
                (λ w, ∃ v, (l ↦U v ∗ (l ↦L w -∗ Φ w)))%I ) with "[] [H] []").
     - iApply awp_ret; iApply wp_value; eauto.
     - done.
-    - iIntros (? w) "-> H". eauto with iFrame.
+    - iNext. iIntros (? w) "-> H". eauto with iFrame.
   Qed.
 
   Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.
@@ -53,7 +53,7 @@ Section derived.
           (λ x, ⌜x = v2⌝ ∧ r ↦U v2)%I  with "[Hl] [Hr] [HΦ]").
     - awp_load_ret l.
     - awp_load_ret r.
-    - iIntros (??) "[-> Hl] [-> Hr]".
+    - iNext. iIntros (??) "[-> Hl] [-> Hr]".
       iApply ("HΦ" with "[$Hl] [$Hr]").
   Qed.
 

theories/c_translation/monad.v

@@ -206,24 +206,23 @@ Section a_wp_rules.
     iIntros "Hunfl". wp_seq. iFrame.
   Qed.
 
-  Lemma awp_par (Ψ1 Ψ2 : val → iProp Σ) e1 e2 (ev1 ev2 : val) R (Φ : val → iProp Σ) :
-    IntoVal e1 ev1 →
-    IntoVal e2 ev2 →
-    awp ev1 R Ψ1 -∗
-    awp ev2 R Ψ2 -∗
+  Lemma awp_par (Ψ1 Ψ2 : val → iProp Σ) e1 e2 R (Φ : val → iProp Σ) :
+    awp e1 R Ψ1 -∗
+    ▷ awp e2 R Ψ2 -∗
     ▷ (∀ w1 w2, Ψ1 w1 -∗ Ψ2 w2 -∗ ▷ Φ (w1,w2)%V) -∗
     awp (a_par e1 e2) R Φ.
   Proof.
-    iIntros (<-%of_to_val <-%of_to_val) "Hwp1 Hwp2 HΦ".
-    rewrite /awp /a_par /=. do 2 wp_lam.
+    iIntros "Hwp1 Hwp2 HΦ". rewrite /a_par /awp /=.
+    wp_bind e1. iApply (wp_wand with "Hwp1").
+    iIntros (ev1) "Hwp1". wp_lam.
+    wp_bind e2. iApply (wp_wand with "Hwp2").
+    iIntros (ev2) "Hwp2". wp_lam.
     iIntros (γ π env l) "#Hlock #Hres [Hunfl1 Hunfl2]". do 2 wp_lam.
     iApply (par_spec (λ v, Ψ1 v ∗ unflocked _ (π/2))%I
                      (λ v, Ψ2 v ∗ unflocked _ (π/2))%I
       with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]").
-    - wp_lam. wp_apply (wp_wand with "Hwp1").
-      iIntros (v) "Hwp1". by iApply "Hwp1".
-    - wp_lam. wp_apply (wp_wand with "Hwp2").
-      iIntros (v) "Hwp2". by iApply "Hwp2".
+    - wp_lam. iApply ("Hwp1" with "Hlock Hres Hunfl1").
+    - wp_lam. iApply ("Hwp2" with "Hlock Hres Hunfl2").
     - iNext. iIntros (w1 w2) "[[HΨ1 $] [HΨ2 $]]".
       iApply ("HΦ" with "[$] [$]").
   Qed.

theories/c_translation/translation.v

@@ -88,8 +88,8 @@ Section proofs.
   Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
     awp e1 R (λ v, ∃ l : loc, ⌜v = #l⌝ ∧ Ψ1 l)-∗
     awp e2 R Ψ2 -∗
-    (∀ (l : loc) w,
-      Ψ1 l -∗ Ψ2 w -∗ (∃ v, l ↦U v ∗ (l ↦L w -∗ Φ w))) -∗
+    ▷ (∀ (l : loc) w,
+        Ψ1 l -∗ Ψ2 w -∗ (∃ v, l ↦U v ∗ (l ↦L w -∗ Φ w))) -∗
     awp (a_store e1 e2) R Φ.
   Proof.
     iIntros "H1 H2 HΦ".
@@ -180,15 +180,15 @@ Section proofs.
 
   Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) :
     awp e1 R Ψ1 -∗ awp e2 R Ψ2 -∗
-    (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗
-         ∃ w, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w)-∗
+    ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗
+          ∃ w, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w)-∗
     awp (a_bin_op op e1 e2) R Φ.
   Proof.
     iIntros "H1 H2 HΦ".
     awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam.
     awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2". awp_lam.
     iApply awp_bind.
-    iApply ((awp_par Ψ1 Ψ2) with "HΨ1 HΨ2").
+    iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2").
     iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst.
     iNext. awp_lam. iApply awp_ret. do 2 wp_proj.
     iSpecialize ("HΦ" with "HΨ1 HΨ2").

theories/tests/fact.v

@@ -37,7 +37,7 @@ Section factorial_spec.
        (λ v,  ⌜v = #n⌝ ∗ l ↦U #n )%I (λ v,  ⌜v = #1⌝)%I with "[Hl] [] [HΦ]").
     + awp_load_ret l.
     + awp_ret_value.
-    + iIntros (? ?) "(% & Hc) %"; subst.
+    + iNext. iIntros (? ?) "(% & Hc) %"; subst.
       iExists #(n+1). iSplit; eauto with iFrame.
    Qed.
 
@@ -54,7 +54,7 @@ Section factorial_spec.
          (λ v,  ⌜v = #k⌝ ∧ c ↦U #k )%I (λ v, ⌜v = #n⌝)%I with "[Hc]").
     - awp_load_ret c.
     - awp_ret_value.
-    - iIntros (v1 v2) "[% Hc] %"; subst.
+    - iNext. iIntros (v1 v2) "[% Hc] %"; subst.
       rewrite /bin_op_eval /=. iExists _; iSplit; eauto.
       case_bool_decide.
       + iLeft. iSplit; eauto.
@@ -67,7 +67,7 @@ Section factorial_spec.
                      (λ v, ⌜v = #(k + 1)⌝ ∗ c ↦U #(k+1))%I with "[Hr] [Hc]").
           * awp_load_ret r.
           * awp_load_ret c.
-          * iIntros (? ?) "[% Hr] [% Hc]". simplify_eq.
+          * iNext. iIntros (? ?) "[% Hr] [% Hc]". simplify_eq.
             rewrite /bin_op_eval /=.
             assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
             { rewrite Nat.add_1_r /fact. lia. }
@@ -110,7 +110,7 @@ Section factorial_spec.
          (λ v,  ⌜v = #k⌝ ∧ c ↦U #k )%I (λ v, ⌜v = #n⌝)%I with "[Hc]").
       + awp_load_ret c.
       + awp_ret_value.
-      + iIntros (v1 v2) "[% Hc] %"; subst.
+      + iNext. iIntros (v1 v2) "[% Hc] %"; subst.
         rewrite /bin_op_eval /=. iExists _; iSplit; eauto.
         case_bool_decide.
         * iRight. iSplit; eauto.
@@ -123,7 +123,7 @@ Section factorial_spec.
                      (λ v, ⌜v = #(k + 1)⌝ ∗ c ↦U #(k+1))%I with "[Hr] [Hc]").
           ** awp_load_ret r.
           ** awp_load_ret c.
-          ** iIntros (? ?) "[% Hr] [% Hc]". simplify_eq.
+          ** iNext. iIntros (? ?) "[% Hr] [% Hc]". simplify_eq.
             rewrite /bin_op_eval /=.
             assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
             { rewrite Nat.add_1_r /fact. lia. }

theories/tests/lists.v

@@ -123,7 +123,7 @@ Section in_place_reversal.
       iApply a_un_op_spec. iApply (a_bin_op_spec _ _
         (λ x, ⌜x = hd⌝ ∧ i ↦U hd)%I (λ x, ⌜x = NONEV⌝)%I  with "[Hi] [] [-]").
       { awp_load_ret i. } { awp_ret_value. }
-      iIntros (? ?) "[-> Hi ] ->". destruct ls.
+      iNext. iIntros (? ?) "[-> Hi ] ->". destruct ls.
       + rewrite{1}/ is_list. iDestruct "Hls" as "->".
         iExists #true; iSplit; first done. iExists #false; iSplit; first done.
         iLeft; iSplit; first done. do 2 iModIntro. awp_seq. awp_load_ret j.

theories/tests/test1.v

@@ -78,33 +78,6 @@ Section test.
     let: "v" := Snd "lv" in
     a_store (a_ret "l") (a_ret "v") ;;;; a_ret "v".
 
-  (* Better a_par spec.
-     But it uses proofmode.v, and cannot be proved from awp_par. *)
-  Lemma a_par_spec (Ψ1 Ψ2 : val → iProp Σ) e1 e2 R (Φ : val → iProp Σ) :
-    awp e1 R Ψ1 -∗
-    awp e2 R Ψ2 -∗
-    ▷ (∀ w1 w2, Ψ1 w1 -∗ Ψ2 w2 -∗ ▷ Φ (w1,w2)%V) -∗
-    awp (a_par e1 e2) R Φ.
-  Proof.
-    iIntros "Hwp1 Hwp2 HΦ".
-    rewrite /a_par /=.
-    awp_apply (a_wp_awp with "Hwp1"); iIntros (ev1) "Hwp1".
-    awp_lam.
-    awp_apply (a_wp_awp with "Hwp2"); iIntros (ev2) "Hwp2".
-    awp_lam.
-    rewrite /awp /=. wp_value_head.
-    iIntros (γ π env l) "#Hlock #Hres [Hunfl1 Hunfl2]". do 2 wp_lam.
-    iApply (par_spec (λ v, Ψ1 v ∗ unflocked _ (π/2))%I
-                     (λ v, Ψ2 v ∗ unflocked _ (π/2))%I
-      with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]").
-    - wp_lam. wp_apply (wp_wand with "Hwp1").
-      iIntros (v) "Hwp1". by iApply "Hwp1".
-    - wp_lam. wp_apply (wp_wand with "Hwp2").
-      iIntros (v) "Hwp2". by iApply "Hwp2".
-    - iNext. iIntros (w1 w2) "[[HΨ1 $] [HΨ2 $]]".
-      iApply ("HΦ" with "[$] [$]").
-  Qed.
-
   Lemma invoke_assignF_1 l (v v' : val) R :
     l ↦U v -∗
     awp (a_invoke assignF (a_par (a_ret #l) (a_ret v'))) R
@@ -112,9 +85,9 @@ Section test.
   Proof.
     iIntros "Hl".
     iApply (a_invoke_simpl _ _ _ (λ v, ⌜v = (#l,v')%V⌝)%I).
-    - iApply (a_par_spec (λ v, ⌜v = #l⌝)%I (λ v, ⌜v = v'⌝)%I).
-      + iApply awp_ret. by wp_value_head.
+    - iApply (awp_par (λ v, ⌜v = #l⌝)%I (λ v, ⌜v = v'⌝)%I).
       + iApply awp_ret. by wp_value_head.
+      + iNext. iApply awp_ret. by wp_value_head.
       + iNext. iIntros (? ? -> ->); done.
     - iIntros (? ->). iModIntro.
       unfold assignF. awp_lam. awp_proj. awp_lam. awp_proj. awp_lam.
@@ -131,9 +104,9 @@ Section test.
           (l ↦U - ∗ R)%I (λ w, ⌜w = v'⌝)%I.
   Proof.
     iApply (a_invoke_spec _ _ _ (λ v, ⌜v = (#l,v')%V⌝)%I).
-    - iApply (a_par_spec (λ v, ⌜v = #l⌝)%I (λ v, ⌜v = v'⌝)%I).
-      + iApply awp_ret. by wp_value_head.
+    - iApply (awp_par (λ v, ⌜v = #l⌝)%I (λ v, ⌜v = v'⌝)%I).
       + iApply awp_ret. by wp_value_head.
+      + iNext. iApply awp_ret. by wp_value_head.
       + iNext. iIntros (? ? -> ->); done.
     - iIntros (? ->). iModIntro.
       iIntros "[Hl HR]". iExists R%I. iFrame.

theories/tests/test2.v

@@ -20,10 +20,10 @@ Section test.
                with "[Hx] [Hx']")%I.
       awp_load_ret x.
       awp_load_ret x.
-      iIntros (? ?) "[% Hx] [% Hx']"; simplify_eq/=.
+      iNext. iIntros (? ?) "[% Hx] [% Hx']"; simplify_eq/=.
       iExists _; eauto. repeat iSplit; eauto.
       by iFrame.
-    - iIntros (? ? ->) "[% Hx]"; simplify_eq/=.
+    - iNext. iIntros (? ? ->) "[% Hx]"; simplify_eq/=.
       iExists _; iFrame. eauto.
   Qed.
 End test.