diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v index 5b681ca30c82b3aeec8fa71ef8ad860ee1855d89..f37cf4ebd65845d13360a69f0bb912fcf498f839 100644 --- a/theories/heap_lang/lib/par.v +++ b/theories/heap_lang/lib/par.v @@ -21,15 +21,15 @@ Context `{!heapG Σ, !spawnG Σ}. brought together. That is strictly stronger than first stripping a later and then merging them, as demonstrated by [tests/joining_existentials.v]. This is why these are not Texan triples. *) -Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ) : - to_val e = Some (f1,f2)%V → +Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ) + `{Hef : !IntoVal e (f1,f2)} : WP f1 #() {{ Ψ1 }} -∗ WP f2 #() {{ Ψ2 }} -∗ (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗ WP par e {{ Φ }}. 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. - 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 _). iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let. wp_apply (join_spec with "[\$Hl]"). iIntros (w) "H1". @@ -42,7 +42,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗ WP e1 ||| e2 {{ Φ }}. 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. Qed. End proof. diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v index 4c9b25a6a0de1e5135e84dab6a810015a8879371..95e104c04a774203ba84e9ae89643683881646fe 100644 --- a/theories/heap_lang/lib/spawn.v +++ b/theories/heap_lang/lib/spawn.v @@ -44,11 +44,10 @@ Global Instance join_handle_ne n l : Proof. solve_proper. Qed. (** The main proofs. *) -Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) : - to_val e = Some f → +Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) `{Hef : !IntoVal e f} : {{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}. 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. iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done. iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?". diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v index 1dcf85049b04cb0b13991192f73686427cc4f5bf..a9d2d5f3aa5b7c2a2eaba39ea2bc0562d48ca318 100644 --- a/theories/heap_lang/proofmode.v +++ b/theories/heap_lang/proofmode.v @@ -12,21 +12,7 @@ Ltac wp_bind_core K := | _ => 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]; simpl. - -(* Solves side-conditions generated specifically by wp_pure *) -Ltac wp_pure_done := - split_and?; wp_done. +Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl. Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ : PureExec φ e1 e2 → @@ -46,9 +32,9 @@ Tactic Notation "wp_pure" open_constr(efoc) := | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => unify e' efoc; eapply (tac_wp_pure K); - [unlock; simpl; apply _ (* PureExec *) - |wp_pure_done (* The pure condition for PureExec *) - |apply _ (* IntoLaters *) + [simpl; apply _ (* PureExec *) + |try fast_done (* The pure condition for PureExec *) + |apply _ (* IntoLaters *) |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: not a 'wp'" diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v index 23235b3c8a509a349a1748af4eaba650834d8c93..f51eb6f5d178f6620f12b686d3b1570c6e907370 100644 --- a/theories/program_logic/weakestpre.v +++ b/theories/program_logic/weakestpre.v @@ -215,12 +215,11 @@ Global Instance wp_mono' E e : Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ _ E e). 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. Lemma wp_value_fupd' E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ E {{ Φ }}. Proof. intros. by rewrite -wp_fupd -wp_value'. Qed. -Lemma wp_value_fupd E Φ e v : - to_val e = Some v → (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}. +Lemma wp_value_fupd E Φ e v `{!IntoVal e v} : (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}. 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 }}. @@ -290,7 +289,6 @@ Section proofmode_classes. ElimModal (|={E1,E2}=> P) P (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. - End proofmode_classes. Hint Extern 0 (atomic _) => assumption : typeclass_instances.