Commit 198e38f7 authored by Robbert Krebbers's avatar Robbert Krebbers

More fancy `wp_branch` tactic that supports pure propositions with Coq intro patterns.

parent 54a2fb5d
......@@ -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 Σ) Φ :
......
......@@ -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.
......
......@@ -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]".
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment