From 5e472be656560a8cde9dc13fb9dfc7c2478c3697 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Oct 2017 11:25:50 +0900
Subject: [PATCH] Generalize `det_head_step_pureexec`.

---
 theories/heap_lang/lifting.v           |  1 -
 theories/program_logic/ectx_language.v | 16 ++++++++--------
 2 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index b893ce3c7..6d6e5762e 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -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)
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 0e4be8c5c..78bc50820 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -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.
 
-- 
GitLab