From 3742f4c2db08cf1dd59af6b9b51e422c59c9e199 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Sun, 18 Dec 2016 16:16:18 +0100
Subject: [PATCH] Adjust lifting lemmas for progress bits.

---
 theories/program_logic/ectx_language.v  |   2 +-
 theories/program_logic/ectx_lifting.v   | 129 ++++++++++++--
 theories/program_logic/ectxi_language.v |   2 +-
 theories/program_logic/lifting.v        |  25 +--
 theories/program_logic/ownp.v           | 216 +++++++++++++++++-------
 5 files changed, 288 insertions(+), 86 deletions(-)

diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 3bad0f053..21dda1f93 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -4,7 +4,7 @@ From iris.algebra Require Export base.
 From iris.program_logic Require Import language.
 Set Default Proof Using "Type".
 
-(* We need to make thos arguments indices that we want canonical structure
+(* We need to make those arguments indices that we want canonical structure
    inference to use a keys. *)
 Class EctxLanguage (expr val ectx state : Type) := {
   of_val : val → expr;
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 4dca79e7f..591e3f4e4 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -6,11 +6,13 @@ Set Default Proof Using "Type".
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
 Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
+Implicit Types p : bool.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types v : val.
 Implicit Types e : expr.
 Hint Resolve head_prim_reducible head_reducible_prim_step.
+Hint Resolve (reducible_not_val _ inhabitant).
 
 Definition head_progressive (e : expr) (σ : state) :=
   is_Some(to_val e) ∨ ∃ K e', e = fill K e' ∧ head_reducible e' σ.
@@ -25,11 +27,13 @@ Qed.
 Hint Resolve progressive_head_progressive.
 
 Lemma wp_ectx_bind {p E e} K Φ :
-  WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }} ⊢ WP fill K e @ p; E {{ Φ }}.
+  WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }}
+  ⊢ WP fill K e @ p; E {{ Φ }}.
 Proof. apply: weakestpre.wp_bind. Qed.
 
 Lemma wp_ectx_bind_inv {p E Φ} K e :
-  WP fill K e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }}.
+  WP fill K e @ p; E {{ Φ }}
+  ⊢ WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }}.
 Proof. apply: weakestpre.wp_bind_inv. Qed.
 
 Lemma wp_lift_head_step {p E Φ} e1 :
@@ -41,9 +45,28 @@ Lemma wp_lift_head_step {p E Φ} e1 :
   ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_step=>//. iIntros (σ1) "Hσ".
