Commit 5e472be6 authored by Robbert Krebbers's avatar Robbert Krebbers

Generalize `det_head_step_pureexec`.

parent 5ed394dd
......@@ -87,7 +87,6 @@ Local Ltac solve_pureexec :=
| H: IntoVal ?e _ |- _ => rewrite -(of_to_val e _ into_val); clear H
| H: AsRec _ _ _ _ |- _ => rewrite H; clear H
end;
apply hoist_pred_pureexec; intros; destruct_and?;
apply det_head_step_pureexec; [ solve_exec_safe | solve_exec_puredet ].
Global Instance pure_rec f x (erec e1 e2 : expr) (v2 : val)
......
......@@ -151,16 +151,16 @@ Section ectx_language.
econstructor; eauto.
Qed.
Lemma det_head_step_pureexec e1 e2 :
( σ, head_reducible e1 σ)
( σ1 e2' σ2 efs, head_step e1 σ1 e2' σ2 efs σ1 = σ2 e2=e2' efs = [])
PureExec True e1 e2.
Lemma det_head_step_pureexec (P : Prop) e1 e2 :
( σ, P head_reducible e1 σ)
( σ1 e2' σ2 efs,
P head_step e1 σ1 e2' σ2 efs σ1 = σ2 e2=e2' efs = [])
PureExec P e1 e2.
Proof.
intros Hp1 Hp2. split.
- intros σ _. destruct (Hp1 σ) as (e2' & σ2 & efs & ?).
eexists e2', σ2, efs.
eapply (Ectx_step _ _ _ _ _ empty_ectx); eauto using fill_empty.
- intros σ1 e2' σ2 efs _ ?%head_reducible_prim_step; eauto.
- intros σ ?. destruct (Hp1 σ) as (e2' & σ2 & efs & ?); first done.
eexists e2', σ2, efs. by apply head_prim_step.
- intros σ1 e2' σ2 efs ? ?%head_reducible_prim_step; eauto.
Qed.
End ectx_language.
......
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