Commit f6ad3a33 authored by Robbert Krebbers's avatar Robbert Krebbers

Use > for wp_tactics that do not strip later.

parent 0a44697a
...@@ -62,7 +62,7 @@ Section LiftingTests. ...@@ -62,7 +62,7 @@ Section LiftingTests.
revert n1; apply löb_all_1=>n1. revert n1; apply löb_all_1=>n1.
rewrite (comm uPred_and ( _)%I) assoc; apply const_elim_r=>?. rewrite (comm uPred_and ( _)%I) assoc; apply const_elim_r=>?.
(* first need to do the rec to get a later *) (* first need to do the rec to get a later *)
wp_rec!. wp_rec>.
(* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *) (* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
rewrite ->(later_intro (Q _)); rewrite -!later_and; apply later_mono. rewrite ->(later_intro (Q _)); rewrite -!later_and; apply later_mono.
wp_rec. wp_bin_op. wp_rec. wp_bin_op=> ?. wp_rec. wp_bin_op. wp_rec. wp_bin_op=> ?.
...@@ -74,7 +74,7 @@ Section LiftingTests. ...@@ -74,7 +74,7 @@ Section LiftingTests.
Lemma Pred_spec n E Q : Q (LitV (n - 1)) wp E (Pred 'n)%L Q. Lemma Pred_spec n E Q : Q (LitV (n - 1)) wp E (Pred 'n)%L Q.
Proof. Proof.
wp_rec!; apply later_mono; wp_bin_op=> ?. wp_rec>; apply later_mono; wp_bin_op=> ?.
- wp_if. wp_un_op. wp_bin_op. - wp_if. wp_un_op. wp_bin_op.
wp_focus (FindPred _ _); rewrite -FindPred_spec. wp_focus (FindPred _ _); rewrite -FindPred_spec.
apply and_intro; first auto with I omega. apply and_intro; first auto with I omega.
......
...@@ -24,7 +24,7 @@ Tactic Notation "wp_value" := ...@@ -24,7 +24,7 @@ Tactic Notation "wp_value" :=
match goal with match goal with
| |- _ wp ?E ?e ?Q => etransitivity; [|eapply wp_value; reflexivity]; simpl | |- _ wp ?E ?e ?Q => etransitivity; [|eapply wp_value; reflexivity]; simpl
end. end.
Tactic Notation "wp_rec" "!" := Tactic Notation "wp_rec" ">" :=
match goal with match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with match eval cbv in e' with
...@@ -32,8 +32,8 @@ Tactic Notation "wp_rec" "!" := ...@@ -32,8 +32,8 @@ Tactic Notation "wp_rec" "!" :=
wp_bind K; etransitivity; [|eapply wp_rec; reflexivity]; wp_finish wp_bind K; etransitivity; [|eapply wp_rec; reflexivity]; wp_finish
end) end)
end. end.
Tactic Notation "wp_rec" := wp_rec!; wp_strip_later. Tactic Notation "wp_rec" := wp_rec>; wp_strip_later.
Tactic Notation "wp_bin_op" "!" := Tactic Notation "wp_bin_op" ">" :=
match goal with match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with match eval cbv in e' with
...@@ -45,8 +45,8 @@ Tactic Notation "wp_bin_op" "!" := ...@@ -45,8 +45,8 @@ Tactic Notation "wp_bin_op" "!" :=
end) end)
end. end.
Tactic Notation "wp_bin_op" := wp_bin_op!; wp_strip_later. Tactic Notation "wp_bin_op" := wp_bin_op>; wp_strip_later.
Tactic Notation "wp_un_op" "!" := Tactic Notation "wp_un_op" ">" :=
match goal with match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with match eval cbv in e' with
...@@ -54,8 +54,8 @@ Tactic Notation "wp_un_op" "!" := ...@@ -54,8 +54,8 @@ Tactic Notation "wp_un_op" "!" :=
wp_bind K; etransitivity; [|eapply wp_un_op; reflexivity]; wp_finish wp_bind K; etransitivity; [|eapply wp_un_op; reflexivity]; wp_finish
end) end)
end. end.
Tactic Notation "wp_un_op" := wp_un_op!; wp_strip_later. Tactic Notation "wp_un_op" := wp_un_op>; wp_strip_later.
Tactic Notation "wp_if" "!" := Tactic Notation "wp_if" ">" :=
try wp_value; try wp_value;
match goal with match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
...@@ -65,7 +65,7 @@ Tactic Notation "wp_if" "!" := ...@@ -65,7 +65,7 @@ Tactic Notation "wp_if" "!" :=
etransitivity; [|apply wp_if_true || apply wp_if_false]; wp_finish etransitivity; [|apply wp_if_true || apply wp_if_false]; wp_finish
end) end)
end. end.
Tactic Notation "wp_if" := wp_if!; wp_strip_later. Tactic Notation "wp_if" := wp_if>; wp_strip_later.
Tactic Notation "wp_focus" open_constr(efoc) := Tactic Notation "wp_focus" open_constr(efoc) :=
match goal with match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ 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