Commit 7827f688 authored by Ralf Jung's avatar Ralf Jung
Browse files

some playing around with wp_tactics

parent 26341006
......@@ -84,7 +84,7 @@ Section LiftingTests.
True wp (Σ:=globalF Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
Proof.
intros E.
wp_focus (Pred '42); rewrite -Pred_spec -later_intro.
wp_focus (Pred _); rewrite -Pred_spec -later_intro.
wp_rec. rewrite -Pred_spec -later_intro; auto with I.
Qed.
End LiftingTests.
......@@ -4,12 +4,12 @@ Import uPred.
Ltac wp_strip_later :=
match goal with
| |- _, _ => let H := fresh in intro H; wp_strip_later; revert H
| |- _ _ => etransitivity; [|apply later_intro]
| |- _ _ => etransitivity; [|by apply later_intro]
end.
Ltac wp_bind K :=
lazymatch eval hnf in K with
| [] => idtac
| _ => etransitivity; [|apply (wp_bind K)]; simpl
| _ => etransitivity; [|by apply (wp_bind K)]; simpl
end.
Ltac wp_finish :=
let rec go :=
......@@ -44,7 +44,6 @@ Tactic Notation "wp_bin_op" ">" :=
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
......
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