Define PureExec for general language

theories/heap_lang/lifting.v

@@ -83,7 +83,8 @@ Qed.
 Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
 Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
 Local Ltac solve_pureexec :=
-  intros; split; intros ?; destruct_and?; [ solve_exec_safe | solve_exec_puredet ].
+  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 v2 :
   PureExec (to_val e2 = Some v2 ∧ e1 = Rec f x erec ∧ Closed (f :b: x :b: []) erec)
@@ -194,7 +195,7 @@ Qed.
 Lemma wp_seq E e1 e2 Φ :
   is_Some (to_val e1) → Closed [] e2 →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?). rewrite -(wp_pure' []); by eauto. Qed.
+Proof. iIntros ([? ?] ?). rewrite -wp_pure'; by eauto. Qed.
 
 Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
 Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
@@ -202,11 +203,11 @@ Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
 Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
   is_Some (to_val e0) → Closed (x1 :b: []) e1 →
   ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?) "?". do 2 (iApply (wp_pure' []); eauto). Qed.
+Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure'; by eauto. Qed.
 
 Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
   is_Some (to_val e0) → Closed (x2 :b: []) e2 →
   ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?) "?". do 2 (iApply (wp_pure' []); eauto). Qed.
+Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure'; by eauto. Qed.
 
 End lifting.

theories/heap_lang/proofmode.v

@@ -46,9 +46,9 @@ Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
   (Δ' ⊢ WP fill K e2 @ E {{ Φ }}) →
   (Δ ⊢ WP fill K e1 @ E {{ Φ }}).
 Proof.
-  intros ??? HΔ'.
-  rewrite into_laterN_env_sound /=.
-  rewrite HΔ' -wp_pure' //.
+  intros ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite -lifting.wp_bind HΔ' -wp_pure' //.
+  by rewrite -ectx_lifting.wp_ectx_bind_inv.
 Qed.
 
 Tactic Notation "wp_pure" open_constr(efoc) :=

theories/program_logic/pure.v

 From iris.proofmode Require Import tactics.
-From iris.program_logic Require Import ectx_lifting.
+From iris.program_logic Require Import lifting language ectx_language.
 Set Default Proof Using "Type".
 
-Section pure.
-Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-Context `{irisG (ectx_lang expr) Σ}.
-Implicit Types P : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-Implicit Types v : val.
-Implicit Types e : expr.
+Section pure_language.
+Context `{irisG Λ Σ}.
+Implicit Types Φ : val Λ → iProp Σ.
+Implicit Types φ : Prop.
+Implicit Types e : expr Λ.
 
-Class PureExec (P : Prop) (e1 e2 : expr) := {
+Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
   pure_exec_safe : 
-    P -> ∀ σ, head_reducible e1 σ;
+    P -> ∀ σ, language.reducible e1 σ;
   pure_exec_puredet : 
-    P -> ∀ σ1 e2' σ2 efs, head_step e1 σ1 e2' σ2 efs -> σ1=σ2 /\ e2=e2' /\ [] = efs;
+    P -> ∀ σ1 e2' σ2 efs, language.prim_step e1 σ1 e2' σ2 efs -> σ1=σ2 /\ e2=e2' /\ [] = efs;
   }.
 
-Lemma wp_pure `{Inhabited state} K E E' e1 e2 φ Φ :
+Lemma wp_pure `{Inhabited (state Λ)} E E' e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
-  (|={E,E'}▷=> WP fill K e2 @ E {{ Φ }}) ⊢ WP fill K e1 @ E {{ Φ }}.
+  (|={E,E'}▷=> WP e2 @ E {{ Φ }}) ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (? Hφ) "HWP".
-  iApply wp_bind.
-  iApply (wp_lift_pure_det_head_step_no_fork with "[HWP]").
-  { destruct (pure_exec_safe Hφ inhabitant) as (? & ? & ? & Hst).
-    eapply ectx_language.val_stuck.
-    apply Hst. }
+  iApply (wp_lift_pure_det_step with "[HWP]").
   { apply (pure_exec_safe Hφ). }
   { apply (pure_exec_puredet Hφ). }
-  iApply wp_bind_inv.
-  iExact "HWP".
+  rewrite big_sepL_nil right_id //.
 Qed.
 
-
-Lemma wp_pure' `{Inhabited state} K E e1 e2 φ Φ :
+Lemma wp_pure' `{Inhabited (state Λ)} E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
-  (▷ WP fill K e2 @ E {{ Φ }}) ⊢ WP fill K e1 @ E {{ Φ }}.
+  (▷ WP e2 @ E {{ Φ }}) ⊢ WP e1 @ E {{ Φ }}.
 Proof. 
   intros ? ?.
   rewrite -wp_pure //.
   rewrite -step_fupd_intro //.
 Qed.
 
-End pure.
+Lemma hoist_pred_pureexec (P : Prop) (e1 e2 : expr Λ) :
+  (P → PureExec True e1 e2) →
+  PureExec P e1 e2.
+Proof.
+  intros HPE.
+  split; intros HP; destruct (HPE HP); eauto.
+Qed.
+
+End pure_language.
+
+Section pure_ectx_language.
+Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
+Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
+
+Lemma det_head_step_pureexec (e1 e2 : expr) :
+  (∀ σ, head_reducible e1 σ) →
+  (∀ σ1 e2' σ2 efs, head_step e1 σ1 e2' σ2 efs -> σ1=σ2 /\ e2=e2' /\ [] = efs) →
+  PureExec True e1 e2.
+Proof.
+  intros Hp1 Hp2.
+  split; intros _.
+  - intros σ. destruct (Hp1 σ) as (? & ? & ? & ?).
+    do 3 eexists. simpl.
+    eapply (Ectx_step _ _ _ _ _ empty_ectx); eauto using fill_empty.
+  - move => σ1 e2' σ2 efs /=.
+    intros ?%head_reducible_prim_step; eauto.
+Qed.
+
+End pure_ectx_language.