-  iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
-  iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%".
-  iApply "H". by eauto.
+  iMod ("H" with "Hσ") as "[% H]"; iModIntro.
+  iSplit; first by destruct p; eauto. iNext. iIntros (e2 σ2 efs) "%".
+  iApply "H"; eauto.
+Qed.
+
+(*
+  PDS: Discard. It's confusing. In practice, we just need rules
+  like wp_lift_head_{step,stuck}.
+*)
+Lemma wp_strong_lift_head_step p E Φ e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E,∅}=∗
+    ⌜if p then head_reducible e1 σ1 else True⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+      state_interp σ2 ∗ WP e2 @ p; E {{ Φ }}
+      ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
+Proof.
+  iIntros (?) "H". iApply wp_lift_step=>//. iIntros (σ1) "Hσ".
+  iMod ("H" with "Hσ") as "[% H]"; iModIntro.
+  iSplit; first by destruct p; eauto. iNext. iIntros (e2 σ2 efs) "%".
+  iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_head_stuck E Φ e :
@@ -52,7 +75,7 @@ Lemma wp_lift_head_stuck E Φ e :
   ⊢ WP e @ E ?{{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_stuck; first done.
-  iIntros (σ) "Hσ". iMod ("H" $! _ with "Hσ") as "%". iModIntro. by auto.
+  iIntros (σ) "Hσ". iMod ("H" with "Hσ") as "%". by auto. 
 Qed.
 
 Lemma wp_lift_pure_head_step {p E E' Φ} e1 :
@@ -63,42 +86,71 @@ Lemma wp_lift_pure_head_step {p E E' Φ} e1 :
   ⊢ WP e1 @ p; E {{ Φ }}.
 Proof using Hinh.
   iIntros (??) "H". iApply wp_lift_pure_step; eauto.
+  { by destruct p; auto. }
   iApply (step_fupd_wand with "H"); iIntros "H".
   iIntros (????). iApply "H"; eauto.
 Qed.
 
-Lemma wp_lift_pure_head_stuck `{Inhabited state} E Φ e :
+(* PDS: Discard. *)
+Lemma wp_strong_lift_pure_head_step p E Φ e1 :
+  to_val e1 = None →
+  (∀ σ1, if p then head_reducible e1 σ1 else True) →
+  (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
+  (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
+    WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
+Proof using Hinh.
+  iIntros (???) "H". iApply wp_lift_pure_step; eauto. by destruct p; auto.
+Qed.
+
+Lemma wp_lift_pure_head_stuck E Φ e :
   to_val e = None →
   (∀ K e1 σ1 e2 σ2 efs, e = fill K e1 → ¬ head_step e1 σ1 e2 σ2 efs) →
   WP e @ E ?{{ Φ }}%I.
-Proof.
+Proof using Hinh.
   iIntros (Hnv Hnstep). iApply wp_lift_head_stuck; first done.
   iIntros (σ) "_". iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
   iModIntro. iPureIntro. case; first by rewrite Hnv; case.
   move=>[] K [] e1 [] Hfill [] e2 [] σ2 [] efs /= Hstep. exact: Hnstep.
 Qed.
 
-Lemma wp_lift_atomic_head_step {p E Φ} e1 :
+Lemma wp_lift_atomic_head_step {E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 ∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ p; E {{ Φ }}.
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
   iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%". iApply "H"; auto.
 Qed.
 
-Lemma wp_lift_atomic_head_step_no_fork {p E Φ} e1 :
+(* PDS: Discard. *)
+Lemma wp_strong_lift_atomic_head_step {p E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜if p then head_reducible e1 σ1 else True⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      state_interp σ2 ∗ default False (to_val e2) Φ
+      ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
+Proof.
+  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
+  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
+  iSplit; first by destruct p; eauto.
+  by iNext; iIntros (e2 σ2 efs ?); iApply "H"; eauto.
+Qed.
+
+Lemma wp_lift_atomic_head_step_no_fork {E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
       ⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
-  ⊢ WP e1 @ p; E {{ Φ }}.
+  ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
@@ -106,13 +158,45 @@ Proof.
   iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
 Qed.
 
+(* PDS: Discard. *)
+Lemma wp_strong_lift_atomic_head_step_no_fork {p E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜if p then head_reducible e1 σ1 else True⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      ⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
+  ⊢ WP e1 @ p; E {{ Φ }}.
+Proof.
+  iIntros (?) "H". iApply wp_strong_lift_atomic_head_step; eauto.
+  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[$ H]"; iModIntro.
+  iNext; iIntros (v2 σ2 efs) "%".
+  iMod ("H" with "[#]") as "(% & $ & $)"=>//; subst.
+  by iApply big_sepL_nil.
+Qed.
+
 Lemma wp_lift_pure_det_head_step {p E E' Φ} e1 e2 efs :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs',
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
   (|={E,E'}▷=> WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
   ⊢ WP e1 @ p; E {{ Φ }}.
-Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
+Proof using Hinh.
+  intros. rewrite -(wp_lift_pure_det_step e1 e2 efs); eauto.
+  destruct p; by auto.
+Qed.
+
+(* PDS: Discard. *)
+Lemma wp_strong_lift_pure_det_head_step {p E Φ} e1 e2 efs :
+  to_val e1 = None →
+  (∀ σ1, if p then head_reducible e1 σ1 else True) →
+  (∀ σ1 e2' σ2 efs',
+    prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+  ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
+Proof using Hinh.
+  iIntros (???) "H"; iApply wp_lift_pure_det_step; eauto.
+  by destruct p; eauto.
+Qed.
 
 Lemma wp_lift_pure_det_head_step_no_fork {p E E' Φ} e1 e2 :
   to_val e1 = None →
@@ -122,6 +206,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {p E E' Φ} e1 e2 :
   (|={E,E'}▷=> WP e2 @ p; E {{ Φ }}) ⊢ WP e1 @ p; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
+  destruct p; by auto.
 Qed.
 
 Lemma wp_lift_pure_det_head_step_no_fork' {p E Φ} e1 e2 :
@@ -129,9 +214,21 @@ Lemma wp_lift_pure_det_head_step_no_fork' {p E Φ} e1 e2 :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs',
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
-  ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
+  ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
 Proof using Hinh.
-  intros. rewrite -[(WP e1 @ _; _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
+  intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
   rewrite -step_fupd_intro //.
 Qed.
+
+(* PDS: Discard. *)
+Lemma wp_strong_lift_pure_det_head_step_no_fork {p E Φ} e1 e2 :
+  to_val e1 = None →
+  (∀ σ1, if p then head_reducible e1 σ1 else True) →
+  (∀ σ1 e2' σ2 efs',
+    prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+  ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
+Proof using Hinh.
+  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
+  by destruct p; eauto.
+Qed.
 End wp.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 6475a921d..0e6d4f2e0 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -4,7 +4,7 @@ From iris.algebra Require Export base.
 From iris.program_logic Require Import language ectx_language.
 Set Default Proof Using "Type".
 
-(* We need to make thos arguments indices that we want canonical structure
+(* We need to make those arguments indices that we want canonical structure
    inference to use a keys. *)
 Class EctxiLanguage (expr val ectx_item state : Type) := {
   of_val : val → expr;
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index c013ded44..9923033c6 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -5,6 +5,7 @@ Set Default Proof Using "Type".
 
 Section lifting.
 Context `{irisG Λ Σ}.
+Implicit Types p : bool.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Implicit Types σ : state Λ.
@@ -14,7 +15,7 @@ Implicit Types Φ : val Λ → iProp Σ.
 Lemma wp_lift_step p E Φ e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
-    ⌜reducible e1 σ1⌝ ∗
+    ⌜if p then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
       state_interp σ2 ∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
   ⊢ WP e1 @ p; E {{ Φ }}.
@@ -36,17 +37,17 @@ Qed.
 
 (** Derived lifting lemmas. *)
 Lemma wp_lift_pure_step `{Inhabited (state Λ)} p E E' Φ e1 :
-  (∀ σ1, reducible e1 σ1) →
+  to_val e1 = None →
+  (∀ σ1, if p then reducible e1 σ1 else True) →
   (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
   (|={E,E'}▷=> ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
     WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
   ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
-  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
-  { eapply reducible_not_val, (Hsafe inhabitant). }
+  iIntros (? Hsafe Hstep) "H". iApply wp_lift_step; first done.
   iIntros (σ1) "Hσ". iMod "H".
-  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
-  iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
+  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver.
+  iSplit; first by iPureIntro; apply Hsafe. iNext. iIntros (e2 σ2 efs ?).
   destruct (Hstep σ1 e2 σ2 efs); auto; subst.
   iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
 Qed.
@@ -67,7 +68,7 @@ Qed.
 Lemma wp_lift_atomic_step {p E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
-    ⌜reducible e1 σ1⌝ ∗
+    ⌜if p then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 ∗
       default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
@@ -83,12 +84,13 @@ Proof.
 Qed.
 
 Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {p E E' Φ} e1 e2 efs :
-  (∀ σ1, reducible e1 σ1) →
+  to_val e1 = None →
+  (∀ σ1, if p then reducible e1 σ1 else true) →
   (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
   (|={E,E'}▷=> WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
   ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
-  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step p E); try done.
+  iIntros (?? Hpuredet) "H". iApply (wp_lift_pure_step p E E'); try done.
   { by intros; eapply Hpuredet. }
   iApply (step_fupd_wand with "H"); iIntros "H".
   by iIntros (e' efs' σ (_&->&->)%Hpuredet).
@@ -100,8 +102,9 @@ Lemma wp_pure_step_fupd `{Inhabited (state Λ)} E E' e1 e2 φ Φ :
   (|={E,E'}▷=> WP e2 @ E {{ Φ }}) ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros ([??] Hφ) "HWP".
-  iApply (wp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|].
-  rewrite big_sepL_nil right_id //.
+  iApply (wp_lift_pure_det_step with "[HWP]"); [|naive_solver|naive_solver|].
+  - apply (reducible_not_val _ inhabitant). by auto.
+  - by rewrite big_sepL_nil right_id.
 Qed.
 
 Lemma wp_pure_step_later `{Inhabited (state Λ)} E e1 e2 φ Φ :
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index dc9bd83a2..f326149af 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -61,7 +61,7 @@ Proof.
     as (γσ) "[Hσ Hσf]"; first done.
   iExists (λ σ, own γσ (● (Excl' (σ:leibnizC _)))). iFrame "Hσ".
   iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]"; first by rewrite /ownP.
-  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
+  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite/ownP.
   iDestruct (own_valid_2 with "Hσ Hσf")
     as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2; auto.
 Qed.
@@ -70,33 +70,36 @@ Qed.
 (** Lifting *)
 Section lifting.
   Context `{ownPG Λ Σ}.
+  Implicit Types p : bool.
   Implicit Types e : expr Λ.
   Implicit Types Φ : val Λ → iProp Σ.
 
+  Lemma ownP_eq σ1 σ2 : state_interp σ1 -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
+  Proof.
+    iIntros "Hσ1 Hσ2"; rewrite/ownP.
+    by iDestruct (own_valid_2 with "Hσ1 Hσ2")
+      as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+  Qed.
   Lemma ownP_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
   Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
   Global Instance ownP_timeless σ : Timeless (@ownP (state Λ) Σ _ σ).
   Proof. rewrite /ownP; apply _. Qed.
 
   Lemma ownP_lift_step p E Φ e1 :
-    (|={E,∅}=> ∃ σ1, ⌜reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
+    to_val e1 = None →
+    (|={E,∅}=> ∃ σ1, ⌜if p then reducible e1 σ1 else True⌝ ∗ ▷ ownP σ1 ∗
       ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
             ={∅,E}=∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
     ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
-    iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
-    - apply of_to_val in EQe1 as <-. iApply fupd_wp.
-      iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred%reducible_not_val.
-      move: Hred; by rewrite to_of_val.
-    - iApply wp_lift_step; [done|]; iIntros (σ1) "Hσ".
-      iMod "H" as (σ1' ?) "[>Hσf H]". rewrite /ownP.
-      iDestruct (own_valid_2 with "Hσ Hσf")
-        as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
-      iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
-      iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
-      { by apply auth_update, option_local_update,
-          (exclusive_local_update _ (Excl σ2)). }
-      iFrame "Hσ". iApply ("H" with "[]"); eauto.
+    iIntros (?) "H". iApply wp_lift_step; first done.
+    iIntros (σ1) "Hσ"; iMod "H" as (σ1') "(% & >Hσf & H)".
+    iDestruct (ownP_eq with "Hσ Hσf") as %->.
+    iModIntro. iSplit; first done. iNext. iIntros (e2 σ2 efs Hstep).
+    rewrite /ownP; iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
+    { by apply auth_update, option_local_update,
+        (exclusive_local_update _ (Excl σ2)). }
+    iFrame "Hσ". by iApply ("H" with "[]"); eauto.
   Qed.
 
   Lemma ownP_lift_stuck E Φ e :
@@ -108,57 +111,59 @@ Section lifting.
       iMod "H" as (σ1) "[#H _]"; iDestruct "H" as %Hstuck; exfalso.
       by apply Hstuck; left; rewrite to_of_val; exists v.
     - iApply wp_lift_stuck; [done|]; iIntros (σ1) "Hσ".
-      iMod "H" as (σ1') "(% & >Hσf)"; rewrite /ownP.
-      by iDestruct (own_valid_2 with "Hσ Hσf")
-        as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+      iMod "H" as (σ1') "(% & >Hσf)".
+      by iDestruct (ownP_eq with "Hσ Hσf") as %->.
   Qed.
 
-  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} p E Φ e1 :
-    (∀ σ1, reducible e1 σ1) →
+  Lemma ownP_lift_pure_step p E Φ e1 :
+    to_val e1 = None →
+    (∀ σ1, if p then reducible e1 σ1 else True) →
     (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
     (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
       WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
     ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
-    iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
-    { eapply reducible_not_val, (Hsafe inhabitant). }
+    iIntros (? Hsafe Hstep) "H"; iApply wp_lift_step; first done.
     iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-    iModIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
+    iModIntro; iSplit; [by destruct p|]; iNext; iIntros (e2 σ2 efs ?).
     destruct (Hstep σ1 e2 σ2 efs); auto; subst.
-    iMod "Hclose"; iModIntro. iFrame "Hσ". iApply "H"; auto.
+    by iMod "Hclose"; iModIntro; iFrame; iApply "H".
   Qed.
 
   (** Derived lifting lemmas. *)
   Lemma ownP_lift_atomic_step {p E Φ} e1 σ1 :
-    reducible e1 σ1 →
+    to_val e1 = None →
+    (if p then reducible e1 σ1 else True) →
     (▷ ownP σ1 ∗ ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
       default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
     ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
-    iIntros (?) "[Hσ H]". iApply ownP_lift_step.
-    iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver. iModIntro.
-    iExists σ1. iFrame "Hσ"; iSplit; eauto.
+    iIntros (??) "[Hσ H]"; iApply ownP_lift_step; first done.
+    iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
+    iModIntro; iExists σ1; iFrame; iSplit; first by destruct p.
     iNext; iIntros (e2 σ2 efs) "% Hσ".
     iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
     destruct (to_val e2) eqn:?; last by iExFalso.
-    iMod "Hclose". iApply wp_value; auto using to_of_val. done.
+    by iMod "Hclose"; iApply wp_value; auto using to_of_val.
   Qed.
 
   Lemma ownP_lift_atomic_det_step {p E Φ e1} σ1 v2 σ2 efs :
-    reducible e1 σ1 →
+    to_val e1 = None →
+    (if p then reducible e1 σ1 else True) →
     (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
                      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
     ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗
       Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
     ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
-    iIntros (? Hdet) "[Hσ1 Hσ2]". iApply ownP_lift_atomic_step; try done.
-    iFrame. iNext. iIntros (e2' σ2' efs') "% Hσ2'".
-    edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
+    iIntros (?? Hdet) "[Hσ1 Hσ2]"; iApply ownP_lift_atomic_step; try done.
+    iFrame; iNext; iIntros (e2' σ2' efs') "% Hσ2'".
+    edestruct Hdet as (->&Hval&->). done. by rewrite Hval; iApply "Hσ2".
   Qed.
 
   Lemma ownP_lift_atomic_det_step_no_fork {p E e1} σ1 v2 σ2 :
-    reducible e1 σ1 →
+    to_val e1 = None →
+    (if p then reducible e1 σ1 else True) →
     (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
       σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
     {{{ ▷ ownP σ1 }}} e1 @ p; E {{{ RET v2; ownP σ2 }}}.
@@ -167,19 +172,20 @@ Section lifting.
     rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
   Qed.
 
-  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {p E Φ} e1 e2 efs :
-    (∀ σ1, reducible e1 σ1) →
+  Lemma ownP_lift_pure_det_step {p E Φ} e1 e2 efs :
+    to_val e1 = None →
+    (∀ σ1, if p then reducible e1 σ1 else True) →
     (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
     ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤{{ _, True }})
     ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
-    iIntros (? Hpuredet) "?". iApply ownP_lift_pure_step; try done.
-    by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
+    iIntros (?? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
+    by apply Hpuredet. by iNext; iIntros (e' efs' σ (_&->&->)%Hpuredet).
   Qed.
 
   Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {p E Φ} e1 e2 :
     to_val e1 = None →
-    (∀ σ1, reducible e1 σ1) →
+    (∀ σ1, if p then reducible e1 σ1 else True) →
     (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
@@ -191,70 +197,166 @@ Section ectx_lifting.
   Import ectx_language.
   Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
   Context `{ownPG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
+  Implicit Types p : bool.
   Implicit Types Φ : val → iProp Σ.
   Implicit Types e : expr.
   Hint Resolve head_prim_reducible head_reducible_prim_step.
 
-  Lemma ownP_lift_head_step p E Φ e1 :
+  Lemma ownP_lift_head_step E Φ e1 :
+    to_val e1 = None →
     (|={E,∅}=> ∃ σ1, ⌜head_reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
       ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
-            ={∅,E}=∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤{{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+            ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
   Proof.
-    iIntros "H". iApply (ownP_lift_step p E); try done.
+    iIntros (?) "H". iApply ownP_lift_step; first done.
     iMod "H" as (σ1 ?) "[Hσ1 Hwp]". iModIntro. iExists σ1.
     iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
     iApply ("Hwp" with "[]"); eauto.
   Qed.
 
-  Lemma ownP_lift_pure_head_step p E Φ e1 :
+  (* PDS: Discard *)
+  Lemma ownP_strong_lift_head_step p E Φ e1 :
+    to_val e1 = None →
+    (|={E,∅}=> ∃ σ1, ⌜if p then head_reducible e1 σ1 else True⌝ ∗ ▷ ownP σ1 ∗
+      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
+            ={∅,E}=∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤{{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
+  Proof.
+    iIntros (?) "H"; iApply ownP_lift_step; first done.
+    iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1.
+    iSplit; first by destruct p; eauto. by iFrame.
+  Qed.
+
+  Lemma ownP_lift_pure_head_step E Φ e1 :
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
     (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
+      WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof using Hinh.
+    iIntros (??) "H". iApply ownP_lift_pure_step;
+      simpl; eauto using (reducible_not_val _ inhabitant).
+    iNext. iIntros (????). iApply "H"; eauto.
+  Qed.
+
+  (* PDS: Discard. *)
+  Lemma ownP_strong_lift_pure_head_step p E Φ e1 :
+    to_val e1 = None →
+    (∀ σ1, if p then head_reducible e1 σ1 else True) →
+    (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
+    (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
       WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
     ⊢ WP e1 @ p; E {{ Φ }}.
   Proof using Hinh.
-    iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext.
-    iIntros (????). iApply "H". eauto.
+    iIntros (???) "H". iApply ownP_lift_pure_step; eauto.
+    by destruct p; eauto.
   Qed.
 
-  Lemma ownP_lift_atomic_head_step {p E Φ} e1 σ1 :
+  Lemma ownP_lift_atomic_head_step {E Φ} e1 σ1 :
     head_reducible e1 σ1 →
     ▷ ownP σ1 ∗ ▷ (∀ e2 σ2 efs,
     ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    iIntros (?) "[? H]". iApply ownP_lift_atomic_step;
+      simpl; eauto using reducible_not_val.
+    iFrame. iNext. iIntros (???) "% ?". iApply ("H" with "[]"); eauto.
+  Qed.
+
+  (* PDS: Discard. *)
+  Lemma ownP_strong_lift_atomic_head_step {p E Φ} e1 σ1 :
+    to_val e1 = None →
+    (if p then head_reducible e1 σ1 else True) →
+    ▷ ownP σ1 ∗ ▷ (∀ e2 σ2 efs,
+    ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
       default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
     ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
-    iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto. iFrame. iNext.
-    iIntros (???) "% ?". iApply ("H" with "[]"); eauto.
+    iIntros (??) "[? H]". iApply ownP_lift_atomic_step; eauto; try iFrame.
+    by destruct p; eauto.
   Qed.
 
-  Lemma ownP_lift_atomic_det_head_step {p E Φ e1} σ1 v2 σ2 efs :
+  Lemma ownP_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
     head_reducible e1 σ1 →
     (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
       σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
+    ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    by eauto 10 using ownP_lift_atomic_det_step, reducible_not_val.
+  Qed.
+
+  Lemma ownP_strong_lift_atomic_det_head_step {p E Φ e1} σ1 v2 σ2 efs :
+    to_val e1 = None →
+    (if p then head_reducible e1 σ1 else True) →
+    (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
+      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
     ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
     ⊢ WP e1 @ p; E {{ Φ }}.
-  Proof. eauto using ownP_lift_atomic_det_step. Qed.
+  Proof.
+    by destruct p; eauto 10 using ownP_lift_atomic_det_step.
+  Qed.
 
-  Lemma ownP_lift_atomic_det_head_step_no_fork {p E e1} σ1 v2 σ2 :
+  Lemma ownP_lift_atomic_det_head_step_no_fork {E e1} σ1 v2 σ2 :
     head_reducible e1 σ1 →
     (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
       σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
+    {{{ ▷ ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
+  Proof.
+    by eauto 10 using ownP_lift_atomic_det_step_no_fork, reducible_not_val.
+  Qed.
+
+  (* PDS: Discard. *)
+  Lemma ownP_strong_lift_atomic_det_head_step_no_fork {p E e1} σ1 v2 σ2 :
+    to_val e1 = None →
+    (if p then head_reducible e1 σ1 else True) →
+    (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
+      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
     {{{ ▷ ownP σ1 }}} e1 @ p; E {{{ RET v2; ownP σ2 }}}.
-  Proof. eauto using ownP_lift_atomic_det_step_no_fork. Qed.
+  Proof.
+    intros ???; apply ownP_lift_atomic_det_step_no_fork; eauto.
+    by destruct p; eauto.
+  Qed.
 
-  Lemma ownP_lift_pure_det_head_step {p E Φ} e1 e2 efs :
+  Lemma ownP_lift_pure_det_head_step {E Φ} e1 e2 efs :
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+    ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof using Hinh.
+    intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_step;
+    eauto using (reducible_not_val _ inhabitant).
+  Qed.
+
+  (* PDS: Discard. *)
+  Lemma ownP_strong_lift_pure_det_head_step {p E Φ} e1 e2 efs :
+    to_val e1 = None →
+    (∀ σ1, if p then head_reducible e1 σ1 else True) →
+    (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
     ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
     ⊢ WP e1 @ p; E {{ Φ }}.
-  Proof using Hinh. eauto using ownP_lift_pure_det_step. Qed.
+  Proof using Hinh.
+    iIntros (???) "H"; iApply wp_lift_pure_det_step; eauto.
+    by destruct p; eauto.
+  Qed.
 
-  Lemma ownP_lift_pure_det_head_step_no_fork {p E Φ} e1 e2 :
+  Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
     to_val e1 = None →
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
+  Proof using Hinh. by eauto using ownP_lift_pure_det_step_no_fork. Qed.
+
+  (* PDS: Discard. *)
+  Lemma ownP_strong_lift_pure_det_head_step_no_fork {p E Φ} e1 e2 :
+    to_val e1 = None →
+    (∀ σ1, if p then head_reducible e1 σ1 else True) →
+    (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
-  Proof using Hinh. eauto using ownP_lift_pure_det_step_no_fork. Qed.
+  Proof using Hinh.
+    iIntros (???) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
+    by destruct p; eauto.
+  Qed.
 End ectx_lifting.
-- 
GitLab