Commit 77318331 authored by Ralf Jung's avatar Ralf Jung

merge wp_bin_op and wp_un_op into wp_op

parent 3dc4997c
......@@ -149,7 +149,7 @@ Section proof.
|| newchan '() {{ Φ }}.
Proof.
rewrite /newchan. wp_rec. (* TODO: wp_seq. *)
rewrite -wp_pvs. wp> eapply wp_alloc; eauto with I ndisj.
rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj.
apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
rewrite !assoc. apply pvs_wand_r.
(* The core of this proof: Allocating the STS and the saved prop. *)
......@@ -266,7 +266,7 @@ Section proof.
rewrite const_equiv /=; last by apply rtc_refl.
rewrite left_id -[( barrier_inv _ _ _)%I]later_intro {3}/barrier_inv.
rewrite -!assoc. apply sep_mono_r, sep_mono_r, wand_intro_l.
wp_bin_op; first done. intros _. wp_if. rewrite !assoc.
wp_op; first done. intros _. wp_if. rewrite !assoc.
eapply wand_apply_r'; first done.
rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro Q) -(exist_intro i).
rewrite !assoc. do 3 (rewrite -pvs_frame_r; apply sep_mono_l).
......@@ -293,7 +293,7 @@ Section proof.
apply wand_intro_l. rewrite [(heap_ctx _ _)%I]sep_elim_r.
rewrite [(sts_own _ _ _ _)%I]sep_elim_r [(sts_ctx _ _ _ _)%I]sep_elim_r.
rewrite !assoc [(_ saved_prop_own i Q)%I]comm !assoc saved_prop_agree.
wp_bin_op>; last done. intros _.
wp_op>; last done. intros _.
etransitivity; last eapply later_mono.
{ (* Is this really the best way to strip the later? *)
erewrite later_sep. apply sep_mono; last apply later_intro.
......
......@@ -35,7 +35,7 @@ Section LiftingTests.
rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
wp eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
wp_rec. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
wp_bin_op. wp eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
wp_op. wp eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
wp_rec. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
by apply const_intro.
Qed.
......@@ -57,7 +57,7 @@ Section LiftingTests.
wp_rec>.
(* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
rewrite ->(later_intro (Φ _)); rewrite -!later_and; apply later_mono.
wp_rec. wp_bin_op. wp_rec. wp_bin_op=> ?; wp_if.
wp_rec. wp_op. wp_rec. wp_op=> ?; wp_if.
- rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
by rewrite left_id impl_elim_l.
- wp_value. assert (n1 = n2 - 1) as -> by omega; auto with I.
......@@ -65,11 +65,11 @@ Section LiftingTests.
Lemma Pred_spec n E Φ : Φ (LitV (n - 1)) || Pred 'n @ E {{ Φ }}.
Proof.
wp_rec>; apply later_mono; wp_bin_op=> ?; wp_if.
- wp_un_op. wp_bin_op.
wp_rec>; apply later_mono; wp_op=> ?; wp_if.
- wp_op. wp_op.
ewp apply FindPred_spec.
apply and_intro; first auto with I omega.
wp_un_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- ewp apply FindPred_spec. auto with I omega.
Qed.
......
......@@ -36,6 +36,7 @@ Tactic Notation "wp_value" :=
match goal with
| |- _ wp ?E ?e ?Q => etransitivity; [|eapply wp_value; reflexivity]; simpl
end.
Tactic Notation "wp_rec" ">" :=
match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
......@@ -45,7 +46,8 @@ Tactic Notation "wp_rec" ">" :=
end)
end.
Tactic Notation "wp_rec" := wp_rec>; wp_strip_later.
Tactic Notation "wp_bin_op" ">" :=
Tactic Notation "wp_op" ">" :=
match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with
......@@ -54,18 +56,12 @@ Tactic Notation "wp_bin_op" ">" :=
| BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish
| BinOp _ _ _ =>
wp_bind K; etransitivity; [|eapply wp_bin_op; reflexivity]; wp_finish
end)
end.
Tactic Notation "wp_bin_op" := wp_bin_op>; wp_strip_later.
Tactic Notation "wp_un_op" ">" :=
match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with
| UnOp _ _ =>
wp_bind K; etransitivity; [|eapply wp_un_op; reflexivity]; wp_finish
end)
end.
Tactic Notation "wp_un_op" := wp_un_op>; wp_strip_later.
Tactic Notation "wp_op" := wp_op>; wp_strip_later.
Tactic Notation "wp_if" ">" :=
match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
......@@ -76,6 +72,7 @@ Tactic Notation "wp_if" ">" :=
end)
end.
Tactic Notation "wp_if" := wp_if>; wp_strip_later.
Tactic Notation "wp_focus" open_constr(efoc) :=
match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
......
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