Commit ab1f6c67 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove wp_case, add wp_match.

This is more natural, match should be used in user code, not case.
parent 91d50c60
......@@ -77,11 +77,11 @@ Proof.
iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
- iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst.
wp_match. iApply ("IH" with "Hγ Hv").
- iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; simplify_eq/=.
+ iSplitL "Hl Hγ".
{ iNext. iExists _; iFrame; eauto. }
wp_case. wp_let. iPvsIntro. by iApply "Hv".
wp_match. by iApply "Hv".
+ iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Qed.
End proof.
......
......@@ -92,16 +92,16 @@ Tactic Notation "wp_if" :=
| _ => fail "wp_if: not a 'wp'"
end.
Tactic Notation "wp_case" :=
Tactic Notation "wp_match" :=
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Case _ _ _ =>
wp_bind K;
etrans; [|first[eapply wp_case_inl; wp_done|eapply wp_case_inr; wp_done]];
wp_finish
end) || fail "wp_case: cannot find 'Case' in" e
| _ => fail "wp_case: not a 'wp'"
etrans; [|first[eapply wp_match_inl; wp_done|eapply wp_match_inr; wp_done]];
simpl_subst; wp_finish
end) || fail "wp_match: cannot find 'Match' in" e
| _ => fail "wp_match: not a 'wp'"
end.
Tactic Notation "wp_focus" open_constr(efoc) :=
......
......@@ -71,15 +71,15 @@ Proof.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
wp_let. iPvsIntro. iIntros "!". wp_seq.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as {m} "[% Hγ']"; subst.
{ wp_case. wp_seq. by iPvsIntro. }
wp_case. wp_let. wp_focus (! _)%E.
{ wp_match. by iPvsIntro. }
wp_match. wp_focus (! _)%E.
iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
{ iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
wp_load.
iCombine "Hγ" "Hγ'" as "Hγ".
iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
iSplitL "Hl"; [iRight; by eauto|].
wp_case. wp_let. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
wp_match. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
Qed.
Lemma hoare_one_shot (Φ : val iProp) :
......
......@@ -40,13 +40,13 @@ Lemma sum_loop_wp `{!heapG Σ} heapN v t l (n : Z) (Φ : val → iPropG heap_lan
WP sum_loop v #l {{ Φ }}.
Proof.
iIntros "(#Hh & Hl & Ht & HΦ)".
iLöb {v t l n Φ} as "IH". wp_rec. wp_let.
iLöb {v t l n Φ} as "IH". wp_rec; wp_let.
destruct t as [n'|tl tr]; simpl in *.
- iDestruct "Ht" as "%"; subst.
wp_case. wp_let. wp_load. wp_op. wp_store.
wp_match. wp_load. wp_op. wp_store.
by iApply ("HΦ" with "Hl").
- iDestruct "Ht" as {ll lr vl vr} "(% & Hll & Htl & Hlr & Htr)"; subst.
wp_case. wp_let. wp_proj. wp_load.
wp_match. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htl"). iIntros "Hl Htl".
wp_seq. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htr"). iIntros "Hl Htr".
......
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