Commit 3a5c5045 authored by Robbert Krebbers's avatar Robbert Krebbers

Move some stuff.

parent 7abcc966
......@@ -5,15 +5,6 @@ From iris.heap_lang Require Export tactics lifting.
Set Default Proof Using "Type".
Import uPred.
(** wp-specific helper tactics *)
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
| [] => idtac
| _ => etrans; [|fast_by apply (wp_bind K)]; simpl
end.
Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
PureExec φ e1 e2
φ
......@@ -26,6 +17,8 @@ Proof.
by rewrite -ectx_lifting.wp_ectx_bind_inv.
Qed.
Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof;
lazymatch goal with
......@@ -54,6 +47,12 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
Tactic Notation "wp_case" := wp_pure (Case _ _ _).
Tactic Notation "wp_match" := wp_case; wp_let.
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
| [] => idtac
| _ => etrans; [|fast_by apply (wp_bind K)]; simpl
end.
Tactic Notation "wp_bind" open_constr(efoc) :=
iStartProof;
lazymatch 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