From 198e38f7411e66a3c03b9e64dee3247e3f3a6682 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 1 Jul 2019 14:37:50 +0200
Subject: [PATCH] More fancy `wp_branch` tactic that supports pure propositions
 with Coq intro patterns.

---
 theories/channel/proofmode.v              | 15 +++++++++++----
 theories/examples/list_sort_elem.v        | 12 +++++-------
 theories/examples/list_sort_elem_client.v |  2 +-
 3 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 42da272..8645c4a 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -194,7 +194,7 @@ Proof.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
 Qed.
 
-Tactic Notation "wp_branch" "as" constr(pat1) constr(pat2) :=
+Tactic Notation "wp_branch_core" "as" tactic3(tac1) tactic3(tac2) :=
   let solve_mapsto _ :=
     let c := match goal with |- _ = Some (_, (?c ↣ _ @ _)%I) => c end in
     iAssumptionCore || fail "wp_branch: cannot find" c "↣ ? @ ?" in
@@ -207,12 +207,19 @@ Tactic Notation "wp_branch" "as" constr(pat1) constr(pat2) :=
       |fail 1 "wp_branch: cannot find 'recv' in" e];
     [solve_mapsto ()
        |iSolveTC || fail 1 "wp_send: protocol not of the shape <&>"
-    |pm_reduce; intros [];
-       [iDestructHyp Hnew as pat1|iDestructHyp Hnew as pat2]; wp_finish]
+    |pm_reduce; intros []; [tac1 Hnew|tac2 Hnew]; wp_finish]
   | _ => fail "wp_branch: not a 'wp'"
   end.
 
-Tactic Notation "wp_branch" := wp_branch as "_" "_".
+Tactic Notation "wp_branch" "as" constr(pat1) "|" constr(pat2) :=
+  wp_branch_core as (fun H => iDestructHyp H as pat1) (fun H => iDestructHyp H as pat2).
+Tactic Notation "wp_branch" "as" "%" intropattern(pat1) "|" constr(pat2) :=
+  wp_branch_core as (fun H => iPure H as pat1) (fun H => iDestructHyp H as pat2).
+Tactic Notation "wp_branch" "as" constr(pat1) "|" "%" intropattern(pat2) :=
+  wp_branch_core as (fun H => iDestructHyp H as pat1) (fun H => iPure H as pat2).
+Tactic Notation "wp_branch" "as" "%" intropattern(pat1) "|" "%" intropattern(pat2) :=
+  wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2).
+Tactic Notation "wp_branch" := wp_branch as %_ | %_.
 
 Lemma tac_wp_select `{!proto_chanG Σ, !heapG Σ} Δ neg i js K N
     c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ :
diff --git a/theories/examples/list_sort_elem.v b/theories/examples/list_sort_elem.v
index 66d0cde..3b7d5d2 100644
--- a/theories/examples/list_sort_elem.v
+++ b/theories/examples/list_sort_elem.v
@@ -122,7 +122,7 @@ Section list_sort_elem.
   Proof.
     iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
     iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
-    wp_rec. wp_branch as "_" "Hys'".
+    wp_rec. wp_branch as %_ | %Hys'.
     - wp_recv (x v) as (Htl) "HI".
       wp_select. wp_send with "[$HI]"; first by auto.
       wp_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
@@ -131,7 +131,7 @@ Section list_sort_elem.
       * auto using Sorted_snoc.
       * intros x'.
         inversion 1; discriminate_list || simplify_list_eq. by constructor.
-    - iDestruct "Hys'" as %Hys'. wp_select with "[]".
+    - wp_select with "[]".
       { by rewrite /= Hys Hxs Hys'. }
       iApply "HΨ". iFrame.
   Qed.
@@ -154,7 +154,7 @@ Section list_sort_elem.
     iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
     iIntros (Ψ) "(Hc & Hc1 & Hc2 & HIy1) HΨ".
     iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
-    wp_rec. wp_branch as "_" "Hys2".
+    wp_rec. wp_branch as %_ | %Hys2.
     - wp_recv (x v) as (Htl2) "HIx".
       wp_pures. wp_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
       case_bool_decide.
@@ -174,8 +174,7 @@ Section list_sort_elem.
         * constructor. by apply total_not.
         * intros x'.
           inversion 1; discriminate_list || simplify_list_eq. by constructor.
-    - iDestruct "Hys2" as %Hys2.
-      wp_select. wp_send with "[$HIy1 //]".
+    - wp_select. wp_send with "[$HIy1 //]".
       wp_apply (list_sort_elem_service_move_spec with "[$Hc $Hc1]").
       * done.
       * by rewrite Hys Hys2 -!assoc_L (comm _ xs2).
@@ -205,8 +204,7 @@ Section list_sort_elem.
         wp_select. wp_send with "[$HIx2]".
         wp_apply (list_sort_elem_service_split_spec with "[$Hc $Hcy $Hcz]").
         iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
-        wp_branch as "_" "Hnil"; last first.
-        { by iDestruct "Hnil" as %?%Permutation_nil_cons. }
+        wp_branch as %_ | %[]%Permutation_nil_cons.
         wp_recv (x v) as "[_ HIx]".
         wp_apply (list_sort_elem_service_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
           with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
diff --git a/theories/examples/list_sort_elem_client.v b/theories/examples/list_sort_elem_client.v
index 9999135..e515e6f 100644
--- a/theories/examples/list_sort_elem_client.v
+++ b/theories/examples/list_sort_elem_client.v
@@ -53,7 +53,7 @@ Section list_sort_elem_client.
   Proof.
     iIntros (Hsort Φ) "Hc HΦ".
     iLöb as "IH" forall (xs ys' Φ Hsort).
-    wp_lam. wp_branch as "_" "Hperm"; wp_pures.
+    wp_lam. wp_branch as %_ | %Hperm; wp_pures.
     - wp_recv (y v) as (Htl) "HIxv".
       wp_apply ("IH" with "[] Hc"); first by auto using Sorted_snoc.
       iIntros (ys ws). rewrite -!assoc_L. iDestruct 1 as (??) "[Hc HI]".
-- 
GitLab