Commit 7abcc966 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Get rid of `wp_done` and make more using of `IntoVal`.

parent 284ccdd5
...@@ -21,15 +21,15 @@ Context `{!heapG Σ, !spawnG Σ}. ...@@ -21,15 +21,15 @@ Context `{!heapG Σ, !spawnG Σ}.
brought together. That is strictly stronger than first stripping a later brought together. That is strictly stronger than first stripping a later
and then merging them, as demonstrated by [tests/joining_existentials.v]. and then merging them, as demonstrated by [tests/joining_existentials.v].
This is why these are not Texan triples. *) This is why these are not Texan triples. *)
Lemma par_spec (Ψ1 Ψ2 : val iProp Σ) e (f1 f2 : val) (Φ : val iProp Σ) : Lemma par_spec (Ψ1 Ψ2 : val iProp Σ) e (f1 f2 : val) (Φ : val iProp Σ)
to_val e = Some (f1,f2)%V `{Hef : !IntoVal e (f1,f2)} :
WP f1 #() {{ Ψ1 }} - WP f2 #() {{ Ψ2 }} - WP f1 #() {{ Ψ1 }} - WP f2 #() {{ Ψ2 }} -
( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) - ( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) -
WP par e {{ Φ }}. WP par e {{ Φ }}.
Proof. Proof.
iIntros (<-%of_to_val) "Hf1 Hf2 HΦ". apply of_to_val in Hef as <-. iIntros "Hf1 Hf2 HΦ".
rewrite /par /=. wp_let. wp_proj. rewrite /par /=. wp_let. wp_proj.
wp_apply (spawn_spec parN with "Hf1"); try wp_done; try solve_ndisj. wp_apply (spawn_spec parN with "Hf1").
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _). iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let. iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1". wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
...@@ -42,7 +42,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) ...@@ -42,7 +42,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ)
( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) - ( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) -
WP e1 ||| e2 {{ Φ }}. WP e1 ||| e2 {{ Φ }}.
Proof. Proof.
iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); try wp_done. iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]").
by wp_let. by wp_let. auto. by wp_let. by wp_let. auto.
Qed. Qed.
End proof. End proof.
...@@ -44,11 +44,10 @@ Global Instance join_handle_ne n l : ...@@ -44,11 +44,10 @@ Global Instance join_handle_ne n l :
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
(** The main proofs. *) (** The main proofs. *)
Lemma spawn_spec (Ψ : val iProp Σ) e (f : val) : Lemma spawn_spec (Ψ : val iProp Σ) e (f : val) `{Hef : !IntoVal e f} :
to_val e = Some f
{{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}. {{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
Proof. Proof.
iIntros (<-%of_to_val Φ) "Hf HΦ". rewrite /spawn /=. apply of_to_val in Hef as <-. iIntros (Φ) "Hf HΦ". rewrite /spawn /=.
wp_let. wp_alloc l as "Hl". wp_let. wp_let. wp_alloc l as "Hl". wp_let.
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done. iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?". iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
......
...@@ -12,21 +12,7 @@ Ltac wp_bind_core K := ...@@ -12,21 +12,7 @@ Ltac wp_bind_core K :=
| _ => etrans; [|fast_by apply (wp_bind K)]; simpl | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
end. end.
(* Solves side-conditions generated by the wp tactics *) Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
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]; simpl.
(* Solves side-conditions generated specifically by wp_pure *)
Ltac wp_pure_done :=
split_and?; wp_done.
Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ : Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
PureExec φ e1 e2 PureExec φ e1 e2
...@@ -46,9 +32,9 @@ Tactic Notation "wp_pure" open_constr(efoc) := ...@@ -46,9 +32,9 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
unify e' efoc; unify e' efoc;
eapply (tac_wp_pure K); eapply (tac_wp_pure K);
[unlock; simpl; apply _ (* PureExec *) [simpl; apply _ (* PureExec *)
|wp_pure_done (* The pure condition for PureExec *) |try fast_done (* The pure condition for PureExec *)
|apply _ (* IntoLaters *) |apply _ (* IntoLaters *)
|simpl_subst; try wp_value_head (* new goal *)]) |simpl_subst; try wp_value_head (* new goal *)])
|| fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct" || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
| _ => fail "wp_pure: not a 'wp'" | _ => fail "wp_pure: not a 'wp'"
......
...@@ -215,12 +215,11 @@ Global Instance wp_mono' E e : ...@@ -215,12 +215,11 @@ Global Instance wp_mono' E e :
Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ E e). Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ E e).
Proof. by intros Φ Φ' ?; apply wp_mono. Qed. Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
Lemma wp_value E Φ e v : to_val e = Some v Φ v WP e @ E {{ Φ }}. Lemma wp_value E Φ e v `{!IntoVal e v} : Φ v WP e @ E {{ Φ }}.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed. Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
Lemma wp_value_fupd' E Φ v : (|={E}=> Φ v) WP of_val v @ E {{ Φ }}. Lemma wp_value_fupd' E Φ v : (|={E}=> Φ v) WP of_val v @ E {{ Φ }}.
Proof. intros. by rewrite -wp_fupd -wp_value'. Qed. Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
Lemma wp_value_fupd E Φ e v : Lemma wp_value_fupd E Φ e v `{!IntoVal e v} : (|={E}=> Φ v) WP e @ E {{ Φ }}.
to_val e = Some v (|={E}=> Φ v) WP e @ E {{ Φ }}.
Proof. intros. rewrite -wp_fupd -wp_value //. Qed. Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
Lemma wp_frame_l E e Φ R : R WP e @ E {{ Φ }} WP e @ E {{ v, R Φ v }}. Lemma wp_frame_l E e Φ R : R WP e @ E {{ Φ }} WP e @ E {{ v, R Φ v }}.
...@@ -290,7 +289,6 @@ Section proofmode_classes. ...@@ -290,7 +289,6 @@ Section proofmode_classes.
ElimModal (|={E1,E2}=> P) P ElimModal (|={E1,E2}=> P) P
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100. (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed. Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
End proofmode_classes. End proofmode_classes.
Hint Extern 0 (atomic _) => assumption : typeclass_instances. Hint Extern 0 (atomic _) => assumption : typeclass_instances.
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