Merged from master.

exercises/ex_04_parallel_add.v

@@ -39,9 +39,7 @@ Section proof1.
     { (* exercise *)
       admit. }
     iIntros (l) "#Hl". wp_let.
-    (*wp_apply (wp_par (λ _, True%I) (λ _, True%I)).*)
-    (* FIXME previous tactic fails (replaced by the following two). *)
-    wp_bind (_ ||| _)%E. iApply (wp_par (λ _, True%I) (λ _, True%I)).
+    wp_apply (par_spec (λ _, True%I) (λ _, True%I)).
     - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]".
       wp_seq. wp_load. wp_op. wp_store.
       wp_apply (release_spec with "[Hr $Hl]"); [|done].
@@ -110,11 +108,7 @@ Section proof2.
     { (* exercise *)
       admit. }
     iIntros (l) "#Hl". wp_let.
-    (*wp_apply (wp_par (λ _, own γ1 (◯ Excl' 2)) (λ _, own γ2 (◯ Excl' 2))
-                with "[Hγ1◯] [Hγ2◯]").*)
-    (* FIXME previous tactic fails (replaced by the following two). *)
-    wp_bind (_ ||| _)%E.
-    iApply (wp_par (λ _, own γ1 (◯ Excl' 2)) (λ _, own γ2 (◯ Excl' 2))
+    wp_apply (par_spec (λ _, own γ1 (◯ Excl' 2)) (λ _, own γ2 (◯ Excl' 2))
                 with "[Hγ1◯] [Hγ2◯]").
     - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)".
       wp_seq. wp_load. wp_op. wp_store.
@@ -148,11 +142,7 @@ Section proof3.
     { (* exercise *)
       admit. }
     iIntros (l) "#Hl". wp_let.
-    (*wp_apply (wp_par (λ _, own γ (◯!{1/2} 2%nat)) (λ _, own γ (◯!{1/2} 2%nat))
-                with "[Hγ1◯] [Hγ2◯]").*)
-    (* FIXME previous tactic fails (replaced by the following two). *)
-    wp_bind (_ ||| _)%E.
-    iApply (wp_par (λ _, own γ (◯!{1/2} 2%nat)) (λ _, own γ (◯!{1/2} 2%nat))
+    wp_apply (par_spec (λ _, own γ (◯!{1/2} 2%nat)) (λ _, own γ (◯!{1/2} 2%nat))
                 with "[Hγ1◯] [Hγ2◯]").
     - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
       wp_seq. wp_load. wp_op. wp_store.

solutions/ex_04_parallel_add.v

@@ -38,9 +38,7 @@ Section proof1.
     wp_apply (newlock_spec (parallel_add_inv_1 r) with "[Hr]").
     { (* exercise *) iExists 0. iFrame. }
     iIntros (l) "#Hl". wp_let.
-    (*wp_apply (wp_par (λ _, True%I) (λ _, True%I)).*)
-    (* FIXME previous tactic fails (replaced by the following two). *)
-    wp_bind (_ ||| _)%E. iApply (wp_par (λ _, True%I) (λ _, True%I)).
+    wp_apply (par_spec (λ _, True%I) (λ _, True%I)).
     - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]".
       wp_seq. wp_load. wp_op. wp_store.
       wp_apply (release_spec with "[Hr $Hl]"); [|done].
@@ -113,11 +111,7 @@ Section proof2.
     wp_apply (newlock_spec (parallel_add_inv_2 r γ1 γ2) with "[Hr Hγ1● Hγ2●]").
     { (* exercise *) iExists 0, 0. iFrame. }
     iIntros (l) "#Hl". wp_let.
-    (*wp_apply (wp_par (λ _, own γ1 (◯ Excl' 2)) (λ _, own γ2 (◯ Excl' 2))
-                with "[Hγ1◯] [Hγ2◯]").*)
-    (* FIXME previous tactic fails (replaced by the following two). *)
-    wp_bind (_ ||| _)%E.
-    iApply (wp_par (λ _, own γ1 (◯ Excl' 2)) (λ _, own γ2 (◯ Excl' 2))
+    wp_apply (par_spec (λ _, own γ1 (◯ Excl' 2)) (λ _, own γ2 (◯ Excl' 2))
                 with "[Hγ1◯] [Hγ2◯]").
     - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)".
       wp_seq. wp_load. wp_op. wp_store.
@@ -160,11 +154,7 @@ Section proof3.
     wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
     { (* exercise *) iExists 0%nat. iFrame. }
     iIntros (l) "#Hl". wp_let.
-    (*wp_apply (wp_par (λ _, own γ (◯!{1/2} 2%nat)) (λ _, own γ (◯!{1/2} 2%nat))
-                with "[Hγ1◯] [Hγ2◯]").*)
-    (* FIXME previous tactic fails (replaced by the following two). *)
-    wp_bind (_ ||| _)%E.
-    iApply (wp_par (λ _, own γ (◯!{1/2} 2%nat)) (λ _, own γ (◯!{1/2} 2%nat))
+    wp_apply (par_spec (λ _, own γ (◯!{1/2} 2%nat)) (λ _, own γ (◯!{1/2} 2%nat))
                 with "[Hγ1◯] [Hγ2◯]").
     - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
       wp_seq. wp_load. wp_op. wp_store.

solutions/ex_05_parallel_add_mul.v

@@ -77,11 +77,7 @@ Section proof.
     wp_apply (newlock_spec (parallel_add_mul_inv r γ1 γ2) with "[Hr Hγ1● Hγ2●]").
     { iExists false, false, 0. iFrame. done. }
     iIntros (l) "#Hl". wp_let.
-    (*wp_apply (wp_par (λ _, own γ1 (◯ Excl' true)) (λ _, own γ2 (◯ Excl' true))
-                with "[Hγ1◯] [Hγ2◯]").*)
-    (* FIXME previous tactic fails (replaced by the following two). *)
-    wp_bind (_ ||| _)%E.
-    iApply (wp_par (λ _, own γ1 (◯ Excl' true)) (λ _, own γ2 (◯ Excl' true))
+    wp_apply (par_spec (λ _, own γ1 (◯ Excl' true)) (λ _, own γ2 (◯ Excl' true))
                 with "[Hγ1◯] [Hγ2◯]").
     - wp_apply (acquire_spec with "Hl").
       iDestruct 1 as (b1 b2 z) "(Hγ1● & Hγ2● & Hr & %)".