diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v index 4f97b4544cc81ad8b7eceb51f9be11b45dc3be1b..7c374b4c5b238dc8b5f71d233e231073764ae51c 100644 --- a/theories/heap_lang/proofmode.v +++ b/theories/heap_lang/proofmode.v @@ -5,15 +5,15 @@ From iris.heap_lang Require Export tactics lifting. Set Default Proof Using "Type". Import uPred. -Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ : +Lemma tac_wp_pure `{heapG Σ} Δ Δ' E e1 e2 φ Φ : PureExec φ e1 e2 → φ → IntoLaterNEnvs 1 Δ Δ' → - envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) → - envs_entails Δ (WP fill K e1 @ E {{ Φ }}). + envs_entails Δ' (WP e2 @ E {{ Φ }}) → + envs_entails Δ (WP e1 @ E {{ Φ }}). Proof. rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=. - rewrite -wp_bind HΔ' -wp_pure_step_later //. by rewrite -wp_bind_inv. + rewrite HΔ' -wp_pure_step_later //. Qed. Lemma tac_wp_value `{heapG Σ} Δ E Φ e v : @@ -28,11 +28,12 @@ Tactic Notation "wp_pure" open_constr(efoc) := lazymatch goal with | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' => unify e' efoc; - eapply (tac_wp_pure K); - [simpl; apply _ (* PureExec *) + eapply tac_wp_pure; + [simpl; change e with (fill K e'); apply _ (* PureExec *) |try fast_done (* The pure condition for PureExec *) |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: not a 'wp'" end. diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v index 660965699c6e6b5d91f7a630b067b4129809a79d..365b9f2216ea451793809b9972f4a6b8225207a9 100644 --- a/theories/program_logic/language.v +++ b/theories/program_logic/language.v @@ -140,6 +140,19 @@ Section language. PureExec P e1 e2. Proof. intros HPE. split; intros; eapply HPE; eauto. Qed. + Global Instance pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ : + PureExec φ e1 e2 → + PureExec φ (K e1) (K e2). + Proof. + intros [Hred Hstep]. split. + - intros σ ?. destruct (Hred σ) as (? & ? & ? & ?); first done. + do 3 eexists. eapply fill_step. done. + - intros σ ???? Hpstep. edestruct fill_step_inv as (? & ? & ?); [|exact Hpstep|]. + + destruct (Hred σ) as (? & ? & ? & ?); first done. + eapply val_stuck. done. + + edestruct Hstep as (? & ? & ?); [done..|]. by subst. + Qed. + (* This is a family of frequent assumptions for PureExec *) Class IntoVal (e : expr Λ) (v : val Λ) := into_val : to_val e = Some v.