Do not try to lift with conditional head_reducibility.

theories/program_logic/ectx_language.v

@@ -61,6 +61,8 @@ Section ectx_language.
     ∃ e' σ' efs, head_step e σ e' σ' efs.
   Definition head_irreducible (e : expr) (σ : state) :=
     ∀ e' σ' efs, ¬head_step e σ e' σ' efs.
+  Definition head_progressive (e : expr) (σ : state) :=
+    is_Some(to_val e) ∨ ∃ K e', e = fill K e' ∧ head_reducible e' σ.
 
   (* All non-value redexes are at the root.  In other words, all sub-redexes are
      values. *)
@@ -117,6 +119,14 @@ Section ectx_language.
     rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible.
   Qed.
 
+  Lemma progressive_head_progressive e σ :
+    progressive e σ → head_progressive e σ.
+  Proof.
+    case=>[?|Hred]; first by left.
+    right. move: Hred=> [] e' [] σ' [] efs [] K e1' e2' EQ EQ' Hstep. subst.
+    exists K, e1'. split; first done. by exists e2', σ', efs.
+  Qed.
+
   Lemma ectx_language_strong_atomic e :
     (∀ σ e' σ' efs, head_step e σ e' σ' efs → is_Some (to_val e')) →
     sub_redexes_are_values e →

theories/program_logic/ectx_lifting.v

@@ -13,17 +13,6 @@ 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' σ.
-
-Lemma progressive_head_progressive e σ :
-  progressive e σ → head_progressive e σ.
-Proof.
-  case=>[?|Hred]; first by left.
-  right. move: Hred=> [] e' [] σ' [] efs [] K e1' e2' EQ EQ' Hstep. subst.
-  exists K, e1'. split; first done. by exists e2', σ', efs.
-Qed.
 Hint Resolve progressive_head_progressive.
 
 Lemma wp_ectx_bind {p E e} K Φ :
@@ -50,25 +39,6 @@ Proof.
   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 :
   to_val e = None →
   (∀ σ, state_interp σ ={E,∅}=∗ ⌜¬ head_progressive e σ⌝)
@@ -91,18 +61,6 @@ Proof using Hinh.
   iIntros (????). iApply "H"; eauto.
 Qed.
 
-(* 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) →
@@ -114,43 +72,28 @@ Proof using Hinh.
   move=>[] K [] e1 [] Hfill [] e2 [] σ2 [] efs /= Hstep. exact: Hnstep.
 Qed.
 
-Lemma wp_lift_atomic_head_step {E Φ} e1 :
+Lemma wp_lift_atomic_head_step {p 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 {{ _, 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.
-
-(* 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 }})
+      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.
+  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iSplit; first by destruct p; auto. iNext. iIntros (e2 σ2 efs) "%".
+  iApply "H"; auto.
 Qed.
 
-Lemma wp_lift_atomic_head_step_no_fork {E Φ} e1 :
+Lemma wp_lift_atomic_head_step_no_fork {p 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 @ E {{ Φ }}.
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
@@ -158,22 +101,6 @@ 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',
@@ -185,19 +112,6 @@ Proof using Hinh.
   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 →
   (∀ σ1, head_reducible e1 σ1) →
@@ -219,16 +133,4 @@ Proof using Hinh.
   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.

theories/program_logic/ownp.v

@@ -201,140 +201,82 @@ Section ectx_lifting.
   Implicit Types Φ : val → iProp Σ.
   Implicit Types e : expr.
   Hint Resolve head_prim_reducible head_reducible_prim_step.
+  Hint Resolve (reducible_not_val _ inhabitant).
+  Hint Resolve progressive_head_progressive.
 
-  Lemma ownP_lift_head_step E Φ e1 :
+  Lemma ownP_lift_head_step p 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 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+            ={∅,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 eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
+    iSplit; first by destruct p; eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
     iApply ("Hwp" with "[]"); eauto.
   Qed.
 
-  (* 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 {{ Φ }}.
+  Lemma ownP_lift_head_stuck E Φ e :
+    (|={E,∅}=> ∃ σ, ⌜¬ head_progressive e σ⌝ ∗ ▷ ownP σ)
+    ⊢ WP e @ 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.
+    iIntros "H". iApply ownP_lift_stuck. iMod "H" as (σ) "[% >Hσ]".
+    iModIntro. iExists σ. iFrame "Hσ". by eauto.
   Qed.
 
-  Lemma ownP_lift_pure_head_step E Φ e1 :
+  Lemma ownP_lift_pure_head_step p E Φ e1 :
+    to_val e1 = None →
     (∀ σ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.
-    by destruct p; eauto.
+    iIntros (???) "H".  iApply ownP_lift_pure_step; eauto.
+    { by destruct p; auto. }
+    iNext. iIntros (????). iApply "H"; eauto.
   Qed.
 
-  Lemma ownP_lift_atomic_head_step {E Φ} e1 σ1 :
+  Lemma ownP_lift_atomic_head_step {p E Φ} e1 σ1 :
+    to_val e1 = None →
     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; try iFrame.
-    by destruct p; eauto.
+    iIntros (??) "[? H]". iApply ownP_lift_atomic_step; eauto.
+    { by destruct p; eauto. }
+    iFrame. iNext. iIntros (???) "% ?". iApply ("H" with "[]"); eauto.
   Qed.
 
-  Lemma ownP_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
+  Lemma ownP_lift_atomic_det_head_step {p E Φ e1} σ1 v2 σ2 efs :
+    to_val e1 = None →
     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.
     by destruct p; eauto 10 using ownP_lift_atomic_det_step.
   Qed.
 
-  Lemma ownP_lift_atomic_det_head_step_no_fork {E e1} σ1 v2 σ2 :
+  Lemma ownP_lift_atomic_det_head_step_no_fork {p E e1} σ1 v2 σ2 :
+    to_val e1 = None →
     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.
     intros ???; apply ownP_lift_atomic_det_step_no_fork; eauto.
     by destruct p; eauto.
   Qed.
 
-  Lemma ownP_lift_pure_det_head_step {E Φ} e1 e2 efs :
+  Lemma ownP_lift_pure_det_head_step {p E Φ} e1 e2 efs :
+    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 = 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.
@@ -342,18 +284,10 @@ Section ectx_lifting.
     by destruct p; eauto.
   Qed.
 
-  Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
+  Lemma ownP_lift_pure_det_head_step_no_fork {p 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.
     iIntros (???) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.