Commit d1fc135b authored by Robbert Krebbers's avatar Robbert Krebbers

Make wp_tactics more robust.

Tactics like wp_proj should always solve all to_val side-conditions. The
tactic wp_done is used to handle these in a uniform way.
parent 80dd5e37
Pipeline #267 passed with stage
...@@ -25,19 +25,15 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) : ...@@ -25,19 +25,15 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
#> par e {{ Φ }}. #> par e {{ Φ }}.
Proof. Proof.
intros. rewrite /par. intros. rewrite /par. ewp (by eapply wp_value). wp_let. wp_proj.
wp_focus e. etransitivity; last by eapply wp_value. wp_let. ewp (eapply spawn_spec; wp_done).
(* FIXME: wp_proj should not spawn these goals. *) apply sep_mono_r, sep_mono_r.
wp_proj; eauto using to_of_val. apply forall_intro=>h. apply wand_intro_l. wp_let. wp_proj.
ewp eapply spawn_spec; eauto using to_of_val.
apply sep_mono_r. apply sep_mono_r.
apply forall_intro=>h. apply wand_intro_l. wp_let.
wp_proj; eauto using to_of_val.
wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. apply wp_mono=>v2. wp_let. wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. apply wp_mono=>v2. wp_let.
ewp eapply join_spec; eauto using to_of_val. apply sep_mono_r. ewp (by eapply join_spec).
apply forall_intro=>v1. apply wand_intro_l. apply sep_mono_r, forall_intro=>v1; apply wand_intro_l.
rewrite (forall_elim v1) (forall_elim v2). rewrite assoc wand_elim_r. rewrite (forall_elim v1) (forall_elim v2). rewrite assoc wand_elim_r.
wp_let. eapply wp_value, to_val_Pair; eapply to_of_val. wp_let. apply wp_value; wp_done.
Qed. Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp) (e1 e2 : expr []) (Φ : val iProp) : Lemma wp_par (Ψ1 Ψ2 : val iProp) (e1 e2 : expr []) (Φ : val iProp) :
...@@ -46,8 +42,6 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) : ...@@ -46,8 +42,6 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
#> ParV e1 e2 {{ Φ }}. #> ParV e1 e2 {{ Φ }}.
Proof. Proof.
intros. rewrite -par_spec //. apply sep_mono_r. intros. rewrite -par_spec //. repeat apply sep_mono; done || by wp_seq.
apply sep_mono; last apply sep_mono_l; by wp_seq.
Qed. Qed.
End proof. End proof.
...@@ -53,14 +53,11 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) : ...@@ -53,14 +53,11 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
(heap_ctx heapN #> f #() {{ Ψ }} l, join_handle l Ψ - Φ (%l)) (heap_ctx heapN #> f #() {{ Ψ }} l, join_handle l Ψ - Φ (%l))
#> spawn e {{ Φ }}. #> spawn e {{ Φ }}.
Proof. Proof.
intros Hval Hdisj. rewrite /spawn. intros Hval Hdisj. rewrite /spawn. ewp (by eapply wp_value). wp_let.
(* TODO: Make this more convenient. *) wp eapply wp_alloc; eauto with I.
wp_focus e. etransitivity; last by eapply wp_value. wp_let.
(* FIXME: can we change the ewp notation so that the parentheses become unnecessary? *)
(ewp eapply wp_alloc); eauto with I. strip_later.
apply forall_intro=>l. apply wand_intro_l. wp_let. apply forall_intro=>l. apply wand_intro_l. wp_let.
rewrite (forall_elim l). eapply sep_elim_True_l. rewrite (forall_elim l). eapply sep_elim_True_l.
{ eapply (own_alloc (Excl ())). done. } { by eapply (own_alloc (Excl ())). }
rewrite !pvs_frame_r. eapply wp_strip_pvs. rewrite !sep_exist_r. rewrite !pvs_frame_r. eapply wp_strip_pvs. rewrite !sep_exist_r.
apply exist_elim=>γ. apply exist_elim=>γ.
(* TODO: Figure out a better way to say "I want to establish ▷ spawn_inv". *) (* TODO: Figure out a better way to say "I want to establish ▷ spawn_inv". *)
...@@ -68,7 +65,7 @@ Proof. ...@@ -68,7 +65,7 @@ Proof.
own γ (Excl ()) (spawn_inv γ l Ψ))%I. own γ (Excl ()) (spawn_inv γ l Ψ))%I.
{ ecancel [ #> _ {{ _ }}; _ - _; heap_ctx _; own _ _]%I. { ecancel [ #> _ {{ _ }}; _ - _; heap_ctx _; own _ _]%I.
rewrite -later_intro /spawn_inv -(exist_intro (InjLV #0)). rewrite -later_intro /spawn_inv -(exist_intro (InjLV #0)).
cancel [l InjLV #0]%I. apply or_intro_l'. by rewrite const_equiv. } cancel [l InjLV #0]%I. by apply or_intro_l', const_intro. }
rewrite (inv_alloc N) // !pvs_frame_l. eapply wp_strip_pvs. rewrite (inv_alloc N) // !pvs_frame_l. eapply wp_strip_pvs.
ewp eapply wp_fork. rewrite [heap_ctx _]always_sep_dup [inv _ _]always_sep_dup. ewp eapply wp_fork. rewrite [heap_ctx _]always_sep_dup [inv _ _]always_sep_dup.
sep_split left: [_ - _; inv _ _; own _ _; heap_ctx _]%I. sep_split left: [_ - _; inv _ _; own _ _; heap_ctx _]%I.
...@@ -104,7 +101,7 @@ Proof. ...@@ -104,7 +101,7 @@ Proof.
cancel [l lv]%I. rewrite sep_or_r. apply or_elim. cancel [l lv]%I. rewrite sep_or_r. apply or_elim.
- (* Case 1 : nothing sent yet, we wait. *) - (* Case 1 : nothing sent yet, we wait. *)
rewrite -or_intro_l. apply const_elim_sep_l=>-> {lv}. rewrite -or_intro_l. apply const_elim_sep_l=>-> {lv}.
do 2 rewrite const_equiv // left_id. wp_case; eauto. do 2 rewrite const_equiv // left_id. wp_case.
wp_seq. rewrite -always_wand_impl always_elim. wp_seq. rewrite -always_wand_impl always_elim.
rewrite !assoc. eapply wand_apply_r'; first done. rewrite !assoc. eapply wand_apply_r'; first done.
rewrite -(exist_intro γ). solve_sep_entails. rewrite -(exist_intro γ). solve_sep_entails.
...@@ -115,8 +112,7 @@ Proof. ...@@ -115,8 +112,7 @@ Proof.
rewrite [(heap_ctx _ _)%I]sep_elim_r !assoc. rewrite -own_op own_valid_l. rewrite [(heap_ctx _ _)%I]sep_elim_r !assoc. rewrite -own_op own_valid_l.
rewrite -!assoc discrete_valid. apply const_elim_sep_l=>-[]. } rewrite -!assoc discrete_valid. apply const_elim_sep_l=>-[]. }
rewrite -or_intro_r. ecancel [own _ _]. rewrite -or_intro_r. ecancel [own _ _].
wp_case; eauto using to_of_val. wp_case. wp_let. ewp (eapply wp_value; wp_done).
wp_let. etransitivity; last by eapply wp_value, to_of_val.
rewrite (forall_elim v). rewrite !assoc. eapply wand_apply_r'; eauto with I. rewrite (forall_elim v). rewrite !assoc. eapply wand_apply_r'; eauto with I.
Qed. Qed.
......
...@@ -21,6 +21,8 @@ Ltac wp_finish := ...@@ -21,6 +21,8 @@ Ltac wp_finish :=
| _ => idtac | _ => idtac
end in simpl; intros_revert go. end in simpl; intros_revert go.
Ltac wp_done := rewrite -/of_val /= ?to_of_val; fast_done.
Tactic Notation "wp_rec" ">" := Tactic Notation "wp_rec" ">" :=
löb ltac:( löb ltac:(
(* Find the redex and apply wp_rec *) (* Find the redex and apply wp_rec *)
...@@ -30,9 +32,7 @@ Tactic Notation "wp_rec" ">" := ...@@ -30,9 +32,7 @@ Tactic Notation "wp_rec" ">" :=
match eval hnf in e' with App ?e1 _ => match eval hnf in e' with App ?e1 _ =>
(* hnf does not reduce through an of_val *) (* hnf does not reduce through an of_val *)
(* match eval hnf in e1 with Rec _ _ _ => *) (* match eval hnf in e1 with Rec _ _ _ => *)
wp_bind K; etrans; wp_bind K; etrans; [|eapply wp_rec'; wp_done]; simpl_subst; wp_finish
[|eapply wp_rec'; repeat rewrite /= to_of_val; fast_done];
simpl_subst; wp_finish
(* end *) end) (* end *) end)
end). end).
Tactic Notation "wp_rec" := wp_rec>; try strip_later. Tactic Notation "wp_rec" := wp_rec>; try strip_later.
...@@ -42,9 +42,7 @@ Tactic Notation "wp_lam" ">" := ...@@ -42,9 +42,7 @@ Tactic Notation "wp_lam" ">" :=
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ => match eval hnf in e' with App ?e1 _ =>
(* match eval hnf in e1 with Rec BAnon _ _ => *) (* match eval hnf in e1 with Rec BAnon _ _ => *)
wp_bind K; etrans; wp_bind K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
[|eapply wp_lam; repeat (fast_done || rewrite /= to_of_val)];
simpl_subst; wp_finish
(* end *) end) (* end *) end)
end. end.
Tactic Notation "wp_lam" := wp_lam>; try strip_later. Tactic Notation "wp_lam" := wp_lam>; try strip_later.
...@@ -73,10 +71,8 @@ Tactic Notation "wp_proj" ">" := ...@@ -73,10 +71,8 @@ Tactic Notation "wp_proj" ">" :=
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 hnf in e' with match eval hnf in e' with
| Fst _ => | Fst _ => wp_bind K; etrans; [|eapply wp_fst; wp_done]; wp_finish
wp_bind K; etrans; [|eapply wp_fst; try fast_done]; wp_finish | Snd _ => wp_bind K; etrans; [|eapply wp_snd; wp_done]; wp_finish
| Snd _ =>
wp_bind K; etrans; [|eapply wp_snd; try fast_done]; wp_finish
end) end)
end. end.
Tactic Notation "wp_proj" := wp_proj>; try strip_later. Tactic Notation "wp_proj" := wp_proj>; try strip_later.
...@@ -95,8 +91,9 @@ Tactic Notation "wp_case" ">" := ...@@ -95,8 +91,9 @@ Tactic Notation "wp_case" ">" :=
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 hnf in e' with Case _ _ _ => match eval hnf in e' with Case _ _ _ =>
wp_bind K; wp_bind K;
etrans; [|eapply wp_case_inl || eapply wp_case_inr]; wp_finish etrans; [|first[eapply wp_case_inl; wp_done|eapply wp_case_inr; wp_done]];
wp_finish
end) end)
end. end.
Tactic Notation "wp_case" := wp_case>; try strip_later. Tactic Notation "wp_case" := wp_case>; try strip_later.
......
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