Skip to content
Snippets Groups Projects
Commit fa7dc440 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge heap_lang/wp_tactics.v into heap_lang/proofmode.v. 

Also:

- Remove the wp_strip_later hack.
- Let wp_lam, wp_rec, wp_... initiate the proof mode.
parent 6bf1e153
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
_CoqProject
+ 0
− 1
View file @ fa7dc440
......@@ -96,7 +96,6 @@ theories/program_logic/ownp.v
theories/heap_lang/lang.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/wp_tactics.v
theories/heap_lang/notation.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
......
theories/heap_lang/proofmode.v
+ 143
− 2
View file @ fa7dc440
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Export wp_tactics lifting.
From iris.heap_lang Require Export tactics lifting.
Import uPred.
Ltac wp_strip_later ::= iNext.
(** 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.
(* Solves side-conditions generated by the wp tactics *)
Ltac wp_done :=
match goal with
| |- Closed _ _ => solve_closed
| |- is_Some (to_val _) => solve_to_val
| |- to_val _ = Some _ => solve_to_val
| |- language.to_val _ = Some _ => solve_to_val
| _ => fast_done
end.
Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; lazy beta.
Ltac wp_seq_head :=
lazymatch goal with
| |- _ ⊢ wp ?E (Seq _ _) ?Q =>
etrans; [|eapply wp_seq; wp_done]; iNext
end.
Ltac wp_finish := intros_revert ltac:(
rewrite /= ?to_of_val;
try iNext;
repeat lazymatch goal with
| |- _ ⊢ wp ?E (Seq _ _) ?Q =>
etrans; [|eapply wp_seq; wp_done]; iNext
| |- _ ⊢ wp ?E _ ?Q => wp_value_head
end).
Tactic Notation "wp_value" :=
iStartProof;
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
| _ => fail "wp_value: not a wp"
end.
Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
Proof. by unlock. Qed.
(* Applied to goals that are equalities of expressions. Will try to unlock the
LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.
Tactic Notation "wp_rec" :=
iStartProof;
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* hnf does not reduce through an of_val *)
(* match eval hnf in e1 with Rec _ _ _ => *)
wp_bind_core K; etrans;
[|eapply wp_rec; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
(* end *) end) || fail "wp_rec: cannot find 'Rec' in" e
| _ => fail "wp_rec: not a 'wp'"
end.
Tactic Notation "wp_lam" :=
iStartProof;
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* match eval hnf in e1 with Rec BAnon _ _ => *)
wp_bind_core K; etrans;
[|eapply wp_lam; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
(* end *) end) || fail "wp_lam: cannot find 'Lam' in" e
| _ => fail "wp_lam: not a 'wp'"
end.
Tactic Notation "wp_let" := wp_lam.
Tactic Notation "wp_seq" := wp_let.
Tactic Notation "wp_op" :=
iStartProof;
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
lazymatch eval hnf in e' with
| BinOp LtOp _ _ => wp_bind_core K; apply wp_lt; wp_finish
| BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
| BinOp EqOp _ _ =>
wp_bind_core K; eapply wp_eq; [wp_done|wp_done|wp_finish|wp_finish]
| BinOp _ _ _ =>
wp_bind_core K; etrans;
[|eapply wp_bin_op; [wp_done|wp_done|try fast_done]]; wp_finish
| UnOp _ _ =>
wp_bind_core K; etrans;
[|eapply wp_un_op; [wp_done|try fast_done]]; wp_finish
end) || fail "wp_op: cannot find 'BinOp' or 'UnOp' in" e
| _ => fail "wp_op: not a 'wp'"
end.
Tactic Notation "wp_proj" :=
iStartProof;
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Fst _ => wp_bind_core K; etrans; [|eapply wp_fst; wp_done]; wp_finish
| Snd _ => wp_bind_core K; etrans; [|eapply wp_snd; wp_done]; wp_finish
end) || fail "wp_proj: cannot find 'Fst' or 'Snd' in" e
| _ => fail "wp_proj: not a 'wp'"
end.
Tactic Notation "wp_if" :=
iStartProof;
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| If _ _ _ =>
wp_bind_core K;
etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
end) || fail "wp_if: cannot find 'If' in" e
| _ => fail "wp_if: not a 'wp'"
end.
Tactic Notation "wp_match" :=
iStartProof;
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Case _ _ _ =>
wp_bind_core K;
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_bind" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match e' with
| efoc => unify e' efoc; wp_bind_core K
end) || fail "wp_bind: cannot find" efoc "in" e
| _ => fail "wp_bind: not a 'wp'"
end.
(** Heap tactics *)
Section heap.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
......
theories/heap_lang/wp_tactics.v deleted 100644 → 0
+ 0
− 138
View file @ 6bf1e153
From iris.heap_lang Require Export tactics lifting.
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.
(* Solves side-conditions generated by the wp tactics *)
Ltac wp_done :=
match goal with
| |- Closed _ _ => solve_closed
| |- is_Some (to_val _) => solve_to_val
| |- to_val _ = Some _ => solve_to_val
| |- language.to_val _ = Some _ => solve_to_val
| _ => fast_done
end.
Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; lazy beta.
Ltac wp_strip_later := idtac. (* a hook to be redefined later *)
Ltac wp_seq_head :=
lazymatch goal with
| |- _ ⊢ wp ?E (Seq _ _) ?Q =>
etrans; [|eapply wp_seq; wp_done]; wp_strip_later
end.
Ltac wp_finish := intros_revert ltac:(
rewrite /= ?to_of_val;
try wp_strip_later;
repeat lazymatch goal with
| |- _ ⊢ wp ?E (Seq _ _) ?Q =>
etrans; [|eapply wp_seq; wp_done]; wp_strip_later
| |- _ ⊢ wp ?E _ ?Q => wp_value_head
end).
Tactic Notation "wp_value" :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
| _ => fail "wp_value: not a wp"
end.
Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
Proof. by unlock. Qed.
(* Applied to goals that are equalities of expressions. Will try to unlock the
LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.
Tactic Notation "wp_rec" :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* hnf does not reduce through an of_val *)
(* match eval hnf in e1 with Rec _ _ _ => *)
wp_bind_core K; etrans;
[|eapply wp_rec; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
(* end *) end) || fail "wp_rec: cannot find 'Rec' in" e
| _ => fail "wp_rec: not a 'wp'"
end.
Tactic Notation "wp_lam" :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* match eval hnf in e1 with Rec BAnon _ _ => *)
wp_bind_core K; etrans;
[|eapply wp_lam; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
(* end *) end) || fail "wp_lam: cannot find 'Lam' in" e
| _ => fail "wp_lam: not a 'wp'"
end.
Tactic Notation "wp_let" := wp_lam.
Tactic Notation "wp_seq" := wp_let.
Tactic Notation "wp_op" :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
lazymatch eval hnf in e' with
| BinOp LtOp _ _ => wp_bind_core K; apply wp_lt; wp_finish
| BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
| BinOp EqOp _ _ =>
wp_bind_core K; eapply wp_eq; [wp_done|wp_done|wp_finish|wp_finish]
| BinOp _ _ _ =>
wp_bind_core K; etrans;
[|eapply wp_bin_op; [wp_done|wp_done|try fast_done]]; wp_finish
| UnOp _ _ =>
wp_bind_core K; etrans;
[|eapply wp_un_op; [wp_done|try fast_done]]; wp_finish
end) || fail "wp_op: cannot find 'BinOp' or 'UnOp' in" e
| _ => fail "wp_op: not a 'wp'"
end.
Tactic Notation "wp_proj" :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Fst _ => wp_bind_core K; etrans; [|eapply wp_fst; wp_done]; wp_finish
| Snd _ => wp_bind_core K; etrans; [|eapply wp_snd; wp_done]; wp_finish
end) || fail "wp_proj: cannot find 'Fst' or 'Snd' in" e
| _ => fail "wp_proj: not a 'wp'"
end.
Tactic Notation "wp_if" :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| If _ _ _ =>
wp_bind_core K;
etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
end) || fail "wp_if: cannot find 'If' in" e
| _ => fail "wp_if: not a 'wp'"
end.
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_core K;
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_bind" open_constr(efoc) :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match e' with
| efoc => unify e' efoc; wp_bind_core K
end) || fail "wp_bind: cannot find" efoc "in" e
| _ => fail "wp_bind: not a 'wp'"
end.
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